Merge branch 'master' into kant/newmsbuildsdk

examples/layeredeffects/DivAction.fst

@@ -1,53 +1,51 @@
 module DivAction
 
-let repr (a : Type) () : Type =
+let repr (a : Type) : Type =
   unit -> Dv a
 
-let return (a : Type) (x : a) : repr a () =
+let return (a : Type) (x : a) : repr a =
   fun () -> x
 
-let bind (a b : Type) (v : repr a ()) (f : (a -> repr b ())) : repr b () =
+let bind (a b : Type) (v : repr a) (f : (a -> repr b)) : repr b  =
   fun () -> f (v ()) ()
 
 total
 reifiable
 reflectable
-layered_effect {
-  ID : a:Type -> eqtype_as_type unit -> Effect
-  with repr         = repr;
-       return       = return;
-       bind         = bind
+effect {
+  ID (a:Type)
+  with {repr; return; bind}
 }
 
 let lift_pure_nd (a:Type) (wp:pure_wp a) (f:(eqtype_as_type unit -> PURE a wp)) :
-  Pure (repr a ()) (requires (wp (fun _ -> True) /\ (forall p1 p2. (forall x. p1 x ==> p2 x) ==> wp p1 ==> wp p2)))
-                   (ensures (fun _ -> True))
+  Pure (repr a) (requires (wp (fun _ -> True) /\ (forall p1 p2. (forall x. p1 x ==> p2 x) ==> wp p1 ==> wp p2)))
+                (ensures (fun _ -> True))
   = fun _ ->
     let r = f () in
     r
 
 sub_effect PURE ~> ID = lift_pure_nd
 
-val fix : #a:_ -> #b:_ -> ((a -> ID b ()) -> (a -> ID b ())) -> (a -> ID b ())
+val fix : #a:_ -> #b:_ -> ((a -> ID b) -> (a -> ID b)) -> (a -> ID b)
 let fix #a #b f =
   let reified : (a -> Dv b) -> (a -> Dv b) =
     fun g x ->
-      let reflected_g : (a -> ID b ()) =
+      let reflected_g : (a -> ID b) =
         fun x -> ID?.reflect (fun () -> g x)
       in
       reify (f reflected_g x) ()
   in
   let rec fixed : (a -> Dv b) =
     fun x -> reified fixed x
   in
-  let reflected : a -> ID b () =
+  let reflected : a -> ID b =
     fun x -> ID?.reflect (fun () -> fixed x)
   in
   reflected
 
 [@@expect_failure]
-let rec bad_div (x:int) : ID int () = bad_div x
+let rec bad_div (x:int) : ID int = bad_div x
 
-let good_div : int -> ID int () = fix #int #int (fun f x -> f x)
+let good_div : int -> ID int = fix #int #int (fun f x -> f x)
 
 let test (x:int) : Dv int = reify (good_div x) ()

examples/layeredeffects/IteSoundness.fst

@@ -122,10 +122,10 @@ effect {
   * Whereas the tactic can instantiate them at will
  *)
 
-type mrepr (a:Type) (_:unit) = a
+type mrepr (a:Type) = a
 
-let mreturn (a:Type) (x:a) : mrepr a () = x
-let mbind (a:Type) (b:Type) (f:mrepr a ()) (g:a -> mrepr b ()) : mrepr b () = g f
+let mreturn (a:Type) (x:a) : mrepr a = x
+let mbind (a:Type) (b:Type) (f:mrepr a) (g:a -> mrepr b) : mrepr b = g f
 
 (*
  * The attribute annotations on the binders below are required,
@@ -135,16 +135,16 @@ let mbind (a:Type) (b:Type) (f:mrepr a ()) (g:a -> mrepr b ()) : mrepr b () = g
 let mif_then_else (a:Type)
   ([@@@ an_attr] phi:Type0)
   ([@@@ an_attr] bb:squash phi) 
-  (f:mrepr a ())
-  (g:mrepr a ())
+  (f:mrepr a)
+  (g:mrepr a)
   (b:bool)
   : Type
-  = mrepr a ()
+  = mrepr a
 
 let msubcomp (a:Type)
   ([@@@ an_attr] phi:Type0)
-  ([@@@ an_attr] bb:squash phi)  (f:mrepr a ())
-  : mrepr a () = f
+  ([@@@ an_attr] bb:squash phi)  (f:mrepr a)
+  : mrepr a = f
 
 [@@ resolve_implicits; an_attr]
 let mtac1 () : Tac unit =
@@ -154,7 +154,7 @@ let mtac1 () : Tac unit =
 
 [@@ ite_soundness_by an_attr]
 effect {
-  M (a:Type) (_:unit)
+  M (a:Type)
   with {repr=mrepr; return=mreturn; bind=mbind; if_then_else=mif_then_else; subcomp=msubcomp}
 }
 
@@ -165,11 +165,11 @@ effect {
  *   to make a proof go through
  *)
 
-type mmrepr (a:Type) (_:unit) = a
-let mmreturn (a:Type) (x:a) : mmrepr a () = x
-let mmbind (a b:Type) (f:mmrepr a ()) (g:a -> mmrepr b ()) : mmrepr b () = g f
-let mmsubcomp (a:Type) (f:mmrepr a ())
-  : Pure (mmrepr a ())
+type mmrepr (a:Type) = a
+let mmreturn (a:Type) (x:a) : mmrepr a = x
+let mmbind (a b:Type) (f:mmrepr a) (g:a -> mmrepr b) : mmrepr b = g f
+let mmsubcomp (a:Type) (f:mmrepr a)
+  : Pure (mmrepr a)
       (requires False)
       (ensures fun _ -> True)
   = f
@@ -181,7 +181,7 @@ let mmsubcomp (a:Type) (f:mmrepr a ())
 
 [@@ expect_failure]
 effect {
-  N (a:Type) (_:unit)
+  N (a:Type)
   with { repr = mmrepr; return = mmreturn; bind = mmbind; subcomp = mmsubcomp }
 }
 
@@ -195,6 +195,6 @@ let mtac2 () : Tac unit =
 
 [@@ ite_soundness_by an_attr]
 effect {
-  N (a:Type) (_:unit)
+  N (a:Type)
   with { repr = mmrepr; return = mmreturn; bind = mmbind; subcomp = mmsubcomp }
 }

examples/layeredeffects/ParametricStateIssue.fst

@@ -49,7 +49,7 @@ module B = LowStar.Buffer
 ///
 /// Specifically, if we have `let lift ... (state:Type0) ... : mrepr a state = e`
 ///
-/// And we pass in `()` for state, it messes up the `mrepr a ()` annotation, and the term `e` gets
+/// And we pass in `()` for state, it messes up the `mrepr a` annotation, and the term `e` gets
 ///   ascribed with `mrepr a unit` which down the line results in some `Obj.magic`s in the extracted
 ///   code
 ///
@@ -63,20 +63,18 @@ module B = LowStar.Buffer
 
 
 inline_for_extraction
-type repr (a:Type) (_:eqtype_as_type unit) =
-  unit ->
-  St (option a)
+type repr (a:Type) = unit -> St (option a)
 
 
 inline_for_extraction
 let return (a:Type) (x:a)
-: repr a ()
+: repr a
 = fun _ -> Some x
 
 inline_for_extraction
 let bind (a:Type) (b:Type)
-  (f:repr a ()) (g:(x:a -> repr b ()))
-: repr b ()
+  (f:repr a) (g:(x:a -> repr b))
+: repr b
 = fun _ ->
   let r = f () in
   match r with
@@ -87,18 +85,14 @@ let bind (a:Type) (b:Type)
 /// The effect definition
 
 reifiable reflectable
-layered_effect {
-  EXN : a:Type -> eqtype_as_type unit -> Effect
-  with
-  repr = repr;
-  return = return;
-  bind = bind
+effect {
+  EXN (a:Type)
+  with {repr; return; bind}
 }
 
-
 inline_for_extraction
 let lift_div_exn (a:Type) (wp:pure_wp a) (f:eqtype_as_type unit -> DIV a wp)
-: repr a ()
+: repr a
 = fun _ -> Some (f ())
 
 
@@ -120,11 +114,9 @@ type rcv_state = {
   id : i:uint_32{i <= B.len b}
 }
 
-
-
 inline_for_extraction
 type mrepr (a:Type) (state:Type0) =
-  state -> EXN (a & state) ()
+  state -> EXN (a & state)
 
 inline_for_extraction noextract
 let streturn (a:Type) (x:a) (state:Type0)
@@ -143,15 +135,11 @@ let stbind (a:Type) (b:Type)
 
 
 reifiable reflectable
-layered_effect {
-  STEXN : a:Type -> state:Type0 -> Effect
-  with
-  repr = mrepr;
-  return = streturn;
-  bind = stbind
+effect {
+  STEXN (a:Type) (state:Type0)
+  with {repr=mrepr; return=streturn; bind=stbind}
 }
 
-
 inline_for_extraction noextract
 let lift_div_stexn (a:Type) (wp:pure_wp a) (state:Type0) (f:eqtype_as_type unit -> DIV a wp)
 : mrepr a state
@@ -164,7 +152,7 @@ let parse_common_exn (#a:Type0)
   (parser:parser_t a)
   (_:unit)
   (st:rcv_state)
-: EXN (a & rcv_state) ()
+: EXN (a & rcv_state)
 = EXN?.reflect (fun _ ->
     let r = parser st.b st.id in
     match r with

examples/layeredeffects/SMTReification.fst

@@ -16,37 +16,33 @@
 
 module SMTReification
 
-type repr (a:Type) (_:unit) = a & int
+type repr (a:Type) = a & int
 
-let return (a:Type) (x:a) : repr a () = x, 0
+let return (a:Type) (x:a) : repr a = x, 0
 
-let bind (a:Type) (b:Type) (f:repr a ()) (g:a -> repr b ()) : repr b () =
+let bind (a:Type) (b:Type) (f:repr a) (g:a -> repr b) : repr b =
   let x, n = f in
   let y, m = g x in
   y, n + m
 
-reifiable reflectable total
-layered_effect {
-  MST : a:Type -> eqtype_as_type unit -> Effect
-  with
-  repr = repr;
-  return = return;
-  bind = bind
+reifiable
+reflectable
+total
+effect {
+  MST (a:Type)
+  with {repr; return; bind}
 }
 
-assume val pure_wp_monotonic (#a:Type) (wp:pure_wp a)
-: Lemma (forall p q. (forall x. p x ==> q x) ==> (wp p ==> wp q))
-
 let lift_pure_mst (a:Type) (wp:pure_wp a) (f:eqtype_as_type unit -> PURE a wp)
-: Pure (repr a ()) (requires wp (fun _ -> True)) (ensures fun _ -> True)
-= pure_wp_monotonic wp;
+: Pure (repr a) (requires wp (fun _ -> True)) (ensures fun _ -> True)
+= FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp;
   f (), 0
 
 sub_effect PURE ~> MST = lift_pure_mst
 
-let set (n:int) : MST unit () = MST?.reflect ((), n)
+let set (n:int) : MST unit = MST?.reflect ((), n)
 
-let incr_and_set (n:int) : MST unit () = set (n+1)
+let incr_and_set (n:int) : MST unit = set (n+1)
 
 //AR: 07/03: backtracking on smt reification for layered effects
 //let reify_incr_and_set () = assert (snd (reify (incr_and_set 0)) == 1)