From 5d8d8e858e56c0d12cb262d5ff8e733ae7afc102 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 10 Jun 2008 19:35:23 +0000 Subject: - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) - Changement au passage de la convention "at -n1 ... -n2" en "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut pas mélanger des positifs et des négatifs. - Au passage: - simplification de gclause avec fusion de onconcl et concl_occs, - généralisation de l'utilisation de la désignation des occurrences par la négative aux cas de setoid_rewrite, clrewrite et rewrite at, - correction d'un bug de "rewrite in at" qui utilisait le at de la conclusion dans les hyps. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/firstorder/rules.ml | 6 ++-- contrib/funind/functional_principles_proofs.ml | 13 ++++---- contrib/funind/invfun.ml | 5 +-- contrib/funind/recdef.ml | 24 +++++++-------- contrib/interface/blast.ml | 4 +-- contrib/interface/pbp.ml | 2 +- contrib/interface/showproof.ml | 4 +-- contrib/interface/xlate.ml | 42 +++++++++++++++++--------- contrib/omega/coq_omega.ml | 2 +- contrib/ring/ring.ml | 6 ++-- contrib/setoid_ring/newring.ml4 | 3 +- 11 files changed, 63 insertions(+), 48 deletions(-) (limited to 'contrib') diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml index b6112e653..813e951cf 100644 --- a/contrib/firstorder/rules.ml +++ b/contrib/firstorder/rules.ml @@ -204,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq= let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str let defined_connectives=lazy - [[],EvalConstRef (destConst (constant "not")); - [],EvalConstRef (destConst (constant "iff"))] + [all_occurrences,EvalConstRef (destConst (constant "not")); + all_occurrences,EvalConstRef (destConst (constant "iff"))] let normalize_evaluables= onAllClauses @@ -213,4 +213,4 @@ let normalize_evaluables= None->unfold_in_concl (Lazy.force defined_connectives) | Some ((_,id),_)-> unfold_in_hyp (Lazy.force defined_connectives) - (([],id),Tacexpr.InHypTypeOnly)) + ((Rawterm.all_occurrences_expr,id),Tacexpr.InHypTypeOnly)) diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 558ca6c21..3d80bd004 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -637,7 +637,7 @@ let build_proof [ h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; - pattern_option [[-1],t] None; + pattern_option [(false,[1]),t] None; h_simplest_case t; (fun g' -> let g'_nb_prod = nb_prod (pf_concl g') in @@ -1246,7 +1246,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [([],Names.EvalConstRef fname)]; + [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)]; let do_prove = build_proof interactive_proof @@ -1347,11 +1347,10 @@ let build_clause eqs = { Tacexpr.onhyps = Some (List.map - (fun id -> ([],id),Tacexpr.InHyp) + (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp) eqs ); - Tacexpr.onconcl = false; - Tacexpr.concl_occs = [] + Tacexpr.concl_occs = Rawterm.no_occurrences_expr } let rec rewrite_eqs_in_eqs eqs = @@ -1364,7 +1363,7 @@ let rec rewrite_eqs_in_eqs eqs = (fun id gl -> observe_tac (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) - (tclTRY (Equality.general_rewrite_in true [] id (mkVar eq) false)) + (tclTRY (Equality.general_rewrite_in true all_occurrences id (mkVar eq) false)) gl ) eqs @@ -1386,7 +1385,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (fun g -> if is_mes then - unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g + unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g else tclIDTAC g ); observe_tac "rew_and_finish" diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index a5bd519e2..0160c290f 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -16,6 +16,7 @@ open Tacticals open Tactics open Indfun_common open Tacmach +open Termops open Sign open Hiddentac @@ -314,7 +315,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | None -> (id::pre_args,pre_tac) | Some b -> (pre_args, - tclTHEN (h_reduce (Rawterm.Unfold([[],EvalVarRef id])) allHyps) pre_tac + tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac ) else (pre_args,pre_tac) @@ -687,7 +688,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = h_generalize (List.map mkVar ids); thin ids ] - else unfold_in_concl [([],Names.EvalConstRef (destConst f))] + else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))] in (* The proof of each branche itself *) let ind_number = ref 0 in diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index f4f852d36..13989f03b 100644 --- a/contrib/funind/recdef.ml +++ b/contrib/funind/recdef.ml @@ -296,7 +296,7 @@ let mkCaseEq a : tactic = [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; (fun g2 -> change_in_concl None - (pattern_occs [([-1], a)] (pf_env g2) Evd.empty (pf_concl g2)) + (pattern_occs [((false,[1]), a)] (pf_env g2) Evd.empty (pf_concl g2)) g2); simplest_case a] g);; @@ -323,7 +323,7 @@ let mkDestructEq : [h_generalize new_hyps; (fun g2 -> change_in_concl None - (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); + (pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); simplest_case expr], to_revert let rec mk_intros_and_continue thin_intros (extra_eqn:bool) @@ -336,7 +336,7 @@ let rec mk_intros_and_continue thin_intros (extra_eqn:bool) h_intros thin_intros; tclMAP - (fun eq -> tclTRY (Equality.general_rewrite_in true [] teq eq false)) + (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences teq eq false)) (List.rev eqs); (fun g1 -> let ty_teq = pf_type_of g1 (mkVar teq) in @@ -397,7 +397,7 @@ let tclUSER tac is_mes l g = clear_tac; if is_mes then tclTHEN - (unfold_in_concl [([], evaluable_of_global_reference + (unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) tac else tac @@ -496,7 +496,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs = Nameops.out_name k_na,Nameops.out_name def_na in tclTHENS - (general_rewrite_bindings false [] + (general_rewrite_bindings false all_occurrences (mkVar eq, ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; dummy_loc, NamedHyp def_id, mkVar def]) false) @@ -531,7 +531,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs observe_tac "intros k h' def" (h_intros [k;h';def]); observe_tac "simple_iter" (simpl_iter onConcl); observe_tac "unfold functional" - (unfold_in_concl[([1],evaluable_of_global_reference func)]); + (unfold_in_concl[((true,[1]),evaluable_of_global_reference func)]); observe_tac "rewriting equations" (list_rewrite true eqs); observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite k def bound cond_eqs le_proofs); @@ -1120,7 +1120,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let x = n_x_id ids nargs in tclTHENLIST [ h_intros x; - unfold_in_concl [([], evaluable_of_global_reference f)]; + unfold_in_concl [(all_occurrences, evaluable_of_global_reference f)]; observe_tac "simplest_case" (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x)))); @@ -1144,7 +1144,7 @@ let base_leaf_eq func eqs f_id g = [|mkApp (delayed_force coq_S, [|mkVar p|]); mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|]))); simpl_iter onConcl; - tclTRY (unfold_in_concl [([1], evaluable_of_global_reference func)]); + tclTRY (unfold_in_concl [((true,[1]), evaluable_of_global_reference func)]); list_rewrite true eqs; apply (delayed_force refl_equal)] g;; @@ -1160,9 +1160,9 @@ let rec introduce_all_values_eq cont_tac functional termine [forward None (IntroIdentifier heq2) (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|])); simpl_iter (onHyp heq2); - unfold_in_hyp [([1], evaluable_of_global_reference + unfold_in_hyp [((true,[1]), evaluable_of_global_reference (global_of_constr functional))] - (([], heq2), Tacexpr.InHyp); + ((all_occurrences_expr, heq2), Tacexpr.InHyp); tclTHENS (fun gls -> let t_eq = compute_renamed_type gls (mkVar heq2) in @@ -1170,7 +1170,7 @@ let rec introduce_all_values_eq cont_tac functional termine let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in Nameops.out_name def_na in - observe_tac "rewrite heq" (general_rewrite_bindings false [] + observe_tac "rewrite heq" (general_rewrite_bindings false all_occurrences (mkVar heq2, ExplicitBindings[dummy_loc,NamedHyp def_id, f]) false) gls) @@ -1226,7 +1226,7 @@ let rec introduce_all_values_eq cont_tac functional termine f_S(mkVar pmax'); dummy_loc, NamedHyp def_id, f]) in - observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false [] + observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences c_b false)) g ) diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 10fafaefc..6ec0fac42 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -188,7 +188,7 @@ and e_my_find_search db_list local_db hdc concl = | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (unify_e_resolve (term,cl)) (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> Auto.conclPattern concl (Option.get p) tacast in @@ -403,7 +403,7 @@ and my_find_search db_list local_db hdc concl = tclTHEN (unify_resolve st (term,cl)) (trivial_fail_db db_list local_db) - | Unfold_nth c -> unfold_in_concl [[],c] + | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> conclPattern concl (Option.get p) tacast)) tacl diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index ac152f906..06b957d9c 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -166,7 +166,7 @@ let make_pbp_atomic_tactic = function TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x])) | PbpGeneralize (h,args) -> let l = List.map make_pbp_pattern args in - TacAtom (zz, TacGeneralize [([],make_app (make_var h) l),Anonymous]) + TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous]) | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings)) | PbpRight -> TacAtom (zz, TacRight (false,NoBindings)) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index a2a504fb4..953fb5e79 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1612,7 +1612,7 @@ and natural_fix ig lh g gs narg ltree = | _ -> assert false and natural_reduce ig lh g gs ge mode la ltree = match la with - {onhyps=Some[];onconcl=true} -> + {onhyps=Some[]} when la.concl_occs <> no_occurrences_expr -> spv [ (natural_lhyp lh ig.ihsg); (show_goal2 lh ig g gs ""); @@ -1620,7 +1620,7 @@ and natural_reduce ig lh g gs ge mode la ltree = {ihsg=All_subgoals_hyp;isgintro="simpl"}) ltree) ] - | {onhyps=Some[hyp]; onconcl=false} -> + | {onhyps=Some[hyp]} when la.concl_occs = no_occurrences_expr -> spv [ (natural_lhyp lh ig.ihsg); (show_goal2 lh ig g gs ""); diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b041272c1..fa8f05713 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -464,24 +464,31 @@ let (xlate_ident_or_metaid: AI (_, x) -> xlate_ident x | MetaId(_, x) -> CT_metaid x;; +let nums_of_occs (b,nums) = + if b then nums + else List.map (function ArgArg x -> ArgArg (-x) | y -> y) nums + let xlate_hyp = function | AI (_,id) -> xlate_ident id | MetaId _ -> xlate_error "MetaId should occur only in quotations" let xlate_hyp_location = function - | (nums, AI (_,id)), InHypTypeOnly -> - CT_intype(xlate_ident id, nums_or_var_to_int_list nums) - | (nums, AI (_,id)), InHypValueOnly -> - CT_invalue(xlate_ident id, nums_or_var_to_int_list nums) - | ([], AI (_,id)), InHyp -> + | (occs, AI (_,id)), InHypTypeOnly -> + CT_intype(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs)) + | (occs, AI (_,id)), InHypValueOnly -> + CT_invalue(xlate_ident id, nums_or_var_to_int_list (nums_of_occs occs)) + | ((true,[]), AI (_,id)), InHyp -> CT_coerce_UNFOLD_to_HYP_LOCATION (CT_coerce_ID_to_UNFOLD (xlate_ident id)) - | (a::l, AI (_,id)), InHyp -> + | ((_,a::l as occs), AI (_,id)), InHyp -> + let nums = nums_of_occs occs in + let a = List.hd nums and l = List.tl nums in CT_coerce_UNFOLD_to_HYP_LOCATION (CT_unfold_occ (xlate_ident id, CT_int_ne_list(num_or_var_to_int a, nums_or_var_to_int_list_aux l))) + | ((false,[]), AI (_,id)), InHyp -> xlate_error "Unused" | (_, MetaId _),_ -> xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)" @@ -494,7 +501,7 @@ let xlate_clause cls = | Some l -> CT_hyp_location_list(List.map xlate_hyp_location l) in CT_clause (hyps_info, - if cls.onconcl then + if cls.concl_occs <> no_occurrences_expr then CT_coerce_STAR_to_STAR_OPT CT_star else CT_coerce_NONE_to_STAR_OPT CT_none) @@ -667,11 +674,13 @@ let xlate_using = function | Some (c2,sl2) -> CT_using (xlate_formula c2, xlate_bindings sl2);; let xlate_one_unfold_block = function - ([],qid) -> + ((true,[]),qid) -> CT_coerce_ID_to_UNFOLD(apply_or_by_notation tac_qualid_to_ct_ID qid) - | (n::nums, qid) -> + | (((_,_::_) as occs), qid) -> + let l = nums_of_occs occs in CT_unfold_occ(apply_or_by_notation tac_qualid_to_ct_ID qid, - nums_or_var_to_int_ne_list n nums) + nums_or_var_to_int_ne_list (List.hd l) (List.tl l)) + | ((false,[]), qid) -> xlate_error "Unused" ;; let xlate_with_names = function @@ -732,7 +741,8 @@ and xlate_red_tactic = | CbvVm -> CT_cbvvm | Hnf -> CT_hnf | Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE - | Simpl (Some (l,c)) -> + | Simpl (Some (occs,c)) -> + let l = nums_of_occs occs in CT_simpl (CT_coerce_PATTERN_to_PATTERN_OPT (CT_pattern_occ @@ -751,9 +761,9 @@ and xlate_red_tactic = | Fold formula_list -> CT_fold(CT_formula_list(List.map xlate_formula formula_list)) | Pattern l -> - let pat_list = List.map (fun (nums,c) -> + let pat_list = List.map (fun (occs,c) -> CT_pattern_occ - (CT_int_list (nums_or_var_to_int_list_aux nums), + (CT_int_list (nums_or_var_to_int_list_aux (nums_of_occs occs)), xlate_formula c)) l in (match pat_list with | first :: others -> CT_pattern (CT_pattern_ne_list (first, others)) @@ -907,6 +917,7 @@ and xlate_tac = | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b) | TacChange (Some(l,c), f, b) -> (* TODO LATER: combine with other constructions of pattern_occ *) + let l = nums_of_occs l in CT_change_local( CT_pattern_occ(CT_int_list(nums_or_var_to_int_list_aux l), xlate_formula c), @@ -1151,8 +1162,9 @@ and xlate_tac = | TacSpecialize (nopt, (c,sl)) -> CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl) | TacGeneralize [] -> xlate_error "" - | TacGeneralize ((([],first),Anonymous) :: cl) - when List.for_all (fun ((o,_),na) -> o = [] & na = Anonymous) cl -> + | TacGeneralize ((((true,[]),first),Anonymous) :: cl) + when List.for_all (fun ((o,_),na) -> o = all_occurrences_expr + & na = Anonymous) cl -> CT_generalize (CT_formula_ne_list (xlate_formula first, List.map (fun ((_,c),_) -> xlate_formula c) cl)) diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index b96b57d5b..0bb18b3b0 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -133,7 +133,7 @@ let exists_tac c = constructor_tac false (Some 1) 1 (Rawterm.ImplicitBindings [c let generalize_tac t = generalize_time (generalize t) let elim t = elim_time (simplest_elim t) let exact t = exact_time (Tactics.refine t) -let unfold s = Tactics.unfold_in_concl [[], Lazy.force s] +let unfold s = Tactics.unfold_in_concl [all_occurrences, Lazy.force s] let rev_assoc k = let rec loop = function diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 66246faf5..92f74d1d9 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -826,9 +826,11 @@ let raw_polynom th op lc gl = c'''i; ci; c'i_eq_c''i |])))) (tclTHENS (tclORELSE - (Setoid_replace.general_s_rewrite true [] c'i_eq_c''i + (Setoid_replace.general_s_rewrite true + Termops.all_occurrences c'i_eq_c''i ~new_goals:[]) - (Setoid_replace.general_s_rewrite false [] c'i_eq_c''i + (Setoid_replace.general_s_rewrite false + Termops.all_occurrences c'i_eq_c''i ~new_goals:[])) [tac])) else diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index c3caa403e..474b3616a 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -104,7 +104,8 @@ let protect_tac map = Tactics.reduct_option (protect_red map,DEFAULTcast) None ;; let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(([],id),InHyp));; + Tactics.reduct_option (protect_red map,DEFAULTcast) + (Some((all_occurrences_expr,id),InHyp));; TACTIC EXTEND protect_fv -- cgit v1.2.3