From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Jul 2009 14:25:44 +0000 (+0000)
Subject: new nrepeat (and block '('...')' ) tactical
X-Git-Tag: make_still_working~3711
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4dc87cc7384ba61136bc82a23effe6a52160e720;p=helm.git

new nrepeat (and block '('...')' ) tactical
---

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
-;;