X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftacticals.ml;h=d48b6a02c28dc5e2ca60876aeaa26a93f288c351;hb=b6c2107995066dea2b31fe9f760af3cac2d8cebc;hp=f3cd13b44c8f9544d766d027ef837242a977fbc9;hpb=71922d0022ee8f9e507f601dc93a2f68c2080d85;p=helm.git

diff --git a/helm/gTopLevel/tacticals.ml b/helm/gTopLevel/tacticals.ml
index f3cd13b44..d48b6a02c 100644
--- a/helm/gTopLevel/tacticals.ml
+++ b/helm/gTopLevel/tacticals.ml
@@ -24,7 +24,6 @@
  *)
 
 open CicReduction
-open PrimitiveTactics
 open ProofEngineTypes
 open UriManager
 
@@ -38,22 +37,32 @@ let warn s =
   if debug then
     prerr_endline ("TACTICALS WARNING: " ^ s)
 
-(** AUX TACTIC{,AL}S *)
+
+(** TACTIC{,AL}S *)
+
+  (* not a tactical, but it's used only here (?) *)
+
+let id_tac ~status:(proof,goal) =
+  (proof,[goal])
+
 
   (**
     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
     if one fails pass to the next one and so on, eventually raises (failure "no
     tactics left")
     TODO warning: not tail recursive due to "try .. with" boxing
+
+    Galla: is this exactly Coq's "First"?
+
   *)
 let rec try_tactics ~(tactics: (string * tactic) list) ~status =
-  warn "in Ring.try_tactics";
+  warn "in Tacticals.try_tactics";
   match tactics with
   | (descr, tac)::tactics ->
-      warn ("Ring.try_tactics IS TRYING " ^ descr);
+      warn ("Tacticals.try_tactics IS TRYING " ^ descr);
       (try
         let res = tac ~status in
-        warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!");
+        warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!");
         res
        with
         e ->
@@ -62,13 +71,15 @@ let rec try_tactics ~(tactics: (string * tactic) list) ~status =
           | (CicTypeChecker.NotWellTyped _)
           | (CicUnification.UnificationFailed) ->
               warn (
-                "Ring.try_tactics failed with exn: " ^
+                "Tacticals.try_tactics failed with exn: " ^
                 Printexc.to_string e);
               try_tactics ~tactics ~status
         | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
       )
   | [] -> raise (Fail "try_tactics: no tactics left")
 
+
+
 let thens ~start ~continuations ~status =
  let (proof,new_goals) = start ~status in
   try
@@ -80,6 +91,8 @@ let thens ~start ~continuations ~status =
   with
    Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
 
+
+
 let then_ ~start ~continuation ~status =
  let (proof,new_goals) = start ~status in
   List.fold_left
@@ -87,3 +100,145 @@ let then_ ~start ~continuation ~status =
      let (proof',new_goals') = continuation ~status:(proof,goal) in
       (proof',goals@new_goals')
    ) (proof,[]) new_goals
+
+
+(* Galla *)
+(* si suppone che tutte le tattiche sollevano solamente Fail? *)
+
+(* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
+
+(* This keep on appling tactic until it fails *)
+(* When <tactic> generates more than one goal, you have a tree of
+   application on the tactic, repeat_tactic works in depth on this tree *)
+
+let rec repeat_tactic ~tactic ~status =
+  warn "in repeat_tactic";
+  try let (proof, goallist) = tactic ~status in
+   let rec step proof goallist =
+    match goallist with
+       [] -> (proof, [])
+     | head::tail -> 
+        let (proof', goallist') = repeat_tactic ~tactic ~status:(proof, head) in
+         let (proof'', goallist'') = step proof' tail in
+          proof'', goallist'@goallist''
+   in
+    step proof goallist
+  with 
+   (Fail _) as e ->
+    warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+    id_tac ~status
+;;
+
+
+
+(* This tries to apply tactic n times *)
+
+let rec do_tactic ~n ~tactic ~status =
+  warn "in do_tactic";
+  try 
+   let (proof, goallist) = 
+    if (n>0) then tactic ~status 
+             else id_tac ~status in
+(*             else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *)
+   let rec step proof goallist =
+    match goallist with
+       [] -> (proof, [])
+     | head::tail -> 
+        let (proof', goallist') = do_tactic ~n:(n-1) ~tactic ~status:(proof, head) in
+        let (proof'', goallist'') = step proof' tail in
+         proof'', goallist'@goallist''
+   in
+    step proof goallist
+  with 
+   (Fail _) as e ->
+    warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+    id_tac ~status
+;;
+
+
+
+(* This applies tactic and catches its possible failure *)
+
+let rec try_tactic ~tactic ~status =
+  warn "in Tacticals.try_tactic";
+  try
+   tactic ~status
+  with
+   (Fail _) as e -> 
+    warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
+    id_tac ~status
+;;
+
+
+(* This tries tactics until one of them doesn't _solve_ the goal *)
+(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
+
+let rec solve_tactics ~(tactics: (string * tactic) list) ~status =
+  warn "in Tacticals.solve_tactics";
+  match tactics with
+  | (descr, currenttactic)::moretactics ->
+      warn ("Tacticals.solve_tactics is trying " ^ descr);
+      (try
+        let (proof, goallist) = currenttactic ~status in
+         match goallist with 
+            [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!");
+(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *)
+(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
+                  (proof, goallist)
+          | _ -> warn ("Tacticals.solve_tactics: try the next tactic");
+                 solve_tactics ~tactics:(moretactics) ~status
+       with
+        (Fail _) as e ->
+         warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e);
+         solve_tactics ~tactics ~status
+      )
+  | [] -> raise (Fail "solve_tactics cannot solve the goal");
+          id_tac ~status
+;;
+
+
+
+
+
+
+  (** tattica di prova per debuggare i tatticali *)
+(*
+let thens' ~start ~continuations ~status =
+ let (proof,new_goals) = start ~status in
+  try
+   List.fold_left2
+    (fun (proof,goals) goal tactic ->
+      let (proof',new_goals') = tactic ~status:(proof,goal) in
+       (proof',goals@new_goals')
+    ) (proof,[]) new_goals continuations
+  with
+   Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+
+let prova_tac =
+ let apply_T_tac ~status:((proof,goal) as status) =
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+   let rel =
+    let rec find n =
+     function
+        [] -> assert false
+      | (Some (Cic.Name name,_))::_ when name = "T" -> n
+      | _::tl -> find (n+1) tl
+    in
+     prerr_endline ("eseguo find");
+     find 1 context
+   in
+    prerr_endline ("eseguo apply");    
+    apply_tac ~term:(Cic.Rel rel) ~status
+ in
+(*  do_tactic ~n:2 *)
+  repeat_tactic
+   ~tactic:
+    (then_
+      ~start:(intros_tac ~name:"pippo")
+      ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)]))
+(* id_tac *)
+;;
+*)
+
+