search

CakeML / cakeml

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

implement stackLang to stackLang transformations #29

Closed myreen closed 8 years ago

xrchz commented 9 years ago

@myreen: What are these transformations?

myreen commented 9 years ago

They are:

  1. introduce the GC implementation into the stubs i.e. remove Alloc, not implemented yet
  2. remove stack operations, i.e. make them memory accesses
  3. renaming variables to match the actual target registers names

Implementing 1. will depend on the GC function used for the proof of the bvp-to-word compiler.

xrchz commented 8 years ago

@myreen is this done?

myreen commented 8 years ago

Yes On Fri, 13 May 2016 at 04:30, Ramana Kumar notifications@github.com wrote:

@myreen https://github.com/myreen is this done?

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/CakeML/cakeml/issues/29#issuecomment-218982710