theories: array -> map

parent 592bab9b
......@@ -143,16 +143,6 @@ theory algebra.AC
remove cloned prop Assoc.Assoc
end
(*
theory array.ArrayLength
syntax type t "%1 farray"
syntax logic select "(%1[%2])"
syntax logic store "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end
*)
(*
Local Variables:
mode: why
......
......@@ -144,8 +144,8 @@ theory algebra.AC
end
theory array.Array
syntax type t "(%1,%2) farray"
theory map.Map
syntax type map "(%1,%2) farray"
syntax logic get "(%1[%2])"
syntax logic set "(%1[%2 <- %3])"
end
......
......@@ -132,8 +132,8 @@ end
*)
theory array.Array
syntax type t "(ARRAY %1 OF %2)"
theory map.Map
syntax type map "(ARRAY %1 OF %2)"
meta "encoding : lskept" logic get
meta "encoding : lskept" logic set
......
......@@ -148,8 +148,8 @@ theory real.Truncate
end
*)
theory array.Array
syntax type t "(Array %1 %2)"
theory map.Map
syntax type map "(Array %1 %2)"
meta "encoding : lskept" logic get
meta "encoding : lskept" logic set
meta "encoding : lskept" logic create_const
......
theory Bidule
use import set.SetArray
use import set.SetMap
type a
type s = t a
type s = set a
logic a : s
logic b : s
......
theory Sorted
use import int.Int
use real.Real
use import array.Array
use import map.Map
type array = t int real
type multi = t real int
type array = map int real
type multi = map real int
logic n : int = 4
......
......@@ -29,12 +29,11 @@ end
module Array
use import int.Int
use import array.Array
type map 'a = t int 'a
use import map.Map as M
type array 'a model {| length : int; mutable elts : map 'a |}
type array 'a model {| length : int; mutable elts : map int 'a |}
logic ([]) (a: array 'a) (i :int) : 'a = get a.elts i
logic ([]) (a: array 'a) (i :int) : 'a = M.([]) a.elts i
parameter get : a:array 'a -> i:int ->
{ 0 <= i < length a } 'a reads a { result = a[i] }
......@@ -98,6 +97,46 @@ module Array
end
module ArraySorted
use import module Array
clone import map.MapSorted as M
logic sorted_sub (a : array elt) (l u : int) =
M.sorted_sub a.elts l u
logic sorted (a : array elt) =
M.sorted_sub a.elts 0 a.length
end
module ArrayEq
use import module Array
clone import map.MapEq as M
logic array_eq_sub (a1 a2: array 'a) (l u: int) =
map_eq_sub a1.elts a2.elts l u
logic array_eq (a1 a2 : array 'a) =
a1.length = a2.length and
array_eq_sub a1 a2 0 a1.length
end
module ArrayPermut
use import module Array
clone import map.MapPermut as M
logic permut_sub (a1 a2 : array 'a) (l u: int) =
M.permut_sub a1.elts a2.elts l u
logic permut (a1 a2 : array 'a) =
a1.length = a2.length and M.permut_sub a1.elts a2.elts 0 a1.length
end
module TestArray
use import int.Int
......
......@@ -217,12 +217,10 @@ let use_export_theory uc th =
add_ns th.th_export uc
let add_impure_pdecl env ltm d uc =
{ uc with uc_impure =
Typing.add_decl env ltm uc.uc_impure d }
{ uc with uc_impure = Typing.add_decl env ltm uc.uc_impure d }
let add_effect_pdecl env ltm d uc =
{ uc with uc_effect =
Typing.add_decl env ltm uc.uc_effect d; }
{ uc with uc_effect = Typing.add_decl env ltm uc.uc_effect d; }
let add_pure_pdecl env ltm d uc =
{ uc with uc_pure = Typing.add_decl env ltm uc.uc_pure d; }
......
theory Array "Theory of arrays"
theory Map "Theory of maps"
type t 'a 'b
type map 'a 'b
logic get (t 'a 'b) 'a : 'b
logic set (t 'a 'b) 'a 'b : t 'a 'b
logic get (a : map 'a 'b) (i : 'a) : 'b
logic set (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b
(* syntactic sugar *)
logic ([]) (a : t 'a 'b) (i : 'a) : 'b = get a i
logic ([<-]) (a : t 'a 'b) (i : 'a) (v : 'b) : t 'a 'b = set a i v
logic ([]) (a : map 'a 'b) (i : 'a) : 'b = get a i
logic ([<-]) (a : map 'a 'b) (i : 'a) (v : 'b) : map 'a 'b = set a i v
axiom Select_eq :
forall m : t 'a 'b. forall a1 a2 : 'a.
forall b : 'b [get (set m a1 b) a2].
a1 = a2 -> get (set m a1 b) a2 = b
forall m : map 'a 'b. forall a1 a2 : 'a.
forall b : 'b [m[a1 <- b][a2]].
a1 = a2 -> m[a1 <- b][a2] = b
axiom Select_neq :
forall m : t 'a 'b. forall a1 a2 : 'a.
forall b : 'b [get (set m a1 b) a2].
a1 <> a2 -> get (set m a1 b) a2 = get m a2
forall m : map 'a 'b. forall a1 a2 : 'a.
forall b : 'b [m[a1 <- b][a2]].
a1 <> a2 -> m[a1 <- b][a2] = m[a2]
logic create_const 'b : t 'a 'b
logic create_const 'b : map 'a 'b
axiom Const : forall b:'b, a:'a. get (create_const b) a = b
axiom Const : forall b:'b, a:'a. (create_const b)[a] = b
end
theory ArrayLength "Theory of arrays with length"
(* these arrays ... *)
theory MapSorted
use import int.Int
use export Array
type map 'a = t int 'a
logic length (map 'a) : int
axiom Length_non_negative (* "Array length is always non negative" *):
forall a : map 'a. length a >= 0
axiom Length_set :
forall a : map 'a. forall k : int. forall v : 'a.
length (set a k v) = length a
logic create_const_length 'a int : map 'a
(* [create_const_length x n] is the array of length n
with all cells initialized to x
(not specified if n is negative)
*)
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.
(* premise needed to guaranty length >= 0 invariant *)
n >= 0 -> length (create_const_length a n) = n
logic create_length int : map 'a
axiom Create_length_length :
forall n : int.
(* premise needed to guaranty length >= 0 invariant *)
n >=0 -> length (create_length n : map 'a) = n
end
theory ArraySorted
use import int.Int
use import ArrayLength
use import Map
type elt
logic le elt elt
logic sorted_sub (a : map elt) (l u : int) =
forall i1 i2 : int. l <= i1 <= i2 <= u -> le a[i1] a[i2]
logic sorted (a : map elt) =
sorted_sub a 0 (length a - 1)
(* a[l..u) is sorted for le *)
logic sorted_sub (a : map int elt) (l u : int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
end
theory ArrayEq
theory MapEq
use import int.Int
use export ArrayLength
use export Map
logic array_eq_sub (a1 a2 : map 'a) (l u : int) =
forall i:int. l <= i <= u -> a1[i] = a2[i]
logic array_eq (a1 a2 : map 'a) =
length a1 = length a2 and
forall i:int. 0 <= i < length a1 -> a1[i] = a2[i]
logic map_eq_sub (a1 a2 : map int 'a) (l u : int) =
forall i:int. l <= i < u -> a1[i] = a2[i]
end
theory ArrayPermut
theory MapPermut
use import int.Int
use export ArrayLength
use export Map
logic exchange (a1 a2 : map 'a) (i j : int) =
length a1 = length a2 and
logic exchange (a1 a2 : map int 'a) (i j : int) =
a1[i] = a2[j] and a2[i] = a1[j] and
forall k:int. (k <> i and k <> j) -> a1[k] = a2[k]
lemma exchange_set :
forall a : map 'a. forall i j : int.
exchange a (set (set a i a[j]) j a[i]) i j
forall a : map int 'a. forall i j : int.
exchange a a[i <- a[j]][j <- a[i]] i j
inductive permut (map 'a) (map 'a) int int =
inductive permut_sub (map int 'a) (map int 'a) int int =
| permut_refl :
forall a : map 'a. forall l u : int. permut a a l u
forall a : map int 'a. forall l u : int. permut_sub a a l u
| permut_sym :
forall a1 a2 : map 'a. forall l u : int.
permut a1 a2 l u -> permut a2 a1 l u
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a1 l u
| permut_trans :
forall a1 a2 a3 : map 'a. forall l u : int.
permut a1 a2 l u -> permut a2 a3 l u -> permut a1 a3 l u
forall a1 a2 a3 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a3 l u -> permut_sub a1 a3 l u
| permut_exchange :
forall a1 a2 : map 'a. forall l u i j : int.
l <= i <= u -> l <= j <= u -> exchange a1 a2 i j -> permut a1 a2 l u
forall a1 a2 : map int 'a. forall l u i j : int.
l <= i < u -> l <= j < u -> exchange a1 a2 i j -> permut_sub a1 a2 l u
lemma permut_weakening :
forall a1 a2 : map 'a. forall l1 r1 l2 r2 : int.
l1 <= l2 <= r2 <= r1 -> permut a1 a2 l2 r2 -> permut a1 a2 l1 r1
forall a1 a2 : map int 'a. forall l1 r1 l2 r2 : int.
l1 <= l2 <= r2 <= r1 -> permut_sub a1 a2 l2 r2 -> permut_sub a1 a2 l1 r1
lemma permut_eq :
forall a1 a2 : map 'a. forall l u : int.
l <= u -> permut a1 a2 l u ->
forall a1 a2 : map int 'a. forall l u : int.
l <= u -> permut_sub a1 a2 l u ->
forall i:int. (i < l or u < i) -> a2[i] = a1[i]
lemma permut_length :
forall a1 a2 : map 'a. forall l u : int.
permut a1 a2 l u -> length a1 = length a2
lemma permut_exists :
forall a1 a2 : map 'a. forall l u : int.
permut a1 a2 l u ->
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u ->
forall i : int. l <= i <= u ->
exists j : int. l <= j <= u and a2[i] = a1[j]
logic permutation (a1 a2 : map 'a) =
permut a1 a2 0 (length a1 - 1)
use export ArrayEq
lemma array_eq_permut :
forall a1 a2 : map 'a. forall l u : int.
array_eq_sub a1 a2 l u -> permut a1 a2 l u
end
theory ArrayRich
use import int.Int
use export ArrayLength
logic sub (map 'a) int int : map 'a
axiom Sub_length :
forall s : map 'a, ofs len : int.
len >= 0 ->
length (sub s ofs len) = len
axiom Sub_get :
forall s : map 'a, ofs len i : int.
get (sub s ofs len) i = get s (ofs + i)
logic app (map 'a) (map 'a) : map 'a
axiom App_length :
forall s1 s2 : map 'a. length (app s1 s2) = length s1 + length s2
axiom App_get :
forall s1 s2 : map 'a, i : int.
get (app s1 s2) i =
if i < length s1 then get s1 i else get s2 (i - length s1)
end
theory BitVector
......@@ -278,6 +187,6 @@ end
(*
Local Variables:
compile-command: "make -C .. theories/array"
compile-command: "make -C .. theories/map"
End:
*)
theory Set
type t 'a
type set 'a
logic mem 'a (t 'a)
logic mem 'a (set 'a)
logic empty : t 'a
logic empty : set 'a
logic is_empty (s : t 'a) = forall x : 'a. not mem x s
logic is_empty (s : set 'a) = forall x : 'a. not mem x s
axiom Empty_def1 : is_empty(empty : t 'a)
axiom Empty_def1 : is_empty(empty : set 'a)
logic add 'a (t 'a) : t 'a
logic add 'a (set 'a) : set 'a
axiom Add_def1 :
forall x y : 'a. forall s : t 'a.
forall x y : 'a. forall s : set 'a.
mem x (add y s) <-> x = y or mem x s
logic remove 'a (t 'a) : t 'a
logic remove 'a (set 'a) : set 'a
axiom Remove_def1 :
forall x y : 'a. forall s : t 'a.
forall x y : 'a. forall s : set 'a.
mem x (remove y s) <-> x <> y and mem x s
logic union (t 'a) (t 'a) : t 'a
logic union (set 'a) (set 'a) : set 'a
axiom Union_def1 :
forall s1 s2 : t 'a. forall x : 'a.
forall s1 s2 : set 'a. forall x : 'a.
mem x (union s1 s2) <-> mem x s1 or mem x s2
logic inter (t 'a) (t 'a) : t 'a
logic inter (set 'a) (set 'a) : set 'a
axiom Inter_def1 :
forall s1 s2 : t 'a. forall x : 'a.
forall s1 s2 : set 'a. forall x : 'a.
mem x (inter s1 s2) <-> mem x s1 and mem x s2
logic diff (t 'a) (t 'a) : t 'a
logic diff (set 'a) (set 'a) : set 'a
axiom Diff_def1 :
forall s1 s2 : t 'a. forall x : 'a.
forall s1 s2 : set 'a. forall x : 'a.
mem x (diff s1 s2) <-> mem x s1 and not mem x s2
logic equal(s1 s2 : t 'a) = forall x : 'a. mem x s1 <-> mem x s2
logic equal(s1 s2 : set 'a) = forall x : 'a. mem x s1 <-> mem x s2
logic subset(s1 s2 : t 'a) = forall x : 'a. mem x s1 -> mem x s2
logic subset(s1 s2 : set 'a) = forall x : 'a. mem x s1 -> mem x s2
end
......@@ -52,22 +52,22 @@ theory Fset
use import int.Int
clone export Set
logic cardinal (t 'a) : int
logic cardinal (set 'a) : int
axiom Cardinal_nonneg : forall s : t 'a. cardinal s >= 0
axiom Cardinal_nonneg : forall s : set 'a. cardinal s >= 0
axiom Cardinal_empty : cardinal(empty : t 'a) = 0
axiom Cardinal_empty : cardinal(empty : set 'a) = 0
axiom Cardinal_add :
forall x : 'a. forall s : t 'a.
forall x : 'a. forall s : set 'a.
not mem x s -> cardinal (add x s) = 1 + cardinal s
axiom Cardinal_remove :
forall x : 'a. forall s : t 'a.
forall x : 'a. forall s : set 'a.
mem x s -> cardinal s = 1 + cardinal (remove x s)
axiom Cardinal_subset :
forall s1 s2 : t 'a. subset s1 s2 -> cardinal s1 <= cardinal s2
forall s1 s2 : set 'a. subset s1 s2 -> cardinal s1 <= cardinal s2
end
......@@ -75,57 +75,64 @@ theory FsetExt
use export Fset
axiom ext: forall s1 s2 : t 'a.
axiom ext: forall s1 s2 : set 'a.
s1 = s2 <-> (forall x : 'a. mem x s1 <-> mem x s2)
end
theory SetArray
use import array.Array as A
theory SetMap
use import map.Map
use import bool.Bool
type t 'a = A.t 'a bool
type set 'a = map 'a bool
logic mem (x:'a) (s:t 'a) = get s x = True
logic mem (x:'a) (s:set 'a) = s[x] = True
logic empty : t 'a = create_const False
logic empty : set 'a = create_const False
logic is_empty (s : t 'a) = forall x : 'a. not mem x s
logic is_empty (s : set 'a) = forall x : 'a. not mem x s
goal Empty_def1 : is_empty(empty : t 'a)
goal Empty_def1 : is_empty(empty : set 'a)
logic add (x:'a) (s:t 'a) : t 'a = set s x True
logic add (x:'a) (s:set 'a) : set 'a = s[x <- True]
logic remove (x:'a) (s:t 'a) : t 'a = set s x False
logic remove (x:'a) (s:set 'a) : set 'a = s[x <- False]
logic union (t 'a) (t 'a) : t 'a
logic union (set 'a) (set 'a) : set 'a
axiom Union_def :
forall s1 s2 : t 'a. forall x : 'a.
get (union s1 s2) x = orb (get s1 x) (get s2 x)
forall s1 s2 : set 'a. forall x : 'a.
(union s1 s2)[x] = orb s1[x] s2[x]
logic inter (t 'a) (t 'a) : t 'a
logic inter (set 'a) (set 'a) : set 'a
axiom Inter_def :
forall s1 s2 : t 'a. forall x : 'a.
get (inter s1 s2) x = andb (get s1 x) (get s2 x)
forall s1 s2 : set 'a. forall x : 'a.
(inter s1 s2)[x] = andb s1[x] s2[x]
logic diff (t 'a) (t 'a) : t 'a
logic diff (set 'a) (set 'a) : set 'a
axiom Diff_def1 :
forall s1 s2 : t 'a. forall x : 'a.
get (diff s1 s2) x = xorb (get s1 x) (get s2 x)
forall s1 s2 : set 'a. forall x : 'a.
(diff s1 s2)[x] = xorb s1[x] s2[x]
logic equal(s1 s2 : t 'a) = forall x : 'a. get s1 x = get s2 x
logic equal(s1 s2 : set 'a) = forall x : 'a. s1[x] = s2[x]
axiom Equal_is_eq : forall s1 s2 : t 'a. equal s1 s2 -> s1 = s2
axiom Equal_is_eq : forall s1 s2 : set 'a. equal s1 s2 -> s1 = s2
logic subset(s1 s2 : t 'a) = forall x : 'a. mem x s1 -> mem x s2
logic subset(s1 s2 : set 'a) = forall x : 'a. mem x s1 -> mem x s2
logic complement (t 'a) : t 'a
logic complement (set 'a) : set 'a
axiom Complement_def :
forall s : t 'a. forall x : 'a.
get (complement s) x = notb (get s x)
forall s : set 'a. forall x : 'a.
(complement s)[x] = notb s[x]
end
\ No newline at end of file
end
(*
Local Variables:
compile-command: "make -C .. theories/set"
End:
*)
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