[CakeML] Behaviour of evaluate_dec

[Yong Kiam]

Hi Lars,

That sounds like what the HOL-to-CakeML translator does. You might want to
look at the translator/ directory, and at Magnus and Scott's ICFP/JFP
paper: https://cakeml.org/jfp14.pdf

Specifically, I think ml_translatorScript (Eval_def) does it for
expressions and mlProgScript lifts it up to decs.

On Mon, May 29, 2017 at 3:41 AM, Lars Hupel <hupel at in.tum.de> wrote:

> > The c field is for new data constructors. let rec doesn’t make any new
> data constructors, so it is empty. The result for each declaration (for
> both variables and constructors) is not cumulative, but just the
> definitions that that declaration makes.
>
> I see. Is the following use case supported somehow:
>
> I want to go through a list of declarations (containing only types and
> let rec) and observe the resulting cumulative environment env', starting
> with an empty environment. I then want to prove some properties about
> evaluation of expressions in env'.
>
> Cheers
> Lars
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170529/88c382fb/attachment.html>