Merge pull request #3808 from mtzguido/nits

Misc improvements

Author: mtzguido

src/parser/FStarC.Parser.AST.Util.fsti

@@ -27,6 +27,9 @@ val eq_binder (b1 b2:binder) : bool
 val eq_pattern (p1 p2:pattern) : bool
 val eq_decl (d1 d2:decl) : bool
 
+(* Returns every identifier mentioned in a decl (including
+the body). This is used from the interactive mode to provide
+hover information and jump-to-definition. *)
 val lidents_of_decl (t:decl) : list FStarC.Ident.lident
 
 type open_namespaces_and_abbreviations = {

src/tactics/FStarC.Tactics.Interpreter.fst

@@ -364,7 +364,7 @@ let run_unembedded_tactic_on_ps
       else
         let open FStarC.Pprint in
         let open FStarC.Errors.Msg in
-        Errors.raise_error0 Errors.Fatal_UserTacticFailure [
+        Errors.raise_error ps.entry_range Errors.Fatal_UserTacticFailure [
           text "A tactic raised the Stop exception but did not log errors.";
           text "Failing anyway."
         ]

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

@@ -1788,29 +1788,31 @@ let default_if_err (def : 'a) (t : tac 'a) : tac 'a =
   | Inl _ -> return def
   | Inr v -> return v
 
-let match_env (e:env) (t1 : term) (t2 : term) : tac bool = wrap_err "match_env" <| (
-    let! ps = get in
-    let! t1, ty1, g1 = __tc e t1 in
-    let! t2, ty2, g2 = __tc e t2 in
-    proc_guard "match_env g1" e g1 None ps.entry_range ;!
-    proc_guard "match_env g2" e g2 None ps.entry_range ;!
-    let must_tot = true in
-    default_if_err false <|
-      tac_and (do_match must_tot e ty1 ty2)
-              (do_match must_tot e t1 t2)
-    )
+let match_env (e:env) (t1 : term) (t2 : term) : tac bool =
+  wrap_err "match_env" <|
+  default_if_err false <| (
+  let! ps = get in
+  let! t1, ty1, g1 = __tc e t1 in
+  let! t2, ty2, g2 = __tc e t2 in
+  proc_guard "match_env g1" e g1 None ps.entry_range ;!
+  proc_guard "match_env g2" e g2 None ps.entry_range ;!
+  let must_tot = true in
+    tac_and (do_match must_tot e ty1 ty2)
+            (do_match must_tot e t1 t2)
+  )
 
-let unify_env (e:env) (t1 : term) (t2 : term) : tac bool = wrap_err "unify_env" <| (
-    let! ps = get in
-    let! t1, ty1, g1 = __tc e t1 in
-    let! t2, ty2, g2 = __tc e t2 in
-    proc_guard "unify_env g1" e g1 None ps.entry_range ;!
-    proc_guard "unify_env g2" e g2 None ps.entry_range ;!
-    let must_tot = true in
-    default_if_err false <|
-      tac_and (do_unify must_tot e ty1 ty2)
-              (do_unify must_tot e t1 t2)
-    )
+let unify_env (e:env) (t1 : term) (t2 : term) : tac bool =
+  wrap_err "unify_env" <|
+  default_if_err false <| (
+  let! ps = get in
+  let! t1, ty1, g1 = __tc e t1 in
+  let! t2, ty2, g2 = __tc e t2 in
+  proc_guard "unify_env g1" e g1 None ps.entry_range ;!
+  proc_guard "unify_env g2" e g2 None ps.entry_range ;!
+  let must_tot = true in
+    tac_and (do_unify must_tot e ty1 ty2)
+            (do_unify must_tot e t1 t2)
+  )
 
 let unify_guard_env (e:env) (t1 : term) (t2 : term) : tac bool = wrap_err "unify_guard_env" <| (
     let! ps = get in
@@ -2386,7 +2388,7 @@ let unexpected_uvars_issue r =
   let i = {
     issue_level = EError;
     issue_range = Some r;
-    issue_msg = Errors.mkmsg "Cannot check relation with uvars";
+    issue_msg = Errors.mkmsg "Cannot check relation with uvars.";
     issue_number = Some (errno Error_UnexpectedUnresolvedUvar);
     issue_ctx = []
   } in

src/typechecker/FStarC.TypeChecker.Tc.fst

@@ -816,9 +816,10 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env =
               | [] -> [ S.Visible_default ]
               | qs -> qs
            in
-            List.map 
-              (fun sp -> { sp with sigquals = sigquals@sp.sigquals; sigattrs = se.sigattrs@sp.sigattrs})
-              ses
+           let ses = ses |> List.map (fun sp ->
+                             { sp with sigquals = sigquals@sp.sigquals; sigattrs = se.sigattrs@sp.sigattrs}) in
+           let ses = ses |> List.map (Compress.deep_compress_se false false) in
+           ses
       else ses
     in
     let ses = ses |> List.map (fun se ->
@@ -915,9 +916,11 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env =
     [se], [], env0)
 
 
-(* [tc_decl env se] typechecks [se] in environment [env] and returns *
+(* [tc_decl env se] typechecks [se] in environment [env] and returns
  * the list of typechecked sig_elts, and a list of new sig_elts elaborated
- * during typechecking but not yet typechecked *)
+ * during typechecking but not yet typechecked. This may also be called
+ * on ALREADY CHECKED declarations coming out of a splice_t. See the
+ * check for sigmeta_already_checked below. *)
 let tc_decl env se: list sigelt & list sigelt & Env.env =
   FStarC.GenSym.reset_gensym();
   let env0 = env in