[CakeML] Behaviour of evaluate_dec

[Magnus Myreen]

On 29 May 2017 at 18:03, Yong Kiam <tanyongkiam at gmail.com> wrote:
> 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.

That's right. It sounds like you want to do what we do in:

https://github.com/CakeML/cakeml/blob/master/translator/ml_progScript.sml

Cheers,
Magnus


> 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
>
>
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>