Issues with identifiers in DM4F affecting extraction

[victor-dumitrescu]

Some names used internally in DM4F are not valid OCaml identifiers, causing syntax errors in the extracted code. The examples I've hit so far are:

• variables beginning with uppercase letter, when the name of the user defined effect also begins with an uppercase letter (e.g. in examples/dm4free/FStar.DM4F.Exceptions.fst, for effect EXN, extracting let EXN___proj__EXN__item__raise_elab e uu____234 = ...
• names containing ^ or - (e.g. g^w)

Some quick fixes would be to either generate these names slightly differently in DM4F or to modify them afterwards if extracting.

[mtzguido]

I think this might be fixed in my branch guido_bug1001 (f6baab15), but I'm having a hard time trying to compile the extracted code, so I'm not completely sure.

Just making a note so we don't forget.

[msprotz]

FYI the code to find a good name for a given let-bound variable is there: https://github.com/FStarLang/FStar/blob/master/src/extraction/FStar.Extraction.ML.UEnv.fs#L193 so you could conceivably change this code to make sure it doesn't shadow anything, but also to make sure it picks a valid OCaml identifier.

[mtzguido]

That sounds like a good change too! But should we really have these kind of names generated by DM4F?

They're also invalid F* names, it just doesn't matter only since it's all internal to the compiler (as far as I understand)

[mtzguido]

Pushed a change as per Jonathan's suggestion to the guido_bug1001 branch. Tests run OK, but if any of you could review to see if it's sane that'd be great.