new tactic whd implemented

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index b69ff18f44592d8c21092f697e1900c2ab14342e..763911b79ea245ae572da11306a1008d5d5d7695 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -55,10 +55,11 @@ type ntactic =
    | NCase1 of loc * string
    | NChange of loc * npattern * CicNotationPt.term
    | NElim of loc * CicNotationPt.term * npattern  
+   | NEval of loc * npattern * [ `Whd of bool ]
+   | NGeneralize of loc * npattern
    | NId of loc
    | NIntro of loc * string
    | NRewrite of loc * direction * CicNotationPt.term * npattern
-   | NGeneralize of loc * npattern
 
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   (* Higher order tactics (i.e. tacticals) *)

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 7be93328e0b1221ab788da4f74b2dd4454d58f51..2099bf06a8ed10987547cc8b7afa4ddddcc49cd3 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -598,6 +598,8 @@ let eval_ng_tac (text, prefix_len, tac) =
       NTactics.elim_tac 
         ~what:(text,prefix_len,what)
         ~where:(text,prefix_len,where)
+  | GrafiteAst.NEval (_loc, where, reduction) ->
+      NTactics.eval_tac ~reduction ~where:(text,prefix_len,where)
   | GrafiteAst.NGeneralize (_loc, where) -> 
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 5fc3a7fad5148d03c5aee0328d9b3fd98ddbd234..dacdc28bdb936f9035d6fc27f5633f0530c38134 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -192,6 +192,10 @@ EXTEND
         GrafiteAst.NGeneralize (loc, p)
     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
         GrafiteAst.NRewrite (loc, dir, what, where)
+    | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
+      where = pattern_spec ->
+        let delta = match delta with None -> true | _ -> false in
+        GrafiteAst.NEval (loc, where, `Whd delta)
     | 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 a6828df113d2afa33623a74306b3c5a7297d6596..a6ae87be720456623a3aaf9da1adaaea7a7dbb9f 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -342,6 +342,17 @@ let generalize_tac ~where =
    ) s) ]
 ;;
 
+let eval_tac ~reduction ~where =
+  let change status t = 
+    match reduction with
+    | `Whd perform_delta -> 
+         whd status
+           ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
+  in
+  let where = GrafiteDisambiguate.disambiguate_npattern where in
+  select0_tac ~where ~job:(`ChangeWith change)
+;;
+
 let change_tac ~where ~with_what =
   let change status t = 
     let status, ww = disambiguate status with_what  None (ctx_of t) in

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index cc79e05b9486408a6071f45ea0c1cf7738ddebfc..9eeebfe7fb2460739ed3c67f199f0e099d6a0b9b 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -41,3 +41,6 @@ val rewrite_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
     NTacStatus.tactic
 val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic
+val eval_tac: 
+      reduction:[ `Whd of bool ] ->
+      where:NTacStatus.tactic_pattern -> NTacStatus.tactic