Merge pull request #513 from mtzguido/misc

Misc

Author: mtzguido

share/pulse/examples/by-example/PulseByExample.fst

@@ -17,6 +17,7 @@
 module PulseByExample
 
 open Pulse.Lib.Core
+open Pulse.Class.PtsTo
 
 (* 
   Things to note:
@@ -64,11 +65,11 @@ module R = Pulse.Lib.Reference
 *)
 fn ref_swap (r1 r2:ref int)
   requires
-    R.pts_to r1 'n1 **
-    R.pts_to r2 'n2
+    r1 |-> 'n1 **
+    r2 |-> 'n2
   ensures
-    R.pts_to r1 'n2 **
-    R.pts_to r2 'n1
+    r1 |-> 'n2 **
+    r2 |-> 'n1
 
 {
   let v1 = !r1;
@@ -78,26 +79,26 @@ fn ref_swap (r1 r2:ref int)
 
 fn ref_non_zero (r1:ref int) (n1:Ghost.erased int)
 requires
-  R.pts_to r1 n1
+  r1 |-> n1
 returns b:bool
-ensures R.pts_to r1 n1 ** pure (b == (Ghost.reveal n1 <> 0))
+ensures r1 |-> n1 ** pure (b == (Ghost.reveal n1 <> 0))
 {
   (0 <> !r1);
 }
 
 fn id (r:ref int)
   requires
-    R.pts_to r 'n
+    r |-> 'n
   returns r':ref int
   ensures
-    R.pts_to r' 'n ** pure (r == r')
+    r' |-> 'n ** pure (r == r')
 {
   r;
 }
 
 fn set (r:ref int) (x:int)
-requires R.pts_to r 'n
-ensures R.pts_to r x
+requires r |-> 'n
+ensures r |-> x
 {
   r := x;
 }
@@ -109,9 +110,9 @@ fn go () () ()
 
 fn test (r:ref int)
   requires 
-    R.pts_to r 'n
+    r |-> 'n
   ensures
-    R.pts_to r 2
+    r |-> 2
 {
   go (set r 1) (set r 4) (set r 2);
 }
@@ -131,11 +132,11 @@ open Pulse.Lib.BoundedIntegers
 
 fn arr_swap (#t:Type0) (n i j:SZ.t) (a:larray t (v n))
   requires
-    A.pts_to a 's0 **
+    a |-> 's0 **
     pure (Seq.length 's0 == v n /\ i < n /\ j < n)
   ensures
     exists* s. 
-    A.pts_to a s **
+    a |-> s **
     pure (Seq.length 's0 == v n /\ Seq.length s == v n /\ i < n /\ j < n
        /\ (forall (k:nat). k < v n /\ k <> v i /\ k <> v j ==> Seq.index 's0 k == Seq.index s k)
        /\ Seq.index 's0 (v i) == Seq.index s (v j)
@@ -156,21 +157,21 @@ fn arr_swap (#t:Type0) (n i j:SZ.t) (a:larray t (v n))
 
 fn max (n:SZ.t) (a:larray nat (v n))
   requires
-    A.pts_to a #'p 's **
+    a |-> Frac 'p 's **
     pure (Seq.length 's == v n)
   returns r:nat
   ensures
-    A.pts_to a #'p 's **
+    a |-> Frac 'p 's **
     pure (Seq.length 's == v n /\
           (forall (i:nat). i < v n ==> Seq.index 's i <= r))
 {
   let mut i : SZ.t = 0sz;
   let mut max : nat = 0;
   while (!i < n)
   invariant exists* (vi:SZ.t) (vmax:nat).
-    A.pts_to a #'p 's **
-    R.pts_to i vi **
-    R.pts_to max vmax **
+    a |-> Frac 'p 's **
+    i |-> vi **
+    max |-> vmax **
     pure (vi <= n
        /\ (forall (j:nat). j < v vi ==> Seq.index 's j <= vmax))
   {
@@ -186,21 +187,21 @@ fn max (n:SZ.t) (a:larray nat (v n))
 
 fn max_alt (n:SZ.t) (a:larray nat (v n))
   requires
-    A.pts_to a #'p 's **
+    a |-> Frac 'p 's **
     pure (Seq.length 's == v n)
   returns r:nat
   ensures
-    A.pts_to a #'p 's **
+    a |-> Frac 'p 's **
     pure (Seq.length 's == v n /\
           (forall (i:nat). i < v n ==> Seq.index 's i <= r))
 {
   let mut i = 0sz;
   let mut max : nat = 0;
   while (!i < n)
   invariant exists* (vi:SZ.t) (vmax:nat).
-    A.pts_to a #'p 's **
-    R.pts_to i vi **
-    R.pts_to max vmax **
+    a |-> Frac 'p 's **
+    i |-> vi **
+    max |-> vmax **
     pure (vi <= n
        /\ (forall (j:nat). j < v vi ==> Seq.index 's j <= vmax))
   {
@@ -211,4 +212,4 @@ fn max_alt (n:SZ.t) (a:larray nat (v n))
     }
   };
   !max
-}
+}

src/checker/Pulse.Checker.Pure.fst

@@ -66,8 +66,8 @@ let check_ln (g:env) (label:string) (t:R.term) : Tac unit =
 let rtb_core_compute_term_type g f e =
   debug g (fun _ ->
     Printf.sprintf "(%s) Calling core_compute_term_type on %s"
-          (T.range_to_string (RU.range_of_term e))
-          (T.term_to_string e));
+          (show (RU.range_of_term e))
+          (show e));
   let res = RU.with_context (get_context g) (fun _ -> RTB.core_compute_term_type f e) in
   res
 
@@ -76,17 +76,17 @@ let rtb_tc_term g f e =
   let e = RU.deep_transform_to_unary_applications e in
   debug g (fun _ ->
     Printf.sprintf "(%s) Calling tc_term on %s"
-      (T.range_to_string (RU.range_of_term e))
-      (T.term_to_string e));
+      (show (RU.range_of_term e))
+      (show e));
   let res = RU.with_context (get_context g) (fun _ -> RTB.tc_term f e) in
   res
 
 let rtb_universe_of (g:env) (f:T.env) (e: T.term)
 : T.Tac (option (u:T.universe{typing_token f e (E_Total, T.pack_ln (Tv_Type u))}) & issues)
 = debug g (fun _ ->
     Printf.sprintf "(%s) Calling universe_of on %s"
-      (T.range_to_string (RU.range_of_term e))
-      (T.term_to_string e));
+      (show (RU.range_of_term e))
+      (show e));
   let res = RU.with_context (get_context g) (fun _ -> RTB.universe_of f e) in
   res
 
@@ -100,17 +100,17 @@ let universe_of_well_typed_term_internal  (g:env) (f:T.env) (e: T.term)
 let rtb_check_subtyping g (t1 t2:term) : Tac (ret_t (subtyping_token g t1 t2)) =
   debug g (fun _ ->
     Printf.sprintf "(%s, %s) Calling check_subtyping on %s <: %s"
-        (T.range_to_string (RU.range_of_term t1))
-        (T.range_to_string (RU.range_of_term t2))
-        (P.term_to_string t1)
-        (P.term_to_string t2));
+        (show (RU.range_of_term t1))
+        (show (RU.range_of_term t2))
+        (show t1)
+        (show t2));
   let f = elab_env_with_range g None in
   let res = RU.with_context (get_context g) (fun _ -> RTB.check_subtyping f t1 t2) in
   res
 
 let rtb_instantiate_implicits g f t expected inst_extra =
   debug g (fun _ -> Printf.sprintf "Calling instantiate_implicits on %s"
-                                       (T.term_to_string t));
+                                       (show t));
   (* WARN: unary dependence, see comment in RU *)
   let t = RU.deep_transform_to_unary_applications t in
   let res, iss = RU.with_context (get_context g) (fun _ -> RTB.instantiate_implicits f t expected inst_extra) in
@@ -151,8 +151,8 @@ let rtb_check_prop_validity (g:env) (sync:bool) (f:_{f == elab_env g }) (p:_) (p
   in
   debug g (fun _ -> 
     Printf.sprintf "(%s) Calling check_prop_validity on %s"
-          (T.range_to_string (RU.range_of_term p))
-          (T.term_to_string p));
+          (show (RU.range_of_term p))
+          (show p));
   let sp = mk_squash0 p in
   let _ : squash (typing_token f sp (E_Total, (`prop))) = magic () in //squash typing
   let res, issues = 
@@ -178,7 +178,7 @@ let catch_all (f:unit -> Tac (option 'a & issues))
 
 let readback_failure (s:R.term) =
   Printf.sprintf "Internal error: failed to readback F* term %s"
-                 (T.term_to_string s)
+                 (show s)
 
 (* Set got_typ = None if we don't have a good type for `t`.
 Note that calling this with None for expected_typ, but Some _ for got_typ
@@ -347,8 +347,8 @@ let compute_term_type (g:env) (t:term)
     = let rng, fg = elab_env_with_term_range g t in
       debug g (fun _ ->
               Printf.sprintf "check_tot : called on %s elaborated to %s"
-                        (P.term_to_string t)
-                        (T.term_to_string t));
+                        (show t)
+                        (show t));
       let res, issues = tc_meta_callback g fg t in
       match res with
       | None -> 
@@ -595,7 +595,7 @@ let try_get_non_informative_witness_aux (g:env) (u:universe) (ty:term) (ty_typin
     | None, issues ->
       None, issues
     | Some r_dict, issues -> (
-      // T.print (Printf.sprintf "Resolved to %s" (T.term_to_string r_dict));
+      // T.print (Printf.sprintf "Resolved to %s" (show r_dict));
       assert (typing_token r_env r_dict (E_Total, goal));
       assume (~(Tv_Unknown? (inspect_ln r_dict)));
       let dict = wr r_dict (RU.range_of_term ty) in
@@ -711,4 +711,4 @@ let norm_well_typed_term_alt
   = let (| t, ty, rel |) = RU.norm_well_typed_term ty steps in
     (|t, ty, rel|)
     in
-    RU.record_stats "Pulse.norm_well_typed_term_alt" aux
+    RU.record_stats "Pulse.norm_well_typed_term_alt" aux