X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=934b88a5ab6b1ebb0fccbdc8564cb8bff0bcd56f;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=3c89150adb96f80b1e1721e433eccce810c0d3e4;hpb=df0606d3bcbc41272fcde2d013bbe0b1aadf98af;p=helm.git

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 3c89150ad..934b88a5a 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -38,34 +38,75 @@ let warn s =
   if debug then
     debug_print ("TACTICALS WARNING: " ^ s)
 
+let id_tac = 
+ let id_tac (proof,goal) = 
+  let _, metasenv, _, _ = proof in
+  let _, _, _ = CicUtil.lookup_meta goal metasenv in
+  (proof,[goal])
+ in 
+  mk_tactic id_tac
 
-(** TACTIC{,AL}S *)
+let fail_tac =
+ let fail_tac (proof,goal) =
+  let _, metasenv, _, _ = proof in
+  let _, _, _ = CicUtil.lookup_meta goal metasenv in
+   raise (Fail "fail tactical")
+ in
+  mk_tactic fail_tac
 
-  (* not a tactical, but it's used only here (?) *)
+module type Status =
+ sig
+   type input_status
+   type output_status
+   type tactic
+   val id_tac : tactic
+   val mk_tactic : (input_status -> output_status) -> tactic
+   val apply_tactic : tactic -> input_status -> output_status
+   val goals : output_status -> ProofEngineTypes.goal list
+   val set_goals: output_status -> ProofEngineTypes.goal list -> output_status
+   val focus : output_status -> ProofEngineTypes.goal -> input_status
+ end
 
-let id_tac = 
- let tac (proof,goal) = (proof,[goal])
- in 
-  mk_tactic tac
+module type T =
+ sig
+  type tactic
+
+  val first: tactics: (string * tactic) list -> tactic
+
+  val thens: start: tactic -> continuations: tactic list -> tactic
+
+  val then_: start: tactic -> continuation: tactic -> tactic
+
+   (** "folding" of then_ *)
+  val seq: tactics: tactic list -> tactic
+
+  val repeat_tactic: tactic: tactic -> tactic
+
+  val do_tactic: n: int -> tactic: tactic -> tactic 
+
+  val try_tactic: tactic: tactic -> tactic 
+
+  val solve_tactics: tactics: (string * tactic) list -> tactic
+ end
+
+module Make (S:Status) : T with type tactic = S.tactic =
+struct
+type tactic = S.tactic
 
   (**
     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 try_tactics ~tactics =
- let rec try_tactics ~(tactics: (string * tactic) list) status =
-  warn "in Tacticals.try_tactics";
+let first ~tactics =
+ let rec first ~(tactics: (string * tactic) list) status =
+  warn "in Tacticals.first";
   match tactics with
   | (descr, tac)::tactics ->
-      warn ("Tacticals.try_tactics IS TRYING " ^ descr);
+      warn ("Tacticals.first IS TRYING " ^ descr);
       (try
-        let res = apply_tactic tac status in
-        warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!");
+        let res = S.apply_tactic tac status in
+        warn ("Tacticals.first: " ^ descr ^ " succedeed!!!");
         res
        with
         e ->
@@ -74,46 +115,57 @@ let try_tactics ~tactics =
           | (CicTypeChecker.TypeCheckerFailure _)
           | (CicUnification.UnificationFailure _) ->
               warn (
-                "Tacticals.try_tactics failed with exn: " ^
+                "Tacticals.first failed with exn: " ^
                 Printexc.to_string e);
-              try_tactics ~tactics status
+              first ~tactics status
         | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
       )
-  | [] -> raise (Fail "try_tactics: no tactics left")
+  | [] -> raise (Fail "first: no tactics left")
  in
-  mk_tactic (try_tactics ~tactics)
+  S.mk_tactic (first ~tactics)
 
 
 let thens ~start ~continuations =
  let thens ~start ~continuations status =
- let (proof,new_goals) = apply_tactic start status in
+ let output_status = S.apply_tactic start status in
+ let new_goals = S.goals output_status in
   try
-   List.fold_left2
-    (fun (proof,goals) goal tactic ->
-      let (proof',new_goals') = apply_tactic tactic (proof,goal) in
-       (proof',goals@new_goals')
-    ) (proof,[]) new_goals continuations
+   let output_status,goals =
+    List.fold_left2
+     (fun (output_status,goals) goal tactic ->
+       let status = S.focus output_status goal in
+       let output_status' = S.apply_tactic tactic status in
+       let new_goals' = S.goals output_status' in
+        (output_status',goals@new_goals')
+     ) (output_status,[]) new_goals continuations
+   in
+    S.set_goals output_status goals
   with
    Invalid_argument _ -> 
-(* FG: more debugging information *)
     let debug = Printf.sprintf "thens: expected %i new goals, found %i"
      (List.length continuations) (List.length new_goals)
     in
     raise (Fail debug)
  in
-  mk_tactic (thens ~start ~continuations )
+  S.mk_tactic (thens ~start ~continuations )
 
 
 let then_ ~start ~continuation =
  let then_ ~start ~continuation status =
- let (proof,new_goals) = apply_tactic start status in
-  List.fold_left
-   (fun (proof,goals) goal ->
-     let (proof',new_goals') = apply_tactic continuation (proof,goal) in
-      (proof',goals@new_goals')
-   ) (proof,[]) new_goals
+ let output_status = S.apply_tactic start status in
+ let new_goals = S.goals output_status in
+  let output_status,goals =
+   List.fold_left
+    (fun (output_status,goals) goal ->
+      let status = S.focus output_status goal in
+      let output_status' = S.apply_tactic continuation status in
+      let new_goals' = S.goals output_status' in
+       (output_status',goals@new_goals')
+    ) (output_status,[]) new_goals
+  in
+   S.set_goals output_status goals
  in
-  mk_tactic (then_ ~start ~continuation)
+  S.mk_tactic (then_ ~start ~continuation)
 
 let rec seq ~tactics =
   match tactics with
@@ -130,53 +182,56 @@ let rec seq ~tactics =
 let repeat_tactic ~tactic =
  let rec repeat_tactic ~tactic status =
   warn "in repeat_tactic";
-  try let (proof, goallist) = apply_tactic tactic status in
-   let rec step proof goallist =
+  try
+   let output_status = S.apply_tactic tactic status in
+   let goallist = S.goals output_status in
+   let rec step output_status goallist =
     match goallist with
-       [] -> (proof, [])
+       [] -> output_status,[]
      | head::tail -> 
-        let (proof', goallist') = repeat_tactic ~tactic (proof, head) in
-         let (proof'', goallist'') = step proof' tail in
-          proof'', goallist'@goallist''
+        let status = S.focus output_status head in
+        let output_status' = repeat_tactic ~tactic status in
+        let goallist' = S.goals output_status' in
+         let output_status'',goallist'' = step output_status' tail in
+          output_status'',goallist'@goallist''
    in
-    step proof goallist
+    let output_status,goallist = step output_status goallist in
+     S.set_goals output_status goallist
   with 
    (Fail _) as e ->
     warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
-    apply_tactic id_tac status
+    S.apply_tactic S.id_tac status
  in 
-  mk_tactic (repeat_tactic ~tactic)
-;;
-
+  S.mk_tactic (repeat_tactic ~tactic)
 
 
 (* This tries to apply tactic n times *)
 let do_tactic ~n ~tactic =
  let rec do_tactic ~n ~tactic status =
-  warn "in do_tactic";
-  try 
-   let (proof, goallist) = 
-    if (n>0) then apply_tactic tactic status 
-             else apply_tactic 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 (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) ;
-    apply_tactic id_tac status
+  if n = 0 then
+   S.apply_tactic S.id_tac status
+  else
+   try 
+    let output_status = S.apply_tactic tactic status in
+    let goallist = S.goals output_status in
+    let rec step output_status goallist =
+     match goallist with
+        [] -> output_status, []
+      | head::tail -> 
+         let status = S.focus output_status head in
+         let output_status' = do_tactic ~n:(n-1) ~tactic status in
+         let goallist' = S.goals output_status' in 
+         let (output_status'', goallist'') = step output_status' tail in
+          output_status'', goallist'@goallist''
+    in
+     let output_status,goals = step output_status goallist in
+      S.set_goals output_status goals
+   with 
+    (Fail _) as e ->
+     warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+     S.apply_tactic S.id_tac status
  in
-  mk_tactic (do_tactic ~n ~tactic)
-;;
+  S.mk_tactic (do_tactic ~n ~tactic)
 
 
 
@@ -185,16 +240,13 @@ let try_tactic ~tactic =
  let rec try_tactic ~tactic status =
   warn "in Tacticals.try_tactic";
   try
-   apply_tactic tactic status
+   S.apply_tactic tactic status
   with
    (Fail _) as e -> 
     warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
-    apply_tactic id_tac status
+    S.apply_tactic S.id_tac status
  in
-  mk_tactic (try_tactic ~tactic)
-;;
-
-let fail_tac = mk_tactic (fun _ -> raise (Fail "fail tactical"))
+  S.mk_tactic (try_tactic ~tactic)
 
 (* This tries tactics until one of them doesn't _solve_ the goal *)
 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
@@ -205,14 +257,15 @@ let solve_tactics ~tactics =
   | (descr, currenttactic)::moretactics ->
       warn ("Tacticals.solve_tactics is trying " ^ descr);
       (try
-        let (proof, goallist) = apply_tactic currenttactic status in
+        let output_status = S.apply_tactic currenttactic status in
+        let goallist = S.goals output_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)
+                  output_status
           | _ -> warn ("Tacticals.solve_tactics: try the next tactic");
                  solve_tactics ~tactics:(moretactics) status
        with
@@ -222,7 +275,24 @@ let solve_tactics ~tactics =
          solve_tactics ~tactics status
       )
   | [] -> raise (Fail "solve_tactics cannot solve the goal");
-          apply_tactic id_tac status
+          S.apply_tactic S.id_tac status
  in
-  mk_tactic (solve_tactics ~tactics)
-;;
+  S.mk_tactic (solve_tactics ~tactics)
+end
+
+module ProofEngineStatus =
+ struct
+   type input_status = ProofEngineTypes.status
+   type output_status = ProofEngineTypes.proof * ProofEngineTypes.goal list
+   type tactic = ProofEngineTypes.tactic
+   let id_tac = id_tac
+   let mk_tactic = ProofEngineTypes.mk_tactic
+   let apply_tactic = ProofEngineTypes.apply_tactic
+   let goals (_,goals) = goals
+   let set_goals (proof,_) goals = proof,goals
+   let focus (proof,_) goal = proof,goal
+ end
+
+module ProofEngineTacticals = Make(ProofEngineStatus)
+
+include ProofEngineTacticals