search

CakeML / cakeml

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

Better names from the translator #123

Closed myreen closed 8 years ago

myreen commented 8 years ago

Currently the translator will add a _1, _2, _3 etc. after a name if that name has already been taken. This can be problematic as pointed out by Yong Kiam.

Here are two alternatives:

  1. have a long-names mode where a bvl_to_bvi$compile gets the name bvl_to_bvi_compile instead of just compile
  2. one could setup a mapping of preferences and the user of can say bvl_to_bvi$compile should be named bvl_compile

I prefer the long-names mode since it requires less user interaction.

tanyongkiam commented 8 years ago

I prefer the 1) mode too. See https://github.com/CakeML/cakeml/blob/master/compiler/bootstrap/translation/backend64ProgScript.sml#L241 for an example of manual proof for side conditions that is affected by the names.

myreen commented 8 years ago

I'll implement 1).

tanyongkiam commented 8 years ago

Works great, closed (w.r.t 91c977b)