From b2a9b21233b1b7c645175e26fc3f3ab03a308c08 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Apr 2009 15:25:37 +0000 Subject: [PATCH] new tactic whd implemented --- helm/software/components/grafite/grafiteAst.ml | 3 ++- .../components/grafite_engine/grafiteEngine.ml | 2 ++ .../components/grafite_parser/grafiteParser.ml | 4 ++++ helm/software/components/ng_tactics/nTactics.ml | 11 +++++++++++ helm/software/components/ng_tactics/nTactics.mli | 3 +++ 5 files changed, 22 insertions(+), 1 deletion(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index b69ff18f4..763911b79 100644 --- 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 7be93328e..2099bf06a 100644 --- 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 5fc3a7fad..dacdc28bd 100644 --- 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 a6828df11..a6ae87be7 100644 --- 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 cc79e05b9..9eeebfe7f 100644 --- 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 -- 2.39.2