'Modul(term)' -> 'Modul.(term)' ; 'Dcon.prm' -> 'Dcon?.prm', 'is_Dcon' -> 'Dcon?' ; improved name resolution

doc/tutorial/code/exercises/Ex04g.fst

@@ -1,5 +1,5 @@
 module Ex04g
 //hd-tl
 
-val hd : l:list 'a{is_Cons l} -> Tot 'a
-val tl : l:list 'a{is_Cons l} -> Tot (list 'a)
+val hd : l:list 'a{Cons? l} -> Tot 'a
+val tl : l:list 'a{Cons? l} -> Tot (list 'a)

doc/tutorial/code/exercises/Ex07a.fst

@@ -89,8 +89,8 @@ let rec typing g e =
       | _         , _      , _       -> None)
 
 val progress : e:exp -> Lemma
-      (requires (is_Some (typing empty e)))
-      (ensures (is_value e \/ (is_Some (step e))))
+      (requires (Some? (typing empty e)))
+      (ensures (is_value e \/ (Some? (step e))))
 let rec progress e = // by_induction_on e progress
   match e with
   | EVar y -> ()
@@ -119,8 +119,8 @@ let rec appears_free_in x e =
   | EFalse -> false
 
 val free_in_context : x:int -> e:exp -> g:env -> Lemma
-      (requires (is_Some (typing g e)))
-      (ensures (appears_free_in x e ==> is_Some (g x)))
+      (requires (Some? (typing g e)))
+      (ensures (appears_free_in x e ==> Some? (g x)))
 let rec free_in_context x e g =
   match e with
   | EVar _
@@ -132,7 +132,7 @@ let rec free_in_context x e g =
                     free_in_context x e2 g; free_in_context x e3 g
 
 val typable_empty_closed : x:int -> e:exp -> Lemma
-      (requires (is_Some (typing empty e)))
+      (requires (Some? (typing empty e)))
       (ensures (not(appears_free_in x e)))
       [SMTPat (appears_free_in x e)]
 let typable_empty_closed x e = free_in_context x e empty
@@ -171,11 +171,11 @@ let typing_extensional g g' e = context_invariance e g g'
 val substitution_preserves_typing : x:int -> e:exp -> v:exp ->
       g:env ->
       Lemma
-        (requires ( is_Some (typing empty v) /\
-              is_Some (typing (extend g x (Some.v (typing empty v))) e)))
-        (ensures (is_Some (typing empty v) /\
+        (requires ( Some? (typing empty v) /\
+              Some? (typing (extend g x (Some?.v (typing empty v))) e)))
+        (ensures (Some? (typing empty v) /\
                   typing g (subst x v e) ==
-                  typing (extend g x (Some.v (typing empty v))) e))
+                  typing (extend g x (Some?.v (typing empty v))) e))
 let rec substitution_preserves_typing x e v g =
   let Some t_x = typing empty v in
   let gx = extend g x t_x in
@@ -208,8 +208,8 @@ let rec substitution_preserves_typing x e v g =
 
 val preservation : e:exp ->
       Lemma
-        (requires(is_Some (typing empty e) /\ is_Some (step e) ))
-        (ensures(is_Some (step e) /\ typing empty (Some.v (step e)) == typing empty e))
+        (requires(Some? (typing empty e) /\ Some? (step e) ))
+        (ensures(Some? (step e) /\ typing empty (Some?.v (step e)) == typing empty e))
 let rec preservation e =
   match e with
   | EApp e1 e2 ->
@@ -225,5 +225,5 @@ let rec preservation e =
       else preservation e1
 
 (* Exercise: implement this function *)
-val typed_step : e:exp{is_Some (typing empty e) /\ not(is_value e)} ->
+val typed_step : e:exp{Some? (typing empty e) /\ not(is_value e)} ->
                  Tot (e':exp{typing empty e' = typing empty e})

doc/tutorial/code/exercises/Ex07b.fst

@@ -126,8 +126,8 @@ let rec typing g e =
       | _         , _      , _       -> None)
 
 val progress : e:exp -> Lemma
-      (requires (is_Some (typing empty e)))
-      (ensures (is_value e \/ (is_Some (step e))))
+      (requires (Some? (typing empty e)))
+      (ensures (is_value e \/ (Some? (step e))))
 let rec progress e =
   match e with
   | EVar y -> ()
@@ -157,8 +157,8 @@ let rec appears_free_in x e =
   | EFalse -> false
 
 val free_in_context : x:int -> e:exp -> g:env -> Lemma
-      (requires (is_Some (typing g e)))
-      (ensures (appears_free_in x e ==> is_Some (g x)))
+      (requires (Some? (typing g e)))
+      (ensures (appears_free_in x e ==> Some? (g x)))
 let rec free_in_context x e g =
   match e with
   | EVar _
@@ -170,7 +170,7 @@ let rec free_in_context x e g =
                     free_in_context x e2 g; free_in_context x e3 g
 
 val typable_empty_closed : x:int -> e:exp -> Lemma
-      (requires (is_Some (typing empty e)))
+      (requires (Some? (typing empty e)))
       (ensures (not(appears_free_in x e)))
       [SMTPat (appears_free_in x e)]
 let typable_empty_closed x e = free_in_context x e empty
@@ -205,10 +205,10 @@ val typing_extensional : g:env -> g':env -> e:exp
 let typing_extensional g g' e = context_invariance e g g'
 
 val substitution_preserves_typing : x:int -> e:exp -> v:exp ->
-      g:env{is_Some (typing empty v) &&
-            is_Some (typing (extend g x (Some.v (typing empty v))) e)} ->
+      g:env{Some? (typing empty v) &&
+            Some? (typing (extend g x (Some?.v (typing empty v))) e)} ->
       Tot (u:unit{typing g (subst x v e) ==
-                  typing (extend g x (Some.v (typing empty v))) e})
+                  typing (extend g x (Some?.v (typing empty v))) e})
 let rec substitution_preserves_typing x e v g =
   let Some t_x = typing empty v in
   let gx = extend g x t_x in
@@ -239,8 +239,8 @@ let rec substitution_preserves_typing x e v g =
         typing_extensional gxy gyx e1;
         substitution_preserves_typing x e1 v gy)
 
-val preservation : e:exp{is_Some (typing empty e) /\ is_Some (step e)} ->
-      Tot (u:unit{typing empty (Some.v (step e)) == typing empty e})
+val preservation : e:exp{Some? (typing empty e) /\ Some? (step e)} ->
+      Tot (u:unit{typing empty (Some?.v (step e)) == typing empty e})
 let rec preservation e =
   match e with
   | EApp e1 e2 ->

doc/tutorial/code/exercises/Ex07c.fst

@@ -90,8 +90,8 @@ let rec typing g e =
       | _         , _      , _       -> None)
 
 val progress : e:exp -> Lemma
-      (requires (is_Some (typing empty e)))
-      (ensures (is_value e \/ (is_Some (step e))))
+      (requires (Some? (typing empty e)))
+      (ensures (is_value e \/ (Some? (step e))))
 let rec progress e =
   match e with
   | EVar y -> ()
@@ -120,8 +120,8 @@ let rec appears_free_in x e =
   | EFalse -> false
 
 val free_in_context : x:int -> e:exp -> g:env -> Lemma
-      (requires (is_Some (typing g e)))
-      (ensures (appears_free_in x e ==> is_Some (g x)))
+      (requires (Some? (typing g e)))
+      (ensures (appears_free_in x e ==> Some? (g x)))
 let rec free_in_context x e g =
   match e with
   | EVar _
@@ -133,7 +133,7 @@ let rec free_in_context x e g =
                     free_in_context x e2 g; free_in_context x e3 g
 
 val typable_empty_closed : x:int -> e:exp -> Lemma
-      (requires (is_Some (typing empty e)))
+      (requires (Some? (typing empty e)))
       (ensures (not(appears_free_in x e)))
       [SMTPat (appears_free_in x e)]
 let typable_empty_closed x e = free_in_context x e empty
@@ -168,10 +168,10 @@ val typing_extensional : g:env -> g':env -> e:exp
 let typing_extensional g g' e = context_invariance e g g'
 
 val substitution_preserves_typing : x:int -> e:exp -> v:exp ->
-      g:env{is_Some (typing empty v) &&
-            is_Some (typing (extend g x (Some.v (typing empty v))) e)} ->
+      g:env{Some? (typing empty v) &&
+            Some? (typing (extend g x (Some?.v (typing empty v))) e)} ->
       Tot (u:unit{typing g (subst x v e) ==
-                  typing (extend g x (Some.v (typing empty v))) e})
+                  typing (extend g x (Some?.v (typing empty v))) e})
 let rec substitution_preserves_typing x e v g =
   let Some t_x = typing empty v in
   let gx = extend g x t_x in
@@ -202,8 +202,8 @@ let rec substitution_preserves_typing x e v g =
         typing_extensional gxy gyx e1;
         substitution_preserves_typing x e1 v gy)
 
-val preservation : e:exp{is_Some (typing empty e) /\ is_Some (step e)} ->
-      Tot (u:unit{typing empty (Some.v (step e)) == typing empty e})
+val preservation : e:exp{Some? (typing empty e) /\ Some? (step e)} ->
+      Tot (u:unit{typing empty (Some?.v (step e)) == typing empty e})
 let rec preservation e =
   match e with
   | EApp e1 e2 ->

doc/tutorial/code/exercises/Ex07d.fst

@@ -89,8 +89,8 @@ let rec typing g e =
       | _         , _      , _       -> None)
 
 val progress : e:exp -> Lemma
-      (requires (is_Some (typing empty e)))
-      (ensures (is_value e \/ (is_Some (step e))))
+      (requires (Some? (typing empty e)))
+      (ensures (is_value e \/ (Some? (step e))))
 let rec progress e = 
   match e with
   | EVar y -> ()
@@ -119,8 +119,8 @@ let rec appears_free_in x e =
   | EFalse -> false
 
 val free_in_context : x:int -> e:exp -> g:env -> Lemma
-      (requires (is_Some (typing g e)))
-      (ensures (appears_free_in x e ==> is_Some (g x)))
+      (requires (Some? (typing g e)))
+      (ensures (appears_free_in x e ==> Some? (g x)))
 let rec free_in_context x e g =
   match e with
   | EVar _
@@ -132,7 +132,7 @@ let rec free_in_context x e g =
                     free_in_context x e2 g; free_in_context x e3 g
 
 val typable_empty_closed : x:int -> e:exp -> Lemma
-      (requires (is_Some (typing empty e)))
+      (requires (Some? (typing empty e)))
       (ensures (not(appears_free_in x e)))
       [SMTPat (appears_free_in x e)]
 let typable_empty_closed x e = free_in_context x e empty
@@ -167,10 +167,10 @@ val typing_extensional : g:env -> g':env -> e:exp
 let typing_extensional g g' e = context_invariance e g g'
 
 val substitution_preserves_typing : x:int -> e:exp -> v:exp ->
-      g:env{is_Some (typing empty v) &&
-            is_Some (typing (extend g x (Some.v (typing empty v))) e)} ->
+      g:env{Some? (typing empty v) &&
+            Some? (typing (extend g x (Some?.v (typing empty v))) e)} ->
       Tot (u:unit{typing g (subst x v e) ==
-                  typing (extend g x (Some.v (typing empty v))) e})
+                  typing (extend g x (Some?.v (typing empty v))) e})
 let rec substitution_preserves_typing x e v g =
   let Some t_x = typing empty v in
   let gx = extend g x t_x in
@@ -201,8 +201,8 @@ let rec substitution_preserves_typing x e v g =
         typing_extensional gxy gyx e1;
         substitution_preserves_typing x e1 v gy)
 
-val preservation : e:exp{is_Some (typing empty e) /\ is_Some (step e)} ->
-      Tot (u:unit{typing empty (Some.v (step e)) == typing empty e})
+val preservation : e:exp{Some? (typing empty e) /\ Some? (step e)} ->
+      Tot (u:unit{typing empty (Some?.v (step e)) == typing empty e})
 let rec preservation e =
   match e with
   | EApp e1 e2 ->
@@ -217,10 +217,10 @@ let rec preservation e =
       if is_value e1 then ()
       else preservation e1
 
-val typed_step : e:exp{is_Some (typing empty e) /\ not(is_value e)} ->
+val typed_step : e:exp{Some? (typing empty e) /\ not(is_value e)} ->
                  Tot (e':exp{typing empty e' = typing empty e})
-let typed_step e = progress e; preservation e; Some.v (step e)
+let typed_step e = progress e; preservation e; Some?.v (step e)
 
 (* Exercise: implement this function *)
-val eval : e:exp{is_Some (typing empty e)} ->
+val eval : e:exp{Some? (typing empty e)} ->
            Dv (v:exp{is_value v && typing empty v = typing empty e})

doc/tutorial/code/exercises/Ex10a.fst

@@ -15,11 +15,11 @@ type db = list entry
 (* We define two pure functions that test whether
    the suitable permission exists in some db *)
 let canWrite db file =
-  is_Some (tryFind (function Writable x -> x=file | _ -> false) db)
+  Some? (tryFind (function Writable x -> x=file | _ -> false) db)
 
 
 let canRead db file =
-  is_Some (tryFind (function Readable x | Writable x -> x=file) db)
+  Some? (tryFind (function Readable x | Writable x -> x=file) db)
 
 (* The acls reference stores the current access-control list, initially empty *)
 val acls: ref db

doc/tutorial/code/exercises/Ex10b.fst

@@ -11,41 +11,41 @@ val new_point: x:int -> y:int -> ST point
   (requires (fun h -> True))
   (ensures (fun h0 p h1 ->
                 modifies TSet.empty h0 h1
-                /\ fresh (Point.x p ^+^ Point.y p) h0 h1
-                /\ Heap.sel h1 (Point.x p) = x
-                /\ Heap.sel h1 (Point.y p) = y))
+                /\ fresh (Point?.x p ^+^ Point?.y p) h0 h1
+                /\ Heap.sel h1 (Point?.x p) = x
+                /\ Heap.sel h1 (Point?.y p) = y))
 let new_point x y =
   let x = alloc x in
   let y = alloc y in
   Point x y
 
 let shift_x p =
-  Point.x p := !(Point.x p) + 1
+  Point?.x p := !(Point?.x p) + 1
 
 // BEGIN: ShiftXP1Spec
 val shift_x_p1: p1:point
-           -> p2:point{   Point.x p2 <> Point.x p1
-                       /\ Point.y p2 <> Point.x p1 }
+           -> p2:point{   Point?.x p2 <> Point?.x p1
+                       /\ Point?.y p2 <> Point?.x p1 }
            -> ST unit
-    (requires (fun h -> Heap.contains h (Point.x p2)
-                    /\  Heap.contains h (Point.y p2)))
-    (ensures (fun h0 _ h1 -> modifies (only (Point.x p1)) h0 h1))
+    (requires (fun h -> Heap.contains h (Point?.x p2)
+                    /\  Heap.contains h (Point?.y p2)))
+    (ensures (fun h0 _ h1 -> modifies (only (Point?.x p1)) h0 h1))
 // END: ShiftXP1Spec
 
 let shift_x_p1 p1 p2 =
-    let p2_0 = !(Point.x p2), !(Point.y p2)  in //p2 is initially p2_0
+    let p2_0 = !(Point?.x p2), !(Point?.y p2)  in //p2 is initially p2_0
     shift_x p1;
-    let p2_1 = !(Point.x p2), !(Point.y p2) in
+    let p2_1 = !(Point?.x p2), !(Point?.y p2) in
     admit(); //fix the precondition and remove the admit
     assert (p2_0 = p2_1)                         //p2 is unchanged
 
 
 val test: unit -> St unit
 let test () =
   let p1 = new_point 0 0 in
-  recall (Point.x p1);
-  recall (Point.y p1);
+  recall (Point?.x p1);
+  recall (Point?.y p1);
   let p2 = new_point 0 1 in
-  recall (Point.x p2);
-  recall (Point.y p2);
+  recall (Point?.x p2);
+  recall (Point?.y p2);
   shift_x_p1 p1 p2