more informative errors for 'proof' and 'apply' steps;
more Seq.result operations;
--- a/src/Pure/General/seq.ML Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/General/seq.ML Tue Oct 16 15:14:12 2012 +0200
@@ -36,9 +36,12 @@
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
@@ -205,6 +208,9 @@
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
@@ -216,17 +222,19 @@
fun map_result f = maps_result (single o f);
(*first result or first error within sequence*)
-fun the_result default_msg seq =
+fun first_result default_msg seq =
let
fun result opt_msg xq =
(case (opt_msg, pull xq) of
- (_, SOME (Result x, _)) => x
+ (_, 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*)
--- a/src/Pure/Isar/isar_syn.ML Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Oct 16 15:14:12 2012 +0200
@@ -681,24 +681,25 @@
val _ =
Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
- (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
+ (Scan.option Parse.nat >> (fn n =>
+ (Toplevel.print o Toplevel.proofs (Seq.make_results o 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.proofs (Seq.make_results o 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)));
@@ -709,12 +710,12 @@
val _ =
Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
- (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
+ (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.also_cmd args)));
val _ =
Outer_Syntax.command @{command_spec "finally"}
"combine calculation and current facts, exhibit result"
- (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
+ (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.finally_cmd args)));
val _ =
Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
--- a/src/Pure/Isar/proof.ML Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/proof.ML Tue Oct 16 15:14:12 2012 +0200
@@ -77,10 +77,13 @@
val begin_notepad: context -> state
val end_notepad: state -> context
val proof: Method.text option -> state -> state Seq.seq
+ val proof_results: Method.text option -> state -> state Seq.result Seq.seq
val defer: int option -> state -> state Seq.seq
val prefer: int -> state -> state Seq.seq
val apply: Method.text -> state -> state Seq.seq
val apply_end: Method.text -> state -> state Seq.seq
+ val apply_results: Method.text -> state -> state Seq.result Seq.seq
+ val apply_end_results: Method.text -> 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) ->
@@ -529,8 +532,8 @@
SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
| NONE => Markup.empty);
-fun method_error name state =
- Seq.single (Proof_Display.method_error name (raw_goal state));
+fun method_error kind state =
+ Seq.single (Proof_Display.method_error kind (raw_goal state));
@@ -808,6 +811,9 @@
#> refine (the_default Method.default_text opt_text)
#> Seq.map (using_facts [] #> enter_forward);
+fun proof_results opt_text =
+ Seq.APPEND (proof opt_text #> Seq.make_results, method_error "initial");
+
fun end_proof bot txt =
Seq.APPEND (fn state =>
state
@@ -818,7 +824,7 @@
|> using_facts []
|> `before_qed |-> (refine o the_default Method.succeed_text)
|> Seq.maps (refine (Method.finish_text txt))
- |> Seq.map Seq.Result, method_error "terminal")
+ |> Seq.make_results, method_error "terminal")
#> Seq.maps_results (Seq.single o finished_goal);
fun check_result msg sq =
@@ -835,6 +841,9 @@
fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
fun apply_end text = assert_forward #> refine_end text;
+fun apply_results text = Seq.APPEND (apply text #> Seq.make_results, method_error "");
+fun apply_end_results text = Seq.APPEND (apply_end text #> Seq.make_results, method_error "");
+
(** goals **)
@@ -970,8 +979,8 @@
(* concluding steps *)
fun terminal_proof qeds initial terminal =
- Seq.APPEND (proof (SOME initial) #> Seq.map Seq.Result, method_error "initial")
- #> Seq.maps_results (qeds terminal) #> Seq.the_result "";
+ 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);
--- a/src/Pure/Isar/proof_display.ML Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/proof_display.ML Tue Oct 16 15:14:12 2012 +0200
@@ -111,9 +111,9 @@
(* method_error *)
-fun method_error name {context = ctxt, facts, goal} = Seq.Error (fn () =>
+fun method_error kind {context = ctxt, facts, goal} = Seq.Error (fn () =>
let
- val pr_header = "Failure of " ^ (if name = "" then "" else name ^ " ") ^ "proof method:\n";
+ val pr_header = "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^ "proof method:\n";
val pr_facts =
if null facts then ""
else
--- a/src/Pure/Isar/proof_node.ML Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/proof_node.ML Tue Oct 16 15:14:12 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;
--- a/src/Pure/Isar/toplevel.ML Tue Oct 16 15:02:49 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Oct 16 15:14:12 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;