search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
964 stars 84 forks source link

sharing of closure environments in semantics, for evaluation #6

Closed xrchz closed 1 week ago

xrchz commented 10 years ago

Want to share closure environments somehow to avoid an exponential blowup during evaluation. See cb15c30b601bd92e25cce965fdd43e88f078f09e.

xrchz commented 8 years ago

@SOwens is this still relevant?

SOwens commented 8 years ago

Yes.

Scott

On 2016/03/18, at 04:58, Ramana Kumar notifications@github.com wrote:

@SOwens is this still relevant?

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub

xrchz commented 5 years ago

What about now?

talsewell commented 5 years ago

Can I ask a scoping question?

The concern is that the env terms in Closure elements refer back to previous environments in a way that creates an exponentially large HOL term (with respect to counting constructors, for instance).

It would seem that the obvious thing to do would be to name the shared environment terms as constants, and avoid EVAL expanding those constant definitions. This is in fact exactly how ml_progLib sets things up. Is this sufficient? Is there a different use case in which a substantial program is created as a program term in HOL but ml_progLib is not involved?

xrchz commented 5 years ago

I can't think of any use case that isn't ml_progLib (but maybe I'm forgetting something). If there isn't one, can this be closed? @SOwens?

SOwens commented 5 years ago

Does ML prog lib give you a way to evaluate an arbitrary CakeML AST, or just ones being build from HOL terms?

Scott

On 2019/01/14, at 07:58, Ramana Kumar notifications@github.com wrote:

I can't think of any use case that isn't ml_progLib (but maybe I'm forgetting something). If there isn't one, can this be closed? @SOwens?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.

talsewell commented 5 years ago

@SOwens : The answer is sort-of neither. The main job of ml_progLib is to stitch together bits of CakeML AST into an entire program. I guess it handles the declaration level, providing an interface for adding the various kinds of thing, opening/closing modules, etc. It handles more stuff than what's extracted by the translator (for instance the current CakeML toplevel) but it isn't specifically written for completeness. You can probably construct most CakeML AST that way, but there might be cases that aren't possible.

The interface isn't exactly what you'd need if you were given a block of AST to evaluate either. Is there a use case for that?

xrchz commented 1 week ago

We no longer have a use case for evaluating the semantics fast (that isn't covered by ml_progLib).