before rebasing

Makefile

@@ -381,6 +381,10 @@ test-1: override FSTAR_EXE := $(abspath stage1/out/bin/fstar.exe)
 test-1: stage1
 	$(MAKE) _test FSTAR_EXE=$(FSTAR_EXE)
 
+_unit-tests-1: override FSTAR_EXE := $(abspath stage1/out/bin/fstar.exe)
+_unit-tests-1: stage1
+	$(MAKE) _unit-tests FSTAR_EXE=$(FSTAR_EXE) unit-tests
+
 test-2: override FSTAR_EXE := $(abspath stage2/out/bin/fstar.exe)
 test-2: stage2
 	$(MAKE) _test FSTAR_EXE=$(FSTAR_EXE)

tests/bug-reports/closed/Bug077.fst

@@ -16,20 +16,18 @@
 module Bug077
 
 assume type a
-assume type p : a -> Type
+assume type p : a -> Type u#0
 
 val ok : x:a{p x} -> r:a{p r}
 let ok x = x
-
 val ok2 : x:a{p x} -> r:(option a){Some? r ==> p (Some?.v r)}
 let ok2 x = Some x
-
 val ok3 : x:a{p x} -> option (r:a{p r})
 let ok3 x = Some x
 
 
 assume type b
-assume type q : a -> b -> Type
+assume type q : a -> b -> Type u#0
 
 val ok4 : x:a -> y:b{q x y} -> r:(a & b){q (fst r) (snd r)}
 let ok4 x y = (x, y)

tests/bug-reports/closed/Bug2169.fst

@@ -41,8 +41,9 @@ let w_return x = as_pure_wp (fun p -> p x)
 unfold
 val w_bind (#a #b : Type) : w a -> (a -> w b) -> w b
 unfold
-let w_bind wp1 k =
-  elim_pure_wp_monotonicity_forall ();
+let w_bind (#a:Type u#a) (#b : Type u#b) wp1 k =
+  elim_pure_wp_monotonicity_forall u#a ();
+  elim_pure_wp_monotonicity_forall u#b ();
   as_pure_wp (fun p -> wp1 (fun x -> k x p))
 
 val interp (#a : Type) : m a -> w a
@@ -120,8 +121,8 @@ let ibind (a : Type) (b : Type) (wp_v : w a) (wp_f: a -> w b) (v : irepr a wp_v)
 
 let isubcomp (a:Type) (wp1 wp2: w a) (f : irepr a wp1) : Pure (irepr a wp2) (requires w_ord wp2 wp1) (ensures fun _ -> True) = f
 
-let wp_if_then_else (#a:Type) (wp1 wp2:w a) (b:bool) : w a=
-  elim_pure_wp_monotonicity_forall ();
+let wp_if_then_else (#a:Type u#a) (wp1 wp2:w a) (b:bool) : w a=
+  elim_pure_wp_monotonicity_forall u#a ();
   as_pure_wp (fun p -> (b ==> wp1 p) /\ ((~b) ==> wp2 p))
 
 let i_if_then_else (a : Type) (wp1 wp2 : w a) (f : irepr a wp1) (g : irepr a wp2) (b : bool) : Type =

tests/bug-reports/closed/Bug2169b.fst

@@ -38,10 +38,11 @@ unfold
 let w_return x = as_pure_wp (fun p -> p x)
 
 unfold
-val w_bind (#a #b : Type) : w a -> (a -> w b) -> w b
+val w_bind (#a:Type u#a) (#b : Type u#b) : w a -> (a -> w b) -> w b
 unfold
-let w_bind wp1 k =
-  elim_pure_wp_monotonicity_forall ();
+let w_bind (#a:Type u#a) (#b : Type u#b) wp1 k =
+  elim_pure_wp_monotonicity_forall u#a ();
+  elim_pure_wp_monotonicity_forall u#b ();
   as_pure_wp (fun p -> wp1 (fun x -> k x p))
 
 val interp (#a : Type) : m a -> w a
@@ -59,8 +60,8 @@ let ibind (a : Type) (b : Type) (wp_v : w a) (wp_f: a -> w b) (v : irepr a wp_v)
 
 let isubcomp (a:Type) (wp1 wp2: w a) (f : irepr a wp1) : Pure (irepr a wp2) (requires w_ord wp2 wp1) (ensures fun _ -> True) = f
 
-let wp_if_then_else (#a:Type) (wp1 wp2:w a) (b:bool) : w a=
-  elim_pure_wp_monotonicity_forall ();
+let wp_if_then_else (#a:Type u#a) (wp1 wp2:w a) (b:bool) : w a=
+  elim_pure_wp_monotonicity_forall u#a ();
   as_pure_wp (fun p -> (b ==> wp1 p) /\ ((~b) ==> wp2 p))
 
 let i_if_then_else (a : Type) (wp1 wp2 : w a) (f : irepr a wp1) (g : irepr a wp2) (b : bool) : Type =

tests/bug-reports/closed/Bug2641.fst

@@ -31,8 +31,8 @@ let hist_return (x:'a) : hist 'a =
 let hist_bind (#a #b:Type) (w : hist a) (kw : a -> hist b) : hist b =
   fun p -> w (fun r -> kw r p)
 
-let wp_lift_pure_hist (w : pure_wp 'a) : hist 'a =
-  FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall ();
+let wp_lift_pure_hist (#a:Type u#a) (w : pure_wp a) : hist a =
+  FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall u#a ();
   w
 
 let partial_call_wp (pre:pure_pre) : hist (squash pre) = 

tests/bug-reports/closed/Bug3120a.fst

@@ -90,7 +90,7 @@ unfold
 let _w_return #a (x : a) : wp a =
   fun post hist -> post [] x
 
-let w_return #a (x : a) : wp a =
+let w_return (#a:Type u#a) (x : a) : wp a =
   _w_return x
 
 unfold
@@ -144,26 +144,27 @@ let w_if_then_else #a (w1 w2 : wp a) (b : bool) : wp a =
 let if_then_else #ac #ad (a : Type) (w1 w2 : wp a) (f : dm #ac #ad a w1) (g : dm #ac #ad a w2) (b : bool) : Type =
   dm #ac #ad a (w_if_then_else w1 w2 b)
 
-let elim_pure #a #w (f : unit -> PURE a w) :
+let elim_pure (#a:Type u#a) #w (f : unit -> PURE a w) :
   Pure
     a
     (requires w (fun _ -> True))
     (ensures fun r -> forall post. w post ==> post r)
-= elim_pure_wp_monotonicity_forall () ;
+= elim_pure_wp_monotonicity_forall u#a () ;
   f ()
 
 unfold
 let wlift #a (w : pure_wp a) : wp a =
   fun post hist -> w (post [])
 
-let as_requires_wlift #a (w : pure_wp a) :
+let as_requires_wlift (#a:Type u#a) (w : pure_wp a) :
   Lemma (forall post hist. wlift w post hist ==> as_requires w)
 = assert (forall post (x : a). post x ==> True) ;
   elim_pure_wp_monotonicity w ;
   assert (forall post. w post ==> w (fun _ -> True)) ;
   assert (forall post. (True ==> w post) ==> w (fun _ -> True))
-
-let lift_pure (a : Type) (w : pure_wp a) (f:(eqtype_as_type unit -> PURE a w)) : dm a (wlift w) =
+// #push-options "--print_universes --print_implicits"
+let lift_pure (a : Type u#0) (w : pure_wp a) (f:(eqtype_as_type unit -> PURE a w)) : dm a (wlift w) =
+  admit();
   as_requires_wlift w ;
   d_bind #_ #_ #_ #_ #_ #_ #_ #(fun _ -> w_return (elim_pure #a #w f)) (d_req (as_requires w)) (fun _ ->
     let r = elim_pure #a #w f in