Merge pull request #2996 from FStarLang/_nik_ide_id_info

Fixing the need to use --ide_id_info_off in Steel and Pulse

src/syntax/FStar.Syntax.Compress.fst

@@ -71,6 +71,17 @@ let deep_compress (allow_uvars:bool) (tm : term) : term =
       tm
   )
 
+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_u false)
+              tm)
+    with
+    | FStar.Errors.Err (Err.Error_UnexpectedUnresolvedUvar, _, _) -> None
+  )
+
 let deep_compress_se (allow_uvars:bool) (se : sigelt) : sigelt =
   Err.with_ctx (format1 "While deep-compressing %s" (Syntax.Print.sigelt_to_string_short se)) (fun () ->
     Visit.visit_sigelt

src/syntax/FStar.Syntax.Compress.fsti

@@ -8,4 +8,8 @@ if allow_uvars is false, it raises a hard error if an *unresolved* uvar
 solutions, as in compress. *)
 val deep_compress (allow_uvars: bool) (t:term) : term
 
+(* Similar to `deep_compress 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

src/tactics/FStar.Tactics.V2.Basic.fst

@@ -2101,6 +2101,8 @@ let refl_typing_builtin_wrapper (f:unit -> 'a) : tac (option 'a & issues) =
       }) in
       [issue], None
   in
+  let! ps = get in
+  Env.promote_id_info ps.main_context (FStar.TypeChecker.Tc.compress_and_norm ps.main_context);
   UF.rollback tx;
   if List.length errs > 0
   then ret (None, errs)

src/typechecker/FStar.TypeChecker.Common.fst

@@ -112,23 +112,24 @@ let id_info__insert ty_map db info =
       | Inr _ ->
         ty_map info.identifier_ty
       | Inl x ->
-        // BU.print1 "id_info__insert: %s\n"
-        //           (print_identifier_info info);
         ty_map info.identifier_ty
     in
-    let info = { info with identifier_range = use_range;
-                           identifier_ty = id_ty } in
+    match id_ty with
+    | None -> db
+    | Some id_ty ->
+      let info = { info with identifier_range = use_range;
+                             identifier_ty = id_ty } in
 
-    let fn = file_of_range use_range in
-    let start = start_of_range use_range in
-    let row, col = line_of_pos start, col_of_pos start in
+      let fn = file_of_range use_range in
+      let start = start_of_range use_range in
+      let row, col = line_of_pos start, col_of_pos start in
 
-    let rows = BU.psmap_find_default db fn (BU.pimap_empty ()) in
-    let cols = BU.pimap_find_default rows row [] in
+      let rows = BU.psmap_find_default db fn (BU.pimap_empty ()) in
+      let cols = BU.pimap_find_default rows row [] in
 
-    insert_col_info col info cols
-    |> BU.pimap_add rows row
-    |> BU.psmap_add db fn
+      insert_col_info col info cols
+      |> BU.pimap_add rows row
+      |> BU.psmap_add db fn
 
 let id_info_insert table id ty range =
     let info = { identifier = id; identifier_ty = ty; identifier_range = range} in
@@ -606,4 +607,4 @@ let check_positivity_qual subtyping p0 p1
          | Some _, None -> true
          | Some BinderUnused, Some BinderStrictlyPositive -> true
          | _ -> false
-    else false
+    else false

src/typechecker/FStar.TypeChecker.Common.fsti

@@ -127,7 +127,7 @@ val id_info_table_empty : id_info_table
 val id_info_insert_bv : id_info_table -> bv -> typ -> id_info_table
 val id_info_insert_fv : id_info_table -> fv -> typ -> id_info_table
 val id_info_toggle    : id_info_table -> bool -> id_info_table
-val id_info_promote   : id_info_table -> (typ -> typ) -> id_info_table
+val id_info_promote   : id_info_table -> (typ -> option typ) -> id_info_table
 val id_info_at_pos    : id_info_table -> string -> int -> int -> option identifier_info
 
 // Reason, term and uvar, and (rough) position where it is introduced
@@ -193,4 +193,4 @@ val lcomp_of_comp : comp -> lcomp
 val simplify : debug:bool -> term -> term
 
 val check_positivity_qual (subtyping:bool) (p0 p1:option positivity_qualifier)
-  : bool
+  : bool

src/typechecker/FStar.TypeChecker.Env.fsti

@@ -287,7 +287,7 @@ val get_range      : env -> Range.range
 val insert_bv_info : env -> bv -> typ -> unit
 val insert_fv_info : env -> fv -> typ -> unit
 val toggle_id_info : env -> bool -> unit
-val promote_id_info : env -> (typ -> typ) -> unit
+val promote_id_info : env -> (typ -> option typ) -> unit
 
 (* Querying identifiers *)
 val lid_exists             : env -> lident -> bool

src/typechecker/FStar.TypeChecker.Tc.fst

@@ -1025,6 +1025,23 @@ let add_sigelt_to_env (env:Env.env) (se:sigelt) (from_cache:bool) : Env.env =
 
     | _ -> env
 
+(* This function is called when promoting entries in the id info table.
+   If t has no dangling uvars, it is normalized and promoted,
+   otherwise discarded *)
+let compress_and_norm env t = 
+    match Compress.deep_compress_if_no_uvars t with
+    | None -> None //if dangling uvars, then just drop this entry
+    | Some t ->  //otherwise, normalize and promote
+      Some (
+        N.normalize
+               [Env.AllowUnboundUniverses; //this is allowed, since we're reducing types that appear deep within some arbitrary context
+                Env.CheckNoUvars;
+                Env.Beta; Env.DoNotUnfoldPureLets; Env.CompressUvars;
+                Env.Exclude Env.Zeta; Env.Exclude Env.Iota; Env.NoFullNorm]
+              env
+              t
+      )
+
 let tc_decls env ses =
   let rec process_one_decl (ses, env) se =
     (* If emacs is peeking, and debugging is on, don't do anything,
@@ -1055,21 +1072,8 @@ let tc_decls env ses =
         then BU.print1 "About to elim vars from (elaborated) %s\n" (Print.sigelt_to_string se);
         N.elim_uvars env se) in
 
-    Profiling.profile 
-      (fun () ->
-        Env.promote_id_info env (fun t ->
-          if Env.debug env (Options.Other "UF")
-          then BU.print1 "check uvars %s\n" (Print.term_to_string t);
-          N.normalize
-               [Env.AllowUnboundUniverses; //this is allowed, since we're reducing types that appear deep within some arbitrary context
-                Env.CheckNoUvars;
-                Env.Beta; Env.DoNotUnfoldPureLets; Env.CompressUvars;
-                Env.Exclude Env.Zeta; Env.Exclude Env.Iota; Env.NoFullNorm]
-              env
-              t))
-        (Some (Ident.string_of_lid (Env.current_module env)))
-        "FStar.TypeChecker.Tc.chec_uvars"; //update the id_info table after having removed their uvars
-
+    Env.promote_id_info env (compress_and_norm env);
+
     // Compress all checked sigelts
     let ses' = ses' |> List.map (Compress.deep_compress_se false) in
 

src/typechecker/FStar.TypeChecker.Tc.fsti

@@ -30,6 +30,7 @@ val push_context: env -> string -> env
 val snapshot_context: env -> string -> ((int * int * solver_depth_t * int) * env)
 val rollback_context: solver_t -> string -> option (int * int * solver_depth_t * int) -> env
 
+val compress_and_norm: env -> typ -> option typ
 val tc_decls: env -> list sigelt -> list sigelt * env
 val tc_partial_modul: env -> modul -> modul * env
 val tc_more_partial_modul: env -> modul -> list sigelt -> modul * list sigelt * env