From 4767d724d489a7ad67f696e9401e70b9f9ae2143 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 15 Oct 2007 19:55:12 +0000 Subject: Imported Upstream version 8.1.pl2+dfsg --- tactics/setoid_replace.ml | 114 ++++++++++++++++++++++++++-------------------- tactics/tacinterp.ml | 35 ++++++++++---- 2 files changed, 90 insertions(+), 59 deletions(-) (limited to 'tactics') diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index c14462eb..9c23dda5 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: setoid_replace.ml 9853 2007-05-23 14:25:47Z letouzey $ *) +(* $Id: setoid_replace.ml 10213 2007-10-10 13:05:59Z letouzey $ *) open Tacmach open Proof_type @@ -819,15 +819,16 @@ let new_morphism m signature id hook = try find_relation_class output' with Not_found -> errorlabstrm "Add Morphism" (str "Not a valid signature: " ++ pr_lconstr output' ++ - str " is neither a registered relation nor the Leibniz " ++ - str " equality.") in + str " is neither a registered relation nor the Leibniz " ++ + str " equality.") in let rel_a,rel_quantifiers_no = match rel with Relation rel -> rel.rel_a, rel.rel_quantifiers_no | Leibniz (Some t) -> t, 0 - | Leibniz None -> assert false in + | Leibniz None -> let _,t = decompose_prod typ in t, 0 in let rel_a_n = - clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in + clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a + in try let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in let argsrev,_ = decompose_prod output_rel_a_n in @@ -1890,47 +1891,49 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_ | Some tac -> Tacticals.tclTRY (Tacticals.tclCOMPLETE tac ) in try - let relation = - match relation with - Some rel -> - (try - match find_relation_class rel with - Relation sa -> sa - | Leibniz _ -> raise Optimize - with - Not_found -> - errorlabstrm "Setoid_rewrite" - (pr_lconstr rel ++ str " is not a registered relation.")) - | None -> - match default_relation_for_carrier (pf_type_of gl c1) with - Relation sa -> sa - | Leibniz _ -> raise Optimize - in - let eq_left_to_right = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in - let eq_right_to_left = mkApp (relation.rel_aeq, [| c2 ; c1 |]) in - let replace dir eq = - tclTHENS (assert_tac false Anonymous eq) - [onLastHyp (fun id -> - tclTHEN - (rewrite_tac dir (mkVar id) ~new_goals) - (clear [id])); - try_prove_eq_tac] - in - tclORELSE - (replace true eq_left_to_right) (replace false eq_right_to_left) gl - with - Optimize -> (* (!replace tac_opt c1 c2) gl *) - let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in - tclTHENS (assert_tac false Anonymous eq) - [onLastHyp (fun id -> - tclTHEN - (rewrite_tac false (mkVar id) ~new_goals) - (clear [id])); - try_prove_eq_tac] gl + let carrier,args = decompose_app (pf_type_of gl c1) in + let relation = + match relation with + Some rel -> + (try + match find_relation_class rel with + Relation sa -> if not (eq_constr carrier sa.rel_a) then + errorlabstrm "Setoid_rewrite" + (str "the carrier of " ++ pr_lconstr rel ++ + str " does not match the type of " ++ pr_lconstr c1); + sa + | Leibniz _ -> raise Optimize + with + Not_found -> + errorlabstrm "Setoid_rewrite" + (pr_lconstr rel ++ str " is not a registered relation.")) + | None -> + match default_relation_for_carrier (pf_type_of gl c1) with + Relation sa -> sa + | Leibniz _ -> raise Optimize + in + let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in + let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in + let replace dir eq = + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN + (rewrite_tac dir (mkVar id) ~new_goals) + (clear [id])); + try_prove_eq_tac] + in + tclORELSE + (replace true eq_left_to_right) (replace false eq_right_to_left) gl + with + Optimize -> (* (!replace tac_opt c1 c2) gl *) + let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN + (rewrite_tac false (mkVar id) ~new_goals) + (clear [id])); + try_prove_eq_tac] gl - - - let setoid_replace = general_setoid_replace general_s_rewrite let setoid_replace_in tac_opt id relation c1 c2 ~new_goals gl = general_setoid_replace (general_s_rewrite_in id) tac_opt relation c1 c2 ~new_goals gl @@ -1970,11 +1973,22 @@ let setoid_symmetry gl = Optimize -> symmetry_red true gl let setoid_symmetry_in id gl = - let new_hyp = - let _,he,c1,c2 = analyse_hypothesis gl (mkVar id) in - mkApp (he, [| c2 ; c1 |]) - in - cut_replacing id new_hyp (tclTHEN setoid_symmetry) gl + let ctype = pf_type_of gl (mkVar id) in + let binders,concl = Sign.decompose_prod_assum ctype in + let (equiv, args) = decompose_app concl in + let rec split_last_two = function + | [c1;c2] -> [],(c1, c2) + | x::y::z -> let l,res = split_last_two (y::z) in x::l, res + | _ -> error "The term provided is not an equivalence" + in + let others,(c1,c2) = split_last_two args in + let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in + let new_hyp' = mkApp (he, [| c2 ; c1 |]) in + let new_hyp = it_mkProd_or_LetIn new_hyp' binders in + tclTHENS (cut new_hyp) + [ intro_replacing id; + tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ] + gl let setoid_transitivity c gl = try diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ac6a396f..37b3cbcb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: tacinterp.ml 10135 2007-09-21 14:28:12Z herbelin $ *) open Constrintern open Closure @@ -436,9 +436,16 @@ let rec intern_intro_pattern lf ist = function and intern_case_intro_pattern lf ist = List.map (List.map (intern_intro_pattern lf ist)) -let intern_quantified_hypothesis ist x = - (* We use identifier both for variables and quantified hyps (no way to - statically check the existence of a quantified hyp); thus nothing to do *) +let intern_quantified_hypothesis ist = function + | AnonHyp n -> AnonHyp n + | NamedHyp id -> + (* Uncomment to disallow "intros until n" in ltac when n is not bound *) + NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*)) + +let intern_binding_name ist x = + (* We use identifier both for variables and binding names *) + (* Todo: consider the body of the lemma to which the binding refer + and if a term w/o ltac vars, check the name is indeed quantified *) x let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c = @@ -453,7 +460,7 @@ let intern_type = intern_constr_gen true (* Globalize bindings *) let intern_binding ist (loc,b,c) = - (loc,intern_quantified_hypothesis ist b,intern_constr ist c) + (loc,intern_binding_name ist b,intern_constr ist c) let intern_bindings ist = function | NoBindings -> NoBindings @@ -1465,8 +1472,17 @@ let interp_quantified_hypothesis ist = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id) - with Not_found - | Stdpp.Exc_located (_, UserError _) | UserError _ (*Compat provisoire*) + with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _ + -> NamedHyp id + +let interp_binding_name ist = function + | AnonHyp n -> AnonHyp n + | NamedHyp id -> + (* If a name is bound, it has to be a quantified hypothesis *) + (* user has to use other names for variables if these ones clash with *) + (* a name intented to be used as a (non-variable) identifier *) + try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id) + with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _ -> NamedHyp id (* Quantified named or numbered hypothesis or hypothesis in context *) @@ -1495,7 +1511,7 @@ let interp_induction_arg ist gl = function (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id))))) let interp_binding ist gl (loc,b,c) = - (loc,interp_quantified_hypothesis ist b,pf_interp_constr ist gl c) + (loc,interp_binding_name ist b,pf_interp_constr ist gl c) let interp_bindings ist gl = function | NoBindings -> NoBindings @@ -2349,7 +2365,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l) | TacCut c -> TacCut (subst_rawconstr subst c) - | TacAssert (b,na,c) -> TacAssert (b,na,subst_rawconstr subst c) + | TacAssert (b,na,c) -> + TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c) | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp) -- cgit v1.2.3