Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

un peu de theories Int et Real

parent 1687b9d1
......@@ -14,7 +14,47 @@ theory Int
logic ( / ) (int, int) : int
logic ( % ) (int, int) : int
axiom TestArith : forall x,y,z:int. x < y -> x+z < y+z
logic neg(int) : int
(* ring structure *)
axiom Add_assoc: forall x,y,z:int. x+(y+z) = (x+y)+z
axiom Add_comm: forall x,y:int. x+y = y+x
axiom Zero_neutral: forall x:int. x+0 = x
axiom Neg: forall x:int. x+neg(x) = 0
axiom Mul_assoc: forall x,y,z:int. x*(y*z) = (x*y)*z
axiom Mul_distr: forall x,y,z:int. x*(y+z) = x*y + x*z
(* int is a unitary, communtative ring *)
axiom Mul_comm: forall x,y:int. x*y = y*x
axiom Unitary: forall x:int. 1*x = x
end
theory Real
logic (<) (real, real)
logic (<=)(real, real)
logic (>) (real, real)
logic (>=)(real, real)
logic ( + ) (real, real) : real
logic ( - ) (real, real) : real
logic ( * ) (real, real) : real
logic ( / ) (real, real) : real
logic neg(real) : real
logic inv(real) : real
(* field structure *)
axiom Add_assoc: forall x,y,z:real. x+(y+z) = (x+y)+z
axiom Add_comm: forall x,y:real. x+y = y+x
axiom Mul_comm: forall x,y:real. x*y = y*x
axiom Zero_neutral: forall x:real. x+0. = x
axiom Neg: forall x:real. x+neg(x) = 0.
axiom Mul_assoc: forall x,y,z:real. x*(y*z) = (x*y)*z
axiom Mul_distr: forall x,y,z:real. x*(y+z) = x*y + x*z
axiom Unitary: forall x:real. 1.*x = x
axiom Inv: forall x:real. x*inv(x) = 1.
end
......
......@@ -374,8 +374,15 @@ and dterm_node loc env = function
Tconst c, Tyapp (Theory.t_int, [])
| PPconst (ConstReal _ as c) ->
Tconst c, Tyapp (Theory.t_real, [])
| _ ->
assert false (*TODO*)
| PPmatch _ ->
assert false (* TODO *)
| PPlet _ ->
assert false (* TODO *)
| PPnamed _ ->
assert false (* TODO *)
| PPexists _ | PPforall _ | PPif _
| PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
error ~loc TermExpected
and dfmla env e = match e.pp_desc with
| PPtrue ->
......@@ -386,10 +393,6 @@ and dfmla env e = match e.pp_desc with
Fnot (dfmla env a)
| PPinfix (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
Fbinop (binop op, dfmla env a, dfmla env b)
(* | PPinfix (a, (PPeq | PPneq as op), b) -> *)
(* let s, _ = specialize_psymbol Theory.eq in *)
(* let f = Fapp (s, [dterm env a; dterm env b]) in *)
(* if op = PPeq then f else Fnot f *)
| PPif (a, b, c) ->
Fif (dfmla env a, dfmla env b, dfmla env c)
| PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *)
......@@ -405,8 +408,16 @@ and dfmla env e = match e.pp_desc with
let s, tyl = specialize_psymbol s in
let tl = dtype_args s.ps_name e.pp_loc env tyl tl in
Fapp (s, tl)
| _ ->
assert false (*TODO*)
| PPmatch _ ->
assert false (* TODO *)
| PPlet _ ->
assert false (* TODO *)
| PPnamed _ ->
assert false (* TODO *)
| PPvar _ ->
assert false (* TODO *)
| PPconst _ | PPprefix (PPneg, _) ->
error ~loc:e.pp_loc PredicateExpected
and dtype_args s loc env el tl =
let n = List.length el and m = List.length tl in
......@@ -609,7 +620,7 @@ let add_logics loc dl th =
Some (vl, fmla env f)
in
Lpredicate (ps, def)
| Some t -> (* function *)
| Some _ -> (* function *)
let fs = Hashtbl.find fsymbols id in
let def = match d.ld_def with
| None ->
......@@ -625,6 +636,7 @@ let add_logics loc dl th =
let dl = List.map type_decl dl in
add_decl th (create_logic dl)
let term env t =
let denv = create_denv env in
let t = dterm denv t in
......
......@@ -2,9 +2,8 @@
(* test file *)
theory TestPrelude
use prelude.Int
use prelude.List
(* use list.IntList *)
use array.IntArray
end
theory A
......
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