From 0d62e3344d7f69c0296c347c7aeddabd09bbab60 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 1 Mar 2008 01:59:59 +0000 Subject: Rework on rich forms of rewrite 1) changed the semantics of rewrite H,H' : the earlier semantics (rewrite H,H' == rewrite H; rewrite H') was poorly suited for situations where first rewrite H generates side-conditions. New semantics is tclTHENFIRST instead of tclTHEN, that is side-conditions are left untouched. Note to myself: check if side-effect-come-first bug of setoid rewrite is still alive, and do something if yes 2) new syntax for rewriting something many times. This syntax is shamelessly taken from ssreflect: rewrite ?H means "H as many times as possible" (i.e. almost repeat rewrite H, except that possible side-conditions are left apart as in 1) rewrite !H means "at least once" (i.e. rewrite H; repeat rewrite H) rewrite 3?H means "up to 3 times", maybe less (i.e. something like: do 3 (try rewrite H)). rewrite 3!H means "exactly 3 times" (i.e. almost do 3 rewrite H). For instance: rewrite 3?foo, <-2!bar in H1,H2|-* 3) By the way, for a try, I've enabled the syntax +/- as synonyms for ->/<- in the orientation of rewrite. Comments welcome ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10612 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_tactic.ml4 | 28 +++++++++++++++++++++++----- parsing/pptactic.ml | 10 +++++++++- 2 files changed, 32 insertions(+), 6 deletions(-) (limited to 'parsing') diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index f305ebd69..724bb2da1 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -288,8 +288,10 @@ GEXTEND Gram orient: [ [ "->" -> true | "<-" -> false + | "+" -> true + | "-" -> false | -> true ]] - ; + ; fixdecl: [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot; ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] @@ -319,9 +321,25 @@ GEXTEND Gram ; rename : [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] - ; + ; rewriter : - [ [ b = orient; c = constr_with_bindings -> (b,c) ] ] + [ [ c = constr_with_bindings -> (Precisely 1, c) + | "!"; c = constr_with_bindings -> (RepeatPlus,c) + | "?"; c = constr_with_bindings -> (RepeatStar,c) + | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c) + | n = natural; "?"; c = constr_with_bindings -> (UpTo n,c) + (* hack for allowing "rewrite ?t" and "rewrite NN?t" that normally + produce a pattern_ident *) + | c = pattern_ident -> + let c = (CRef (Libnames.Ident (dummy_loc,c)), NoBindings) in + (RepeatStar, c) + | n = natural; c = pattern_ident -> + let c = (CRef (Libnames.Ident (dummy_loc,c)), NoBindings) in + (UpTo n, c) + ] ] + ; + oriented_rewriter : + [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] ; simple_tactic: [ [ @@ -451,9 +469,9 @@ GEXTEND Gram | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) - | IDENT "rewrite"; l = LIST1 rewriter SEP ","; cl = clause -> + | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause -> TacRewrite (false,l,cl) - | IDENT "erewrite"; l = LIST1 rewriter SEP ","; cl = clause -> + | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause -> TacRewrite (true,l,cl) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 67858b3c6..da915a5cc 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -428,6 +428,13 @@ let pr_clause_pattern pr_id = function let pr_orient b = if b then mt () else str " <-" +let pr_multi = function + | Precisely 1 -> mt () + | Precisely n -> pr_int n ++ str "!" + | UpTo n -> pr_int n ++ str "?" + | RepeatStar -> str "?" + | RepeatPlus -> str "!" + let pr_induction_arg prlc prc = function | ElimOnConstr c -> pr_with_bindings prlc prc c | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) @@ -818,7 +825,8 @@ and pr_atom1 = function hov 1 (str (if ev then "erewrite" else "rewrite") ++ prlist_with_sep (fun () -> str ","++spc()) - (fun (b,c) -> pr_orient b ++ spc() ++ pr_with_bindings c) + (fun (b,m,c) -> + pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c) l ++ pr_clauses pr_ident cl) | TacInversion (DepInversion (k,c,ids),hyp) -> -- cgit v1.2.3