diff --git a/lib/prelude/prelude.why b/lib/prelude/prelude.why index c7b68a926a04e9b6d3872caf6c9c3bfdc4f7448a..ef76684b088eedb877294407c76b51af4ea5385a 100644 --- a/lib/prelude/prelude.why +++ b/lib/prelude/prelude.why @@ -13,8 +13,48 @@ theory Int logic ( * ) (int, int) : int logic ( / ) (int, int) : int logic ( % ) (int, int) : int + + 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) - axiom TestArith : forall x,y,z:int. x < y -> x+z < y+z + 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 diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 104a78fa4e2fb30a6eed318bc85e2d92f88bb95c..3b7ecaaa03ef1a6115799eea932d336e04ce6527 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -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 diff --git a/src/test.why b/src/test.why index f1d4545c6eb934821628908fd6d258872581a8b2..c0d1ed1d4237ca2685b6d95751dae59dc68d5f99 100644 --- a/src/test.why +++ b/src/test.why @@ -2,9 +2,8 @@ (* test file *) theory TestPrelude + use prelude.Int use prelude.List - (* use list.IntList *) - use array.IntArray end theory A