Nits

src/parser/FStarC.Parser.AST.fsti

@@ -354,6 +354,7 @@ val string_of_pragma : pragma -> string
 val pat_to_string : pattern -> string
 val binder_to_string : binder -> string
 val modul_to_string : modul -> string
+val decl_to_string : decl -> string
 
 val decl_is_val : ident -> decl -> bool
 

src/parser/FStarC.Parser.Const.Tuples.fst

@@ -19,6 +19,7 @@ open FStarC
 open FStarC.Effect
 open FStarC.Ident
 open FStarC.Range
+open FStarC.Class.Show
 
 // Arity, type constructor, and data constructor for tuples
 private
@@ -38,21 +39,21 @@ let tuple_table : list (int & string & string) = [
   (14,  "FStar.Pervasives.Native.tuple14", "FStar.Pervasives.Native.Mktuple14");
 ]
 
-let mk_tuple_lid n r =
+let lookup_tuple n =
   match List.tryFind (fun (n', _, _) -> n = n') tuple_table with
-  | Some (_, s, _) ->
-    let l = Ident.lid_of_str s in
-    set_lid_range l r
+  | Some r -> r
   | None ->
-    failwith "Tuple too large"
+    failwith ("Tuple too large: " ^ (show n))
+
+let mk_tuple_lid n r =
+  let (_, s, _) = lookup_tuple n in
+  let l = Ident.lid_of_str s in
+  set_lid_range l r
 
 let mk_tuple_data_lid n r =
-  match List.tryFind (fun (n', _, _) -> n = n') tuple_table with
-  | Some (_, _, s) ->
-    let l = Ident.lid_of_str s in
-    set_lid_range l r
-  | None ->
-    failwith "Tuple too large"
+  let (_, _, s) = lookup_tuple n in
+  let l = Ident.lid_of_str s in
+  set_lid_range l r
 
 let get_tuple_datacon_arity (s:string) : option int =
   match List.tryFind (fun (_, _, s') -> s = s') tuple_table with
@@ -84,21 +85,21 @@ let dtuple_table : list (int & string & string) = [
   (5, "FStar.Pervasives.dtuple5", "FStar.Pervasives.Mkdtuple5");
 ]
 
-let mk_dtuple_lid n r =
+let lookup_dtuple n =
   match List.tryFind (fun (n', _, _) -> n = n') dtuple_table with
-  | Some (_, s, _) ->
-    let l = Ident.lid_of_str s in
-    set_lid_range l r
+  | Some r -> r
   | None ->
-    failwith "Dependent Tuple too large"
+    failwith ("DTuple too large: " ^ (show n))
+
+let mk_dtuple_lid n r =
+  let (_, s, _) = lookup_dtuple n in
+  let l = Ident.lid_of_str s in
+  set_lid_range l r
 
 let mk_dtuple_data_lid n r =
-  match List.tryFind (fun (n', _, _) -> n = n') dtuple_table with
-  | Some (_, _, s) ->
-    let l = Ident.lid_of_str s in
-    set_lid_range l r
-  | None ->
-    failwith "Dependent Tuple too large"
+  let (_, _, s) = lookup_dtuple n in
+  let l = Ident.lid_of_str s in
+  set_lid_range l r
 
 let get_dtuple_datacon_arity (s:string) : option int =
   match List.tryFind (fun (_, _, s') -> s = s') dtuple_table with

ulib/FStar.ModifiesGen.fst

@@ -1504,11 +1504,12 @@ let loc_addresses_unused_in #al c r a h = ()
 let loc_addresses_not_unused_in #al c r a h = ()
 #pop-options
 
-#push-options "--z3rlimit 50"
+// Using spinoff and z3refresh to avoid a crash in Z3 4.13.3
+#push-options "--z3rlimit 50 --z3refresh"
 let loc_unused_in_not_unused_in_disjoint #al c h =
-  assert (Ghost.reveal (Loc?.aux (loc_unused_in c h)) `loc_aux_disjoint` Ghost.reveal (Loc?.aux (loc_not_unused_in c h)));
-  assert_spinoff (loc_disjoint #al #c (loc_unused_in #al c h)
-                                      (loc_not_unused_in #al c h))
+  assert_spinoff (Ghost.reveal (Loc?.aux (loc_unused_in c h)) `loc_aux_disjoint` Ghost.reveal (Loc?.aux (loc_not_unused_in c h)));
+  assert_spinoff (loc_disjoint #al #c (loc_unused_in #al c h) (loc_not_unused_in #al c h));
+  ()
 #pop-options
 
 #push-options "--z3cliopt 'smt.qi.eager_threshold=100'"