fix some universes to 0

needed because GenElim in FStarLang/FStar#2349 now accepts universe 1
project-everest · Mar 4, 2024 · 914f926 · 914f926
1 parent 5761ad5
commit 914f926
Show file tree

Hide file tree

Showing 7 changed files with 44 additions and 29 deletions.
diff --git a/src/lowparse/LowParse.SteelST.Access.fst b/src/lowparse/LowParse.SteelST.Access.fst
@@ -219,7 +219,7 @@ let ghost_peek_strong
 inline_for_extraction
 let peek_strong_with_size
   (#k: Ghost.erased parser_kind)
-  (#t: Type)
+  (#t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (#va: AP.v byte)
   (p: parser k t)
   (a: byte_array)

diff --git a/src/lowparse/LowParse.SteelST.Combinators.fst b/src/lowparse/LowParse.SteelST.Combinators.fst
@@ -163,7 +163,8 @@ let jump_pair
 
 let g_split_pair
   #opened
-  #k1 #t1 (p1: parser k1 t1)
+  #k1 (#t1: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  (p1: parser k1 t1)
   #k2 #t2 (p2: parser k2 t2)
   #y (a: byte_array)
 : STGhost (Ghost.erased (byte_array)) opened
@@ -209,7 +210,8 @@ let split_pair'
 inline_for_extraction
 let split_pair
   (#k1: Ghost.erased parser_kind) #t1 (#p1: parser k1 t1) (j1: jumper p1)
-  (#k2: Ghost.erased parser_kind) #t2 (p2: parser k2 t2)
+  (#k2: Ghost.erased parser_kind) (#t2: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  (p2: parser k2 t2)
   #y (a: byte_array)
 : ST (byte_array)
     (aparse (p1 `nondep_then` p2) a y)
@@ -269,7 +271,8 @@ let clens_fst
 inline_for_extraction
 let with_pair_fst
   (#k1: Ghost.erased parser_kind) #t1 (p1: parser k1 t1)
-  (#k2: Ghost.erased parser_kind) #t2 (p2: parser k2 t2)
+  (#k2: Ghost.erased parser_kind) (#t2: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  (p2: parser k2 t2)
 : Pure (accessor (p1 `nondep_then` p2) p1 (clens_fst _ _))
     (k1.parser_kind_subkind == Some ParserStrong)
     (fun _ -> True)
@@ -405,7 +408,7 @@ let read_synth'
 inline_for_extraction
 let write_synth
   (#k: parser_kind)
-  (#t1: Type)
+  (#t1: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (#p: parser k t1)
   (#s: serializer p)
   (w: writer s)
@@ -505,7 +508,8 @@ let jump_fail
 
 inline_for_extraction
 let validate_filter
-  (#k: Ghost.erased parser_kind) #t (#p: parser k t) (v: validator p) (r: leaf_reader p)
+  (#k: Ghost.erased parser_kind) (#t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  (#p: parser k t) (v: validator p) (r: leaf_reader p)
   (f: t -> GTot bool)
   (f' : ((x: t) -> Tot (y: bool { y == f x } )))
 : Pure (validator (p  `parse_filter` f))
@@ -603,7 +607,7 @@ let read_filter
 inline_for_extraction
 let write_filter
   (#k: parser_kind)
-  (#t: Type)
+  (#t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (#p: parser k t)
   (#s: serializer p)
   (w: writer s)
@@ -743,7 +747,7 @@ let exists_and_then_payload
 let ghost_split_and_then
   (#opened: _)
   (#k1: parser_kind)
-  (#t1: Type)
+  (#t1: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (p1: parser k1 t1)
   (#k2: parser_kind)
   (#t2: Type)
@@ -772,7 +776,7 @@ let split_and_then
   (#p1: parser k1 t1)
   (j1: jumper p1)
   (#k2: Ghost.erased parser_kind)
-  (#t2: Type)
+  (#t2: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (p2: (t1 -> parser k2 t2))
   (u: squash (and_then_cases_injective p2 /\ k1.parser_kind_subkind == Some ParserStrong))
   (#va: _)
@@ -799,7 +803,7 @@ let ghost_and_then_tag
   (#t1: Type)
   (p1: parser k1 t1)
   (#k2: parser_kind)
-  (#t2: Type)
+  (#t2: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (p2: (t1 -> parser k2 t2))
   (u: squash (and_then_cases_injective p2 /\ k1.parser_kind_subkind == Some ParserStrong))
   #y #y1 (a1: byte_array) (a2: byte_array)
@@ -878,7 +882,7 @@ let intro_and_then
 inline_for_extraction
 let validate_tagged_union
   (#kt: Ghost.erased parser_kind)
-  (#tag_t: Type)
+  (#tag_t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (#pt: parser kt tag_t)
   (vt: validator pt)
   (rt: leaf_reader pt)
@@ -920,7 +924,7 @@ let validate_tagged_union
 inline_for_extraction
 let jump_tagged_union
   (#kt: Ghost.erased parser_kind)
-  (#tag_t: Type)
+  (#tag_t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (#pt: parser kt tag_t)
   (vt: jumper pt)
   (rt: leaf_reader pt)
@@ -989,7 +993,7 @@ let exists_tagged_union_payload
 let ghost_split_tagged_union
   (#opened: _)
   (#kt: parser_kind)
-  (#tag_t: Type)
+  (#tag_t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (pt: parser kt tag_t)
   (#data_t: Type)
   (tag_of_data: (data_t -> GTot tag_t))
@@ -1018,7 +1022,7 @@ let split_tagged_union
   (#tag_t: Type)
   (#pt: parser kt tag_t)
   (jt: jumper pt)
-  (#data_t: Type)
+  (#data_t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (tag_of_data: (data_t -> GTot tag_t))
   (#k: Ghost.erased parser_kind)
   (p: (t: tag_t) -> Tot (parser k (refine_with_tag tag_of_data t)))
@@ -1046,7 +1050,7 @@ let ghost_tagged_union_tag
   (#kt: parser_kind)
   (#tag_t: Type)
   (pt: parser kt tag_t)
-  (#data_t: Type)
+  (#data_t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (tag_of_data: (data_t -> GTot tag_t))
   (#k: parser_kind)
   (p: (t: tag_t) -> Tot (parser k (refine_with_tag tag_of_data t)))
@@ -1219,7 +1223,7 @@ let hop_dtuple2_tag_with_size
   (#tag_t: Type)
   (pt: parser kt tag_t)
   (#k: Ghost.erased parser_kind)
-  (#data_t: tag_t -> Type)
+  (#data_t: tag_t -> Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (p: (t: tag_t) -> Tot (parser k (data_t t)))
   #y #y1 (a1: byte_array) (sz1: SZ.t) (a2: Ghost.erased byte_array)
 : ST byte_array

diff --git a/src/lowparse/LowParse.SteelST.Fold.Gen.fst b/src/lowparse/LowParse.SteelST.Fold.Gen.fst
@@ -488,7 +488,7 @@ let elim_impl_for_inv_aux_false
   #state_i #state_t #ll_state #ll_state_ptr
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
-  (#t: Type)
+  (#t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (from0: SZ.t) (to: SZ.t)
   (f: Ghost.erased ((x: nat { SZ.v from0 <= x /\ x < SZ.v to }) -> fold_t state_t t unit inv inv))
   (l: t)
@@ -593,7 +593,8 @@ let impl_for_inv
 
 inline_for_extraction
 let impl_for_test
-  #state_i #state_t #ll_state #ll_state_ptr
+  #state_i #state_t (#ll_state: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  #ll_state_ptr
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
   (#k: Ghost.erased parser_kind)
@@ -647,7 +648,8 @@ let rec fold_for_snoc
 
 inline_for_extraction
 let impl_for_body
-  #state_i #state_t #ll_state #ll_state_ptr
+  #state_i #state_t (#ll_state: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  #ll_state_ptr
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
   (#k: Ghost.erased parser_kind)
@@ -796,7 +798,8 @@ let elim_impl_for_inv_aux_false_strong
 
 inline_for_extraction
 let impl_for_post
-  #state_i #state_t #ll_state #ll_state_ptr
+  #state_i #state_t (#ll_state: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  #ll_state_ptr
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
   (#k: Ghost.erased parser_kind)
@@ -875,7 +878,7 @@ let impl_for
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
   (#k: Ghost.erased parser_kind)
-  (#t: Type)
+  (#t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (p: parser k t)
   (from: SZ.t) (to: SZ.t)
   (f: Ghost.erased ((x: nat { SZ.v from <= x /\ x < SZ.v to }) -> fold_t state_t t unit inv inv))
@@ -1497,7 +1500,9 @@ let impl_list_hole_inv
 
 inline_for_extraction
 let impl_list_post_true
-  #state_i #state_t #ll_state #ll_state_ptr
+  #state_i (#state_t: _ -> Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  (#ll_state: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  #ll_state_ptr
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
   (#t: Type)
@@ -1548,7 +1553,9 @@ let impl_list_post_true
 
 inline_for_extraction
 let impl_list_post_false
-  #state_i #state_t #ll_state #ll_state_ptr
+  #state_i (#state_t: _ -> Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  (#ll_state: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  #ll_state_ptr
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
   (#t: Type)
@@ -1624,7 +1631,9 @@ let fold_list_snoc
 
 inline_for_extraction
 let impl_list_body_false
-  #state_i #state_t #ll_state #ll_state_ptr
+  #state_i (#state_t: _ -> Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  (#ll_state: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  #ll_state_ptr
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
   (#t: Type)
@@ -1654,7 +1663,9 @@ let impl_list_body_false
 
 inline_for_extraction
 let impl_list_body_true
-  #state_i #state_t #ll_state #ll_state_ptr
+  #state_i (#state_t: _ -> Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  (#ll_state: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
+  #ll_state_ptr
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
   (#t: Type)

diff --git a/src/lowparse/LowParse.SteelST.Fold.Gen.fsti b/src/lowparse/LowParse.SteelST.Fold.Gen.fsti
@@ -514,7 +514,7 @@ val impl_for
   (cl: low_level_state state_i state_t ll_state ll_state_ptr)
   (inv: state_i)
   (#k: Ghost.erased parser_kind)
-  (#t: Type)
+  (#t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (p: parser k t)
   (from: SZ.t) (to: SZ.t)
   (f: Ghost.erased ((x: nat { SZ.v from <= x /\ x < SZ.v to }) -> fold_t state_t t unit inv inv))

diff --git a/src/lowparse/LowParse.SteelST.Fold.SerializationState.fst b/src/lowparse/LowParse.SteelST.Fold.SerializationState.fst
@@ -1676,7 +1676,7 @@ let r_to_l_write_t
 let r_to_l_write_post_rewrite
   (#opened: _)
   (#k: parser_kind)
-  (#t: Type)
+  (#t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (p: parser k t)
   (#k': parser_kind)
   (p': parser k' t)

diff --git a/src/lowparse/LowParse.SteelST.List.Iter.WithInterrupt.fst b/src/lowparse/LowParse.SteelST.List.Iter.WithInterrupt.fst
@@ -179,7 +179,7 @@ let list_iter_with_interrupt_close
 inline_for_extraction
 let list_iter_with_interrupt_test
   (#k: Ghost.erased parser_kind)
-  (#t: Type)
+  (#t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (p: parser k t)
   (state: bool -> list t -> vprop)
   (v0: v parse_list_kind (list t))

diff --git a/src/lowparse/LowParse.SteelST.Write.fst b/src/lowparse/LowParse.SteelST.Write.fst
@@ -52,7 +52,7 @@ let exact_writer
 inline_for_extraction
 let exact_write
   (#k: parser_kind)
-  (#t: Type)
+  (#t: Type0) // FIXME: if the universe is left out, then F* master will determine universe 0, but F* #2349 cannot, since gen_elim now allows universes 0 and 1. So let's stay at universe 0 for now.
   (#p: parser k t)
   (#s: serializer p)
   (w: writer s)