From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- plugins/decl_mode/g_decl_mode.ml4 | 5 +- plugins/dp/Dp.v | 118 --- plugins/dp/TODO | 24 - plugins/dp/dp.ml | 1133 ------------------------ plugins/dp/dp.mli | 20 - plugins/dp/dp_plugin.mllib | 5 - plugins/dp/dp_why.ml | 185 ---- plugins/dp/dp_why.mli | 17 - plugins/dp/dp_zenon.mli | 7 - plugins/dp/dp_zenon.mll | 189 ---- plugins/dp/fol.mli | 58 -- plugins/dp/g_dp.ml4 | 77 -- plugins/dp/test2.v | 80 -- plugins/dp/tests.v | 300 ------- plugins/dp/vo.itarget | 1 - plugins/dp/zenon.v | 92 -- plugins/extraction/extract_env.ml | 11 +- plugins/extraction/modutil.ml | 11 +- plugins/firstorder/g_ground.ml4 | 2 - plugins/funind/functional_principles_proofs.ml | 3 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/invfun.ml | 55 +- plugins/funind/recdef.ml | 42 +- plugins/micromega/coq_micromega.ml | 19 +- plugins/nsatz/nsatz.ml4 | 2 +- plugins/pluginsbyte.itarget | 1 - plugins/pluginsdyn.itarget | 1 - plugins/pluginsopt.itarget | 1 - plugins/pluginsvo.itarget | 3 +- plugins/rtauto/proof_search.ml | 4 +- plugins/rtauto/proof_search.mli | 2 +- plugins/subtac/eterm.ml | 17 +- plugins/subtac/g_subtac.ml4 | 4 +- plugins/subtac/subtac.ml | 4 +- plugins/subtac/subtac_cases.ml | 2 +- plugins/subtac/subtac_classes.ml | 9 +- plugins/subtac/subtac_coercion.ml | 107 ++- plugins/subtac/subtac_command.ml | 2 +- plugins/subtac/subtac_obligations.ml | 25 +- plugins/subtac/subtac_pretyping.ml | 4 +- plugins/subtac/subtac_pretyping_F.ml | 33 +- plugins/subtac/subtac_utils.ml | 11 +- plugins/subtac/subtac_utils.mli | 1 + plugins/xml/dumptree.ml4 | 4 +- 44 files changed, 216 insertions(+), 2477 deletions(-) delete mode 100644 plugins/dp/Dp.v delete mode 100644 plugins/dp/TODO delete mode 100644 plugins/dp/dp.ml delete mode 100644 plugins/dp/dp.mli delete mode 100644 plugins/dp/dp_plugin.mllib delete mode 100644 plugins/dp/dp_why.ml delete mode 100644 plugins/dp/dp_why.mli delete mode 100644 plugins/dp/dp_zenon.mli delete mode 100644 plugins/dp/dp_zenon.mll delete mode 100644 plugins/dp/fol.mli delete mode 100644 plugins/dp/g_dp.ml4 delete mode 100644 plugins/dp/test2.v delete mode 100644 plugins/dp/tests.v delete mode 100644 plugins/dp/vo.itarget delete mode 100644 plugins/dp/zenon.v (limited to 'plugins') diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 27def8cc..362f6a61 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -29,7 +29,7 @@ let pr_goal gs = (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), (str "thesis := " ++ fnl ()), Printer.pr_context_of env, - Printer.pr_ltype_env_at_top env (Goal.V82.concl sigma g) + Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g) in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ @@ -103,7 +103,7 @@ let proof_instr = Gram.entry_create "proofmode:instr" (* [Genarg.create_arg] creates a new embedding into Genarg. *) let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) = - Genarg.create_arg "proof_instr" + Genarg.create_arg None "proof_instr" let _ = Tacinterp.add_interp_genarg "proof_instr" begin begin fun e x -> (* declares the globalisation function *) @@ -111,6 +111,7 @@ let _ = Tacinterp.add_interp_genarg "proof_instr" (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x)) end, begin fun ist gl x -> (* declares the interpretation function *) + Tacmach.project gl , Genarg.in_gen wit_proof_instr (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x)) end, diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v deleted file mode 100644 index 1b66c334..00000000 --- a/plugins/dp/Dp.v +++ /dev/null @@ -1,118 +0,0 @@ -(* Calls to external decision procedures *) - -Require Export ZArith. -Require Export Classical. - -(* Zenon *) - -(* Copyright 2004 INRIA *) -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/plugins/dp/TODO b/plugins/dp/TODO deleted file mode 100644 index 44349e21..00000000 --- a/plugins/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/plugins/dp/dp.ml b/plugins/dp/dp.ml deleted file mode 100644 index 837195e4..00000000 --- a/plugins/dp/dp.ml +++ /dev/null @@ -1,1133 +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 Namegen -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 : int -> obj = - declare_object - {(default_object "Dp_timeout") with - cache_function = (fun (_,x) -> set_timeout x); - load_function = (fun _ (_,x) -> set_timeout x)} - -let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x) - -let dp_debug_obj : bool -> obj = - declare_object - {(default_object "Dp_debug") with - cache_function = (fun (_,x) -> set_debug x); - load_function = (fun _ (_,x) -> set_debug x)} - -let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x) - -let dp_trace_obj : bool -> obj = - declare_object - {(default_object "Dp_trace") with - cache_function = (fun (_,x) -> set_trace x); - load_function = (fun _ (_,x) -> set_trace 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"; "Reals"; "Rdefinitions"]; - ["Coq"; "Reals"; "Raxioms";]; - ["Coq"; "Reals"; "Rbasic_fun";]; - ["Coq"; "Reals"; "R_sqrt";]; - ["Coq"; "Reals"; "Rfunctions";]] - @ [["Coq"; "omega"; "OmegaLemmas"]] - -let constant = gen_constant_in_modules "dp" coq_modules - -(* integers constants and operations *) -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") - -(* real constants and operations *) -let coq_R = lazy (constant "R") -let coq_R0 = lazy (constant "R0") -let coq_R1 = lazy (constant "R1") -let coq_Rgt = lazy (constant "Rgt") -let coq_Rle = lazy (constant "Rle") -let coq_Rge = lazy (constant "Rge") -let coq_Rlt = lazy (constant "Rlt") -let coq_Rplus = lazy (constant "Rplus") -let coq_Rmult = lazy (constant "Rmult") -let coq_Ropp = lazy (constant "Ropp") -let coq_Rminus = lazy (constant "Rminus") -let coq_Rdiv = lazy (constant "Rdiv") -let coq_powerRZ = lazy (constant "powerRZ") - -(* 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_subscript 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.basename_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 (Termops.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 (Termops.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 (Termops.dependent (mkRel 1) b) -> - let avoid = Termops.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 () -> ()) } - -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 big_two = Big_int.succ_big_int Big_int.unit_big_int - -let rec tr_positive p = match kind_of_term p with - | Term.Construct _ when p = Lazy.force coq_xH -> - Big_int.unit_big_int - | Term.App (f, [|a|]) when f = Lazy.force coq_xI -> -(* - Plus (Mult (Cst 2, tr_positive a), Cst 1) -*) - Big_int.succ_big_int (Big_int.mult_big_int big_two (tr_positive a)) - | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> -(* - Mult (Cst 2, tr_positive a) -*) - Big_int.mult_big_int big_two (tr_positive a) - | Term.Cast (p, _, _) -> - tr_positive p - | _ -> - raise NotArithConstant - -(* translates a closed Coq term t:Z or R into a FOL term of type int or real *) -let rec tr_arith_constant t = match kind_of_term t with - | Term.Construct _ when t = Lazy.force coq_Z0 -> - Cst Big_int.zero_big_int - | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> - Cst (tr_positive a) - | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - Cst (Big_int.minus_big_int (tr_positive a)) - | Term.Const _ when t = Lazy.force coq_R0 -> - RCst Big_int.zero_big_int - | Term.Const _ when t = Lazy.force coq_R1 -> - RCst Big_int.unit_big_int - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> - let ta = tr_arith_constant a in - let tb = tr_arith_constant b in - begin match ta,tb with - | RCst na, RCst nb -> RCst (Big_int.add_big_int na nb) - | _ -> raise NotArithConstant - end - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rmult -> - let ta = tr_arith_constant a in - let tb = tr_arith_constant b in - begin match ta,tb with - | RCst na, RCst nb -> RCst (Big_int.mult_big_int na nb) - | _ -> raise NotArithConstant - end - | Term.App (f, [|a;b|]) when f = Lazy.force coq_powerRZ -> - tr_powerRZ a b - | Term.Cast (t, _, _) -> - tr_arith_constant t - | _ -> - raise NotArithConstant - -(* translates a constant of the form (powerRZ 2 int_constant) *) -and tr_powerRZ a b = - (* checking first that a is (R1 + R1) *) - match kind_of_term a with - | Term.App (f, [|c;d|]) when f = Lazy.force coq_Rplus -> - begin - match kind_of_term c,kind_of_term d with - | Term.Const _, Term.Const _ - when c = Lazy.force coq_R1 && d = Lazy.force coq_R1 -> - begin - match tr_arith_constant b with - | Cst n -> Power2 n - | _ -> raise NotArithConstant - end - | _ -> raise NotArithConstant - end - | _ -> 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 if t = Lazy.force coq_R then - Tid ("real", []) - 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 -> - raise NotFO - (* [CM 07/09/2009] deactivated because it generates - unbound identifiers 'abstraction_' - 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 body_of_constant (Global.lookup_constant c) 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 = - try - tr_arith_constant t - with NotArithConstant -> - match kind_of_term t with - (* binary operations on integers *) - | 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.App (f, [|a|]) when f = Lazy.force coq_Zopp -> - Opp (tr_term tv bv env a) - (* binary operations on reals *) - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> - Plus (tr_term tv bv env a, tr_term tv bv env b) - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rminus -> - Moins (tr_term tv bv env a, tr_term tv bv env b) - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rmult -> - Mult (tr_term tv bv env a, tr_term tv bv env b) - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Rdiv -> - 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, []) - | _ -> - 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 - (* comparisons on integers *) - | _, [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)) - (* comparisons on reals *) - | _, [a;b] when c = Lazy.force coq_Rle -> - Fatom (Le (tr_term tv bv env a, tr_term tv bv env b)) - | _, [a;b] when c = Lazy.force coq_Rlt -> - Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b)) - | _, [a;b] when c = Lazy.force coq_Rge -> - Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b)) - | _, [a;b] when c = Lazy.force coq_Rgt -> - 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_Prop (Typing.type_of env Evd.empty a) 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 | CVC3 | Z3 - -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 call_prover ?(opt="") file = - if !debug then Format.eprintf "calling prover on %s@." file; - let out = Filename.temp_file "out" "" in - let cmd = - sprintf "why-dp -timeout %d -batch %s > %s 2>&1" !timeout file out in - match Sys.command cmd with - 0 -> Valid None - | 1 -> Failure (sprintf "could not run why-dp\n%s" (file_contents out)) - | 2 -> Invalid - | 3 -> DontKnow - | 4 -> Timeout - | 5 -> Failure (sprintf "prover failed:\n%s" (file_contents out)) - | n -> Failure (sprintf "Unknown exit status of why-dp: %d" n) - -let prelude_files = ref ([] : string list) - -let set_prelude l = prelude_files := l - -let dp_prelude_obj : string list -> obj = - declare_object - {(default_object "Dp_prelude") with - cache_function = (fun (_,x) -> set_prelude x); - load_function = (fun _ (_,x) -> set_prelude 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 -*) - let r = call_prover fsx 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*) - (*NB: why-dp can't handle -cctrace - let cmd = - if !trace then - sprintf "alt-ergo -cctrace %s %s" ftrace fwhy - - else - sprintf "alt-ergo %s" fwhy - in*) - let r = call_prover fwhy in - if not !debug then remove_files [fwhy; (*out*)]; - r - - -let call_zenon fwhy = - let cmd = - sprintf "why --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 -(* why-dp won't let us having coqterm... - 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 r = call_prover fznn in - if not !debug then remove_files [fwhy; fznn]; - r - -let call_smt ~smt 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 opt = "-smt-solver " ^ smt in - let r = call_prover ~opt fsmt in - if not !debug then remove_files [fwhy; fsmt]; - r - -(* -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_cvc3 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 cvc3 -lang 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 -*) - let r = call_prover fcvc 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]; -*) - let r = call_prover frv in - if not !debug then remove_files [fwhy; frv]; - 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 - | CVC3 -> call_smt ~smt:"cvc3" fwhy - | Yices -> call_smt ~smt:"yices" fwhy - | Z3 -> call_smt ~smt:"z3" 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 cvc3 = tclTHEN intros (dp CVC3) -let yices = tclTHEN intros (dp Yices) -let z3 = tclTHEN intros (dp Z3) -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 : reference list -> obj = - declare_object - {(default_object "Dp_hint") with - cache_function = (fun (_,l) -> dp_hint l); - load_function = (fun _ (_,l) -> dp_hint l)} - -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 : reference * string -> 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)} - -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 := []) } diff --git a/plugins/dp/dp.mli b/plugins/dp/dp.mli deleted file mode 100644 index f40f8688..00000000 --- a/plugins/dp/dp.mli +++ /dev/null @@ -1,20 +0,0 @@ - -open Libnames -open Proof_type - -val simplify : tactic -val ergo : tactic -val cvc3 : tactic -val yices : tactic -val cvc_lite : tactic -val harvey : tactic -val zenon : tactic -val gwhy : tactic -val z3: 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/plugins/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib deleted file mode 100644 index 63252d6a..00000000 --- a/plugins/dp/dp_plugin.mllib +++ /dev/null @@ -1,5 +0,0 @@ -Dp_why -Dp_zenon -Dp -G_dp -Dp_plugin_mod diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml deleted file mode 100644 index 199c3087..00000000 --- a/plugins/dp/dp_why.ml +++ /dev/null @@ -1,185 +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 ("real", []) -> fprintf fmt "real" - | 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 print_arg fmt (id,typ) = fprintf fmt "%a: %a" ident id print_typ typ - -let rec print_term fmt = function - | Cst n -> - fprintf fmt "%s" (Big_int.string_of_big_int n) - | RCst s -> - fprintf fmt "%s.0" (Big_int.string_of_big_int s) - | Power2 n -> - fprintf fmt "0x1p%s" (Big_int.string_of_big_int 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 - | Opp (a) -> - fprintf fmt "@[(-@ %a)@]" print_term a - | 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 rec remove_iff args = function - Forall (id,t,p) -> remove_iff ((id,t)::args) p - | Iff(_,b) -> List.rev args, b - | _ -> raise Not_found - -let print_query fmt (decls,concl) = - let find_declared_preds l = - function - DeclPred (id,_,args) -> (id,args) :: l - | _ -> l - in - let find_defined_preds declared l = function - Axiom(id,f) -> - (try - let _decl = List.assoc id declared in - (id,remove_iff [] f)::l - with Not_found -> l) - | _ -> l - in - let declared_preds = - List.fold_left find_declared_preds [] decls in - let defined_preds = - List.fold_left (find_defined_preds declared_preds) [] decls - in - 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, _, []) when not (List.mem_assoc id defined_preds) -> - fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id - | DeclPred (id, _, l) when not (List.mem_assoc id defined_preds) -> - fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" - ident id (print_list comma print_typ) l - | DeclType _ | Axiom _ | DeclPred _ -> - () - in - let print_assert = function - | Axiom(id,_) when List.mem_assoc id defined_preds -> - let args, def = List.assoc id defined_preds in - fprintf fmt "@[predicate %a(%a) =@\n%a@]@\n" ident id - (print_list comma print_arg) args print_predicate def - | Axiom (id, f) -> - fprintf fmt "@[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 "@[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/plugins/dp/dp_why.mli b/plugins/dp/dp_why.mli deleted file mode 100644 index 0efa24a2..00000000 --- a/plugins/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/plugins/dp/dp_zenon.mli b/plugins/dp/dp_zenon.mli deleted file mode 100644 index 0a727d1f..00000000 --- a/plugins/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/plugins/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll deleted file mode 100644 index 949e91e3..00000000 --- a/plugins/dp/dp_zenon.mll +++ /dev/null @@ -1,189 +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 "%s" (Big_int.string_of_big_int n) - | RCst s -> - fprintf fmt "%s" (Big_int.string_of_big_int s) - | Power2 n -> - fprintf fmt "@[(powerRZ 2 %s)@]" (Big_int.string_of_big_int n) - - (* TODO: bug, it might be operations on reals *) - | 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 - | Opp (a) -> - fprintf fmt "@[(Zopp %a)@]" print_term a - | 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/plugins/dp/fol.mli b/plugins/dp/fol.mli deleted file mode 100644 index 4fb763a6..00000000 --- a/plugins/dp/fol.mli +++ /dev/null @@ -1,58 +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 Big_int.big_int - | RCst of Big_int.big_int - | Power2 of Big_int.big_int - | Plus of term * term - | Moins of term * term - | Mult of term * term - | Div of term * term - | Opp of 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/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4 deleted file mode 100644 index 001ccce8..00000000 --- a/plugins/dp/g_dp.ml4 +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [ simplify ] -END - -TACTIC EXTEND Ergo - [ "ergo" ] -> [ ergo ] -END - -TACTIC EXTEND Yices - [ "yices" ] -> [ yices ] -END - -TACTIC EXTEND CVC3 - [ "cvc3" ] -> [ cvc3 ] -END - -TACTIC EXTEND Z3 - [ "z3" ] -> [ z3 ] -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 - -(* 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/plugins/dp/test2.v b/plugins/dp/test2.v deleted file mode 100644 index ce660052..00000000 --- a/plugins/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). -Arguments IN [A] _ _. - -Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l). - zenon. -Print In. diff --git a/plugins/dp/tests.v b/plugins/dp/tests.v deleted file mode 100644 index dc85d2ee..00000000 --- a/plugins/dp/tests.v +++ /dev/null @@ -1,300 +0,0 @@ - -Require Import ZArith. -Require Import Classical. -Require Export Reals. - - -(* real numbers *) - -Lemma real_expr: (0 <= 9 * 4)%R. -ergo. -Qed. - -Lemma powerRZ_translation: (powerRZ 2 15 < powerRZ 2 17)%R. -ergo. -Qed. - -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 dp/injection 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/plugins/dp/vo.itarget b/plugins/dp/vo.itarget deleted file mode 100644 index 4d282709..00000000 --- a/plugins/dp/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Dp.vo diff --git a/plugins/dp/zenon.v b/plugins/dp/zenon.v deleted file mode 100644 index 89028c4f..00000000 --- a/plugins/dp/zenon.v +++ /dev/null @@ -1,92 +0,0 @@ -(* Copyright 2004 INRIA *) -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. diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 73062328..83ebb139 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -155,7 +155,9 @@ let factor_fix env l cb msb = function | (l,SFBconst cb') -> let check' = check_fix env cb' (j+1) in - if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible; + if not (fst check = fst check' && + prec_declaration_equal (snd check) (snd check')) + then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; labels, recd, msb'' @@ -196,13 +198,14 @@ let rec msid_of_seb = function | SEBwith (seb,_) -> msid_of_seb seb | _ -> assert false -let env_for_mtb_with env mp seb idl = +let env_for_mtb_with_def env mp seb idl = let sig_b = match seb with | SEBstruct(sig_b) -> sig_b | _ -> assert false in let l = label_of_id (List.hd idl) in - let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in + let spot = function (l',SFBconst _) -> l = l' | _ -> false in + let before = fst (list_split_when spot sig_b) in Modops.add_signature mp before empty_delta_resolver env (* From a [structure_body] (i.e. a list of [structure_field_body]) @@ -241,7 +244,7 @@ let rec extract_sfb_spec env mp = function and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with | SEBident mp -> Visit.add_mp_all mp; MTident mp | SEBwith(seb',With_definition_body(idl,cb))-> - let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in + let env' = env_for_mtb_with_def env (msid_of_seb seb') seb idl in let mt = extract_seb_spec env mp1 (seb,seb') in (match extract_with_type env' cb with (* cb peut contenir des kn *) | None -> mt diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 9e8dd828..4e0dbcab 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -194,6 +194,15 @@ let signature_of_structure s = (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *) +let is_modular = function + | SEdecl _ -> false + | SEmodule _ | SEmodtype _ -> true + +let rec search_structure l m = function + | [] -> raise Not_found + | (lab,d)::_ when lab=l && is_modular d = m -> d + | _::fields -> search_structure l m fields + let get_decl_in_structure r struc = try let base_mp,ll = labels_of_ref r in @@ -202,7 +211,7 @@ let get_decl_in_structure r struc = let rec go ll sel = match ll with | [] -> assert false | l :: ll -> - match List.assoc l sel with + match search_structure l (ll<>[]) sel with | SEdecl d -> d | SEmodtype m -> assert false | SEmodule m -> diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 4a38c48d..034dc3c2 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -134,8 +134,6 @@ TACTIC EXTEND firstorder | [ "firstorder" tactic_opt(t) firstorder_using(l) "with" ne_preident_list(l') ] -> [ gen_ground_tac true (Option.map eval_tactic t) l l' ] -| [ "firstorder" tactic_opt(t) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) [] [] ] END TACTIC EXTEND gintuition diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 1d1e4a2a..33d77568 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1371,7 +1371,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) (* rewrite *) (* ) *) - Eauto.gen_eauto false (false,5) [] (Some []) + Eauto.gen_eauto (false,5) [] (Some []) ] gls @@ -1449,7 +1449,6 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = ( tclCOMPLETE( Eauto.eauto_with_bases - false (true,5) [Evd.empty,Lazy.force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 123399d5..06abb8ce 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Verna let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype), (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype), (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) = - Genarg.create_arg "function_rec_definition_loc" + Genarg.create_arg None "function_rec_definition_loc" VERNAC COMMAND EXTEND Function ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] -> [ diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0b04a572..95ca86c2 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -588,15 +588,15 @@ let rec reflexivity_with_destruct_cases g = ) in (tclFIRST - [ reflexivity; - tclTHEN (tclPROGRESS discr_inject) (destruct_case ()); + [ observe_tac "reflexivity_with_destruct_cases : reflexivity" reflexivity; + observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ())); (* We reach this point ONLY if the same value is matched (at least) two times along binding path. In this case, either we have a discriminable hypothesis and we are done, either at least an injectable one and we do the injection before continuing *) - tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases + observe_tac "reflexivity_with_destruct_cases : others" (tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases) ]) g @@ -752,6 +752,7 @@ let do_save () = Lemmas.save_named false *) let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = + let previous_state = States.freeze () in let funs = Array.of_list funs and graphs = Array.of_list graphs in let funs_constr = Array.map mkConst funs in try @@ -793,22 +794,21 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.iteri (fun i f_as_constant -> let f_id = id_of_label (con_label f_as_constant) in - Lemmas.start_proof - (*i The next call to mk_correct_id is valid since we are constructing the lemma + (*i The next call to mk_correct_id is valid since we are constructing the lemma Ensures by: obvious - i*) - (mk_correct_id f_id) + i*) + let lem_id = mk_correct_id f_id in + Lemmas.start_proof lem_id (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); - Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i)); + Pfedit.by + (observe_tac ("prove correctness ("^(string_of_id f_id)^")") + (proving_tac i)); do_save (); let finfo = find_Function_infos f_as_constant in - update_Function - {finfo with - correctness_lemma = Some (destConst (Constrintern.global_reference (mk_correct_id f_id))) - } - + let lem_cst = destConst (Constrintern.global_reference lem_id) in + update_Function {finfo with correctness_lemma = Some lem_cst} ) funs; let lemmas_types_infos = @@ -845,34 +845,27 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.iteri (fun i f_as_constant -> let f_id = id_of_label (con_label f_as_constant) in - Lemmas.start_proof - (*i The next call to mk_complete_id is valid since we are constructing the lemma + (*i The next call to mk_complete_id is valid since we are constructing the lemma Ensures by: obvious - i*) - (mk_complete_id f_id) + i*) + let lem_id = mk_complete_id f_id in + Lemmas.start_proof lem_id (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); - Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i)); + Pfedit.by + (observe_tac ("prove completeness ("^(string_of_id f_id)^")") + (proving_tac i)); do_save (); let finfo = find_Function_infos f_as_constant in - update_Function - {finfo with - completeness_lemma = Some (destConst (Constrintern.global_reference (mk_complete_id f_id))) - } + let lem_cst = destConst (Constrintern.global_reference lem_id) in + update_Function {finfo with completeness_lemma = Some lem_cst} ) funs; with e -> (* In case of problem, we reset all the lemmas *) - (*i The next call to mk_correct_id is valid since we are erasing the lemmas - Ensures by: obvious - i*) - let first_lemma_id = - let f_id = id_of_label (con_label funs.(0)) in - - mk_correct_id f_id - in - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ()); + Pfedit.delete_all_proofs (); + States.unfreeze previous_state; raise e diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 55ebd31b..3355300e 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -48,7 +48,8 @@ open Genarg let compute_renamed_type gls c = - rename_bound_vars_as_displayed [] (pf_type_of gls c) + rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] + (pf_type_of gls c) let qed () = Lemmas.save_named true let defined () = Lemmas.save_named false @@ -232,18 +233,19 @@ let rec (find_call_occs : int -> int -> constr -> constr -> | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[]) | Var(_) when eq_constr expr f -> errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function") | Var(id) -> (fun l -> expr), [] - | Meta(_) -> error "find_call_occs : Meta" - | Evar(_) -> error "find_call_occs : Evar" + | Meta(_) -> error "Found a metavariable. Can not treat such a term" + | Evar(_) -> error "Found an evar. Can not treat such a term" | Sort(_) -> (fun l -> expr), [] | Cast(b,_,_) -> find_call_occs nb_arg nb_lam f b - | Prod(_,_,_) -> error "find_call_occs : Prod" + | Prod(na,t,b) -> + error "Found a product. Can not treat such a term" | Lambda(na,t,b) -> begin match find_call_occs nb_arg (succ nb_lam) f b with | _, [] -> (* Lambda are authorized as long as they do not contain recursives calls *) (fun l -> expr),[] - | _ -> error "find_call_occs : Lambda" + | _ -> error "Found a lambda which body contains a recursive call. Such terms are not allowed" end | LetIn(na,v,t,b) -> begin @@ -254,7 +256,7 @@ let rec (find_call_occs : int -> int -> constr -> constr -> ((fun l -> mkLetIn(na,v,t,cf l)),l) | (cf,(_::_ as l)),(_,[]) -> ((fun l -> mkLetIn(na,cf l,t,b)), l) - | _ -> error "find_call_occs : LetIn" + | _ -> error "Found a letin with recursive calls in both variable value and body. Such terms are not allowed." end | Const(_) -> (fun l -> expr), [] | Ind(_) -> (fun l -> expr), [] @@ -263,8 +265,8 @@ let rec (find_call_occs : int -> int -> constr -> constr -> (match find_call_occs nb_arg nb_lam f a with cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args) | _ -> (fun l -> expr),[]) - | Fix(_) -> error "find_call_occs : Fix" - | CoFix(_) -> error "find_call_occs : CoFix";; + | Fix(_) -> error "Found a local fixpoint. Can not treat such a term" + | CoFix(_) -> error "Found a local cofixpoint : CoFix";; let coq_constant s = Coqlib.gen_constant_in_modules "RecursiveDefinition" @@ -896,6 +898,20 @@ let build_and_l l = let conj_constr = coq_conj () in let mk_and p1 p2 = Term.mkApp(and_constr,[|p1;p2|]) in + let rec is_well_founded t = + match kind_of_term t with + | Prod(_,_,t') -> is_well_founded t' + | App(_,_) -> + let (f,_) = decompose_app t in + eq_constr f (well_founded ()) + | _ -> assert false + in + let compare t1 t2 = + let b1,b2= is_well_founded t1,is_well_founded t2 in + if (b1&&b2) || not (b1 || b2) then 0 + else if b1 && not b2 then 1 else -1 + in + let l = List.sort compare l in let rec f = function | [] -> failwith "empty list of subgoals!" | [p] -> p,tclIDTAC,1 @@ -1006,7 +1022,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) e_assumption; Eauto.eauto_with_bases - false (true,5) [Evd.empty,delayed_force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] @@ -1378,6 +1393,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = + let previous_label = Lib.current_command_label () in let function_type = interp_constr Evd.empty (Global.env()) type_of_f in let env = push_named (function_name,None,function_type) (Global.env()) in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) @@ -1429,7 +1445,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e) else anomaly "Cannot create equation Lemma" ; -(* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *) stop := true; end end; @@ -1461,10 +1476,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num hook with e -> begin - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); -(* anomaly "Cannot create termination Lemma" *) + (try ignore (Backtrack.backto previous_label) with _ -> ()); + (* anomaly "Cannot create termination Lemma" *) raise e end - - - diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 1ad49bb8..8b7ee55b 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -895,7 +895,9 @@ struct let parse_expr parse_constant parse_exp ops_spec env term = if debug then (Pp.pp (Pp.str "parse_expr: "); - Pp.pp_flush ();Pp.pp (Printer.prterm term); Pp.pp_flush ()); + Pp.pp (Printer.prterm term); + Pp.pp (Pp.str "\n"); + Pp.pp_flush ()); (* let constant_or_variable env term = @@ -991,8 +993,12 @@ struct else raise ParseError | App(op,args) -> begin - try - (assoc_const op rconst_assoc) (rconstant args.(0)) (rconstant args.(1)) + try + (* the evaluation order is important in the following *) + let f = assoc_const op rconst_assoc in + let a = rconstant args.(0) in + let b = rconstant args.(1) in + f a b with ParseError -> match op with @@ -1009,10 +1015,12 @@ struct if debug then (Pp.pp_flush (); Pp.pp (Pp.str "rconstant: "); - Pp.pp (Printer.prterm term); Pp.pp_flush ()); + Pp.pp (Printer.prterm term); + Pp.pp (Pp.str "\n"); + Pp.pp_flush ()); let res = rconstant term in if debug then - (Printf.printf "rconstant -> %a" pp_Rcst res ; flush stdout) ; + (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; res @@ -1052,6 +1060,7 @@ struct then (Pp.pp_flush (); Pp.pp (Pp.str "parse_arith: "); Pp.pp (Printer.prterm cstr); + Pp.pp (Pp.str "\n"); Pp.pp_flush ()); match kind_of_term cstr with | App(op,args) -> diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index e48643b4..a317307e 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -474,7 +474,7 @@ let remove_zeros zero lci = done; !lcr) lr in - info ("unuseful spolynomials: " + info ("useless spolynomials: " ^string_of_int (m-List.length lr)^"\n"); info ("useful spolynomials: " ^string_of_int (List.length lr)^"\n"); diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget index 04cbdccb..787995ed 100644 --- a/plugins/pluginsbyte.itarget +++ b/plugins/pluginsbyte.itarget @@ -8,7 +8,6 @@ fourier/fourier_plugin.cma romega/romega_plugin.cma omega/omega_plugin.cma micromega/micromega_plugin.cma -dp/dp_plugin.cma xml/xml_plugin.cma subtac/subtac_plugin.cma ring/ring_plugin.cma diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget index bbadfe69..bd3cec01 100644 --- a/plugins/pluginsdyn.itarget +++ b/plugins/pluginsdyn.itarget @@ -8,7 +8,6 @@ fourier/fourier_plugin.cmxs romega/romega_plugin.cmxs omega/omega_plugin.cmxs micromega/micromega_plugin.cmxs -dp/dp_plugin.cmxs xml/xml_plugin.cmxs subtac/subtac_plugin.cmxs ring/ring_plugin.cmxs diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget index 74b3f527..5264ba37 100644 --- a/plugins/pluginsopt.itarget +++ b/plugins/pluginsopt.itarget @@ -8,7 +8,6 @@ fourier/fourier_plugin.cmxa romega/romega_plugin.cmxa omega/omega_plugin.cmxa micromega/micromega_plugin.cmxa -dp/dp_plugin.cmxa xml/xml_plugin.cmxa subtac/subtac_plugin.cmxa ring/ring_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget index db56534c..bab15ad0 100644 --- a/plugins/pluginsvo.itarget +++ b/plugins/pluginsvo.itarget @@ -1,4 +1,3 @@ -dp/vo.otarget field/vo.otarget fourier/vo.otarget funind/vo.otarget @@ -10,4 +9,4 @@ ring/vo.otarget romega/vo.otarget rtauto/vo.otarget setoid_ring/vo.otarget -extraction/vo.otarget \ No newline at end of file +extraction/vo.otarget diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index d773b153..576f7d4e 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -509,8 +509,8 @@ let pp_gl gl= cut () ++ let pp = function - Incomplete(gl,ctx) -> msgnl (pp_gl gl) - | _ -> msg (str "") + Incomplete(gl,ctx) -> pp_gl gl ++ fnl () + | _ -> str "" let pp_info () = let count_info = diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index b236aa72..275e94cd 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -38,7 +38,7 @@ val branching: state -> state list val success: state -> bool -val pp: state -> unit +val pp: state -> Pp.std_ppcmds val pr_form : form -> unit diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml index 5ed335d0..f4d8b769 100644 --- a/plugins/subtac/eterm.ml +++ b/plugins/subtac/eterm.ml @@ -132,18 +132,29 @@ let rec chop_product n t = | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None | _ -> None -let evar_dependencies evm ev = +let evars_of_evar_info evi = + Intset.union (Evarutil.evars_of_term evi.evar_concl) + (Intset.union + (match evi.evar_body with + | Evar_empty -> Intset.empty + | Evar_defined b -> Evarutil.evars_of_term b) + (Evarutil.evars_of_named_context (evar_filtered_context evi))) + +let evar_dependencies evm oev = let one_step deps = Intset.fold (fun ev s -> let evi = Evd.find evm ev in - Intset.union (Evarutil.evars_of_evar_info evi) s) + let deps' = evars_of_evar_info evi in + if Intset.mem oev deps' then + raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev)) + else Intset.union deps' s) deps deps in let rec aux deps = let deps' = one_step deps in if Intset.equal deps deps' then deps else aux deps' - in aux (Intset.singleton ev) + in aux (Intset.singleton oev) let move_after (id, ev, deps as obl) l = let rec aux restdeps = function diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index ca1240e5..6a131d39 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -75,14 +75,14 @@ type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstra let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype), (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype), (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) = - Genarg.create_arg "subtac_gallina_loc" + Genarg.create_arg None "subtac_gallina_loc" type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type let (wit_subtac_withtac : Genarg.tlevel withtac_argtype), (globwit_subtac_withtac : Genarg.glevel withtac_argtype), (rawwit_subtac_withtac : Genarg.rlevel withtac_argtype) = - Genarg.create_arg "subtac_withtac" + Genarg.create_arg None "subtac_withtac" VERNAC COMMAND EXTEND Subtac [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ] diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 710149ae..d626396f 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -82,11 +82,9 @@ let start_proof_com env isevars sopt kind (bl,t) hook = Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps]; hook loc gr) -let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () - let start_proof_and_print env isevars idopt k t hook = start_proof_com env isevars idopt k t hook; - print_subgoals () + Vernacentries.print_subgoals () let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 368d8bac..16d4e21e 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -1845,7 +1845,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = refl_arg :: refl_args, pred slift, (Name id, b, t) :: argsign')) - (env, 0, [], [], slift, []) args argsign + (env, neqs, [], [], slift, []) args argsign in let eq = mk_JMeq (lift (nargeqs + slift) appt) diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index c08dd16d..6b3fe718 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -52,7 +52,7 @@ let type_ctx_instance evars env ctx inst subst = | None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l | Some b -> substl subst b, l in - evars := resolve_typeclasses ~onlyargs:true ~fail:true env !evars; + evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars; let d = na, Some c', t' in aux (c' :: subst, d :: instctx) l ctx | [] -> subst @@ -107,9 +107,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in Namegen.next_global_ident_away i (Termops.ids_of_context env) in + evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars; + let ctx = Evarutil.nf_rel_context_evar !evars ctx + and ctx' = Evarutil.nf_rel_context_evar !evars ctx' in let env' = push_rel_context ctx env in - evars := Evarutil.nf_evar_map !evars; - evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars; let sigma = !evars in let subst = List.map (Evarutil.nf_evar sigma) subst in let props = @@ -157,6 +158,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst) in evars := Evarutil.nf_evar_map !evars; + evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars; + evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:false env !evars; let term, termtype = match subst with | Inl subst -> diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 74f31a90..eb29bd04 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -27,6 +27,9 @@ open Subtac_errors open Eterm open Pp +let app_opt env evars f t = + whd_betaiota !evars (app_opt f t) + let pair_of_array a = (a.(0), a.(1)) let make_name s = Name (id_of_string s) @@ -80,7 +83,8 @@ module Coercion = struct | Type _, Prop Null -> Prop Null | _, Type _ -> s2 - let hnf env isevars c = whd_betadeltaiota env ( !isevars) c + let hnf env isevars c = whd_betadeltaiota env isevars c + let hnf_nodelta env evars c = whd_betaiota evars c let lift_args n sign = let rec liftrec k = function @@ -90,15 +94,16 @@ module Coercion = struct liftrec (List.length sign) sign let rec mu env isevars t = - let isevars = ref isevars in let rec aux v = - let v = hnf env isevars v in + let v = hnf env !isevars v in match disc_subset v with Some (u, p) -> let f, ct = aux u in + let p = hnf env !isevars p in (Some (fun x -> - app_opt f (mkApp ((delayed_force sig_).proj1, - [| u; p; x |]))), + app_opt env isevars + f (mkApp ((delayed_force sig_).proj1, + [| u; p; x |]))), ct) | None -> (None, v) in aux t @@ -106,9 +111,8 @@ module Coercion = struct and coerce loc env isevars (x : Term.constr) (y : Term.constr) : (Term.constr -> Term.constr) option = - let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in let rec coerce_unify env x y = - let x = hnf env isevars x and y = hnf env isevars y in + let x = hnf env !isevars x and y = hnf env !isevars y in try isevars := the_conv_x_leq env x y !isevars; None @@ -167,7 +171,7 @@ module Coercion = struct let env' = push_rel (name', None, a') env in let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) - let coec1 = app_opt c1 (mkRel 1) in + let coec1 = app_opt env' isevars c1 (mkRel 1) in (* env, x : a' |- c1[x] : lift 1 a *) let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in (* env, x : a' |- c2 : b[c1[x]/x]] > b' *) @@ -177,7 +181,7 @@ module Coercion = struct Some (fun f -> mkLambda (name', a', - app_opt c2 + app_opt env' isevars c2 (mkApp (Term.lift 1 f, [| coec1 |]))))) | App (c, l), App (c', l') -> @@ -220,9 +224,9 @@ module Coercion = struct Some (fun x -> let x, y = - app_opt c1 (mkApp (existS.proj1, + app_opt env' isevars c1 (mkApp (existS.proj1, [| a; pb; x |])), - app_opt c2 (mkApp (existS.proj2, + app_opt env' isevars c2 (mkApp (existS.proj2, [| a; pb; x |])) in mkApp (existS.intro, [| a'; pb'; x ; y |])) @@ -240,9 +244,9 @@ module Coercion = struct Some (fun x -> let x, y = - app_opt c1 (mkApp (prod.proj1, + app_opt env isevars c1 (mkApp (prod.proj1, [| a; b; x |])), - app_opt c2 (mkApp (prod.proj2, + app_opt env isevars c2 (mkApp (prod.proj2, [| a; b; x |])) in mkApp (prod.intro, [| a'; b'; x ; y |])) @@ -276,7 +280,7 @@ module Coercion = struct Some (u, p) -> let c = coerce_unify env u y in let f x = - app_opt c (mkApp ((delayed_force sig_).proj1, + app_opt env isevars c (mkApp ((delayed_force sig_).proj1, [| u; p; x |])) in Some f | None -> @@ -285,7 +289,7 @@ module Coercion = struct let c = coerce_unify env x u in Some (fun x -> - let cx = app_opt c x in + let cx = app_opt env isevars c x in let evar = make_existential loc env isevars (mkApp (p, [| cx |])) in (mkApp @@ -300,7 +304,8 @@ module Coercion = struct let coerce_itf loc env isevars v t c1 = let evars = ref isevars in let coercion = coerce loc env evars t c1 in - !evars, Option.map (app_opt coercion) v + let t = Option.map (app_opt env evars coercion) v in + !evars, t (* Taken from pretyping/coercion.ml *) @@ -354,34 +359,36 @@ module Coercion = struct with _ -> anomaly "apply_coercion" let inh_app_fun env isevars j = - let t = whd_betadeltaiota env ( isevars) j.uj_type in + let isevars = ref isevars in + let t = hnf env !isevars j.uj_type in match kind_of_term t with - | Prod (_,_,_) -> (isevars,j) - | Evar ev when not (is_defined_evar isevars ev) -> - let (isevars',t) = define_evar_as_product isevars ev in + | Prod (_,_,_) -> (!isevars,j) + | Evar ev when not (is_defined_evar !isevars ev) -> + let (isevars',t) = define_evar_as_product !isevars ev in (isevars',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try let t,p = - lookup_path_to_fun_from env ( isevars) j.uj_type in - (isevars,apply_coercion env ( isevars) p j t) + lookup_path_to_fun_from env !isevars j.uj_type in + (!isevars,apply_coercion env !isevars p j t) with Not_found -> try let coercef, t = mu env isevars t in - (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t }) + let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in + (!isevars, res) with NoSubtacCoercion | NoCoercion -> - (isevars,j)) + (!isevars,j)) let inh_tosort_force loc env isevars j = try let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in let j1 = apply_coercion env ( isevars) p j t in - (isevars,type_judgment env (j_nf_evar ( isevars) j1)) + (isevars, type_judgment env (j_nf_evar ( isevars) j1)) with Not_found -> error_not_a_type_loc loc env ( isevars) j let inh_coerce_to_sort loc env isevars j = - let typ = whd_betadeltaiota env ( isevars) j.uj_type in + let typ = hnf env isevars j.uj_type in match kind_of_term typ with | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined_evar isevars ev) -> @@ -391,15 +398,19 @@ module Coercion = struct inh_tosort_force loc env isevars j let inh_coerce_to_base loc env isevars j = - let typ = whd_betadeltaiota env ( isevars) j.uj_type in + let isevars = ref isevars in + let typ = hnf env !isevars j.uj_type in let ct, typ' = mu env isevars typ in - isevars, { uj_val = app_opt ct j.uj_val; - uj_type = typ' } + let res = + { uj_val = app_opt env isevars ct j.uj_val; + uj_type = typ' } + in !isevars, res let inh_coerce_to_prod loc env isevars t = - let typ = whd_betadeltaiota env ( isevars) (snd t) in + let isevars = ref isevars in + let typ = hnf env !isevars (snd t) in let _, typ' = mu env isevars typ in - isevars, (fst t, typ') + !isevars, (fst t, typ') let inh_coerce_to_fail env evd rigidonly v t c1 = if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) @@ -452,23 +463,23 @@ module Coercion = struct (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) = match n with - None -> - let (evd', val') = - try - inh_conv_coerce_to_fail loc env evd rigidonly - (Some (nf_evar evd cj.uj_val)) - (nf_evar evd cj.uj_type) (nf_evar evd t) - with NoCoercion -> - let sigma = evd in - try - coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t - with NoSubtacCoercion -> - error_actual_type_loc loc env sigma cj t - in - let val' = match val' with Some v -> v | None -> assert(false) in - (evd',{ uj_val = val'; uj_type = t }) - | Some (init, cur) -> - (evd, cj) + | None -> + let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type } + and t = hnf_nodelta env evd t in + let (evd', val') = + try + inh_conv_coerce_to_fail loc env evd rigidonly + (Some cj.uj_val) cj.uj_type t + with NoCoercion -> + (try + coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t + with NoSubtacCoercion -> + error_actual_type_loc loc env evd cj t) + in + let val' = match val' with Some v -> v | None -> assert(false) in + (evd',{ uj_val = val'; uj_type = t }) + | Some (init, cur) -> + (evd, cj) let inh_conv_coerce_to = inh_conv_coerce_to_gen false let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index ecae6759..ced390aa 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -458,7 +458,7 @@ let interp_recursive fixkind l = (* Instantiate evars and check all are resolved *) let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in let evd = Typeclasses.resolve_typeclasses - ~onlyargs:true ~split:true ~fail:false env_rec evd + ~filter:Typeclasses.no_goals ~split:true ~fail:false env_rec evd in let evd = Evarutil.nf_evar_map evd in let fixdefs = List.map (nf_evar evd) fixdefs in diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 64d9f72c..6a5878b3 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -445,12 +445,12 @@ let deps_remaining obls deps = else x :: acc) deps [] -let has_dependencies obls n = - let res = ref false in +let dependencies obls n = + let res = ref Intset.empty in Array.iteri (fun i obl -> if i <> n && Intset.mem n obl.obl_deps then - res := true) + res := Intset.add i !res) obls; !res @@ -502,8 +502,9 @@ let rec solve_obligation prg num tac = in match res with | Remain n when n > 0 -> - if has_dependencies obls num then - ignore(auto_solve_obligations (Some prg.prg_name) None) + let deps = dependencies obls num in + if deps <> Intset.empty then + ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps) | _ -> ()); trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); @@ -553,14 +554,18 @@ and solve_obligation_by_tac prg obls i tac = | Util.Anomaly _ as e -> raise e | e -> false -and solve_prg_obligations prg tac = +and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in let rem = ref rem in let obls' = Array.copy obls in + let p = match oblset with + | None -> (fun _ -> true) + | Some s -> (fun i -> Intset.mem i s) + in let _ = Array.iteri (fun i x -> - if solve_obligation_by_tac prg obls' i tac then - decr rem) + if p i && solve_obligation_by_tac prg obls' i tac then + decr rem) obls' in update_obls prg obls' !rem @@ -582,9 +587,9 @@ and try_solve_obligation n prg tac = and try_solve_obligations n tac = try ignore (solve_obligations n tac) with NoObligations _ -> () -and auto_solve_obligations n tac : progress = +and auto_solve_obligations n ?oblset tac : progress = Flags.if_verbose msgnl (str "Solving obligations automatically..."); - try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent + try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent open Pp let show_obligations_of_prg ?(msg=true) prg = diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 7c0d1232..e56fa4f5 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -67,8 +67,8 @@ let interp env isevars c tycon = let _ = isevars := Evarutil.nf_evar_map !isevars in let evd = consider_remaining_unif_problems env !isevars in (* let unevd = undefined_evars evd in *) - let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in - let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in + let unevd' = Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~split:true ~fail:true env evd in + let unevd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~split:true ~fail:false env unevd' in let evm = unevd' in isevars := unevd'; nf_evar evm j.uj_val, nf_evar evm j.uj_type diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index d5d427c7..9a4e1883 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -88,7 +88,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* coerce to tycon if any *) let inh_conv_coerce_to_tycon loc env evdref j = function - | None -> j_nf_evar !evdref j + | None -> j | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t let push_rels vars env = List.fold_right push_rel vars env @@ -323,7 +323,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct else tycon in match ty with - | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty + | Some (_, t) -> + if Subtac_coercion.disc_subset (whd_betadeltaiota env !evdref t) = None then ty + else None | _ -> None in let fj = pretype ftycon env evdref lvar f in @@ -340,13 +342,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon; let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in evdref := evd; - let hj = pretype (mk_tycon (nf_evar !evdref c1)) env evdref lvar c in + let hj = pretype (mk_tycon c1) env evdref lvar c in let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in - let typ' = nf_evar !evdref typ in apply_rec env (n+1) - { uj_val = nf_evar !evdref value; - uj_type = nf_evar !evdref typ' } - (Option.map (fun (abs, c) -> abs, nf_evar !evdref c) tycon) rest + { uj_val = value; + uj_type = typ } + (Option.map (fun (abs, c) -> abs, c) tycon) rest | _ -> let hj = pretype empty_tycon env evdref lvar c in @@ -354,9 +355,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (join_loc floc argloc) env !evdref resj [hj] in - let resj = j_nf_evar !evdref (apply_rec env 1 fj ftycon args) in + let resj = apply_rec env 1 fj ftycon args in let resj = - match kind_of_term resj.uj_val with + match kind_of_term (whd_evar !evdref resj.uj_val) with | App (f,args) when isInd f or isConst f -> let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in @@ -508,10 +509,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar !evdref pred in let p = nf_evar !evdref p in - (* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*) let f cs b = let n = rel_context_length cs.cs_args in - let pi = lift n pred in (* liftn n 2 pred ? *) + let pi = lift n pred in let pi = beta_applist (pi, [build_dependent_constructor cs]) in let csgn = if not !allow_anonymous_refs then @@ -525,7 +525,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct cs.cs_args in let env_c = push_rels csgn env in -(* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *) let bj = pretype (mk_tycon pi) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs.cs_args in let b1 = f cstrs.(0) b1 in @@ -551,8 +550,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | CastConv (k,t) -> let tj = pretype_type empty_valcon env evdref lvar t in let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in - (* User Casts are for helping pretyping, experimentally not to be kept*) - (* ... except for Correctness *) let v = mkCast (cj.uj_val, k, tj.utj_val) in { uj_val = v; uj_type = tj.utj_val } in @@ -600,9 +597,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct in if resolve_classes then (try - evdref := Typeclasses.resolve_typeclasses ~onlyargs:true + evdref := Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~split:true ~fail:true env !evdref; - evdref := Typeclasses.resolve_typeclasses ~onlyargs:false + evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref with e -> if fail_evar then raise e else ()); evdref := consider_remaining_unif_problems env !evdref; @@ -647,8 +644,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let understand_type sigma env c = snd (ise_pretype_gen true false true sigma env ([],[]) IsType c) - let understand_ltac expand_evar sigma env lvar kind c = - ise_pretype_gen expand_evar false true sigma env lvar kind c + let understand_ltac ?(resolve_classes=false) expand_evar sigma env lvar kind c = + ise_pretype_gen expand_evar false resolve_classes sigma env lvar kind c let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 28bbdd35..fbb44811 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -161,12 +161,11 @@ let print_args env args = Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "") let make_existential loc ?(opaque = Define true) env isevars c = - let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in - let (key, args) = destEvar evar in - (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++ - print_args env args ++ str " for type: "++ - my_print_constr env c) with _ -> ()); - evar + Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c + +let no_goals_or_obligations = function + | GoalEvar | QuestionMark _ -> false + | _ -> true let make_existential_expr loc env c = let key = Evarutil.new_untyped_evar () in diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index de96cc60..112b1795 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -82,6 +82,7 @@ val app_opt : ('a -> 'a) option -> 'a -> 'a val print_args : env -> constr array -> std_ppcmds val make_existential : loc -> ?opaque:obligation_definition_status -> env -> evar_map ref -> types -> constr +val no_goals_or_obligations : Typeclasses.evar_filter val make_existential_expr : loc -> 'a -> 'b -> constr_expr val string_of_hole_kind : hole_kind -> string val evars_of_term : evar_map -> evar_map -> constr -> evar_map diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 3c3e54fa..56ce7ef2 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -107,7 +107,7 @@ let pr_context_xml env = let pr_subgoal_metas_xml metas env= let pr_one (meta, typ) = - fnl () ++ str "" in List.fold_left (++) (mt ()) (List.map pr_one metas) @@ -117,7 +117,7 @@ let pr_goal_xml sigma g = let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in if Decl_mode.try_get_info sigma g = None then (hov 2 (str "" ++ fnl () ++ str "" ++ (pr_context_xml env)) ++ fnl () ++ str "") -- cgit v1.2.3