theories: no more string (use array.ArrayMonoRich instead); theory renaming in array

examples/programs/dijkstra.mlw

 {
-use set.Fset as S
-use array.Array as M
+  use set.Fset as S
+  use array.ArrayPoly as M
 }
 
 (* iteration on a set *)
@@ -64,7 +64,7 @@ parameter init :
     unit writes visited, q, d 
     { S.is_empty !visited and 
       !q = S.add src S.empty and 
-      !d = M.store (old !d) src 0  }
+      !d = M.set (old !d) src 0  }
 
 parameter relax :
   u:vertex -> v:vertex -> 
@@ -72,19 +72,19 @@ parameter relax :
     unit reads visited writes d,q 
     { (S.mem v !visited and !q = old !q and !d = old !d) 
       or
-      (S.mem v !q and M.select !d u + weight u v >= M.select !d v and 
+      (S.mem v !q and M.get !d u + weight u v >= M.get !d v and 
         !q = old !q and !d = old !d) 
       or	
-      (S.mem v !q  and M.select !d u + weight u v < M.select !d v and 
-        !q = old !q and !d = M.store (old !d) v (M.select !d u + weight u v))
+      (S.mem v !q  and M.get !d u + weight u v < M.get !d v and 
+        !q = old !q and !d = M.set (old !d) v (M.get !d u + weight u v))
       or
       (not S.mem v !visited and not S.mem v !q and !q = S.add v (old !q) and
-        !d = M.store (old !d) v (M.select !d u + weight u v)) }	
+        !d = M.set (old !d) v (M.get !d u + weight u v)) }	
 
 {
 logic min (m:vertex) (q:S.t vertex) (d:M.t vertex int) =
   S.mem m q and 
-  forall x:vertex. S.mem x q -> M.select d x <= M.select d m
+  forall x:vertex. S.mem x q -> M.get d x <= M.get d m
 }
 
 parameter q_extract_min :
@@ -153,15 +153,15 @@ logic inv (src:vertex) (s q:S.t vertex) (d:M.t vertex int) =
   (forall v:vertex. S.mem v q -> S.mem v s -> false)
   (* we already found the shortest paths for vertices in S *)
   and
-  (forall v:vertex. S.mem v s -> shortest_path src v (M.select d v))
+  (forall v:vertex. S.mem v s -> shortest_path src v (M.get d v))
   (* there are paths for vertices in Q *)
   and
-  (forall v:vertex. S.mem v q -> path src v (M.select d v))
+  (forall v:vertex. S.mem v q -> path src v (M.get d v))
   (* vertices at distance < min(Q) are already in S *)
   and
   (forall m:vertex. min m q d -> 
      forall x:vertex. forall dx:int. shortest_path src x dx -> 
-       dx < M.select d m -> S.mem x s) 
+       dx < M.get d m -> S.mem x s) 
 
 logic inv_succ (src:vertex) (s q : S.t vertex) =
   (* successors of vertices in S are either in S or in Q *)
@@ -186,7 +186,7 @@ let shortest_path_code (src:vertex) (dst:vertex) =
     invariant { inv src !visited !q !d and inv_succ src !visited !q }
     variant   { S.cardinal v - S.cardinal !visited }
     let u = q_extract_min () in
-    assert { shortest_path src u (M.select !d u) };
+    assert { shortest_path src u (M.get !d u) };
     visited_add u;
     let su = ref (g_succ u) in
     while not (set_has_next su) do 
@@ -199,7 +199,7 @@ let shortest_path_code (src:vertex) (dst:vertex) =
     done
   done
   { (forall v:vertex. 
-       S.mem v !visited -> shortest_path src v (M.select !d v)) 
+       S.mem v !visited -> shortest_path src v (M.get !d v)) 
     and
     (forall v:vertex. 
        not S.mem v !visited -> forall dv:int. not path src v dv) }

examples/programs/fib.mlw

@@ -7,19 +7,19 @@
 
   type option 'a = None | Some 'a
 
-  use array.Array as A
+  use array.ArrayPoly as A
 
   type table = A.t int (option int)
 
   logic inv (t : table) =
-    forall x y : int. A.select t x = Some y -> y = fib x
+    forall x y : int. A.get t x = Some y -> y = fib x
 }
 
 parameter table : ref table
 
 parameter add : 
   x:int -> y:int -> 
-    {} unit writes table { !table = A.store (old !table) x (Some y) }
+    {} unit writes table { !table = A.set (old !table) x (Some y) }
 
 exception Not_found
 
@@ -27,8 +27,8 @@ parameter find :
   x:int -> 
    {} 
    int reads table raises Not_found 
-   { A.select !table x = Some result } 
-   | Not_found -> { A.select !table x = None }
+   { A.get !table x = Some result } 
+   | Not_found -> { A.get !table x = None }
   
 let rec fibo n =
   { 0 <= n and inv !table }

examples/programs/ropes.mlw

 
 {
-  use string.String as S
-  type string = S.t
+  use array.ArrayRich as S
+  type char
+  type string = S.t char
 
   type rope =
-    | Str string (*ofs:*) int (len: int)
-    | App rope rope (len: int)
+    | Str string int  (len: int)
+    | App rope   rope (len: int)
 
   logic inv (r: rope) = match r with
     | Str s ofs len -> 0 <= ofs < S.length s and ofs + len <= S.length s
-    | App l r len   -> 0 < len l and 0 < len r
-    end
+    | App l r   len -> 0 < len l and inv l and 0 < len r and inv r
+  end
 
   logic model (r: rope) : string = match r with
     | Str s ofs len -> S.sub s ofs len
     | App l r _     -> S.app (model l) (model r)
-    end
+  end
 
-}
+  logic eq (s1 s2: string) =
+    S.length s1 = S.length s2 and
+    forall i:int. 0 <= i < S.length s1 -> S.get s1 i = S.get s2 i
 
-let empty () = Str (S.create 0) 0 0
+}
 
-let length r = len r
+let empty () = 
+  {} 
+  Str (S.create 1) 0 0 
+  { len result = 0 and inv result and eq (model result) (S.create 0) }
+
+let length r = 
+  {} 
+  len r 
+  { result = len r }
+
+let rec get r i = 
+  { inv r and 0 <= i < len r }
+  match r with
+  | Str s ofs len -> 
+      S.get s (ofs + i)
+  | App l r   _   -> 
+      let n = length l in
+      if i < n then get l i else get r (i - n)
+  end
+  { result = S.get (model r) i }
 
 
 (*

examples/programs/vacid_0_sparse_array.mlw

@@ -31,7 +31,7 @@ back  +-+-+-+-------------------+
 
   type array 'a = A.t 'a
 
-  logic (#) (a : array 'a) (i : int) : 'a = A.select a i
+  logic (#) (a : array 'a) (i : int) : 'a = A.get a i
 
   type sparse_array = SA (sa_val  : array elt) 
                          (sa_idx  : array int)
@@ -106,8 +106,8 @@ let test a i =
   let idx = sa_idx !a in
   let back = sa_back !a in
   let n = sa_n !a in
-  0 <= A.select idx i && A.select idx i < n &&
-  A.select back (A.select idx i) = i
+  0 <= A.get idx i && A.get idx i < n &&
+  A.get back (A.get idx i) = i
   { result=True <-> is_elt !a i }
 
 (*
@@ -121,7 +121,7 @@ let get a i =
   { 0 <= i < sa_sz !a and invariant !a } 
   let val = sa_val !a in
   if test a i then
-    A.select val i 
+    A.get val i 
   else
     default
   { result = model !a i }
@@ -144,13 +144,13 @@ let set a i v =
   let back = sa_back !a in
   let sz= sa_sz !a in
   let n = sa_n !a in
-  let val = A.store val i v in
+  let val = A.set val i v in
   if test a i then
     a := SA val idx back sz n
   else begin
     assert { n < sz };
-    let idx = A.store idx i n in 
-    let back = A.store back n i in
+    let idx = A.set idx i n in 
+    let back = A.set back n i in
     a := SA val idx back sz (n+1)
   end
   { invariant !a and 

examples/programs/vacid_0_union_find.mlw

@@ -5,7 +5,7 @@
 
   type array 'a = A.t 'a
 
-  logic (#) (a : array 'a) (i : int) : 'a = A.select a i
+  logic (#) (a : array 'a) (i : int) : 'a = A.get a i
 
   type uf = UF (link : array int)
                (dist : array int) (* distance to representative *)
@@ -42,7 +42,7 @@ let create (n:int) =
     invariant { 0 <= !i <= n and
                 forall j:int. 0 <= j < !i -> !l#j = j } 
     variant { n - !i }
-    l := A.store !l !i !i;
+    l := A.set !l !i !i;
     i := !i + 1
   done;
   ref (UF !l (A.const_length 0 n) n n)
@@ -52,11 +52,11 @@ let create (n:int) =
 
 let rec find (u:ref uf) (x:int) variant { dist !u # x } =
   { inv !u and 0 <= x < size !u } 
-  let y = A.select (link !u) x in
+  let y = A.get (link !u) x in
   if y <> x then begin
     let r = find u y in
-    let l = A.store (link !u) x r in
-    let d = A.store (dist !u) x 1 in
+    let l = A.set (link !u) x r in
+    let d = A.set (dist !u) x 1 in
     u := UF l d (size !u) (num !u);
     r
   end else
@@ -82,7 +82,7 @@ let increment (u : ref uf) (r : int) =
                        if repr !u j = r and j < !i then 1 else 0 }
     variant { size !u - !i }
     if ghost_find u !i = r then
-      d := A.store !d !i (A.select !d !i + 1)
+      d := A.set !d !i (A.get !d !i + 1)
   done;
   !d
   { forall i:int. 0 <= i < size !u ->
@@ -95,7 +95,7 @@ let union (u:ref uf) (a b:int) =
   let rb = find u b in
   let l = link !u in
   let d = increment u ra in
-  u := UF (A.store l ra rb) d (size !u) (num !u - 1)
+  u := UF (A.set l ra rb) d (size !u) (num !u - 1)
   { inv !u and 
     same !u a b and
     size !u = size (old !u) and num !u = num (old !u) - 1 and 

theories/array.why

 
-theory Array
+theory ArrayPoly
 
   type t 'a 'b
 
-  logic select (t 'a 'b) 'a : 'b
-  logic store (t 'a 'b) 'a 'b : t 'a 'b
+  logic get (t 'a 'b) 'a : 'b
+  logic set (t 'a 'b) 'a 'b : t 'a 'b
   
   axiom Select_eq : 
     forall m : t 'a 'b. forall a1 a2 : 'a. 
-    forall b : 'b [select (store m a1 b) a2].
-    a1 = a2 -> select (store m a1 b) a2  = b
+    forall b : 'b [get (set m a1 b) a2].
+    a1 = a2 -> get (set m a1 b) a2  = b
 
   axiom Select_neq : 
     forall m : t 'a 'b. forall a1 a2 : 'a. 
-    forall b : 'b [select (store m a1 b) a2].
-    a1 <> a2 -> select (store m a1 b) a2 = select m a2
+    forall b : 'b [get (set m a1 b) a2].
+    a1 <> a2 -> get (set m a1 b) a2 = get m a2
 
   logic const 'b : t 'a 'b
 
-  axiom Const : forall b:'b, a:'a. select (const b) a = b
+  axiom Const : forall b:'b, a:'a. get (const b) a = b
 
 end
 
-theory ArrayKey
+theory Array
 
   type key
 
   type t 'a
 
-  logic select (t 'a) key : 'a
-  logic store (t 'a) key 'a : t 'a
+  logic get (t 'a) key : 'a
+  logic set (t 'a) key 'a : t 'a
   
   axiom Select_eq : 
     forall m : t 'a. forall a1 a2 : key. 
-    forall b : 'a [select (store m a1 b) a2].
-    a1 = a2 -> select (store m a1 b) a2 = b
+    forall b : 'a [get (set m a1 b) a2].
+    a1 = a2 -> get (set m a1 b) a2 = b
 
   axiom Select_neq : 
     forall m : t 'a. forall a1 a2 : key. 
-    forall b : 'a [select (store m a1 b) a2].
-    a1 <> a2 -> select (store m a1 b) a2 = select m a2
+    forall b : 'a [get (set m a1 b) a2].
+    a1 <> a2 -> get (set m a1 b) a2 = get m a2
 
   logic const 'a : t 'a
 
-  axiom Const : forall b:'a. forall a:key. select (const b) a = b
+  axiom Const : forall b:'a. forall a:key. get (const b) a = b
 
 end
 
 theory ArrayLength
 
-  clone export ArrayKey with type key = int
+  clone export Array with type key = int
 
   logic length (t 'a) : int
 
   logic const_length 'a int : t 'a
 
   axiom Const_contents : 
-    forall b:'a. forall n i:int. select (const_length b n) i = b
+    forall b:'a. forall n i:int. get (const_length b n) i = b
 
   axiom Length_const : 
     forall a : 'a. forall n : int. length (const_length a n) = n
 
-  axiom Length_store : 
+  axiom Length_set : 
     forall a : t 'a. forall k : int. forall v : 'a.
-    length (store a k v) = length a
+    length (set a k v) = length a
+
+end
+
+theory ArrayRich
+
+  use import int.Int
+  
+  clone export ArrayLength
+
+  logic create int : t 'a
+
+  axiom Create_length : 
+    forall n : int. length (create n : t 'a) = n
+
+  logic sub (t 'a) int int : t 'a
+
+  axiom Sub_length : 
+    forall s : t 'a, ofs len : int. length (sub s ofs len) = len
+
+  axiom Sub_get :
+    forall s : t 'a, ofs len i : int. 
+    get (sub s ofs len) i = get s (ofs + i)
+
+  logic app (t 'a) (t 'a) : t 'a
 
 end
 

theories/string.why

-
-theory String
-
-  use import int.Int
-
-  type char
-
-  type t
-
-  logic get t int : char
-  logic set t int char : t
-  
-  axiom Get_set_eq : 
-    forall s : t. forall i j : int. 
-    forall c : char [get (set s i c) j].
-    i = j -> get (set s i c) j = c
-
-  axiom Get_set_neq : 
-    forall s : t. forall i j : int. 
-    forall c : char [get (set s i c) j].
-    i <> j -> get (set s i c) j = get s j
-
-  logic length t : int
-
-  logic create int : t
-
-  axiom Create_length : 
-    forall n : int. length (create n) = n
-
-  axiom Length_set : 
-    forall s : t. forall i : int. forall c : char.
-    length (set s i c) = length s
-
-  logic sub t int int : t
-
-  logic app t t : t
-
-end