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

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 9817474cddbb50cadea0f5b143d333bb65fdc3ce..c0bfdb933aee59858b261f4d6f4d5884f55f9db2 100644 (file)
--- 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 =
@@ -705,7 +712,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj_kind =
          NCicUntrusted.map_obj_kind 
           (NCicUntrusted.apply_subst subst []) obj_kind in
-        let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
+        let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
         (* fix the height inside the object *)
         let rec fix () = function 
           | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri ->