(** perform debugging output? *)
let debug = false
+let debug_print = fun _ -> ()
(** debugging print *)
let warn s =
if debug then
- prerr_endline ("TACTICALS WARNING: " ^ s)
+ debug_print ("TACTICALS WARNING: " ^ s)
(** TACTIC{,AL}S *)
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? *)
| (Some (Cic.Name name,_))::_ when name = "T" -> n
| _::tl -> find (n+1) tl
in
- prerr_endline ("eseguo find");
+ debug_print ("eseguo find");
find 1 context
in
- prerr_endline ("eseguo apply");
+ debug_print ("eseguo apply");
apply_tac ~term:(Cic.Rel rel) status
in
(* do_tactic ~n:2 *)