in
mk_tactic tac
-
(**
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
in
mk_tactic (then_ ~start ~continuation)
-(* Galla *)
-(* si suppone che tutte le tattiche sollevino solamente Fail? *)
-
+let rec seq ~tactics =
+ match tactics with
+ | [] -> assert false
+ | [tac] -> tac
+ | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl)
(* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
mk_tactic (try_tactic ~tactic)
;;
+let fail = mk_tactic (fun _ -> raise (Fail "fail tactical"))
(* This tries tactics until one of them doesn't _solve_ the goal *)
(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)