X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.ml;h=34ecb2d99d1c68f6f18a58cca383cb396358f663;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=28bd71b2da5901c199114dde8ce8bacf79aaa17f;hpb=4885f49660dc31fc6ecbed36c383b111381a8684;p=helm.git

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index 28bd71b2d..34ecb2d99 100644
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -42,7 +42,7 @@ module PET = ProofEngineTypes
 
 let id_tac = 
  let id_tac (proof,goal) = 
-  let _, metasenv, _, _ = proof in
+  let _, metasenv, _, _, _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
   (proof,[goal])
  in 
@@ -50,7 +50,7 @@ let id_tac =
 
 let fail_tac =
  let fail_tac (proof,goal) =
-  let _, metasenv, _, _ = proof in
+  let _, metasenv, _, _ , _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
    raise (PET.Fail (lazy "fail tactical"))
  in
@@ -88,244 +88,18 @@ let goals_diff ~before ~after ~opened =
   in
   sort_opened opened add, remove
 
-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
-  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
-  val progress_tactic: tactic: tactic -> tactic 
-
-  val tactic: tactic -> tactic
-  val skip: tactic
-  val dot: tactic
-  val semicolon: tactic
-  val branch: tactic
-  val shift: tactic
-  val pos: int list -> tactic
-  val wildcard: tactic
-  val merge: tactic
-  val focus: int list -> tactic
-  val unfocus: tactic
-end
-
-module Make (S: Continuationals.Status) : T with type tactic = S.tactic =
-struct
-  module C = Continuationals.Make (S)
-
-  type tactic = S.tactic
-
-  let fold_eval status ts =
-    let istatus =
-      List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts
-    in
-    S.inject istatus
-
-  (**
-    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")
-  *)
-  let first ~tactics =
-    let rec first ~(tactics: (string * tactic) list) istatus =
-      info (lazy "in Tacticals.first");
-      match tactics with
-      | (descr, tac)::tactics ->
-          info (lazy ("Tacticals.first IS TRYING " ^ descr));
-          (try
-            let res = S.apply_tactic tac istatus in
-            info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
-            res
-          with
-          e ->
-            match e with
-            | (PET.Fail _)
-            | (CicTypeChecker.TypeCheckerFailure _)
-            | (CicUnification.UnificationFailure _) ->
-                info (lazy (
-                  "Tacticals.first failed with exn: " ^
-                  Printexc.to_string e));
-                  first ~tactics istatus
-            | _ -> raise e) (* [e] must not be caught ; let's re-raise it *)
-      | [] -> raise (PET.Fail (lazy "first: no tactics left"))
-    in
-    S.mk_tactic (first ~tactics)
-
-  let thens ~start ~continuations =
-    S.mk_tactic
-      (fun istatus ->
-        fold_eval istatus
-          ([ C.Tactical (C.Tactic start); C.Branch ]
-          @ (HExtlib.list_concat ~sep:[ C.Shift ]
-              (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
-          @ [ C.Merge ]))
-
-  let then_ ~start ~continuation =
-    S.mk_tactic
-      (fun istatus ->
-        let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
-        let opened,closed = S.goals ostatus in
-         match opened with
-            [] -> ostatus
-          | _ ->
-            fold_eval (S.focus ~-1 ostatus)
-              [ C.Semicolon;
-                C.Tactical (C.Tactic continuation) ])
-
-  let seq ~tactics =
-    S.mk_tactic
-      (fun istatus ->
-        fold_eval istatus
-          (HExtlib.list_concat ~sep:[ C.Semicolon ]
-            (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
-
-  (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno
-   * applicato la tattica *)
-
-  let rec step f output_status opened closed =
-    match opened with
-    | [] -> output_status, [], closed
-    | head :: tail -> 
-        let status = S.focus head output_status in
-        let output_status' = f status in
-        let opened', closed' = S.goals output_status' in
-        let output_status'', opened'', closed'' =
-          step f output_status' tail []
-        in
-        output_status'', opened' @ opened'', closed' @ closed''
-
-  (* 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 repeat_tactic ~tactic =
-   let rec repeat_tactic ~tactic status =
-    info (lazy "in repeat_tactic");
-    try
-     let output_status = S.apply_tactic tactic status in
-     let opened, closed = S.goals output_status in
-     let output_status, opened', closed' =
-       step (repeat_tactic ~tactic) output_status opened closed
-     in
-     S.set_goals (opened', closed') output_status
-    with 
-     (PET.Fail _) as e ->
-      info (lazy
-        ("Tacticals.repeat_tactic failed after nth time with exception: "
-         ^ Printexc.to_string e));
-      S.apply_tactic S.id_tactic status
-   in 
-    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 =
-    if n = 0 then
-     S.apply_tactic S.id_tactic status
-    else
-     try 
-      let output_status = S.apply_tactic tactic status in
-      let opened, closed = S.goals output_status in
-       let output_status, opened', closed' =
-         step (do_tactic ~n:(n-1) ~tactic) output_status opened closed
-       in
-       S.set_goals (opened', closed') output_status
-     with 
-      (PET.Fail _) as e ->
-       info (lazy
-          ("Tacticals.do_tactic failed after nth time with exception: "
-           ^ Printexc.to_string e)) ;
-       S.apply_tactic S.id_tactic status
-   in
-    S.mk_tactic (do_tactic ~n ~tactic)
-
-  (* This applies tactic and catches its possible failure *)
-  let try_tactic ~tactic =
-   let try_tactic status =
-    info (lazy "in Tacticals.try_tactic");
-    try
-     S.apply_tactic tactic status
-    with
-     (PET.Fail _) as e -> 
-      info (lazy (
-        "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
-      S.apply_tactic S.id_tactic status
-   in
-    S.mk_tactic try_tactic
-
-  (* This tries tactics until one of them doesn't _solve_ the goal *)
-  (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
-  let solve_tactics ~tactics =
-   let rec solve_tactics ~(tactics: (string * tactic) list) status =
-    info (lazy "in Tacticals.solve_tactics");
-    match tactics with
-    | (descr, currenttactic)::moretactics ->
-        info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
-        (try
-          let output_status = S.apply_tactic currenttactic status in
-          let opened, closed = S.goals output_status in
-           match opened with 
-            | [] -> info (lazy ("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!) *)
-                    output_status
-            | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
-                   solve_tactics ~tactics:(moretactics) status
-         with
-          (PET.Fail _) as e ->
-           info (lazy (
-              "Tacticals.solve_tactics: current tactic failed with exn: "
-              ^ Printexc.to_string e));
-           solve_tactics ~tactics status
-        )
-    | [] ->
-        raise (PET.Fail
-          (lazy "solve_tactics cannot solve the goal"))
-   in
-    S.mk_tactic (solve_tactics ~tactics)
-
-  let progress_tactic ~tactic =
-    let msg = lazy "Failed to progress" in
-    let get_sequent (proof, goal) =
-      let (_, metasenv, _, _) = proof in
-      let _, context, ty = CicUtil.lookup_meta goal metasenv in
-      context, ty
-    in
-    let progress_tactic ist =
-      let before = get_sequent (S.get_status ist) in
-      let ost = S.apply_tactic tactic ist in
-      match S.goals ost with
-        | [goal], _ when before <> get_sequent (S.get_proof ost, goal) ->
-           raise (PET.Fail msg)
-        | _  -> ost
-    in
-    S.mk_tactic progress_tactic
-
-  let cont_proxy cont = S.mk_tactic (C.eval cont)
-
-  let tactic t = cont_proxy (C.Tactical (C.Tactic t))
-  let skip = cont_proxy (C.Tactical C.Skip)
-  let dot = cont_proxy C.Dot
-  let semicolon = cont_proxy C.Semicolon
-  let branch = cont_proxy C.Branch
-  let shift = cont_proxy C.Shift
-  let pos i = cont_proxy (C.Pos i)
-  let wildcard =  cont_proxy C.Wildcard
-  let merge = cont_proxy C.Merge
-  let focus goals = cont_proxy (C.Focus goals)
-  let unfocus = cont_proxy C.Unfocus
-end
-
 module ProofEngineStatus =
 struct
   module Stack = Continuationals.Stack
 
+  (* The stack is used and saved only at the very end of the eval function;
+     it is read only at the beginning of the eval;
+     we need it just to apply several times in a row this machine to an
+     initial stack, i.e. to chain several applications of the machine together,
+     i.e. to dump and restore the state of the machine.
+     The stack is never used by the tactics: each tactic of type
+     PET.tactic ignore the stack. To make a tactic from the eval function
+     of a machine we apply the eval on a fresh stack (via the mk_tactic). *)
   type input_status =
     PET.status (* (proof, goal) *) * Stack.t
 
@@ -334,43 +108,200 @@ struct
 
   type tactic = PET.tactic
 
-  let id_tactic = id_tac
-
+  (* f is an eval function of a machine;
+     the machine is applied to a fresh stack and the final stack is read
+     back to obtain the result of the tactic *)
   let mk_tactic f =
     PET.mk_tactic
-      (fun (proof, goal) as pstatus ->
+      (fun ((proof, goal) as pstatus) ->
         let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
         let istatus = pstatus, stack in
-(*         let ostatus = f istatus in
-        let ((proof, opened, _), _) = ostatus in *)
         let (proof, _, _), stack = f istatus in
         let opened = Continuationals.Stack.open_goals stack in
         proof, opened)
 
+  (* it applies a tactic ignoring (and preserving) the stack *)
   let apply_tactic tac ((proof, _) as pstatus, stack) =
     let proof', opened = PET.apply_tactic tac pstatus in
-(* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *)
     let before = PET.goals_of_proof proof in
     let after = PET.goals_of_proof proof' in
     let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
-(* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *)
     (proof', opened_goals, closed_goals), stack
 
-  let get_status (status, _) = status
-  let get_proof ((proof, _, _), _) = proof
-
   let goals ((_, opened, closed), _) = opened, closed
-  let set_goals (opened, closed) ((proof, _, _), stack) =
-    (proof, opened, closed), stack
 
+  (* Done only at the beginning of the eval of the machine *)
   let get_stack = snd
+  (* Done only at the end of the eval of the machine *)
   let set_stack stack (opstatus, _) = opstatus, stack
 
   let inject ((proof, _), stack) = ((proof, [], []), stack)
   let focus goal ((proof, _, _), stack) = (proof, goal), stack
 end
 
-module ProofEngineTacticals = Make (ProofEngineStatus)
+module S = ProofEngineStatus
+module C = Continuationals.Make (S)
+
+type tactic = S.tactic
+
+let fold_eval status ts =
+  let istatus =
+    List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts
+  in
+  S.inject istatus
+
+(* Tacticals implemented on top of tynycals *)
+
+let thens ~start ~continuations =
+  S.mk_tactic
+    (fun istatus ->
+      fold_eval istatus
+        ([ C.Tactical (C.Tactic start); C.Branch ]
+        @ (HExtlib.list_concat ~sep:[ C.Shift ]
+            (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
+        @ [ C.Merge ]))
+
+let then_ ~start ~continuation =
+  S.mk_tactic
+    (fun istatus ->
+      let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
+      let opened,closed = S.goals ostatus in
+       match opened with
+          [] -> ostatus
+        | _ ->
+          fold_eval (S.focus ~-1 ostatus)
+            [ C.Semicolon;
+              C.Tactical (C.Tactic continuation) ])
+
+let seq ~tactics =
+  S.mk_tactic
+    (fun istatus ->
+      fold_eval istatus
+        (HExtlib.list_concat ~sep:[ C.Semicolon ]
+          (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
+
+(* Tacticals that cannot be implemented on top of tynycals *)
+
+let const_tac res = PET.mk_tactic (fun _ -> res)
+
+let if_ ~start ~continuation ~fail =
+   let if_ status =
+      let xoutput = 
+         try
+	    let result = PET.apply_tactic start status in
+	    info (lazy ("Tacticals.if_: succedeed!!!"));
+	    Some result 
+	 with PET.Fail _ -> None
+      in
+      let tactic = match xoutput with
+         | Some res -> then_ ~start:(const_tac res) ~continuation
+	 | None     -> fail
+      in 
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic if_
+
+let ifs ~start ~continuations ~fail =
+   let ifs status =
+      let xoutput = 
+         try
+	    let result = PET.apply_tactic start status in
+	    info (lazy ("Tacticals.ifs: succedeed!!!"));
+	    Some result 
+	 with PET.Fail _ -> None
+      in
+      let tactic = match xoutput with
+         | Some res -> thens ~start:(const_tac res) ~continuations
+	 | None     -> fail
+      in 
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic ifs
 
-include ProofEngineTacticals
+let first ~tactics =
+  let rec first ~(tactics: tactic list) status =
+    info (lazy "in Tacticals.first");
+    match tactics with
+      [] -> raise (PET.Fail (lazy "first: no tactics left"))
+    | tac::tactics ->
+        try
+         let res = PET.apply_tactic tac status in
+          info (lazy ("Tacticals.first: succedeed!!!"));
+          res
+        with 
+         PET.Fail _ -> first ~tactics status
+  in
+  PET.mk_tactic (first ~tactics)
 
+let rec do_tactic ~n ~tactic =
+ PET.mk_tactic
+  (function status ->
+    if n = 0 then
+     PET.apply_tactic id_tac status
+    else
+     PET.apply_tactic
+      (then_ ~start:tactic ~continuation:(do_tactic ~n:(n-1) ~tactic))
+      status)
+
+(* This applies tactic and catches its possible failure *)
+let try_tactic ~tactic =
+ let try_tactic status =
+  try
+    PET.apply_tactic tactic status
+  with (PET.Fail _) as e -> 
+    info (lazy (
+      "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
+    PET.apply_tactic id_tac status
+ in
+  PET.mk_tactic try_tactic
+
+let rec repeat_tactic ~tactic =
+ ProofEngineTypes.mk_tactic
+  (fun status ->
+    ProofEngineTypes.apply_tactic
+     (then_ ~start:tactic
+       ~continuation:(try_tactic (repeat_tactic ~tactic))) status)
+
+(* This tries tactics until one of them solves the goal *)
+let solve_tactics ~tactics =
+ let rec solve_tactics ~(tactics: tactic list) status =
+  info (lazy "in Tacticals.solve_tactics");
+  match tactics with
+  | currenttactic::moretactics ->
+      (try
+        let (proof, opened) as output_status =
+         PET.apply_tactic currenttactic status 
+        in
+        match opened with 
+          | [] -> info (lazy ("Tacticals.solve_tactics: solved the goal!!!"));
+                  output_status
+          | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
+                 raise (PET.Fail (lazy "Goal not solved"))
+       with (PET.Fail _) as e ->
+         info (lazy (
+            "Tacticals.solve_tactics: current tactic failed with exn: "
+            ^ Printexc.to_string e));
+         solve_tactics ~tactics:moretactics status)
+  | [] ->
+      raise (PET.Fail
+        (lazy "solve_tactics cannot solve the goal"))
+ in
+  PET.mk_tactic (solve_tactics ~tactics)
+
+let progress_tactic ~tactic =
+  let msg = lazy "Failed to progress" in
+  let progress_tactic (((_,metasenv,_,_,_,_),g) as istatus) =
+    let ((_,metasenv',_,_,_,_),opened) as ostatus =
+     PET.apply_tactic tactic istatus
+    in
+    match opened with
+    | [g1] ->
+        let _,oc,oldty = CicUtil.lookup_meta g metasenv in
+        let _,nc,newty = CicUtil.lookup_meta g1 metasenv' in
+        if oldty = newty && oc = nc then
+          raise (PET.Fail msg)
+        else
+          ostatus
+    | _ -> ostatus
+  in
+  PET.mk_tactic progress_tactic