ulib layered effects updated to bool in if_then_else

FStarLang · Jul 1, 2020 · 731b353 · 731b353
1 parent ad745c9
commit 731b353
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 12 deletions.
diff --git a/ulib/experimental/MST.fst b/ulib/experimental/MST.fst
@@ -92,7 +92,7 @@ let if_then_else
       (ens_else:post_t state a)
       (f:repr a state rel req_then ens_then)
       (g:repr a state rel req_else ens_else)
-      (p:Type0)
+      (p:bool)
     : Type
     =
   repr a state rel

diff --git a/ulib/experimental/MSTTotal.fst b/ulib/experimental/MSTTotal.fst
@@ -92,12 +92,12 @@ let if_then_else
       (ens_else:post_t state a)
       (f:repr a state rel req_then ens_then)
       (g:repr a state rel req_else ens_else)
-      (p:Type0)
+      (p:bool)
     : Type
     =
   repr a state rel
-    (fun s -> (p ==> req_then s) /\ ((~ p) ==> req_else s))
-    (fun s0 x s1 -> (p ==> ens_then s0 x s1) /\ ((~ p) ==> ens_else s0 x s1))
+    (fun s -> (b2t p ==> req_then s) /\ ((~ (b2t p)) ==> req_else s))
+    (fun s0 x s1 -> (b2t p ==> ens_then s0 x s1) /\ ((~ (b2t p)) ==> ens_else s0 x s1))
 
 total
 reifiable reflectable

diff --git a/ulib/experimental/NMSTTotal.fst b/ulib/experimental/NMSTTotal.fst
@@ -84,7 +84,7 @@ let if_then_else
       (ens_else:M.post_t state a)
       (f:repr a state rel req_then ens_then)
       (g:repr a state rel req_else ens_else)
-      (p:Type0)
+      (p:bool)
     : Type
     =
   repr a state rel

diff --git a/ulib/experimental/Steel.Effect.Atomic.fst b/ulib/experimental/Steel.Effect.Atomic.fst
@@ -54,7 +54,7 @@ let subcomp (a:Type) (uses:Set.set lock_addr) (is_ghost:bool) (pre:pre_t) (post:
 let if_then_else (a:Type) (uses:Set.set lock_addr) (pre:pre_t) (post:post_t a)
   (f:atomic_repr a uses true pre post)
   (g:atomic_repr a uses true pre post)
-  (p:Type0)
+  (p:bool)
   : Type
   = atomic_repr a uses true pre post
 

diff --git a/ulib/experimental/Steel.Effect.fst b/ulib/experimental/Steel.Effect.fst
@@ -157,23 +157,23 @@ let subcomp (a:Type) (pre:pre_t) (post:post_t a)
 unfold
 let if_then_else_req (#pre:pre_t)
   (req_then:req_t pre) (req_else:req_t pre)
-  (p:Type0)
+  (p:bool)
 : req_t pre
-= fun h -> (p ==> req_then h) /\ ((~ p) ==> req_else h)
+= fun h -> ((b2t p) ==> req_then h) /\ ((~ (b2t p)) ==> req_else h)
 
 unfold
 let if_then_else_ens (#a:Type) (#pre:pre_t) (#post:post_t a)
   (ens_then:ens_t pre a post) (ens_else:ens_t pre a post)
-  (p:Type0)
+  (p:bool)
 : ens_t pre a post
-= fun h0 x h1 -> (p ==> ens_then h0 x h1) /\ ((~ p) ==> ens_else h0 x h1)
+= fun h0 x h1 -> ((b2t p) ==> ens_then h0 x h1) /\ ((~ (b2t p)) ==> ens_else h0 x h1)
 
 let if_then_else (a:Type) (pre:pre_t) (post:post_t a)
   (req_then:req_t pre) (ens_then:ens_t pre a post)
   (req_else:req_t pre) (ens_else:ens_t pre a post)
   (f:repr a pre post req_then ens_then)
   (g:repr a pre post req_else ens_else)
-  (p:Type0)
+  (p:bool)
 : Type
 = repr a pre post
     (if_then_else_req req_then req_else p)

diff --git a/ulib/experimental/Steel.FramingEffect.fst b/ulib/experimental/Steel.FramingEffect.fst
@@ -235,7 +235,7 @@ let if_then_else (a:Type)
   (req_else:req_t pre) (ens_else:ens_t pre a post)
   (f:repr a pre post req_then ens_then)
   (g:repr a pre post req_else ens_else)
-  (p:Type0)
+  (p:bool)
 : Type
 = repr a pre post
     (if_then_else_req req_then req_else p)