summaryrefslogtreecommitdiff
path: root/contrib/dp
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/dp')
-rw-r--r--contrib/dp/Dp.v120
-rw-r--r--contrib/dp/TODO24
-rw-r--r--contrib/dp/dp.ml991
-rw-r--r--contrib/dp/dp.mli20
-rw-r--r--contrib/dp/dp_gappa.ml445
-rw-r--r--contrib/dp/dp_why.ml151
-rw-r--r--contrib/dp/dp_why.mli17
-rw-r--r--contrib/dp/dp_zenon.mli7
-rw-r--r--contrib/dp/dp_zenon.mll181
-rw-r--r--contrib/dp/fol.mli55
-rw-r--r--contrib/dp/g_dp.ml479
-rw-r--r--contrib/dp/test2.v80
-rw-r--r--contrib/dp/test_gappa.v91
-rw-r--r--contrib/dp/tests.v288
-rw-r--r--contrib/dp/zenon.v94
15 files changed, 0 insertions, 2643 deletions
diff --git a/contrib/dp/Dp.v b/contrib/dp/Dp.v
deleted file mode 100644
index 857c182c..00000000
--- a/contrib/dp/Dp.v
+++ /dev/null
@@ -1,120 +0,0 @@
-(* Calls to external decision procedures *)
-
-Require Export ZArith.
-Require Export Classical.
-
-(* Zenon *)
-
-(* Copyright 2004 INRIA *)
-(* $Id: Dp.v 10739 2008-04-01 14:45:20Z herbelin $ *)
-
-Lemma zenon_nottrue :
- (~True -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_noteq : forall (T : Type) (t : T),
- ((t <> t) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_and : forall P Q : Prop,
- (P -> Q -> False) -> (P /\ Q -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_or : forall P Q : Prop,
- (P -> False) -> (Q -> False) -> (P \/ Q -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_imply : forall P Q : Prop,
- (~P -> False) -> (Q -> False) -> ((P -> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_equiv : forall P Q : Prop,
- (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notand : forall P Q : Prop,
- (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notor : forall P Q : Prop,
- (~P -> ~Q -> False) -> (~(P \/ Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notimply : forall P Q : Prop,
- (P -> ~Q -> False) -> (~(P -> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notequiv : forall P Q : Prop,
- (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_ex : forall (T : Type) (P : T -> Prop),
- (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T),
- ((P t) -> False) -> ((forall x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T),
- (~(P t) -> False) -> (~(exists x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_notall : forall (T : Type) (P : T -> Prop),
- (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
-Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed.
-
-Lemma zenon_equal_base : forall (T : Type) (f : T), f = f.
-Proof. auto. Qed.
-
-Lemma zenon_equal_step :
- forall (S T : Type) (fa fb : S -> T) (a b : S),
- (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)).
-Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed.
-
-Lemma zenon_pnotp : forall P Q : Prop,
- (P = Q) -> (P -> ~Q -> False).
-Proof. intros P Q Ha. rewrite Ha. auto. Qed.
-
-Lemma zenon_notequal : forall (T : Type) (a b : T),
- (a = b) -> (a <> b -> False).
-Proof. auto. Qed.
-
-Ltac zenon_intro id :=
- intro id || let nid := fresh in (intro nid; clear nid)
-.
-
-Definition zenon_and_s := fun P Q a b => zenon_and P Q b a.
-Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a.
-Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a.
-Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a.
-Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a.
-Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a.
-Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a.
-Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a.
-Definition zenon_ex_s := fun T P a b => zenon_ex T P b a.
-Definition zenon_notall_s := fun T P a b => zenon_notall T P b a.
-
-Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b.
-Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.
-
-(* Ergo *)
-
-Set Implicit Arguments.
-Section congr.
- Variable t:Type.
-Lemma ergo_eq_concat_1 :
- forall (P:t -> Prop) (x y:t),
- P x -> x = y -> P y.
-Proof.
- intros; subst; auto.
-Qed.
-
-Lemma ergo_eq_concat_2 :
- forall (P:t -> t -> Prop) (x1 x2 y1 y2:t),
- P x1 x2 -> x1 = y1 -> x2 = y2 -> P y1 y2.
-Proof.
- intros; subst; auto.
-Qed.
-
-End congr.
diff --git a/contrib/dp/TODO b/contrib/dp/TODO
deleted file mode 100644
index 44349e21..00000000
--- a/contrib/dp/TODO
+++ /dev/null
@@ -1,24 +0,0 @@
-
-TODO
-----
-
-- axiomes pour les prédicats récursifs comme
-
- Fixpoint even (n:nat) : Prop :=
- match n with
- O => True
- | S O => False
- | S (S p) => even p
- end.
-
- ou encore In sur les listes du module Coq List.
-
-- discriminate
-
-- inversion (Set et Prop)
-
-
-BUGS
-----
-
-
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
deleted file mode 100644
index d8803847..00000000
--- a/contrib/dp/dp.ml
+++ /dev/null
@@ -1,991 +0,0 @@
-(* Authors: Nicolas Ayache and Jean-Christophe Filliâtre *)
-(* Tactics to call decision procedures *)
-
-(* Works in two steps:
-
- - first the Coq context and the current goal are translated in
- Polymorphic First-Order Logic (see fol.mli in this directory)
-
- - then the resulting query is passed to the Why tool that translates
- it to the syntax of the selected prover (Simplify, CVC Lite, haRVey,
- Zenon)
-*)
-
-open Util
-open Pp
-open Libobject
-open Summary
-open Term
-open Tacmach
-open Tactics
-open Tacticals
-open Fol
-open Names
-open Nameops
-open Termops
-open Coqlib
-open Hipattern
-open Libnames
-open Declarations
-open Dp_why
-
-let debug = ref false
-let set_debug b = debug := b
-let trace = ref false
-let set_trace b = trace := b
-let timeout = ref 10
-let set_timeout n = timeout := n
-
-let (dp_timeout_obj,_) =
- declare_object
- {(default_object "Dp_timeout") with
- cache_function = (fun (_,x) -> set_timeout x);
- load_function = (fun _ (_,x) -> set_timeout x);
- export_function = (fun x -> Some x)}
-
-let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
-
-let (dp_debug_obj,_) =
- declare_object
- {(default_object "Dp_debug") with
- cache_function = (fun (_,x) -> set_debug x);
- load_function = (fun _ (_,x) -> set_debug x);
- export_function = (fun x -> Some x)}
-
-let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
-
-let (dp_trace_obj,_) =
- declare_object
- {(default_object "Dp_trace") with
- cache_function = (fun (_,x) -> set_trace x);
- load_function = (fun _ (_,x) -> set_trace x);
- export_function = (fun x -> Some x)}
-
-let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x)
-
-let logic_dir = ["Coq";"Logic";"Decidable"]
-let coq_modules =
- init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
- @ [["Coq"; "ZArith"; "BinInt"]]
- @ [["Coq"; "omega"; "OmegaLemmas"]]
-
-let constant = gen_constant_in_modules "dp" coq_modules
-
-let coq_Z = lazy (constant "Z")
-let coq_Zplus = lazy (constant "Zplus")
-let coq_Zmult = lazy (constant "Zmult")
-let coq_Zopp = lazy (constant "Zopp")
-let coq_Zminus = lazy (constant "Zminus")
-let coq_Zdiv = lazy (constant "Zdiv")
-let coq_Zs = lazy (constant "Zs")
-let coq_Zgt = lazy (constant "Zgt")
-let coq_Zle = lazy (constant "Zle")
-let coq_Zge = lazy (constant "Zge")
-let coq_Zlt = lazy (constant "Zlt")
-let coq_Z0 = lazy (constant "Z0")
-let coq_Zpos = lazy (constant "Zpos")
-let coq_Zneg = lazy (constant "Zneg")
-let coq_xH = lazy (constant "xH")
-let coq_xI = lazy (constant "xI")
-let coq_xO = lazy (constant "xO")
-let coq_iff = lazy (constant "iff")
-
-(* not Prop typed expressions *)
-exception NotProp
-
-(* not first-order expressions *)
-exception NotFO
-
-(* Renaming of Coq globals *)
-
-let global_names = Hashtbl.create 97
-let used_names = Hashtbl.create 97
-
-let rename_global r =
- try
- Hashtbl.find global_names r
- with Not_found ->
- let rec loop id =
- if Hashtbl.mem used_names id then
- loop (lift_ident id)
- else begin
- Hashtbl.add used_names id ();
- let s = string_of_id id in
- Hashtbl.add global_names r s;
- s
- end
- in
- loop (Nametab.id_of_global r)
-
-let foralls =
- List.fold_right
- (fun (x,t) p -> Forall (x, t, p))
-
-let fresh_var = function
- | Anonymous -> rename_global (VarRef (id_of_string "x"))
- | Name x -> rename_global (VarRef x)
-
-(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of
- env names, and returns the new variables together with the new
- environment *)
-let coq_rename_vars env vars =
- let avoid = ref (ids_of_named_context (Environ.named_context env)) in
- List.fold_right
- (fun (na,t) (newvars, newenv) ->
- let id = next_name_away na !avoid in
- avoid := id :: !avoid;
- id :: newvars, Environ.push_named (id, None, t) newenv)
- vars ([],env)
-
-(* extract the prenex type quantifications i.e.
- type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *)
-let decomp_type_quantifiers env t =
- let rec loop vars t = match kind_of_term t with
- | Prod (n, a, t) when is_Set a || is_Type a ->
- loop ((n,a) :: vars) t
- | _ ->
- let vars, env = coq_rename_vars env vars in
- let t = substl (List.map mkVar vars) t in
- List.rev vars, env, t
- in
- loop [] t
-
-(* same thing with lambda binders (for axiomatize body) *)
-let decomp_type_lambdas env t =
- let rec loop vars t = match kind_of_term t with
- | Lambda (n, a, t) when is_Set a || is_Type a ->
- loop ((n,a) :: vars) t
- | _ ->
- let vars, env = coq_rename_vars env vars in
- let t = substl (List.map mkVar vars) t in
- List.rev vars, env, t
- in
- loop [] t
-
-let decompose_arrows =
- let rec arrows_rec l c = match kind_of_term c with
- | Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c
- | Cast (c,_,_) -> arrows_rec l c
- | _ -> List.rev l, c
- in
- arrows_rec []
-
-let rec eta_expanse t vars env i =
- assert (i >= 0);
- if i = 0 then
- t, vars, env
- else
- match kind_of_term (Typing.type_of env Evd.empty t) with
- | Prod (n, a, b) when not (dependent (mkRel 1) b) ->
- let avoid = ids_of_named_context (Environ.named_context env) in
- let id = next_name_away n avoid in
- let env' = Environ.push_named (id, None, a) env in
- let t' = mkApp (t, [| mkVar id |]) in
- eta_expanse t' (id :: vars) env' (pred i)
- | _ ->
- assert false
-
-let rec skip_k_args k cl = match k, cl with
- | 0, _ -> cl
- | _, _ :: cl -> skip_k_args (k-1) cl
- | _, [] -> raise NotFO
-
-(* Coq global references *)
-
-type global = Gnot_fo | Gfo of Fol.decl
-
-let globals = ref Refmap.empty
-let globals_stack = ref []
-
-(* synchronization *)
-let () =
- Summary.declare_summary "Dp globals"
- { Summary.freeze_function = (fun () -> !globals, !globals_stack);
- Summary.unfreeze_function =
- (fun (g,s) -> globals := g; globals_stack := s);
- Summary.init_function = (fun () -> ());
- Summary.survive_module = false;
- Summary.survive_section = false }
-
-let add_global r d = globals := Refmap.add r d !globals
-let mem_global r = Refmap.mem r !globals
-let lookup_global r = match Refmap.find r !globals with
- | Gnot_fo -> raise NotFO
- | Gfo d -> d
-
-let locals = Hashtbl.create 97
-
-let lookup_local r = match Hashtbl.find locals r with
- | Gnot_fo -> raise NotFO
- | Gfo d -> d
-
-let iter_all_constructors i f =
- let _, oib = Global.lookup_inductive i in
- Array.iteri
- (fun j tj -> f j (mkConstruct (i, j+1)))
- oib.mind_nf_lc
-
-
-(* injection c [t1,...,tn] adds the injection axiom
- forall x1:t1,...,xn:tn,y1:t1,...,yn:tn.
- c(x1,...,xn)=c(y1,...,yn) -> x1=y1 /\ ... /\ xn=yn *)
-
-let injection c l =
- let i = ref 0 in
- let var s = incr i; id_of_string (s ^ string_of_int !i) in
- let xl = List.map (fun t -> rename_global (VarRef (var "x")), t) l in
- i := 0;
- let yl = List.map (fun t -> rename_global (VarRef (var "y")), t) l in
- let f =
- List.fold_right2
- (fun (x,_) (y,_) p -> And (Fatom (Eq (App (x,[]),App (y,[]))), p))
- xl yl True
- in
- let vars = List.map (fun (x,_) -> App(x,[])) in
- let f = Imp (Fatom (Eq (App (c, vars xl), App (c, vars yl))), f) in
- let foralls = List.fold_right (fun (x,t) p -> Forall (x, t, p)) in
- let f = foralls xl (foralls yl f) in
- let ax = Axiom ("injection_" ^ c, f) in
- globals_stack := ax :: !globals_stack
-
-(* rec_names_for c [|n1;...;nk|] builds the list of constant names for
- identifiers n1...nk with the same path as c, if they exist; otherwise
- raises Not_found *)
-let rec_names_for c =
- let mp,dp,_ = Names.repr_con c in
- array_map_to_list
- (function
- | Name id ->
- let c' = Names.make_con mp dp (label_of_id id) in
- ignore (Global.lookup_constant c');
- msgnl (Printer.pr_constr (mkConst c'));
- c'
- | Anonymous ->
- raise Not_found)
-
-(* abstraction tables *)
-
-let term_abstractions = Hashtbl.create 97
-
-let new_abstraction =
- let r = ref 0 in fun () -> incr r; "abstraction_" ^ string_of_int !r
-
-(* Arithmetic constants *)
-
-exception NotArithConstant
-
-(* translates a closed Coq term p:positive into a FOL term of type int *)
-let rec tr_positive p = match kind_of_term p with
- | Term.Construct _ when p = Lazy.force coq_xH ->
- Cst 1
- | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
- Plus (Mult (Cst 2, tr_positive a), Cst 1)
- | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
- Mult (Cst 2, tr_positive a)
- | Term.Cast (p, _, _) ->
- tr_positive p
- | _ ->
- raise NotArithConstant
-
-(* translates a closed Coq term t:Z into a FOL term of type int *)
-let rec tr_arith_constant t = match kind_of_term t with
- | Term.Construct _ when t = Lazy.force coq_Z0 ->
- Cst 0
- | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos ->
- tr_positive a
- | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
- Moins (Cst 0, tr_positive a)
- | Term.Cast (t, _, _) ->
- tr_arith_constant t
- | _ ->
- raise NotArithConstant
-
-(* translate a Coq term t:Set into a FOL type expression;
- tv = list of type variables *)
-and tr_type tv env t =
- let t = Reductionops.nf_betadeltaiota env Evd.empty t in
- if t = Lazy.force coq_Z then
- Tid ("int", [])
- else match kind_of_term t with
- | Var x when List.mem x tv ->
- Tvar (string_of_id x)
- | _ ->
- let f, cl = decompose_app t in
- begin try
- let r = global_of_constr f in
- match tr_global env r with
- | DeclType (id, k) ->
- assert (k = List.length cl); (* since t:Set *)
- Tid (id, List.map (tr_type tv env) cl)
- | _ ->
- raise NotFO
- with
- | Not_found ->
- raise NotFO
- | NotFO ->
- (* we need to abstract some part of (f cl) *)
- (*TODO*)
- raise NotFO
- end
-
-and make_term_abstraction tv env c =
- let ty = Typing.type_of env Evd.empty c in
- let id = new_abstraction () in
- match tr_decl env id ty with
- | DeclFun (id,_,_,_) as d ->
- begin try
- Hashtbl.find term_abstractions c
- with Not_found ->
- Hashtbl.add term_abstractions c id;
- globals_stack := d :: !globals_stack;
- id
- end
- | _ ->
- raise NotFO
-
-(* translate a Coq declaration id:ty in a FOL declaration, that is either
- - a type declaration : DeclType (id, n) where n:int is the type arity
- - a function declaration : DeclFun (id, tl, t) ; that includes constants
- - a predicate declaration : DeclPred (id, tl)
- - an axiom : Axiom (id, p)
- *)
-and tr_decl env id ty =
- let tv, env, t = decomp_type_quantifiers env ty in
- if is_Set t || is_Type t then
- DeclType (id, List.length tv)
- else if is_Prop t then
- DeclPred (id, List.length tv, [])
- else
- let s = Typing.type_of env Evd.empty t in
- if is_Prop s then
- Axiom (id, tr_formula tv [] env t)
- else
- let l, t = decompose_arrows t in
- let l = List.map (tr_type tv env) l in
- if is_Prop t then
- DeclPred(id, List.length tv, l)
- else
- let s = Typing.type_of env Evd.empty t in
- if is_Set s || is_Type s then
- DeclFun (id, List.length tv, l, tr_type tv env t)
- else
- raise NotFO
-
-(* tr_global(r) = tr_decl(id(r),typeof(r)) + a cache mechanism *)
-and tr_global env r = match r with
- | VarRef id ->
- lookup_local id
- | r ->
- try
- lookup_global r
- with Not_found ->
- try
- let ty = Global.type_of_global r in
- let id = rename_global r in
- let d = tr_decl env id ty in
- (* r can be already declared if it is a constructor *)
- if not (mem_global r) then begin
- add_global r (Gfo d);
- globals_stack := d :: !globals_stack
- end;
- begin try axiomatize_body env r id d with NotFO -> () end;
- d
- with NotFO ->
- add_global r Gnot_fo;
- raise NotFO
-
-and axiomatize_body env r id d = match r with
- | VarRef _ ->
- assert false
- | ConstRef c ->
- begin match (Global.lookup_constant c).const_body with
- | Some b ->
- let b = force b in
- let axioms =
- (match d with
- | DeclPred (id, _, []) ->
- let tv, env, b = decomp_type_lambdas env b in
- let value = tr_formula tv [] env b in
- [id, Iff (Fatom (Pred (id, [])), value)]
- | DeclFun (id, _, [], _) ->
- let tv, env, b = decomp_type_lambdas env b in
- let value = tr_term tv [] env b in
- [id, Fatom (Eq (Fol.App (id, []), value))]
- | DeclFun (id, _, l, _) | DeclPred (id, _, l) ->
- (*Format.eprintf "axiomatize_body %S@." id;*)
- let b = match kind_of_term b with
- (* a single recursive function *)
- | Fix (_, (_,_,[|b|])) ->
- subst1 (mkConst c) b
- (* mutually recursive functions *)
- | Fix ((_,i), (names,_,bodies)) ->
- (* we only deal with named functions *)
- begin try
- let l = rec_names_for c names in
- substl (List.rev_map mkConst l) bodies.(i)
- with Not_found ->
- b
- end
- | _ ->
- b
- in
- let tv, env, b = decomp_type_lambdas env b in
- let vars, t = decompose_lam b in
- let n = List.length l in
- let k = List.length vars in
- assert (k <= n);
- let vars, env = coq_rename_vars env vars in
- let t = substl (List.map mkVar vars) t in
- let t, vars, env = eta_expanse t vars env (n-k) in
- let vars = List.rev vars in
- let bv = vars in
- let vars = List.map (fun x -> string_of_id x) vars in
- let fol_var x = Fol.App (x, []) in
- let fol_vars = List.map fol_var vars in
- let vars = List.combine vars l in
- begin match d with
- | DeclFun (_, _, _, ty) ->
- begin match kind_of_term t with
- | Case (ci, _, e, br) ->
- equations_for_case env id vars tv bv ci e br
- | _ ->
- let t = tr_term tv bv env t in
- let ax =
- add_proof (Fun_def (id, vars, ty, t))
- in
- let p = Fatom (Eq (App (id, fol_vars), t)) in
- [ax, foralls vars p]
- end
- | DeclPred _ ->
- let value = tr_formula tv bv env t in
- let p = Iff (Fatom (Pred (id, fol_vars)), value) in
- [id, foralls vars p]
- | _ ->
- assert false
- end
- | DeclType _ ->
- raise NotFO
- | Axiom _ -> assert false)
- in
- let axioms = List.map (fun (id,ax) -> Axiom (id, ax)) axioms in
- globals_stack := axioms @ !globals_stack
- | None ->
- () (* Coq axiom *)
- end
- | IndRef i ->
- iter_all_constructors i
- (fun _ c ->
- let rc = global_of_constr c in
- try
- begin match tr_global env rc with
- | DeclFun (_, _, [], _) -> ()
- | DeclFun (idc, _, al, _) -> injection idc al
- | _ -> ()
- end
- with NotFO ->
- ())
- | _ -> ()
-
-and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
- | Var x when List.exists (fun (y, _) -> string_of_id x = y) vars ->
- let eqs = ref [] in
- iter_all_constructors ci.ci_ind
- (fun j cj ->
- try
- let cjr = global_of_constr cj in
- begin match tr_global env cjr with
- | DeclFun (idc, _, l, _) ->
- let b = br.(j) in
- let rec_vars, b = decompose_lam b in
- let rec_vars, env = coq_rename_vars env rec_vars in
- let coq_rec_vars = List.map mkVar rec_vars in
- let b = substl coq_rec_vars b in
- let rec_vars = List.rev rec_vars in
- let coq_rec_term = applist (cj, List.rev coq_rec_vars) in
- let b = replace_vars [x, coq_rec_term] b in
- let bv = bv @ rec_vars in
- let rec_vars = List.map string_of_id rec_vars in
- let fol_var x = Fol.App (x, []) in
- let fol_rec_vars = List.map fol_var rec_vars in
- let fol_rec_term = App (idc, fol_rec_vars) in
- let rec_vars = List.combine rec_vars l in
- let fol_vars = List.map fst vars in
- let fol_vars = List.map fol_var fol_vars in
- let fol_vars = List.map (fun y -> match y with
- | App (id, _) ->
- if id = string_of_id x
- then fol_rec_term
- else y
- | _ -> y)
- fol_vars in
- let vars = vars @ rec_vars in
- let rec remove l e = match l with
- | [] -> []
- | (y, t)::l' -> if y = string_of_id e then l'
- else (y, t)::(remove l' e) in
- let vars = remove vars x in
- let p =
- Fatom (Eq (App (id, fol_vars),
- tr_term tv bv env b))
- in
- eqs := (id ^ "_" ^ idc, foralls vars p) :: !eqs
- | _ ->
- assert false end
- with NotFO ->
- ());
- !eqs
- | _ ->
- raise NotFO
-
-(* assumption: t:T:Set *)
-and tr_term tv bv env t = match kind_of_term t with
- | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus ->
- Plus (tr_term tv bv env a, tr_term tv bv env b)
- | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus ->
- Moins (tr_term tv bv env a, tr_term tv bv env b)
- | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult ->
- Mult (tr_term tv bv env a, tr_term tv bv env b)
- | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv ->
- Div (tr_term tv bv env a, tr_term tv bv env b)
- | Term.Var id when List.mem id bv ->
- App (string_of_id id, [])
- | _ ->
- try
- tr_arith_constant t
- with NotArithConstant ->
- let f, cl = decompose_app t in
- begin try
- let r = global_of_constr f in
- match tr_global env r with
- | DeclFun (s, k, _, _) ->
- let cl = skip_k_args k cl in
- Fol.App (s, List.map (tr_term tv bv env) cl)
- | _ ->
- raise NotFO
- with
- | Not_found ->
- raise NotFO
- | NotFO -> (* we need to abstract some part of (f cl) *)
- let rec abstract app = function
- | [] ->
- Fol.App (make_term_abstraction tv env app, [])
- | x :: l as args ->
- begin try
- let s = make_term_abstraction tv env app in
- Fol.App (s, List.map (tr_term tv bv env) args)
- with NotFO ->
- abstract (applist (app, [x])) l
- end
- in
- let app,l = match cl with
- | x :: l -> applist (f, [x]), l | [] -> raise NotFO
- in
- abstract app l
- end
-
-and quantifiers n a b tv bv env =
- let vars, env = coq_rename_vars env [n,a] in
- let id = match vars with [x] -> x | _ -> assert false in
- let b = subst1 (mkVar id) b in
- let t = tr_type tv env a in
- let bv = id :: bv in
- id, t, bv, env, b
-
-(* assumption: f is of type Prop *)
-and tr_formula tv bv env f =
- let c, args = decompose_app f in
- match kind_of_term c, args with
- | Var id, [] ->
- Fatom (Pred (rename_global (VarRef id), []))
- | _, [t;a;b] when c = build_coq_eq () ->
- let ty = Typing.type_of env Evd.empty t in
- if is_Set ty || is_Type ty then
- let _ = tr_type tv env t in
- Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b))
- else
- raise NotFO
- | _, [a;b] when c = Lazy.force coq_Zle ->
- Fatom (Le (tr_term tv bv env a, tr_term tv bv env b))
- | _, [a;b] when c = Lazy.force coq_Zlt ->
- Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b))
- | _, [a;b] when c = Lazy.force coq_Zge ->
- Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b))
- | _, [a;b] when c = Lazy.force coq_Zgt ->
- Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b))
- | _, [] when c = build_coq_False () ->
- False
- | _, [] when c = build_coq_True () ->
- True
- | _, [a] when c = build_coq_not () ->
- Not (tr_formula tv bv env a)
- | _, [a;b] when c = build_coq_and () ->
- And (tr_formula tv bv env a, tr_formula tv bv env b)
- | _, [a;b] when c = build_coq_or () ->
- Or (tr_formula tv bv env a, tr_formula tv bv env b)
- | _, [a;b] when c = Lazy.force coq_iff ->
- Iff (tr_formula tv bv env a, tr_formula tv bv env b)
- | Prod (n, a, b), _ ->
- if is_imp_term f then
- Imp (tr_formula tv bv env a, tr_formula tv bv env b)
- else
- let id, t, bv, env, b = quantifiers n a b tv bv env in
- Forall (string_of_id id, t, tr_formula tv bv env b)
- | _, [_; a] when c = build_coq_ex () ->
- begin match kind_of_term a with
- | Lambda(n, a, b) ->
- let id, t, bv, env, b = quantifiers n a b tv bv env in
- Exists (string_of_id id, t, tr_formula tv bv env b)
- | _ ->
- (* unusual case of the shape (ex p) *)
- raise NotFO (* TODO: we could eta-expanse *)
- end
- | _ ->
- begin try
- let r = global_of_constr c in
- match tr_global env r with
- | DeclPred (s, k, _) ->
- let args = skip_k_args k args in
- Fatom (Pred (s, List.map (tr_term tv bv env) args))
- | _ ->
- raise NotFO
- with Not_found ->
- raise NotFO
- end
-
-
-let tr_goal gl =
- Hashtbl.clear locals;
- let tr_one_hyp (id, ty) =
- try
- let s = rename_global (VarRef id) in
- let d = tr_decl (pf_env gl) s ty in
- Hashtbl.add locals id (Gfo d);
- d
- with NotFO ->
- Hashtbl.add locals id Gnot_fo;
- raise NotFO
- in
- let hyps =
- List.fold_right
- (fun h acc -> try tr_one_hyp h :: acc with NotFO -> acc)
- (pf_hyps_types gl) []
- in
- let c = tr_formula [] [] (pf_env gl) (pf_concl gl) in
- let hyps = List.rev_append !globals_stack (List.rev hyps) in
- hyps, c
-
-
-type prover = Simplify | Ergo | Yices | CVCLite | Harvey | Zenon | Gwhy
-
-let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ())
-
-let sprintf = Format.sprintf
-
-let file_contents f =
- let buf = Buffer.create 1024 in
- try
- let c = open_in f in
- begin try
- while true do
- let s = input_line c in Buffer.add_string buf s;
- Buffer.add_char buf '\n'
- done;
- assert false
- with End_of_file ->
- close_in c;
- Buffer.contents buf
- end
- with _ ->
- sprintf "(cannot open %s)" f
-
-let timeout_sys_command cmd =
- if !debug then Format.eprintf "command line: %s@." cmd;
- let out = Filename.temp_file "out" "" in
- let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in
- let ret = Sys.command cmd in
- if !debug then
- Format.eprintf "Output file %s:@.%s@." out (file_contents out);
- ret, out
-
-let timeout_or_failure c cmd out =
- if c = 152 then
- Timeout
- else
- Failure
- (sprintf "command %s failed with output:\n%s " cmd (file_contents out))
-
-let prelude_files = ref ([] : string list)
-
-let set_prelude l = prelude_files := l
-
-let (dp_prelude_obj,_) =
- declare_object
- {(default_object "Dp_prelude") with
- cache_function = (fun (_,x) -> set_prelude x);
- load_function = (fun _ (_,x) -> set_prelude x);
- export_function = (fun x -> Some x)}
-
-let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x)
-
-let why_files f = String.concat " " (!prelude_files @ [f])
-
-let call_simplify fwhy =
- let cmd =
- sprintf "why --simplify %s" (why_files fwhy)
- in
- if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
- let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
- let cmd =
- sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out"
- !timeout fsx
- in
- let out = Sys.command cmd in
- let r =
- if out = 0 then Valid None else if out = 1 then Invalid else Timeout
- in
- if not !debug then remove_files [fwhy; fsx];
- r
-
-let call_ergo fwhy =
- let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in
- if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
- let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
- let ftrace = Filename.temp_file "ergo_trace" "" in
- let cmd =
- if !trace then
- sprintf "ergo -cctrace %s %s" ftrace fwhy
- else
- sprintf "ergo %s" fwhy
- in
- let ret,out = timeout_sys_command cmd in
- let r =
- if ret <> 0 then
- timeout_or_failure ret cmd out
- else if Sys.command (sprintf "grep -q -w Valid %s" out) = 0 then
- Valid (if !trace then Some ftrace else None)
- else if Sys.command (sprintf "grep -q -w \"I don't know\" %s" out) = 0 then
- DontKnow
- else if Sys.command (sprintf "grep -q -w \"Invalid\" %s" out) = 0 then
- Invalid
- else
- Failure ("command failed: " ^ cmd)
- in
- if not !debug then remove_files [fwhy; out];
- r
-
-let call_zenon fwhy =
- let cmd =
- sprintf "why --no-prelude --no-zenon-prelude --zenon %s" (why_files fwhy)
- in
- if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
- let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in
- let out = Filename.temp_file "dp_out" "" in
- let cmd =
- sprintf "timeout %d zenon -ocoqterm %s > %s 2>&1" !timeout fznn out
- in
- let c = Sys.command cmd in
- if not !debug then remove_files [fwhy; fznn];
- if c = 137 then
- Timeout
- else begin
- if c <> 0 then anomaly ("command failed: " ^ cmd);
- if Sys.command (sprintf "grep -q -w Error %s" out) = 0 then
- error "Zenon failed";
- let c = Sys.command (sprintf "grep -q PROOF-FOUND %s" out) in
- if c = 0 then Valid (Some out) else Invalid
- end
-
-let call_yices fwhy =
- let cmd =
- sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
- in
- if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
- let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
- let cmd =
- sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out"
- !timeout fsmt
- in
- let out = Sys.command cmd in
- let r =
- if out = 0 then Valid None else if out = 1 then Invalid else Timeout
- in
- if not !debug then remove_files [fwhy; fsmt];
- r
-
-let call_cvcl fwhy =
- let cmd =
- sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy)
- in
- if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
- let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
- let cmd =
- sprintf "timeout %d cvcl < %s > out 2>&1 && grep -q -w Valid out"
- !timeout fcvc
- in
- let out = Sys.command cmd in
- let r =
- if out = 0 then Valid None else if out = 1 then Invalid else Timeout
- in
- if not !debug then remove_files [fwhy; fcvc];
- r
-
-let call_harvey fwhy =
- let cmd =
- sprintf "why --harvey --encoding strat %s" (why_files fwhy)
- in
- if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
- let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
- let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in
- if out <> 0 then anomaly ("call to rvc -e -t " ^ frv ^ " failed");
- let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in
- let outf = Filename.temp_file "rv" ".out" in
- let out =
- Sys.command (sprintf "timeout %d rv -e\"-T 2000\" %s > %s 2>&1"
- !timeout f outf)
- in
- let r =
- if out <> 0 then
- Timeout
- else
- let cmd =
- sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf
- in
- if Sys.command cmd = 0 then Valid None else Invalid
- in
- if not !debug then remove_files [fwhy; frv; outf];
- r
-
-let call_gwhy fwhy =
- let cmd = sprintf "gwhy %s" (why_files fwhy) in
- if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
- NoAnswer
-
-let ergo_proof_from_file f gl =
- let s =
- let buf = Buffer.create 1024 in
- let c = open_in f in
- try
- while true do Buffer.add_string buf (input_line c) done; assert false
- with End_of_file ->
- close_in c;
- Buffer.contents buf
- in
- let parsed_constr = Pcoq.parse_string Pcoq.Constr.constr s in
- let t = Constrintern.interp_constr (project gl) (pf_env gl) parsed_constr in
- exact_check t gl
-
-let call_prover prover q =
- let fwhy = Filename.temp_file "coq_dp" ".why" in
- Dp_why.output_file fwhy q;
- match prover with
- | Simplify -> call_simplify fwhy
- | Ergo -> call_ergo fwhy
- | Yices -> call_yices fwhy
- | Zenon -> call_zenon fwhy
- | CVCLite -> call_cvcl fwhy
- | Harvey -> call_harvey fwhy
- | Gwhy -> call_gwhy fwhy
-
-let dp prover gl =
- Coqlib.check_required_library ["Coq";"ZArith";"ZArith"];
- let concl_type = pf_type_of gl (pf_concl gl) in
- if not (is_Prop concl_type) then error "Conclusion is not a Prop";
- try
- let q = tr_goal gl in
- begin match call_prover prover q with
- | Valid (Some f) when prover = Zenon -> Dp_zenon.proof_from_file f gl
- | Valid (Some f) when prover = Ergo -> ergo_proof_from_file f gl
- | Valid _ -> Tactics.admit_as_an_axiom gl
- | Invalid -> error "Invalid"
- | DontKnow -> error "Don't know"
- | Timeout -> error "Timeout"
- | Failure s -> error s
- | NoAnswer -> Tacticals.tclIDTAC gl
- end
- with NotFO ->
- error "Not a first order goal"
-
-
-let simplify = tclTHEN intros (dp Simplify)
-let ergo = tclTHEN intros (dp Ergo)
-let yices = tclTHEN intros (dp Yices)
-let cvc_lite = tclTHEN intros (dp CVCLite)
-let harvey = dp Harvey
-let zenon = tclTHEN intros (dp Zenon)
-let gwhy = tclTHEN intros (dp Gwhy)
-
-let dp_hint l =
- let env = Global.env () in
- let one_hint (qid,r) =
- if not (mem_global r) then begin
- let ty = Global.type_of_global r in
- let s = Typing.type_of env Evd.empty ty in
- if is_Prop s then
- try
- let id = rename_global r in
- let tv, env, ty = decomp_type_quantifiers env ty in
- let d = Axiom (id, tr_formula tv [] env ty) in
- add_global r (Gfo d);
- globals_stack := d :: !globals_stack
- with NotFO ->
- add_global r Gnot_fo;
- msg_warning
- (pr_reference qid ++
- str " ignored (not a first order proposition)")
- else begin
- add_global r Gnot_fo;
- msg_warning
- (pr_reference qid ++ str " ignored (not a proposition)")
- end
- end
- in
- List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
-
-let (dp_hint_obj,_) =
- declare_object
- {(default_object "Dp_hint") with
- cache_function = (fun (_,l) -> dp_hint l);
- load_function = (fun _ (_,l) -> dp_hint l);
- export_function = (fun x -> Some x)}
-
-let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l)
-
-let dp_predefined qid s =
- let r = Nametab.global qid in
- let ty = Global.type_of_global r in
- let env = Global.env () in
- let id = rename_global r in
- try
- let d = match tr_decl env id ty with
- | DeclType (_, n) -> DeclType (s, n)
- | DeclFun (_, n, tyl, ty) -> DeclFun (s, n, tyl, ty)
- | DeclPred (_, n, tyl) -> DeclPred (s, n, tyl)
- | Axiom _ as d -> d
- in
- match d with
- | Axiom _ -> msg_warning (str " ignored (axiom)")
- | d -> add_global r (Gfo d)
- with NotFO ->
- msg_warning (str " ignored (not a first order declaration)")
-
-let (dp_predefined_obj,_) =
- declare_object
- {(default_object "Dp_predefined") with
- cache_function = (fun (_,(id,s)) -> dp_predefined id s);
- load_function = (fun _ (_,(id,s)) -> dp_predefined id s);
- export_function = (fun x -> Some x)}
-
-let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s))
-
-let _ = declare_summary "Dp options"
- { freeze_function =
- (fun () -> !debug, !trace, !timeout, !prelude_files);
- unfreeze_function =
- (fun (d,tr,tm,pr) ->
- debug := d; trace := tr; timeout := tm; prelude_files := pr);
- init_function =
- (fun () ->
- debug := false; trace := false; timeout := 10;
- prelude_files := []);
- survive_module = true;
- survive_section = true }
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
deleted file mode 100644
index 6dbc05e1..00000000
--- a/contrib/dp/dp.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-
-open Libnames
-open Proof_type
-
-val simplify : tactic
-val ergo : tactic
-val yices : tactic
-val cvc_lite : tactic
-val harvey : tactic
-val zenon : tactic
-val gwhy : tactic
-
-val dp_hint : reference list -> unit
-val dp_timeout : int -> unit
-val dp_debug : bool -> unit
-val dp_trace : bool -> unit
-val dp_prelude : string list -> unit
-val dp_predefined : reference -> string -> unit
-
-
diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml
deleted file mode 100644
index 9c035aa8..00000000
--- a/contrib/dp/dp_gappa.ml
+++ /dev/null
@@ -1,445 +0,0 @@
-
-open Format
-open Util
-open Pp
-open Term
-open Tacmach
-open Tactics
-open Tacticals
-open Names
-open Nameops
-open Termops
-open Coqlib
-open Hipattern
-open Libnames
-open Declarations
-open Evarutil
-
-let debug = ref false
-
-(* 1. gappa syntax trees and output *)
-
-module Constant = struct
-
- open Bigint
-
- type t = { mantissa : bigint; base : int; exp : bigint }
-
- let create (b, m, e) =
- { mantissa = m; base = b; exp = e }
-
- let of_int x =
- { mantissa = x; base = 1; exp = zero }
-
- let print fmt x = match x.base with
- | 1 -> fprintf fmt "%s" (to_string x.mantissa)
- | 2 -> fprintf fmt "%sb%s" (to_string x.mantissa) (to_string x.exp)
- | 10 -> fprintf fmt "%se%s" (to_string x.mantissa) (to_string x.exp)
- | _ -> assert false
-
-end
-
-type binop = Bminus | Bplus | Bmult | Bdiv
-
-type unop = Usqrt | Uabs | Uopp
-
-type rounding_mode = string
-
-type term =
- | Tconst of Constant.t
- | Tvar of string
- | Tbinop of binop * term * term
- | Tunop of unop * term
- | Tround of rounding_mode * term
-
-type pred =
- | Pin of term * Constant.t * Constant.t
-
-let rec print_term fmt = function
- | Tconst c -> Constant.print fmt c
- | Tvar s -> pp_print_string fmt s
- | Tbinop (op, t1, t2) ->
- let op = match op with
- | Bplus -> "+" | Bminus -> "-" | Bmult -> "*" | Bdiv -> "/"
- in
- fprintf fmt "(%a %s %a)" print_term t1 op print_term t2
- | Tunop (Uabs, t) ->
- fprintf fmt "|%a|" print_term t
- | Tunop (Uopp | Usqrt as op, t) ->
- let s = match op with
- | Uopp -> "-" | Usqrt -> "sqrt" | _ -> assert false
- in
- fprintf fmt "(%s(%a))" s print_term t
- | Tround (m, t) ->
- fprintf fmt "(%s(%a))" m print_term t
-
-let print_pred fmt = function
- | Pin (t, c1, c2) ->
- fprintf fmt "%a in [%a, %a]"
- print_term t Constant.print c1 Constant.print c2
-
-let temp_file f = if !debug then f else Filename.temp_file f ".v"
-let remove_file f = if not !debug then try Sys.remove f with _ -> ()
-
-let read_gappa_proof f =
- let buf = Buffer.create 1024 in
- Buffer.add_char buf '(';
- let cin = open_in f in
- let rec skip_space () =
- let c = input_char cin in if c = ' ' then skip_space () else c
- in
- while input_char cin <> '=' do () done;
- try
- while true do
- let c = skip_space () in
- if c = ':' then raise Exit;
- Buffer.add_char buf c;
- let s = input_line cin in
- Buffer.add_string buf s;
- Buffer.add_char buf '\n';
- done;
- assert false
- with Exit ->
- close_in cin;
- remove_file f;
- Buffer.add_char buf ')';
- Buffer.contents buf
-
-exception GappaFailed
-exception GappaProofFailed
-
-let patch_gappa_proof fin fout =
- let cin = open_in fin in
- let cout = open_out fout in
- let fmt = formatter_of_out_channel cout in
- let last = ref "" in
- let defs = ref "" in
- try
- while true do
- let s = input_line cin in
- if s = "Qed." then
- fprintf fmt "Defined.@\n"
- else begin
- begin
- try Scanf.sscanf s "Lemma %s "
- (fun n -> defs := n ^ " " ^ !defs; last := n)
- with Scanf.Scan_failure _ ->
- try Scanf.sscanf s "Definition %s "
- (fun n -> defs := n ^ " " ^ !defs)
- with Scanf.Scan_failure _ ->
- ()
- end;
- fprintf fmt "%s@\n" s
- end
- done
- with End_of_file ->
- close_in cin;
- fprintf fmt "Definition proof := Eval cbv delta [%s] in %s.@." !defs !last;
- close_out cout
-
-let call_gappa hl p =
- let gappa_in = temp_file "gappa_input" in
- let c = open_out gappa_in in
- let fmt = formatter_of_out_channel c in
- fprintf fmt "@[{ ";
- List.iter (fun h -> fprintf fmt "%a ->@ " print_pred h) hl;
- fprintf fmt "%a }@]@." print_pred p;
- close_out c;
- let gappa_out = temp_file "gappa_output" in
- let cmd = sprintf "gappa -Bcoq < %s > %s 2> /dev/null" gappa_in gappa_out in
- let out = Sys.command cmd in
- if out <> 0 then raise GappaFailed;
- remove_file gappa_in;
- let gappa_out2 = temp_file "gappa2" in
- patch_gappa_proof gappa_out gappa_out2;
- remove_file gappa_out;
- let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out2 in
- let out = Sys.command cmd in
- if out <> 0 then raise GappaProofFailed;
- let gappa_out3 = temp_file "gappa3" in
- let c = open_out gappa_out3 in
- let gappa2 = Filename.chop_suffix (Filename.basename gappa_out2) ".v" in
- Printf.fprintf c
- "Require \"%s\". Set Printing Depth 999999. Print %s.proof."
- (Filename.chop_suffix gappa_out2 ".v") gappa2;
- close_out c;
- let lambda = temp_file "gappa_lambda" in
- let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out3 ^ " > " ^ lambda in
- let out = Sys.command cmd in
- if out <> 0 then raise GappaProofFailed;
- remove_file gappa_out2; remove_file gappa_out3;
- remove_file (gappa_out2 ^ "o"); remove_file (gappa_out3 ^ "o");
- read_gappa_proof lambda
-
-(* 2. coq -> gappa translation *)
-
-exception NotGappa
-
-let logic_dir = ["Coq";"Logic";"Decidable"]
-let coq_modules =
- init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
- @ [["Coq"; "ZArith"; "BinInt"];
- ["Coq"; "Reals"; "Rdefinitions"];
- ["Coq"; "Reals"; "Raxioms";];
- ["Coq"; "Reals"; "Rbasic_fun";];
- ["Coq"; "Reals"; "R_sqrt";];
- ["Coq"; "Reals"; "Rfunctions";];
- ["Gappa"; "Gappa_tactic";];
- ["Gappa"; "Gappa_fixed";];
- ["Gappa"; "Gappa_float";];
- ["Gappa"; "Gappa_round_def";];
- ["Gappa"; "Gappa_pred_bnd";];
- ["Gappa"; "Gappa_definitions";];
- ]
-
-let constant = gen_constant_in_modules "gappa" coq_modules
-
-let coq_refl_equal = lazy (constant "refl_equal")
-let coq_Rle = lazy (constant "Rle")
-let coq_R = lazy (constant "R")
-(*
-let coq_Rplus = lazy (constant "Rplus")
-let coq_Rminus = lazy (constant "Rminus")
-let coq_Rmult = lazy (constant "Rmult")
-let coq_Rdiv = lazy (constant "Rdiv")
-let coq_powerRZ = lazy (constant "powerRZ")
-let coq_R1 = lazy (constant "R1")
-let coq_Ropp = lazy (constant "Ropp")
-let coq_Rabs = lazy (constant "Rabs")
-let coq_sqrt = lazy (constant "sqrt")
-*)
-
-let coq_convert = lazy (constant "convert")
-let coq_reUnknown = lazy (constant "reUnknown")
-let coq_reFloat2 = lazy (constant "reFloat2")
-let coq_reFloat10 = lazy (constant "reFloat10")
-let coq_reInteger = lazy (constant "reInteger")
-let coq_reBinary = lazy (constant "reBinary")
-let coq_reUnary = lazy (constant "reUnary")
-let coq_reRound = lazy (constant "reRound")
-let coq_roundDN = lazy (constant "roundDN")
-let coq_roundUP = lazy (constant "roundUP")
-let coq_roundNE = lazy (constant "roundNE")
-let coq_roundZR = lazy (constant "roundZR")
-let coq_rounding_fixed = lazy (constant "rounding_fixed")
-let coq_rounding_float = lazy (constant "rounding_float")
-let coq_boAdd = lazy (constant "boAdd")
-let coq_boSub = lazy (constant "boSub")
-let coq_boMul = lazy (constant "boMul")
-let coq_boDiv = lazy (constant "boDiv")
-let coq_uoAbs = lazy (constant "uoAbs")
-let coq_uoNeg = lazy (constant "uoNeg")
-let coq_uoSqrt = lazy (constant "uoSqrt")
-let coq_subset = lazy (constant "subset")
-let coq_makepairF = lazy (constant "makepairF")
-
-let coq_true = lazy (constant "true")
-let coq_false = lazy (constant "false")
-
-let coq_Z0 = lazy (constant "Z0")
-let coq_Zpos = lazy (constant "Zpos")
-let coq_Zneg = lazy (constant "Zneg")
-let coq_xH = lazy (constant "xH")
-let coq_xI = lazy (constant "xI")
-let coq_xO = lazy (constant "xO")
-let coq_IZR = lazy (constant "IZR")
-
-(* translates a closed Coq term p:positive into a FOL term of type int *)
-let rec tr_positive p = match kind_of_term p with
- | Term.Construct _ when p = Lazy.force coq_xH ->
- 1
- | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
- 2 * (tr_positive a) + 1
- | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
- 2 * (tr_positive a)
- | Term.Cast (p, _, _) ->
- tr_positive p
- | _ ->
- raise NotGappa
-
-(* translates a closed Coq term t:Z into a term of type int *)
-let rec tr_arith_constant t = match kind_of_term t with
- | Term.Construct _ when t = Lazy.force coq_Z0 -> 0
- | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_positive a
- | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - (tr_positive a)
- | Term.Cast (t, _, _) -> tr_arith_constant t
- | _ -> raise NotGappa
-
-(* translates a closed Coq term p:positive into a FOL term of type bigint *)
-let rec tr_bigpositive p = match kind_of_term p with
- | Term.Construct _ when p = Lazy.force coq_xH ->
- Bigint.one
- | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
- Bigint.add_1 (Bigint.mult_2 (tr_bigpositive a))
- | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
- (Bigint.mult_2 (tr_bigpositive a))
- | Term.Cast (p, _, _) ->
- tr_bigpositive p
- | _ ->
- raise NotGappa
-
-(* translates a closed Coq term t:Z into a term of type bigint *)
-let rec tr_arith_bigconstant t = match kind_of_term t with
- | Term.Construct _ when t = Lazy.force coq_Z0 -> Bigint.zero
- | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_bigpositive a
- | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
- Bigint.neg (tr_bigpositive a)
- | Term.Cast (t, _, _) -> tr_arith_bigconstant t
- | _ -> raise NotGappa
-
-let decomp c =
- let c, args = decompose_app c in
- kind_of_term c, args
-
-let tr_bool c = match decompose_app c with
- | c, [] when c = Lazy.force coq_true -> true
- | c, [] when c = Lazy.force coq_false -> false
- | _ -> raise NotGappa
-
-let tr_float b m e =
- (b, tr_arith_bigconstant m, tr_arith_bigconstant e)
-
-let tr_binop c = match decompose_app c with
- | c, [] when c = Lazy.force coq_boAdd -> Bplus
- | c, [] when c = Lazy.force coq_boSub -> Bminus
- | c, [] when c = Lazy.force coq_boMul -> Bmult
- | c, [] when c = Lazy.force coq_boDiv -> Bdiv
- | _ -> assert false
-
-let tr_unop c = match decompose_app c with
- | c, [] when c = Lazy.force coq_uoNeg -> Uopp
- | c, [] when c = Lazy.force coq_uoSqrt -> Usqrt
- | c, [] when c = Lazy.force coq_uoAbs -> Uabs
- | _ -> raise NotGappa
-
-let tr_var c = match decomp c with
- | Var x, [] -> string_of_id x
- | _ -> assert false
-
-let tr_mode c = match decompose_app c with
- | c, [] when c = Lazy.force coq_roundDN -> "dn"
- | c, [] when c = Lazy.force coq_roundNE -> "ne"
- | c, [] when c = Lazy.force coq_roundUP -> "up"
- | c, [] when c = Lazy.force coq_roundZR -> "zr"
- | _ -> raise NotGappa
-
-let tr_rounding_mode c = match decompose_app c with
- | c, [a;b] when c = Lazy.force coq_rounding_fixed ->
- let a = tr_mode a in
- let b = tr_arith_constant b in
- sprintf "fixed<%d,%s>" b a
- | c, [a;p;e] when c = Lazy.force coq_rounding_float ->
- let a = tr_mode a in
- let p = tr_positive p in
- let e = tr_arith_constant e in
- sprintf "float<%d,%d,%s>" p (-e) a
- | _ ->
- raise NotGappa
-
-(* REexpr -> term *)
-let rec tr_term c0 =
- let c, args = decompose_app c0 in
- match kind_of_term c, args with
- | _, [a] when c = Lazy.force coq_reUnknown ->
- Tvar (tr_var a)
- | _, [a; b] when c = Lazy.force coq_reFloat2 ->
- Tconst (Constant.create (tr_float 2 a b))
- | _, [a; b] when c = Lazy.force coq_reFloat10 ->
- Tconst (Constant.create (tr_float 10 a b))
- | _, [a] when c = Lazy.force coq_reInteger ->
- Tconst (Constant.create (1, tr_arith_bigconstant a, Bigint.zero))
- | _, [op;a;b] when c = Lazy.force coq_reBinary ->
- Tbinop (tr_binop op, tr_term a, tr_term b)
- | _, [op;a] when c = Lazy.force coq_reUnary ->
- Tunop (tr_unop op, tr_term a)
- | _, [op;a] when c = Lazy.force coq_reRound ->
- Tround (tr_rounding_mode op, tr_term a)
- | _ ->
- msgnl (str "tr_term: " ++ Printer.pr_constr c0);
- assert false
-
-let tr_rle c =
- let c, args = decompose_app c in
- match kind_of_term c, args with
- | _, [a;b] when c = Lazy.force coq_Rle ->
- begin match decompose_app a, decompose_app b with
- | (ac, [at]), (bc, [bt])
- when ac = Lazy.force coq_convert && bc = Lazy.force coq_convert ->
- at, bt
- | _ ->
- raise NotGappa
- end
- | _ ->
- raise NotGappa
-
-let tr_pred c =
- let c, args = decompose_app c in
- match kind_of_term c, args with
- | _, [a;b] when c = build_coq_and () ->
- begin match tr_rle a, tr_rle b with
- | (c1, t1), (t2, c2) when t1 = t2 ->
- begin match tr_term c1, tr_term c2 with
- | Tconst c1, Tconst c2 ->
- Pin (tr_term t1, c1, c2)
- | _ ->
- raise NotGappa
- end
- | _ ->
- raise NotGappa
- end
- | _ ->
- raise NotGappa
-
-let is_R c = match decompose_app c with
- | c, [] when c = Lazy.force coq_R -> true
- | _ -> false
-
-let tr_hyps =
- List.fold_left
- (fun acc (_,h) -> try tr_pred h :: acc with NotGappa -> acc) []
-
-let constr_of_string gl s =
- let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
- Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
-
-let var_name = function
- | Name id ->
- let s = string_of_id id in
- let s = String.sub s 1 (String.length s - 1) in
- mkVar (id_of_string s)
- | Anonymous ->
- assert false
-
-let build_proof_term c0 =
- let bl,c = decompose_lam c0 in
- List.fold_right
- (fun (x,t) pf ->
- mkApp (pf, [| if is_R t then var_name x else mk_new_meta () |]))
- bl c0
-
-let gappa_internal gl =
- try
- let c = tr_pred (pf_concl gl) in
- let s = call_gappa (tr_hyps (pf_hyps_types gl)) c in
- let pf = constr_of_string gl s in
- let pf = build_proof_term pf in
- Tacticals.tclTHEN (Tacmach.refine_no_check pf) Tactics.assumption gl
- with
- | NotGappa -> error "not a gappa goal"
- | GappaFailed -> error "gappa failed"
- | GappaProofFailed -> error "incorrect gappa proof term"
-
-let gappa_prepare =
- let id = Ident (dummy_loc, id_of_string "gappa_prepare") in
- lazy (Tacinterp.interp (Tacexpr.TacArg (Tacexpr.Reference id)))
-
-let gappa gl =
- Coqlib.check_required_library ["Gappa"; "Gappa_tactic"];
- Tacticals.tclTHEN (Lazy.force gappa_prepare) gappa_internal gl
-
-(*
-Local Variables:
-compile-command: "make -C ../.. bin/coqc.opt bin/coqide.opt"
-End:
-*)
-
diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml
deleted file mode 100644
index e24049ad..00000000
--- a/contrib/dp/dp_why.ml
+++ /dev/null
@@ -1,151 +0,0 @@
-
-(* Pretty-print PFOL (see fol.mli) in Why syntax *)
-
-open Format
-open Fol
-
-type proof =
- | Immediate of Term.constr
- | Fun_def of string * (string * typ) list * typ * term
-
-let proofs = Hashtbl.create 97
-let proof_name =
- let r = ref 0 in fun () -> incr r; "dp_axiom__" ^ string_of_int !r
-
-let add_proof pr = let n = proof_name () in Hashtbl.add proofs n pr; n
-
-let find_proof = Hashtbl.find proofs
-
-let rec print_list sep print fmt = function
- | [] -> ()
- | [x] -> print fmt x
- | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
-
-let space fmt () = fprintf fmt "@ "
-let comma fmt () = fprintf fmt ",@ "
-
-let is_why_keyword =
- let h = Hashtbl.create 17 in
- List.iter
- (fun s -> Hashtbl.add h s ())
- ["absurd"; "and"; "array"; "as"; "assert"; "axiom"; "begin";
- "bool"; "do"; "done"; "else"; "end"; "exception"; "exists";
- "external"; "false"; "for"; "forall"; "fun"; "function"; "goal";
- "if"; "in"; "int"; "invariant"; "label"; "let"; "logic"; "not";
- "of"; "or"; "parameter"; "predicate"; "prop"; "raise"; "raises";
- "reads"; "real"; "rec"; "ref"; "returns"; "then"; "true"; "try";
- "type"; "unit"; "variant"; "void"; "while"; "with"; "writes" ];
- Hashtbl.mem h
-
-let ident fmt s =
- if is_why_keyword s then fprintf fmt "coq__%s" s else fprintf fmt "%s" s
-
-let rec print_typ fmt = function
- | Tvar x -> fprintf fmt "'%a" ident x
- | Tid ("int", []) -> fprintf fmt "int"
- | Tid (x, []) -> fprintf fmt "%a" ident x
- | Tid (x, [t]) -> fprintf fmt "%a %a" print_typ t ident x
- | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x
-
-let rec print_term fmt = function
- | Cst n ->
- fprintf fmt "%d" n
- | Plus (a, b) ->
- fprintf fmt "@[(%a +@ %a)@]" print_term a print_term b
- | Moins (a, b) ->
- fprintf fmt "@[(%a -@ %a)@]" print_term a print_term b
- | Mult (a, b) ->
- fprintf fmt "@[(%a *@ %a)@]" print_term a print_term b
- | Div (a, b) ->
- fprintf fmt "@[(%a /@ %a)@]" print_term a print_term b
- | App (id, []) ->
- fprintf fmt "%a" ident id
- | App (id, tl) ->
- fprintf fmt "@[%a(%a)@]" ident id print_terms tl
-
-and print_terms fmt tl =
- print_list comma print_term fmt tl
-
-let rec print_predicate fmt p =
- let pp = print_predicate in
- match p with
- | True ->
- fprintf fmt "true"
- | False ->
- fprintf fmt "false"
- | Fatom (Eq (a, b)) ->
- fprintf fmt "@[(%a =@ %a)@]" print_term a print_term b
- | Fatom (Le (a, b)) ->
- fprintf fmt "@[(%a <=@ %a)@]" print_term a print_term b
- | Fatom (Lt (a, b))->
- fprintf fmt "@[(%a <@ %a)@]" print_term a print_term b
- | Fatom (Ge (a, b)) ->
- fprintf fmt "@[(%a >=@ %a)@]" print_term a print_term b
- | Fatom (Gt (a, b)) ->
- fprintf fmt "@[(%a >@ %a)@]" print_term a print_term b
- | Fatom (Pred (id, [])) ->
- fprintf fmt "%a" ident id
- | Fatom (Pred (id, tl)) ->
- fprintf fmt "@[%a(%a)@]" ident id print_terms tl
- | Imp (a, b) ->
- fprintf fmt "@[(%a ->@ %a)@]" pp a pp b
- | Iff (a, b) ->
- fprintf fmt "@[(%a <->@ %a)@]" pp a pp b
- | And (a, b) ->
- fprintf fmt "@[(%a and@ %a)@]" pp a pp b
- | Or (a, b) ->
- fprintf fmt "@[(%a or@ %a)@]" pp a pp b
- | Not a ->
- fprintf fmt "@[(not@ %a)@]" pp a
- | Forall (id, t, p) ->
- fprintf fmt "@[(forall %a:%a.@ %a)@]" ident id print_typ t pp p
- | Exists (id, t, p) ->
- fprintf fmt "@[(exists %a:%a.@ %a)@]" ident id print_typ t pp p
-
-let print_query fmt (decls,concl) =
- let print_dtype = function
- | DeclType (id, 0) ->
- fprintf fmt "@[type %a@]@\n@\n" ident id
- | DeclType (id, 1) ->
- fprintf fmt "@[type 'a %a@]@\n@\n" ident id
- | DeclType (id, n) ->
- fprintf fmt "@[type (";
- for i = 1 to n do
- fprintf fmt "'a%d" i; if i < n then fprintf fmt ", "
- done;
- fprintf fmt ") %a@]@\n@\n" ident id
- | DeclFun _ | DeclPred _ | Axiom _ ->
- ()
- in
- let print_dvar_dpred = function
- | DeclFun (id, _, [], t) ->
- fprintf fmt "@[logic %a : -> %a@]@\n@\n" ident id print_typ t
- | DeclFun (id, _, l, t) ->
- fprintf fmt "@[logic %a : %a -> %a@]@\n@\n"
- ident id (print_list comma print_typ) l print_typ t
- | DeclPred (id, _, []) ->
- fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id
- | DeclPred (id, _, l) ->
- fprintf fmt "@[logic %a : %a -> prop@]@\n@\n"
- ident id (print_list comma print_typ) l
- | DeclType _ | Axiom _ ->
- ()
- in
- let print_assert = function
- | Axiom (id, f) ->
- fprintf fmt "@[<hov 2>axiom %a:@ %a@]@\n@\n" ident id print_predicate f
- | DeclType _ | DeclFun _ | DeclPred _ ->
- ()
- in
- List.iter print_dtype decls;
- List.iter print_dvar_dpred decls;
- List.iter print_assert decls;
- fprintf fmt "@[<hov 2>goal coq___goal: %a@]" print_predicate concl
-
-let output_file f q =
- let c = open_out f in
- let fmt = formatter_of_out_channel c in
- fprintf fmt "@[%a@]@." print_query q;
- close_out c
-
-
diff --git a/contrib/dp/dp_why.mli b/contrib/dp/dp_why.mli
deleted file mode 100644
index b38a3d37..00000000
--- a/contrib/dp/dp_why.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-
-open Fol
-
-(* generation of the Why file *)
-
-val output_file : string -> query -> unit
-
-(* table to translate the proofs back to Coq (used in dp_zenon) *)
-
-type proof =
- | Immediate of Term.constr
- | Fun_def of string * (string * typ) list * typ * term
-
-val add_proof : proof -> string
-val find_proof : string -> proof
-
-
diff --git a/contrib/dp/dp_zenon.mli b/contrib/dp/dp_zenon.mli
deleted file mode 100644
index 0a727d1f..00000000
--- a/contrib/dp/dp_zenon.mli
+++ /dev/null
@@ -1,7 +0,0 @@
-
-open Fol
-
-val set_debug : bool -> unit
-
-val proof_from_file : string -> Proof_type.tactic
-
diff --git a/contrib/dp/dp_zenon.mll b/contrib/dp/dp_zenon.mll
deleted file mode 100644
index e15e280d..00000000
--- a/contrib/dp/dp_zenon.mll
+++ /dev/null
@@ -1,181 +0,0 @@
-
-{
-
- open Lexing
- open Pp
- open Util
- open Names
- open Tacmach
- open Dp_why
- open Tactics
- open Tacticals
-
- let debug = ref false
- let set_debug b = debug := b
-
- let buf = Buffer.create 1024
-
- let string_of_global env ref =
- Libnames.string_of_qualid (Nametab.shortest_qualid_of_global env ref)
-
- let axioms = ref []
-
- (* we cannot interpret the terms as we read them (since some lemmas
- may need other lemmas to be already interpreted) *)
- type lemma = { l_id : string; l_type : string; l_proof : string }
- type zenon_proof = lemma list * string
-
-}
-
-let ident = ['a'-'z' 'A'-'Z' '_' '0'-'9' '\'']+
-let space = [' ' '\t' '\r']
-
-rule start = parse
-| "(* BEGIN-PROOF *)" "\n" { scan lexbuf }
-| _ { start lexbuf }
-| eof { anomaly "malformed Zenon proof term" }
-
-(* here we read the lemmas and the main proof term;
- meanwhile we maintain the set of axioms that were used *)
-
-and scan = parse
-| "Let" space (ident as id) space* ":"
- { let t = read_coq_term lexbuf in
- let p = read_lemma_proof lexbuf in
- let l,pr = scan lexbuf in
- { l_id = id; l_type = t; l_proof = p } :: l, pr }
-| "Definition theorem:"
- { let t = read_main_proof lexbuf in [], t }
-| _ | eof
- { anomaly "malformed Zenon proof term" }
-
-and read_coq_term = parse
-| "." "\n"
- { let s = Buffer.contents buf in Buffer.clear buf; s }
-| "coq__" (ident as id) (* a Why keyword renamed *)
- { Buffer.add_string buf id; read_coq_term lexbuf }
-| ("dp_axiom__" ['0'-'9']+) as id
- { axioms := id :: !axioms; Buffer.add_string buf id; read_coq_term lexbuf }
-| _ as c
- { Buffer.add_char buf c; read_coq_term lexbuf }
-| eof
- { anomaly "malformed Zenon proof term" }
-
-and read_lemma_proof = parse
-| "Proof" space
- { read_coq_term lexbuf }
-| _ | eof
- { anomaly "malformed Zenon proof term" }
-
-(* skip the main proof statement and then read its term *)
-and read_main_proof = parse
-| ":=" "\n"
- { read_coq_term lexbuf }
-| _
- { read_main_proof lexbuf }
-| eof
- { anomaly "malformed Zenon proof term" }
-
-
-{
-
- let read_zenon_proof f =
- Buffer.clear buf;
- let c = open_in f in
- let lb = from_channel c in
- let p = start lb in
- close_in c;
- if not !debug then begin try Sys.remove f with _ -> () end;
- p
-
- let constr_of_string gl s =
- let parse_constr = Pcoq.parse_string Pcoq.Constr.constr in
- Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s)
-
- (* we are lazy here: we build strings containing Coq terms using a *)
- (* pretty-printer Fol -> Coq *)
- module Coq = struct
- open Format
- open Fol
-
- let rec print_list sep print fmt = function
- | [] -> ()
- | [x] -> print fmt x
- | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
-
- let space fmt () = fprintf fmt "@ "
- let comma fmt () = fprintf fmt ",@ "
-
- let rec print_typ fmt = function
- | Tvar x -> fprintf fmt "%s" x
- | Tid ("int", []) -> fprintf fmt "Z"
- | Tid (x, []) -> fprintf fmt "%s" x
- | Tid (x, [t]) -> fprintf fmt "(%s %a)" x print_typ t
- | Tid (x,tl) ->
- fprintf fmt "(%s %a)" x (print_list comma print_typ) tl
-
- let rec print_term fmt = function
- | Cst n ->
- fprintf fmt "%d" n
- | Plus (a, b) ->
- fprintf fmt "@[(Zplus %a %a)@]" print_term a print_term b
- | Moins (a, b) ->
- fprintf fmt "@[(Zminus %a %a)@]" print_term a print_term b
- | Mult (a, b) ->
- fprintf fmt "@[(Zmult %a %a)@]" print_term a print_term b
- | Div (a, b) ->
- fprintf fmt "@[(Zdiv %a %a)@]" print_term a print_term b
- | App (id, []) ->
- fprintf fmt "%s" id
- | App (id, tl) ->
- fprintf fmt "@[(%s %a)@]" id print_terms tl
-
- and print_terms fmt tl =
- print_list space print_term fmt tl
-
- (* builds the text for "forall vars, f vars = t" *)
- let fun_def_axiom f vars t =
- let binder fmt (x,t) = fprintf fmt "(%s: %a)" x print_typ t in
- fprintf str_formatter
- "@[(forall %a, %s %a = %a)@]@."
- (print_list space binder) vars f
- (print_list space (fun fmt (x,_) -> pp_print_string fmt x)) vars
- print_term t;
- flush_str_formatter ()
-
- end
-
- let prove_axiom id = match Dp_why.find_proof id with
- | Immediate t ->
- exact_check t
- | Fun_def (f, vars, ty, t) ->
- tclTHENS
- (fun gl ->
- let s = Coq.fun_def_axiom f vars t in
- if !debug then Format.eprintf "axiom fun def = %s@." s;
- let c = constr_of_string gl s in
- assert_tac (Name (id_of_string id)) c gl)
- [tclTHEN intros reflexivity; tclIDTAC]
-
- let exact_string s gl =
- let c = constr_of_string gl s in
- exact_check c gl
-
- let interp_zenon_proof (ll,p) =
- let interp_lemma l gl =
- let ty = constr_of_string gl l.l_type in
- tclTHENS
- (assert_tac (Name (id_of_string l.l_id)) ty)
- [exact_string l.l_proof; tclIDTAC]
- gl
- in
- tclTHEN (tclMAP interp_lemma ll) (exact_string p)
-
- let proof_from_file f =
- axioms := [];
- msgnl (str "proof_from_file " ++ str f);
- let zp = read_zenon_proof f in
- msgnl (str "proof term is " ++ str (snd zp));
- tclTHEN (tclMAP prove_axiom !axioms) (interp_zenon_proof zp)
-
-}
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
deleted file mode 100644
index b94bd3e3..00000000
--- a/contrib/dp/fol.mli
+++ /dev/null
@@ -1,55 +0,0 @@
-
-(* Polymorphic First-Order Logic (that is Why's input logic) *)
-
-type typ =
- | Tvar of string
- | Tid of string * typ list
-
-type term =
- | Cst of int
- | Plus of term * term
- | Moins of term * term
- | Mult of term * term
- | Div of term * term
- | App of string * term list
-
-and atom =
- | Eq of term * term
- | Le of term * term
- | Lt of term * term
- | Ge of term * term
- | Gt of term * term
- | Pred of string * term list
-
-and form =
- | Fatom of atom
- | Imp of form * form
- | Iff of form * form
- | And of form * form
- | Or of form * form
- | Not of form
- | Forall of string * typ * form
- | Exists of string * typ * form
- | True
- | False
-
-(* the integer indicates the number of type variables *)
-type decl =
- | DeclType of string * int
- | DeclFun of string * int * typ list * typ
- | DeclPred of string * int * typ list
- | Axiom of string * form
-
-type query = decl list * form
-
-
-(* prover result *)
-
-type prover_answer =
- | Valid of string option
- | Invalid
- | DontKnow
- | Timeout
- | NoAnswer
- | Failure of string
-
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
deleted file mode 100644
index 99bcf477..00000000
--- a/contrib/dp/g_dp.ml4
+++ /dev/null
@@ -1,79 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(* $Id: g_dp.ml4 10924 2008-05-13 14:01:11Z filliatr $ *)
-
-open Dp
-
-TACTIC EXTEND Simplify
- [ "simplify" ] -> [ simplify ]
-END
-
-TACTIC EXTEND Ergo
- [ "ergo" ] -> [ ergo ]
-END
-
-TACTIC EXTEND Yices
- [ "yices" ] -> [ yices ]
-END
-
-TACTIC EXTEND CVCLite
- [ "cvcl" ] -> [ cvc_lite ]
-END
-
-TACTIC EXTEND Harvey
- [ "harvey" ] -> [ harvey ]
-END
-
-TACTIC EXTEND Zenon
- [ "zenon" ] -> [ zenon ]
-END
-
-TACTIC EXTEND Gwhy
- [ "gwhy" ] -> [ gwhy ]
-END
-
-TACTIC EXTEND Gappa_internal
- [ "gappa_internal" ] -> [ Dp_gappa.gappa_internal ]
-END
-
-TACTIC EXTEND Gappa
- [ "gappa" ] -> [ Dp_gappa.gappa ]
-END
-
-(* should be part of basic tactics syntax *)
-TACTIC EXTEND admit
- [ "admit" ] -> [ Tactics.admit_as_an_axiom ]
-END
-
-VERNAC COMMAND EXTEND Dp_hint
- [ "Dp_hint" ne_global_list(l) ] -> [ dp_hint l ]
-END
-
-VERNAC COMMAND EXTEND Dp_timeout
-| [ "Dp_timeout" natural(n) ] -> [ dp_timeout n ]
-END
-
-VERNAC COMMAND EXTEND Dp_prelude
-| [ "Dp_prelude" string_list(l) ] -> [ dp_prelude l ]
-END
-
-VERNAC COMMAND EXTEND Dp_predefined
-| [ "Dp_predefined" global(g) "=>" string(s) ] -> [ dp_predefined g s ]
-END
-
-VERNAC COMMAND EXTEND Dp_debug
-| [ "Dp_debug" ] -> [ dp_debug true; Dp_zenon.set_debug true ]
-END
-
-VERNAC COMMAND EXTEND Dp_trace
-| [ "Dp_trace" ] -> [ dp_trace true ]
-END
-
diff --git a/contrib/dp/test2.v b/contrib/dp/test2.v
deleted file mode 100644
index 3e4c0f6d..00000000
--- a/contrib/dp/test2.v
+++ /dev/null
@@ -1,80 +0,0 @@
-Require Import ZArith.
-Require Import Classical.
-Require Import List.
-
-Open Scope list_scope.
-Open Scope Z_scope.
-
-Dp_debug.
-Dp_timeout 3.
-Require Export zenon.
-
-Definition neg (z:Z) : Z := match z with
- | Z0 => Z0
- | Zpos p => Zneg p
- | Zneg p => Zpos p
- end.
-
-Goal forall z, neg (neg z) = z.
- Admitted.
-
-Open Scope nat_scope.
-Print plus.
-
-Goal forall x, x+0=x.
- induction x; ergo.
- (* simplify resoud le premier, pas le second *)
- Admitted.
-
-Goal 1::2::3::nil = 1::2::(1+2)::nil.
- zenon.
- Admitted.
-
-Definition T := nat.
-Parameter fct : T -> nat.
-Goal fct O = O.
- Admitted.
-
-Fixpoint even (n:nat) : Prop :=
- match n with
- O => True
- | S O => False
- | S (S p) => even p
- end.
-
-Goal even 4%nat.
- try zenon.
- Admitted.
-
-Definition p (A B:Set) (a:A) (b:B) : list (A*B) := cons (a,b) nil.
-
-Definition head :=
-fun (A : Set) (l : list A) =>
-match l with
-| nil => None (A:=A)
-| x :: _ => Some x
-end.
-
-Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
-
-Admitted.
-
-(*
-BUG avec head prédéfini : manque eta-expansion sur A:Set
-
-Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
-
-Print value.
-Print Some.
-
-zenon.
-*)
-
-Inductive IN (A:Set) : A -> list A -> Prop :=
- | IN1 : forall x l, IN A x (x::l)
- | IN2: forall x l, IN A x l -> forall y, IN A x (y::l).
-Implicit Arguments IN [A].
-
-Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l).
- zenon.
-Print In.
diff --git a/contrib/dp/test_gappa.v b/contrib/dp/test_gappa.v
deleted file mode 100644
index eb65a59d..00000000
--- a/contrib/dp/test_gappa.v
+++ /dev/null
@@ -1,91 +0,0 @@
-Require Export Gappa_tactic.
-Require Export Reals.
-
-Open Scope Z_scope.
-Open Scope R_scope.
-
-Lemma test_base10 :
- forall x y:R,
- 0 <= x <= 4 ->
- 0 <= x * (24 * powerRZ 10 (-1)) <= 10.
-Proof.
- gappa.
-Qed.
-
-(*
-@rnd = float< ieee_32, zr >;
-a = rnd(a_); b = rnd(b_);
-{ a in [3.2,3.3] /\ b in [1.4,1.9] ->
- rnd(a - b) - (a - b) in [0,0] }
-*)
-
-Definition rnd := gappa_rounding (rounding_float roundZR 43 (120)).
-
-Lemma test_float3 :
- forall a_ b_ a b : R,
- a = rnd a_ ->
- b = rnd b_ ->
- 52 / 16 <= a <= 53 / 16 ->
- 22 / 16 <= b <= 30 / 16 ->
- 0 <= rnd (a - b) - (a - b) <= 0.
-Proof.
- unfold rnd.
- gappa.
-Qed.
-
-Lemma test_float2 :
- forall x y:R,
- 0 <= x <= 1 ->
- 0 <= y <= 1 ->
- 0 <= gappa_rounding (rounding_float roundNE 53 (1074)) (x+y) <= 2.
-Proof.
- gappa.
-Qed.
-
-Lemma test_float1 :
- forall x y:R,
- 0 <= gappa_rounding (rounding_fixed roundDN (0)) x -
- gappa_rounding (rounding_fixed roundDN (0)) y <= 0 ->
- Rabs (x - y) <= 1.
-Proof.
- gappa.
-Qed.
-
-Lemma test1 :
- forall x y:R,
- 0 <= x <= 1 ->
- 0 <= -y <= 1 ->
- 0 <= x * (-y) <= 1.
-Proof.
- gappa.
-Qed.
-
-Lemma test2 :
- forall x y:R,
- 3/4 <= x <= 3 ->
- 0 <= sqrt x <= 1775 * (powerRZ 2 (-10)).
-Proof.
- gappa.
-Qed.
-
-Lemma test3 :
- forall x y z:R,
- 0 <= x - y <= 3 ->
- -2 <= y - z <= 4 ->
- -2 <= x - z <= 7.
-Proof.
- gappa.
-Qed.
-
-Lemma test4 :
- forall x1 x2 y1 y2 : R,
- 1 <= Rabs y1 <= 1000 ->
- 1 <= Rabs y2 <= 1000 ->
- - powerRZ 2 (-53) <= (x1 - y1) / y1 <= powerRZ 2 (-53) ->
- - powerRZ 2 (-53) <= (x2 - y2) / y2 <= powerRZ 2 (-53) ->
- - powerRZ 2 (-51) <= (x1 * x2 - y1 * y2) / (y1 * y2) <= powerRZ 2 (-51).
-Proof.
- gappa.
-Qed.
-
-
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
deleted file mode 100644
index a6d4f2e1..00000000
--- a/contrib/dp/tests.v
+++ /dev/null
@@ -1,288 +0,0 @@
-
-Require Import ZArith.
-Require Import Classical.
-
-Dp_debug.
-Dp_timeout 3.
-
-(* module renamings *)
-
-Module M.
- Parameter t : Set.
-End M.
-
-Lemma test_module_0 : forall x:M.t, x=x.
-ergo.
-Qed.
-
-Module N := M.
-
-Lemma test_module_renaming_0 : forall x:N.t, x=x.
-ergo.
-Qed.
-
-Dp_predefined M.t => "int".
-
-Lemma test_module_renaming_1 : forall x:N.t, x=x.
-ergo.
-Qed.
-
-(* Coq lists *)
-
-Require Export List.
-
-Lemma test_pol_0 : forall l:list nat, l=l.
-ergo.
-Qed.
-
-Parameter nlist: list nat -> Prop.
-
-Lemma poly_1 : forall l, nlist l -> True.
-intros.
-simplify.
-Qed.
-
-(* user lists *)
-
-Inductive list (A:Set) : Set :=
-| nil : list A
-| cons: forall a:A, list A -> list A.
-
-Fixpoint app (A:Set) (l m:list A) {struct l} : list A :=
-match l with
-| nil => m
-| cons a l1 => cons A a (app A l1 m)
-end.
-
-Lemma entail: (nil Z) = app Z (nil Z) (nil Z) -> True.
-intros; ergo.
-Qed.
-
-(* polymorphism *)
-Require Import List.
-
-Inductive mylist (A:Set) : Set :=
- mynil : mylist A
-| mycons : forall a:A, mylist A -> mylist A.
-
-Parameter my_nlist: mylist nat -> Prop.
-
- Goal forall l, my_nlist l -> True.
- intros.
- simplify.
-Qed.
-
-(* First example with the 0 and the equality translated *)
-
-Goal 0 = 0.
-simplify.
-Qed.
-
-(* Examples in the Propositional Calculus
- and theory of equality *)
-
-Parameter A C : Prop.
-
-Goal A -> A.
-simplify.
-Qed.
-
-
-Goal A -> (A \/ C).
-
-simplify.
-Qed.
-
-
-Parameter x y z : Z.
-
-Goal x = y -> y = z -> x = z.
-ergo.
-Qed.
-
-
-Goal ((((A -> C) -> A) -> A) -> C) -> C.
-
-ergo.
-Qed.
-
-(* Arithmetic *)
-Open Scope Z_scope.
-
-Goal 1 + 1 = 2.
-yices.
-Qed.
-
-
-Goal 2*x + 10 = 18 -> x = 4.
-
-simplify.
-Qed.
-
-
-(* Universal quantifier *)
-
-Goal (forall (x y : Z), x = y) -> 0=1.
-try zenon.
-ergo.
-Qed.
-
-Goal forall (x: nat), (x + 0 = x)%nat.
-
-induction x0; ergo.
-Qed.
-
-
-(* No decision procedure can solve this problem
- Goal forall (x a b : Z), a * x + b = 0 -> x = - b/a.
-*)
-
-
-(* Functions definitions *)
-
-Definition fst (x y : Z) : Z := x.
-
-Goal forall (g : Z -> Z) (x y : Z), g (fst x y) = g x.
-
-simplify.
-Qed.
-
-
-(* Eta-expansion example *)
-
-Definition snd_of_3 (x y z : Z) : Z := y.
-
-Definition f : Z -> Z -> Z := snd_of_3 0.
-
-Goal forall (x y z z1 : Z), snd_of_3 x y z = f y z1.
-
-simplify.
-Qed.
-
-
-(* Inductive types definitions - call to incontrib/dp/jection function *)
-
-Inductive even : Z -> Prop :=
-| even_0 : even 0
-| even_plus2 : forall z : Z, even z -> even (z + 2).
-
-
-(* Simplify and Zenon can't prove this goal before the timeout
- unlike CVC Lite *)
-
-Goal even 4.
-ergo.
-Qed.
-
-
-Definition skip_z (z : Z) (n : nat) := n.
-
-Definition skip_z1 := skip_z.
-
-Goal forall (z : Z) (n : nat), skip_z z n = skip_z1 z n.
-yices.
-Qed.
-
-
-(* Axioms definitions and dp_hint *)
-
-Parameter add : nat -> nat -> nat.
-Axiom add_0 : forall (n : nat), add 0%nat n = n.
-Axiom add_S : forall (n1 n2 : nat), add (S n1) n2 = S (add n1 n2).
-
-Dp_hint add_0.
-Dp_hint add_S.
-
-(* Simplify can't prove this goal before the timeout
- unlike zenon *)
-
-Goal forall n : nat, add n 0 = n.
-induction n ; yices.
-Qed.
-
-
-Definition pred (n : nat) : nat := match n with
- | 0%nat => 0%nat
- | S n' => n'
-end.
-
-Goal forall n : nat, n <> 0%nat -> pred (S n) <> 0%nat.
-yices.
-(*zenon.*)
-Qed.
-
-
-Fixpoint plus (n m : nat) {struct n} : nat :=
- match n with
- | 0%nat => m
- | S n' => S (plus n' m)
-end.
-
-Goal forall n : nat, plus n 0%nat = n.
-
-induction n; ergo.
-Qed.
-
-
-(* Mutually recursive functions *)
-
-Fixpoint even_b (n : nat) : bool := match n with
- | O => true
- | S m => odd_b m
-end
-with odd_b (n : nat) : bool := match n with
- | O => false
- | S m => even_b m
-end.
-
-Goal even_b (S (S O)) = true.
-ergo.
-(*
-simplify.
-zenon.
-*)
-Qed.
-
-
-(* sorts issues *)
-
-Parameter foo : Set.
-Parameter ff : nat -> foo -> foo -> nat.
-Parameter g : foo -> foo.
-Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O.
-yices.
-(*zenon.*)
-Qed.
-
-
-
-(* abstractions *)
-
-Parameter poly_f : forall A:Set, A->A.
-
-Goal forall x:nat, poly_f nat x = poly_f nat x.
-ergo.
-(*zenon.*)
-Qed.
-
-
-
-(* Anonymous mutually recursive functions : no equations are produced
-
-Definition mrf :=
- fix even2 (n : nat) : bool := match n with
- | O => true
- | S m => odd2 m
- end
- with odd2 (n : nat) : bool := match n with
- | O => false
- | S m => even2 m
- end for even.
-
- Thus this goal is unsolvable
-
-Goal mrf (S (S O)) = true.
-
-zenon.
-
-*)
diff --git a/contrib/dp/zenon.v b/contrib/dp/zenon.v
deleted file mode 100644
index 4ad00a11..00000000
--- a/contrib/dp/zenon.v
+++ /dev/null
@@ -1,94 +0,0 @@
-(* Copyright 2004 INRIA *)
-(* $Id: zenon.v 10739 2008-04-01 14:45:20Z herbelin $ *)
-
-Require Export Classical.
-
-Lemma zenon_nottrue :
- (~True -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_noteq : forall (T : Type) (t : T),
- ((t <> t) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_and : forall P Q : Prop,
- (P -> Q -> False) -> (P /\ Q -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_or : forall P Q : Prop,
- (P -> False) -> (Q -> False) -> (P \/ Q -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_imply : forall P Q : Prop,
- (~P -> False) -> (Q -> False) -> ((P -> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_equiv : forall P Q : Prop,
- (~P -> ~Q -> False) -> (P -> Q -> False) -> ((P <-> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notand : forall P Q : Prop,
- (~P -> False) -> (~Q -> False) -> (~(P /\ Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notor : forall P Q : Prop,
- (~P -> ~Q -> False) -> (~(P \/ Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notimply : forall P Q : Prop,
- (P -> ~Q -> False) -> (~(P -> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_notequiv : forall P Q : Prop,
- (~P -> Q -> False) -> (P -> ~Q -> False) -> (~(P <-> Q) -> False).
-Proof. tauto. Qed.
-
-Lemma zenon_ex : forall (T : Type) (P : T -> Prop),
- (forall z : T, ((P z) -> False)) -> ((exists x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_all : forall (T : Type) (P : T -> Prop) (t : T),
- ((P t) -> False) -> ((forall x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_notex : forall (T : Type) (P : T -> Prop) (t : T),
- (~(P t) -> False) -> (~(exists x : T, (P x)) -> False).
-Proof. firstorder. Qed.
-
-Lemma zenon_notall : forall (T : Type) (P : T -> Prop),
- (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
-Proof. intros T P Ha Hb. apply Hb. intro. apply NNPP. exact (Ha x). Qed.
-
-Lemma zenon_equal_base : forall (T : Type) (f : T), f = f.
-Proof. auto. Qed.
-
-Lemma zenon_equal_step :
- forall (S T : Type) (fa fb : S -> T) (a b : S),
- (fa = fb) -> (a <> b -> False) -> ((fa a) = (fb b)).
-Proof. intros. rewrite (NNPP (a = b)). congruence. auto. Qed.
-
-Lemma zenon_pnotp : forall P Q : Prop,
- (P = Q) -> (P -> ~Q -> False).
-Proof. intros P Q Ha. rewrite Ha. auto. Qed.
-
-Lemma zenon_notequal : forall (T : Type) (a b : T),
- (a = b) -> (a <> b -> False).
-Proof. auto. Qed.
-
-Ltac zenon_intro id :=
- intro id || let nid := fresh in (intro nid; clear nid)
-.
-
-Definition zenon_and_s := fun P Q a b => zenon_and P Q b a.
-Definition zenon_or_s := fun P Q a b c => zenon_or P Q b c a.
-Definition zenon_imply_s := fun P Q a b c => zenon_imply P Q b c a.
-Definition zenon_equiv_s := fun P Q a b c => zenon_equiv P Q b c a.
-Definition zenon_notand_s := fun P Q a b c => zenon_notand P Q b c a.
-Definition zenon_notor_s := fun P Q a b => zenon_notor P Q b a.
-Definition zenon_notimply_s := fun P Q a b => zenon_notimply P Q b a.
-Definition zenon_notequiv_s := fun P Q a b c => zenon_notequiv P Q b c a.
-Definition zenon_ex_s := fun T P a b => zenon_ex T P b a.
-Definition zenon_notall_s := fun T P a b => zenon_notall T P b a.
-
-Definition zenon_pnotp_s := fun P Q a b c => zenon_pnotp P Q c a b.
-Definition zenon_notequal_s := fun T a b x y => zenon_notequal T a b y x.