]> matita.cs.unibo.it Git - helm.git/commitdiff
EXPERIMENTAL and _INCOMPLETE_ COMMIT:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Apr 2007 17:21:09 +0000 (17:21 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Apr 2007 17:21:09 +0000 (17:21 +0000)
Tacticals invoked from the top-level but the ones implemented on top
of tinycals  where not working properly because of several bugs.

The current commit changes the code in quite a few places:

1) there is no longer a function Tacticals.Make since tacticals implemented
   on top of tinycals always instantiated the functor with
   Tacticals.ProofEngineStatus, and the toplevel can avoid any instantiation
   at all since it can invoke tinycals directly on the low-level machine
   (implemented by the functor Continuationals.Make)
2) when GrafiteEngine now meets a punctuation tacticals, it directly invokes
   an instantiation of Continuationals.Make, without going througw Tacticals.
   Instead, when it meets a real tactical, it directly invokes Tacticals
   (where Continuationals.Make is applied to Tacticals.ProofEngineStatus
   and not to the module defined in GrafiteEngine and used for punctuation
   tacticals)
3) most of the tacticals not implemented on top of tinycals were bugged
   (and unused). E.g.: solve always diverged unless it was applied to the
   empty list. All these bugs have been fixed.

The commit is incomplete since:

1) all tacticals not implemented on top of tactics now accept only a single
   tactic as argument (if they require a list, the list must be a singleton).
   This limitation is going to disappear again, but we must change GrafiteAst
   so that an atomic tactical becomes a recursive tactic.
2) Seq and Then are not branched (for the same reasons as 1 and a bit of
   lazyness)
3) several auxiliary functions in the argument of Continuaniolas.Make can now
   be removed since they were introduced for wrong reasons.

helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/tactics/tacticals.ml
helm/software/components/tactics/tacticals.mli

index 51b86fa5e092db484f01737a5113db82087f8adc..c93aeb6547255185ae535f40d90b657feebd319c 100644 (file)
@@ -302,31 +302,20 @@ let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
   before @ produced_metas @ after, goals 
   
 let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) =
-(* prerr_endline "apply_tactic"; *)
-(* prerr_endline (Continuationals.Stack.pp (GrafiteTypes.get_stack status)); *)
  let starting_metasenv = GrafiteTypes.get_proof_metasenv status in
  let before = List.map (fun g, _, _ -> g) starting_metasenv in
-(* prerr_endline "disambiguate"; *)
  let status, tactic = disambiguate_tactic status goal (text,prefix_len,tactic) in
  let metasenv_after_refinement =  GrafiteTypes.get_proof_metasenv status in
  let proof = GrafiteTypes.get_current_proof status in
  let proof_status = proof, goal in
  let needs_reordering, always_opens_a_goal = classify_tactic tactic in
  let tactic = tactic_of_ast status tactic in
- (* apply tactic will change the lexicon_status ... *)
-(* prerr_endline "apply_tactic bassa"; *)
  let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
  let after = ProofEngineTypes.goals_of_proof proof in
  let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
-(* prerr_endline("before: " ^ String.concat ", " (List.map string_of_int before));
-prerr_endline("after: " ^ String.concat ", " (List.map string_of_int after));
-prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); *)
-(* prerr_endline("opened_goals: " ^ String.concat ", " (List.map string_of_int opened_goals));
-prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *)
  let proof, opened_goals = 
    if needs_reordering then begin
      let uri, metasenv_after_tactic, t, ty, attrs = proof in
-(* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *)
      let reordered_metasenv, opened_goals = 
        reorder_metasenv
         starting_metasenv
@@ -334,7 +323,6 @@ prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int clos
         opened goal always_opens_a_goal
      in
      let proof' = uri, reordered_metasenv, t, ty, attrs in
-(* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *)
      proof', opened_goals
    end
       else
@@ -350,6 +338,43 @@ prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int clos
      { incomplete_proof with GrafiteTypes.proof = proof } },
  opened_goals, closed_goals
 
+let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) (status, goal) =
+ let starting_metasenv = GrafiteTypes.get_proof_metasenv status in
+ let before = List.map (fun g, _, _ -> g) starting_metasenv in
+ let status, tactic = disambiguate_tactic status goal (text,prefix_len,tactic) in
+ let metasenv_after_refinement =  GrafiteTypes.get_proof_metasenv status in
+ let proof = GrafiteTypes.get_current_proof status in
+ let proof_status = proof, goal in
+ let needs_reordering, always_opens_a_goal = classify_tactic tactic in
+ let tactic = tactic_of_ast status tactic in
+ let tactic = patch tactic in
+ let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
+ let after = ProofEngineTypes.goals_of_proof proof in
+ let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
+ let proof, opened_goals = 
+   if needs_reordering then begin
+     let uri, metasenv_after_tactic, t, ty, attrs = proof in
+     let reordered_metasenv, opened_goals = 
+       reorder_metasenv
+        starting_metasenv
+        metasenv_after_refinement metasenv_after_tactic
+        opened goal always_opens_a_goal
+     in
+     let proof' = uri, reordered_metasenv, t, ty, attrs in
+     proof', opened_goals
+   end
+      else
+        proof, opened_goals
+ in
+ let incomplete_proof =
+   match status.GrafiteTypes.proof_status with
+   | GrafiteTypes.Incomplete_proof p -> p
+   | _ -> assert false
+ in
+ { status with GrafiteTypes.proof_status =
+    GrafiteTypes.Incomplete_proof
+     { incomplete_proof with GrafiteTypes.proof = proof } },
+ opened_goals, closed_goals
 type eval_ast =
  {ea_go:
   'term 'lazy_term 'reduction 'obj 'ident.
@@ -491,45 +516,101 @@ let eval_tactical ~disambiguate_tactic status tac =
    let focus goal (status, _, _) = (status, goal)
   end
  in
- let module MatitaTacticals = Tacticals.Make (MatitaStatus) in
-  let rec tactical_of_ast l (text,prefix_len,tac) =
+(*
+ let rec atomic_tactical_of_ast (text,prefix_len,tac) =
+  match tac with
+   | GrafiteAst.Tactic (loc, tactic) ->
+      cic_tactic_of_ast ~disambiguate_tactic (text,prefix_len,tactic)
+       (status,~-1)
+   | GrafiteAst.Seq (loc,tacticals) ->
+      Tacticals.seq
+       (List.map atomic_tactical_of_ast
+        (List.map (fun x -> text,prefix_len,x) tacticals))
+   | _ -> assert false
+ in
+*)
+ let module MatitaTacticals = Continuationals.Make(MatitaStatus) in
+  let tactical_of_ast l (text,prefix_len,tac) =
     let apply_tactic t = apply_tactic (text, prefix_len, t) in
-    let tactical_of_ast l t = tactical_of_ast l (text,prefix_len,t) in
     match tac with
     | GrafiteAst.Tactic (loc, tactic) ->
-        MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic))
+        MatitaTacticals.eval
+         (MatitaTacticals.Tactical
+          (MatitaTacticals.Tactic
+           (MatitaStatus.mk_tactic (apply_tactic tactic))))
+(*
     | GrafiteAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
        assert (l > 0);
        MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals)
     | GrafiteAst.Do (loc, n, tactical) ->
         MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical)
-    | GrafiteAst.Repeat (loc, tactical) ->
-        MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical)
+*)
+    | GrafiteAst.Repeat (loc, GrafiteAst.Tactic (_,tactical)) ->
+       MatitaTacticals.eval
+        (MatitaTacticals.Tactical
+          (MatitaTacticals.Tactic
+           (MatitaStatus.mk_tactic
+            (apply_atomic_tactical ~disambiguate_tactic
+              ~patch:(fun tactic -> Tacticals.repeat_tactic ~tactic)
+              (text,prefix_len,tactical)))))
+(*
     | GrafiteAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
         assert (l > 0);
         MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical)
           ~continuations:(List.map (tactical_of_ast (l+1)) tacticals)
-    | GrafiteAst.First (loc, tacticals) ->
-        MatitaTacticals.first
-          ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
-    | GrafiteAst.Try (loc, tactical) ->
-        MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical)
-    | GrafiteAst.Solve (loc, tacticals) ->
-        MatitaTacticals.solve_tactics
-         ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
-    | GrafiteAst.Progress (loc, tactical) ->
-        MatitaTacticals.progress_tactic ~tactic:(tactical_of_ast (l+1) tactical)
-
-    | GrafiteAst.Skip _loc -> MatitaTacticals.skip
-    | GrafiteAst.Dot _loc -> MatitaTacticals.dot
-    | GrafiteAst.Semicolon _loc -> MatitaTacticals.semicolon
-    | GrafiteAst.Branch _loc -> MatitaTacticals.branch
-    | GrafiteAst.Shift _loc -> MatitaTacticals.shift
-    | GrafiteAst.Pos (_loc, i) -> MatitaTacticals.pos i
-    | GrafiteAst.Merge _loc -> MatitaTacticals.merge
-    | GrafiteAst.Focus (_loc, goals) -> MatitaTacticals.focus goals
-    | GrafiteAst.Unfocus _loc -> MatitaTacticals.unfocus
-    | GrafiteAst.Wildcard _loc -> MatitaTacticals.wildcard
+*)
+    | GrafiteAst.First (loc, [GrafiteAst.Tactic (_,tacticals)]) ->
+       MatitaTacticals.eval
+        (MatitaTacticals.Tactical
+          (MatitaTacticals.Tactic
+           (MatitaStatus.mk_tactic
+            (apply_atomic_tactical ~disambiguate_tactic
+              ~patch:(fun tactic ->Tacticals.first ~tactics:["",tactic])
+              (text,prefix_len,tacticals)))))
+    | GrafiteAst.Try (loc, GrafiteAst.Tactic (_,tactical)) ->
+       MatitaTacticals.eval
+        (MatitaTacticals.Tactical
+          (MatitaTacticals.Tactic
+           (MatitaStatus.mk_tactic
+            (apply_atomic_tactical ~disambiguate_tactic
+              ~patch:(fun tactic -> Tacticals.try_tactic ~tactic)
+              (text,prefix_len,tactical)))))
+    | GrafiteAst.Solve (loc, [GrafiteAst.Tactic (_,tacticals)]) ->
+       MatitaTacticals.eval
+        (MatitaTacticals.Tactical
+          (MatitaTacticals.Tactic
+           (MatitaStatus.mk_tactic
+            (apply_atomic_tactical ~disambiguate_tactic
+              ~patch:(fun tactic ->Tacticals.solve_tactics ~tactics:["",tactic])
+              (text,prefix_len,tacticals)))))
+    | GrafiteAst.Progress (loc, GrafiteAst.Tactic (_,tactical)) ->
+       MatitaTacticals.eval
+        (MatitaTacticals.Tactical
+          (MatitaTacticals.Tactic
+           (MatitaStatus.mk_tactic
+            (apply_atomic_tactical ~disambiguate_tactic
+              ~patch:(fun tactic -> Tacticals.progress_tactic ~tactic)
+              (text,prefix_len,tactical)))))
+    | GrafiteAst.Skip _loc ->
+       MatitaTacticals.eval (MatitaTacticals.Tactical MatitaTacticals.Skip)
+    | GrafiteAst.Dot _loc ->
+       MatitaTacticals.eval (MatitaTacticals.Dot)
+    | GrafiteAst.Semicolon _loc ->
+       MatitaTacticals.eval (MatitaTacticals.Semicolon)
+    | GrafiteAst.Branch _loc ->
+       MatitaTacticals.eval MatitaTacticals.Branch
+    | GrafiteAst.Shift _loc ->
+       MatitaTacticals.eval MatitaTacticals.Shift
+    | GrafiteAst.Pos (_loc, i) ->
+       MatitaTacticals.eval (MatitaTacticals.Pos i)
+    | GrafiteAst.Merge _loc ->
+       MatitaTacticals.eval MatitaTacticals.Merge
+    | GrafiteAst.Focus (_loc, goals) ->
+       MatitaTacticals.eval (MatitaTacticals.Focus goals)
+    | GrafiteAst.Unfocus _loc ->
+       MatitaTacticals.eval MatitaTacticals.Unfocus
+    | GrafiteAst.Wildcard _loc ->
+       MatitaTacticals.eval MatitaTacticals.Wildcard
   in
   let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
   let status =  (* is proof completed? *)
index c6fbc36a40594cf0b3aa0f23fede5cf72f48ae1b..eb3ebc1bba506c4a748b846d36a45a968fe814ec 100644 (file)
@@ -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
 
@@ -336,24 +110,24 @@ struct
 
   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 ->
         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
@@ -363,14 +137,144 @@ struct
   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 first ~tactics =
+  let rec first ~(tactics: (string * tactic) list) status =
+    info (lazy "in Tacticals.first");
+    match tactics with
+      [] -> raise (PET.Fail (lazy "first: no tactics left"))
+    | (descr, tac)::tactics ->
+        info (lazy ("Tacticals.first IS TRYING " ^ descr));
+        try
+         let res = PET.apply_tactic tac status in
+          info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
+          res
+        with 
+         PET.Fail _ -> first ~tactics status
+  in
+  PET.mk_tactic (first ~tactics)
+
 
-include ProofEngineTacticals
+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: (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 (proof, opened) as output_status =
+         PET.apply_tactic currenttactic status 
+        in
+        match opened with 
+          | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^ 
+                   " 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,_,_,_),_) as istatus) =
+    let ((_,metasenv',_,_,_),_) as ostatus =
+     PET.apply_tactic tactic istatus
+    in
+     (*CSC: Warning
+       If just the index of some metas changes the tactic is recognized
+       as a progressing one. This is wrong. *)
+     if metasenv' = metasenv then
+      raise (PET.Fail msg)
+     else
+      ostatus
+  in
+  PET.mk_tactic progress_tactic
index 83e00d1067c3d80a90b17c53b617f27c5664ed52..a1b8ec7cd3e272af6f107344c81fc14620aec611 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-val id_tac : ProofEngineTypes.tactic
-val fail_tac: ProofEngineTypes.tactic
+type tactic = ProofEngineTypes.tactic
 
-(* module type Status =
- sig
-|+    type external_input_status +|
-   type input_status
-   type output_status
-|+    type external_output_status +|
+val id_tac : tactic
+val fail_tac: tactic
 
-|+    val internalize: external_input_status -> input_status
-   val externalize: output_status -> external_output_status +|
-
-   type tactic
-
-   val mk_tactic : (input_status -> output_status) -> tactic
-   val apply_tactic : tactic -> input_status -> output_status
-
-   val id_tac : tactic
-
-   val goals : output_status -> ProofEngineTypes.goal list
-   val get_stack : input_status -> stack
-   val set_stack : stack -> output_status -> output_status
-
-   val inject : input_status -> output_status
-   val focus : goal -> output_status -> input_status
- end *)
-
-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 (** "folding" of then_ *)
-  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 
-
-(*   module C:
-  sig *)
-  val tactic: tactic -> tactic  (** apply tactic to all goal in env *)
-  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 *)
-end
-
-module Make (S: Continuationals.Status) : T with type tactic = S.tactic
-
-include T with type tactic = ProofEngineTypes.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 (** "folding" of then_ *)
+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 
 
 (* TODO temporary *)
 val goals_diff:
@@ -91,4 +44,3 @@ val goals_diff:
   after:ProofEngineTypes.goal list ->
   opened:ProofEngineTypes.goal list ->
     ProofEngineTypes.goal list * ProofEngineTypes.goal list
-