Merge pull request #3215 from mtzguido/3213b

Further fix for #3213
FStarLang · Feb 12, 2024 · 85aa684 · 85aa684
2 parents 10183ea + 3e66169
commit 85aa684
Show file tree

Hide file tree

Showing 15 changed files with 891 additions and 765 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
diff --git a/src/smtencoding/FStar.SMTEncoding.Term.fst b/src/smtencoding/FStar.SMTEncoding.Term.fst
@@ -52,7 +52,7 @@ F* would encode this to SMT as (roughly)
 ```
 (declare-fun n () Term)
 (assert (HasType n u32))
-(assert (n = U32.uint_to_to 0))
+(assert (n = U32.uint_to_t 0))
 ```
 
 i.e., ground facts about the `n`'s typing and definition would be

diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst
@@ -214,11 +214,13 @@ let prim_from_list (l : list primitive_step) : prim_step_set =
 let built_in_primitive_steps = prim_from_list built_in_primitive_steps_list
 let equality_ops = prim_from_list equality_ops_list
 
-let cfg_to_string cfg =
-    String.concat "\n"
-        ["{";
-         BU.format1 "  steps = %s" (steps_to_string cfg.steps);
-         "}" ]
+instance showable_cfg : showable cfg = {
+  show = (fun cfg ->
+             String.concat "\n"
+                 ["{";
+                 BU.format1 "  steps = %s" (steps_to_string cfg.steps);
+                 "}" ]);
+}
 
 let cfg_env cfg = cfg.tcenv
 

diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fsti b/src/typechecker/FStar.TypeChecker.Cfg.fsti
@@ -29,9 +29,10 @@ open FStar.Syntax.Subst
 open FStar.Syntax.Util
 open FStar.TypeChecker
 open FStar.TypeChecker.Env
-
 open FStar.TypeChecker.Primops
 
+open FStar.Class.Show
+
 module S  = FStar.Syntax.Syntax
 module SS = FStar.Syntax.Subst
 module BU = FStar.Compiler.Util
@@ -116,7 +117,7 @@ val primop_time_report : unit -> string
 
 val cfg_env: cfg -> Env.env
 
-val cfg_to_string : cfg -> string
+instance val showable_cfg : showable cfg
 
 val log : cfg -> (unit -> unit) -> unit
 val log_top : cfg -> (unit -> unit) -> unit