repeat_tac

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index fe7f176a0e5a3a8ed3a44e0d4c7e9a0228868da4..e044cd3bf2d194a467036480d6fe0525904c2515 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -13,7 +13,7 @@
 
 open Printf
 
-let debug = true
+let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 open Continuationals.Stack
@@ -22,7 +22,7 @@ module Ast = CicNotationPt
 
 let id_tac status = status ;;
 let print_tac print_status message status = 
-  if print_status then pp_tac_status status;
+  if print_status then pp_status status;
   prerr_endline message; 
   status
 ;;
@@ -179,17 +179,16 @@ let compare_statuses ~past ~present =
    (e.g. the tactic could perform a global analysis of the set of goals)
 *)
 
-let exec tac low_status g =
+let exec tac (low_status : #lowtac_status) g =
   let stack = [ [0,Open g], [], [], `NoTag ] in
   let status =
-   (new NTacStatus.status low_status#obj stack)#set_estatus
-    (low_status :> NEstatus.status)
+   (new NTacStatus.status low_status#obj stack)#set_estatus low_status
   in
   let status = tac status in
-   (low_status#set_estatus (status :> NEstatus.status))#set_obj status#obj
+   (low_status#set_estatus status)#set_obj status#obj
 ;;
 
-let distribute_tac tac status =
+let distribute_tac tac (status : #tac_status) =
   match status#stack with
   | [] -> assert false
   | (g, t, k, tag) :: s ->
@@ -226,7 +225,7 @@ let distribute_tac tac status =
       let stack =
         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
       in
-       ((status#set_stack stack)#set_obj (sn :> lowtac_status)#obj)#set_estatus (sn :> NEstatus.status)
+       ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
 ;;
 
 let atomic_tac htac = distribute_tac (exec htac) ;;
@@ -244,11 +243,11 @@ let first_tac tacl status =
     (fun tac _ -> try Some (tac status) with NTacStatus.Error _ -> None) tacl
   in
     match res with
-      | None -> raise (NTacStatus.Error (lazy("No tactic left")))
+      | None -> fail (lazy "No tactics left")
       | Some x -> x
 ;;
 
-let exact_tac t = distribute_tac (fun status goal ->
+let exact_tac t : 's tactic = distribute_tac (fun status goal ->
  let goalty = get_goalty status goal in
  let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
  instantiate status goal t)
@@ -602,13 +601,20 @@ let auto ~params:(l,_) status goal =
         (status, (t,ty) :: l))
       (status,[]) l
   in
-  let pt, metasenv, subst = 
-    Paramod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
-  in      
-  let status = status#set_obj (n,h,metasenv,subst,o) in
-  instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
+  match
+    NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
+  with
+  | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
+  | (pt, metasenv, subst)::_ -> 
+      let status = status#set_obj (n,h,metasenv,subst,o) in
+      instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
 ;;
 
 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
+;;