From 097b7147a9daf37360fa51828e0f14843b5bd881 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 25 Oct 2005 16:39:45 +0000 Subject: [PATCH] Semantic change: applying a tactic to the empty goal list is now an error. --- helm/ocaml/tactics/continuationals.ml | 3 +- helm/ocaml/tactics/tacticals.ml | 81 +++------------------------ 2 files changed, 10 insertions(+), 74 deletions(-) diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml index 345502d5b..b720b6b70 100644 --- a/helm/ocaml/tactics/continuationals.ml +++ b/helm/ocaml/tactics/continuationals.ml @@ -25,7 +25,7 @@ open Printf -let debug = true +let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () exception Error of string lazy_t @@ -268,6 +268,7 @@ struct match cmd, stack with | _, [] -> assert false | Tactical tac, (g, t, k, tag) :: s -> + if g = [] then fail (lazy "can't apply a tactic to zero goals"); debug_print (lazy ("context length " ^string_of_int (List.length g))); let rec aux s go gc = function diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 827d58bbc..8281c9452 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -159,54 +159,17 @@ struct (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations)) @ [ C.Merge ])) -(* let thens ~start ~continuations = - let thens ~start ~continuations status = - let output_status = S.apply_tactic start status in - let new_goals = S.goals output_status in - try - let output_status,goals = - List.fold_left2 - (fun (output_status,goals) goal tactic -> - let status = S.focus goal output_status in - let output_status' = S.apply_tactic tactic status in - let new_goals' = S.goals output_status' in - (output_status',goals@new_goals') - ) (output_status,[]) new_goals continuations - in - S.set_goals output_status goals - with - Invalid_argument _ -> - let debug = Printf.sprintf "thens: expected %i new goals, found %i" - (List.length continuations) (List.length new_goals) - in - raise (Fail debug) - in - S.mk_tactic (thens ~start ~continuations ) *) - let then_ ~start ~continuation = S.mk_tactic (fun istatus -> - fold_eval istatus - [ C.Tactical (C.Tactic start); - C.Semicolon; - C.Tactical (C.Tactic continuation) ]) - -(* let then_ ~start ~continuation = - let then_ ~start ~continuation status = - let output_status = S.apply_tactic start status in - let new_goals = S.goals output_status in - let output_status,goals = - List.fold_left - (fun (output_status,goals) goal -> - let status = S.focus goal output_status in - let output_status' = S.apply_tactic continuation status in - let new_goals' = S.goals output_status' in - (output_status',goals@new_goals') - ) (output_status,[]) new_goals - in - S.set_goals output_status goals - in - S.mk_tactic (then_ ~start ~continuation) *) + 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 @@ -215,12 +178,6 @@ struct (HExtlib.list_concat ~sep:[ C.Semicolon ] (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics))) -(* 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 *) @@ -243,18 +200,6 @@ struct let rec repeat_tactic ~tactic status = info (lazy "in repeat_tactic"); try -(* let rec step output_status opened closed = - match opened with - | [] -> output_status, [], closed - | head :: tail -> - let status = S.focus head output_status in - let output_status' = repeat_tactic ~tactic status in - let opened', closed' = S.goals output_status' in - let output_status'', opened'', closed'' = - step output_status' tail [] - in - output_status'', opened' @ opened'', closed' @ closed'' - in *) let output_status = S.apply_tactic tactic status in let opened, closed = S.goals output_status in let output_status, opened', closed' = @@ -279,16 +224,6 @@ struct try let output_status = S.apply_tactic tactic status in let opened, closed = S.goals output_status in -(* let rec step output_status goallist = - match goallist with - [] -> output_status, [] - | head::tail -> - let status = S.focus head output_status 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, opened', closed' = step (do_tactic ~n:(n-1) ~tactic) output_status opened closed in -- 2.39.2