- nrewrite ((very?) rough implementation)

  PATTERNS DO NOT WORK (why?)

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 512f5ede40c8643b21415f1ee3ceeaeb4bde1786..a83023140b3eb3d65fa1cd8652cfdab54848bc89 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -57,6 +57,7 @@ type ntactic =
    | NElim of loc * CicNotationPt.term * npattern  
    | NId of loc
    | NIntro of loc * string
+   | NRewrite of loc * direction * CicNotationPt.term * npattern
 
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   (* Higher order tactics (i.e. tacticals) *)

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 22e4cbe09e19348aab695521a9947693bcfdaf4a..95600c1828eb635e3b3233b8315b0031416b3d75 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -100,6 +100,7 @@ let pp_ntactic ~map_unicode_to_tex = function
       assert false ^ " " ^ assert false
   | NId _ -> "nid"
   | NIntro (_,n) -> "#" ^ n
+  | NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index af8b086bfb58a256999d28a49fbe34cc72990f44..a41415fe7bbcbcacb1ec001c3e50e9877e4f1d36 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -600,6 +600,9 @@ let eval_ng_tac (text, prefix_len, tac) =
         ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NRewrite (_loc,dir,what,where) ->
+     NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
+      ~where:(text,prefix_len,where)
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 8f37c918e83e8834446ddc667cb835dfc95bb04f..2316c04cad0bb9934d47514e917bf0b5ed643a12 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -188,6 +188,8 @@ EXTEND
         GrafiteAst.NChange (loc, what, with_what)
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         GrafiteAst.NElim (loc, what, where)
+    | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
+        GrafiteAst.NRewrite (loc, dir, what, where)
     | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
     | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
     | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index f967a2ac47a2fc82d0850887df32ff82bfb4e0ef..d54f97145a021a2ce493fe4b977e033d088933ab 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -371,6 +371,18 @@ let elim_tac ~what ~where status =
    status
 ;;
 
+let rewrite_tac ~dir ~what:(_,_,what) ~where =
+ let name =
+  match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"
+ in
+  block_tac
+   [ select_tac ~where true;
+     exact_tac
+      ("",0,
+       Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
+        [what]))]
+;;
+
 let intro_tac name =
  block_tac
   [ exact_tac

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index a834c4e52a8439ac1fea0eda294ad9435c8c5fa2..0b805d22bdbc40f7e1b43bcdb58909835843e3da 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -36,4 +36,7 @@ val cases_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      NTacStatus.tactic
 val case1_tac: string -> NTacStatus.tactic
-
+val rewrite_tac:
+  dir:[ `LeftToRight | `RightToLeft ] ->
+   what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
+    NTacStatus.tactic