# HG changeset patch # User wenzelm # Date 1350419914 -7200 # Node ID 9db36f881137b654282f6027d432bba591dec6ba # Parent a6ebdaf8e2679977cfee762923330849be3c09f4# Parent 2b82358694e62d1bff926befd37928e721ee6d95 merged diff -r a6ebdaf8e267 -r 9db36f881137 NEWS --- a/NEWS Tue Oct 16 20:31:08 2012 +0200 +++ b/NEWS Tue Oct 16 22:38:34 2012 +0200 @@ -41,6 +41,9 @@ specifications: nesting of "context fixes ... context assumes ..." and "class ... context ...". +* More informative error messages for Isar proof commands involving +lazy enumerations (method applications etc.). + *** Pure *** @@ -201,6 +204,10 @@ *** ML *** +* Type Seq.results and related operations support embedded error +messages within lazy enumerations, and thus allow to provide +informative errors in the absence of any usable results. + * Renamed Position.str_of to Position.here to emphasize that this is a formal device to inline positions into message text, but not necessarily printing visible text. diff -r a6ebdaf8e267 -r 9db36f881137 src/Doc/IsarImplementation/Integration.thy --- a/src/Doc/IsarImplementation/Integration.thy Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Doc/IsarImplementation/Integration.thy Tue Oct 16 22:38:34 2012 +0200 @@ -154,7 +154,7 @@ Toplevel.transition -> Toplevel.transition"} \\ @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> Toplevel.transition -> Toplevel.transition"} \\ - @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) -> + @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> Toplevel.transition -> Toplevel.transition"} \\ @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> Toplevel.transition -> Toplevel.transition"} \\ diff -r a6ebdaf8e267 -r 9db36f881137 src/HOL/BNF/Tools/bnf_tactics.ML --- a/src/HOL/BNF/Tools/bnf_tactics.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Tue Oct 16 22:38:34 2012 +0200 @@ -10,7 +10,6 @@ sig val ss_only: thm list -> simpset - val prefer_tac: int -> tactic val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic val fo_rtac: thm -> Proof.context -> int -> tactic val unfold_thms_tac: Proof.context -> thm list -> tactic @@ -39,9 +38,6 @@ fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms; -(* FIXME: why not in "Pure"? *) -fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1); - fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); diff -r a6ebdaf8e267 -r 9db36f881137 src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Tue Oct 16 22:38:34 2012 +0200 @@ -318,7 +318,7 @@ Args.$$$ "narrow" |-- timeout "step_timeout" quick_timeout -- timeout "final_timeout" default_timeout >> boogie_narrow_vc) -- vc_name -- Method.parse >> - (fn ((f, vc_name), meth) => f vc_name meth) + (fn ((f, vc_name), (meth, _)) => f vc_name meth) val status_vc = (scan_arg diff -r a6ebdaf8e267 -r 9db36f881137 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/HOL/Statespace/state_space.ML Tue Oct 16 22:38:34 2012 +0200 @@ -146,7 +146,7 @@ thy |> Expression.sublocale_cmd I (name, Position.none) (expression_no_pos expr) [] |> Proof.global_terminal_proof - (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE) + ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.none), NONE) |> Proof_Context.theory_of fun add_locale name expr elems thy = diff -r a6ebdaf8e267 -r 9db36f881137 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/HOL/Tools/try0.ML Tue Oct 16 22:38:34 2012 +0200 @@ -55,7 +55,7 @@ #> Outer_Syntax.scan Position.start #> filter Token.is_proper #> Scan.read Token.stopper Method.parse - #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source") + #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source") fun apply_named_method_on_first_goal method thy = method |> parse_method diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/General/seq.ML --- a/src/Pure/General/seq.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/General/seq.ML Tue Oct 16 22:38:34 2012 +0200 @@ -35,6 +35,14 @@ val singleton: ('a list -> 'b list seq) -> 'a -> 'b seq val print: (int -> 'a -> unit) -> int -> 'a seq -> unit val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq + datatype 'a result = Result of 'a | Error of unit -> string + val make_results: 'a seq -> 'a result seq + val filter_results: 'a result seq -> 'a seq + val maps_results: ('a -> 'b result seq) -> 'a result seq -> 'b result seq + val maps_result: ('a -> 'b seq) -> 'a result seq -> 'b result seq + val map_result: ('a -> 'b) -> 'a result seq -> 'b result seq + val first_result: string -> 'a result seq -> 'a * 'a seq + val the_result: string -> 'a result seq -> 'a val succeed: 'a -> 'a seq val fail: 'a -> 'b seq val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq @@ -110,7 +118,7 @@ fun of_list xs = fold_rev cons xs empty; -(*sequence append: put the elements of xq in front of those of yq*) +(*sequence append: put the elements of xq in front of those of yq*) fun append xq yq = let fun copy s = @@ -161,7 +169,12 @@ NONE => NONE | SOME (x, xq') => SOME (f x, map f xq'))); -fun maps f = flat o map f; +fun maps f xq = + make (fn () => + (case pull xq of + NONE => NONE + | SOME (x, xq') => pull (append (f x) (maps f xq')))); + fun map_filter f = maps (fn x => (case f x of NONE => empty | SOME y => single y)); fun lift f xq y = map (fn x => f x y) xq; @@ -191,6 +204,38 @@ in its xq end; +(* embedded errors *) + +datatype 'a result = Result of 'a | Error of unit -> string; + +fun make_results xq = map Result xq; +fun filter_results xq = map_filter (fn Result x => SOME x | Error _ => NONE) xq; + +fun maps_results f xq = + make (fn () => + (case pull xq of + NONE => NONE + | SOME (Result x, xq') => pull (append (f x) (maps_results f xq')) + | SOME (Error msg, xq') => SOME (Error msg, maps_results f xq'))); + +fun maps_result f = maps_results (map Result o f); +fun map_result f = maps_result (single o f); + +(*first result or first error within sequence*) +fun first_result default_msg seq = + let + fun result opt_msg xq = + (case (opt_msg, pull xq) of + (_, SOME (Result x, xq')) => (x, filter_results xq') + | (SOME _, SOME (Error _, xq')) => result opt_msg xq' + | (NONE, SOME (Error msg, xq')) => result (SOME msg) xq' + | (SOME msg, NONE) => error (msg ()) + | (NONE, NONE) => error (if default_msg = "" then "Empty result sequence" else default_msg)); + in result NONE seq end; + +fun the_result default_msg seq = #1 (first_result default_msg seq); + + (** sequence functions **) (*cf. Pure/tactical.ML*) diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/Isar/calculation.ML Tue Oct 16 22:38:34 2012 +0200 @@ -13,12 +13,12 @@ val sym_add: attribute val sym_del: attribute val symmetric: attribute - val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq + val also: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq val also_cmd: (Facts.ref * Attrib.src list) list option -> - bool -> Proof.state -> Proof.state Seq.seq - val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq + bool -> Proof.state -> Proof.state Seq.result Seq.seq + val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool -> - Proof.state -> Proof.state Seq.seq + Proof.state -> Proof.state Seq.result Seq.seq val moreover: bool -> Proof.state -> Proof.state val ultimately: bool -> Proof.state -> Proof.state end; @@ -129,32 +129,48 @@ fun calculate prep_rules final raw_rules int state = let val ctxt = Proof.context_of state; + val pretty_thm = Display.pretty_thm ctxt; val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl); - fun projection ths th = exists (curry eq_prop th) ths; + fun check_projection ths th = + (case find_index (curry eq_prop th) ths of + ~1 => Seq.Result [th] + | i => + Seq.Error (fn () => + (Pretty.string_of o Pretty.chunks) + [Pretty.block [Pretty.str "Vacuous calculation result:", Pretty.brk 1, pretty_thm th], + (Pretty.block o Pretty.fbreaks) + (Pretty.str ("derived as projection (" ^ string_of_int (i + 1) ^ ") from:") :: + map pretty_thm ths)])); val opt_rules = Option.map (prep_rules ctxt) raw_rules; fun combine ths = - (case opt_rules of SOME rules => rules - | NONE => - (case ths of - [] => Item_Net.content (#1 (get_rules ctxt)) - | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th))) - |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths) - |> Seq.filter (not o projection ths); + Seq.append + ((case opt_rules of + SOME rules => rules + | NONE => + (case ths of + [] => Item_Net.content (#1 (get_rules ctxt)) + | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th))) + |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths) + |> Seq.map (check_projection ths)) + (Seq.single (Seq.Error (fn () => + (Pretty.string_of o Pretty.block o Pretty.fbreaks) + (Pretty.str "No matching trans rules for calculation:" :: + map pretty_thm ths)))); val facts = Proof.the_facts (assert_sane final state); val (initial, calculations) = (case get_calculation state of - NONE => (true, Seq.single facts) - | SOME calc => (false, Seq.map single (combine (calc @ facts)))); + NONE => (true, Seq.single (Seq.Result facts)) + | SOME calc => (false, combine (calc @ facts))); val _ = initial andalso final andalso error "No calculation yet"; val _ = initial andalso is_some opt_rules andalso error "Initial calculation -- no rules to be given"; in - calculations |> Seq.map (fn calc => maintain_calculation int final calc state) + calculations |> Seq.map_result (fn calc => maintain_calculation int final calc state) end; val also = calculate (K I) false; diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Tue Oct 16 22:38:34 2012 +0200 @@ -30,8 +30,8 @@ val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state - val qed: Method.text option -> Toplevel.transition -> Toplevel.transition - val terminal_proof: Method.text * Method.text option -> + val qed: Method.text_position option -> Toplevel.transition -> Toplevel.transition + val terminal_proof: Method.text_position * Method.text_position option -> Toplevel.transition -> Toplevel.transition val default_proof: Toplevel.transition -> Toplevel.transition val immediate_proof: Toplevel.transition -> Toplevel.transition diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Oct 16 22:38:34 2012 +0200 @@ -681,24 +681,24 @@ val _ = Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state" - (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer))); + (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n))); val _ = Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state" - (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer))); + (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n))); val _ = Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)" - (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply))); + (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results))); val _ = Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement (unstructured)" - (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end))); + (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results))); val _ = Outer_Syntax.command @{command_spec "proof"} "backward proof" (Scan.option Method.parse >> (fn m => Toplevel.print o - Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o + Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o Toplevel.skip_proof (fn i => i + 1))); diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/Isar/method.ML Tue Oct 16 22:38:34 2012 +0200 @@ -20,8 +20,6 @@ val SIMPLE_METHOD: tactic -> method val SIMPLE_METHOD': (int -> tactic) -> method val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method - val defer: int option -> method - val prefer: int -> method val cheating: bool -> Proof.context -> method val intro: thm list -> method val elim: thm list -> method @@ -75,7 +73,10 @@ type modifier = (Proof.context -> Proof.context) * attribute val section: modifier parser list -> thm list context_parser val sections: modifier parser list -> thm list list context_parser - val parse: text parser + type text_position = text * Position.T + val parse: text_position parser + val text: text_position option -> text option + val position: text_position option -> Position.T end; structure Method: METHOD = @@ -124,12 +125,6 @@ end; -(* shuffle subgoals *) - -fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1))); -fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i))); - - (* cheating *) fun cheating int ctxt = @@ -419,7 +414,23 @@ and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x; -in val parse = meth3 end; +in + +val parse = + Scan.trace meth3 >> (fn (m, toks) => (m, Position.set_range (Token.position_range_of toks))); + +end; + + +(* text position *) + +type text_position = text * Position.T; + +fun text NONE = NONE + | text (SOME (txt, _)) = SOME txt; + +fun position NONE = Position.none + | position (SOME (_, pos)) = pos; (* theory setup *) diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/Isar/proof.ML Tue Oct 16 22:38:34 2012 +0200 @@ -77,27 +77,30 @@ val begin_notepad: context -> state val end_notepad: state -> context val proof: Method.text option -> state -> state Seq.seq - val defer: int option -> state -> state Seq.seq - val prefer: int -> state -> state Seq.seq + val proof_results: Method.text_position option -> state -> state Seq.result Seq.seq + val defer: int -> state -> state + val prefer: int -> state -> state val apply: Method.text -> state -> state Seq.seq val apply_end: Method.text -> state -> state Seq.seq + val apply_results: Method.text_position -> state -> state Seq.result Seq.seq + val apply_end_results: Method.text_position -> state -> state Seq.result Seq.seq val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) -> (context -> 'a -> attribute) -> ('b list -> context -> (term list list * (context -> context)) * context) -> string -> Method.text option -> (thm list list -> state -> state) -> ((binding * 'a list) * 'b) list -> state -> state - val local_qed: Method.text option * bool -> state -> state + val local_qed: Method.text_position option * bool -> state -> state val theorem: Method.text option -> (thm list list -> context -> context) -> (term * term list) list list -> context -> state val theorem_cmd: Method.text option -> (thm list list -> context -> context) -> (string * string list) list list -> context -> state - val global_qed: Method.text option * bool -> state -> context - val local_terminal_proof: Method.text * Method.text option -> state -> state + val global_qed: Method.text_position option * bool -> state -> context + val local_terminal_proof: Method.text_position * Method.text_position option -> state -> state val local_default_proof: state -> state val local_immediate_proof: state -> state val local_skip_proof: bool -> state -> state val local_done_proof: state -> state - val global_terminal_proof: Method.text * Method.text option -> state -> context + val global_terminal_proof: Method.text_position * Method.text_position option -> state -> context val global_default_proof: state -> context val global_immediate_proof: state -> context val global_skip_proof: bool -> state -> context @@ -113,8 +116,10 @@ val schematic_goal: state -> bool val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context - val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state - val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context + val local_future_terminal_proof: Method.text_position * Method.text_position option -> bool -> + state -> state + val global_future_terminal_proof: Method.text_position * Method.text_position option -> bool -> + state -> context end; structure Proof: PROOF = @@ -333,32 +338,20 @@ fun pretty_facts _ _ NONE = [] | pretty_facts s ctxt (SOME ths) = - [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""]; + [(Pretty.block o Pretty.fbreaks) + (Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"] :: + map (Display.pretty_thm ctxt) ths), Pretty.str ""]; fun pretty_state nr state = let val {context = ctxt, facts, mode, goal = _} = top state; val verbose = Config.get ctxt Proof_Context.verbose; - fun levels_up 0 = "" - | levels_up 1 = "1 level up" - | levels_up i = string_of_int i ^ " levels up"; - - fun subgoals 0 = "" - | subgoals 1 = "1 subgoal" - | subgoals n = string_of_int n ^ " subgoals"; - - fun description strs = - (case filter_out (fn s => s = "") strs of [] => "" - | strs' => enclose " (" ")" (commas strs')); - - fun prt_goal (SOME (_, (i, + fun prt_goal (SOME (_, (_, {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) = pretty_facts "using " ctxt (if mode <> Backward orelse null using then NONE else SOME using) @ - [Pretty.str ("goal" ^ - description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ - Goal_Display.pretty_goals ctxt goal @ + [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @ (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages)) | prt_goal NONE = []; @@ -487,8 +480,7 @@ val string_of_term = Syntax.string_of_term ctxt; val string_of_thm = Display.string_of_thm ctxt; - val _ = Thm.no_prems goal orelse - error (Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt goal)); + val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal); val extra_hyps = Assumption.extra_hyps ctxt goal; val _ = null extra_hyps orelse @@ -514,20 +506,13 @@ | recover_result _ _ = lost_structure (); in recover_result propss results end; -fun the_finished_goal results = - (case Seq.pull results of - SOME ((f1, state1), rest) => - let val (ctxt1, (_, goal1)) = get_goal state1 in - if Thm.no_prems goal1 then f1 state1 - else - (case Seq.pull (Seq.filter (Thm.no_prems o #2 o #2 o get_goal o #2) rest) of - SOME ((f, state), _) => f state - | NONE => - error ("Failed to finish proof:\n" ^ - Pretty.string_of - (Goal_Display.pretty_goal {main = true, limit = false} ctxt1 goal1))) - end - | NONE => error "Failed to finish proof"); +val finished_goal_error = "Failed to finish proof"; + +fun finished_goal state = + let val (ctxt, (_, goal)) = get_goal state in + if Thm.no_prems goal then Seq.Result state + else Seq.Error (fn () => finished_goal_error ^ ":\n" ^ Proof_Display.string_of_goal ctxt goal) + end; (* goal views -- corresponding to methods *) @@ -549,6 +534,9 @@ SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal) | NONE => Markup.empty); +fun method_error kind pos state = + Seq.single (Proof_Display.method_error kind pos (raw_goal state)); + (*** structured proof commands ***) @@ -825,15 +813,22 @@ #> refine (the_default Method.default_text opt_text) #> Seq.map (using_facts [] #> enter_forward); -fun end_proof bot txt state = - state - |> assert_forward - |> assert_bottom bot - |> close_block - |> assert_current_goal true - |> using_facts [] - |> `before_qed |-> (refine o the_default Method.succeed_text) - |> Seq.maps (refine (Method.finish_text txt)); +fun proof_results arg = + Seq.APPEND (proof (Method.text arg) #> Seq.make_results, + method_error "initial" (Method.position arg)); + +fun end_proof bot (arg, immed) = + Seq.APPEND (fn state => + state + |> assert_forward + |> assert_bottom bot + |> close_block + |> assert_current_goal true + |> using_facts [] + |> `before_qed |-> (refine o the_default Method.succeed_text) + |> Seq.maps (refine (Method.finish_text (Method.text arg, immed))) + |> Seq.make_results, method_error "terminal" (Method.position arg)) + #> Seq.maps_results (Seq.single o finished_goal); fun check_result msg sq = (case Seq.pull sq of @@ -843,12 +838,24 @@ (* unstructured refinement *) -fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i))); -fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i))); +fun defer i = + assert_no_chain #> + refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd; + +fun prefer i = + assert_no_chain #> + refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd; fun apply text = assert_backward #> refine text #> Seq.map (using_facts []); + fun apply_end text = assert_forward #> refine_end text; +fun apply_results (text, pos) = + Seq.APPEND (apply text #> Seq.make_results, method_error "" pos); + +fun apply_end_results (text, pos) = + Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos); + (** goals **) @@ -952,12 +959,12 @@ |> tap (Variable.warn_extra_tfrees (context_of state) o context_of) end; -fun local_qeds txt = - end_proof false txt - #> Seq.map (pair (generic_qed Proof_Context.auto_bind_facts #-> - (fn ((after_qed, _), results) => after_qed results))); +fun local_qeds arg = + end_proof false arg + #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #-> + (fn ((after_qed, _), results) => after_qed results)); -fun local_qed txt = local_qeds txt #> the_finished_goal; +fun local_qed arg = local_qeds arg #> Seq.the_result finished_goal_error; (* global goals *) @@ -973,51 +980,31 @@ val theorem = global_goal Proof_Context.bind_propp_schematic_i; val theorem_cmd = global_goal Proof_Context.bind_propp_schematic; -fun global_qeds txt = - end_proof true txt - #> Seq.map (pair (generic_qed (K I) #> (fn (((_, after_qed), results), state) => - after_qed results (context_of state)))); +fun global_qeds arg = + end_proof true arg + #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) => + after_qed results (context_of state))); -fun global_qed txt = global_qeds txt #> the_finished_goal; +fun global_qed arg = global_qeds arg #> Seq.the_result finished_goal_error; (* concluding steps *) -local - -fun failure_initial state = - let - val (ctxt, (facts, goal)) = get_goal state; - val pr_facts = - if null facts then "" - else Pretty.string_of (Pretty.big_list "facts:" (map (Display.pretty_thm ctxt) facts)) ^ "\n"; - val pr_goal = - "goal:\n" ^ Pretty.string_of (Goal_Display.pretty_goal {main = false, limit = false} ctxt goal); - in error ("Failure of initial proof method on goal state:\n" ^ pr_facts ^ pr_goal) end; - -fun failure_terminal _ = error "Failure of terminal proof method"; - -val op ORELSE = Seq.ORELSE; - fun terminal_proof qeds initial terminal = - (((proof (SOME initial) ORELSE failure_initial) - #> Seq.maps (qeds terminal)) ORELSE failure_terminal) #> the_finished_goal; - -in + proof_results (SOME initial) #> Seq.maps_results (qeds terminal) + #> Seq.the_result ""; fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true); -val local_default_proof = local_terminal_proof (Method.default_text, NONE); -val local_immediate_proof = local_terminal_proof (Method.this_text, NONE); -fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE); -val local_done_proof = terminal_proof local_qeds Method.done_text (NONE, false); +val local_default_proof = local_terminal_proof ((Method.default_text, Position.none), NONE); +val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.none), NONE); +fun local_skip_proof int = local_terminal_proof ((Method.sorry_text int, Position.none), NONE); +val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.none) (NONE, false); fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true); -val global_default_proof = global_terminal_proof (Method.default_text, NONE); -val global_immediate_proof = global_terminal_proof (Method.this_text, NONE); -fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE); -val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false); - -end; +val global_default_proof = global_terminal_proof ((Method.default_text, Position.none), NONE); +val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.none), NONE); +fun global_skip_proof int = global_terminal_proof ((Method.sorry_text int, Position.none), NONE); +val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.none) (NONE, false); (* common goal statements *) diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/Isar/proof_display.ML Tue Oct 16 22:38:34 2012 +0200 @@ -17,6 +17,10 @@ val pretty_full_theory: bool -> theory -> Pretty.T val print_theory: theory -> unit val string_of_rule: Proof.context -> string -> thm -> string + val pretty_goal_header: thm -> Pretty.T + val string_of_goal: Proof.context -> thm -> string + val method_error: string -> Position.T -> + {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result val print_results: Markup.T -> bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit @@ -86,6 +90,43 @@ val string_of_rule = Pretty.string_of ooo pretty_rule; +(* goals *) + +local + +fun subgoals 0 = [] + | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"] + | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")]; + +in + +fun pretty_goal_header goal = + Pretty.block ([Pretty.command "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]); + +end; + +fun string_of_goal ctxt goal = + Pretty.string_of (Pretty.chunks + [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]); + + +(* method_error *) + +fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () => + let + val pr_header = + "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^ + "proof method" ^ Position.here pos ^ ":\n"; + val pr_facts = + if null facts then "" + else + (Pretty.string_of o Pretty.block o Pretty.fbreaks) + (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] :: + map (Display.pretty_thm ctxt) facts) ^ "\n"; + val pr_goal = string_of_goal ctxt goal; + in pr_header ^ pr_facts ^ pr_goal end); + + (* results *) local diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/proof_node.ML --- a/src/Pure/Isar/proof_node.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/Isar/proof_node.ML Tue Oct 16 22:38:34 2012 +0200 @@ -11,7 +11,7 @@ val current: T -> Proof.state val position: T -> int val back: T -> T - val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T + val applys: (Proof.state -> Proof.state Seq.result Seq.seq) -> T -> T val apply: (Proof.state -> Proof.state) -> T -> T end; @@ -42,10 +42,8 @@ (* apply transformer *) fun applys f (Proof_Node ((st, _), n)) = - (case Seq.pull (f st) of - NONE => error "empty result sequence -- proof command failed" - | SOME res => Proof_Node (res, n + 1)); + Proof_Node (Seq.first_result "Empty result sequence -- proof command failed" (f st), n + 1); -fun apply f = applys (Seq.single o f); +fun apply f = applys (Seq.single o Seq.Result o f); end; diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/Isar/token.ML Tue Oct 16 22:38:34 2012 +0200 @@ -18,6 +18,7 @@ val str_of_kind: kind -> string val position_of: T -> Position.T val end_position_of: T -> Position.T + val position_range_of: T list -> Position.range val pos_of: T -> string val eof: T val is_eof: T -> bool @@ -130,6 +131,9 @@ fun position_of (Token ((_, (pos, _)), _, _)) = pos; fun end_position_of (Token ((_, (_, pos)), _, _)) = pos; +fun position_range_of [] = Position.no_range + | position_range_of toks = (position_of (hd toks), end_position_of (List.last toks)); + val pos_of = Position.here o position_of; diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/Isar/toplevel.ML Tue Oct 16 22:38:34 2012 +0200 @@ -74,9 +74,9 @@ val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition val forget_proof: transition -> transition val present_proof: (state -> unit) -> transition -> transition - val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition + val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition - val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition + val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof: (Proof.state -> Proof.state) -> transition -> transition val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition val skip_proof: (int -> int) -> transition -> transition @@ -556,7 +556,7 @@ | skip as SkipProof _ => skip | _ => raise UNDEF)); -fun proof' f = proofs' (Seq.single oo f); +fun proof' f = proofs' ((Seq.single o Seq.Result) oo f); val proofs = proofs' o K; val proof = proof' o K; diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/PIDE/command.ML Tue Oct 16 22:38:34 2012 +0200 @@ -22,14 +22,8 @@ (* span range *) -fun range [] = (Position.none, Position.none) - | range toks = - let - val start_pos = Token.position_of (hd toks); - val end_pos = Token.end_position_of (List.last toks); - in (start_pos, end_pos) end; - -val proper_range = range o #1 o take_suffix Token.is_space; +val range = Token.position_range_of; +val proper_range = Token.position_range_of o #1 o take_suffix Token.is_space; (* memo results *) diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/ROOT.ML Tue Oct 16 22:38:34 2012 +0200 @@ -305,17 +305,6 @@ use "ProofGeneral/proof_general_emacs.ML"; -(* the Pure theory *) - -use "pure_syn.ML"; -Thy_Info.use_thy ("Pure", Position.none); -Context.set_thread_data NONE; -structure Pure = struct val thy = Thy_Info.get_theory "Pure" end; - - -use "ProofGeneral/pgip_tests.ML"; - - (* ML toplevel pretty printing *) toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"\")"; @@ -326,7 +315,6 @@ toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm"; toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm"; toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp"; -toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy"; toplevel_pp ["Context", "theory"] "Context.pretty_thy"; toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; @@ -339,6 +327,18 @@ if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else (); +(* the Pure theory *) + +use "pure_syn.ML"; +Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none)); +Context.set_thread_data NONE; +structure Pure = struct val thy = Thy_Info.get_theory "Pure" end; + +toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy"; + +use "ProofGeneral/pgip_tests.ML"; + + (* ML toplevel commands *) fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name)); diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/logic.ML --- a/src/Pure/logic.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/logic.ML Tue Oct 16 22:38:34 2012 +0200 @@ -557,8 +557,10 @@ (* goal states *) -fun get_goal st i = nth_prem (i, st) - handle TERM _ => error "Goal number out of range"; +fun get_goal st i = + nth_prem (i, st) handle TERM _ => + error ("Subgoal number " ^ string_of_int i ^ " out of range (a total of " ^ + string_of_int (count_prems st) ^ " subgoals)"); (*reverses parameters for substitution*) fun goal_params st i = diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/tactic.ML Tue Oct 16 22:38:34 2012 +0200 @@ -53,6 +53,7 @@ val rename_tac: string list -> int -> tactic val rotate_tac: int -> int -> tactic val defer_tac: int -> tactic + val prefer_tac: int -> tactic val filter_prems_tac: (term -> bool) -> int -> tactic end; @@ -318,6 +319,9 @@ (*Rotates the given subgoal to be the last.*) fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1); +(*Rotates the given subgoal to be the first.*) +fun prefer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1 #> Thm.permute_prems 0 ~1); + (* remove premises that do not satisfy p; fails if all prems satisfy p *) fun filter_prems_tac p = let fun Then NONE tac = SOME tac diff -r a6ebdaf8e267 -r 9db36f881137 src/Pure/tactical.ML --- a/src/Pure/tactical.ML Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Pure/tactical.ML Tue Oct 16 22:38:34 2012 +0200 @@ -55,6 +55,7 @@ val TRYALL: (int -> tactic) -> tactic val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic val SUBGOAL: ((term * int) -> tactic) -> int -> tactic + val ASSERT_SUBGOAL: (int -> tactic) -> int -> tactic val CHANGED_GOAL: (int -> tactic) -> int -> tactic val SOLVED': (int -> tactic) -> int -> tactic val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic @@ -328,6 +329,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); + (*Returns all states that have changed in subgoal i, counted from the LAST subgoal. For stac, for example.*) fun CHANGED_GOAL tac i st = diff -r a6ebdaf8e267 -r 9db36f881137 src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Tue Oct 16 20:31:08 2012 +0200 +++ b/src/Tools/jEdit/src/info_dockable.scala Tue Oct 16 22:38:34 2012 +0200 @@ -16,7 +16,7 @@ import java.lang.System import java.awt.BorderLayout -import java.awt.event.{ComponentEvent, ComponentAdapter} +import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent} import org.gjt.sp.jedit.View @@ -28,17 +28,20 @@ private var implicit_snapshot = Document.State.init.snapshot() private var implicit_info: XML.Body = Nil - def apply(view: View, snapshot: Document.Snapshot, info: XML.Body) + private def set_implicit(snapshot: Document.Snapshot, info: XML.Body) { Swing_Thread.require() implicit_snapshot = snapshot implicit_info = info + } - view.getDockableWindowManager.floatDockableWindow("isabelle-info") + private def reset_implicit(): Unit = set_implicit(Document.State.init.snapshot(), Nil) - implicit_snapshot = Document.State.init.snapshot() - implicit_info = Nil + def apply(view: View, snapshot: Document.Snapshot, info: XML.Body) + { + set_implicit(snapshot, info) + view.getDockableWindowManager.floatDockableWindow("isabelle-info") } } @@ -52,13 +55,22 @@ private var zoom_factor = 100 + private val snapshot = Info_Dockable.implicit_snapshot + private val info = Info_Dockable.implicit_info + + private val window_focus_listener = + new WindowFocusListener { + def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, info) } + def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() } + } + /* pretty text area */ private val pretty_text_area = new Pretty_Text_Area(view) set_content(pretty_text_area) - pretty_text_area.update(Info_Dockable.implicit_snapshot, Info_Dockable.implicit_info) + pretty_text_area.update(snapshot, info) private def handle_resize() { @@ -85,6 +97,7 @@ { Swing_Thread.require() + JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener)) Isabelle.session.global_options += main_actor handle_resize() } @@ -93,6 +106,7 @@ { Swing_Thread.require() + JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener)) Isabelle.session.global_options -= main_actor delay_resize.revoke() }