From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 7 Apr 2009 22:23:31 +0000 (+0000)
Subject: - nrewrite ((very?) rough implementation)
X-Git-Tag: make_still_working~4107
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d58b48162ad53fb369d285e60a99f746a497ad89;p=helm.git

- 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 512f5ede4..a83023140 100644
--- 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 22e4cbe09..95600c182 100644
--- 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 af8b086bf..a41415fe7 100644
--- 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 8f37c918e..2316c04ca 100644
--- 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 f967a2ac4..d54f97145 100644
--- 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 a834c4e52..0b805d22b 100644
--- 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