--- a/src/Pure/tactical.ML Sat Aug 15 22:47:03 2015 +0200
+++ b/src/Pure/tactical.ML Sat Aug 15 23:10:13 2015 +0200
@@ -88,9 +88,9 @@
Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
Does not backtrack to tac2 if tac1 was initially chosen. *)
fun (tac1 ORELSE tac2) st =
- case Seq.pull(tac1 st) of
- NONE => tac2 st
- | sequencecell => Seq.make(fn()=> sequencecell);
+ (case Seq.pull (tac1 st) of
+ NONE => tac2 st
+ | some => Seq.make (fn () => some));
(*The tactical APPEND combines the results of two tactics.
@@ -104,9 +104,9 @@
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac)
*)
fun (tac THEN_ELSE (tac1, tac2)) st =
- case Seq.pull(tac st) of
- NONE => tac2 st (*failed; try tactic 2*)
- | seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*)
+ (case Seq.pull (tac st) of
+ NONE => tac2 st (*failed; try tactic 2*)
+ | some => Seq.maps tac1 (Seq.make (fn () => some))); (*succeeded; use tactic 1*)
(*Versions for combining tactic-valued functions, as in
@@ -127,35 +127,35 @@
(*Conditional tactical: testfun controls which tactic to use next.
Beware: due to eager evaluation, both thentac and elsetac are evaluated.*)
-fun COND testfun thenf elsef = (fn prf =>
- if testfun prf then thenf prf else elsef prf);
+fun COND testfun thenf elsef =
+ (fn st => if testfun st then thenf st else elsef st);
(*Do the tactic or else do nothing*)
fun TRY tac = tac ORELSE all_tac;
+
(*** List-oriented tactics ***)
local
(*This version of EVERY avoids backtracking over repeated states*)
fun EVY (trail, []) st =
- Seq.make (fn()=> SOME(st,
- Seq.make (fn()=> Seq.pull (evyBack trail))))
- | EVY (trail, tac::tacs) st =
- case Seq.pull(tac st) of
- NONE => evyBack trail (*failed: backtrack*)
- | SOME(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
+ Seq.make (fn () => SOME (st, Seq.make (fn () => Seq.pull (evyBack trail))))
+ | EVY (trail, tac :: tacs) st =
+ (case Seq.pull (tac st) of
+ NONE => evyBack trail (*failed: backtrack*)
+ | SOME (st', q) => EVY ((st', q, tacs) :: trail, tacs) st')
and evyBack [] = Seq.empty (*no alternatives*)
- | evyBack ((st',q,tacs)::trail) =
- case Seq.pull q of
- NONE => evyBack trail
- | SOME(st,q') => if Thm.eq_thm (st',st)
- then evyBack ((st',q',tacs)::trail)
- else EVY ((st,q',tacs)::trail, tacs) st
+ | evyBack ((st', q, tacs) :: trail) =
+ (case Seq.pull q of
+ NONE => evyBack trail
+ | SOME (st, q') =>
+ if Thm.eq_thm (st', st)
+ then evyBack ((st', q', tacs) :: trail)
+ else EVY ((st, q', tacs) :: trail, tacs) st);
in
-
-(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *)
-fun EVERY tacs = EVY ([], tacs);
+ (* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *)
+ fun EVERY tacs = EVY ([], tacs);
end;
@@ -188,9 +188,9 @@
(*Pause until a line is typed -- if non-empty then fail. *)
fun pause_tac st =
- (tracing "** Press RETURN to continue:";
- if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
- else (tracing "Goodbye"; Seq.empty));
+ (tracing "** Press RETURN to continue:";
+ if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
+ else (tracing "Goodbye"; Seq.empty));
exception TRACE_EXIT of thm
and TRACE_QUIT;
@@ -201,21 +201,22 @@
(*Handle all tracing commands for current state and tactic *)
fun exec_trace_command flag (tac, st) =
- case TextIO.inputLine TextIO.stdIn of
- SOME "\n" => tac st
- | SOME "f\n" => Seq.empty
- | SOME "o\n" => (flag := false; tac st)
- | SOME "s\n" => (suppress_tracing := true; tac st)
- | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
- | SOME "quit\n" => raise TRACE_QUIT
- | _ => (tracing
-"Type RETURN to continue or...\n\
-\ f - to fail here\n\
-\ o - to switch tracing off\n\
-\ s - to suppress tracing until next entry to a tactical\n\
-\ x - to exit at this point\n\
-\ quit - to abort this tracing run\n\
-\** Well? " ; exec_trace_command flag (tac, st));
+ (case TextIO.inputLine TextIO.stdIn of
+ SOME "\n" => tac st
+ | SOME "f\n" => Seq.empty
+ | SOME "o\n" => (flag := false; tac st)
+ | SOME "s\n" => (suppress_tracing := true; tac st)
+ | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
+ | SOME "quit\n" => raise TRACE_QUIT
+ | _ =>
+ (tracing
+ "Type RETURN to continue or...\n\
+ \ f - to fail here\n\
+ \ o - to switch tracing off\n\
+ \ s - to suppress tracing until next entry to a tactical\n\
+ \ x - to exit at this point\n\
+ \ quit - to abort this tracing run\n\
+ \** Well? "; exec_trace_command flag (tac, st)));
(*Extract from a tactic, a thm->thm seq function that handles tracing*)
@@ -229,38 +230,40 @@
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
fun traced_tac seqf st =
- (suppress_tracing := false;
- Seq.make (fn()=> seqf st
- handle TRACE_EXIT st' => SOME(st', Seq.empty)));
+ (suppress_tracing := false;
+ Seq.make (fn () => seqf st handle TRACE_EXIT st' => SOME (st', Seq.empty)));
(*Deterministic REPEAT: only retains the first outcome;
uses less space than REPEAT; tail recursive.
If non-negative, n bounds the number of repetitions.*)
fun REPEAT_DETERM_N n tac =
- let val tac = tracify trace_REPEAT tac
- fun drep 0 st = SOME(st, Seq.empty)
- | drep n st =
- (case Seq.pull(tac st) of
- NONE => SOME(st, Seq.empty)
- | SOME(st',_) => drep (n-1) st')
- in traced_tac (drep n) end;
+ let
+ val tac = tracify trace_REPEAT tac;
+ fun drep 0 st = SOME (st, Seq.empty)
+ | drep n st =
+ (case Seq.pull (tac st) of
+ NONE => SOME(st, Seq.empty)
+ | SOME (st', _) => drep (n - 1) st');
+ in traced_tac (drep n) end;
(*Allows any number of repetitions*)
val REPEAT_DETERM = REPEAT_DETERM_N ~1;
(*General REPEAT: maintains a stack of alternatives; tail recursive*)
fun REPEAT tac =
- let val tac = tracify trace_REPEAT tac
- fun rep qs st =
- case Seq.pull(tac st) of
- NONE => SOME(st, Seq.make(fn()=> repq qs))
- | SOME(st',q) => rep (q::qs) st'
- and repq [] = NONE
- | repq(q::qs) = case Seq.pull q of
- NONE => repq qs
- | SOME(st,q) => rep (q::qs) st
- in traced_tac (rep []) end;
+ let
+ val tac = tracify trace_REPEAT tac;
+ fun rep qs st =
+ (case Seq.pull (tac st) of
+ NONE => SOME (st, Seq.make (fn () => repq qs))
+ | SOME (st', q) => rep (q :: qs) st')
+ and repq [] = NONE
+ | repq (q :: qs) =
+ (case Seq.pull q of
+ NONE => repq qs
+ | SOME (st, q) => rep (q :: qs) st);
+ in traced_tac (rep []) end;
(*Repeat 1 or more times*)
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac;
@@ -288,21 +291,23 @@
(*For n subgoals, performs tac(n) THEN ... THEN tac(1)
Essential to work backwards since tac(i) may add/delete subgoals at i. *)
fun ALLGOALS tac st =
- let fun doall 0 = all_tac
- | doall n = tac(n) THEN doall(n-1)
- in doall (Thm.nprems_of st) st end;
+ let
+ fun doall 0 = all_tac
+ | doall n = tac n THEN doall (n - 1);
+ in doall (Thm.nprems_of st) st end;
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *)
fun SOMEGOAL tac st =
- let fun find 0 = no_tac
- | find n = tac(n) ORELSE find(n-1)
- in find (Thm.nprems_of st) st end;
+ let
+ fun find 0 = no_tac
+ | find n = tac n ORELSE find (n - 1);
+ in find (Thm.nprems_of st) st end;
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n).
More appropriate than SOMEGOAL in some cases.*)
fun FIRSTGOAL tac st =
- let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n)
- in find (1, Thm.nprems_of st) st end;
+ let fun find (i, n) = if i > n then no_tac else tac i ORELSE find (i + 1, n)
+ in find (1, Thm.nprems_of st) st end;
(*First subgoal only.*)
fun HEADGOAL tac = tac 1;
@@ -328,7 +333,8 @@
fun SUBGOAL goalfun =
CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i));
-fun ASSERT_SUBGOAL (tac: int -> tactic) i st = (Logic.get_goal (Thm.prop_of st) i; tac i st);
+fun ASSERT_SUBGOAL (tac: int -> tactic) i st =
+ (Logic.get_goal (Thm.prop_of st) i; tac i st);
(*Returns all states that have changed in subgoal i, counted from the LAST
subgoal. For stac, for example.*)