From 1ea4a8d26516af14670cc677a5a0fce04b90caf7 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 12 Apr 2008 16:01:36 +0000 Subject: Adding 'at' to rewrite, as it is already implemented in setoid_rewrite. Uses setoid_rewrite even if rewriting with leibniz if there are specified occurences, maybe a combination of pattern and rewrite could be done instead. Correct spelling of occurrences. Coq does not compile with this patch, the next one will make it compile again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10781 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/autorewrite.ml | 4 +- tactics/equality.ml | 96 ++++++++++++++++++++++++---------------------- tactics/equality.mli | 10 ++--- tactics/extraargs.ml4 | 6 +-- tactics/extraargs.mli | 6 +-- tactics/setoid_replace.ml | 10 ++--- tactics/setoid_replace.mli | 6 +-- 7 files changed, 72 insertions(+), 66 deletions(-) (limited to 'tactics') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e2ce6baeb..5402e6120 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -80,7 +80,7 @@ let one_base general_rewrite_maybe_in tac_main bas = let autorewrite tac_main lbas = tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac bas -> - tclTHEN tac (one_base general_rewrite tac_main bas)) tclIDTAC lbas)) + tclTHEN tac (one_base (fun dir -> general_rewrite dir []) tac_main bas)) tclIDTAC lbas)) let autorewrite_multi_in idl tac_main lbas : tactic = fun gl -> @@ -96,7 +96,7 @@ let autorewrite_multi_in idl tac_main lbas : tactic = | _ -> (* even the hypothesis id is missing *) error ("No such hypothesis : " ^ (string_of_id !id)) in - let gl' = general_rewrite_in dir !id cstr false gl in + let gl' = general_rewrite_in dir [] !id cstr false gl in let gls = (fst gl').Evd.it in match gls with g::_ -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 60acd9092..f91845a5c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -84,14 +84,14 @@ let general_s_rewrite_clause = function let general_setoid_rewrite_clause = ref general_s_rewrite_clause let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause -let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl = +let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl = let ctype = pf_apply get_type_of gl c in (* A delta-reduction would be here too strong, since it would break search for a defined setoid relation in head position. *) let t = snd (decompose_prod (whd_betaiotazeta ctype)) in let head = if isApp t then fst (destApp t) else t in if relation_table_mem head && l = NoBindings then - !general_setoid_rewrite_clause cls lft2rgt c [] gl + !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl else (* Original code. In particular, [splay_prod] performs delta-reduction. *) let env = pf_env gl in @@ -100,45 +100,51 @@ let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl = match match_with_equation t with | None -> if l = NoBindings - then !general_setoid_rewrite_clause cls lft2rgt c [] gl + then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl else error "The term provided does not end with an equation" | Some (hdcncl,_) -> - let hdcncls = string_of_inductive hdcncl in - let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in - let dir = if cls=None then lft2rgt else not lft2rgt in - let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in - let elim = - try pf_global gl (id_of_string rwr_thm) - with Not_found -> - error ("Cannot find rewrite principle "^rwr_thm) - in - try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl - with e -> - let eq = build_coq_eq () in - if not (eq_constr eq head) then - try !general_setoid_rewrite_clause cls lft2rgt c [] gl - with _ -> raise e - else raise e - + if occs <> [] then ( + !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl) + else + let hdcncls = string_of_inductive hdcncl in + let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in + let dir = if cls=None then lft2rgt else not lft2rgt in + let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in + let elim = + try pf_global gl (id_of_string rwr_thm) + with Not_found -> + error ("Cannot find rewrite principle "^rwr_thm) + in + try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl + with e -> + let eq = build_coq_eq () in + if not (eq_constr eq head) then + try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl + with _ -> raise e + else raise e + let general_rewrite_ebindings = general_rewrite_ebindings_clause None -let general_rewrite_bindings l2r (c,bl) = - general_rewrite_ebindings_clause None l2r (c,inj_ebindings bl) +let general_rewrite_bindings l2r occs (c,bl) = + general_rewrite_ebindings_clause None l2r occs (c,inj_ebindings bl) -let general_rewrite l2r c = - general_rewrite_bindings l2r (c,NoBindings) false +let general_rewrite l2r occs c = + general_rewrite_bindings l2r occs (c,NoBindings) false -let general_rewrite_ebindings_in l2r id = - general_rewrite_ebindings_clause (Some id) l2r -let general_rewrite_bindings_in l2r id (c,bl) = - general_rewrite_ebindings_clause (Some id) l2r (c,inj_ebindings bl) -let general_rewrite_in l2r id c = - general_rewrite_ebindings_clause (Some id) l2r (c,NoBindings) +let general_rewrite_ebindings_in l2r occs id = + general_rewrite_ebindings_clause (Some id) l2r occs +let general_rewrite_bindings_in l2r occs id (c,bl) = + general_rewrite_ebindings_clause (Some id) l2r occs (c,inj_ebindings bl) +let general_rewrite_in l2r occs id c = + general_rewrite_ebindings_clause (Some id) l2r occs (c,NoBindings) let general_multi_rewrite l2r with_evars c cl = - if cl.concl_occs <> [] then - error "The \"at\" syntax isn't available yet for the rewrite/replace tactic" - else match cl.onhyps with + let occs = List.fold_left + (fun acc -> + function ArgArg x -> x :: acc | ArgVar _ -> acc) + [] cl.concl_occs + in + match cl.onhyps with | Some l -> (* If a precise list of locations is given, success is mandatory for each of these locations. *) @@ -146,12 +152,12 @@ let general_multi_rewrite l2r with_evars c cl = | [] -> tclIDTAC | ((_,id),_) :: l -> tclTHENFIRST - (general_rewrite_ebindings_in l2r id c with_evars) + (general_rewrite_ebindings_in l2r occs id c with_evars) (do_hyps l) in if not cl.onconcl then do_hyps l else tclTHENFIRST - (general_rewrite_ebindings l2r c with_evars) + (general_rewrite_ebindings l2r occs c with_evars) (do_hyps l) | None -> (* Otherwise, if we are told to rewrite in all hypothesis via the @@ -160,7 +166,7 @@ let general_multi_rewrite l2r with_evars c cl = | [] -> (fun gl -> error "Nothing to rewrite.") | id :: l -> tclIFTHENTRYELSEMUST - (general_rewrite_ebindings_in l2r id c with_evars) + (general_rewrite_ebindings_in l2r occs id c with_evars) (do_hyps_atleastonce l) in let do_hyps gl = @@ -172,7 +178,7 @@ let general_multi_rewrite l2r with_evars c cl = in if not cl.onconcl then do_hyps else tclIFTHENTRYELSEMUST - (general_rewrite_ebindings l2r c with_evars) + (general_rewrite_ebindings l2r occs c with_evars) do_hyps let general_multi_multi_rewrite with_evars l cl tac = @@ -200,20 +206,20 @@ let general_multi_multi_rewrite with_evars l cl tac = to the resolution of the conditions by a given tactic *) let conditional_rewrite lft2rgt tac (c,bl) = - tclTHENSFIRSTn (general_rewrite_ebindings lft2rgt (c,bl) false) + tclTHENSFIRSTn (general_rewrite_ebindings lft2rgt [] (c,bl) false) [|tclIDTAC|] (tclCOMPLETE tac) -let rewriteLR_bindings = general_rewrite_bindings true -let rewriteRL_bindings = general_rewrite_bindings false +let rewriteLR_bindings = general_rewrite_bindings true [] +let rewriteRL_bindings = general_rewrite_bindings false [] -let rewriteLR = general_rewrite true -let rewriteRL = general_rewrite false +let rewriteLR = general_rewrite true [] +let rewriteRL = general_rewrite false [] -let rewriteLRin_bindings = general_rewrite_bindings_in true -let rewriteRLin_bindings = general_rewrite_bindings_in false +let rewriteLRin_bindings = general_rewrite_bindings_in true [] +let rewriteRLin_bindings = general_rewrite_bindings_in false [] let conditional_rewrite_in lft2rgt id tac (c,bl) = - tclTHENSFIRSTn (general_rewrite_ebindings_in lft2rgt id (c,bl) false) + tclTHENSFIRSTn (general_rewrite_ebindings_in lft2rgt [] id (c,bl) false) [|tclIDTAC|] (tclCOMPLETE tac) let rewriteRL_clause = function diff --git a/tactics/equality.mli b/tactics/equality.mli index 91a0d33c6..19cf1ed56 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -26,9 +26,9 @@ open Genarg (*i*) val general_rewrite_bindings : - bool -> constr with_bindings -> evars_flag -> tactic + bool -> int list -> constr with_bindings -> evars_flag -> tactic val general_rewrite : - bool -> constr -> tactic + bool -> int list -> constr -> tactic (* Obsolete, use [general_rewrite_bindings l2r] [val rewriteLR_bindings : constr with_bindings -> tactic] @@ -43,12 +43,12 @@ val rewriteRL : constr -> tactic val register_general_setoid_rewrite_clause : (identifier option -> - bool -> constr -> new_goals:constr list -> tactic) -> unit + bool -> int list -> constr -> new_goals:constr list -> tactic) -> unit val general_rewrite_bindings_in : - bool -> identifier -> constr with_bindings -> evars_flag -> tactic + bool -> int list -> identifier -> constr with_bindings -> evars_flag -> tactic val general_rewrite_in : - bool -> identifier -> constr -> evars_flag -> tactic + bool -> int list -> identifier -> constr -> evars_flag -> tactic val general_multi_rewrite : bool -> evars_flag -> constr with_ebindings -> clause -> tactic diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 1d9d5e0e9..3124e10a0 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -33,14 +33,14 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient | [ ] -> [ true ] END -let pr_occurences _prc _prlc _prt l = +let pr_occurrences _prc _prlc _prt l = let rec aux = function | i :: l -> Pp.int i ++ Pp.spc () ++ aux l | [] -> Pp.mt() in aux l -ARGUMENT EXTEND occurences TYPED AS int list PRINTED BY pr_occurences -| [ integer(i) occurences(l) ] -> [ i :: l ] +ARGUMENT EXTEND occurrences TYPED AS int list PRINTED BY pr_occurrences +| [ integer(i) occurrences(l) ] -> [ i :: l ] | [ ] -> [ [] ] END diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index ead64ac3b..f5813e40b 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -19,9 +19,9 @@ val rawwit_orient : bool raw_abstract_argument_type val wit_orient : bool typed_abstract_argument_type val orient : bool Pcoq.Gram.Entry.e -val rawwit_occurences : (int list) raw_abstract_argument_type -val wit_occurences : (int list) typed_abstract_argument_type -val occurences : (int list) Pcoq.Gram.Entry.e +val rawwit_occurrences : (int list) raw_abstract_argument_type +val wit_occurrences : (int list) typed_abstract_argument_type +val occurrences : (int list) Pcoq.Gram.Entry.e val rawwit_morphism_signature : Setoid_replace.morphism_signature raw_abstract_argument_type diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 1b3f4d21b..9f8821341 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1806,7 +1806,7 @@ let relation_rewrite_no_unif c1 c2 hyp ~new_goals sigma gl = if_output_relation_is_if gl with Optimize -> - !general_rewrite (fst hyp = Left2Right) (snd hyp) gl + !general_rewrite (fst hyp = Left2Right) [] (snd hyp) gl let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl = let (sigma,cl,c1,c2) = unification_rewrite c1 c2 cl (pf_concl gl) gl in @@ -1824,7 +1824,7 @@ let analyse_hypothesis gl c = let others,(c1,c2) = split_last_two args in eqclause,mkApp (equiv, Array.of_list others),c1,c2 -let general_s_rewrite lft2rgt c ~new_goals gl = +let general_s_rewrite lft2rgt occs c ~new_goals gl = let eqclause,_,c1,c2 = analyse_hypothesis gl c in if lft2rgt then relation_rewrite c1 c2 (Left2Right,eqclause) ~new_goals gl @@ -1861,7 +1861,7 @@ let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl = (relation_rewrite_no_unif c2 c1 (oppdir,cl) ~new_goals sigma)))) gl -let general_s_rewrite_in id lft2rgt c ~new_goals gl = +let general_s_rewrite_in id lft2rgt occs c ~new_goals gl = let eqclause,_,c1,c2 = analyse_hypothesis gl c in if lft2rgt then relation_rewrite_in id c1 c2 (Left2Right,eqclause) ~new_goals gl @@ -1916,7 +1916,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_ tclTHENS (assert_tac false Anonymous eq) [onLastHyp (fun id -> tclTHEN - (rewrite_tac dir (mkVar id) ~new_goals) + (rewrite_tac dir [] (mkVar id) ~new_goals) (clear [id])); try_prove_eq_tac] in @@ -1928,7 +1928,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_ tclTHENS (assert_tac false Anonymous eq) [onLastHyp (fun id -> tclTHEN - (rewrite_tac false (mkVar id) ~new_goals) + (rewrite_tac false [] (mkVar id) ~new_goals) (clear [id])); try_prove_eq_tac] gl diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 2dd153b3f..1eb0141c6 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -40,7 +40,7 @@ type morphism_signature = (bool option * constr_expr) list * constr_expr val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds val register_replace : (tactic option -> constr -> constr -> tactic) -> unit -val register_general_rewrite : (bool -> constr -> tactic) -> unit +val register_general_rewrite : (bool -> int list -> constr -> tactic) -> unit val print_setoids : unit -> unit @@ -58,9 +58,9 @@ val setoid_replace_in : identifier -> constr option -> constr -> constr -> new_goals:constr list -> tactic -val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic +val general_s_rewrite : bool -> int list -> constr -> new_goals:constr list -> tactic val general_s_rewrite_in : - identifier -> bool -> constr -> new_goals:constr list -> tactic + identifier -> bool -> int list -> constr -> new_goals:constr list -> tactic val setoid_reflexivity : tactic val setoid_symmetry : tactic -- cgit v1.2.3