Reducing the amount of Tm_names in checked files #2845
Conversation
For debugging. This requires a small change to getopt to return Success (instead of Help) when no file was provided.
Also use it over sigelts after elim_uvars has run, and just before serializing a module, in order to make sure there are no free names in the terms
Also forbid them from mentioning external local variables.
| let tc_modul (env0:env) (m:modul) (iface_exists:bool) :(modul * env) = | ||
| let msg = "Internals for " ^ string_of_lid m.name in | ||
| //AR: push env, this will also push solver, and then finish_partial_modul will do the pop | ||
| let env0 = push_context env0 msg in | ||
| let modul, env = tc_partial_modul env0 m in | ||
| // Compress all sigelts so we write a good checked file, plus we make | ||
| // sure that we are not leaking uvars, names, etc. | ||
| let modul = deep_compress_modul modul in |
There was a problem hiding this comment.
I wonder if this compression can happen after type checking each sigelt, so that even when we add them to the typechecking environment, we know they are sane.
There was a problem hiding this comment.
Good point, let me try that.
| @@ -3305,7 +3304,7 @@ let rec elim_uvars (env:Env.env) (s:sigelt) = | |||
| | Sig_let((b, lbs), lids) -> | |||
| let lbs = lbs |> List.map (fun lb -> | |||
| let opening, lbunivs = Subst.univ_var_opening lb.lbunivs in | |||
| let elim t = Subst.deep_compress false (Subst.close_univ_vars lbunivs (remove_uvar_solutions env (Subst.subst opening t))) in | |||
| let elim t = Subst.close_univ_vars lbunivs (remove_uvar_solutions env (Subst.subst opening t)) in | |||
There was a problem hiding this comment.
The deep_compress calls are not needed because remove_uvar already removes all the uvars?
There was a problem hiding this comment.
Yes, but also, I would like to make deep_compress fail if it find a Tm_name as we are not supposed to write those to checked files. In the line removed above, the binders have been opened so that is not true, and we would could not raise an error then. Here the same applies for universe names.
| @@ -180,10 +180,69 @@ and letbinding = { //let f : forall u1..un. M t = e | |||
| lbattrs:list attribute; //attrs | |||
| lbpos :range; //original position of 'e' | |||
| } | |||
| and antiquotations = list (bv * term) | |||
| and antiquotations = int * list term | |||
There was a problem hiding this comment.
Does it need a checked file version increment?
There was a problem hiding this comment.
Yes, thanks! Doing it now.
|
|
||
| open FStar.Syntax.Syntax | ||
|
|
||
| val visit_term : (term -> term) -> term -> term |
There was a problem hiding this comment.
Some docs/comments here would be useful, especially if there are some parts of the syntax that are not covered here?
| finish_partial_modul false iface_exists env modul | ||
|
|
||
| let load_checked_module (en:env) (m:modul) :env = | ||
| (* Another compression pass to make sure we are not loading a corrupt | ||
| module. *) | ||
| let m = deep_compress_modul m in |
There was a problem hiding this comment.
Can/should it be guarded under a debug flag?
|
Thanks @mtzguido, I added some minor comments, but looks good to me. |
|
The id_info_table should not be affected by this change (Nik mentioned to look at it today). I've left the additional load-time check of the checked files for now.. I don't think it's a noticeable performance hit (just measured and it's pretty much 0ms every time), but we could revisit that whenever. |
Following up on that gensym bug, this:
deep_compresswith it.--debug, when a Tm_name is being output into a checked file. I am hoping to remove all cases of this soon and make it into an error.deep_compressafter checking a module, instead of being called on each sigelt (indirectly, by elim_uvars). This is mostly due to the fact that it would have been hard to modify elim_uvars to properly detect escaping Tm_names. However we could still be more eager and compress each sigelt as we check them...