Merge pull request #3025 from FStarLang/guido_deepcompress

deep_compress: remove some spurious warnings about Tm_names

src/syntax/FStar.Syntax.Compress.fst

@@ -13,15 +13,15 @@ module Err = FStar.Errors
 (* This function really just checks for bad(tm) things happening, the
 actual `compress` call is done by the visitor, so no need to repeat it
 here. Morally, `deep_compress` is just `visit id` with some checks. *)
-let compress1_t (allow_uvars:bool) : term -> term =
+let compress1_t (allow_uvars: bool) (allow_names: bool) : term -> term =
   fun t ->
     let mk x = Syntax.mk x t.pos in
     match t.n with
     | Tm_uvar (uv, s) when not allow_uvars ->
       Err.raise_err (Err.Error_UnexpectedUnresolvedUvar,
                      format1 "Internal error: unexpected unresolved uvar in deep_compress: %s" (string_of_int (Unionfind.uvar_id uv.ctx_uvar_head)))
 
-    | Tm_name bv when not allow_uvars ->
+    | Tm_name bv when not allow_names ->
       (* This currently happens, and often, but it should not! *)
       if Options.debug_any () then
         Errors.log_issue t.pos (Err.Warning_NameEscape, format1 "Tm_name %s in deep compress" (Syntax.Print.bv_to_string bv));
@@ -63,29 +63,31 @@ function.
 [1] OCaml's Marshal module can actually serialize closures, but this
 makes .checked files more brittle, so we don't do it.
 *)
-let deep_compress (allow_uvars:bool) (tm : term) : term =
+let deep_compress (allow_uvars:bool) (allow_names: bool) (tm : term) : term =
   Err.with_ctx ("While deep-compressing a term") (fun () ->
     Visit.visit_term_univs
-      (compress1_t allow_uvars)
+      (compress1_t allow_uvars allow_names)
       (compress1_u allow_uvars)
       tm
   )
 
+let deep_compress_uvars = deep_compress false true
+
 let deep_compress_if_no_uvars (tm : term) : option term =
   Err.with_ctx ("While deep-compressing a term") (fun () ->
     try 
       Some (Visit.visit_term_univs
-              (compress1_t false)
+              (compress1_t false true)
               (compress1_u false)
               tm)
     with
     | FStar.Errors.Err (Err.Error_UnexpectedUnresolvedUvar, _, _) -> None
   )
 
-let deep_compress_se (allow_uvars:bool) (se : sigelt) : sigelt =
+let deep_compress_se (allow_uvars:bool) (allow_names:bool) (se : sigelt) : sigelt =
   Err.with_ctx (format1 "While deep-compressing %s" (Syntax.Print.sigelt_to_string_short se)) (fun () ->
     Visit.visit_sigelt
-      (compress1_t allow_uvars)
+      (compress1_t allow_uvars allow_names)
       (compress1_u allow_uvars)
       se
   )

src/syntax/FStar.Syntax.Compress.fsti

@@ -6,10 +6,14 @@ open FStar.Syntax.Syntax
 if allow_uvars is false, it raises a hard error if an *unresolved* uvar
 (term or universe) remains. Resolved uvars are replaced by their
 solutions, as in compress. *)
-val deep_compress (allow_uvars: bool) (t:term) : term
+val deep_compress (allow_uvars: bool) (allow_names: bool) (t:term) : term
 
-(* Similar to `deep_compress false t`, except instead of a hard error
+(* Alias for deep_compress false true. i.e. allows names but not uvars,
+useful to check that a potentially open term does not have any uvars. *)
+val deep_compress_uvars (t:term) : term
+
+(* Similar to `deep_compress false false t`, except instead of a hard error
    this returns None in case an unresolved uvar is found. *)
 val deep_compress_if_no_uvars (t:term) : option term
 
-val deep_compress_se (allow_uvars: bool) (se:sigelt) : sigelt
+val deep_compress_se (allow_uvars: bool) (allow_names: bool) (se:sigelt) : sigelt