open Printf
-exception Error of string
-
-let fail msg = raise (Error msg)
+exception Error of string Lazy.t
module type Engine =
sig
match tactical, switch with
| Tactic tac, Open n -> E.apply_tactic tac proof n
| Skip, Closed n -> proof, [], [n]
- | Tactic _, Closed _ -> fail "can't apply tactic to a closed goal"
- | Skip, Open _ -> fail "can't skip an open goal"
+ | Tactic _, Closed _ -> raise (Error (lazy "can't apply tactic to a closed goal"))
+ | Skip, Open _ -> raise (Error (lazy "can't skip an open goal"))
let eval continuational status =
match continuational, status with
| Dot, (proof, (env, todo, left, tag)::tail) ->
let env, left =
match List.filter is_open env, left with
- | [], [] -> fail "There is nothig to do for '.'"
+ | [], [] -> raise (Error (lazy "There is nothig to do for '.'"))
| g::env,left -> [g], union (List.map goal_of env) left
| [], g::left -> [dummy_pos, Open g], left
in
| Branch, (proof, (g1::tl, todo, left, tag)::tail) ->
assert (List.length tl >= 1);
proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail
- | Branch, (_, _) -> fail "can't branch on a singleton context"
+ | Branch, (_, _) -> raise (Error (lazy "can't branch on a singleton context"))
| Shift opt_pos, (proof, (leftopen, t, l,BranchTag)::
(goals, todo, left,tag)::tail) ->
let next_goal, rem_goals =
| Some pos, _ ->
(try
list_assoc_extract pos goals
- with Not_found -> fail (sprintf "position %d not found" pos))
- | None, [] -> fail "no more goals to shift"
+ with Not_found -> raise (Error (lazy (sprintf "position %d not found" pos))))
+ | None, [] -> raise (Error (lazy "no more goals to shift"))
in
let t =
union t (union (List.map goal_of (List.filter is_open leftopen)) l)
in
proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail
- | Shift _, (_, _) -> fail "no more goals to shift"
+ | Shift _, (_, _) -> raise (Error (lazy "no more goals to shift"))
| Select gl, (proof, stack) ->
List.iter
(fun g ->
if E.is_goal_closed g proof then
- fail "you can't select a closed goal")
+ raise (Error (lazy "you can't select a closed goal")))
gl;
(proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack)
| End, (proof, stack) ->
(union not_processed (List.filter is_open leftopen))))
in
proof, (env,todo,left,tag)::tail
- | _ -> fail "can't end here")
+ | _ -> raise (Error (lazy "can't end here")))
let init proof =
proof,