From d4b0f689e40e8aff43cc5dd1c721f29ae1e783c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois@bobot.eu>
Date: Thu, 31 Jan 2013 20:30:20 +0100
Subject: [PATCH] [EGraph] equal_solve find the class because it can change du
to a subst [Test] add some of altergo tests
---
Makefile | 4 +-
src/arith.ml | 16 +-
src/arith.mli | 2 +
src/egraph_simple.ml | 10 +-
src/inputlang/altergo/popop_of_altergo.ml | 147 ++
src/inputlang/altergo/popop_of_altergo.mli | 34 +
src/inputlang/altergo/symbols.ml | 141 ++
src/inputlang/altergo/symbols.mli | 64 +
src/inputlang/altergo/ty.ml | 370 ++++
src/inputlang/altergo/ty.mli | 87 +
src/inputlang/altergo/why_lexer.mll | 308 +++
src/inputlang/altergo/why_parser.mly | 555 ++++++
src/inputlang/altergo/why_ptree.mli | 193 ++
src/inputlang/altergo/why_typing.ml | 1390 ++++++++++++++
src/inputlang/altergo/why_typing.mli | 36 +
src/uninterp.mli | 1 +
src/util/exn_printer.ml | 26 +-
src/util/extmap.ml | 2 -
src/util/loc.ml | 5 +
src/util/strings.ml | 9 +-
src/util/strings.mli | 3 +
tests/tests.ml | 31 +-
tests/tests_altergo_arith.split | 1960 ++++++++++++++++++++
tests/tests_altergo_qualif.split | 1234 ++++++++++++
tests/tests_arith.ml | 7 +-
tests/tests_lib.ml | 23 +
tests/tests_uf.ml | 5 +
27 files changed, 6636 insertions(+), 27 deletions(-)
create mode 100644 src/inputlang/altergo/popop_of_altergo.ml
create mode 100644 src/inputlang/altergo/popop_of_altergo.mli
create mode 100644 src/inputlang/altergo/symbols.ml
create mode 100644 src/inputlang/altergo/symbols.mli
create mode 100644 src/inputlang/altergo/ty.ml
create mode 100644 src/inputlang/altergo/ty.mli
create mode 100644 src/inputlang/altergo/why_lexer.mll
create mode 100644 src/inputlang/altergo/why_parser.mly
create mode 100644 src/inputlang/altergo/why_ptree.mli
create mode 100644 src/inputlang/altergo/why_typing.ml
create mode 100644 src/inputlang/altergo/why_typing.mli
create mode 100644 tests/tests_altergo_arith.split
create mode 100644 tests/tests_altergo_qualif.split
create mode 100644 tests/tests_lib.ml
diff --git a/Makefile b/Makefile
index c884931a6..b894f2b51 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,8 @@
PACKAGES=-package oUnit -package zarith
-OPTIONS=-tag annot -tag debug
-DIRECTORIES=-I src -I src/util
+OPTIONS=-tag annot -tag debug -no-sanitize
+DIRECTORIES=-I src -I src/util -I src/inputlang/altergo
.PHONY: tests tests.native tests_debug
diff --git a/src/arith.ml b/src/arith.ml
index 53b4bb315..cb7c436e8 100644
--- a/src/arith.ml
+++ b/src/arith.ml
@@ -124,9 +124,7 @@ module Th = struct
let solve d (p1,cl1) cl2 =
- match X.extract (E.Delayed.repr d cl2) with
- | None -> Cl.M.empty, cl1
- | Some p2 ->
+ let p2 = embed d cl2 in
let p = sub p1 p2 in
if Cl.M.is_empty p.poly
then if Q.equal Q.zero p.cst
@@ -184,5 +182,17 @@ let add t cl1 cl2 =
let sub t cl1 cl2 =
basecl t (sub (embed t cl1) (embed t cl2))
+let uninterp_mul env = Uninterp.fun2 env " *"
+
+let mult t cl1 cl2 =
+ let m1 = embed t cl1 in
+ let m2 = embed t cl2 in
+ if Cl.M.is_empty m1.poly || Cl.M.is_empty m2.poly then
+ let cst,m = if Cl.M.is_empty m1.poly then m1.cst, m2 else m2.cst, m1 in
+ basecl t (mult_cst cst m)
+ else
+ let f,t = uninterp_mul t in
+ f t cl1 cl2
+
let mult_cst t cst cl =
basecl t (mult_cst cst (embed t cl))
diff --git a/src/arith.mli b/src/arith.mli
index de9177a5c..64d906d96 100644
--- a/src/arith.mli
+++ b/src/arith.mli
@@ -33,3 +33,5 @@ val sub : env -> cl -> cl -> cl * env
val mult_cst : env -> Q.t -> cl -> cl * env
+
+val mult : env -> cl -> cl -> cl * env
diff --git a/src/egraph_simple.ml b/src/egraph_simple.ml
index 121990dcb..829719773 100644
--- a/src/egraph_simple.ml
+++ b/src/egraph_simple.ml
@@ -273,6 +273,11 @@ let rec equal_solve env t1 t2 =
Debug.dprintf debug
"[EGraph] Equal_solve @[@[%a@] =>@ @[%a@]@]@."
(print_cl env) t1 (print_cl env) t2;
+ (** I don't really like to take the find now...*)
+ let t1 = UnionFind.find env t1 in
+ let t2 = UnionFind.find env t2 in
+ if Cl.equal t1 t2 then env
+ else
let queue = Queue.create () in
let d = ref env in
let s, cl = MTerm.solve d (repr env t1,t1) (repr env t2,t2) in
@@ -293,10 +298,7 @@ let equal env cl1 cl2 =
Debug.dprintf debug
"[EGraph] Equal @[@[%a@] ==@ @[%a@]@]@."
(print_cl env) cl1 (print_cl env) cl2;
- let cl1 = UnionFind.find env cl1 in
- let cl2 = UnionFind.find env cl2 in
- if Cl.equal cl1 cl2 then env
- else equal_solve env cl1 cl2
+ equal_solve env cl1 cl2
let () = Exn_printer.register (fun fmt exn ->
match exn with
diff --git a/src/inputlang/altergo/popop_of_altergo.ml b/src/inputlang/altergo/popop_of_altergo.ml
new file mode 100644
index 000000000..f3716921c
--- /dev/null
+++ b/src/inputlang/altergo/popop_of_altergo.ml
@@ -0,0 +1,147 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2013 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Why_ptree
+
+exception Not_supported of Loc.position
+
+
+let rec add_lexpr_term env t =
+ match t.pp_desc with
+ | PPvar s -> Uninterp.cst env s
+ | PPapp (s,l) ->
+ let f,env = Uninterp.cst env s in
+ let env,l = Lists.map_fold_left
+ (fun env e -> let e,env = add_lexpr_term env e in env,e) env l in
+ Uninterp.appl env f l
+ | PPconst (ConstInt s) ->
+ Arith.cst env (Q.of_string s)
+ | PPconst (ConstReal q) ->
+ Arith.cst env q
+ | PPinfix (t1,op,t2) ->
+ let cl1,env = add_lexpr_term env t1 in
+ let cl2,env = add_lexpr_term env t2 in
+ let op = match op with
+ | PPadd -> Arith.add
+ | PPsub -> Arith.sub
+ | PPmul -> Arith.mult
+ | _ -> raise (Not_supported (Loc.extract t.pp_loc)) in
+ op env cl1 cl2
+ | PPprefix (PPneg,e) ->
+ let cl1, env = add_lexpr_term env e in
+ Arith.mult_cst env (Q.of_int (-1)) cl1
+ | _ -> raise (Not_supported (Loc.extract t.pp_loc))
+
+let uninterp_true env = Uninterp.cst env " true"
+
+let rec add_lexpr_axiom _true env t =
+ match t.pp_desc with
+ | PPapp (s,l) ->
+ let f,env = Uninterp.cst env s in
+ let env,l = Lists.map_fold_left
+ (fun env e -> let e,env = add_lexpr_term env e in env,e) env l in
+ let cl,env = Uninterp.appl env f l in
+ let cl,env = Egraph_simple.add env cl in
+ let env = Egraph_simple.equal env cl _true in
+ env
+ | PPinfix (t1,PPand,t2) ->
+ let env = add_lexpr_axiom _true env t1 in
+ let env = add_lexpr_axiom _true env t2 in
+ env
+ | PPinfix (t1,PPeq,t2) ->
+ let cl1,env = add_lexpr_term env t1 in
+ let cl1,env = Egraph_simple.add env cl1 in
+ let cl2,env = add_lexpr_term env t2 in
+ let cl2,env = Egraph_simple.add env cl2 in
+ let env = Egraph_simple.equal env cl1 cl2 in
+ env
+ | _ -> raise (Not_supported (Loc.extract t.pp_loc))
+
+
+let rec add_lexpr_goal _true env t =
+ match t.pp_desc with
+ | PPapp (s,l) ->
+ let f,env = Uninterp.cst env s in
+ let env,l = Lists.map_fold_left
+ (fun env e -> let e,env = add_lexpr_term env e in env,e) env l in
+ let cl,env = Uninterp.appl env f l in
+ let cl,env = Egraph_simple.add env cl in
+ Egraph_simple.is_equal env cl _true
+ | PPinfix (t1,PPand,t2) ->
+ let b1 = add_lexpr_goal _true env t1 in
+ let b2 = add_lexpr_goal _true env t2 in
+ b1 && b2
+ | PPinfix (t1,PPimplies,t2) ->
+ let env = add_lexpr_axiom _true env t1 in
+ let b2 = add_lexpr_goal _true env t2 in
+ b2
+ | PPinfix (t1,PPeq,t2) ->
+ let cl1,env = add_lexpr_term env t1 in
+ let cl1,env = Egraph_simple.add env cl1 in
+ let cl2,env = add_lexpr_term env t2 in
+ let cl2,env = Egraph_simple.add env cl2 in
+ Egraph_simple.is_equal env cl1 cl2
+ | PPforall (_,_,_,e) | PPforall_named (_,_,_,e) -> add_lexpr_goal _true env e
+ | _ -> raise (Not_supported (Loc.extract t.pp_loc))
+
+
+
+let rec add_decl _true env = function
+ | [] -> raise (Not_supported Loc.dummy_position)
+ | Axiom(_,_,_,e)::l -> add_decl _true (add_lexpr_axiom _true env e) l
+ | Goal(_,_,e)::_ -> add_lexpr_goal _true env e
+ | _::l -> add_decl _true env l
+
+let check_goal l =
+ let _true,env = uninterp_true Egraph_simple.MTerm.UnionFind.empty in
+ add_decl _true env l
+
+let loc lb = Loc.extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)
+
+let with_location f lb =
+ if Debug.test_flag Debug.stack_trace then f lb else
+ try f lb with
+ | Loc.Located _ as e -> raise e
+ | e -> raise (Loc.Located (loc lb, e))
+
+let read_file s =
+ let cin = open_in s in
+ let lb = Lexing.from_channel cin in
+ Loc.set_file s lb;
+ let _, decls = with_location (Why_parser.file Why_lexer.token) lb in
+ decls
+
+let read_split s =
+ let cin = open_in s in
+ let lb = Lexing.from_channel cin in
+ Loc.set_file s lb;
+ with_location (Why_parser.split_file Why_lexer.token) lb
+
+
+
+let () = Exn_printer.register (fun fmt exn ->
+ match exn with
+ | Not_supported pos ->
+ Format.fprintf fmt
+ "%a@ popop can't convert alt-ergo construct"
+ Loc.report_position pos
+ | _ -> raise exn)
diff --git a/src/inputlang/altergo/popop_of_altergo.mli b/src/inputlang/altergo/popop_of_altergo.mli
new file mode 100644
index 000000000..9212bf903
--- /dev/null
+++ b/src/inputlang/altergo/popop_of_altergo.mli
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2013 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Why_ptree
+
+exception Not_supported of Loc.position
+
+val read_file: string -> Why_ptree.file
+val read_split: string -> (string * Loc.position * Why_ptree.file) list
+
+
+val check_goal: Why_ptree.file -> bool
+(** true: goal verified
+ false: goal not verified
+*)
diff --git a/src/inputlang/altergo/symbols.ml b/src/inputlang/altergo/symbols.ml
new file mode 100644
index 000000000..4ddd1418a
--- /dev/null
+++ b/src/inputlang/altergo/symbols.ml
@@ -0,0 +1,141 @@
+(**************************************************************************)
+(* *)
+(* The Alt-Ergo theorem prover *)
+(* Copyright (C) 2006-2011 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* *)
+(* Francois Bobot *)
+(* Mohamed Iguernelala *)
+(* Stephane Lescuyer *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+open Hashcons
+
+type operator =
+ | Plus | Minus | Mult | Div | Modulo | Concat | Extract
+ | Get | Set | Access of Strings.Hashcons.t | Record
+
+type name_kind = Ac | Constructor | Other
+
+type t =
+ | True
+ | False
+ | Void
+ | Name of Strings.Hashcons.t * name_kind
+ | Int of Strings.Hashcons.t
+ | Real of Strings.Hashcons.t
+ | Bitv of string
+ | Op of operator
+ | Var of Strings.Hashcons.t
+type s = t
+
+let name ?(kind=Other) s = Name (Strings.Hashcons.make s, kind)
+let var s = Var (Strings.Hashcons.make s)
+let int i = Int (Strings.Hashcons.make i)
+let real r = Real (Strings.Hashcons.make r)
+
+let is_ac = function
+ | Name(_, Ac) -> true
+ | _ -> false
+
+let underscoring = function
+ Var s -> Var (Strings.Hashcons.make ("$"^Strings.Hashcons.view s))
+ | _ -> assert false
+
+let compare_kind k1 k2 = match k1, k2 with
+ | Ac , Ac -> 0
+ | Ac , _ -> 1
+ | _ , Ac -> -1
+ | Other, Other -> 0
+ | Other, _ -> 1
+ | _ , Other -> -1
+ | Constructor, Constructor -> 0
+
+let compare s1 s2 = match s1, s2 with
+ | Name (n1,k1), Name (n2,k2) ->
+ let c = compare_kind k1 k2 in
+ if c = 0 then Strings.Hashcons.compare n1 n2 else c
+ | Name _, _ -> -1
+ | _, Name _ -> 1
+ | Var n1, Var n2 -> Strings.Hashcons.compare n1 n2
+ | Var _, _ -> -1
+ | _ ,Var _ -> 1
+ | Int i1, Int i2 -> Strings.Hashcons.compare i1 i2
+ | Int _, _ -> -1
+ | _ ,Int _ -> 1
+ | Op(Access s1), Op(Access s2) -> Strings.Hashcons.compare s1 s2
+ | Op(Access _), _ -> -1
+ | _, Op(Access _) -> 1
+ | _ -> Pervasives.compare s1 s2
+
+let equal s1 s2 = compare s1 s2 = 0
+
+let hash = function
+ | Name (n,Ac) -> Strings.Hashcons.hash n * 19 + 1
+ | Name (n,_) -> Strings.Hashcons.hash n * 19
+ | Var n (*| Int n*) -> Strings.Hashcons.hash n * 19 + 1
+ | Op (Access s) -> Strings.Hashcons.hash s + 19
+ | s -> Hashtbl.hash s
+
+let to_string = function
+ | Name (n,_) -> Strings.Hashcons.view n
+ | Var x -> (Strings.Hashcons.view x)
+ | Int n -> Strings.Hashcons.view n
+ | Real n -> Strings.Hashcons.view n
+ | Bitv s -> "[|"^s^"|]"
+ | Op Plus -> "+"
+ | Op Minus -> "-"
+ | Op Mult -> "*"
+ | Op Div -> "/"
+ | Op Modulo -> "%"
+ | Op (Access s) -> "@Access_"^(Strings.Hashcons.view s)
+ | Op Record -> "@Record"
+ | Op Get -> "get"
+ | Op Set -> "set"
+ | True -> "true"
+ | False -> "false"
+ | Void -> "void"
+ | _ -> "" (*assert false*)
+
+let print fmt s = Format.fprintf fmt "%s" (to_string s)
+
+let dummy = Name (Strings.Hashcons.make "_one", Other)
+
+let fresh =
+ let cpt = ref 0 in
+ fun s ->
+ incr cpt;
+ (* garder le suffixe "__" car cela influence l'ordre *)
+ name (Format.sprintf "!?__%s%i" s (!cpt))
+
+let is_get f = equal f (Op Get)
+let is_set f = equal f (Op Set)
+
+module Map =
+ Map.Make(struct type t' = t type t=t' let compare=compare end)
+
+module Set =
+ Set.Make(struct type t' = t type t=t' let compare=compare end)
+
+
+
+module Labels = Hashtbl.Make(struct
+ type t = s
+ let equal = equal
+ let hash = hash
+end)
+
+let labels = Labels.create 100007
+
+let add_label lbl t = Labels.replace labels t lbl
+
+let label t = try Labels.find labels t with Not_found ->
+ Strings.Hashcons.make ""
diff --git a/src/inputlang/altergo/symbols.mli b/src/inputlang/altergo/symbols.mli
new file mode 100644
index 000000000..eca619020
--- /dev/null
+++ b/src/inputlang/altergo/symbols.mli
@@ -0,0 +1,64 @@
+(**************************************************************************)
+(* *)
+(* The Alt-Ergo theorem prover *)
+(* Copyright (C) 2006-2011 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* *)
+(* Francois Bobot *)
+(* Mohamed Iguernelala *)
+(* Stephane Lescuyer *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+type operator =
+ | Plus | Minus | Mult | Div | Modulo | Concat | Extract
+ | Get | Set | Access of Strings.Hashcons.t | Record
+
+type name_kind = Ac | Constructor | Other
+
+type t =
+ | True
+ | False
+ | Void
+ | Name of Strings.Hashcons.t * name_kind
+ | Int of Strings.Hashcons.t
+ | Real of Strings.Hashcons.t
+ | Bitv of string
+ | Op of operator
+ | Var of Strings.Hashcons.t
+
+val name : ?kind:name_kind -> string -> t
+val var : string -> t
+val underscoring : t -> t
+val int : string -> t
+val real : string -> t
+
+val is_ac : t -> bool
+
+val equal : t -> t -> bool
+val compare : t -> t -> int
+val hash : t -> int
+
+val to_string : t -> string
+val print : Format.formatter -> t -> unit
+
+val dummy : t
+
+val fresh : string -> t
+
+val is_get : t -> bool
+val is_set : t -> bool
+
+
+module Map : Map.S with type key = t
+module Set : Set.S with type elt = t
+
+val add_label : Strings.Hashcons.t -> t -> unit
+val label : t -> Strings.Hashcons.t
diff --git a/src/inputlang/altergo/ty.ml b/src/inputlang/altergo/ty.ml
new file mode 100644
index 000000000..5f0819880
--- /dev/null
+++ b/src/inputlang/altergo/ty.ml
@@ -0,0 +1,370 @@
+(**************************************************************************)
+(* *)
+(* The Alt-Ergo theorem prover *)
+(* Copyright (C) 2006-2011 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* *)
+(* Francois Bobot *)
+(* Mohamed Iguernelala *)
+(* Stephane Lescuyer *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+open Hashcons
+open Format
+
+type t =
+ | Tint
+ | Treal
+ | Tbool
+ | Tunit
+ | Tvar of tvar
+ | Tbitv of int
+ | Text of t list * Strings.Hashcons.t
+ | Tfarray of t * t
+ | Tnext of t
+ | Tsum of Strings.Hashcons.t * Strings.Hashcons.t list
+ | Trecord of trecord
+
+and tvar = { v : int ; mutable value : t option }
+and trecord = {
+ mutable args : t list;
+ name : Strings.Hashcons.t;
+ mutable lbs : (Strings.Hashcons.t * t) list
+}
+
+exception TypeClash of t*t
+exception Shorten of t
+
+
+
+(*** pretty print ***)
+let print full fmt ty =
+ let h = Hashtbl.create 17 in
+ let rec print fmt = function
+ | Tint -> fprintf fmt "int"
+ | Treal -> fprintf fmt "real"
+ | Tbool -> fprintf fmt "bool"
+ | Tunit -> fprintf fmt "unit"
+ | Tbitv n -> fprintf fmt "bitv[%d]" n
+ | Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v
+ | Tvar{v=v ; value = Some (Trecord {args=l; name=n} as t) } ->
+ if Hashtbl.mem h v then
+ fprintf fmt "%a%s" printl l (Strings.Hashcons.view n)
+ else
+ (Hashtbl.add h v ();
+ (*fprintf fmt "('a_%d->%a)" v print t *)
+ print fmt t)
+ | Tvar{v=v ; value = Some t} ->
+ (*fprintf fmt "('a_%d->%a)" v print t *)
+ print fmt t
+ | Text(l, s) -> fprintf fmt "%a%s" printl l (Strings.Hashcons.view s)
+ | Tfarray (t1, t2) -> fprintf fmt "(%a,%a) farray" print t1 print t2
+ | Tnext t -> fprintf fmt "%a next" print t
+ | Tsum(s, _) -> fprintf fmt "%s" (Strings.Hashcons.view s)
+ | Trecord {args=lv; name=n; lbs=lbls} ->
+ fprintf fmt "%a%s" printl lv (Strings.Hashcons.view n);
+ if full then begin
+ fprintf fmt " = {";
+ let first = ref true in
+ List.iter
+ (fun (s, t) ->
+ fprintf fmt "%s%s : %a" (if !first then "" else "; ")
+ (Strings.Hashcons.view s) print t;
+ first := false
+ ) lbls;
+ fprintf fmt "}"
+ end
+
+ and printl fmt = function
+ [] -> ()
+ | [t] -> fprintf fmt "%a " print t
+ | t::l -> fprintf fmt "%a,%a" print t printl l
+ in
+ print fmt ty
+
+let print_full = print true
+let print = print false
+
+
+(* smart constructors *)
+
+let tunit = Text ([],Strings.Hashcons.make "unit")
+
+let text l s = Text (l,Strings.Hashcons.make s)
+
+let tsum s lc = Tsum (Strings.Hashcons.make s, List.map Strings.Hashcons.make lc)
+
+let trecord lv n lbs =
+ let lbs = List.map (fun (l,ty) -> Strings.Hashcons.make l, ty) lbs in
+ let lbs = List.sort (fun (l1, _) (l2, _) -> Strings.Hashcons.compare l1 l2) lbs in
+ Trecord { args = lv; name = Strings.Hashcons.make n; lbs = lbs}
+
+let rec shorten t =
+ match t with
+ | Tvar {value=None} -> t
+ | Tvar {value=Some(Tvar{value=None} as t')} -> t'
+ | Tvar ({value=Some(Tvar t2)} as t1) -> t1.value <- t2.value; shorten t
+ | Tvar {v = n; value = Some t'} -> shorten t'
+ | Text (l,s) -> Text(List.map shorten l,s)
+ | Tfarray (t1,t2) -> Tfarray(shorten t1,shorten t2)
+ | Trecord r ->
+ r.args <- List.map shorten r.args;
+ r.lbs <- List.map (fun (lb, ty) -> lb, shorten ty) r.lbs;
+ t
+ | _ -> t
+
+let fresh_var =
+ let cpt = ref (-1) in
+ fun () -> incr cpt; {v= !cpt ; value = None }
+
+let fresh_empty_text =
+ let cpt = ref (-1) in
+ fun () -> incr cpt; text [] ("'_c"^(string_of_int !cpt))
+
+let rec hash t =
+ match t with
+ | Tvar{v=v} -> v
+ | Text(l,s) ->
+ abs (List.fold_left (fun acc x-> acc*19 + hash x) (Strings.Hashcons.hash s) l)
+ | Tfarray (t1,t2) -> 19 * (hash t1) + 23 * (hash t2)
+ | Trecord { args = args; name = s; lbs = lbs} ->
+ let h =
+ List.fold_left (fun h ty -> 27 * h + hash ty) (Strings.Hashcons.hash s) args
+ in
+ let h =
+ List.fold_left
+ (fun h (lb, ty) -> 23 * h + 19 * (Strings.Hashcons.hash lb) + hash ty)
+ (abs h) lbs
+ in
+ abs h
+ | Tsum (s, l) ->
+ let h =
+ List.fold_left
+ (fun h x -> 13 * h + Strings.Hashcons.hash x) (Strings.Hashcons.hash s) l
+ in
+ abs h
+ | _ -> Hashtbl.hash t
+
+let rec equal t1 t2 =
+ match shorten t1 , shorten t2 with
+ | Tvar{v=v1}, Tvar{v=v2} -> v1 = v2
+ | Text(l1, s1), Text(l2, s2) ->
+ (try Strings.Hashcons.equal s1 s2 && List.for_all2 equal l1 l2
+ with Invalid_argument _ -> false)
+ | Tfarray (ta1, ta2), Tfarray (tb1, tb2) ->
+ equal ta1 tb1 && equal ta2 tb2
+ | Tsum (s1, _), Tsum (s2, _) -> Strings.Hashcons.equal s1 s2
+ | Trecord {args=a1;name=s1;lbs=l1}, Trecord {args=a2;name=s2;lbs=l2} ->
+ begin
+ try
+ Strings.Hashcons.equal s1 s2 && List.for_all2 equal a1 a2 &&
+ List.for_all2
+ (fun (l1, ty1) (l2, ty2) ->
+ Strings.Hashcons.equal l1 l2 && equal ty1 ty2) l1 l2
+ with Invalid_argument _ -> false
+ end
+ | Tint, Tint | Treal, Treal | Tbool, Tbool | Tunit, Tunit -> true
+ | Tbitv n1, Tbitv n2 -> n1 =n2
+ | Tnext t1, Tnext t2 -> equal t1 t2
+ | _ -> false
+
+let rec compare t1 t2 =
+ match shorten t1 , shorten t2 with
+ | Tvar{v=v1} , Tvar{v=v2} -> Pervasives.compare v1 v2
+ | Tvar _, _ -> -1 | _ , Tvar _ -> 1
+ | Text(l1, s1) , Text(l2, s2) ->
+ let c = Strings.Hashcons.compare s1 s2 in
+ if c<>0 then c
+ else compare_list l1 l2
+ | Text _, _ -> -1 | _ , Text _ -> 1
+ | Tfarray (ta1,ta2), Tfarray (tb1,tb2) ->
+ let c = compare ta1 tb1 in
+ if c<>0 then c
+ else compare ta2 tb2
+ | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1
+ | Tsum(s1, _), Tsum(s2, _) ->
+ Strings.Hashcons.compare s1 s2
+ | Tsum _, _ -> -1 | _ , Tsum _ -> 1
+ | Trecord {args=a1;name=s1;lbs=l1},Trecord {args=a2;name=s2;lbs=l2} ->
+ let c = Strings.Hashcons.compare s1 s2 in
+ if c <> 0 then c else
+ let c = compare_list a1 a2 in
+ if c <> 0 then c else
+ let l1, l2 = List.map snd l1, List.map snd l2 in
+ compare_list l1 l2
+ | Trecord _, _ -> -1 | _ , Trecord _ -> 1
+ | t1 , t2 -> Pervasives.compare t1 t2
+and compare_list l1 l2 = match l1, l2 with
+ | [] , [] -> 0
+ | [] , _ -> -1
+ | _ , [] -> 1
+ | x::ll1 , y::ll2 ->
+ let c = compare x y in
+ if c<>0 then c else compare_list ll1 ll2
+
+let occurs {v=n} t =
+ let rec occursrec = function
+ Tvar {v=m} -> n=m
+ | Text(l,_) -> List.exists occursrec l
+ | Tfarray (t1,t2) -> occursrec t1 || occursrec t2
+ | _ -> false
+ in occursrec t
+
+(*** destructive unification ***)
+let rec unify t1 t2 =
+ let t1 = shorten t1 in
+ let t2 = shorten t2 in
+ match t1 , t2 with
+ Tvar ({v=n;value=None} as tv1), Tvar {v=m;value=None} ->
+ if n<>m then tv1.value <- Some t2
+ | _ , Tvar ({value=None} as tv) ->
+ if (occurs tv t1) then raise (TypeClash(t1,t2));
+ tv.value <- Some t1
+ | Tvar ({value=None} as tv) , _ ->
+ if (occurs tv t2) then raise (TypeClash(t1,t2));
+ tv.value <- Some t2
+ | Text(l1,s1) , Text(l2,s2) when Strings.Hashcons.equal s1 s2 ->
+ List.iter2 unify l1 l2
+ | Tfarray (ta1,ta2), Tfarray (tb1,tb2) -> unify ta1 tb1;unify ta2 tb2
+ | Trecord r1, Trecord r2 when Strings.Hashcons.equal r1.name r2.name ->
+ List.iter2 unify r1.args r2.args
+ | Tsum(s1, _) , Tsum(s2, _) when Strings.Hashcons.equal s1 s2 -> ()
+ | Tint, Tint | Tbool, Tbool | Treal, Treal | Tunit, Tunit -> ()
+ | Tbitv n , Tbitv m when m=n -> ()
+ | _ , _ ->
+ raise (TypeClash(t1,t2))
+
+
+(*** matching with a substitution mechanism ***)
+module M = Map.Make(struct type t=int let compare = Pervasives.compare end)
+type subst = t M.t
+
+let esubst = M.empty
+
+let rec matching s pat t =
+ match pat , t with
+ | Tvar {v=n;value=None} , _ ->
+ (try if not (equal (M.find n s) t) then raise (TypeClash(pat,t)); s
+ with Not_found -> M.add n t s)
+ | Tvar {value=_}, _ -> raise (Shorten pat)
+ | Text (l1,s1) , Text (l2,s2) when Strings.Hashcons.equal s1 s2 ->
+ List.fold_left2 matching s l1 l2
+ | Tfarray (ta1,ta2), Tfarray (tb1,tb2) ->
+ matching (matching s ta1 tb1) ta2 tb2
+ | Trecord r1, Trecord r2 when Strings.Hashcons.equal r1.name r2.name ->
+ let s = List.fold_left2 matching s r1.args r2.args in
+ List.fold_left2
+ (fun s (_, p) (_, ty) -> matching s p ty) s r1.lbs r2.lbs
+ | Tsum (s1, _), Tsum (s2, _) when Strings.Hashcons.equal s1 s2 -> s
+ | Tint , Tint | Tbool , Tbool | Treal , Treal | Tunit, Tunit -> s
+ | Tbitv n , Tbitv m when n=m -> s
+ | _ , _ ->
+ raise (TypeClash(pat,t))
+
+let rec apply_subst s ty =
+ match ty with
+ | Tvar {v=n} ->
+ (try M.find n s with Not_found -> ty)
+ | Text (l,e) -> Text(List.map (apply_subst s) l,e)
+ | Tfarray (t1,t2) -> Tfarray (apply_subst s t1,apply_subst s t2)
+ | Trecord r ->
+ let lbs = List.map (fun (x,t) -> x, apply_subst s t) r.lbs in
+ Trecord
+ {args = List.map (apply_subst s) r.args;
+ name = r.name;
+ lbs = lbs}
+ | t -> t
+
+let instantiate lvar lty ty =
+ let s =
+ List.fold_left2
+ (fun s x t ->
+ match x with
+ | Tvar {v=n} ->
+ M.add n t s
+ | _ -> assert false) M.empty lvar lty
+ in
+ apply_subst s ty
+
+let union_subst s1 s2 =
+ M.fold (fun k x s2 -> M.add k x s2) (M.map (apply_subst s2) s1) s2
+
+let compare_subst = M.compare Pervasives.compare
+
+let rec fresh ty subst =
+ match ty with
+ | Tvar {v=x} ->
+ begin
+ try M.find x subst, subst
+ with Not_found ->
+ let nv = Tvar (fresh_var()) in
+ nv, M.add x nv subst
+ end
+ | Text (args, n) ->
+ let args, subst = fresh_list args subst in
+ Text (args, n), subst
+ | Tfarray (ty1, ty2) ->
+ let ty1, subst = fresh ty1 subst in
+ let ty2, subst = fresh ty2 subst in
+ Tfarray (ty1, ty2), subst
+ | Trecord {args = args; name = n; lbs = lbs} ->
+ let args, subst = fresh_list args subst in
+ let lbs, subst =
+ List.fold_right
+ (fun (x,ty) (lbs, subst) ->
+ let ty, subst = fresh ty subst in
+ (x, ty)::lbs, subst) lbs ([], subst)
+ in
+ Trecord { args = args; name = n; lbs = lbs}, subst
+ | t -> t, subst
+and fresh_list lty subst =
+ List.fold_right
+ (fun ty (lty, subst) ->
+ let ty, subst = fresh ty subst in
+ ty::lty, subst) lty ([], subst)
+
+module Svty =
+ Set.Make(struct type t = int let compare = Pervasives.compare end)
+
+let vty_of t =
+ let rec vty_of_rec acc t =
+ let t = shorten t in
+ match t with
+ | Tvar { v = i ; value = None } -> Svty.add i acc
+ | Text(l,_) -> List.fold_left vty_of_rec acc l
+ | Tfarray (t1,t2) -> vty_of_rec (vty_of_rec acc t1) t2
+ | Trecord {args = args; name = s; lbs = lbs} ->
+ let acc = List.fold_left vty_of_rec acc args in
+ List.fold_left (fun acc (_, ty) -> vty_of_rec acc ty) acc lbs
+ | _ -> acc
+ in
+ vty_of_rec Svty.empty t
+
+let rec monomorphize ty =
+ match ty with
+ | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum _ -> ty
+ | Text (tyl,hs) -> Text (List.map monomorphize tyl, hs)
+ | Trecord {args = tylv; name = n; lbs = tylb} ->
+ let m_tylv = List.map monomorphize tylv in
+ let m_tylb =
+ List.map (fun (lb, ty_lb) -> lb, monomorphize ty_lb) tylb
+ in
+ Trecord {args = m_tylv; name = n; lbs = m_tylb}
+ | Tfarray (ty1,ty2) -> Tfarray (monomorphize ty1,monomorphize ty2)
+ | Tnext ty -> Tnext (monomorphize ty)
+ | Tvar {v=v; value=None} -> text [] ("'_c"^(string_of_int v))
+ | Tvar ({value=Some ty1} as r) ->
+ Tvar { r with value = Some (monomorphize ty1)}
+
+
+let print_subst fmt sbt =
+ M.iter (fun n ty -> fprintf fmt "%d -> %a" n print ty) sbt;
+ fprintf fmt "@?"
diff --git a/src/inputlang/altergo/ty.mli b/src/inputlang/altergo/ty.mli
new file mode 100644
index 000000000..fd9468d00
--- /dev/null
+++ b/src/inputlang/altergo/ty.mli
@@ -0,0 +1,87 @@
+(**************************************************************************)
+(* *)
+(* The Alt-Ergo theorem prover *)
+(* Copyright (C) 2006-2011 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* *)
+(* Francois Bobot *)
+(* Mohamed Iguernelala *)
+(* Stephane Lescuyer *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+type t =
+ | Tint
+ | Treal
+ | Tbool
+ | Tunit
+ | Tvar of tvar
+ | Tbitv of int
+ | Text of t list * Strings.Hashcons.t
+ | Tfarray of t * t
+ | Tnext of t
+ | Tsum of Strings.Hashcons.t * Strings.Hashcons.t list
+ | Trecord of trecord
+
+and tvar = { v : int ; mutable value : t option }
+and trecord = {
+ mutable args : t list;
+ name : Strings.Hashcons.t;
+ mutable lbs : (Strings.Hashcons.t * t) list
+}
+
+
+type subst
+
+val esubst : subst
+
+exception TypeClash of t*t
+
+val tunit : t
+
+val text : t list -> string -> t
+val tsum : string -> string list -> t
+val trecord : t list -> string -> (string * t) list -> t
+
+val shorten : t -> t
+
+val fresh_var : unit -> tvar
+val fresh_empty_text : unit -> t
+
+val fresh : t -> subst -> t * subst
+val fresh_list : t list -> subst -> t list * subst
+
+val equal : t -> t -> bool
+val hash : t -> int
+val compare : t -> t -> int
+
+val unify : t -> t -> unit
+val matching : subst -> t -> t -> subst
+
+val apply_subst : subst -> t -> t
+val instantiate : t list -> t list -> t -> t
+
+(* Applique la seconde substitution sur la premiere
+ puis fais l'union des map avec prioritée à la première *)
+val union_subst : subst -> subst -> subst
+
+val compare_subst : subst -> subst -> int
+
+val print : Format.formatter -> t -> unit
+val print_full : Format.formatter -> t -> unit
+(*val printl : Format.formatter -> t list -> unit*)
+
+module Svty : Set.S
+
+val vty_of : t -> Svty.t
+
+val monomorphize: t -> t
+
+val print_subst: Format.formatter -> subst -> unit
diff --git a/src/inputlang/altergo/why_lexer.mll b/src/inputlang/altergo/why_lexer.mll
new file mode 100644
index 000000000..7a08a2e55
--- /dev/null
+++ b/src/inputlang/altergo/why_lexer.mll
@@ -0,0 +1,308 @@
+(**************************************************************************)
+(* *)
+(* The Alt-Ergo theorem prover *)
+(* Copyright (C) 2006-2011 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* *)
+(* Francois Bobot *)
+(* Mohamed Iguernelala *)
+(* Stephane Lescuyer *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+(*
+ * The Why certification tool
+ * Copyright (C) 2002 Jean-Christophe FILLIATRE
+ *
+ * This software is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public
+ * License version 2, as published by the Free Software Foundation.
+ *
+ * This software is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+ *
+ * See the GNU General Public License version 2 for more details
+ * (enclosed in the file GPL).
+ *)
+
+(* $Id: why_lexer.mll,v 1.26 2011-02-24 15:35:48 mebsout Exp $ *)
+
+{
+ open Lexing
+ open Why_parser
+ open Format
+
+ let rules () = 1 (** replace open Option *)
+ let fmt = Debug.get_debug_formatter ()
+
+ let keywords = Hashtbl.create 97
+ let () =
+ List.iter
+ (fun (x,y) -> Hashtbl.add keywords x y)
+ [ "ac", AC;
+ "and", AND;
+ "axiom", AXIOM;
+ "inversion", INVERSION;
+ "bitv", BITV;
+ "bool", BOOL;
+ "check", CHECK;
+ "cut", CUT;
+ "distinct", DISTINCT;
+ "else", ELSE;
+ "exists", EXISTS;
+ "false", FALSE;
+ "forall", FORALL;
+ "function", FUNCTION;
+ "goal", GOAL;
+ "if", IF;
+ "in", IN;
+ "include", INCLUDE;
+ "int", INT;
+ "let", LET;
+ "logic", LOGIC;
+ "not", NOT;
+ "or", OR;
+ "predicate", PREDICATE;
+ "prop", PROP;
+ "real", REAL;
+ "rewriting", REWRITING;
+ "then", THEN;
+ "true", TRUE;
+ "type", TYPE;
+ "unit", UNIT;
+ "void", VOID;
+ "with", WITH;
+ ]
+
+ let newline lexbuf =
+ let pos = lexbuf.lex_curr_p in
+ lexbuf.lex_curr_p <-
+ { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
+
+ let string_buf = Buffer.create 1024
+
+ exception Lexical_error of string
+
+ let char_for_backslash = function
+ | 'n' -> '\n'
+ | 't' -> '\t'
+ | c -> c
+
+ let num0 = Z.of_int 0
+ let num10 = Z.of_int 10
+ let num16 = Z.of_int 16
+
+ let decnumber s =
+ let r = ref num0 in
+ for i=0 to String.length s - 1 do
+ r := Z.add (Z.mul num10 !r)
+ (Z.of_int (Char.code s.[i] - Char.code '0'))
+ done;
+ !r
+
+ let hexnumber s =
+ let r = ref num0 in
+ for i=0 to String.length s - 1 do
+ let c = s.[i] in
+ let v =
+ match c with
+ | '0'..'9' -> Char.code c - Char.code '0'
+ | 'a'..'f' -> Char.code c - Char.code 'a' + 10
+ | 'A'..'F' -> Char.code c - Char.code 'A' + 10
+ | _ -> assert false
+ in
+ r := Z.add (Z.mul num16 !r) (Z.of_int v)
+ done;
+ !r
+
+}
+
+let newline = '\n'
+let space = [' ' '\t' '\r']
+let alpha = ['a'-'z' 'A'-'Z']
+let letter = alpha | '_'
+let digit = ['0'-'9']
+let hexdigit = ['0'-'9''a'-'f''A'-'F']
+let ident = (letter | '?') (letter | digit | '?' | '\'')*
+
+rule token = parse
+ | newline
+ { newline lexbuf; token lexbuf }
+ | space+
+ { token lexbuf }
+ | ident as id (* identifiers *)
+ { try
+ let k = Hashtbl.find keywords id in
+ if rules () = 0 then fprintf fmt "[rule] TR-Lexical-keyword@.";
+ k
+ with Not_found ->
+ if rules () = 0 then fprintf fmt "[rule] TR-Lexical-identifier@.";
+ IDENT id }
+ | digit+ as s (* integers *)
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-integer@.";
+ INTEGER s }
+ | (digit+ as i) ("" as f) ['e' 'E'] (['-' '+']? as sign (digit+ as exp))
+ | (digit+ as i) '.' (digit* as f)
+ (['e' 'E'] (['-' '+']? as sign (digit+ as exp)))?
+ | (digit* as i) '.' (digit+ as f)
+ (['e' 'E'] (['-' '+']? as sign (digit+ as exp)))?
+ (* decimal real literals *)
+ { (*
+ Format.eprintf "decimal real literal found: i=%s f=%s sign=%a exp=%a"
+ i f so sign so exp;
+ *)
+ if rules () = 0 then fprintf fmt "[rule] TR-Lexical-real@.";
+ let v =
+ match exp,sign with
+ | Some exp,Some "-" ->
+ Q.div (Q.of_bigint (decnumber (i^f)))
+ (Q.of_bigint (Z.pow (Z.of_int 10) (Z.to_int (decnumber exp))))
+ | Some exp,_ ->
+ Q.mul (Q.of_bigint (decnumber (i^f)))
+ (Q.of_bigint (Z.pow (Z.of_int 10) (Z.to_int (decnumber exp))))
+ | None,_ -> Q.of_bigint (decnumber (i^f))
+ in
+ let v =
+ Q.div v
+ (Q.of_bigint (Z.pow (Z.of_int 10) (String.length f)))
+ in
+ (* Format.eprintf " -> value = %s@." (Num.string_of_num v); *)
+ NUM v
+ }
+
+ (* hexadecimal real literals a la C99 (0x..p..) *)
+ | "0x" (hexdigit+ as e) ('.' (hexdigit* as f))?
+ ['p''P'] (['+''-']? as sign) (digit+ as exp)
+ { (* Format.eprintf "hex num found: %s" (lexeme lexbuf); *)
+ if rules () = 0 then fprintf fmt "[rule] TR-Lexical-hexponent@.";
+ if rules () = 0 then fprintf fmt "[rule] TR-Lexical-hexa@.";
+ let f = match f with None -> "" | Some f -> f in
+ let v =
+ match sign with
+ | "-" ->
+ Q.div (Q.of_bigint (hexnumber (e^f)))
+ (Q.of_bigint (Z.pow (Z.of_int 2) (Z.to_int (decnumber exp))))
+ | _ ->
+ Q.mul (Q.of_bigint (hexnumber (e^f)))
+ (Q.of_bigint (Z.pow (Z.of_int 2) (Z.to_int (decnumber exp))))
+ in
+ let v =
+ Q.div v
+ (Q.of_bigint (Z.pow (Z.of_int 16) (String.length f)))
+ in
+ (* Format.eprintf " -> value = %s@." (Num.string_of_num v); *)
+ NUM v
+ }
+ | "(*"
+ { comment lexbuf; token lexbuf }
+ | "(* status:" space* (ident as id) space* "*)" { STATUS id }
+ | "'"
+ { QUOTE }
+ | ","
+ { COMMA }
+ | ";"
+ { PV }
+ | "("
+ { LEFTPAR }
+ | ")"
+ { RIGHTPAR }
+ | ":"
+ { COLON }
+ | "->"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ ARROW }
+ | "<-"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ LEFTARROW }
+ | "<->"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ LRARROW }
+ | "="
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ EQUAL }
+ | "<"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ LT }
+ | "<="
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ LE }
+ | ">"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ GT }
+ | ">="
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ GE }
+ | "<>"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ NOTEQ }
+ | "+"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ PLUS }
+ | "-"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ MINUS }
+ | "*"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ TIMES }
+ | "/"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ SLASH }
+ | "%"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ PERCENT }
+ | "@"
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-operator@.";
+ AT }
+ | "."
+ { DOT }
+ | "["
+ { LEFTSQ }
+ | "]"
+ { RIGHTSQ }
+ | "{"
+ { LEFTBR }
+ | "}"
+ { RIGHTBR }
+ | "|"
+ { BAR }
+ | "^"
+ { HAT }
+ | "\""
+ { Buffer.clear string_buf; string lexbuf }
+ | eof
+ { EOF }
+ | _ as c
+ { raise (Lexical_error ("illegal character: " ^ String.make 1 c)) }
+
+and comment = parse
+ | "*)"
+ { () }
+ | "(*"
+ { comment lexbuf; comment lexbuf }
+ | newline
+ { newline lexbuf; comment lexbuf }
+ | eof
+ { raise (Lexical_error "unterminated comment") }
+ | _
+ { comment lexbuf }
+
+and string = parse
+ | "\""
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-string@.";
+ STRING (Buffer.contents string_buf) }
+ | "\\" (_ as c)
+ { Buffer.add_char string_buf (char_for_backslash c); string lexbuf }
+ | newline
+ { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
+ | eof
+ { raise (Lexical_error "unterminated string") }
+ | _ as c
+ { Buffer.add_char string_buf c; string lexbuf }
diff --git a/src/inputlang/altergo/why_parser.mly b/src/inputlang/altergo/why_parser.mly
new file mode 100644
index 000000000..7c98200f0
--- /dev/null
+++ b/src/inputlang/altergo/why_parser.mly
@@ -0,0 +1,555 @@
+/**************************************************************************/
+/* */
+/* The Alt-Ergo theorem prover */
+/* Copyright (C) 2006-2011 */
+/* */
+/* Sylvain Conchon */
+/* Evelyne Contejean */
+/* */
+/* Francois Bobot */
+/* Mohamed Iguernelala */
+/* Stephane Lescuyer */
+/* Alain Mebsout */
+/* Claire Dross */
+/* */
+/* CNRS - INRIA - Universite Paris Sud */
+/* */
+/* This file is distributed under the terms of the CeCILL-C licence */
+/* */
+/**************************************************************************/
+
+/*
+ * The Why certification tool
+ * Copyright (C) 2002 Jean-Christophe FILLIATRE
+ *
+ * This software is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public
+ * License version 2, as published by the Free Software Foundation.
+ *
+ * This software is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+ *
+ * See the GNU General Public License version 2 for more details
+ * (enclosed in the file GPL).
+ */
+
+/* from http://www.lysator.liu.se/c/ANSI-C-grammar-y.html */
+
+%{
+
+ open Why_ptree
+ open Parsing
+ open Format
+
+ let rules () = 1 (** replace open Option *)
+ let fmt = Debug.get_debug_formatter ()
+
+ let loc () = (symbol_start_pos (), symbol_end_pos ())
+ let loc_i i = (rhs_start_pos i, rhs_end_pos i)
+ let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
+
+ let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
+ let mk_pp d = mk_ppl (loc ()) d
+ let mk_pp_i i d = mk_ppl (loc_i i) d
+
+ let infix_ppl loc a i b = mk_ppl loc (PPinfix (a, i, b))
+ let infix_pp a i b = infix_ppl (loc ()) a i b
+
+ let prefix_ppl loc p a = mk_ppl loc (PPprefix (p, a))
+ let prefix_pp p a = prefix_ppl (loc ()) p a
+
+ let check_binary_mode s =
+ String.iter (fun x-> if x<>'0' && x<>'1' then raise Parsing.Parse_error) s;
+ s
+
+%}
+
+/* Tokens */
+
+%token <string> IDENT
+%token <string> INTEGER
+%token <string> FLOAT
+%token <Q.t> NUM
+%token <string> STRING
+%token INCLUDE
+%token WITH
+%token AND LEFTARROW ARROW AC AT AXIOM INVERSION REWRITING
+%token BAR HAT
+%token BOOL COLON COMMA PV DISTINCT DOT ELSE EOF EQUAL
+%token EXISTS FALSE VOID FORALL FUNCTION GE GOAL GT CHECK CUT ADDTERM
+%token IF IN INT BITV
+%token LE LET LEFTPAR LEFTSQ LEFTBR LOGIC LRARROW LT MINUS
+%token NOT NOTEQ OR PERCENT PLUS PREDICATE PROP
+%token QUOTE REAL UNIT
+%token RIGHTPAR RIGHTSQ RIGHTBR
+%token SLASH
+%token THEN TIMES TRUE TYPE
+%token REACH
+
+%token <string> STATUS
+
+/* Precedences */
+
+%nonassoc INCLUDE
+%nonassoc WITH
+%nonassoc IN
+%nonassoc prec_forall prec_exists
+%right ARROW LRARROW
+%right OR
+%right AND
+%nonassoc prec_ite
+%left prec_relation EQUAL NOTEQ LT LE GT GE
+%left PLUS MINUS
+%left TIMES SLASH PERCENT AT
+%nonassoc HAT
+%nonassoc uminus
+%nonassoc NOT DOT
+%right prec_named
+%nonassoc CHECK CUT ADDTERM
+%left LEFTSQ
+%nonassoc LIDENT
+
+/* Entry points */
+
+%type <Why_ptree.lexpr list> trigger
+%start trigger
+%type <Why_ptree.lexpr> lexpr
+%start lexpr
+%type <string list * Why_ptree.file> file
+%start file
+%type <(string (* resultat *) * Loc.position * Why_ptree.file) list> split_file
+%start split_file
+%%
+
+split_file:
+ | EOF { [] }
+ | STATUS list1_decl split_file { ($1,Loc.extract (loc_i 2), $2)::$3 }
+
+file:
+| includes list1_decl EOF
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-file@.";
+ $1, $2 }
+| list1_decl EOF
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-file@.";
+ [], $1 }
+| EOF
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-file@.";
+ [], [] }
+;
+
+includes:
+| INCLUDE STRING { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-file@.";
+ [$2]}
+| INCLUDE STRING includes{ if rules () = 0 then fprintf fmt "[rule] TR-Lexical-file@.";
+ $2::$3}
+
+list1_decl:
+| decl
+ { [$1] }
+| decl list1_decl
+ { $1 :: $2 }
+;
+
+decl:
+| TYPE type_vars ident
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ TypeDecl (loc_ij 1 2, $2, $3, Abstract) }
+| TYPE type_vars ident EQUAL list1_constructors_sep_bar
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ TypeDecl (loc_i 2, $2, $3, Enum $5 ) }
+| TYPE type_vars ident EQUAL record_type
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ TypeDecl (loc_i 2, $2, $3, Record $5 ) }
+| LOGIC ac_modifier list1_named_ident_sep_comma COLON logic_type
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ Logic (loc (), $2, $3, $5) }
+| FUNCTION named_ident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR COLON
+ primitive_type EQUAL lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ Function_def (loc (), $2, $4, $7, $9) }
+| PREDICATE named_ident EQUAL lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ Predicate_def (loc (), $2, [], $4) }
+| PREDICATE named_ident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR EQUAL lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ Predicate_def (loc (), $2, $4, $7) }
+| AXIOM ident COLON lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ if false (* !Preoptions.inversion_axioms*) then
+ let b =
+ try String.sub $2 (String.length $2 - 9) 9 = "inversion"
+ with Invalid_argument _ -> false
+ in
+ Axiom (loc (), $2, b, $4)
+ else Axiom (loc (), $2, false, $4) }
+| INVERSION ident COLON lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ Axiom (loc (), $2, true, $4) }
+| REWRITING ident COLON list1_lexpr_sep_pv
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ Rewriting(loc (), $2, $4) }
+| GOAL ident COLON lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-decl@.";
+ Goal (loc (), $2, $4) }
+;
+
+ac_modifier:
+ /* */ { Symbols.Other }
+| AC { Symbols.Ac }
+
+primitive_type:
+| INT
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-primitive-type@.";
+ PPTint }
+| BOOL
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-primitive-type@.";
+ PPTbool }
+| REAL
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-primitive-type@.";
+ PPTreal }
+| UNIT
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-primitive-type@.";
+ PPTunit }
+| BITV LEFTSQ INTEGER RIGHTSQ
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-primitive-type@.";
+ PPTbitv(int_of_string $3) }
+| ident
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-primitive-type@.";
+ PPTexternal ([], $1, loc ()) }
+| type_var
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-primitive-type@.";
+ PPTvarid ($1, loc ()) }
+| primitive_type ident
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-primitive-type@.";
+ PPTexternal ([$1], $2, loc_i 2) }
+| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR ident
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-primitive-type@.";
+ PPTexternal ($2, $4, loc_i 4) }
+;
+
+logic_type:
+| list0_primitive_type_sep_comma ARROW PROP
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-logic-type@.";
+ PPredicate $1 }
+| PROP
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-logic-type@.";
+ PPredicate [] }
+| list0_primitive_type_sep_comma ARROW primitive_type
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-logic-type@.";
+ PFunction ($1, $3) }
+| primitive_type
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-logic-type@.";
+ PFunction ([], $1) }
+;
+
+list1_primitive_type_sep_comma:
+| primitive_type { [$1] }
+| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
+;
+
+list0_primitive_type_sep_comma:
+| /* epsilon */ { [] }
+| list1_primitive_type_sep_comma { $1 }
+;
+
+list0_logic_binder_sep_comma:
+| /* epsilon */ { [] }
+| list1_logic_binder_sep_comma { $1 }
+;
+
+list1_logic_binder_sep_comma:
+| logic_binder { [$1] }
+| logic_binder COMMA list1_logic_binder_sep_comma { $1 :: $3 }
+;
+
+logic_binder:
+| ident COLON primitive_type
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-logic-binder@.";
+ (loc_i 1, $1, $3) }
+;
+
+list1_constructors_sep_bar:
+| ident { [$1] }
+| ident BAR list1_constructors_sep_bar { $1 :: $3}
+;
+
+
+lexpr:
+
+| simple_expr { $1 }
+
+/* binary operators */
+
+| lexpr PLUS lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 PPadd $3 }
+| lexpr MINUS lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 PPsub $3 }
+| lexpr TIMES lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 PPmul $3 }
+| lexpr SLASH lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 PPdiv $3 }
+| lexpr PERCENT lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 PPmod $3 }
+| lexpr AND lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 PPand $3 }
+| lexpr OR lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 PPor $3 }
+| lexpr LRARROW lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 PPiff $3 }
+| lexpr ARROW lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 PPimplies $3 }
+| lexpr relation lexpr %prec prec_relation
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ infix_pp $1 $2 $3 }
+
+/* unary operators */
+
+| NOT lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ prefix_pp PPnot $2 }
+| MINUS lexpr %prec uminus
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ prefix_pp PPneg $2 }
+
+/* bit vectors */
+
+| LEFTSQ BAR INTEGER BAR RIGHTSQ
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-bitv@.";
+ if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPconst (ConstBitv (check_binary_mode $3))) }
+| lexpr HAT LEFTBR INTEGER COMMA INTEGER RIGHTBR
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ let i = mk_pp (PPconst (ConstInt $4)) in
+ let j = mk_pp (PPconst (ConstInt $6)) in
+ mk_pp (PPextract ($1, i, j)) }
+| lexpr AT lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPconcat($1, $3)) }
+
+/* predicate or function calls */
+
+| DISTINCT LEFTPAR list2_lexpr_sep_comma RIGHTPAR
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPdistinct $3) }
+
+
+| IF lexpr THEN lexpr ELSE lexpr %prec prec_ite
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPif ($2, $4, $6)) }
+
+| FORALL list1_named_ident_sep_comma COLON primitive_type triggers
+ DOT lexpr %prec prec_forall
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPforall_named ($2, $4, $5, $7)) }
+
+| EXISTS list1_named_ident_sep_comma COLON primitive_type triggers
+ DOT lexpr %prec prec_exists
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPexists_named ($2, $4, $5, $7)) }
+
+| STRING COLON lexpr %prec prec_named
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPnamed ($1, $3)) }
+
+| LET ident EQUAL lexpr IN lexpr
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPlet ($2, $4, $6)) }
+
+| CHECK lexpr
+ { mk_pp (PPcheck $2) }
+
+| CUT lexpr
+ { mk_pp (PPcut $2) }
+;
+
+simple_expr :
+
+/* constants */
+| INTEGER
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPconst (ConstInt $1)) }
+| NUM
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPconst (ConstReal $1)) }
+| TRUE
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPconst ConstTrue) }
+| FALSE
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPconst ConstFalse) }
+| VOID
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPconst ConstVoid) }
+| ident
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPvar $1) }
+
+/* records */
+
+| LEFTBR list1_label_expr_sep_PV RIGHTBR
+ { mk_pp (PPrecord $2) }
+
+| LEFTBR simple_expr WITH list1_label_expr_sep_PV RIGHTBR
+ { mk_pp (PPwith($2, $4)) }
+
+| simple_expr DOT ident
+ { mk_pp (PPdot($1, $3)) }
+
+/* function or predicat calls */
+
+| ident LEFTPAR list0_lexpr_sep_comma RIGHTPAR
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPapp ($1, $3)) }
+
+
+/* arrays */
+
+| simple_expr LEFTSQ lexpr RIGHTSQ
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp(PPget($1, $3)) }
+| simple_expr LEFTSQ array_assignements RIGHTSQ
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ let acc, l = match $3 with
+ | [] -> assert false
+ | (i, v)::l -> mk_pp (PPset($1, i, v)), l
+ in
+ List.fold_left (fun acc (i,v) -> mk_pp (PPset(acc, i, v))) acc l
+ }
+
+| LEFTPAR lexpr RIGHTPAR
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ $2 }
+
+| simple_expr COLON primitive_type
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-expr@.";
+ mk_pp (PPcast($1,$3))
+ }
+;
+
+array_assignements:
+| array_assignement { [$1] }
+| array_assignement COMMA array_assignements { $1 :: $3 }
+;
+
+array_assignement:
+| lexpr LEFTARROW lexpr { $1, $3 }
+;
+
+triggers:
+| /* epsilon */
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-triggers@.";
+ [] }
+| LEFTSQ list1_trigger_sep_bar RIGHTSQ
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-triggers@.";
+ $2 }
+;
+
+list1_trigger_sep_bar:
+| trigger { [$1] }
+| trigger BAR list1_trigger_sep_bar { $1 :: $3 }
+;
+
+trigger:
+ list1_lexpr_sep_comma
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-trigger@.";
+ $1 }
+;
+
+
+list1_lexpr_sep_pv:
+| lexpr { [$1] }
+| lexpr PV { [$1] }
+| lexpr PV list1_lexpr_sep_pv { $1 :: $3 }
+;
+
+list0_lexpr_sep_comma:
+| /*empty */ { [] }
+| lexpr { [$1] }
+| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
+;
+
+list1_lexpr_sep_comma:
+| lexpr { [$1] }
+| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
+;
+
+list2_lexpr_sep_comma:
+| lexpr COMMA lexpr { [$1; $3] }
+| lexpr COMMA list2_lexpr_sep_comma { $1 :: $3 }
+;
+
+relation:
+| LT { PPlt }
+| LE { PPle }
+| GT { PPgt }
+| GE { PPge }
+| EQUAL { PPeq }
+| NOTEQ { PPneq }
+;
+
+record_type:
+| LEFTBR list1_label_sep_PV RIGHTBR
+ { $2 }
+;
+
+list1_label_sep_PV:
+| label_with_type { [$1] }
+| label_with_type PV list1_label_sep_PV { $1::$3 }
+;
+
+label_with_type:
+| ident COLON primitive_type
+ { $1,$3 }
+;
+
+
+list1_label_expr_sep_PV:
+| ident EQUAL lexpr
+ { [$1, $3] }
+| ident EQUAL lexpr PV list1_label_expr_sep_PV
+ { ($1, $3) :: $5 }
+;
+
+type_var:
+| QUOTE ident
+ { if rules () = 0 then fprintf fmt "[rule] TR-Lexical-car-type@.";
+ $2 }
+;
+
+type_vars:
+| /* empty */
+ { [] }
+| type_var
+ { [$1] }
+| LEFTPAR list1_type_var_sep_comma RIGHTPAR
+ { $2 }
+
+list1_type_var_sep_comma:
+| type_var { [$1] }
+| type_var COMMA list1_type_var_sep_comma { $1 :: $3 }
+;
+
+ident:
+| IDENT { $1 }
+;
+
+list1_named_ident_sep_comma:
+| named_ident { [$1] }
+| named_ident COMMA list1_named_ident_sep_comma { $1 :: $3 }
+;
+
+named_ident:
+| IDENT { $1, "" }
+| IDENT STRING { $1, $2 }
+;
+
diff --git a/src/inputlang/altergo/why_ptree.mli b/src/inputlang/altergo/why_ptree.mli
new file mode 100644
index 000000000..acbba4894
--- /dev/null
+++ b/src/inputlang/altergo/why_ptree.mli
@@ -0,0 +1,193 @@
+(**************************************************************************)
+(* *)
+(* The Alt-Ergo theorem prover *)
+(* Copyright (C) 2006-2011 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* *)
+(* Francois Bobot *)
+(* Mohamed Iguernelala *)
+(* Stephane Lescuyer *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+type loc = Lexing.position * Lexing.position
+
+type constant =
+ | ConstBitv of string
+ | ConstInt of string
+ | ConstReal of Q.t
+ | ConstTrue
+ | ConstFalse
+ | ConstVoid
+
+type pp_infix =
+ | PPand | PPor | PPimplies | PPiff
+ | PPlt | PPle | PPgt | PPge | PPeq | PPneq
+ | PPadd | PPsub | PPmul | PPdiv | PPmod
+
+type pp_prefix =
+ | PPneg | PPnot
+
+type ppure_type =
+ | PPTint
+ | PPTbool
+ | PPTreal
+ | PPTunit
+ | PPTbitv of int
+ | PPTvarid of string * loc
+ | PPTexternal of ppure_type list * string * loc
+
+type lexpr =
+ { pp_loc : loc; pp_desc : pp_desc }
+
+and pp_desc =
+ | PPvar of string
+ | PPapp of string * lexpr list
+ | PPdistinct of lexpr list
+ | PPconst of constant
+ | PPinfix of lexpr * pp_infix * lexpr
+ | PPprefix of pp_prefix * lexpr
+ | PPget of lexpr * lexpr
+ | PPset of lexpr * lexpr * lexpr
+ | PPdot of lexpr * string
+ | PPrecord of (string * lexpr) list
+ | PPwith of lexpr * (string * lexpr) list
+ | PPextract of lexpr * lexpr * lexpr
+ | PPconcat of lexpr * lexpr
+ | PPif of lexpr * lexpr * lexpr
+ | PPforall of string list * ppure_type * lexpr list list * lexpr
+ | PPexists of string list * ppure_type * lexpr list list * lexpr
+ | PPforall_named of
+ (string * string) list * ppure_type * lexpr list list * lexpr
+ | PPexists_named of
+ (string * string) list * ppure_type * lexpr list list * lexpr
+ | PPnamed of string * lexpr
+ | PPlet of string * lexpr * lexpr
+ | PPcheck of lexpr
+ | PPcut of lexpr
+ | PPcast of lexpr * ppure_type
+
+(* Declarations. *)
+
+type plogic_type =
+ | PPredicate of ppure_type list
+ | PFunction of ppure_type list * ppure_type
+
+type name_kind = Symbols.name_kind
+
+type body_type_decl =
+ | Record of (string * ppure_type) list (* lbl : t *)
+ | Enum of string list
+ | Abstract
+
+type inversion = bool
+
+type decl =
+ | Axiom of loc * string * inversion * lexpr
+ | Rewriting of loc * string * lexpr list
+ | Goal of loc * string * lexpr
+ | Logic of loc * name_kind * (string * string) list * plogic_type
+ | Predicate_def of
+ loc * (string * string) *
+ (loc * string * ppure_type) list * lexpr
+ | Function_def of
+ loc * (string * string) *
+ (loc * string * ppure_type) list * ppure_type * lexpr
+ | TypeDecl of loc * string list * string * body_type_decl
+
+type file = decl list
+
+(*** typed ast *)
+
+type ('a, 'b) annoted =
+ { c : 'a;
+ annot : 'b }
+
+type tconstant =
+ | Tint of string
+ | Treal of Num.num
+ | Tbitv of string
+ | Ttrue
+ | Tfalse
+ | Tvoid
+
+type 'a tterm =
+ { tt_ty : Ty.t; tt_desc : 'a tt_desc }
+and 'a tt_desc =
+ | TTconst of tconstant
+ | TTvar of Symbols.t
+ | TTinfix of ('a tterm, 'a) annoted * Symbols.t * ('a tterm, 'a) annoted
+ | TTprefix of Symbols.t * ('a tterm, 'a) annoted
+ | TTapp of Symbols.t * ('a tterm, 'a) annoted list
+ | TTget of ('a tterm, 'a) annoted * ('a tterm, 'a) annoted
+ | TTset of
+ ('a tterm, 'a) annoted * ('a tterm, 'a) annoted * ('a tterm, 'a) annoted
+ | TTextract of
+ ('a tterm, 'a) annoted * ('a tterm, 'a) annoted * ('a tterm, 'a) annoted
+ | TTconcat of ('a tterm, 'a) annoted * ('a tterm, 'a) annoted
+ | TTdot of ('a tterm, 'a) annoted * Strings.Hashcons.t
+ | TTrecord of (Strings.Hashcons.t * ('a tterm, 'a) annoted) list
+ | TTlet of Symbols.t * ('a tterm, 'a) annoted * ('a tterm, 'a) annoted
+ | TTnamed of Strings.Hashcons.t * ('a tterm, 'a) annoted
+
+type 'a tatom =
+ | TAtrue
+ | TAfalse
+ | TAeq of ('a tterm, 'a) annoted list
+ | TAdistinct of ('a tterm, 'a) annoted list
+ | TAneq of ('a tterm, 'a) annoted list
+ | TAle of ('a tterm, 'a) annoted list
+ | TAlt of ('a tterm, 'a) annoted list
+ | TApred of ('a tterm, 'a) annoted
+ | TAbuilt of Strings.Hashcons.t * ('a tterm, 'a) annoted list
+
+type 'a oplogic =
+ OPand |OPor | OPimp | OPnot | OPiff
+ | OPif of ('a tterm, 'a) annoted
+
+type 'a quant_form = {
+ (* quantified variables that appear in the formula *)
+ qf_bvars : (Symbols.t * Ty.t) list ;
+ qf_upvars : (Symbols.t * Ty.t) list ;
+ qf_triggers : ('a tterm, 'a) annoted list list ;
+ qf_form : ('a tform, 'a) annoted
+}
+
+and 'a tform =
+ | TFatom of ('a tatom, 'a) annoted
+ | TFop of 'a oplogic * (('a tform, 'a) annoted) list
+ | TFforall of 'a quant_form
+ | TFexists of 'a quant_form
+ | TFlet of (Symbols.t * Ty.t) list * Symbols.t *
+ ('a tterm, 'a) annoted * ('a tform, 'a) annoted
+ | TFnamed of Strings.Hashcons.t * ('a tform, 'a) annoted
+
+
+type 'a rwt_rule = {
+ rwt_vars : (Symbols.t * Ty.t) list;
+ rwt_left : 'a;
+ rwt_right : 'a
+}
+
+type goal_sort = Cut | Check | Thm
+
+type 'a tdecl =
+ | TAxiom of loc * string * inversion * ('a tform, 'a) annoted
+ | TRewriting of loc * string * (('a tterm, 'a) annoted rwt_rule) list
+ | TGoal of loc * goal_sort * string * ('a tform, 'a) annoted
+ | TLogic of loc * string list * plogic_type
+ | TPredicate_def of
+ loc * string *
+ (string * ppure_type) list * ('a tform, 'a) annoted
+ | TFunction_def of
+ loc * string *
+ (string * ppure_type) list * ppure_type * ('a tform, 'a) annoted
+ | TTypeDecl of loc * string list * string * body_type_decl
+
diff --git a/src/inputlang/altergo/why_typing.ml b/src/inputlang/altergo/why_typing.ml
new file mode 100644
index 000000000..c74051886
--- /dev/null
+++ b/src/inputlang/altergo/why_typing.ml
@@ -0,0 +1,1390 @@
+(**************************************************************************)
+(* *)
+(* The Alt-Ergo theorem prover *)
+(* Copyright (C) 2006-2011 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* *)
+(* Francois Bobot *)
+(* Mohamed Iguernelala *)
+(* Stephane Lescuyer *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+open Options
+open Format
+open Why_ptree
+open Common
+
+module S = Set.Make(String)
+module Sy = Symbols.Set
+
+module MString =
+ Map.Make(struct type t = string let compare = Pervasives.compare end)
+
+module Types = struct
+
+ (* environment for user-defined types *)
+ type t = {
+ to_ty : Ty.t MString.t;
+ from_labels : string MString.t; }
+
+ let to_tyvars = ref MString.empty
+
+ let empty =
+ { to_ty = MString.empty;
+ from_labels = MString.empty }
+
+ let fresh_vars env vars loc =
+ List.map
+ (fun x ->
+ if MString.mem x !to_tyvars then
+ error (TypeDuplicateVar x) loc;
+ let nv = Ty.Tvar (Ty.fresh_var ()) in
+ to_tyvars := MString.add x nv !to_tyvars;
+ nv
+ ) vars
+
+ let check_number_args loc lty ty =
+ match ty with
+ | Ty.Text (lty', s) | Ty.Trecord {Ty.args=lty'; name=s} ->
+ if List.length lty <> List.length lty' then
+ error (WrongNumberofArgs (Hstring.view s)) loc;
+ lty'
+ | Ty.Tsum (s, _) ->
+ if List.length lty <> 0 then
+ error (WrongNumberofArgs (Hstring.view s)) loc;
+ []
+ | _ -> assert false
+
+ let equal_pp_vars lpp lvars =
+ try
+ List.for_all2
+ (fun pp x ->
+ match pp with PPTvarid (y, _) -> x = y | _ -> false) lpp lvars
+ with Invalid_argument _ -> false
+
+ let rec ty_of_pp loc env rectype = function
+ | PPTint -> Ty.Tint
+ | PPTbool -> Ty.Tbool
+ | PPTunit -> Ty.Tunit
+ | PPTreal -> Ty.Treal
+ | PPTbitv n -> Ty.Tbitv n
+ | PPTvarid (s, _) ->
+ begin
+ try MString.find s !to_tyvars
+ with Not_found ->
+ let nty = Ty.Tvar (Ty.fresh_var ()) in
+ to_tyvars := MString.add s nty !to_tyvars;
+ nty
+ end
+ | PPTexternal (l, s, loc) when s = "farray" ->
+ let t1,t2 = match l with
+ | [t2] -> PPTint,t2
+ | [t1;t2] -> t1,t2
+ | _ -> error (WrongArity(s,2)) loc in
+ let ty1 = ty_of_pp loc env rectype t1 in
+ let ty2 = ty_of_pp loc env rectype t2 in
+ Ty.Tfarray (ty1, ty2)
+ | PPTexternal (l, s, loc) ->
+ begin
+ match rectype with
+ | Some (id, vars, ty) when s = id && equal_pp_vars l vars -> ty
+ | _ ->
+ try
+ let lty = List.map (ty_of_pp loc env rectype) l in
+ let ty = MString.find s env.to_ty in
+ let vars = check_number_args loc lty ty in
+ Ty.instantiate vars lty ty
+ with Not_found ->
+ error (UnknownType s) loc
+ end
+
+ let add env vars id body loc =
+ if MString.mem id env.to_ty then error (ClashType id) loc;
+ let ty_vars = fresh_vars env vars loc in
+ match body with
+ | Abstract ->
+ { env with to_ty = MString.add id (Ty.text ty_vars id) env.to_ty }
+ | Enum lc ->
+ { env with to_ty = MString.add id (Ty.tsum id lc) env.to_ty }
+ | Record lbs ->
+ let lbs =
+ List.map (fun (x, pp) -> x, ty_of_pp loc env None pp) lbs in
+ { to_ty = MString.add id (Ty.trecord ty_vars id lbs) env.to_ty;
+ from_labels =
+ List.fold_left
+ (fun fl (l,_) -> MString.add l id fl) env.from_labels lbs }
+
+ module SH = Set.Make(Hstring)
+
+ let check_labels lbs ty loc =
+ let rec check_duplicates s = function
+ | [] -> ()
+ | (lb, _) :: l ->
+ if SH.mem lb s then error (DuplicateLabel lb) loc;
+ check_duplicates (SH.add lb s) l
+ in
+ check_duplicates SH.empty lbs;
+ match ty with
+ | Ty.Trecord {Ty.lbs=l} ->
+ if List.length lbs <> List.length l then
+ error WrongNumberOfLabels loc;
+ List.iter
+ (fun (lb, _) ->
+ try ignore (Hstring.list_assoc lb l)
+ with Not_found -> error (WrongLabel(lb, ty)) loc) lbs;
+ ty
+ | _ -> assert false
+
+
+ let from_labels env lbs loc =
+ match lbs with
+ | [] -> assert false
+ | (l, _) :: _ ->
+ try
+ let l = Hstring.view l in
+ let ty = MString.find (MString.find l env.from_labels) env.to_ty in
+ check_labels lbs ty loc
+ with Not_found -> error (NoRecordType l) loc
+
+ let rec monomorphized = function
+ | PPTvarid (x, _) when not (MString.mem x !to_tyvars) ->
+ to_tyvars := MString.add x (Ty.fresh_empty_text ()) !to_tyvars;
+
+ | PPTexternal (args, _, _) ->
+ List.iter monomorphized args
+
+ | pp_ty -> ()
+
+ let init_labels fl id loc = function
+ | Record lbs ->
+ List.fold_left
+ (fun fl (s, _) ->
+ if MString.mem s fl then
+ error (ClashLabel (s, (MString.find s fl))) loc;
+ MString.add s id fl) fl lbs
+ | _ -> fl
+
+end
+
+module Env = struct
+
+ type profile = { args : Ty.t list; result : Ty.t }
+
+ type t = {
+ var_map : (Symbols.t * Ty.t) MString.t ; (* variables' map*)
+ types : Types.t ;
+ logics : (Symbols.t * profile) MString.t (* logic symbols' map *)
+ }
+
+ let empty = {
+ var_map = MString.empty;
+ types = Types.empty;
+ logics = MString.empty
+ }
+
+ let add env lv fvar ty =
+ let vmap =
+ List.fold_left
+ (fun vmap x -> MString.add x (fvar x, ty) vmap) env.var_map lv in
+ { env with var_map = vmap }
+
+ let add_var env lv pp_ty loc =
+ let ty = Types.ty_of_pp loc env.types None pp_ty in
+ add env lv Symbols.var ty
+
+ let add_names env lv pp_ty loc =
+ Types.monomorphized pp_ty;
+ let ty = Types.ty_of_pp loc env.types None pp_ty in
+ add env lv Symbols.name ty
+
+ let add_names_lbl env lv pp_ty loc =
+ Types.monomorphized pp_ty;
+ let ty = Types.ty_of_pp loc env.types None pp_ty in
+ let rlv =
+ List.fold_left (fun acc (x, lbl) ->
+ let lbl = Hstring.make lbl in
+ if not (Hstring.equal lbl Hstring.empty) then
+ Symbols.add_label lbl (Symbols.name x);
+ x::acc
+ ) [] lv in
+ let lv = List.rev rlv in
+ add env lv Symbols.name ty
+
+ let add_logics env ac names pp_profile loc =
+ let profile =
+ match pp_profile with
+ | PPredicate args ->
+ { args = List.map (Types.ty_of_pp loc env.types None) args;
+ result = Ty.Tbool }
+ (*| PFunction ([], PPTvarid (_, loc)) ->
+ error CannotGeneralize loc*)
+ | PFunction(args, res) ->
+ let args = List.map (Types.ty_of_pp loc env.types None) args in
+ let res = Types.ty_of_pp loc env.types None res in
+ { args = args; result = res }
+ in
+ let logics =
+ List.fold_left
+ (fun logics (n, lbl) ->
+ let sy = Symbols.name n ~kind:ac in
+ if MString.mem n logics then error (SymbAlreadyDefined n) loc;
+
+ let lbl = Hstring.make lbl in
+ if not (Hstring.equal lbl Hstring.empty) then
+ Symbols.add_label lbl sy;
+
+ MString.add n (sy, profile) logics)
+ env.logics names
+ in
+ { env with logics = logics }
+
+ let find {var_map=m} n = MString.find n m
+
+ let mem n {var_map=m} = MString.mem n m
+
+ let list_of {var_map=m} = MString.fold (fun _ c acc -> c::acc) m []
+
+ let add_type_decl env vars id body loc =
+ { env with types = Types.add env.types vars id body loc }
+
+ (* returns a type with fresh variables *)
+ let fresh_type env n loc =
+ try
+ let s, { args = args; result = r} = MString.find n env.logics in
+ let args, subst = Ty.fresh_list args Ty.esubst in
+ let res, _ = Ty.fresh r subst in
+ s, { args = args; result = res }
+ with Not_found -> error (SymbUndefined n) loc
+
+end
+
+let new_id = let r = ref 0 in fun () -> r := !r+1; !r
+
+let rec freevars_term acc t = match t.c.tt_desc with
+ | TTvar x -> Sy.add x acc
+ | TTapp (_,lt) -> List.fold_left freevars_term acc lt
+ | TTinfix (t1,_,t2) | TTget(t1, t2) ->
+ List.fold_left freevars_term acc [t1; t2]
+ | TTset (t1, t2, t3) ->
+ List.fold_left freevars_term acc [t1; t2; t3]
+ | TTdot (t1, _) -> freevars_term acc t1
+ | TTrecord lbs ->
+ List.fold_left (fun acc (_, t) -> freevars_term acc t) acc lbs
+ | _ -> acc
+
+let freevars_atom a = match a.c with
+ | TAeq lt | TAneq lt | TAle lt
+ | TAlt lt | TAbuilt(_,lt) | TAdistinct lt ->
+ List.fold_left freevars_term Sy.empty lt
+ | TApred t -> freevars_term Sy.empty t
+ | _ -> Sy.empty
+
+let rec freevars_form f = match f with
+ | TFatom a -> freevars_atom a
+ | TFop (_,lf) ->
+ List.fold_left Sy.union Sy.empty
+ (List.map (fun f -> freevars_form f.c) lf)
+ | TFforall qf | TFexists qf ->
+ let s = freevars_form qf.qf_form.c in
+ List.fold_left (fun acc (s,_) -> Sy.remove s acc) s qf.qf_bvars
+ | TFlet(up,v,t,f) -> freevars_term (Sy.remove v (freevars_form f.c)) t
+ | TFnamed(_, f) -> freevars_form f.c
+
+let symbol_of = function
+ PPadd -> Symbols.Op Symbols.Plus
+ | PPsub -> Symbols.Op Symbols.Minus
+ | PPmul -> Symbols.Op Symbols.Mult
+ | PPdiv -> Symbols.Op Symbols.Div
+ | PPmod -> Symbols.Op Symbols.Modulo
+ | _ -> assert false
+
+let rec type_term env f =
+ let e,t = type_term_desc env f.pp_loc f.pp_desc in
+ {c = { tt_desc = e ; tt_ty = t }; annot = new_id ()}
+
+and type_term_desc env loc = function
+ | PPconst ConstTrue ->
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-Const type %a@." Ty.print Ty.Tbool;
+ TTconst Ttrue, Ty.Tbool
+ | PPconst ConstFalse ->
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-Const type %a@." Ty.print Ty.Tbool;
+ TTconst Tfalse, Ty.Tbool
+ | PPconst ConstVoid ->
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-Const type %a@." Ty.print Ty.Tunit;
+ TTconst Tvoid, Ty.Tunit
+ | PPconst (ConstInt n) ->
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-Const type %a@." Ty.print Ty.Tint;
+ TTconst(Tint n), Ty.Tint
+ | PPconst (ConstReal n) ->
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-Const type %a@." Ty.print Ty.Treal;
+ TTconst(Treal n), Ty.Treal
+ | PPconst (ConstBitv n) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-Const type %a@." Ty.print
+ (Ty.Tbitv (String.length n));
+ TTconst(Tbitv n), Ty.Tbitv (String.length n)
+ | PPvar p ->
+ begin
+ try let s,t = Env.find env p in
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-Var$_\\Gamma$ type %a@."
+ Ty.print t;
+ TTvar s , t
+ with Not_found ->
+ match Env.fresh_type env p loc with
+ | s, { Env.args = []; result = ty} ->
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-Var$_\\Delta$ type %a@."
+ Ty.print ty;
+ TTvar s , ty
+ | _ -> error (ShouldBeApply p) loc
+ end
+ | PPapp(p,args) ->
+ begin
+ let te_args = List.map (type_term env) args in
+ let lt_args = List.map (fun {c={tt_ty=t}} -> t) te_args in
+ let s, {Env.args = lt; result = t} = Env.fresh_type env p loc in
+ try
+ List.iter2 Ty.unify lt lt_args;
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-App type %a@." Ty.print t;
+ TTapp(s,te_args), t
+ with
+ | Ty.TypeClash(t1,t2) ->
+ error (Unification(t1,t2)) loc
+ | Invalid_argument _ ->
+ error (WrongNumberofArgs p) loc
+ end
+ | PPinfix(t1,(PPadd | PPsub | PPmul | PPdiv as op),t2) ->
+ begin
+ let s = symbol_of op in
+ let te1 = type_term env t1 in
+ let te2 = type_term env t2 in
+ let ty1 = Ty.shorten te1.c.tt_ty in
+ let ty2 = Ty.shorten te2.c.tt_ty in
+ match ty1, ty2 with
+ | Ty.Tint, Ty.Tint ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpBin type %a@."
+ Ty.print ty1;
+ TTinfix(te1,s,te2) , ty1
+ | Ty.Treal, Ty.Treal ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpBin type %a@."
+ Ty.print ty2;
+ TTinfix(te1,s,te2), ty2
+ | Ty.Tint, _ -> error (ShouldHaveType(ty2,Ty.Tint)) t2.pp_loc
+ | Ty.Treal, _ -> error (ShouldHaveType(ty2,Ty.Treal)) t2.pp_loc
+ | _ -> error (ShouldHaveTypeIntorReal ty1) t1.pp_loc
+ end
+ | PPinfix(t1, PPmod, t2) ->
+ begin
+ let s = symbol_of PPmod in
+ let te1 = type_term env t1 in
+ let te2 = type_term env t2 in
+ let ty1 = Ty.shorten te1.c.tt_ty in
+ let ty2 = Ty.shorten te2.c.tt_ty in
+ match ty1, ty2 with
+ | Ty.Tint, Ty.Tint ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpMod type %a@."
+ Ty.print ty1;
+ TTinfix(te1,s,te2) , ty1
+ | _ -> error (ShouldHaveTypeInt ty1) t1.pp_loc
+ end
+ | PPprefix(PPneg, {pp_desc=PPconst (ConstInt n)}) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpUnarith type %a@."
+ Ty.print Ty.Tint;
+ TTconst(Tint ("-"^n)), Ty.Tint
+ | PPprefix(PPneg, {pp_desc=PPconst (ConstReal n)}) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpUnarith type %a@."
+ Ty.print Ty.Treal;
+ TTconst(Treal (Num.minus_num n)), Ty.Treal
+ | PPprefix(PPneg, e) ->
+ let te = type_term env e in
+ let ty = Ty.shorten te.c.tt_ty in
+ if ty<>Ty.Tint && ty<>Ty.Treal then
+ error (ShouldHaveTypeIntorReal ty) e.pp_loc;
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpUnarith type %a@."
+ Ty.print ty;
+ TTprefix(Symbols.Op Symbols.Minus, te), ty
+ | PPconcat(t1, t2) ->
+ begin
+ let te1 = type_term env t1 in
+ let te2 = type_term env t2 in
+ let ty1 = Ty.shorten te1.c.tt_ty in
+ let ty2 = Ty.shorten te2.c.tt_ty in
+ match ty1, ty2 with
+ | Ty.Tbitv n , Ty.Tbitv m ->
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-OpConcat type %a@."
+ Ty.print (Ty.Tbitv (n+m));
+ TTconcat(te1, te2), Ty.Tbitv (n+m)
+ | Ty.Tbitv _ , _ -> error (ShouldHaveTypeBitv ty2) t2.pp_loc
+ | _ , Ty.Tbitv _ -> error (ShouldHaveTypeBitv ty1) t1.pp_loc
+ | _ -> error (ShouldHaveTypeBitv ty1) t1.pp_loc
+ end
+ | PPextract(e, ({pp_desc=PPconst(ConstInt i)} as ei),
+ ({pp_desc=PPconst(ConstInt j)} as ej)) ->
+ begin
+ let te = type_term env e in
+ let tye = Ty.shorten te.c.tt_ty in
+ let i = int_of_string i in
+ let j = int_of_string j in
+ match tye with
+ | Ty.Tbitv n ->
+ if i>j then error (BitvExtract(i,j)) loc;
+ if j>=n then error (BitvExtractRange(n,j) ) loc;
+ let tei = type_term env ei in
+ let tej = type_term env ej in
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-OpExtract type %a@."
+ Ty.print (Ty.Tbitv (j-i+1));
+ TTextract(te, tei, tej), Ty.Tbitv (j-i+1)
+ | _ -> error (ShouldHaveType(tye,Ty.Tbitv (j+1))) loc
+ end
+ | PPget (t1, t2) ->
+ begin
+ let te1 = type_term env t1 in
+ let te2 = type_term env t2 in
+ let tyarray = Ty.shorten te1.c.tt_ty in
+ let tykey2 = Ty.shorten te2.c.tt_ty in
+ match tyarray with
+ | Ty.Tfarray (tykey,tyval) ->
+ begin try
+ Ty.unify tykey tykey2;
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-OpGet type %a@."
+ Ty.print tyval;
+ TTget(te1, te2), tyval
+ with
+ | Ty.TypeClash(t1,t2) ->
+ error (Unification(t1,t2)) loc
+ end
+ | _ -> error ShouldHaveTypeArray t1.pp_loc
+ end
+ | PPset (t1, t2, t3) ->
+ begin
+ let te1 = type_term env t1 in
+ let te2 = type_term env t2 in
+ let te3 = type_term env t3 in
+ let ty1 = Ty.shorten te1.c.tt_ty in
+ let tykey2 = Ty.shorten te2.c.tt_ty in
+ let tyval2 = Ty.shorten te3.c.tt_ty in
+ try
+ match ty1 with
+ | Ty.Tfarray (tykey,tyval) ->
+ Ty.unify tykey tykey2;Ty.unify tyval tyval2;
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-OpSet type %a@."
+ Ty.print ty1;
+ TTset(te1, te2, te3), ty1
+ | _ -> error ShouldHaveTypeArray t1.pp_loc
+ with
+ | Ty.TypeClash(t, t') ->
+ error (Unification(t, t')) loc
+ end
+ | PPif(t1,t2,t3) ->
+ begin
+ let te1 = type_term env t1 in
+ let ty1 = Ty.shorten te1.c.tt_ty in
+ if not (Ty.equal ty1 Ty.Tbool) then
+ error (ShouldHaveType(ty1,Ty.Tbool)) t1.pp_loc;
+ let te2 = type_term env t2 in
+ let te3 = type_term env t3 in
+ let ty2 = Ty.shorten te2.c.tt_ty in
+ let ty3 = Ty.shorten te3.c.tt_ty in
+ if not (Ty.equal ty2 ty3) then
+ error (ShouldHaveType(ty3,ty2)) t3.pp_loc;
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-Ite type %a@." Ty.print ty2;
+ TTapp(Symbols.name "ite",[te1;te2;te3]) , ty2
+ end
+ | PPdot(t, a) ->
+ begin
+ let te = type_term env t in
+ let ty = Ty.shorten te.c.tt_ty in
+ match ty with
+ | Ty.Trecord {Ty.name=g; lbs=lbs} ->
+ begin
+ try
+ let a = Hstring.make a in
+ TTdot(te, a), Hstring.list_assoc a lbs
+ with Not_found ->
+ let g = Hstring.view g in
+ error (ShouldHaveLabel(g,a)) t.pp_loc
+ end
+ | _ -> error (ShouldHaveTypeRecord ty) t.pp_loc
+ end
+ | PPrecord lbs ->
+ begin
+ let lbs =
+ List.map (fun (lb, t) -> Hstring.make lb, type_term env t) lbs in
+ let lbs = List.sort
+ (fun (l1, _) (l2, _) -> Hstring.compare l1 l2) lbs in
+ let ty = Types.from_labels env.Env.types lbs loc in
+ let ty, _ = Ty.fresh (Ty.shorten ty) Ty.esubst in
+ match ty with
+ | Ty.Trecord {Ty.lbs=ty_lbs} ->
+ begin
+ try
+ let lbs =
+ List.map2
+ (fun (s, te) (lb,ty_lb)->
+ Ty.unify te.c.tt_ty ty_lb;
+ lb, te) lbs ty_lbs
+ in
+ TTrecord(lbs), ty
+ with Ty.TypeClash(t1,t2) -> error (Unification(t1,t2)) loc
+ end
+ | _ -> error ShouldBeARecord loc
+ end
+ | PPwith(e, lbs) ->
+ begin
+ let te = type_term env e in
+ let lbs =
+ List.map
+ (fun (lb, t) -> Hstring.make lb, (type_term env t, t.pp_loc)) lbs in
+ let ty = Ty.shorten te.c.tt_ty in
+ match ty with
+ | Ty.Trecord {Ty.lbs=ty_lbs} ->
+ let nlbs =
+ List.map
+ (fun (lb, ty_lb) ->
+ try
+ let v, _ = Hstring.list_assoc lb lbs in
+ Ty.unify ty_lb v.c.tt_ty;
+ lb, v
+ with
+ | Not_found ->
+ lb, {c = { tt_desc = TTdot(te, lb); tt_ty = ty_lb};
+ annot = te.annot }
+ | Ty.TypeClash(t1,t2) ->
+ error (Unification(t1,t2)) loc
+ ) ty_lbs
+ in
+ List.iter
+ (fun (lb, _) ->
+ try ignore (Hstring.list_assoc lb ty_lbs)
+ with Not_found -> error (NoLabelInType(lb, ty)) loc) lbs;
+ TTrecord(nlbs), ty
+ | _ -> error ShouldBeARecord loc
+ end
+ | PPlet(x, t1, t2) ->
+ let te1 = type_term env t1 in
+ let ty1 = Ty.shorten te1.c.tt_ty in
+ let env = Env.add env [x] Symbols.name ty1 in
+ let te2 = type_term env t2 in
+ let ty2 = Ty.shorten te2.c.tt_ty in
+ let s, _ = Env.find env x in
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-Let type %a@." Ty.print ty2;
+ TTlet(s, te1, te2), ty2
+
+ (* | PPnamed(lbl, t) -> *)
+ (* let te = type_term env t in *)
+ (* te.c.tt_desc, te.c.tt_ty *)
+
+ | PPnamed (lbl, t) ->
+ let te = type_term env t in
+ let ty = Ty.shorten te.c.tt_ty in
+ let lbl = Hstring.make lbl in
+ TTnamed (lbl, te), ty
+
+ | PPcast (t,ty) ->
+ let ty = Types.ty_of_pp loc env.Env.types None ty in
+ let te = type_term env t in
+ begin try
+ Ty.unify te.c.tt_ty ty;
+ te.c.tt_desc, Ty.shorten te.c.tt_ty
+ with
+ | Ty.TypeClash(t1,t2) ->
+ error (Unification(t1,t2)) loc
+ end
+
+ | _ -> error SyntaxError loc
+
+
+let rec join_forall f = match f.pp_desc with
+ | PPforall(vs, ty, trs1, f) ->
+ let tyvars,trs2,f = join_forall f in
+ (vs,ty)::tyvars , trs1@trs2 , f
+ | PPforall_named (vs, ty, trs1, f) ->
+ let vs = List.map fst vs in
+ join_forall {f with pp_desc = PPforall (vs, ty, trs1, f)}
+ | PPnamed(lbl, f) ->
+ join_forall f
+ | _ -> [] , [] , f
+
+let rec join_exists f = match f.pp_desc with
+ | PPexists (vars, ty, trs1, f) ->
+ let tyvars,trs2,f = join_exists f in
+ (vars, ty)::tyvars , trs1@trs2, f
+ | PPexists_named (vs, ty, trs1, f) ->
+ let vs = List.map fst vs in
+ join_exists {f with pp_desc = PPexists (vs, ty, trs1, f)}
+ | PPnamed (_, f) -> join_exists f
+ | _ -> [] , [] , f
+
+let rec type_form env f =
+ let rec type_pp_desc pp_desc = match pp_desc with
+ | PPconst ConstTrue ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-True$_F$@.";
+ TFatom {c=TAtrue; annot=new_id ()}, Sy.empty
+ | PPconst ConstFalse ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-False$_F$@.";
+ TFatom {c=TAfalse; annot=new_id ()}, Sy.empty
+ | PPvar p ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-Var$_F$@.";
+ let r = begin
+ match Env.fresh_type env p f.pp_loc with
+ | s, { Env.args = []; result = Ty.Tbool} ->
+ let t2 = {c = {tt_desc=TTconst Ttrue;tt_ty=Ty.Tbool};
+ annot = new_id ()} in
+ let t1 = {c = {tt_desc=TTvar s; tt_ty=Ty.Tbool};
+ annot = new_id ()} in
+ TFatom {c = TAeq [t1;t2]; annot=new_id ()}
+ | _ -> error (NotAPropVar p) f.pp_loc
+ end in r, freevars_form r
+
+ | PPapp(p,args ) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-App$_F$@.";
+ let r =
+ begin
+ let te_args = List.map (type_term env) args in
+ let lt_args = List.map (fun {c={tt_ty=t}} -> t) te_args in
+ match Env.fresh_type env p f.pp_loc with
+ | s , { Env.args = lt; result = Ty.Tbool} ->
+ begin
+ try
+ List.iter2 Ty.unify lt lt_args;
+ if p = "<=" || p = "<" then
+ TFatom { c = TAbuilt(Hstring.make p,te_args);
+ annot=new_id ()}
+ else
+ let t1 = {
+ c = {tt_desc=TTapp(s,te_args); tt_ty=Ty.Tbool};
+ annot=new_id (); }
+ in
+ TFatom { c = TApred t1; annot=new_id () }
+ with
+ | Ty.TypeClash(t1,t2) ->
+ error (Unification(t1,t2)) f.pp_loc
+ | Invalid_argument _ ->
+ error (WrongNumberofArgs p) f.pp_loc
+ end
+ | _ -> error (NotAPredicate p) f.pp_loc
+ end
+ in r, freevars_form r
+
+ | PPdistinct (args) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-Distinct$_F$@.";
+ let r =
+ begin
+ let te_args = List.map (type_term env) args in
+ let lt_args = List.map (fun {c={tt_ty=t}} -> t) te_args in
+ try
+ let t = match lt_args with
+ | t::_ -> t
+ | [] ->
+ error (WrongNumberofArgs "distinct") f.pp_loc
+ in
+ List.iter (Ty.unify t) lt_args;
+ TFatom { c = TAdistinct te_args; annot=new_id () }
+ with
+ | Ty.TypeClash(t1,t2) -> error (Unification(t1,t2)) f.pp_loc
+ end
+ in r, freevars_form r
+
+ | PPinfix
+ ({pp_desc = PPinfix (_, (PPlt|PPle|PPgt|PPge|PPeq|PPneq), a)} as p,
+ (PPlt | PPle | PPgt | PPge | PPeq | PPneq as r), b) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpComp$_F$@.";
+ let r =
+ let q = { pp_desc = PPinfix (a, r, b); pp_loc = f.pp_loc } in
+ let f1,_ = type_form env p in
+ let f2,_ = type_form env q in
+ TFop(OPand, [f1;f2])
+ in r, freevars_form r
+ | PPinfix(t1, (PPeq | PPneq as op), t2) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpBin$_F$@.";
+ let r =
+ let tt1 = type_term env t1 in
+ let tt2 = type_term env t2 in
+ try
+ Ty.unify tt1.c.tt_ty tt2.c.tt_ty;
+ match op with
+ | PPeq -> TFatom {c = TAeq [tt1; tt2]; annot = new_id()}
+ | PPneq -> TFatom {c = TAneq [tt1; tt2]; annot = new_id()}
+ | _ -> assert false
+ with Ty.TypeClash(t1,t2) -> error (Unification(t1,t2)) f.pp_loc
+ in r, freevars_form r
+ | PPinfix(t1, (PPlt | PPgt | PPge | PPle as op), t2) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpComp$_F$@.";
+ let r =
+ let tt1 = type_term env t1 in
+ let tt2 = type_term env t2 in
+ try
+ Ty.unify tt1.c.tt_ty tt2.c.tt_ty;
+ let ty = Ty.shorten tt1.c.tt_ty in
+ match ty with
+ | Ty.Tint | Ty.Treal ->
+ let top =
+ match op with
+ | PPlt -> TAlt [tt1; tt2]
+ | PPgt -> TAlt [tt2; tt1]
+ | PPle -> TAle [tt1; tt2]
+ | PPge -> TAle [tt2; tt1]
+ | PPeq -> TAeq [tt1; tt2]
+ | PPneq -> TAneq [tt1; tt2]
+ | _ -> assert false
+ in
+ TFatom {c = top; annot=new_id ()}
+ | _ -> error (ShouldHaveTypeIntorReal ty) t1.pp_loc
+ with Ty.TypeClash(t1,t2) -> error (Unification(t1,t2)) f.pp_loc
+ in r, freevars_form r
+ | PPinfix(f1,op ,f2) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpConnectors$_F$@.";
+ begin
+ let f1,fv1 = type_form env f1 in
+ let f2,fv2 = type_form env f2 in
+ ((match op with
+ | PPand ->
+ TFop(OPand,[f1;f2])
+ | PPor -> TFop(OPor,[f1;f2])
+ | PPimplies -> TFop(OPimp,[f1;f2])
+ | PPiff -> TFop(OPiff,[f1;f2])
+ | _ -> assert false), Sy.union fv1 fv2)
+ end
+ | PPprefix(PPnot,f) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-OpNot$_F$@.";
+ let f, fv = type_form env f in TFop(OPnot,[f]),fv
+ | PPif(f1,f2,f3) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-Ite$_F$@.";
+ let f1 = type_term env f1 in
+ let f2,fv2 = type_form env f2 in
+ let f3,fv3 = type_form env f3 in
+ TFop(OPif f1,[f2;f3]), Sy.union fv2 fv3
+ | PPnamed(lbl,f) ->
+ let f, fv = type_form env f in
+ let lbl = Hstring.make lbl in
+ TFnamed(lbl, f), fv
+ | PPforall _ | PPexists _ ->
+ let ty_vars, ty, triggers, f' =
+ match pp_desc with
+ | PPforall(vars,ty,triggers,f') ->
+ let ty_vars, triggers', f' = join_forall f' in
+ (vars, ty)::ty_vars,ty ,triggers@triggers', f'
+ | PPexists(vars,ty,triggers,f') ->
+ let ty_vars, triggers', f' = join_exists f' in
+ (vars, ty)::ty_vars, ty, triggers@triggers', f'
+ | _ -> assert false
+ in
+ let env' =
+ List.fold_left
+ (fun env (lv, pp_ty) ->
+ Env.add_var env lv pp_ty f.pp_loc) env ty_vars in
+ let f', fv = type_form env' f' in
+ let ty_triggers = List.map (List.map (type_term env')) triggers in
+ let upbvars = Env.list_of env in
+ let bvars =
+ List.fold_left
+ (fun acc (l,_) ->
+ let tys = List.map (Env.find env') l in
+ let tys = List.filter (fun (s,_) -> Sy.mem s fv) tys in
+ tys @ acc) [] ty_vars in
+ let qf_form = {
+ qf_upvars = upbvars ;
+ qf_bvars = bvars ;
+ qf_triggers = ty_triggers ;
+ qf_form = f'}
+ in
+ (match pp_desc with
+ | PPforall _ ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-Forall$_F$@.";
+ TFforall qf_form
+ | PPexists _ ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-Exists$_F$@.";
+ Existantial.make qf_form
+ | _ -> assert false),
+ (List.fold_left (fun acc (l,_) -> Sy.remove l acc) fv bvars)
+ | PPlet (var,t,f) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-Let$_F$@.";
+ let {c= { tt_ty = ttype }} as tt = type_term env t in
+ let svar = Symbols.var var in
+ let up = Env.list_of env in
+ let env =
+ {env with
+ Env.var_map = MString.add var (svar, ttype) env.Env.var_map} in
+ let f,fv = type_form env f in
+ TFlet (up ,svar , tt, f), freevars_term (Sy.remove svar fv) tt
+
+
+ (* Remove labels : *)
+ | PPforall_named (lx, tys, trs, f) ->
+ let lx = List.map fst lx in
+ type_pp_desc (PPforall (lx, tys, trs, f))
+ | PPexists_named (lx, tys, trs, f) ->
+ let lx = List.map fst lx in
+ type_pp_desc (PPexists (lx, tys, trs, f))
+
+ | PPcheck _ | PPcut _ -> assert false
+
+ | _ ->
+ let te1 = type_term env f in
+ let ty = te1.c.tt_ty in
+ match ty with
+ | Ty.Tbool ->
+ let te2 = {c = {tt_desc=TTconst Ttrue;tt_ty=Ty.Tbool};
+ annot = new_id ()}
+ in
+ let r = TFatom {c = TAeq [te1;te2]; annot=new_id ()} in
+ r, freevars_form r
+ | _ -> error ShouldHaveTypeProp f.pp_loc
+ in
+ let form, vars = type_pp_desc f.pp_desc in
+ {c = form; annot = new_id ()}, vars
+
+
+let make_rules loc f = match f.c with
+ | TFforall {qf_bvars = vars; qf_form = {c = TFatom {c = TAeq [t1; t2]}}} ->
+ {rwt_vars = vars; rwt_left = t1; rwt_right = t2}
+ | TFatom {c = TAeq [t1; t2]} ->
+ {rwt_vars = []; rwt_left = t1; rwt_right = t2}
+ | _ -> error SyntaxError loc
+
+
+let fresh_var =
+ let cpt = ref 0 in
+ fun x -> incr cpt; ("_"^x^(string_of_int !cpt))
+
+let rec alpha_renaming_b s f =
+ { f with pp_desc = alpha_rec s f.pp_desc }
+and alpha_rec ((up, m) as s) f =
+ match f with
+ | PPvar x ->
+ begin
+ try
+ let y = MString.find x m in
+ PPvar y
+ with Not_found -> f
+ end
+ | PPapp(k, l) ->
+ PPapp(k, List.map (alpha_renaming_b s) l)
+ | PPdistinct l ->
+ PPdistinct (List.map (alpha_renaming_b s) l)
+ | PPconst _ -> f
+ | PPinfix(f1, op, f2) ->
+ let ff1 = alpha_renaming_b s f1 in
+ let ff2 = alpha_renaming_b s f2 in
+ PPinfix(ff1, op, ff2)
+ | PPprefix(op, f1) ->
+ PPprefix(op, alpha_renaming_b s f1)
+ | PPget(f1,f2) ->
+ let ff1 = alpha_renaming_b s f1 in
+ let ff2 = alpha_renaming_b s f2 in
+ PPget(ff1, ff2)
+ | PPset(f1, f2, f3) ->
+ let ff1 = alpha_renaming_b s f1 in
+ let ff2 = alpha_renaming_b s f2 in
+ let ff3 = alpha_renaming_b s f3 in
+ PPset(ff1, ff2, ff3)
+ | PPextract(f1, f2, f3) ->
+ let ff1 = alpha_renaming_b s f1 in
+ let ff2 = alpha_renaming_b s f2 in
+ let ff3 = alpha_renaming_b s f3 in
+ PPextract(ff1, ff2, ff3)
+ | PPconcat(f1, f2) ->
+ let ff1 = alpha_renaming_b s f1 in
+ let ff2 = alpha_renaming_b s f2 in
+ PPconcat(ff1, ff2)
+ | PPif(f1, f2, f3) ->
+ let ff1 = alpha_renaming_b s f1 in
+ let ff2 = alpha_renaming_b s f2 in
+ let ff3 = alpha_renaming_b s f3 in
+ PPif(ff1, ff2, ff3)
+ | PPnamed(n, f1) ->
+ PPnamed(n, alpha_renaming_b s f1)
+ | PPforall(xs, ty, trs, f1) ->
+ let xs1, xs2 = List.partition (fun x -> S.mem x up) xs in
+ let nv = List.map fresh_var xs1 in
+ let m = List.fold_left2
+ (fun m x nx -> MString.add x nx m) m xs1 nv in
+ let xs = nv@xs2 in
+ let up = List.fold_left (fun up x -> S.add x up) up xs in
+ let s = (up, m) in
+ let ff1 = alpha_renaming_b s f1 in
+ let trs = List.map (List.map (alpha_renaming_b s)) trs in
+ PPforall(xs, ty, trs, ff1)
+ | PPforall_named (xs, ty, trs, f1) ->
+ let xs1, xs2 = List.partition (fun (x, _) -> S.mem x up) xs in
+ let nv = List.map (fun (x, lbl) -> fresh_var x, lbl) xs1 in
+ let m = List.fold_left2
+ (fun m (x,_) (nx, _) -> MString.add x nx m) m xs1 nv in
+ let xs = nv@xs2 in
+ let up = List.fold_left (fun up (x, _) -> S.add x up) up xs in
+ let s = (up, m) in
+ let ff1 = alpha_renaming_b s f1 in
+ let trs = List.map (List.map (alpha_renaming_b s)) trs in
+ PPforall_named (xs, ty, trs, ff1)
+ | PPdot(f1, a) ->
+ PPdot(alpha_renaming_b s f1, a)
+ | PPrecord l ->
+ PPrecord (List.map (fun (a,e) -> a, alpha_renaming_b s e) l)
+ | PPwith(e, l) ->
+ let l = List.map (fun (a,e) -> a, alpha_renaming_b s e) l in
+ PPwith(alpha_renaming_b s e, l)
+ | PPlet(x, f1, f2) ->
+ let ff1 = alpha_renaming_b s f1 in
+ let s, x =
+ if S.mem x up then
+ let nx = fresh_var x in
+ let m = MString.add x nx m in
+ let up = S.add nx up in
+ (up, m), nx
+ else
+ (S.add x up, m), x
+ in
+ let ff2 = alpha_renaming_b s f2 in
+ PPlet(x, ff1, ff2)
+
+ | PPexists(lx, ty, trs, f1) ->
+ let s, lx =
+ List.fold_left
+ (fun (s, lx) x ->
+ if S.mem x up then
+ let nx = fresh_var x in
+ let m = MString.add x nx m in
+ let up = S.add nx up in
+ (up, m), nx :: lx
+ else
+ (S.add x up, m), x :: lx)
+ (s, []) lx
+ in
+ let trs = List.map (List.map (alpha_renaming_b s)) trs in
+ let ff1 = alpha_renaming_b s f1 in
+ PPexists(lx, ty, trs, ff1)
+ | PPexists_named (lx, ty, trs, f1) ->
+ let s, lx =
+ List.fold_left
+ (fun (s, lx) (x, lbl) ->
+ if S.mem x up then
+ let nx = fresh_var x in
+ let m = MString.add x nx m in
+ let up = S.add nx up in
+ (up, m), (nx, lbl) :: lx
+ else
+ (S.add x up, m), (x, lbl) :: lx)
+ (s, []) lx
+ in
+ let ff1 = alpha_renaming_b s f1 in
+ let trs = List.map (List.map (alpha_renaming_b s)) trs in
+ PPexists_named (lx, ty, trs, ff1)
+ | PPcheck f' -> PPcheck (alpha_renaming_b s f')
+ | PPcut f' -> PPcut (alpha_renaming_b s f')
+ | PPcast (f',ty) -> PPcast (alpha_renaming_b s f',ty)
+
+let alpha_renaming = alpha_renaming_b (S.empty, MString.empty)
+
+
+let alpha_renaming_env env =
+ let up = MString.fold (fun s _ up -> S.add s up)
+ env.Env.logics S.empty in
+ let up = MString.fold (fun s _ up -> S.add s up) env.Env.var_map up in
+ alpha_renaming_b (up, MString.empty)
+
+
+let inv_infix = function
+ | PPand -> PPor | PPor -> PPand | _ -> assert false
+
+let rec elim_toplevel_forall env bnot f =
+ (* bnot = true : nombre impaire de not *)
+ match f.pp_desc with
+ | PPforall (lv, pp_ty, _, f) when bnot->
+ elim_toplevel_forall (Env.add_names env lv pp_ty f.pp_loc) bnot f
+
+ | PPforall_named (lvb, pp_ty, _, f) when bnot->
+ elim_toplevel_forall (Env.add_names_lbl env lvb pp_ty f.pp_loc) bnot f
+
+ | PPinfix (f1, PPand, f2) when not bnot ->
+ let f1 , env = elim_toplevel_forall env false f1 in
+ let f2 , env = elim_toplevel_forall env false
+ (alpha_renaming_env env f2) in
+ { f with pp_desc = PPinfix(f1, PPand , f2)}, env
+
+ | PPinfix (f1, PPor, f2) when bnot ->
+ let f1 , env = elim_toplevel_forall env true f1 in
+ let f2 , env = elim_toplevel_forall env true
+ (alpha_renaming_env env f2) in
+ { f with pp_desc = PPinfix(f1, PPand , f2)}, env
+
+ | PPinfix (f1, PPimplies, f2) when bnot ->
+ let f1 , env = elim_toplevel_forall env false f1 in
+ let f2 , env = elim_toplevel_forall env true
+ (alpha_renaming_env env f2) in
+ { f with pp_desc = PPinfix(f1,PPand,f2)}, env
+
+ | PPprefix (PPnot, f) -> elim_toplevel_forall env (not bnot) f
+
+
+ | _ when bnot ->
+ { f with pp_desc = PPprefix (PPnot, f) }, env
+
+ | _ -> f , env
+
+
+let rec intro_hypothesis env valid_mode f =
+ match f.pp_desc with
+ | PPinfix(f1,PPimplies,f2) when valid_mode ->
+ let ((f1, env) as f1_env) =
+ elim_toplevel_forall env (not valid_mode) f1 in
+ let axioms, goal = intro_hypothesis env valid_mode
+ (alpha_renaming_env env f2) in
+ f1_env::axioms, goal
+ | PPforall (lv, pp_ty, _, f) when valid_mode ->
+ intro_hypothesis (Env.add_names env lv pp_ty f.pp_loc) valid_mode f
+ | PPexists (lv, pp_ty, _, f) when not valid_mode->
+ intro_hypothesis (Env.add_names env lv pp_ty f.pp_loc) valid_mode f
+ | PPforall_named (lvb, pp_ty, _, f) when valid_mode ->
+ intro_hypothesis (Env.add_names_lbl env lvb pp_ty f.pp_loc) valid_mode f
+ | PPexists_named (lvb, pp_ty, _, f) when not valid_mode->
+ intro_hypothesis (Env.add_names_lbl env lvb pp_ty f.pp_loc) valid_mode f
+ | _ ->
+ let f_env = elim_toplevel_forall env valid_mode f in
+ [] , f_env
+
+let fresh_hypothesis_name =
+ let cpt = ref 0 in
+ fun sort ->
+ incr cpt;
+ match sort with
+ | Thm -> "@H"^(string_of_int !cpt)
+ | _ -> "@L"^(string_of_int !cpt)
+
+let fresh_check_name =
+ let cpt = ref 0 in fun () -> incr cpt; "check_"^(string_of_int !cpt)
+
+let fresh_cut_name =
+ let cpt = ref 0 in fun () -> incr cpt; "cut_"^(string_of_int !cpt)
+
+let check_duplicate_params l =
+ let rec loop l acc =
+ match l with
+ | [] -> ()
+ | (loc,x,_)::rem ->
+ if List.mem x acc then
+ error (ClashParam x) loc
+ else loop rem (x::acc)
+ in
+ loop l []
+
+let rec make_pred loc trs f = function
+ [] -> f
+ | [x,t] ->
+ { pp_desc = PPforall([x],t,trs,f) ; pp_loc = loc }
+ | (x,t)::l ->
+ { pp_desc = PPforall([x],t,[],(make_pred loc trs f l)) ;
+ pp_loc = loc }
+
+let rec max_terms acc f =
+ match f.pp_desc with
+ | PPinfix(f1, ( PPand | PPor | PPimplies | PPiff ), f2)
+ | PPconcat(f1, f2) ->
+ let acc = max_terms acc f1 in
+ max_terms acc f2
+
+ | PPforall(_, _, _, _)
+ | PPexists(_, _, _, _)
+ | PPforall_named(_, _, _, _)
+ | PPexists_named(_, _, _, _)
+ | PPvar _
+ | PPlet(_, _, _)
+ | PPinfix(_, _, _) -> raise Exit
+
+ | PPif(f1, f2, f3) ->
+ let acc = max_terms acc f1 in
+ let acc = max_terms acc f2 in
+ max_terms acc f3
+ | PPextract(f1, _, _) | PPprefix(_, f1)
+ | PPnamed(_, f1) ->
+ max_terms acc f1
+ | _ -> f::acc
+
+let max_terms f = try max_terms [] f with Exit -> []
+
+let rec mono_term {c = {tt_ty=tt_ty; tt_desc=tt_desc}; annot = id} =
+ let tt_desc = match tt_desc with
+ | TTconst _ | TTvar _ ->
+ tt_desc
+ | TTinfix (t1, sy, t2) ->
+ TTinfix(mono_term t1, sy, mono_term t2)
+ | TTprefix (sy,t) ->
+ TTprefix(sy, mono_term t)
+ | TTapp (sy,tl) ->
+ TTapp (sy, List.map mono_term tl)
+ | TTget (t1,t2) ->
+ TTget (mono_term t1, mono_term t2)
+ | TTset (t1,t2,t3) ->
+ TTset(mono_term t1, mono_term t2, mono_term t3)
+ | TTextract (t1,t2,t3) ->
+ TTextract(mono_term t1, mono_term t2, mono_term t3)
+ | TTconcat (t1,t2)->
+ TTconcat (mono_term t1, mono_term t2)
+ | TTdot (t1, a) ->
+ TTdot (mono_term t1, a)
+ | TTrecord lbs ->
+ TTrecord (List.map (fun (x, t) -> x, mono_term t) lbs)
+ | TTlet (sy,t1,t2)->
+ TTlet (sy, mono_term t1, mono_term t2)
+ | TTnamed (lbl, t)->
+ TTnamed (lbl, mono_term t)
+ in
+ { c = {tt_ty = Ty.monomorphize tt_ty; tt_desc=tt_desc}; annot = id}
+
+
+let monomorphize_atom tat =
+ let c = match tat.c with
+ | TAtrue | TAfalse -> tat.c
+ | TAeq tl -> TAeq (List.map mono_term tl)
+ | TAneq tl -> TAneq (List.map mono_term tl)
+ | TAle tl -> TAle (List.map mono_term tl)
+ | TAlt tl -> TAlt (List.map mono_term tl)
+ | TAdistinct tl -> TAdistinct (List.map mono_term tl)
+ | TApred t -> TApred (mono_term t)
+ | TAbuilt (hs, tl) -> TAbuilt(hs, List.map mono_term tl)
+ in
+ { tat with c = c }
+
+let monomorphize_var (s,ty) = s, Ty.monomorphize ty
+
+let rec monomorphize_form tf =
+ let c = match tf.c with
+ | TFatom tat -> TFatom (monomorphize_atom tat)
+ | TFop (oplogic , tfl) ->
+ TFop(oplogic, List.map monomorphize_form tfl)
+ | TFforall qf ->
+ TFforall
+ { qf_bvars = List.map monomorphize_var qf.qf_bvars;
+ qf_upvars = List.map monomorphize_var qf.qf_upvars;
+ qf_form = monomorphize_form qf.qf_form;
+ qf_triggers = List.map (List.map mono_term) qf.qf_triggers}
+ | TFexists qf ->
+ TFexists
+ { qf_bvars = List.map monomorphize_var qf.qf_bvars;
+ qf_upvars = List.map monomorphize_var qf.qf_upvars;
+ qf_form = monomorphize_form qf.qf_form;
+ qf_triggers = List.map (List.map mono_term) qf.qf_triggers}
+ | TFlet (l, sy, tt, tf) ->
+ let l = List.map monomorphize_var l in
+ TFlet(l,sy, mono_term tt, monomorphize_form tf)
+ | TFnamed (hs,tf) ->
+ TFnamed(hs, monomorphize_form tf)
+ in
+ { tf with c = c }
+
+let axioms_of_rules keep_triggers loc name lf acc env =
+ let acc =
+ List.fold_left
+ (fun acc (f, _) ->
+ let f = Triggers.make keep_triggers false f in
+ let name = (Common.fresh_string ()) ^ "_" ^ name in
+ let td = {c = TAxiom(loc,name,false,f); annot = new_id () } in
+ (td, env)::acc
+ ) acc lf
+ in
+ acc, env
+
+
+
+let type_hypothesis keep_triggers acc env_f loc sort f =
+ let f,_ = type_form env_f f in
+ let f = monomorphize_form f in
+ let f = Triggers.make keep_triggers false f in
+ let td =
+ {c = TAxiom(loc, fresh_hypothesis_name sort, false,f);
+ annot = new_id () } in
+ (td, env_f)::acc
+
+
+let type_goal keep_triggers acc env_g loc sort n goal =
+ let goal, _ = type_form env_g goal in
+ let goal = monomorphize_form goal in
+ let goal = Triggers.make keep_triggers true goal in
+ let td = {c = TGoal(loc, sort, n, goal); annot = new_id () } in
+ (td, env_g)::acc
+
+
+let rec type_and_intro_goal keep_triggers acc env loc sort n f =
+ let axioms, (goal, env_g) =
+ intro_hypothesis env (not (!smtfile or !smt2file or !satmode)) f in
+ let acc =
+ List.fold_left
+ (fun acc (f, env_f) -> match f.pp_desc with
+ | PPcut f ->
+ let acc = type_and_intro_goal keep_triggers acc env_f
+ loc Cut (fresh_cut_name ()) f in
+ type_hypothesis keep_triggers acc env_f loc sort f
+
+ | PPcheck f ->
+ type_and_intro_goal keep_triggers acc env_f
+ loc Check (fresh_check_name ()) f
+
+ | _ ->
+ type_hypothesis keep_triggers acc env_f loc sort f
+ ) acc axioms
+ in
+ type_goal keep_triggers acc env_g loc sort n goal
+
+
+let type_decl keep_triggers (acc, env) d =
+ Types.to_tyvars := MString.empty;
+ try
+ match d with
+ | Logic (loc, ac, lp, pp_ty) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-LogicFun$_F$@.";
+ let env' = Env.add_logics env ac lp pp_ty loc in
+ let lp = List.map fst lp in
+ let td = {c = TLogic(loc,lp,pp_ty); annot = new_id () } in
+ (td, env)::acc, env'
+
+ | Axiom(loc,name,inv,f) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-AxiomDecl$_F$@.";
+ let f, _ = type_form env f in
+ let f = Triggers.make keep_triggers false f in
+ let td = {c = TAxiom(loc,name,inv,f); annot = new_id () } in
+ (td, env)::acc, env
+
+ | Rewriting(loc, name, lr) ->
+ let lf = List.map (type_form env) lr in
+ if Options.rewriting () then
+ let rules = List.map (fun (f,_) -> make_rules loc f) lf in
+ let td = {c = TRewriting(loc, name, rules); annot = new_id () } in
+ (td, env)::acc, env
+ else
+ axioms_of_rules keep_triggers loc name lf acc env
+
+
+ | Goal(loc, n, f) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-GoalDecl$_F$@.";
+ (*let f = move_up f in*)
+ let f = alpha_renaming_env env f in
+ type_and_intro_goal keep_triggers acc env loc Thm n f, env
+
+ | Predicate_def(loc,n,l,e)
+ | Function_def(loc,n,l,_,e) ->
+ check_duplicate_params l;
+ let ty =
+ let l = List.map (fun (_,_,x) -> x) l in
+ match d with
+ Function_def(_,_,_,t,_) -> PFunction(l,t)
+ | _ -> PPredicate l
+ in
+ let l = List.map (fun (_,x,t) -> (x,t)) l in
+
+ let env = Env.add_logics env Symbols.Other [n] ty loc in (* TODO *)
+
+ let n = fst n in
+
+ let lvar = List.map (fun (x,_) -> {pp_desc=PPvar x;pp_loc=loc}) l in
+ let p = {pp_desc=PPapp(n,lvar) ; pp_loc=loc } in
+ let infix = match d with Function_def _ -> PPeq | _ -> PPiff in
+ let f = { pp_desc = PPinfix(p,infix,e) ; pp_loc = loc } in
+ (* le trigger [[p]] ne permet pas de replier la definition,
+ donc on calcule les termes maximaux de la definition pour
+ laisser une possibilite de replier *)
+ let trs = max_terms e in
+ let f = make_pred loc ([p]::[trs]) f l in
+ let f,_ = type_form env f in
+ let f = Triggers.make keep_triggers false f in
+ let td =
+ match d with
+ | Function_def(_,_,_,t,_) ->
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-LogicFun$_F$@.";
+ TFunction_def(loc,n,l,t,f)
+ | _ ->
+ if rules () = 1 then
+ fprintf fmt "[rule] TR-Typing-LogicPred$_F$@.";
+ TPredicate_def(loc,n,l,f)
+ in
+ let td_a = { c = td; annot=new_id () } in
+ (td_a, env)::acc, env
+
+ | TypeDecl(loc, ls, s, body) ->
+ if rules () = 1 then fprintf fmt "[rule] TR-Typing-TypeDecl$_F$@.";
+ let env1 = Env.add_type_decl env ls s body loc in
+ let td1 = TTypeDecl(loc, ls, s, body) in
+ let td1_a = { c = td1; annot=new_id () } in
+ let tls = List.map (fun s -> PPTvarid (s,loc)) ls in
+ let ty = PFunction([], PPTexternal(tls, s, loc)) in
+ match body with
+ | Enum lc ->
+ let lcl = List.map (fun c -> c, "") lc in (* TODO change this *)
+ let env2 = Env.add_logics env1 Symbols.Constructor lcl ty loc in
+ let td2 = TLogic(loc, lc, ty) in
+ let td2_a = { c = td2; annot=new_id () } in
+ (td1_a, env1)::(td2_a,env2)::acc, env2
+ | _ -> (td1_a, env1)::acc, env1
+
+ with Warning(e,loc) ->
+ Loc.report std_formatter loc;
+ acc, env
+
+let file keep_triggers env ld =
+ let ltd, env =
+ List.fold_left
+ (fun acc d -> type_decl keep_triggers acc d)
+ ([], env) ld
+ in
+ List.rev ltd, env
+
+let is_local_hyp s =
+ try String.sub s 0 2 = "@L" with Invalid_argument _ -> false
+
+let is_global_hyp s =
+ try String.sub s 0 2 = "@H" with Invalid_argument _ -> false
+
+let split_goals l =
+ let _, _, _, ret =
+ List.fold_left
+ (fun (ctx, global_hyp, local_hyp, ret) ( (td, env) as x) ->
+ match td.c with
+ | TGoal (_, (Check | Cut), _, _) ->
+ ctx, global_hyp, [], (x::(local_hyp@global_hyp@ctx))::ret
+
+ | TGoal (_, _, _, _) ->
+ ctx, [], [], (x::(local_hyp@global_hyp@ctx))::ret
+
+ | TAxiom (_, s, _, _) when is_global_hyp s ->
+ ctx, x::global_hyp, local_hyp, ret
+
+ | TAxiom (_, s, _, _) when is_local_hyp s ->
+ ctx, global_hyp, x::local_hyp, ret
+
+ | _ -> x::ctx, global_hyp, local_hyp, ret
+ ) ([],[],[],[]) l
+ in
+ List.rev_map List.rev ret
+
+let term env vars t =
+ let vmap =
+ List.fold_left
+ (fun m (s,ty)->
+ let str = Symbols.to_string s in
+ MString.add str (s,ty) m
+ ) env.Env.var_map vars in
+ let env = { env with Env.var_map = vmap } in
+ type_term env t
+
+type env = Env.t
+
+let empty_env = Env.empty
diff --git a/src/inputlang/altergo/why_typing.mli b/src/inputlang/altergo/why_typing.mli
new file mode 100644
index 000000000..9e1b8c91f
--- /dev/null
+++ b/src/inputlang/altergo/why_typing.mli
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(* *)
+(* The Alt-Ergo theorem prover *)
+(* Copyright (C) 2006-2011 *)
+(* *)
+(* Sylvain Conchon *)
+(* Evelyne Contejean *)
+(* *)
+(* Francois Bobot *)
+(* Mohamed Iguernelala *)
+(* Stephane Lescuyer *)
+(* Alain Mebsout *)
+(* *)
+(* CNRS - INRIA - Universite Paris Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+open Why_ptree
+
+type env
+
+val empty_env : env
+
+val file : bool -> env -> file ->
+ ((int tdecl, int) annoted * env) list * env
+
+val split_goals :
+ ((int tdecl, int) annoted * env) list ->
+ ((int tdecl, int) annoted * env) list list
+
+val term : env -> (Symbols.t * Ty.t) list -> Why_ptree.lexpr ->
+ (int tterm, int) annoted
+
+val new_id : unit -> int
diff --git a/src/uninterp.mli b/src/uninterp.mli
index c7fd996ae..e4e80fd8d 100644
--- a/src/uninterp.mli
+++ b/src/uninterp.mli
@@ -32,6 +32,7 @@ type env = UnionFind.t
val cst: env -> string -> cl * env
val app: env -> cl -> cl -> cl * env
+val appl: env -> cl -> cl list -> cl * env
val fun1 : env -> string -> (env -> cl -> cl * env) * env
val fun2 : env -> string -> (env -> cl -> cl -> cl * env) * env
diff --git a/src/util/exn_printer.ml b/src/util/exn_printer.ml
index 1b3460e8e..4c68203cb 100644
--- a/src/util/exn_printer.ml
+++ b/src/util/exn_printer.ml
@@ -14,7 +14,7 @@ type exn_printer = Format.formatter -> exn -> unit
let exn_printers =
(Stack.create () : (Format.formatter -> exn -> unit) Stack.t)
-let register exn_printer = Stack.push exn_printer exn_printers;
+let register exn_printer = Stack.push exn_printer exn_printers
exception Exit_loop
@@ -32,5 +32,29 @@ let exn_printer fmt exn =
raise exn
with Exit_loop -> ()
+
+let exn_printer fmt exn =
+ let test f =
+ try
+ Format.fprintf fmt "@[%a@]" f exn;
+ raise Exit_loop
+ with
+ | Exit_loop -> raise Exit_loop
+ | _ -> ()
+ in
+ try
+ Stack.iter test exn_printers;
+ raise exn
+ with Exit_loop -> ()
+
+
let () =
Printexc.register_printer (fun exn -> Some (Pp.string_of exn_printer exn))
+
+
+(** usual version *)
+let exn_printer fmt exn =
+ try
+ exn_printer fmt exn
+ with e ->
+ Format.fprintf fmt "anomaly: %s" (Printexc.to_string exn)
diff --git a/src/util/extmap.ml b/src/util/extmap.ml
index 0aae9c9c0..fd6c00abe 100644
--- a/src/util/extmap.ml
+++ b/src/util/extmap.ml
@@ -499,8 +499,6 @@ struct
let (l1, d1, r1) = split v2 s1 in
concat_or_join (union_merge f l1 l2) v2 (f v2 d1 d2)
(union_merge f r1 r2)
- | _ ->
- assert false
let rec inter f s1 s2 =
diff --git a/src/util/loc.ml b/src/util/loc.ml
index e6accedb6..bcf05235e 100644
--- a/src/util/loc.ml
+++ b/src/util/loc.ml
@@ -117,3 +117,8 @@ let () = Exn_printer.register
| _ ->
raise exn)
+let () = Exn_printer.register
+ (fun fmt exn -> match exn with
+ | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
+ | _ -> raise exn)
+
diff --git a/src/util/strings.ml b/src/util/strings.ml
index 2192f805b..fd554af62 100644
--- a/src/util/strings.ml
+++ b/src/util/strings.ml
@@ -57,9 +57,16 @@ module Hashcons = struct
Hint.add hi i s;
i
+ let view i = Hint.find hi i
+
let print fmt i =
try
- Format.pp_print_string fmt (Hint.find hi i)
+ Format.pp_print_string fmt (view i)
with Not_found -> Format.fprintf fmt "<unknown %i>" i
+ let compare (x:t) y = Pervasives.compare x y
+ let equal (x:t) y = x = y
+ let hash (x:t) = x
+ let tag = hash
+
end
diff --git a/src/util/strings.mli b/src/util/strings.mli
index b704653e3..e707cfeeb 100644
--- a/src/util/strings.mli
+++ b/src/util/strings.mli
@@ -21,6 +21,9 @@ val pad_right : char -> string -> int -> string
module Hashcons : sig
type t = private int
+ include Stdlib.OrderedHashedType with type t := t
val make: string -> t
+ val view: t -> string
+ val tag: t -> int
val print: Format.formatter -> t -> unit
end
diff --git a/tests/tests.ml b/tests/tests.ml
index c35ce61f5..23560f0b4 100644
--- a/tests/tests.ml
+++ b/tests/tests.ml
@@ -14,9 +14,9 @@ let print_seed fmt = function
let rec make_tests acc seed =
let module Uf = Tests_uf.Tests(Egraph_simple) in
let module Arith = Tests_arith.Tests(Egraph_simple) in
- let module Arith = Tests_arith_uninterp.Tests(Egraph_simple) in
+ let module UfArith = Tests_arith_uninterp.Tests(Egraph_simple) in
let test = ((Pp.sprintf "seed %a" print_seed seed) >:::
- [Uf.tests;Arith.tests]) in
+ [Uf.tests;Arith.tests;UfArith.tests]) in
let test = test_decorate
(fun f -> (fun () -> Shuffle.set_shuffle seed; f ())) test in
test::acc
@@ -26,7 +26,7 @@ let tests () =
(!opt_seed + 1) (!opt_seed + 9)in
make_tests l None
-let tests =
+let tests () =
(* test_decorate
(fun f ->
if Printexc.backtrace_status ()
@@ -34,7 +34,7 @@ let tests =
raise exn
else f
) *)
- lazy (TestList (tests ()))
+ TestList (tests ())
(** From oUnit.ml v 1.2.2 *)
(** just need to make the tests lazily computed *)
@@ -70,7 +70,7 @@ let run_test_tt_main ?(arg_specs=[]) suite =
List.iter
(fun pth ->
print_endline (string_of_path pth))
- (test_case_paths (Lazy.force suite));
+ (test_case_paths (suite ()));
exit 0),
" List tests";
] @ arg_specs
@@ -82,10 +82,10 @@ let run_test_tt_main ?(arg_specs=[]) suite =
let verbose = Debug.test_flag debug in
let nsuite =
if !only_test = [] then
- Lazy.force suite
+ suite ()
else
begin
- match test_filter ~skip:true !only_test (Lazy.force suite) with
+ match test_filter ~skip:true !only_test (suite ()) with
| Some test ->
test
| None ->
@@ -103,9 +103,14 @@ let run_test_tt_main ?(arg_specs=[]) suite =
(*** End *)
let _ =
- run_test_tt_main
- ~arg_specs:["--seed",Arg.Set_int opt_seed,
- " Base seed used for shuffling the arbitrary decision";
- Debug.Args.desc_debug;
- Debug.Args.desc_debug_all]
- tests
+ try
+ run_test_tt_main
+ ~arg_specs:["--seed",Arg.Set_int opt_seed,
+ " Base seed used for shuffling the arbitrary decision";
+ Debug.Args.desc_debug;
+ Debug.Args.desc_debug_all]
+ tests
+ with e when not (Debug.test_flag Debug.stack_trace) ->
+ Format.eprintf "%a@." Exn_printer.exn_printer e;
+ exit 1
+
diff --git a/tests/tests_altergo_arith.split b/tests/tests_altergo_arith.split
new file mode 100644
index 000000000..b31ebc602
--- /dev/null
+++ b/tests/tests_altergo_arith.split
@@ -0,0 +1,1960 @@
+(*
+$$$arith
+$cobj:La fonctionnalité à vérifier est que Alt-Ergo est capable de prouver des buts d'arithmétique linéaire en utilisant la procédure de décision de Fourier Motzkin ou le solveur Oméga.
+*)
+
+(*deactivated
+(* status: Valid *)
+goal g1: forall x:int. x<=x
+*)
+
+(* status: Valid *)
+goal g2: forall x:int. x-x = 0
+
+(*deactivated
+(* status: Valid *)
+goal g3: forall x:int. 0<=x -> 0=x-x and 0<=x and x<=x
+
+(* status: Valid *)
+goal g4: forall x,y,z:int. x<=y and y+z<=x and 0<=z -> x=y
+
+(* status: Valid *)
+logic P:prop
+goal g5: forall x:int. x=10 and (3<x -> P) -> P
+
+(* status: Valid *)
+logic f: int -> int
+goal g6: forall x,y:int. x+1=y -> f(x+2)=f(y+1)
+
+(* status: Valid *)
+logic Q:int -> prop
+goal g7: forall x,y:int. Q(y) -> (y<=x and x<=y) -> Q(x)
+
+(* status: Valid *)
+logic f: int -> int
+goal g8:
+ forall x,y,u,v,z:int.
+ u=v and u<=x+y and x+y<=u and v<=z+x+4 and z+x+4<=v -> f(x+y) = f(z+x+4)
+
+(* status: Valid *)
+logic f: int -> int
+goal g9: forall x:int. f(x) = x -> f(2*x - f(x)) = x
+
+(* status: Valid *)
+logic f : int -> 'a
+goal g10:
+ forall x,z:int.
+ forall u,t:'a.
+ f(x+3)=u and f(z+2)=t and x=z-1 -> u=t
+
+(* status: Valid *)
+logic f : int -> 'a
+goal g11:
+ forall x,y,z:int.
+ forall u,t:'a.
+ x=y-1 and f(x)=u and z=2 and f(z)=t and y=3 -> u=t
+
+(* status: Valid *)
+goal g12:forall x,z,v,u:int. v<=z+4 and u<=v+2 and z+6<=u -> u+v=z+u+4
+
+(* status: Valid *)
+logic P:prop
+goal g13: 1=2 -> P
+
+(* status: Valid *)
+goal g14: forall x,y:int. x=y-1 and y=2 -> x=1
+
+(* status: Valid *)
+goal g15: forall x:int. x<0 -> -x >=0
+
+(* status: Valid *)
+logic p,q : int -> prop
+goal g16 :
+ (forall k:int. 0 <= k <= 10 -> p(k)) ->
+ p(11) ->
+ forall k:int. 0 <= k <= 11 -> p(k)
+
+(* status: Valid *)
+logic p,q : int -> prop
+goal g17 :
+ (forall k:int. 0 <= k <= 10 -> (p(k) and q(k))) ->
+ p(11) -> q(11) ->
+ forall k:int. 0 <= k <= 11 -> (p(k) and q(k))
+
+(* status: Valid *)
+logic p,q : int -> prop
+goal g18 :
+ (forall k:int. 0 <= k <= 10 -> p(k) -> q(k)) ->
+ (p(11) -> q(11)) ->
+ forall k:int. 0 <= k <= 11 -> p(k) -> q(k)
+
+(* status: Valid *)
+logic p,q : int -> prop
+logic a,b : int
+
+goal g19 :
+ (forall k:int. a <= k <= b -> p(k)) ->
+ p(b+1) ->
+ forall k:int. a <= k <= b+1 -> p(k)
+
+(* status: Valid *)
+logic p,q : int -> prop
+logic a,b : int
+
+goal g20 :
+ (forall k:int. a <= k <= b -> (p(k) and q(k))) ->
+ p(b+1) -> q(b+1) ->
+ forall k:int. a <= k <= b+1 -> (p(k) and q(k))
+
+(* status: Valid *)
+goal g21:
+ forall size:int. (0 <= size) -> (size <= size) and (0 = (size - size))
+
+
+(* status: Valid *)
+
+logic f : int -> int
+logic t,u,x,y,z : int
+
+goal g22:t=f(0) -> u=f(4*x+5*y-3*z-3) -> 8*x+10*y=6*z+6 -> t=u
+
+
+(* status: Valid *)
+goal g23: forall x:int. x*x>=0 -> 1=1
+
+
+(* status: Valid *)
+goal g24: forall x:int. (2+4)*x = (1+1)*x + (2*3)*x -(3-2)*x + (1*x)*(3-4)
+
+(* status: Valid *)
+logic a:int
+
+goal g25: a=0 -> 0<=a-1 -> false
+
+
+(* status: Valid *)
+goal g26: forall i0:int.(i0 <= 7) -> (i0 <> 6) -> (i0 >= 6) -> i0 = 7
+
+
+(* status: Valid *)
+logic f:int ->int
+
+goal g27:
+ forall n:int.
+ forall count:int.
+ forall sum:int.
+ sum = (f(count) * f(count)) ->
+ (sum <= n) ->
+ forall count0:int.
+ (count0 = f(count)) ->
+ (n >= count0 * count0)
+
+(* status: Valid *)
+logic q : int
+logic p : int
+logic b : int
+logic a : int
+
+axiom a1: forall x:int. x*0 = 0
+axiom a2: forall x:int. 0*x = 0
+
+axiom x9 : q = a
+axiom x10 : p = 0
+goal g28 : a = p * b + q
+*)
+(* status: Valid *)
+
+logic f : int -> int
+logic u,t,x : int
+
+goal g29: u=f(0) -> t=f(x) -> x=0 -> u=t
+
+
+(* status: Valid *)
+
+goal g30: forall x:int. x = 3*x+4 -> x = -2
+
+
+(*deactivated
+(* status: Valid *)
+type 't pointer
+
+type ('t, 'v) memory
+
+logic select : ('a2, 'a1) memory, 'a2 pointer -> 'a1
+
+logic store : ('a1, 'a2) memory, 'a1 pointer, 'a2 -> ('a1, 'a2) memory
+
+axiom select_store_eq:
+ (forall m:('a1, 'a2) memory.
+ (forall p1:'a1 pointer.
+ (forall p2:'a1 pointer.
+ (forall a:'a2 [store(m, p1, a), p2].
+ ((p1 = p2) -> (select(store(m, p1, a), p2) = a))))))
+
+axiom select_store_neq:
+ (forall m:('a1, 'a2) memory.
+ (forall p1:'a1 pointer.
+ (forall p2:'a1 pointer.
+ (forall a:'a2 [store(m, p1, a), p2].
+ ((p1 <> p2) -> (select(store(m, p1, a), p2) = select(m, p2)))))))
+
+type int32
+
+logic f : int32 -> int
+
+type int_P
+
+logic aa:int
+
+goal f_ensures_default_po_1:
+ forall p:int_P pointer.
+ forall m1:(int_P, int32) memory.
+ forall result:int32.
+ f(result) = 1 ->
+ forall m2:(int_P, int32) memory.
+ m2 = store(m1, p, result) ->
+ f(select(m2, p)) = 1
+
+
+(* status: Valid *)
+
+goal g30_1: forall x:int. x<>1 and 1 <= x and x <= 2 -> x=2
+
+
+(* status: Valid *)
+
+goal g30_2 : forall x:int. 0 <= x <= 1 -> x=0 or x=1
+
+
+(* status: Valid *)
+
+goal g30_3 : forall x:int. 0 <= x <= 1 -> (x = 0 or x = 1)
+
+
+(* status: Valid *)
+
+logic p,q : int -> prop
+
+goal g30_4 :
+ (forall k:int. 0 <= k <= 10 -> p(k)) ->
+ p(11) ->
+ forall k:int. 0 <= k <= 11 -> p(k)
+
+
+(* status: Valid *)
+
+logic f : int -> int
+
+logic x:int
+
+goal g30_5 :
+ f(x) <> f(30) ->
+ f(x) <> f(31) ->
+ 2 <= x ->
+ f(x) <> f(32) ->
+ f(x) <> f(33) ->
+ f(x) <> f(100) ->
+ f(x) <> f(0) ->
+ 2 <= x <= 29
+ or
+ 34 <= x <= 99
+ or
+ 101 <= x
+
+
+(* status: Valid *)
+
+logic P,Q : int -> prop
+axiom a1: forall x:int. x <= 1 -> Q(x)
+axiom a2: forall x:int. P(x) -> Q(x)
+axiom a3: forall x:int. x >= 6 -> P(x)
+axiom a4: P(5)
+axiom a6: P(4)
+axiom a7: Q(2)
+axiom a8: Q(3)
+
+goal g31 : forall x:int. 0 <= x <= 7 -> Q(x)
+
+
+(* status: Valid *)
+goal g32: forall x:real. -1. <= x <= 1. -> (x< -1. or x> 1.) -> false
+*)
+
+(*
+$$$ac_arith
+$cobj:La fonctionnalité à vérifier est que Alt-Ergo est capable de prouver des buts faisant intervenir des symboles associatifs commutatifs qui sont traités par l'algorithme AC(X) modulo la théorie de l'arithmétique.
+*)
+(*deactivated
+(* status: Valid *)
+logic ac f : int,int -> int
+goal g1 : forall a,b,c,x:int. c = a + x -> a = f(c,b) -> x=1 -> f(c,b)=c-1
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g2 :
+ a = b ->
+ f(a+1,a) = f(a,b+1)
+
+
+(* status: Valid *)
+logic a,b,c,x,beta,gamma,d:int
+
+logic ac f : int,int -> int
+
+goal g3 :
+ f((f(a,b) + x),c) = gamma ->
+ x = 0 ->
+ f(a,c) = a ->
+ f(a,d) = beta ->
+ f(b,beta) = f(d,gamma)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+goal g4 : forall a,b,c,x:int. c = a + x -> a = f(c,b) -> x=0 -> f(c,b)=c
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g5 :
+ a = b ->
+ f(a+1,a) = f(a,b+1)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g6 :
+ a = b ->
+ f(a+1,a) = f(a+1,b)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g7 :
+ a + 1 = b ->
+ f(a+1,a) = f(a,b)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g8 :
+ a + 1 = b + x ->
+ x = 1 ->
+ f(a,a) = f(a,b)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g9 : a = b -> b = a
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g10 :
+ f(a,a) = a ->
+ a = b ->
+ f(a,b) + a =a + b
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g11 :
+ a = b ->
+ f(a+1,a+2) = f(a+1,b+2)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g12 :
+ a + 1 = b + 2 ->
+ f(a,a-1) = f(a,b)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g13 :
+ 2 * a = 3 * b ->
+ f(x,2 * a) = f(3 * b,x)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:real
+logic ac f : real,real -> real
+goal g14 :
+ 2. * a = 3. * b ->
+ f(x,2./3. * a) = f(b,x)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g15 :
+ f(a,a) = a ->
+ a = b ->
+ f(a,b) + a =a + b
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,x,y:int
+
+goal g16:
+ f(a,b) + x = b ->
+ x = 0 ->
+ f(a,f(b,y)) = f(b,y)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g17:
+ f(a,b) = gamma ->
+ x = 0 ->
+ f(a,c) = beta + x ->
+ f(c,gamma) = f(b,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g18:
+ f(a,b) = gamma + x ->
+ x = 0 ->
+ f(a,c) = beta + x ->
+ f(c,gamma) = f(b,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g19:
+ f(a,b) = gamma ->
+ f(a,c) = beta + x ->
+ x = 0 ->
+ f(c,gamma) = f(b,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g20:
+ f(a,b) = gamma + x ->
+ f(a,c) = beta + x ->
+ x = 0 ->
+ f(c,gamma) = f(b,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g21:
+ f(a,b) = gamma + x ->
+ f(a,c) = beta ->
+ x = 0 ->
+ f(c,gamma) = f(b,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g22:
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ x = 0 ->
+ f(c,x + gamma) = f(b,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+(* axiome special pour corriger le pb de matching AC *)
+axiom neutre : forall u,v:int. f(u,f(v,0))= f(u,v)
+
+goal g23:
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ x = 0 ->
+ f(c,gamma) = f(f(b,x),beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g24:
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ x = 0 ->
+ f(c,gamma) = f(b + x,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g25:
+ x = 0 ->
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(c,x + gamma) = f(b,beta)
+
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,x : int
+logic ac f : int,int -> int
+
+goal g26 :
+ f(a,b+x) = gamma ->
+ f(a,c) = beta ->
+ x = 1 ->
+ f(b + 1,beta) = f(c,gamma)
+
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,x : int
+logic ac f : int,int -> int
+
+goal g27 :
+ f(a,b+x) = gamma ->
+ f(a,c) = beta ->
+ x = 0 ->
+ f(b,beta) = f(c,gamma)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,u,v,w,x:int
+
+goal g28 :
+ x = 0 ->
+ f(a,b) + x = u ->
+ f(a,c) = w ->
+ f(u,c) = f(w,b)
+
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,x : int
+logic ac f : int,int -> int
+
+goal g29 :
+ f(b,a) = f(b+x,f(a+x,a+x)) ->
+ x = 1 ->
+ f(b,c) = beta ->
+ f(b+1,f(a+1, f(a+1, c))) = f(a,beta)
+
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,x : int
+logic ac f : int,int -> int
+
+goal g30 :
+ f(b,a) = f(b+x,f(a+x,a+x)) ->
+ f(b,c) = beta ->
+ x = 1 ->
+ f(b + 1,f(a + 1, f(a + 1, c))) = f(a,beta)
+
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,x : int
+logic ac f : int,int -> int
+
+goal g31 :
+ x = 1 ->
+ f(b,a) = f(b+x,f(a+x,a+x)) ->
+ f(b,c) = beta ->
+ f(b + 1,f(a + 1, f(a + 1, c))) = f(a,beta)
+
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,x : int
+logic ac f : int,int -> int
+
+goal g32 :
+ x = 2 ->
+ f(a,b) = f(a,f(b,c)) ->
+ f(a,f(b,gamma)) = f(a,f(b,f(c,gamma)))
+
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,x : int
+logic ac f : int,int -> int
+
+goal g33 :
+ x = 1 ->
+ f(a,b) = f(b+x,f(a+x,a+x)) ->
+ f(b + 1,f(a + 1, f(a + 1, c))) = f(b,f(a,c))
+
+$
+
+logic a,b,c, beta,gamma,x : int
+logic ac f : int,int -> int
+
+goal g34 :
+ x = 1 ->
+ f(a,b+x) = gamma ->
+ f(a,c) = beta ->
+ f(gamma,c) = f(beta, b + 1)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,u,v,w,x,y:int
+
+goal g35 :
+ x = 0 ->
+ f(a,b) = u ->
+ f(a,b) + x = v + y ->
+ f(a,c)=w ->
+ f(v+y,c) = f(w,b)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,u,v,w,x:int
+
+goal g36 :
+ x = 0 ->
+ f(a,b) = u ->
+ f(a,b) + x = v ->
+ f(a,c)=w ->
+ f(v,c) = f(w,b)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,u,v,w,x:int
+
+goal g37:
+ f(a,c) = w ->
+ f(a,b) + x = v ->
+ x = 0 ->
+ f(v,c) = f(w,b)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,u,v,w,x:int
+
+goal g38:
+ f(a,b) = u -> (* ne sert pas! juste une pollution*)
+ f(a,b) + x = v ->
+ x = 0 ->
+ f(a,c) = w ->
+ f(v,c) = f(w,b)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,u,v,w,x:int
+
+goal g39:
+ f(a,b) = u ->
+ x = 0 ->
+ f(a,b) + x = v ->
+ f(a,c) = w ->
+ f(v,c) = f(w,b)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g40:
+ x = 0 ->
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(c,gamma) = f(b + x,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g41:
+ x = 0 ->
+ f(a,b) = gamma + x ->
+ f(a,c) = beta + x ->
+ f(c,gamma) = f(b,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,gamma,beta,x:int
+
+goal g42:
+ f(a,b) = gamma + x ->
+ x = 0 ->
+ f(a,c) = beta ->
+ f(c,gamma) = f(b,beta)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,u,v,w,x:int
+
+goal g43:
+ f(a,c) = w ->
+ f(a,b) + x = b ->
+ x = 0 ->
+ f(b,c) = f(w,b)
+
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,u,v,w,x:int
+
+goal g44:
+ b = v ->
+ f(a,c) = w ->
+ f(a,b) + x = v ->
+ x = 0 ->
+ f(v,c) = f(w,b)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y,t:int
+logic ac f,g : int,int -> int
+
+goal g45 :
+ f(a+1,b) = gamma ->
+ f(a+t,c) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduit *)
+ g(f(gamma,c),d) = x ->
+ g(f(beta,b),e) = y ->
+ t = 1 ->
+ g(x,e) = g(y,d)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y,t:int
+logic ac f,g : int,int -> int
+
+goal g46 :
+ f(a+1,b) = gamma ->
+ f(a+t,c) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduit *)
+ g(f(gamma,c),d) = x ->
+ t = 1 ->
+ g(f(beta,b),e) = y ->
+ g(x,e) = g(y,d)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y,t:int
+logic ac f,g : int,int -> int
+
+goal g47 :
+ f(a+t,b) = gamma ->
+ f(a+t,c) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduit *)
+ g(f(gamma,c),d) = x ->
+ t = 1 ->
+ g(f(beta,b),e) = y ->
+ g(x,e) = g(y,d)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y,t:int
+logic ac f,g : int,int -> int
+
+goal g48 :
+ f(a,b) = gamma ->
+ f(a+t,c) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduit *)
+ t = 0 ->
+ g(f(gamma,c),d) = x ->
+ g(f(beta,b),e) = y ->
+ g(x,e) = g(y,d)
+
+
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y,t:int
+logic ac f,g : int,int -> int
+
+goal g49 :
+ f(a,b) = gamma ->
+ f(a,c+t) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduit *)
+ g(f(gamma,c+t),d) = x ->
+ g(f(beta,b),e) = y ->
+ g(x,e) = g(y,d)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y,t:int
+logic ac f,g : int,int -> int
+
+goal g50 :
+ f(a,b) = gamma ->
+ f(a,c+t) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduit *)
+ g(f(gamma,c+1),d) = x ->
+ g(f(beta,b),e) = y ->
+ t = 1 ->
+ g(x,e) = g(y,d)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y,t:int
+logic ac f,g : int,int -> int
+
+goal g51 :
+ f(a,b) = gamma ->
+ f(a,c+t) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduit *)
+ t = 1 ->
+ g(f(gamma,c+t),d) = x ->
+ g(f(beta,b),e) = y ->
+ g(x,e) = g(y,d)
+
+
+
+(* status: Valid *)
+
+logic a,b,c,gamma,beta,t2,t4:int
+logic ac f,g : int,int -> int
+
+goal g52 :
+ f(g(a,b+t2),c+t4) = gamma ->
+ g(a,b+t2) = beta ->
+ 1 = t2 ->
+ t4 = 2 * t2->
+ f(beta,c+2)= gamma
+
+
+
+(* status: Valid *)
+
+logic a,b,c,gamma,beta,t3,t1:int
+logic ac f,g : int,int -> int
+
+goal g53 :
+ f(g(a,b+1)+t1,c+2) + t3 = gamma ->
+ g(a+t3,b+1) = beta ->
+ t3 = t1 ->
+ t1 = 0 ->
+ f(beta,c+2)= gamma
+
+
+
+(* status: Valid *)
+
+logic a,b,c,gamma,beta,t3,t2,t4:int
+logic ac f : int,int -> int
+
+goal g54 :
+ a = beta ->
+ f(a,5) + t3 = gamma ->
+ t3 = 0 ->
+ f(a,5)= gamma
+
+
+
+(* status: Valid *)
+logic ac f : int,int -> int
+logic a,b,c,x : int
+
+goal g55 :
+ f(a,b) = f(a,x + f(c,f(b,a))) ->
+ x = 0 ->
+ f(a,b) = f(a,f(c,f(a,b)))
+
+
+
+(* status: Valid *)
+logic ac f,h : int,int -> int
+logic a,b,c,d,x,y,z,beta,gamma : int
+
+goal g56 :
+ y = 1 ->
+ f(a,b) = gamma ->
+ f(a,c+y) = beta ->
+ h(f(f(a,b),c+1),d) = f(gamma,beta) ->
+ h(f(gamma,c+y),d) = f(gamma,beta)
+
+
+
+(* status: Valid *)
+logic ac f,g,h : int,int -> int
+logic a,b,c,d,e,x,y,z,t,m,n,alpha,beta,gamma,delta : int
+
+goal g57 :
+ f(a+x+y, b+z) = gamma ->
+ f(a+x+1, c+y) = beta ->
+ h(f(f(a+x+1,b),c+1),d+z) = f(beta,f(a+x+y, b+z)) ->
+ h(f(beta,b+y-1),g(h(z,x),y)) = h(delta,h(delta,beta)) ->
+ x + y = x + 1 ->
+ z + 1 = y ->
+ x = 100 ->
+ h(d+z,h(delta,h(delta,beta))) = h(f(f(a+x+y, b+z),f(a+x+1, c+y)),g(h(x,z),y))
+
+
+(* status: Valid *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g58 : (forall v,w:int[v,w]. f(v,w) = w) -> a = b
+
+*)
+
+
+(*
+$$$modulo
+$cobj:La fonctionnalité à vérifier est que Alt-Ergo est capable de prouver des buts d'arithmérique linéaire avec comme seul symbole d'arithmétique linéaire le \texttt{modulo}.
+Le test vérifie que les contraintes relatives au \texttt{make} du \texttt{mod} sont bien crées.
+*)
+
+(*deactivated
+(* status: Valid *)
+goal g1: forall a:int. a % 2 = 1 -> (a + 1) % 2 = 1 -> false
+
+
+(* status: Valid *)
+goal g2: forall a:int. a % 2 = 1 -> (a + 1) % 2 = 0
+
+
+(* status: Valid *)
+goal g3: forall a,b:int. a % 2 = 1 -> a = b -> b % 2 = 1
+
+
+(* status: Valid *)
+goal g4: forall a:int. a % 2 = (a + 0)% (1+1)
+
+
+(* status: Valid *)
+goal g5: forall a:int. a % 8 = 6 -> a % 4 = 2 and a % 2 = 0
+
+
+(* status: Valid *)
+goal g6: forall a:int. a % 10 = 12 -> false
+
+
+(* status: Valid *)
+goal g7: forall a,m:int. a%10 = m -> 0 <= m < 10
+
+
+(* status: Valid *)
+goal g9: forall a,m,n,k:int. k = m + n -> a % k = a % (m+n)
+
+
+(* status: Valid *)
+goal g10: forall a:int. a % 4 = 1 -> a % 4 <> 0 and a % 4 <> 2 and a % 4 <> 3
+
+
+(* status: Valid *)
+goal g11: forall a,b:int. a % b = 1 -> b = 10 -> a % 10 = 1
+
+
+(* status: Valid *)
+goal g12: forall a:int. a % 2 = (a + 2) % 2
+
+
+(* status: Valid *)
+goal g12: forall a,b:int. a % 2 = (a + 2*b) % 2
+
+*)
+
+(*
+$$$non_lineaire
+$cobj:La fonctionnalité à vérifier est que Alt-Ergo est capable de prouver des buts d'arithmérique non linéaire.
+Le test vérifie que les axiomes sur l'arithmétique non linéaires d'intervalle sont correctement implémentés et que la coopération avec l'algorithme AC(X) est correcte et termine.
+*)
+
+(*deactivated
+(* status: Valid *)
+goal sum_po_7:
+ forall n,i,s:int.
+ n >= 0 -> 2*s = i*(i + 1) and i <= n -> i >= n -> 2 * s = n*(n + 1)
+
+
+
+(* status: Valid *)
+goal sum_po_3:
+ forall n,i,s:int.
+ n >= 0 -> 2 * s = i * (i + 1) and i <= n ->
+ i < n -> 2 * (s + i + 1) = (i + 1) * (i + 2)
+
+
+logic x,y,z,t1,t2,t3,t4 :int
+goal g1:
+ x * y = t1 * t2 ->
+ x * z = t3 * t4 ->
+ z * t1 * t2 = y * t3 * t4
+
+
+
+(* status: Valid *)
+
+logic x,y,z,t1,t2,t3,t4 :int
+goal g2:
+ x * y = t1 * t2 ->
+ x * z = t3 * t4 ->
+ z * (t1 * t2) = (y * t3) * t4
+
+
+
+(* status: Valid *)
+
+logic x,y,z:int
+
+goal g3:
+ x * y * z = 12 ->
+ x = 2 ->
+ y = 3 ->
+ z = 2
+
+
+
+(* status: Valid *)
+
+goal g4: forall x,y,z:int.
+ x*x*x * y*y * z = 23040 ->
+ x = 4 ->
+ y = 6 ->
+ z = 10
+
+
+(* status: Valid *)
+goal g5: forall x,y,z:int.
+ y = 6 ->
+ x = 4 ->
+ x*x*x * y*y * z = 23040 ->
+ z = 10
+
+
+
+(* status: Valid *)
+goal g6: forall x,y,z:int.
+ y = 6 ->
+ x = 4 ->
+ x*x*x * y*y * z = 23040 ->
+ 4 * y * y * z * z = 360 * z * x
+
+
+(* status: Valid *)
+goal g7: forall x,y,z:int.
+ 5*x + x*y = 4*z + 20 ->
+ x = 4 ->
+ y = z
+
+
+(* status: Valid *)
+goal g8: forall x,y,z:int.
+ x * (5 + y) = 4* (z + 5) ->
+ x = 4 ->
+ y = z
+
+
+
+(* status: Valid *)
+goal g9 : forall x:int. x*x = 0 -> x = 0
+
+
+
+(* status: Valid *)
+goal g10 : forall x:int. x*x*x = 1 -> x = 1
+
+
+
+(* status: Valid *)
+logic x,z : int
+
+goal g11 : x*x <= 0 -> x + z <= 3 -> z <= 3
+
+
+
+(* status: Valid *)
+logic x,z : int
+
+goal g12 : x*x = 0 -> x + z = 3 -> z = 3
+
+
+
+(* status: Valid *)
+
+logic x,y,z:int
+
+goal g13 :
+ z * y * x = 20 ->
+ x * y = 4 ->
+ z = 5
+
+
+(* status: Valid *)
+logic x,y,z:int
+logic ac f : int,int -> int
+goal g14 :
+ 4 * f(2,3) = z * y * x ->
+ x * y = 4 ->
+ f(2,3) = z
+
+
+(* status: Valid *)
+logic a,b,c,d,x,y,z:int
+logic ac f : int,int -> int
+goal g15 :
+ 4 * a*b*c*d = z * y * x ->
+ x * y = 4 ->
+ 4 * a*b*c*d = 4 * z
+
+
+
+(* status: Valid *)
+
+logic x,y:int
+
+goal g16: x*x <=0 -> x + y = 4 -> y = 4
+
+
+(* status: Valid *)
+
+logic x,y:int
+goal g17: x*x*x = -1 -> x + y = 4 -> y = 5
+
+
+
+(* status: Valid *)
+logic x:int
+goal g18: -1<= x <= 1 -> x*x <> 1 -> x = 0
+
+
+
+(* status: Valid *)
+logic x:int
+goal g19 : 2 <= x*x <= 9 -> x= -2 or x = -3 or 2 <= x <= 3
+
+
+
+(* status: Valid *)
+logic x:int
+goal g20 : x*x*x*x <= 16 -> -2 <= x <= 2
+
+
+
+(* status: Valid *)
+logic x:int
+goal g21 : x >= 0 -> x*x = 9 -> x = 3
+
+
+
+(* status: Valid *)
+logic x:int
+goal g22 : 10 <= x*x*x <= 27 -> x = 3
+
+
+
+(* status: Valid *)
+logic x:int
+goal g23 : x*x*x = 64 -> x = 4
+
+
+
+(* status: Valid *)
+logic x:int
+goal g24 : x*x*x = -1000 -> x = -10
+
+
+
+(* status: Valid *)
+logic y:real
+goal g25 : y*y = 9. -> -3. = y or y = 3.
+
+
+
+(* status: Valid *)
+(* prouvé grace à la cooperation des intervalles,
+ de arith (solve et subst) et de AC (collapse) *)
+goal g26:
+ forall x:int. x*x*x = x*x -> x*x = 1 -> x = 1
+
+
+
+(* status: Valid *)
+(* inconsistent *)
+goal g27:
+ forall x:int. x*x*x = x*x -> x*x = 4 -> false
+
+
+
+
+(* status: Valid *)
+goal g28:
+ forall x:int. x >= 0 -> x <= (x + 1) * (x + 1)
+
+*)
+
+
+(*
+$$$arith_div
+$cobj:La fonctionnalité à vérifier est que Alt-Ergo est capable de prouver des buts d'arithmérique non linéaire faisant intervenir des divisions (entières ou non).
+Le test vérifie que les contraintes relatives au \texttt{make} du \texttt{div} sont bien crées et que les axiomes de la division d'intervalles sont corrects.
+*)
+
+(*deactivated
+(* status: Valid *)
+logic x,y:int
+goal g1: 2 <= x / y <= 4 -> y = 2 -> 4 <= x <= 9
+
+
+
+(* status: Valid *)
+logic x,y:int
+goal g2: 4 <= x <= 9 -> 2 <= x / 2 <= 4
+
+
+
+(* status: Valid *)
+logic x,y:int
+goal g3: 4 <= x <= 8 -> -2 <= y <= 2 -> y <> 0 -> -8 <= x / y <= 8
+
+
+
+(* status: Valid *)
+logic x:int
+goal g5 : x <> 0 -> x/x = 1
+
+
+
+(* status: Valid *)
+logic x,y,z,t:int
+goal g6 : -4*x+2*y-z*t <> 0 -> (12*x-6*y+3*z*t)/(8*x-4*y+2*z*t) = 1
+
+
+
+(* status: Valid *)
+logic x:int
+goal g7 : 0/0 = 0/0 -> true
+
+
+
+(* status: Valid *)
+logic x:int
+goal g8 : 0/0 = 0/0
+
+
+
+(* status: Valid *)
+
+logic x,y : int
+
+goal g9 : x<>0 -> x = y -> y/y = 1
+
+
+(* status: Valid *)
+logic x,y : int
+
+goal g10 : x > 0 -> y > 0 -> x/y >=0
+
+
+(* status: Valid *)
+logic x : int
+
+goal g11 : x<>0 -> x/x = 1
+
+
+(* status: Valid *)
+logic x,y,z:int
+
+goal g12:
+
+x <> 0 -> (-2*x) / x = -2
+
+
+(* status: Valid *)
+logic x,y,z:int
+
+goal g13:
+
+x <> 0 -> x / (-2*x) = -1
+
+
+(* status: Valid *)
+logic x,y,z:int
+
+goal g14:
+
+2*x + 2*y <> 0 -> (4*x + 4*y ) / (2*x + 2*y ) = 2
+
+
+(* status: Valid *)
+logic x,y,z:int
+
+goal g15:
+
+2*x + 2*y +1 <> 0 -> (4*x + 4*y + 2 ) / (2*x + 2*y + 1) = 2
+
+
+(* status: Valid *)
+goal g16 (*sqrt_po_8*):
+ forall x,y:int.
+ x <> 0 ->
+ y = (x + 1) / 2 ->
+ y = ((x / x) + x) / 2
+
+
+(* status: Valid *)
+goal g17 (*sqrt_po_8*):
+ forall x,y:int.
+ x <> 0 ->
+ (x + 1) / 2 = ((x / x) + x) / 2
+
+
+(* status: Valid *)
+goal g18 (*sqrt_po_8*):
+ forall x,y:int.
+ x <> 0 ->
+ y <> 0 ->
+ (x + 1) / y = ((x / x) + x) / y
+
+
+(* status: Valid *)
+goal g19:
+ forall x,y,z:int.
+ x > 3 ->
+ y > 0 ->
+ z > 0 ->
+ y > z ->
+ z = ((x / y) + y) / 2 ->
+ z > 1 and y > 2
+*)
+
+(*
+$$$arith_modulo_div
+$cobj:La fonctionnalité à vérifier est que Alt-Ergo est capable de prouver des buts d'arithmérique non linéaire faisant intervenir des divisions (entières ou non) et des modulos.
+Le test vérifie que les contraintes relatives au \texttt{make} de \texttt{div} et \texttt{mod} sont bien crées et que les axiomes de la division d'intervalles sont corrects.
+*)
+
+(*deactivated
+(* status: Valid *)
+goal g0: forall a: int. a > 0 -> a / 2 < a
+
+
+(* status: Valid *)
+goal mult_po_9: forall a,b :int. a % 2 <> 1 -> (a / 2) * 2 * b = a * b
+
+
+(* status: Valid *)
+goal mult_po_8: forall a:int. a > 0 -> a % 2 <> 1 -> a / 2 >= 0
+
+
+(* status: Valid *)
+goal mult_po_6: forall a:int. a > 0 -> a % 2 = 1 -> a / 2 < a
+
+
+(* status: Valid *)
+goal mult_po_4: forall a,b:int. a > 0 -> a % 2 = 1 -> b + (a / 2) * (2 * b) = a * b
+
+
+(* status: Valid *)
+goal mult_po_3: forall a:int. a > 0 -> a % 2 = 1 -> a / 2 >= 0
+
+
+(* status: Valid *)
+goal mult_po_11: forall a:int. a > 0 -> a % 2 <> 1 -> a/2 < a
+
+*)
+
+
+(*
+$$$polynomes
+$cobj:La fonctionnalité à vérifier est que Alt-Ergo est capable de prouver des buts d'arithmérique non linéaire en utilisant la distributivité de la multiplication sur l'addition effectuée par le \texttt{make} des polynômes.
+*)
+
+(* deactivated
+(* status: Valid *)
+goal g1 : (*goal sqrt_po_10*)
+ forall x,y:int.
+ x > 3 ->
+ y = (x + 1) / 2 ->
+ x < (y + 1) * (y + 1)
+
+
+
+(* status: Valid *)
+
+goal g2 :
+ forall x,y,z,t:int.
+ 0 <= y + z <= 1 ->
+ x + t + y + z = 1 ->
+ y + z <> 0 ->
+ x + t = 0
+*)
+
+
+(*
+$$$arith_false
+$cobj:La fonctionnalité à vérifier est que le raisonnement fait par la coopération du module d'intervalles et l'algorithme Fourier-Motzkin est correct et que Alt-Ergo ne prouve pas des buts faux faisant intervenir de l'arithmétique linéaire.
+*)
+
+(* status: Unknown *)
+goal g1: 1=2
+
+
+(* status: Unknown *)
+logic a:int
+goal g2: a+0 = a+1
+
+(*deactivated
+(* status: Unknown *)
+logic Q,P: prop
+
+goal g3:
+ forall c,v:int. (Q and c<=v and v<=c) ->P
+*)
+
+(* status: Unknown *)
+logic f: int -> int
+goal g4:
+ forall x,y:int. f(x-1) = x + 2 and f(y) = y - 2 and y + 1 = x
+
+(*deactivated
+(* status: Unknown *)
+logic f: int -> int
+goal g5:
+ forall u,v,x,y:int.
+ u<=v and v<=u and 2*x +1 <= 2*y and x=f(u) and y=f(v)
+
+
+(* status: Unknown *)
+logic P: prop
+goal g6:
+ forall x:int. x=1 and (3<x -> P) -> P
+
+
+(* status: Unknown *)
+logic Q,P: prop
+goal g7:
+ forall x:int. x=3 and (3<x -> P) -> P
+
+
+(* status: Unknown *)
+logic b,a,c: int
+
+goal g8: b<=c -> (b<>a)-> a+1<=b -> false
+
+
+(* status: Unknown *)
+goal g9: forall x:int. 0<=x<=1 -> x=0
+
+
+(* status: Unknown *)
+goal g10: forall x:int. 0<=x<=1 -> x=1
+
+
+(* status: Unknown *)
+
+goal g11:
+forall x,y:int. 9*x + 13*y + 1 = 0 -> false
+
+(* status: Unknown *)
+ goal g12:
+ forall diff:int.
+ forall left:int.
+ forall right:int.
+ diff = right - left ->
+ diff > 0 ->
+ forall r6:int. r6 = diff / 2 ->
+ forall r8:int. r8 = left + r6 ->
+ right - r8 < diff
+
+(* status: Unknown *)
+
+logic a, b, c :int
+
+goal g13:
+ 3*c -2 = 8*a and
+ c <= 0 and
+ - b - c <= 0 and
+ 2*b + c - 2 <= 0
+ -> false
+
+
+
+(* status: Unknown *)
+goal g14 :
+ forall x,y,z,t:int. 30*x = 15*y + 10*z + t ->
+ t = 5 -> false
+
+
+
+(* status: Unknown *)
+goal g15:
+ forall a,min, max,k : int.
+ min = a ->
+ min <= k <= max ->
+ max - min <= 10 ->
+ max - min = 0 ->
+ false
+
+
+
+(* status: Unknown *)
+goal g16 : forall x:real. x < 3.0 -> x <= 2.0
+
+
+
+(* status: Unknown *)
+logic p:int
+
+goal g17:
+(* 1 *) p <> 0 and p <> 1 and p <= 9 and
+(* 2 *) p >= 4 and p <= 10 and p <> 5 and
+(* 3 *) p >= 1 and p <= 4
+ -> false
+*)
+
+(*
+$$$ac_arith_mult_false
+$cobj:La fonctionnalité à vérifier est que le raisonnement fait par la coopération du module d'intervalles et de l'algorithme AC(X) est correct et que Alt-Ergo ne prouve pas des buts faux faisant intervenir de l'arithmétique non linéaire.
+*)
+
+(*deactivated
+(* status: Unknown *)
+logic y:real
+goal g1 : y*y = 9.1 -> -3. = y or y = 3.
+
+
+
+(* status: Unknown *)
+logic x:int
+goal g2 : 4 <= x*x <= 9 -> 2 <= x <= 3
+
+
+
+(* status: Unknown *)
+
+logic f : int -> int
+
+goal g3 :
+ forall a,b,x,y,z,t:int.
+ x * x = f(z) + 2 ->
+ x * y = f(t) + 2 ->
+ false
+
+
+
+(* status: Unknown *)
+logic x:int
+goal g4 : 0 <= x*x <= 4 -> 0 <= x <= 2
+
+
+
+(* status: Unknown *)
+logic x:int
+goal g5 : x*x = 25 -> x = 5
+
+*)
+
+(*
+$$$div_false
+$cobj:La fonctionnalité à vérifier est que les contraintes du \texttt{make} de la divisions sont bien crées, que le raisonnement fait par le module d'intervalles sur la division est correct et que Alt-Ergo ne prouve pas des buts faux faisant intervenir des divisions non linéaires.
+*)
+
+(*deactivated
+(* status: Unknown *)
+logic x,y:int
+goal g1: 2 <= x / y <= 4 -> y = 2 -> 4 <= x <= 8
+
+
+
+(* status: Unknown *)
+logic x,y:int
+goal g2: 4 <= x <= 8 -> -2 <= y <= 2 -> -8 <= x / y <= 8
+
+
+
+(* status: Unknown *)
+logic x,y:int
+goal g3: 0 / 0 = 0
+
+
+
+(* status: Unknown *)
+logic x,y:int
+goal g4: -1 <= x <= 1 -> 0 / x = 0
+
+
+
+(* status: Unknown *)
+logic x:int
+goal g5 : x/x = 1
+
+
+
+
+(* status: Unknown *)
+logic x:int
+goal g6 : 0/0 = 1
+
+
+
+(* status: Unknown *)
+logic x:int
+goal g7 : 0/0 = 0/0 -> false
+
+
+
+(* status: Unknown *)
+logic x:int
+goal g8 : 0/0 <> 0/0
+
+
+
+(* status: Unknown *)
+logic x:int
+logic P,Q: int -> prop
+goal g9 : P(0/x) -> P(0)
+
+
+
+(* status: Unknown *)
+logic x:int
+logic P,Q: int -> prop
+goal g10 : P(0) -> P(x)
+
+
+
+(* status: Unknown *)
+logic x,y:int
+goal g11 : y >= 1 -> (x/y)*y = x
+
+
+
+(* status: Unknown *)
+logic P : int -> prop
+
+logic x,y : int
+
+goal g12 : y = 0 -> P(x/y) -> false
+
+
+
+(* status: Unknown *)
+logic x,y : int
+
+goal g13 : -1 < x/y <1 -> false
+
+
+
+(* status: Unknown *)
+logic x,y : int
+
+goal g14 : x > 0 -> y > 0 -> x/y >0
+
+
+
+(* status: Unknown *)
+logic x,y,z : int
+
+goal g15 : x>=0 -> y >=0 -> x/y>=0
+
+
+
+(* status: Unknown *)
+
+logic x,y,z : int
+
+goal g16 : x>=0 -> y >=0 -> x/y = z -> y = 0 -> x/y>=0
+
+*)
+
+(*
+$$$ac_arith_false
+$cobj:La fonctionnalité à vérifier est que le raisonnement fait par l'algorithme AC(X) modulo la théorie de l'arithmétique est correct et que Alt-Ergo ne prouve pas des buts faux faisant intervenir de l'arithmétique linéaire et des symboles associatifs commutatifs.
+*)
+
+(*deactivated
+
+(* status: Unknown *)
+logic a,b,c,x,beta,gamma,d:int
+
+logic ac f : int,int -> int
+
+goal g1 :
+ f((f(a,b) + x),c) = gamma ->
+ x = 1 ->
+ f(a,c) = a ->
+ f(a,d) = beta ->
+ f(b,beta) = f(d,gamma)
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,gamma,beta,x : int
+logic ac f : int , int -> int
+
+goal g2 :
+ f(a,b) = f(x,gamma) ->
+ f(a,c) = f(x,beta) ->
+ f(gamma,c) = f(beta,b)
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,gamma,beta,x,u,v : int
+logic f : int , int -> int
+
+goal g3 :
+ f(a,b) = u ->
+ f(a,c) = v ->
+ f(x,gamma) = u ->
+ f(x,beta) = v ->
+ f(gamma,c) = f(beta,b)
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,gamma,beta,x,y: int
+logic ac f : int , int -> int
+
+goal g4 :
+ f(a,b) = f(x,gamma) ->
+ f(a,c) = f(x,beta) ->
+ f(x,f(gamma,c)) = f(y,f(beta,b))
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g5 :
+ f(a+1,a) = f(a,b+1)
+
+
+
+(* status: Unknown *)
+logic a,b,c,x,beta,gamma,d:int
+
+logic ac f : int,int -> int
+
+goal g6 :
+ f((f(a,b) + x),c) = gamma ->
+ f(a,c) = a ->
+ f(a,d) = beta ->
+ f(b,beta) = f(d,gamma)
+
+
+
+(* status: Unknown *)
+
+logic ac f : int,int -> int
+goal g7 : forall a,b,c,x:int. c = a + x -> a = f(c,b) -> a=0 -> f(c,b)=c
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g8 :
+ f(a+1,a) = f(a+1,b)
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g9 :
+ a = b ->
+ f(a+1,a) = f(a,b)
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g10 :
+ a + 1 = b + x ->
+ x = b ->
+ f(a,a) = f(a,b)
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g11 :
+ f(a,a) = a ->
+ f(a,b) + a =a + b->
+ a = b
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g12 :
+ a + 1 = b + 1 ->
+ f(a,a-1) = f(a,b)
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+goal g13 :
+ 2 * a = 3 * b ->
+ f(x,(2/3) * a) = f(b,x)
+
+
+
+(* status: Unknown *)
+
+logic a,b,c,x:int
+logic ac f : int,int -> int
+
+goal g15 :
+ f(b,a) = a ->
+ f(a,b) + a = a + b
+
+
+
+(* status: Unknown *)
+
+logic ac f : int,int -> int
+
+goal g16 : (forall v,w:int[v,w]. f(v,w) = w) -> (exists v,w:int. v <> w)
+
+*)
\ No newline at end of file
diff --git a/tests/tests_altergo_qualif.split b/tests/tests_altergo_qualif.split
new file mode 100644
index 000000000..06eebb8ff
--- /dev/null
+++ b/tests/tests_altergo_qualif.split
@@ -0,0 +1,1234 @@
+(** cc *)
+
+(* status: Valid *)
+
+type t
+logic a,b,c,d,e: t
+logic f,h : 'a -> 'a
+logic g: 'a , 'a -> 'a
+
+goal g1:
+ forall x:t. h(x)=x and g(a,x)=a -> g(g(a,h(x)),x)=a
+
+(*deactivated
+(* status: Valid *)
+
+type t
+logic a,b,c,d,e,f: t
+
+goal g2:
+ a=c and c=e and a<>b and b=d and d=f -> c<>f
+*)
+
+(* status: Valid *)
+
+type t
+logic a,b,c,d,e: t
+logic f : 'a -> 'a
+logic g,h: 'a , 'a -> 'a
+
+goal g3:
+ forall x,y:t. f(f(f(a)))=a and f(f(f(f(f(a)))))=a and g(x,y)=x ->
+ h(g(g(x,y),y),a)=h(x,f(a))
+
+(*deactivated
+(* status: Valid *)
+logic P,Q: int -> prop
+logic f: int -> int
+axiom a :
+ forall x:int[P(f(x))].
+ P(f(x)) -> Q(x)
+goal g4:
+ forall a,b,c:int.
+ P(a) -> a= f(b) -> a = f(c) ->
+ Q(b) and Q(c)
+*)
+
+(*deactivated
+(* status: Valid *)
+logic P : int -> prop
+
+goal g5 : (exists x:int. P(x)) -> exists y:int. P(y)
+*)
+
+(* status: Valid *)
+logic f, g : int -> int
+logic h: int,int -> int
+logic a, b:int
+
+goal g6:
+ h(g(a),g(b)) = g(b) ->
+ f(h(g(a),g(b))) - f(g(b)) = 0
+
+
+(* status: Valid *)
+
+logic f, g : int -> int
+logic h: int,int -> int
+logic a, b:int
+
+goal g7:
+ h(g(a),g(b)) = g(b) ->
+ g(f(h(g(a),g(b))) - f(g(b))) = g(0)
+
+
+(* status: Valid *)
+logic h,g,f: int,int -> int
+logic a, b:int
+
+goal g8:
+ h(g(a,a),g(b,b)) = g(b,b) ->
+ a = b ->
+ g(f(h(g(a,a),g(b,b)),b) - f(g(b,b),a),
+ f(h(g(a,a),g(b,b)),a) - f(g(b,b),b)) = g(0,0)
+
+
+(* status: Valid *)
+
+logic h,g,f: int,int -> int
+logic a, b:int
+
+goal g9:
+ a = b ->
+ g(f(b,b) - f(b,a),
+ f(a,b) - f(a,a)) = g(0,0)
+
+
+(* status: Valid *)
+
+logic f: int -> int
+logic a, b:int
+
+goal g10:
+ a = b ->
+ f(f(a) - f(b)) = f(0)
+
+
+(* status: Valid *)
+
+logic f: int -> int
+logic a, b:int
+
+goal g11:
+ a = b ->
+ f(f(a) - f(b)) = f(f(b)-f(a))
+
+
+(* status: Valid *)
+
+logic f: int -> int
+logic a, b:int
+
+goal g12:
+ a = b ->
+ f(0) = f(f(a) - f(b))
+
+
+
+
+
+
+(* ac_empty
+ La fonctionnalité à vérifier est que l'algorithme AC(X) implémente bien ses spécifications et que Alt-Ergo est capable de prouver des buts faisant intervenir de l'égalité et des symboles associatifs-commutatifs.
+*)
+
+(*deactivated
+(* status: Valid *)
+logic ac m: int,int -> int
+logic t1,t2,t3,t4,t5,t6,t7,t8:int
+
+goal g1:
+ m(m(m(m(m(m(m(t1,t2),t3),t4),t5),t6),t7),t8) =
+ m(t1,m(t2,m(t3,m(t4,m(t5,m(t6,m(t7,t8)))))))
+
+
+(* status: Valid *)
+
+logic a, c, x, y, beta, gamma: int
+logic h: int -> int
+logic ac f: int, int -> int
+
+
+goal g2 :
+ f(a,h(x)) = gamma ->
+ f(a,c) = beta ->
+ x = y ->
+ f(a,f(h(x),c)) = f(h(y),beta)
+
+
+(* status: Valid *)
+
+type set
+logic ac u: set,set -> set
+
+axiom idem : forall x,X: set. u(u(x,x),X)=u(x,X)
+goal g3: forall r,s,t: set. u(t,u(t,s)) = u(s,t)
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g4 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(a,b) = gamma
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+
+goal g5 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g6 :
+ gamma = f(a,b)->
+ f(a,c) = beta ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g7 :
+ f(a,b) = gamma ->
+ beta = f(a,c) ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g8 :
+ gamma = f(a,b) ->
+ beta = f(a,c) ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g9 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g10 :
+ gamma = f(a,b)->
+ f(a,c) = beta ->
+ f(c,gamma) = f(b,beta)
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g11 :
+ f(a,b) = gamma ->
+ beta = f(a,c) ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g12 :
+ gamma = f(a,b) ->
+ beta = f(a,c) ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+logic a,b,c, beta,gamma,lambda : int
+logic ac f : int,int -> int
+
+goal g13 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(b,f(lambda,beta)) = f(f(c,lambda),gamma)
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,lambda : int
+logic ac f : int,int -> int
+
+goal g14 :
+ gamma = f(a,b)->
+ f(a,c) = beta ->
+ f(gamma,f(lambda,f(b,beta))) = f(f(c,gamma),f(lambda,gamma))
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,lambda : int
+logic ac f : int,int -> int
+
+goal g15 :
+ f(a,b) = gamma ->
+ beta = f(a,c) ->
+ f(f(b,beta),lambda) = f(lambda,f(c,gamma))
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,lambda : int
+logic ac f : int,int -> int
+
+goal g16 :
+ gamma = f(a,b) ->
+ beta = f(a,c) ->
+ f(lambda,f(b,beta)) = f(c,f(lambda,gamma))
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,lambda : int
+logic ac f : int,int -> int
+
+goal g17 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(f(c,gamma),lambda) = f(f(lambda,b),beta)
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,lambda : int
+logic ac f : int,int -> int
+
+goal g18 :
+ gamma = f(a,b)->
+ f(a,c) = beta ->
+ f(lambda,f(c,gamma)) = f(b,f(beta,lambda))
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,lambda : int
+logic ac f : int,int -> int
+
+goal g19 :
+ f(a,b) = gamma ->
+ beta = f(a,c) ->
+ f(lambda,f(c,gamma)) = f(b,f(lambda,beta))
+
+
+(* status: Valid *)
+
+logic a,b,c, beta,gamma,lambda : int
+logic ac f : int,int -> int
+
+goal g20 :
+ gamma = f(a,b) ->
+ beta = f(a,c) ->
+ f(c,f(gamma,lambda)) = f(f(b,beta),lambda)
+
+
+(* status: Valid *)
+
+logic aa,a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g21 :
+ a = aa ->
+ f(a,b) = gamma ->
+ f(aa,c) = beta ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+logic aa,a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g22 :
+ gamma = f(a,b)->
+ f(aa,c) = beta ->
+ a = aa ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+logic aa,a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g23 :
+ f(a,b) = gamma ->
+ beta = f(aa,c) ->
+ a = aa ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+logic aa,a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g24 :
+ gamma = f(a,b) ->
+ beta = f(aa,c) ->
+ a = aa ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+logic aa,a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g25 :
+ f(a,b) = gamma ->
+ f(aa,c) = beta ->
+ a = aa ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+
+logic aa,a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g26 :
+ gamma = f(a,b)->
+ f(aa,c) = beta ->
+ a = aa ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+
+logic aa,a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g27 :
+ f(a,b) = gamma ->
+ beta = f(aa,c) ->
+ a = aa ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+
+logic aa, a,b,c, beta,gamma : int
+logic ac f : int,int -> int
+
+goal g28 :
+ gamma = f(a,b) ->
+ beta = f(aa,c) ->
+ a = aa ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+
+type a
+logic a,b,c, beta,gamma : a
+logic ac f : a,a -> a
+
+goal g29 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(a,b) = gamma
+
+
+(* status: Valid *)
+
+type a
+logic a,b,c, beta,gamma : a
+logic ac f : a,a -> a
+
+goal g30 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+type a
+logic a,b,c, beta,gamma : a
+logic ac f : a,a -> a
+
+goal g31 :
+ gamma = f(a,b)->
+ f(a,c) = beta ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+type a
+logic a,b,c, beta,gamma : a
+logic ac f : a,a -> a
+
+goal g32 :
+ f(a,b) = gamma ->
+ beta = f(a,c) ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+type a
+logic a,b,c, beta,gamma : a
+logic ac f : a,a -> a
+
+goal g33 :
+ gamma = f(a,b) ->
+ beta = f(a,c) ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+type a
+logic a,b,c, beta,gamma : a
+logic ac f : a,a -> a
+
+goal g34 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+
+type a
+logic a,b,c, beta,gamma : a
+logic ac f : a,a -> a
+
+goal g35 :
+ gamma = f(a,b)->
+ f(a,c) = beta ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+
+type a
+
+logic a,b,c, beta,gamma : a
+logic ac f : a,a -> a
+
+goal g36 :
+ f(a,b) = gamma ->
+ beta = f(a,c) ->
+ f(c,gamma) = f(b,beta)
+
+
+(* status: Valid *)
+
+type a
+logic a,b,c, beta,gamma : a
+logic ac f : a,a -> a
+
+goal g37 :
+ gamma = f(a,b) ->
+ beta = f(a,c) ->
+ f(c,gamma) = f(b,beta)
+
+(* status: Valid *)
+
+(* c = beta *)
+logic a,b,c, gamma : int
+logic ac f : int,int -> int
+
+goal g38 :
+ c = f(a,c) ->
+ f(a,b) = gamma ->
+ f(b,c) = f(c,gamma)
+
+
+(* status: Valid *)
+
+(* c = beta *)
+logic a,b,c, gamma : int
+logic ac f : int,int -> int
+
+goal g39 :
+ f(a,c) = c ->
+ f(a,b) = gamma ->
+ f(b,c) = f(c,gamma)
+
+
+(* status: Valid *)
+
+(* gamma |-> b et beta |-> c *)
+logic a, b, c : int
+logic ac f : int,int -> int
+
+goal g40 :
+ c = f(a,b) ->
+ b = f(a,c) ->
+ f(c,c) = f(b,b)
+
+
+(* status: Valid *)
+
+(* gamma |-> b et beta |-> c *)
+logic a, b, c : int
+logic ac f : int,int -> int
+
+goal g41 :
+ f(a,b) = c ->
+ f(a,c) = b ->
+ f(b,b) = f(c,c)
+
+(* status: Valid *)
+
+logic a1, a2, a3, b1, b2, x,y,z ,beta, gamma : int
+logic ac f : int,int -> int
+
+goal g42 :
+ f(a1,f(a2,f(a3,x))) = gamma ->
+ f(b1,f(b2,f(y,z))) = beta -> (* boucle ici*)
+ f(a1,f(a2,a3)) = f(b1,b2) ->
+ f(gamma,f(y,z)) = f(beta,x)
+
+
+(* status: Valid *)
+
+logic a1, a2, a3, b1, b2, x,y,z ,beta, gamma : int
+logic ac f : int,int -> int
+
+goal g43 :
+ f(a1,f(a2,f(a3,x))) = gamma ->
+ f(b1,f(b2,f(y,z))) = beta -> (* boucle ici*)
+ f(a1,f(a2,a3)) = f(b1,b2) ->
+ f(gamma,f(y,z)) = f(beta,x)
+
+
+(* status: Valid *)
+
+(* une pc car f(a1,a2,a3) = f(b1,b2)*)
+logic a1, a2, a3, b1, b2, y ,beta, gamma : int
+logic ac f : int,int -> int
+
+goal g44 :
+ f(a1,f(a2,a3)) = gamma ->
+ f(b1,f(b2,y)) = beta -> (* boucle ici*)
+ f(b1,b2) = f(a1,f(a2,a3)) ->
+ f(gamma,y) = beta
+
+
+(* status: Valid *)
+
+(* pc sur a1 = a1
+ ou seulement pc sur f(a1,a2,a3) = f(a1,b2)*)
+logic a1, a2, a3, b1, b2, x,y,z ,beta, gamma : int
+logic ac f : int,int -> int
+
+goal g45 :
+ f(a1,f(a2,f(a3,x))) = gamma ->
+ f(a1,f(b2,f(y,z))) = beta ->
+ f(a1,f(a2,a3)) = f(a1,b2) ->
+ f(gamma,f(y,z)) = f(beta,x)
+
+
+(* status: Valid *)
+
+(* pc sur a1 = a1
+ ou seulement pc sur f(a1,a2,a3) = f(a1,b2)*)
+logic a1, a2, a3, b1, b2, x,y,z ,beta, gamma : int
+logic ac f : int,int -> int
+
+goal g46 :
+ f(a1,f(a2,f(a3,x))) = gamma ->
+ f(a1,f(b2,f(y,z))) = beta ->
+ a3 = b2 ->
+ f(gamma,f(y,z)) = f(beta,f(a2,x))
+
+
+(* status: Valid *)
+(* pc sur a1 = a1
+ ou seulement pc sur f(a1,a2,a3) = f(a1,b2)*)
+logic a1, a11, a2, a3, b1, b2, x,y,z ,beta, gamma : int
+logic ac f : int,int -> int
+
+goal g47 :
+ f(a1,f(a2,f(a3,x))) = gamma ->
+ f(a1,f(b2,f(y,z))) = beta ->
+ f(a2,a3) = b2 ->
+ f(gamma,f(y,z)) = f(beta,x)
+
+
+(* status: Valid *)
+
+(* pc sur a1 = a1
+ ou seulement pc sur f(a1,a2,a3) = f(a1,b2)*)
+
+logic a1, a11, a2, a3, b1, b2, x,y,z ,beta, gamma : int
+logic ac f : int,int -> int
+
+goal g48 :
+ f(a1,f(a2,f(a3,x))) = gamma ->
+ f(a11,f(b2,f(y,z))) = beta ->
+ f(a2,f(a3,a1)) = f(b2,a11) ->
+ f(gamma,f(y,z)) = f(beta,x)
+
+
+(* status: Valid *)
+
+logic a,b,c,s : int
+logic g : int -> int
+logic ac f : int,int -> int
+
+goal g49:
+ f(b,c) = s ->
+ f(g(s),c) = b ->
+ f(g(s),s) = f(b,b)
+
+
+(* status: Valid *)
+
+logic a,b,c,s : int
+logic g : int -> int
+logic ac f : int,int -> int
+
+goal g50:
+ f(b,c) = s ->
+ f(g(s),c) = b ->
+ g(s) = s ->
+ f(s,s) = f(b,b)
+
+
+(* status: Valid *)
+
+logic a,b,c,gamma,beta,x: int
+logic ac f : int , int -> int
+
+goal g51 :
+ f(a,b) = f(x,gamma) ->
+ f(a,c) = f(x,beta) ->
+ f(x,f(gamma,c)) = f(x,f(beta,b))
+
+
+(* status: Valid *)
+
+logic a,b,c,gamma,beta,x: int
+logic ac f : int , int -> int
+
+goal g52 :
+ f(a,b) = f(x,gamma) ->
+ f(a,c) = f(x,beta) ->
+ f(a,f(gamma,c)) = f(a,f(beta,b))
+
+
+(* status: Valid *)
+
+logic a,b,c,gamma,beta,x,y : int
+logic ac f : int , int -> int
+
+goal g53 :
+ f(a,b) = f(x,gamma) ->
+ f(a,c) = f(y,beta) ->
+ f(x,f(gamma,c)) = f(y,f(beta,b))
+
+
+(* status: Valid *)
+
+logic a,b,x,y,z : int
+logic ac f: int,int -> int
+
+goal g54:
+ f(a,x) = f(a,y) ->
+ f(a,z) = b ->
+ f(z,f(a,y)) = f(x,b) and f(z,f(a,x)) = f(y,b)
+
+
+
+
+
+
+(* status: Valid *)
+
+logic a,b,c,d,x,y,gamma,beta : int
+logic ac f,g:int,int -> int
+
+goal g55 :
+ g(x,y) = f(a,b) ->
+ f(g(x,y),d) = gamma ->
+ f(a,c) = beta ->
+ f(gamma,c) = f(beta,f(b,d))
+
+
+(* status: Valid *)
+
+logic a,b,c,x,gamma,beta,delta,omega : int
+logic ac f,g:int,int -> int
+
+goal g56 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ g(x,gamma)= delta ->
+ g(x,beta) = omega ->
+ g(beta,delta) = g(gamma,omega)
+
+
+(* status: Valid *)
+
+logic a,b,c,x,gamma,beta,delta,omega : int
+logic ac f,g:int,int -> int
+
+goal g57 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ g(x,gamma)= delta ->
+ g(x,beta) = omega ->
+ f(b,beta) = f(c,gamma)
+
+
+(* status: Valid *)
+
+logic a, b, c, x,y,z : int
+logic ac g : int, int -> int
+
+goal g58:
+
+ g(a,b) = g(x,y) ->
+ g(a,c)=g(x,z) ->
+ g(b,g(x,z)) = g(c,g(x,y))
+
+
+(* status: Valid *)
+
+logic x,y,z,t,b : int
+logic ac f,g : int,int -> int
+
+goal g59:
+ f(z,g(y,x)) = t ->
+ y = b ->
+ f(z,g(x,b)) = t
+
+
+(* status: Valid *)
+
+logic x,y,z,t,gamma,beta : int
+logic ac f,g : int,int -> int
+
+goal g60:
+ f(x,g(y,z)) = gamma ->
+ f(x,t) = beta ->
+ f(gamma,t) = f(beta,g(y,z))
+
+
+(* status: Valid *)
+
+logic b, c,a, d,z, subst : int
+logic ac f : int, int -> int
+logic g : int -> int
+
+goal g61 :
+ f(a,c) = a ->
+ f(c, g (f (b, c))) = b ->
+ g(f (b, c)) = f (b, c) ->
+ f(b,b) = f(f(b,c),f(b,c))
+
+
+(* status: Valid *)
+
+logic b, c,a, d,z, s : int
+logic ac f : int, int -> int
+logic g : int -> int
+
+goal g62 :
+ f(b,c) = s ->
+ f(a,c) = a ->
+ f(c,g(s)) = b ->
+ g(s) = s ->
+ f(b,b) = f(s,s)
+
+
+(* status: Valid *)
+
+logic b, c,a, d,z, s : int
+logic ac f : int, int -> int
+logic g : int -> int
+
+goal g63 :
+ f(b,c) = s ->
+ f(a,c) = a ->
+ f(c,g(s)) = b ->
+ g(s) = s ->
+ f(b,b) = f(g(s),s)
+
+
+(* status: Valid *)
+
+logic b, c,a, d,z, s : int
+logic ac f : int, int -> int
+logic g : int -> int
+
+goal g64 :
+ s = f(b,c) ->
+ f(a,c) = a ->
+ f(c,g(s)) = b ->
+ g(s) = s ->
+ f(b,b) = f(s,s)
+
+
+(* status: Valid *)
+
+logic a,b,c :int
+logic ac f :int,int-> int
+
+goal g65 : a = b -> f(c,a) = f(c,b)
+
+
+(* status: Valid *)
+
+logic a, b, c, d, x, y : int
+logic ac g : int, int -> int
+
+goal g66:
+ g(x,g(a,b)) = g(c,g(y,d)) ->
+ g(g(a,b),g(b,x)) = g(g(c,d),g(y,b))
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,f,g,h,x,y,z,t : int
+logic ac k : int, int -> int
+
+goal g67:
+ k(a,b) =x ->
+ k(b,g) =y ->
+ k(k(a,c),e)=z ->
+ k(g,h) =t ->
+ k(z,(k(k(t,y),x)))=k(k(a,b),k(k(k(g,e),k(b,k(a,c))),k(h,g)))
+
+
+(* status: Valid *)
+
+logic a, b, c, d, x, y,t : int
+logic ac f : int, int -> int
+
+goal g68 :
+ f(a,a) = a ->
+ f(a,b) = c ->
+ f(f(a,a),b) = a ->
+ f(a,f(f(a,a),a)) = f(a,c)
+
+
+(* status: Valid *)
+
+logic a,b,aa,x : int
+logic ac f : int,int -> int
+
+goal g69:
+ a = a ->
+ b = b ->
+ aa = aa ->
+ a = aa -> f(a,b) = f(aa,b)
+
+
+(* status: Valid *)
+
+logic a,b,aa,x : int
+logic ac f : int,int -> int
+
+goal g70:
+ f(a,b) = x -> a = aa -> a+1=aa+1
+
+
+(* status: Valid *)
+
+logic a,b,aa,x : int
+logic ac f : int,int -> int
+
+goal g71:
+ f(a,b) = x -> a = aa -> f(a,b) = f(aa,b) = x
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y:int
+logic ac f,g : int,int -> int
+
+goal g72 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduite *)
+ g(f(gamma,c),d) = x ->
+ g(f(beta,b),e) = y ->
+ g(x,e) = g(y,d)
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y:int
+logic ac f,g : int,int -> int
+
+goal g73 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduite *)
+ f(f(gamma,c),d) = x ->
+ f(f(beta,b),e) = y ->
+ f(x,e) = f(y,d)
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y:int
+logic ac f,g : int,int -> int
+
+goal g74 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ (* f(gamma,c) = f(beta,b) est déduit *)
+ g(f(f(a,c),b),d) = x ->
+ g(f(beta,b),e) = y ->
+ g(x,e) = g(y,d)
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta,x,y:int
+logic ac f : int,int -> int
+logic g : int,int -> int
+
+axiom commut : forall x,y:int. g(x,y) = g(y,x)
+goal g75 :
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ g(a,f(gamma,c)) = g(f(a,f(c,b)),a)
+
+
+
+(* status: Valid *)
+
+type set
+
+logic a,b :set
+logic ac union : set,set -> set
+
+axiom idem : forall x,X: set. union (union(x,x),X)=union(x,X)
+
+goal g76 : union(a,union(b,a)) = union(a,b)
+
+
+
+(* status: Valid *)
+logic a,b :int
+logic ac f : int,int -> int
+axiom idem : forall x,X: int. f (f(x,x),X)=f(x,X)
+
+goal g77 :
+ f(a,f(b,a)) = f(a,b)
+
+
+
+(* status: Valid *)
+
+logic a,b :int
+logic ac f : int,int -> int
+
+axiom idem : forall x,X: int. f (f(x,x),X)=f(x,X)
+
+goal g78 :
+ f(f(a,f(a,f(b,a))),f(a,b)) = f(f(a,b),f(b,b))
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,d,beta,gamma : int
+
+goal g79 :
+ f(a,b) = gamma -> (* 1 *)
+ f(a,d) = beta -> (* 2 *)
+ f(a,c) = gamma -> (* 3 *)
+ f(b,c) = beta -> (* 4 *)
+
+ f(gamma , d) = f(beta , b) (* 1 & 2 *)
+and f(gamma , c) = f(gamma , b) (* 1 & 3 *)
+and f(gamma , c) = f(beta , a) (* 1 & 4 *)
+and f(beta , c) = f(gamma , d) (* 2 & 3 *)
+and true (* 2 & 4 *)
+and f(gamma , b) = f(beta , a) (* 3 & 4 *)
+
+
+(* status: Valid *)
+
+logic a,b,c,d, x, y , beta , gamma : int
+
+logic ac f : int,int -> int
+
+goal g80 :
+ (*1*) f(f(a,b),c) = gamma ->
+ (*2*) f(a,b) = x ->
+ (*3*) f(x,y) = beta ->
+ (*4*) f(gamma,y) = f(beta,c)
+
+
+(* status: Valid *)
+
+logic ac f : int,int -> int
+logic a,b,c,beta,gamma : int
+
+goal g81 :
+ f(a,f(b,c)) = gamma ->
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(beta,gamma) = f(a,gamma)
+
+
+(* status: Valid *)
+
+logic a,b,c,d,e,gamma,beta:int
+logic ac f,g : int,int -> int
+
+goal g82 :
+ f(f(a,a),f(a,b)) = f(f(a,a),b)->
+ f(a,b) = gamma ->
+ f(a,c) = beta ->
+ f(gamma,c) = f(beta,b)
+*)
+
+
+
+
+(*
+ case_split
+ La fonctionnalité à vérifier est que l'algorithme CC(X) implémente bien ses spécifications et que Alt-Ergo est capable de prouver des buts demandant un raisonnement par analyse par cas.
+*)
+
+(*deactivated
+(* status: Valid *)
+goal g1 : forall x,y,z:int.
+ -z <= 0 ->
+ 3 * y - 8*x - 6 <= 0 ->
+ -y + 12*x +3 <= 0 ->
+ y*y*y <= 1
+
+
+(* status: Valid *)
+goal g2 : forall x,y,z:int.
+ 3 * y - 8*x - 6 <= 0 ->
+ -y + 12*x +3 <= 0 ->
+ -y*y*y <= 0 ->
+ false
+*)
+
+
+
+
+
+(*
+ cc-false
+ La fonctionnalité à vérifier est que l'algorithme CC(X) implémente bien ses spécifications et que Alt-Ergo ne prouve pas des buts faux faisant intervenir de l'égalité et des symboles de fonction non interprétés.
+*)
+
+
+(* status: Unknown *)
+type t
+logic a,b,c,d,e: t
+logic f,h : 'a -> 'a
+logic g: 'a , 'a -> 'a
+
+goal g1:
+ forall x:t. h(x)=x and g(a,x)=a -> g(g(x,g(a,h(x))),x)=a
+
+(*deactivated
+(* status: Unknown *)
+type t
+logic a,b,c,d,e,f: t
+
+goal g2:
+ a=c and c=e and a<>b and b=f and d <> b -> c<>d
+*)
+
+(* status: Unknown *)
+type t
+logic a,b,c,d,e: t
+logic f : 'a -> 'a
+logic g,h: 'a , 'a -> 'a
+
+goal g3:
+ forall x,y:t. f(f(f(a)))=a and f(f(f(f(f(f(a))))))=a and g(x,y)=x ->
+ h(g(g(x,y),y),a)=h(x,f(a))
+
+
+(*deactivated
+(* status: Unknown *)
+logic P,Q: int -> prop
+logic f: int -> int
+axiom a :
+ forall x:int[P(f(x))].
+ P(f(x)) -> Q(x)
+goal g4:
+ forall a,b,c:int.
+ P(a) -> a= f(b) -> a = f(f(c)) ->
+ Q(b) and Q(c)
+*)
+
+
+(*deactivated
+(* ac-false
+ La fonctionnalité à vérifier est que l'algorithme AC(X) implémente bien ses spécifications et que Alt-Ergo ne prouve pas des buts faux faisant intervenir de l'égalité et des symboles associatifs-commutatifs.
+*)
+
+(* status: Unknown *)
+
+logic a,b,c,gamma,beta,x : int
+logic ac f : int , int -> int
+
+goal g2 :
+ f(a,b) = f(x,gamma) ->
+ f(a,c) = f(x,beta) ->
+ f(gamma,c) = f(beta,b)
+
+
+(* status: Unknown *)
+
+logic a,b,c,gamma,beta,x,u,v : int
+logic f : int , int -> int
+
+goal g3 :
+ f(a,b) = u ->
+ f(a,c) = v ->
+ f(x,gamma) = u ->
+ f(x,beta) = v ->
+ f(gamma,c) = f(beta,b)
+
+
+(* status: Unknown *)
+
+logic a,b,c,gamma,beta,x,y: int
+logic ac f : int , int -> int
+
+goal g4 :
+ f(a,b) = f(x,gamma) ->
+ f(a,c) = f(x,beta) ->
+ f(x,f(gamma,c)) = f(y,f(beta,b))
+
+*)
\ No newline at end of file
diff --git a/tests/tests_arith.ml b/tests/tests_arith.ml
index 7096168a7..6850a20d2 100644
--- a/tests/tests_arith.ml
+++ b/tests/tests_arith.ml
@@ -108,7 +108,12 @@ let basic = "Basic" >::: ["a+1 = b+1 => a = b " >:: solve1;
]
-let tests = TestList [basic]
+let files = ["tests/tests_altergo_arith.split"]
+
+let altergo = TestList (List.map Tests_lib.test_split files)
+
+
+let tests = TestList [basic;altergo]
end
diff --git a/tests/tests_lib.ml b/tests/tests_lib.ml
new file mode 100644
index 000000000..be92fa9d9
--- /dev/null
+++ b/tests/tests_lib.ml
@@ -0,0 +1,23 @@
+open OUnit
+
+let test_file s =
+ s >::
+ fun () ->
+ let d = Popop_of_altergo.read_file s in
+ assert_bool "" (Popop_of_altergo.check_goal d)
+
+
+let test_split s =
+ s >::: begin
+ let l = Popop_of_altergo.read_split s in
+ List.map (fun (res,loc,d) ->
+ (Pp.string_of Loc.gen_report_position loc) >::
+ fun () ->
+ let b = (Popop_of_altergo.check_goal d) in
+ match res with
+ | "Valid" -> assert_bool "" b
+ | "Unknown" -> assert_bool "" (not b)
+ | _ -> invalid_arg "Unknown status"
+
+ ) l
+ end
diff --git a/tests/tests_uf.ml b/tests/tests_uf.ml
index 2b0fa8313..e726e2c8f 100644
--- a/tests/tests_uf.ml
+++ b/tests/tests_uf.ml
@@ -149,6 +149,11 @@ let altergo2 =
let altergo = "altergo tests" >::: [altergo1; altergo2]
+let files = ["tests/tests_altergo_qualif.split"]
+
+let altergo = TestList (List.map Tests_lib.test_split files)
+
+
let tests = TestList [basic;congru1;congru2;altergo]
end
--
GitLab