Importing types from F* into Vale

[Chris-Hawblitzel]

We have a tool called importFStarTypes.exe that translates F* declarations into Vale declarations so that programmers don't have to write the Vale declarations by hand. This tool does not read F* files directly, but instead reads the output of fstar.exe --print_implicits --print_universes --print_effect_args --print_full_names --print_bound_var_types --ugly --dump_module. However, this output is meant more for informal debugging than as a formal language. As a result, the output is hard to parse and is not stable across F* releases.

I'd like to have a more stable, parseable format for exchanging expressions and declarations between F* and importFStarTypes. I'd suggest the following:

• Take a subset of the standard syntax for F* expressions and declarations, which looks nice
• Add some extra mandatory parentheses so that there's a yacc grammar with no conflicts and so that there's more room to add additional information
• Anything that isn't already part of F*'s standard syntax (e.g. <ascribed: [Prims.PURE]) would be printed as attributes inside the expression, maybe using [@...] syntax, so that tools could ignore unknown or irrelevant attributes