--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id$ *)
+
+(* open CicReduction
+open ProofEngineTypes
+open UriManager *)
+
+(** DEBUGGING *)
+
+ (** perform debugging output? *)
+let debug = false
+let debug_print = fun _ -> ()
+
+ (** debugging print *)
+let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s)))
+
+module PET = ProofEngineTypes
+
+let id_tac =
+ let id_tac (proof,goal) =
+ let _, metasenv, _subst, _, _, _ = proof in
+ let _, _, _ = CicUtil.lookup_meta goal metasenv in
+ (proof,[goal])
+ in
+ PET.mk_tactic id_tac
+
+let fail_tac =
+ let fail_tac (proof,goal) =
+ let _, metasenv, _subst, _ , _, _ = proof in
+ let _, _, _ = CicUtil.lookup_meta goal metasenv in
+ raise (PET.Fail (lazy "fail tactical"))
+ in
+ PET.mk_tactic fail_tac
+
+type goal = PET.goal
+
+ (** TODO needed until tactics start returning both opened and closed goals
+ * First part of the function performs a diff among goals ~before tactic
+ * application and ~after it. Second part will add as both opened and closed
+ * the goals which are returned as opened by the tactic *)
+let goals_diff ~before ~after ~opened =
+ let sort_opened opened add =
+ opened @ (List.filter (fun g -> not (List.mem g opened)) add)
+ in
+ let remove =
+ List.fold_left
+ (fun remove e -> if List.mem e after then remove else e :: remove)
+ [] before
+ in
+ let add =
+ List.fold_left
+ (fun add e -> if List.mem e before then add else e :: add)
+ []
+ after
+ in
+ let add, remove = (* adds goals which have been both opened _and_ closed *)
+ List.fold_left
+ (fun (add, remove) opened_goal ->
+ if List.mem opened_goal before
+ then opened_goal :: add, opened_goal :: remove
+ else add, remove)
+ (add, remove)
+ opened
+ in
+ sort_opened opened add, remove
+
+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
+
+ type output_status =
+ (PET.proof * goal list * goal list) * Stack.t
+
+ type tactic = PET.tactic
+
+ (* 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 (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 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
+ (proof', opened_goals, closed_goals), stack
+
+ let goals ((_, opened, closed), _) = opened, closed
+
+ (* 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 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
+
+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,_subst,_,_,_),g) as istatus) =
+ let ((_,metasenv',_subst,_,_,_),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
projects / helm.git / blobdiff