Merge pull request #3852 from FStarLang/_nik_eqtype_as_type

Remove eqtype_as_type from layered effect samples

Author: nikswamy

examples/layeredeffects/GenericTotalDM4A.fst

@@ -85,7 +85,7 @@ effect {
  *     there is now a check in the typechecker to forbid it,
  *     so the lift below fails
  *)
-let lift_pure_dm4a (a:Type) (f:(eqtype_as_type unit -> Tot a))
+let lift_pure_dm4a (a:Type) (f:(unit -> Tot a))
   : repr a (w_return (f ()))
   = return _ (f ())
 

examples/oplss2021/OPLSS2021.ParDiv.fst

@@ -349,7 +349,7 @@ val bind_pure_c_ (a:Type) (b:Type)
   (wp:pure_wp a)
   (pre:hm.r)
   (post:b -> hm.r)
-  (f:eqtype_as_type unit -> PURE a wp)
+  (f:unit -> PURE a wp)
   (g:(x:a -> comp b pre post))
  : Pure (comp b
               pre
@@ -364,7 +364,7 @@ val bind_div_c_ (a:Type) (b:Type)
   (wp:pure_wp a)
   (pre:hm.r)
   (post:b -> hm.r)
-  (f:eqtype_as_type unit -> DIV a wp)
+  (f:unit -> DIV a wp)
   (g:(x:a -> comp b pre post))
  : Pure (comp b
               pre

examples/oplss2021/OPLSS2021.ParNDSDiv.fst

@@ -349,7 +349,7 @@ val bind_pure_c_ (a:Type) (b:Type)
   (wp:pure_wp a)
   (pre:hm.r)
   (post:b -> hm.r)
-  (f:eqtype_as_type unit -> PURE a wp)
+  (f:unit -> PURE a wp)
   (g:(x:a -> comp b pre post))
  : Pure (comp b
               pre
@@ -364,7 +364,7 @@ val bind_div_c_ (a:Type) (b:Type)
   (wp:pure_wp a)
   (pre:hm.r)
   (post:b -> hm.r)
-  (f:eqtype_as_type unit -> DIV a wp)
+  (f:unit -> DIV a wp)
   (g:(x:a -> comp b pre post))
  : Pure (comp b
               pre

tests/bug-reports/closed/Bug2055.fst

@@ -9,7 +9,7 @@ let bind a b (x: repr a _) (f:a-> repr b _) : repr b () = f x
 reifiable
 reflectable
 layered_effect {
-  ND : a:Type -> dummy:eqtype_as_type unit -> Effect
+  ND : a:Type -> dummy:unit -> Effect
   with repr         = repr;
        return       = return;
        bind         = bind
@@ -18,7 +18,7 @@ layered_effect {
 let monotonic #a (wp : pure_wp a) =
   forall p1 p2. (forall x. p1 x ==> p2 x) ==> wp p1 ==> wp p2
 
-let lift_pure_nd (a:Type) (wp:pure_wp a) (f:(eqtype_as_type unit -> PURE a wp)) :
+let lift_pure_nd (a:Type) (wp:pure_wp a) (f:(unit -> PURE a wp)) :
   Pure (repr a ()) (requires (wp (fun _ -> True))) // <--- This is a lift from Tot only
                    (ensures (fun _ -> True))
   = assume (monotonic wp);

tests/bug-reports/closed/Bug2169.fst

@@ -138,7 +138,7 @@ layered_effect {
        if_then_else = i_if_then_else
 }
 
-let lift_pure_nd (a:Type) (wp:pure_wp a) (f:(eqtype_as_type unit -> PURE a wp)) :
+let lift_pure_nd (a:Type) (wp:pure_wp a) (f:(unit -> PURE a wp)) :
   Pure (irepr a wp) (requires True)
                     (ensures (fun _ -> True))
   = fun p _ -> let r = elim_pure f p in [r]

tests/bug-reports/closed/Bug2169b.fst

@@ -78,7 +78,7 @@ layered_effect {
        if_then_else = i_if_then_else
 }
 
-let lift_pure_nd (a:Type) (wp:pure_wp a) (f:(eqtype_as_type unit -> PURE a wp)) :
+let lift_pure_nd (a:Type) (wp:pure_wp a) (f:(unit -> PURE a wp)) :
   Pure (irepr a wp) (requires True)
                     (ensures (fun _ -> True))
   = fun p _ -> elim_pure f p

tests/bug-reports/closed/Bug2641.fst

@@ -105,7 +105,7 @@ let dm_free_subcomp a wp1 wp2 f = f
 val lift_pure_dm_free :
   a: Type ->
   w: pure_wp a ->
-  f: (_: eqtype_as_type unit -> PURE a w) ->
+  f: (_: unit -> PURE a w) ->
   Tot (dm_free a (wp_lift_pure_hist w))
 let lift_pure_dm_free a w f =
   FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall ();

tests/bug-reports/closed/Bug3120a.fst

@@ -163,7 +163,7 @@ let as_requires_wlift #a (w : pure_wp a) :
   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) =
+let lift_pure (a : Type) (w : pure_wp a) (f:(unit -> PURE a w)) : dm a (wlift w) =
   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

tests/micro-benchmarks/Effects.Coherence.fst

@@ -26,7 +26,7 @@ let return (a:Type) (x:a) : repr a () = x
 let bind (a:Type) (b:Type) (f:repr a ()) (g:a -> repr b ()) : repr b () = g f
 
 layered_effect {
-  M1 : Type -> eqtype_as_type unit -> Effect
+  M1 : Type -> unit -> Effect
   with
   repr = repr;
   return = return;
@@ -36,7 +36,7 @@ layered_effect {
 new_effect M2 = M1
 new_effect M3 = M1
 
-let lift_pure_m (a:Type) (wp:_) (f:eqtype_as_type unit -> PURE a wp)
+let lift_pure_m (a:Type) (wp:_) (f:unit -> PURE a wp)
   : Pure (repr a ()) (requires wp (fun _ -> True)) (ensures fun _ -> True)
   = FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall ();
     f ()

tests/micro-benchmarks/Erasable.fst

@@ -71,13 +71,13 @@ let e_unit_5 = t
 
 (* Tests for extraction of erasable effects, combined with their lifts to non-erasable effects *)
 
-type repr (a:Type) (_:eqtype_as_type unit) = a
+type repr (a:Type) (_:unit) = a
 let return (a:Type) (x:a) : repr a () = x
 let bind (a b:Type) (f:repr a ()) (g:a -> repr b ()) : repr b () = g f
 [@@ primitive_extraction]
 total
 effect {
-  MPURE (a:Type) (_:eqtype_as_type unit) with {repr; return; bind}
+  MPURE (a:Type) (_:unit) with {repr; return; bind}
 }
 
 //an erasable effect must be marked total
@@ -88,7 +88,7 @@ new_effect MGHOST = MPURE
 total new_effect MGHOST = MPURE
 
 //a lift cannot be in Ghost effect if the source effect is not erasable
-let lift_PURE_MPURE_error (a:Type) (wp:pure_wp a) (f:eqtype_as_type unit -> PURE a wp)
+let lift_PURE_MPURE_error (a:Type) (wp:pure_wp a) (f:unit -> PURE a wp)
   : Ghost (repr a ())
       (requires wp (fun _ -> True))
       (ensures fun _ -> True)
@@ -99,7 +99,7 @@ sub_effect PURE ~> MPURE = lift_PURE_MPURE_error
 
 //lifts from GHOST effect are not allowed
 //GHOST effect is implicitly lifted/combined with effects when appropriate
-let lift_GHOST_MPURE (a:Type) (wp:pure_wp a) (f:eqtype_as_type unit -> GHOST a wp)
+let lift_GHOST_MPURE (a:Type) (wp:pure_wp a) (f:unit -> GHOST a wp)
   : Ghost (repr a ())
       (requires wp (fun _ -> True))
       (ensures fun _ -> True)
@@ -108,7 +108,7 @@ let lift_GHOST_MPURE (a:Type) (wp:pure_wp a) (f:eqtype_as_type unit -> GHOST a w
 [@@expect_failure [187]]
 sub_effect GHOST ~> MPURE = lift_GHOST_MPURE
 
-let lift_PURE_MPURE (a:Type) (wp:pure_wp a) (f:eqtype_as_type unit -> PURE a wp)
+let lift_PURE_MPURE (a:Type) (wp:pure_wp a) (f:unit -> PURE a wp)
   : Pure (repr a ())
       (requires wp (fun _ -> True))
       (ensures fun _ -> True)
@@ -205,7 +205,7 @@ total
 new_effect M2 = MPURE
 
 //instead of defining lifts from PURE To M1 or M2, we define polymonadic binds
-let bind_PURE_M1 (a b:Type) (wp:pure_wp a) (f:eqtype_as_type unit -> PURE a wp) (g:a -> repr b ())
+let bind_PURE_M1 (a b:Type) (wp:pure_wp a) (f:unit -> PURE a wp) (g:a -> repr b ())
   : Pure (repr b ())
       (requires wp (fun _ -> True))
       (ensures fun _ -> True)