# HG changeset patch # User wenzelm # Date 1350415596 -7200 # Node ID 3039922ffd8def7f985b2625dc78c4d43475bd25 # Parent d3053a55bfcbbe695fd7ccca9654a5434356adc3 more informative errors for 'also' and 'finally'; diff -r d3053a55bfcb -r 3039922ffd8d src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Tue Oct 16 20:35:24 2012 +0200 +++ b/src/Pure/Isar/calculation.ML Tue Oct 16 21:26:36 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 d3053a55bfcb -r 3039922ffd8d src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Oct 16 20:35:24 2012 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Oct 16 21:26:36 2012 +0200 @@ -709,12 +709,12 @@ val _ = Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts" - (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.also_cmd args))); + (calc_args >> (Toplevel.proofs' o Calculation.also_cmd)); val _ = Outer_Syntax.command @{command_spec "finally"} "combine calculation and current facts, exhibit result" - (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.finally_cmd args))); + (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd)); val _ = Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"