# HG changeset patch # User wenzelm # Date 1439673013 -7200 # Node ID e7c761c63c180e9b33bd8d721ef58a34ff8fe734 # Parent 4c108cce6b3565e21a81c3c90bc7f631a5b3756e tuned whitespace; diff -r 4c108cce6b35 -r e7c761c63c18 src/Pure/tactical.ML --- 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.*)