Commit 34ff042c authored by Francois Bobot's avatar Francois Bobot

ajout de théories dans test.why

parent 5a3231c6
......@@ -191,6 +191,10 @@ uqualid:
| uqualid DOT uident { Qdot ($1, $3) }
;
qualid:
|lqualid {$1}
|uqualid {$1}
decl:
| LOGIC list1_lident_sep_comma COLON logic_type
{ Logic (loc_i 3, $2, $4) }
......@@ -370,9 +374,9 @@ lexpr:
{ infix_pp $1 PPmod $3 }
| MINUS lexpr %prec uminus
{ prefix_pp PPneg $2 }
| lqualid
| qualid
{ mk_pp (PPvar $1) }
| lqualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR
| qualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR
{ mk_pp (PPapp ($1, $3)) }
/***
| qualid_ident LEFTSQ lexpr RIGHTSQ
......
......@@ -43,7 +43,21 @@ end
theory Eq
logic eq : 'a, 'a -> prop
logic eq : 'a, 'a -> prop
(* This part is just a definition of the equality *)
(* This theory define eq but of course these axioms should not be send
to provers *)
axiom refl : forall x:'a. eq(x,x)
axiom sym : forall x,y:'a. eq(x,y) -> eq(y,x)
axiom trans : forall x,y,z:'a. eq(x,y) -> eq(y,z) -> eq(x,z)
(* This one can't be written in first order logic. *)
type t
type u
logic f : t -> u
axiom congru : forall x,y:t. eq(x,y) -> eq(f(x),f(y))
end
......@@ -53,7 +67,7 @@ theory Set
type t
logic in_ : elt, t -> prop
logic in_ : elt , t -> prop
logic empty : t
......@@ -68,6 +82,25 @@ theory Set
end
theory Set_poly
type 'a t
logic in_ : 'a , 'a t -> prop
logic empty : 'a t
axiom empty_def1 : forall x:'a. not in_(x, empty)
logic add : 'a, 'a t -> 'a t
uses Eq
axiom add_def1 : forall x,y:'a. forall s:'a t.
in_(x, add(y, s)) <-> (Eq.eq(x, y) or in_(x, s))
end
theory Test
uses Eq, L : List
......@@ -76,3 +109,45 @@ theory Test
end
theory Array
type ('a,'b) t
logic select : ('a,'b) t,'a -> 'b
logic store : ('a,'b) t,'a,'b -> ('a,'b) t
uses Eq
axiom select_eq : forall m : ('a,'b) t. forall a1,a2 : 'a. forall b : 'b.
Eq.eq(a1,a2) -> Eq.eq(select(store(m,a1,b),a2),b)
axiom select_eq : forall m : ('a,'b) t. forall a1,a2 : 'a. forall b : 'b.
not Eq.eq(a1,a2) -> Eq.eq(select(store(m,a1,b),a2),select(m,a2))
logic const : 'b -> ('a,'b) t
axiom const : forall b:'b. forall a:'a. Eq.eq(select(const(b),a),b)
end
theory Bool
type t = | True | False
end
theory Set_array
uses Array, Bool
(*type 'a t = ('a,bool_.t) Array.t*)
uses Eq
logic empty : ('a,Bool.t) Array.t
axiom empty : Eq.eq(empty,Array.const(Bool.False))
logic in_ : 'a, ('a,Bool.t) Array.t -> prop
axiom in_ : forall s:'a t. forall e:'a.
in_(e,s) <-> Eq.eq(select(x,y),Bool.True)
logic add : 'a, ('a,Bool.t) Array.t -> ('a,Bool.t) Array.t (* add(x,s) = store(x,s,bool.True) *)
axiom add : forall x:'a. forall s: ('a,Bool.t) Array.t. Eq.eq(add(x,s),store(s,x,Bool.True))
end
\ No newline at end of file
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