search

CakeML / pure

A verified compiler for a lazy functional language
Other
32 stars 4 forks source link

Remove Box from ThunkLang #38

Closed myreen closed 1 year ago

myreen commented 1 year ago

The Box constructor is never used in ThunkLang, but was intended as an already evaluated thunk value. In discussions with @hrutvik, I realised that Box shouldn't be present in ThunkLang at all.

myreen commented 1 year ago

Note that this simplifies the ThunkLang value type. Currently, the Thunk constructor is defined:

  v = ... | Thunk (v + exp) | ...

Once Box is removed from exp, the value type should be:

  v = ... | Thunk exp | ...