From 8602460eb7ac815a9f86231b58798083d2a438d7 Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 8 Sep 2009 14:49:21 +0000 Subject: Fix the bug-ridden code used to choose leibniz or generalized rewriting (thanks to Georges Gonthier for pointing it out). We try to find a declared rewrite relation when the equation does not look like an equality and otherwise try to reduce it to find a leibniz equality but don't backtrack on generalized rewriting if this fails. This new behavior make two fsets scripts fail as they are trying to use an underlying leibniz equality for a declared rewrite relation, a [red] fixes it. Do some renaming from "setoid" to "rewrite". Fix [is_applied_rewrite_relation]'s bad handling of evars and the environment. Fix some [dual] hints in RelationClasses.v and assert that any declared [Equivalence] can be considered a [RewriteRelation]. Fix minor tex output problem in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12310 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/equality.ml | 51 ++++++++++++++++++++++++--------------------------- 1 file changed, 24 insertions(+), 27 deletions(-) (limited to 'tactics/equality.ml') diff --git a/tactics/equality.ml b/tactics/equality.ml index 699f33441..076f05f24 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -155,17 +155,17 @@ let general_elim_clause with_evars tac cls sigma c t l l2r elim gl = else tclMAP try_clause cs gl (* The next function decides in particular whether to try a regular - rewrite or a setoid rewrite. + rewrite or a generalized rewrite. Approach is to break everything, if [eq] appears in head position - then regular rewrite else try setoid rewrite. - If occurrences are set, use setoid_rewrite. + then regular rewrite else try general rewrite. + If occurrences are set, use general rewrite. *) -let general_setoid_rewrite_clause = ref (fun _ -> assert false) -let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause +let general_rewrite_clause = ref (fun _ -> assert false) +let register_general_rewrite_clause = (:=) general_rewrite_clause -let is_applied_setoid_relation = ref (fun _ -> false) -let register_is_applied_setoid_relation = (:=) is_applied_setoid_relation +let is_applied_rewrite_relation = ref (fun _ _ _ _ -> None) +let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) @@ -190,12 +190,12 @@ let adjust_rewriting_direction args lft2rgt = (* other equality *) lft2rgt -let setoid_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) +let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) let general_rewrite_ebindings_clause cls lft2rgt occs ?tac ((c,l) : open_constr with_bindings) with_evars gl = if occs <> all_occurrences then ( - setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl) + rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl) else let env = pf_env gl in let sigma, c' = c in @@ -208,24 +208,21 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ?tac leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' (it_mkProd_or_LetIn t rels) l with_evars gl hdcncl | None -> - let env' = push_rel_context rels env in - let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) - match match_with_equality_type t' with - | Some (hdcncl,args) -> (* Maybe a setoid relation with eq inside *) - let lft2rgt = adjust_rewriting_direction args lft2rgt in - if l = NoBindings && !is_applied_setoid_relation t then - setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl - else - (try leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' - (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars gl hdcncl - with e -> - try setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl - with _ -> raise e) - | None -> (* Can't be leibniz, try setoid *) - if l = NoBindings - then setoid_side_tac (!general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[]) tac gl - else error "The term provided does not end with an equation." - + match !is_applied_rewrite_relation env sigma rels t with + | Some _ -> + rewrite_side_tac (!general_rewrite_clause cls + lft2rgt occs (c,l) ~new_goals:[]) tac gl + | None -> + let env' = push_rel_context rels env in + let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) + match match_with_equality_type t' with + | Some (hdcncl,args) -> + let lft2rgt = adjust_rewriting_direction args lft2rgt in + leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' + (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars gl hdcncl + | None -> + error "The provided term does not end with an equality or a declared rewrite relation." + let general_rewrite_ebindings = general_rewrite_ebindings_clause None -- cgit v1.2.3