more informative errors for 'proof' and 'apply' steps;
authorwenzelm
Tue Oct 16 15:14:12 2012 +0200 (2012-10-16 ago)
changeset 49863b5fb6e7f8d81
parent 49862 fb2d8ba7d3a9
child 49864 34437e7245cc
more informative errors for 'proof' and 'apply' steps;
more Seq.result operations;
src/Pure/General/seq.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/proof_node.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/General/seq.ML	Tue Oct 16 15:02:49 2012 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Tue Oct 16 15:14:12 2012 +0200
     1.3 @@ -36,9 +36,12 @@
     1.4    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
     1.5    val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
     1.6    datatype 'a result = Result of 'a | Error of unit -> string
     1.7 +  val make_results: 'a seq -> 'a result seq
     1.8 +  val filter_results: 'a result seq -> 'a seq
     1.9    val maps_results: ('a -> 'b result seq) -> 'a result seq -> 'b result seq
    1.10    val maps_result: ('a -> 'b seq) -> 'a result seq -> 'b result seq
    1.11    val map_result: ('a -> 'b) -> 'a result seq -> 'b result seq
    1.12 +  val first_result: string -> 'a result seq -> 'a * 'a seq
    1.13    val the_result: string -> 'a result seq -> 'a
    1.14    val succeed: 'a -> 'a seq
    1.15    val fail: 'a -> 'b seq
    1.16 @@ -205,6 +208,9 @@
    1.17  
    1.18  datatype 'a result = Result of 'a | Error of unit -> string;
    1.19  
    1.20 +fun make_results xq = map Result xq;
    1.21 +fun filter_results xq = map_filter (fn Result x => SOME x | Error _ => NONE) xq;
    1.22 +
    1.23  fun maps_results f xq =
    1.24    make (fn () =>
    1.25      (case pull xq of
    1.26 @@ -216,17 +222,19 @@
    1.27  fun map_result f = maps_result (single o f);
    1.28  
    1.29  (*first result or first error within sequence*)
    1.30 -fun the_result default_msg seq =
    1.31 +fun first_result default_msg seq =
    1.32    let
    1.33      fun result opt_msg xq =
    1.34        (case (opt_msg, pull xq) of
    1.35 -        (_, SOME (Result x, _)) => x
    1.36 +        (_, SOME (Result x, xq')) => (x, filter_results xq')
    1.37        | (SOME _, SOME (Error _, xq')) => result opt_msg xq'
    1.38        | (NONE, SOME (Error msg, xq')) => result (SOME msg) xq'
    1.39        | (SOME msg, NONE) => error (msg ())
    1.40        | (NONE, NONE) => error (if default_msg = "" then "Empty result sequence" else default_msg));
    1.41    in result NONE seq end;
    1.42  
    1.43 +fun the_result default_msg seq = #1 (first_result default_msg seq);
    1.44 +
    1.45  
    1.46  
    1.47  (** sequence functions **)      (*cf. Pure/tactical.ML*)
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 15:02:49 2012 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 15:14:12 2012 +0200
     2.3 @@ -681,24 +681,25 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
     2.7 -    (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
     2.8 +    (Scan.option Parse.nat >> (fn n =>
     2.9 +      (Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.defer n))));
    2.10  
    2.11  val _ =
    2.12    Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
    2.13 -    (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
    2.14 +    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proofs (Seq.make_results o Proof.prefer n)));
    2.15  
    2.16  val _ =
    2.17    Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
    2.18 -    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
    2.19 +    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
    2.20  
    2.21  val _ =
    2.22    Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement (unstructured)"
    2.23 -    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
    2.24 +    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
    2.25  
    2.26  val _ =
    2.27    Outer_Syntax.command @{command_spec "proof"} "backward proof"
    2.28      (Scan.option Method.parse >> (fn m => Toplevel.print o
    2.29 -      Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
    2.30 +      Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
    2.31        Toplevel.skip_proof (fn i => i + 1)));
    2.32  
    2.33  
    2.34 @@ -709,12 +710,12 @@
    2.35  
    2.36  val _ =
    2.37    Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
    2.38 -    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
    2.39 +    (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.also_cmd args)));
    2.40  
    2.41  val _ =
    2.42    Outer_Syntax.command @{command_spec "finally"}
    2.43      "combine calculation and current facts, exhibit result"
    2.44 -    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
    2.45 +    (calc_args >> (fn args => Toplevel.proofs' (Seq.make_results oo Calculation.finally_cmd args)));
    2.46  
    2.47  val _ =
    2.48    Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
     3.1 --- a/src/Pure/Isar/proof.ML	Tue Oct 16 15:02:49 2012 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 16 15:14:12 2012 +0200
     3.3 @@ -77,10 +77,13 @@
     3.4    val begin_notepad: context -> state
     3.5    val end_notepad: state -> context
     3.6    val proof: Method.text option -> state -> state Seq.seq
     3.7 +  val proof_results: Method.text option -> state -> state Seq.result Seq.seq
     3.8    val defer: int option -> state -> state Seq.seq
     3.9    val prefer: int -> state -> state Seq.seq
    3.10    val apply: Method.text -> state -> state Seq.seq
    3.11    val apply_end: Method.text -> state -> state Seq.seq
    3.12 +  val apply_results: Method.text -> state -> state Seq.result Seq.seq
    3.13 +  val apply_end_results: Method.text -> state -> state Seq.result Seq.seq
    3.14    val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
    3.15      (context -> 'a -> attribute) ->
    3.16      ('b list -> context -> (term list list * (context -> context)) * context) ->
    3.17 @@ -529,8 +532,8 @@
    3.18      SOME {goal, ...} => Isabelle_Markup.proof_state (Thm.nprems_of goal)
    3.19    | NONE => Markup.empty);
    3.20  
    3.21 -fun method_error name state =
    3.22 -  Seq.single (Proof_Display.method_error name (raw_goal state));
    3.23 +fun method_error kind state =
    3.24 +  Seq.single (Proof_Display.method_error kind (raw_goal state));
    3.25  
    3.26  
    3.27  
    3.28 @@ -808,6 +811,9 @@
    3.29    #> refine (the_default Method.default_text opt_text)
    3.30    #> Seq.map (using_facts [] #> enter_forward);
    3.31  
    3.32 +fun proof_results opt_text =
    3.33 +  Seq.APPEND (proof opt_text #> Seq.make_results, method_error "initial");
    3.34 +
    3.35  fun end_proof bot txt =
    3.36    Seq.APPEND (fn state =>
    3.37      state
    3.38 @@ -818,7 +824,7 @@
    3.39      |> using_facts []
    3.40      |> `before_qed |-> (refine o the_default Method.succeed_text)
    3.41      |> Seq.maps (refine (Method.finish_text txt))
    3.42 -    |> Seq.map Seq.Result, method_error "terminal")
    3.43 +    |> Seq.make_results, method_error "terminal")
    3.44    #> Seq.maps_results (Seq.single o finished_goal);
    3.45  
    3.46  fun check_result msg sq =
    3.47 @@ -835,6 +841,9 @@
    3.48  fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
    3.49  fun apply_end text = assert_forward #> refine_end text;
    3.50  
    3.51 +fun apply_results text = Seq.APPEND (apply text #> Seq.make_results, method_error "");
    3.52 +fun apply_end_results text = Seq.APPEND (apply_end text #> Seq.make_results, method_error "");
    3.53 +
    3.54  
    3.55  
    3.56  (** goals **)
    3.57 @@ -970,8 +979,8 @@
    3.58  (* concluding steps *)
    3.59  
    3.60  fun terminal_proof qeds initial terminal =
    3.61 -  Seq.APPEND (proof (SOME initial) #> Seq.map Seq.Result, method_error "initial")
    3.62 -  #> Seq.maps_results (qeds terminal) #> Seq.the_result "";
    3.63 +  proof_results (SOME initial) #> Seq.maps_results (qeds terminal)
    3.64 +  #> Seq.the_result "";
    3.65  
    3.66  fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
    3.67  val local_default_proof = local_terminal_proof (Method.default_text, NONE);
     4.1 --- a/src/Pure/Isar/proof_display.ML	Tue Oct 16 15:02:49 2012 +0200
     4.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Oct 16 15:14:12 2012 +0200
     4.3 @@ -111,9 +111,9 @@
     4.4  
     4.5  (* method_error *)
     4.6  
     4.7 -fun method_error name {context = ctxt, facts, goal} = Seq.Error (fn () =>
     4.8 +fun method_error kind {context = ctxt, facts, goal} = Seq.Error (fn () =>
     4.9    let
    4.10 -    val pr_header = "Failure of " ^ (if name = "" then "" else name ^ " ") ^ "proof method:\n";
    4.11 +    val pr_header = "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^ "proof method:\n";
    4.12      val pr_facts =
    4.13        if null facts then ""
    4.14        else
     5.1 --- a/src/Pure/Isar/proof_node.ML	Tue Oct 16 15:02:49 2012 +0200
     5.2 +++ b/src/Pure/Isar/proof_node.ML	Tue Oct 16 15:14:12 2012 +0200
     5.3 @@ -11,7 +11,7 @@
     5.4    val current: T -> Proof.state
     5.5    val position: T -> int
     5.6    val back: T -> T
     5.7 -  val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
     5.8 +  val applys: (Proof.state -> Proof.state Seq.result Seq.seq) -> T -> T
     5.9    val apply: (Proof.state -> Proof.state) -> T -> T
    5.10  end;
    5.11  
    5.12 @@ -42,10 +42,8 @@
    5.13  (* apply transformer *)
    5.14  
    5.15  fun applys f (Proof_Node ((st, _), n)) =
    5.16 -  (case Seq.pull (f st) of
    5.17 -    NONE => error "empty result sequence -- proof command failed"
    5.18 -  | SOME res => Proof_Node (res, n + 1));
    5.19 +  Proof_Node (Seq.first_result "Empty result sequence -- proof command failed" (f st), n + 1);
    5.20  
    5.21 -fun apply f = applys (Seq.single o f);
    5.22 +fun apply f = applys (Seq.single o Seq.Result o f);
    5.23  
    5.24  end;
     6.1 --- a/src/Pure/Isar/toplevel.ML	Tue Oct 16 15:02:49 2012 +0200
     6.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Oct 16 15:14:12 2012 +0200
     6.3 @@ -74,9 +74,9 @@
     6.4    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
     6.5    val forget_proof: transition -> transition
     6.6    val present_proof: (state -> unit) -> transition -> transition
     6.7 -  val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
     6.8 +  val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
     6.9    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
    6.10 -  val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
    6.11 +  val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
    6.12    val proof: (Proof.state -> Proof.state) -> transition -> transition
    6.13    val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
    6.14    val skip_proof: (int -> int) -> transition -> transition
    6.15 @@ -556,7 +556,7 @@
    6.16      | skip as SkipProof _ => skip
    6.17      | _ => raise UNDEF));
    6.18  
    6.19 -fun proof' f = proofs' (Seq.single oo f);
    6.20 +fun proof' f = proofs' ((Seq.single o Seq.Result) oo f);
    6.21  val proofs = proofs' o K;
    6.22  val proof = proof' o K;
    6.23