From c039d78bd098a499a34038e64bd1e5fbe280d7f3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 28 Jul 2017 15:31:28 +0200 Subject: [PATCH] locus: Add an AtLeastOneOccurrence constructor. The semantics is obviously that it is an error if not at least one occurrence is found (natural semantics for rewriting for example). --- plugins/ltac/tacintern.ml | 2 +- plugins/ltac/tacinterp.ml | 2 +- pretyping/evarconv.ml | 2 +- pretyping/find_subterm.ml | 2 +- pretyping/locus.ml | 1 + pretyping/locusops.ml | 17 ++++++++++++----- pretyping/locusops.mli | 2 ++ pretyping/tacred.ml | 1 + pretyping/unification.ml | 2 +- tactics/autorewrite.ml | 2 +- tactics/equality.ml | 15 ++++++++------- tactics/ppred.ml | 1 + 12 files changed, 31 insertions(+), 18 deletions(-) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index a1e21aab04b8..543d4de0fe7c 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -557,7 +557,7 @@ let rec intern_atomic lf ist x = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in TacChange (None, diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 525ff7fd0f6c..d17a8e3cc811 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1746,7 +1746,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in let c_interp patvars env sigma = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aa30ed8d2e59..f8e5e0759b7c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1148,7 +1148,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | (id,_,c,cty,evsref,filter,occs)::subst -> let set_var k = match occs with - | Some Locus.AllOccurrences -> mkVar id + | Some (Locus.AtLeastOneOccurrence | Locus.AllOccurrences) -> mkVar id | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") | None -> let evty = set_holes evdref cty subst in diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index b16087031bc8..d150f8e1cb66 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -125,7 +125,7 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t = end; add_subst t subst; incr pos; (* Check nested matching subterms *) - if occs != Locus.AllOccurrences && occs != Locus.NoOccurrences then + if not (Locusops.is_all_occurrences occs) && occs != Locus.NoOccurrences then begin nested := true; ignore (subst_below k t); nested := false end; (* Do the effective substitution *) Vars.lift k (bywhat ())) diff --git a/pretyping/locus.ml b/pretyping/locus.ml index 37dd120c1a3a..087a6b9174d5 100644 --- a/pretyping/locus.ml +++ b/pretyping/locus.ml @@ -20,6 +20,7 @@ type 'a or_var = type 'a occurrences_gen = | AllOccurrences + | AtLeastOneOccurrence | AllOccurrencesBut of 'a list (** non-empty *) | NoOccurrences | OnlyOccurrences of 'a list (** non-empty *) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 6b6a3f8a9fc0..aaa4ce684d76 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -19,15 +19,17 @@ let occurrences_map f = function | AllOccurrencesBut l -> let l' = f l in if l' = [] then AllOccurrences else AllOccurrencesBut l' - | (NoOccurrences|AllOccurrences) as o -> o + | (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o let convert_occs = function + | AtLeastOneOccurrence -> (false,[]) | AllOccurrences -> (false,[]) | AllOccurrencesBut l -> (false,l) | NoOccurrences -> (true,[]) | OnlyOccurrences l -> (true,l) let is_selected occ = function + | AtLeastOneOccurrence -> true | AllOccurrences -> true | AllOccurrencesBut l -> not (Int.List.mem occ l) | OnlyOccurrences l -> Int.List.mem occ l @@ -46,6 +48,11 @@ let is_nowhere = function | { onhyps=Some[]; concl_occs=NoOccurrences } -> true | _ -> false +let is_all_occurrences = function + | AtLeastOneOccurrence + | AllOccurrences -> true + | _ -> false + (** Clause conversion functions, parametrized by a hyp enumeration function *) (** From [clause] to [simple_clause] *) @@ -61,12 +68,12 @@ let simple_clause_of enum_hyps cl = List.map Option.make (enum_hyps ()) | Some l -> List.map (fun ((occs,id),w) -> - if occs <> AllOccurrences then error_occurrences (); + if not (is_all_occurrences occs) then error_occurrences (); if w = InHypValueOnly then error_body_selection (); Some id) l in if cl.concl_occs = NoOccurrences then hyps else - if cl.concl_occs <> AllOccurrences then error_occurrences () + if not (is_all_occurrences cl.concl_occs) then error_occurrences () else None :: hyps (** From [clause] to [concrete_clause] *) @@ -111,7 +118,7 @@ let clause_with_generic_occurrences cls = List.for_all (function ((AllOccurrences,_),_) -> true | _ -> false) hyps in let concl = match cls.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in hyps && concl @@ -122,6 +129,6 @@ let clause_with_generic_context_selection cls = List.for_all (function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in let concl = match cls.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in hyps && concl diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index a07c018c321a..ac15fe1018cf 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -21,6 +21,8 @@ val convert_occs : occurrences -> bool * int list val is_selected : int -> occurrences -> bool +val is_all_occurrences : 'a occurrences_gen -> bool + (** Usual clauses *) val allHypsAndConcl : 'a clause_expr diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2308a541fbe4..5db571433a20 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1105,6 +1105,7 @@ let unfoldoccs env sigma (occs,name) c = | AllOccurrences -> unfold env sigma name c | OnlyOccurrences l -> unfo true l | AllOccurrencesBut l -> unfo false l + | AtLeastOneOccurrence -> unfo false [] (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ac0b58b92bb1..ce97912b84a8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1649,7 +1649,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> (push_named_context_val d sign,depdecls) - | AllOccurrences, InHyp as occ -> + | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index f82455270544..3b8232d20a46 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -145,7 +145,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = let try_do_hyps treat_id l = autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas in - if cl.concl_occs != AllOccurrences && + if not (Locusops.is_all_occurrences cl.concl_occs) && cl.concl_occs != NoOccurrences then Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.") diff --git a/tactics/equality.ml b/tactics/equality.ml index 769e702da12a..a8cfc87f9cba 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -437,7 +437,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac ((c,l) : constr with_bindings) with_evars = - if occs != AllOccurrences then ( + if not (Locusops.is_all_occurrences occs) then ( rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac) else Proofview.Goal.enter begin fun gl -> @@ -595,15 +595,16 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else check_required_library ["Coq";"Setoids";"Setoid"] -let check_setoid cl = +let check_setoid cl = + let concloccs = Locusops.occurrences_map (fun x -> x) cl.concl_occs in Option.fold_left - ( List.fold_left + (List.fold_left (fun b ((occ,_),_) -> - b||(Locusops.occurrences_map (fun x -> x) occ <> AllOccurrences) + b||(not (Locusops.is_all_occurrences (Locusops.occurrences_map (fun x -> x) occ))) ) ) - ((Locusops.occurrences_map (fun x -> x) cl.concl_occs <> AllOccurrences) && - (Locusops.occurrences_map (fun x -> x) cl.concl_occs <> NoOccurrences)) + (not (Locusops.is_all_occurrences concloccs) && + (concloccs <> NoOccurrences)) cl.onhyps let replace_core clause l2r eq = @@ -1724,7 +1725,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = tclTHENLIST ((if need_rewrite then [revert (List.map snd dephyps); - general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); + general_rewrite dir AtLeastOneOccurrence true dep_proof_ok (mkVar hyp); (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)] else [Proofview.tclUNIT ()]) @ diff --git a/tactics/ppred.ml b/tactics/ppred.ml index dd1bcd469952..d832dc279c51 100644 --- a/tactics/ppred.ml +++ b/tactics/ppred.ml @@ -6,6 +6,7 @@ open Pputils let pr_with_occurrences pr keyword (occs,c) = match occs with + | AtLeastOneOccurrence -> hov 1 (pr c ++ spc () ++ keyword "at" ++ str" +") | AllOccurrences -> pr c | NoOccurrences ->