From 4dc87cc7384ba61136bc82a23effe6a52160e720 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Jul 2009 14:25:44 +0000 Subject: [PATCH] new nrepeat (and block '('...')' ) tactical --- helm/software/components/grafite/grafiteAst.ml | 2 ++ helm/software/components/grafite/grafiteAstPp.ml | 5 ++++- .../components/grafite_engine/grafiteEngine.ml | 11 +++++++++-- .../components/grafite_parser/grafiteParser.ml | 4 +++- helm/software/components/ng_tactics/nTactics.ml | 16 +++++++++++----- 5 files changed, 29 insertions(+), 9 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index e807c6f48..14c487702 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -75,6 +75,8 @@ type ntactic = | NUnfocus of loc | NTry of loc * ntactic | NAssumption of loc + | NRepeat of loc * ntactic + | NBlock of loc * ntactic list 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 f05cb9595..8fbe6b8d1 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -119,8 +119,11 @@ let rec pp_ntactic ~map_unicode_to_tex = function (String.concat " " (List.map string_of_int l)) | NUnfocus _ -> "##unfocus" | NSkip _ -> "##skip" - | NTry (_,tac) -> "ntry (" ^ pp_ntactic ~map_unicode_to_tex tac ^ ")" + | NTry (_,tac) -> "ntry " ^ pp_ntactic ~map_unicode_to_tex tac | NAssumption _ -> "nassumption" + | NBlock (_,l) -> + "(" ^ String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) l)^ ")" + | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic ~map_unicode_to_tex t ;; 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 eb994854f..c0bfdb933 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -625,7 +625,8 @@ let eval_ng_punct (_text, _prefix_len, punct) = | GrafiteAst.Merge _ -> NTactics.merge_tac ;; -let rec eval_ng_tac (text, prefix_len, tac) = +let eval_ng_tac tac = + let rec aux f (text, prefix_len, tac) = match tac with | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) | GrafiteAst.NAssert (_loc, seqs) -> @@ -677,8 +678,14 @@ let rec eval_ng_tac (text, prefix_len, tac) = | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac | GrafiteAst.NTry (_,tac) -> NTactics.try_tac - (eval_ng_tac (text, prefix_len, tac)) + (aux f (text, prefix_len, tac)) | GrafiteAst.NAssumption _ -> NTactics.assumption_tac + | GrafiteAst.NBlock (_,l) -> + NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l) + |GrafiteAst.NRepeat (_,tac) -> + NTactics.repeat_tac (f f (text, prefix_len, tac)) + in + aux aux tac (* trick for non uniform recursion call *) ;; let subst_metasenv_and_fix_names status = diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index cc2bf2cda..d031bbad3 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -264,7 +264,9 @@ EXTEND G.NReduce (loc, kind, p) | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec -> G.NRewrite (loc, dir, what, where) - | IDENT "ntry"; LPAREN ; tac = SELF ; RPAREN -> G.NTry (loc,tac) + | IDENT "ntry"; tac = SELF -> G.NTry (loc,tac) + | IDENT "nrepeat"; tac = SELF -> G.NRepeat (loc,tac) + | LPAREN; l = LIST1 SELF; RPAREN -> G.NBlock (loc,l) | IDENT "nassumption" -> G.NAssumption loc | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n) | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_") diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index e044cd3bf..596a74e2e 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -157,6 +157,7 @@ let block_tac l status = List.fold_left (fun status tac -> tac status) status l ;; + let compare_statuses ~past ~present = let _,_,past,_,_ = past#obj in let _,_,present,_,_ = present#obj in @@ -228,7 +229,16 @@ let distribute_tac tac (status : #tac_status) = ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn ;; -let atomic_tac htac = distribute_tac (exec htac) ;; +let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;; + +let repeat_tac t s = + let rec repeat t (status : #tac_status as 'a) : 'a = + try repeat t (t status) + with NTacStatus.Error _ -> status + in + atomic_tac (repeat t) s +;; + let try_tac tac status = try @@ -614,7 +624,3 @@ let auto_tac ~params status = distribute_tac (auto ~params) status ;; -let rec repeat_tac t status = - try repeat_tac t (atomic_tac t status) - with NTacStatus.Error _ -> status -;; -- 2.39.2