theories: monomorphic versions of arrays

parent 51437588
{
use array.ArrayRich as S
type char
type string = S.t char
clone array.ArrayMonoRich as S with type elt = char
type string = S.t
type rope =
| 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 inv l and 0 < len r and inv r
| Str s ofs len ->
len = 0 or 0 <= ofs < S.length s and ofs + len <= S.length s
| 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
......@@ -26,8 +28,8 @@
let empty () =
{}
Str (S.create 1) 0 0
{ len result = 0 and inv result and eq (model result) (S.create 0) }
Str (S.create_length 0) 0 0
{ len result = 0 and inv result and eq (model result) (S.create_length 0) }
let length r =
{}
......
......@@ -36,7 +36,7 @@ let get_num_classes (u:ref uf) =
let create (n:int) =
{ 0 <= n }
let l = ref (A.const_length 0 n) in
let l = ref (A.create_const_length 0 n) in
let i = ref 0 in
while !i < n do
invariant { 0 <= !i <= n and
......@@ -45,7 +45,7 @@ let create (n:int) =
l := A.set !l !i !i;
i := !i + 1
done;
ref (UF !l (A.const_length 0 n) n n)
ref (UF !l (A.create_const_length 0 n) n n)
{ inv !result and
num !result = n and size !result = n and
forall x:int. 0 <= x < n -> repr !result x = x }
......
......@@ -22,6 +22,8 @@ theory ArrayPoly
end
(* arrays with monomorphic keys *)
theory Array
type key
......@@ -41,9 +43,10 @@ theory Array
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
logic create_const 'a : t 'a
axiom Const : forall b:'a. forall a:key. get (const b) a = b
axiom Create_const_get :
forall b:'a. forall a:key. get (create_const b) a = b
end
......@@ -53,18 +56,23 @@ theory ArrayLength
logic length (t 'a) : int
logic const_length 'a int : t 'a
axiom Const_contents :
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_set :
forall a : t 'a. forall k : int. forall v : 'a.
length (set a k v) = length a
logic create_const_length 'a int : t 'a
axiom Create_const_length_get :
forall b:'a. forall n i:int. get (create_const_length b n) i = b
axiom Create_const_length_length :
forall a : 'a. forall n : int. length (create_const_length a n) = n
logic create_length int : t 'a
axiom Create_length_length :
forall n : int. length (create_length n : t 'a) = n
end
theory ArrayRich
......@@ -73,11 +81,6 @@ theory ArrayRich
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 :
......@@ -89,6 +92,96 @@ theory ArrayRich
logic app (t 'a) (t 'a) : t 'a
axiom App_length :
forall s1 s2 : t 'a. length (app s1 s2) = length s1 + length s2
axiom App_get :
forall s1 s2 : t 'a, i : int.
get (app s1 s2) i =
if i < length s1 then get s1 i else get s2 (i - length s1)
end
(* monomorphic versions (the type of elements is elt) *)
theory ArrayMono
type key
type elt
type t
logic get t key : elt
logic set t key elt : t
axiom Select_eq :
forall m : t. forall a1 a2 : key.
forall b : elt [get (set m a1 b) a2].
a1 = a2 -> get (set m a1 b) a2 = b
axiom Select_neq :
forall m : t. forall a1 a2 : key.
forall b : elt [get (set m a1 b) a2].
a1 <> a2 -> get (set m a1 b) a2 = get m a2
logic create_const elt : t
axiom Create_const_get :
forall b:elt. forall a:key. get (create_const b) a = b
end
theory ArrayMonoLength
clone export ArrayMono with type key = int
logic length t : int
axiom Length_set :
forall a : t. forall k : int. forall v : elt.
length (set a k v) = length a
logic create_const_length elt int : t
axiom Create_const_length_get :
forall b:elt. forall n i:int. get (create_const_length b n) i = b
axiom Create_const_length_length :
forall a : elt. forall n : int. length (create_const_length a n) = n
logic create_length int : t
axiom Create_length_length :
forall n : int. length (create_length n : t) = n
end
theory ArrayMonoRich
use import int.Int
clone export ArrayMonoLength
logic sub t int int : t
axiom Sub_length :
forall s : t, ofs len : int. length (sub s ofs len) = len
axiom Sub_get :
forall s : t, ofs len i : int.
get (sub s ofs len) i = get s (ofs + i)
logic app t t : t
axiom App_length :
forall s1 s2 : t. length (app s1 s2) = length s1 + length s2
axiom App_get :
forall s1 s2 : t, i : int.
get (app s1 s2) i =
if i < length s1 then get s1 i else get s2 (i - length s1)
end
theory BitVector
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment