From 9accb5a66da5d68fa01c4c3b8e7b74985e84f6fa Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 20 May 2007 17:44:23 +0000 Subject: - Propagation des evars non résolues vers les with_bindings; permet par exemple de résoudre des buts comme celui-ci : MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Record nat_retract : Type := {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}. Goal nat_retract. exists (fun x => x) (fun x => x). - Nouvelle tentative d'utilisation des types des metas/evars pour inférer de nouvelles instances de metas/evars; permet par exemple d'utiliser f_equal sans option with, mais aussi, avec la modif précédente, de résoudre des buts tels que Goal exists f:bool->Prop, f true = True. exists (fun x => True). [Les expériences passées avaient montré qu'en prenant en compte les types dans l'unification, on peut unifier trop tôt une evars à une mauvaise sorte; à défaut de mécanisme de prise en compte des problème d'unification avec sous-typage, on s'est interdit ici d'unifier des types qui sont des arités.] - Tout les constr de tactic_expr deviennent des open_constr (même si seul with_bindings les accepte au final... c'est pas l'idéal). - Renommage env -> evd et templenv -> env dans clausenv. - Renommage closed_generic_argument -> typed_generic_argument. - Renommage closed_abstract_argument_type -> typed_abstract_argument_type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/first-order/instances.ml | 4 ++-- contrib/funind/indfun_main.ml4 | 23 ++++++++++++++++++++--- contrib/funind/invfun.ml | 10 +++++----- contrib/interface/showproof.ml | 16 ++++++++-------- contrib/jprover/jprover.ml4 | 2 +- contrib/omega/coq_omega.ml | 2 +- contrib/recdef/recdef.ml4 | 26 +++++++++++++------------- contrib/subtac/subtac_utils.ml | 2 +- 8 files changed, 51 insertions(+), 34 deletions(-) (limited to 'contrib') diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 8eeb8b642..fac39df93 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -182,11 +182,11 @@ let right_instance_tac inst continue seq= [introf; (fun gls-> split (Rawterm.ImplicitBindings - [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); + [inj_open (mkVar (Tacmach.pf_nth_hyp_id gls 1))]) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (Rawterm.ImplicitBindings [t])) + (tclTHEN (split (Rawterm.ImplicitBindings [inj_open t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index ae3da9523..169542e3c 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -29,20 +29,37 @@ let pr_bindings prc prlc = function Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | Rawterm.NoBindings -> mt () - let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) - let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) +(* Duplication of printing functions because "'a with_bindings" is + (internally) not uniform in 'a: indeed constr_with_bindings at the + "typed" level has type "open_constr with_bindings" instead of + "constr with_bindings"; hence, its printer cannot be polymorphic in + (prc,prlc)... *) + +let pr_with_bindings_typed prc prlc (c,bl) = + prc c ++ + hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl) + +let pr_fun_ind_using_typed prc prlc _ opt_c = + match opt_c with + | None -> mt () + | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b)) + ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings_opt - PRINTED BY pr_fun_ind_using + PRINTED BY pr_fun_ind_using_typed + RAW_TYPED AS constr_with_bindings_opt + RAW_PRINTED BY pr_fun_ind_using + GLOB_TYPED AS constr_with_bindings_opt + GLOB_PRINTED BY pr_fun_ind_using | [ "using" constr_with_bindings(c) ] -> [ Some c ] | [ ] -> [ None ] END diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 9ec02d4c4..fbf72805b 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -23,13 +23,13 @@ open Hiddentac let pr_binding prc = function - | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.NamedHyp id, (_,c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.AnonHyp n, (_,c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | Rawterm.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l + Util.prlist_with_sep spc (fun (_,c) -> prc c) l | Rawterm.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l @@ -425,7 +425,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Nameops.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid + (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -435,7 +435,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Nameops.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid) + (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 48c9b9eb4..ab4da05e3 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -166,7 +166,7 @@ let rule_to_ntactic r = let rt = (match r with Nested(Tactic (t,_),_) -> t - | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h) + | Prim (Refine h) -> TacAtom (dummy_loc,TacExact (Tactics.inj_open h)) | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in if rule_is_complex r then (match rt with @@ -1184,8 +1184,8 @@ let rec natural_ntree ig ntree = | TacIntroMove _ -> natural_intros ig lh g gs ltree | TacFix (_,n) -> natural_fix ig lh g gs n ltree | TacSplit (_,NoBindings) -> natural_split ig lh g gs ge [] ltree - | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge l ltree - | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree + | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree + | TacGeneralize l -> natural_generalize ig lh g gs ge (List.map snd l) ltree | TacRight _ -> natural_right ig lh g gs ltree | TacLeft _ -> natural_left ig lh g gs ltree | (* "Simpl" *)TacReduce (r,cl) -> @@ -1202,17 +1202,17 @@ let rec natural_ntree ig ntree = | TacExtend (_,"InductionIntro",[a]) -> let id=(out_gen wit_ident a) in natural_induction ig lh g gs ge id ltree true - | TacApply (false,(c,_)) -> natural_apply ig lh g gs c ltree - | TacExact c -> natural_exact ig lh g gs c ltree - | TacCut c -> natural_cut ig lh g gs c ltree + | TacApply (false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree + | TacExact c -> natural_exact ig lh g gs (snd c) ltree + | TacCut c -> natural_cut ig lh g gs (snd c) ltree | TacExtend (_,"CutIntro",[a]) -> let _c = out_gen wit_constr a in natural_cutintro ig lh g gs a ltree - | TacCase (c,_) -> natural_case ig lh g gs ge c ltree false + | TacCase (c,_) -> natural_case ig lh g gs ge (snd c) ltree false | TacExtend (_,"CaseIntro",[a]) -> let c = out_gen wit_constr a in natural_case ig lh g gs ge c ltree true - | TacElim ((c,_),_) -> natural_elim ig lh g gs ge c ltree false + | TacElim ((c,_),_) -> natural_elim ig lh g gs ge (snd c) ltree false | TacExtend (_,"ElimIntro",[a]) -> let c = out_gen wit_constr a in natural_elim ig lh g gs ge c ltree true diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4 index 294943f7d..5fd763c36 100644 --- a/contrib/jprover/jprover.ml4 +++ b/contrib/jprover/jprover.ml4 @@ -410,7 +410,7 @@ i*) | Negl -> dyn_negl s1 | Allr -> dyn_allr (JT.dest_var t2) | Alll -> dyn_alll s1 s2 (constr_of_jterm t2) - | Exr -> dyn_exr (constr_of_jterm t2) + | Exr -> dyn_exr (Tactics.inj_open (constr_of_jterm t2)) | Exl -> dyn_exl s1 s2 (JT.dest_var t2) | Ax -> T.assumption (*i TCL.tclIDTAC i*) | Truer -> dyn_truer diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 951378d4b..497fcdb6c 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -1221,7 +1221,7 @@ let replay_history tactic_normalisation = (clear [aux]); (intros_using [id]); (loop l) ]; - tclTHEN (exists_tac eq1) reflexivity ] + tclTHEN (exists_tac (inj_open eq1)) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 7a2133a02..49791c367 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -416,8 +416,8 @@ let base_leaf_terminate (func:global_reference) eqs expr = [k';h] -> k',h | _ -> assert false in - tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [expr])); - observe_tac "second split" (split (ImplicitBindings [delayed_force coq_O])); + tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [inj_open expr])); + observe_tac "second split" (split (ImplicitBindings [inj_open (delayed_force coq_O)])); observe_tac "intro k" (h_intro k'); observe_tac "case on k" (tclTHENS @@ -459,7 +459,7 @@ let rec compute_le_proofs = function in apply_with_bindings (le_trans, - ExplicitBindings[dummy_loc,NamedHyp m_id,a]) + ExplicitBindings[dummy_loc,NamedHyp m_id,inj_open a]) g ) [compute_le_proofs tl; @@ -477,7 +477,7 @@ let make_lt_proof pmax le_proof = in apply_with_bindings (le_lt_trans, - ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g) + ExplicitBindings[dummy_loc,NamedHyp m_id, inj_open pmax]) g) [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];; @@ -496,8 +496,8 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs = tclTHENS (general_rewrite_bindings false (mkVar eq, - ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; - dummy_loc, NamedHyp def_id, mkVar def]) false) + ExplicitBindings[dummy_loc, NamedHyp k_id, inj_open (mkVar k); + dummy_loc, NamedHyp def_id, inj_open (mkVar def)]) false) [list_cond_rewrite k def pmax eqs le_proofs; observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g ) @@ -515,7 +515,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs let ids = h'::ids in let def = next_global_ident_away true def_id ids in tclTHENLIST - [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max])); + [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [inj_open s_max])); observe_tac "introduce_all_equalities_final intro k" (h_intro k); tclTHENS (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k))) @@ -575,8 +575,8 @@ let rec introduce_all_values is_mes acc_inv func context_fn (match args with [] -> tclTHENLIST - [observe_tac "split" (split(ImplicitBindings - [context_fn (List.map mkVar (List.rev values))])); + [observe_tac "split" (split(ImplicitBindings + [inj_open (context_fn (List.map mkVar (List.rev values)))])); observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])] | arg::args -> @@ -1194,9 +1194,9 @@ let rec introduce_all_values_eq cont_tac functional termine general_rewrite_bindings false (mkVar heq1, ExplicitBindings[dummy_loc,NamedHyp k_id, - f_S(f_S(mkVar pmax)); + inj_open (f_S(f_S(mkVar pmax))); dummy_loc,NamedHyp def_id, - f]) false gls ) + inj_open f]) false gls ) [tclTHENLIST [simpl_iter(); unfold_constr (reference_of_constr functional); @@ -1247,8 +1247,8 @@ let rec introduce_all_values_eq cont_tac functional termine (mkVar heq, ExplicitBindings [dummy_loc, NamedHyp k_id, - f_S(mkVar pmax'); - dummy_loc, NamedHyp def_id, f]) false)) + inj_open (f_S(mkVar pmax')); + dummy_loc, NamedHyp def_id, inj_open f]) false)) g ) [tclIDTAC; diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index fb58a14eb..5a32d2e42 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -231,7 +231,7 @@ let build_dependent_sum l = ([intros; (tclTHENSEQ [constructor_tac (Some 1) 1 - (Rawterm.ImplicitBindings [mkVar n]); + (Rawterm.ImplicitBindings [inj_open (mkVar n)]); cont]); ]))) in -- cgit v1.2.3