(* This tries to apply tactic n times *)
let do_tactic ~n ~tactic =
let rec do_tactic ~n ~tactic status =
- warn "in do_tactic";
- try
- let output_status =
- if (n>0) then S.apply_tactic tactic status
- else S.apply_tactic S.id_tac status in
- let goallist = S.goals output_status in
-(* else (proof, []) in *)
-(* perche' non va bene questo? stessa questione di ##### ? *)
- let rec step output_status goallist =
- match goallist with
- [] -> output_status, []
- | head::tail ->
- let status = S.focus output_status head in
- let output_status' = do_tactic ~n:(n-1) ~tactic status in
- let goallist' = S.goals output_status' in
- let (output_status'', goallist'') = step output_status' tail in
- output_status'', goallist'@goallist''
- in
- let output_status,goals = step output_status goallist in
- S.set_goals output_status goals
- with
- (Fail _) as e ->
- warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
- S.apply_tactic S.id_tac status
+ if n = 0 then
+ S.apply_tactic S.id_tac status
+ else
+ try
+ let output_status = S.apply_tactic tactic status in
+ let goallist = S.goals output_status in
+ let rec step output_status goallist =
+ match goallist with
+ [] -> output_status, []
+ | head::tail ->
+ let status = S.focus output_status head in
+ let output_status' = do_tactic ~n:(n-1) ~tactic status in
+ let goallist' = S.goals output_status' in
+ let (output_status'', goallist'') = step output_status' tail in
+ output_status'', goallist'@goallist''
+ in
+ let output_status,goals = step output_status goallist in
+ S.set_goals output_status goals
+ with
+ (Fail _) as e ->
+ warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
+ S.apply_tactic S.id_tac status
in
S.mk_tactic (do_tactic ~n ~tactic)