src/Pure/Isar/runtime.ML
author wenzelm
Wed Nov 26 14:35:55 2014 +0100 (2014-11-26 ago)
changeset 59055 5a7157b8e870
parent 58894 447972249785
child 59056 cbe9563c03d1
permissions -rw-r--r--
more informative failure of protocol commands, with exception trace;
eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);
wenzelm@31476
     1
(*  Title:      Pure/Isar/runtime.ML
wenzelm@31476
     2
    Author:     Makarius
wenzelm@31476
     3
wenzelm@31476
     4
Isar toplevel runtime support.
wenzelm@31476
     5
*)
wenzelm@31476
     6
wenzelm@31476
     7
signature RUNTIME =
wenzelm@31476
     8
sig
wenzelm@31476
     9
  exception UNDEF
wenzelm@31476
    10
  exception EXCURSION_FAIL of exn * string
wenzelm@31476
    11
  exception TOPLEVEL_ERROR
wenzelm@31476
    12
  val exn_context: Proof.context option -> exn -> exn
wenzelm@51285
    13
  type error = ((serial * string) * string option)
wenzelm@56303
    14
  val exn_messages_ids: exn -> error list
wenzelm@56303
    15
  val exn_messages: exn -> (serial * string) list
wenzelm@56303
    16
  val exn_message: exn -> string
wenzelm@56303
    17
  val exn_error_message: exn -> unit
wenzelm@57975
    18
  val exn_system_message: exn -> unit
wenzelm@56303
    19
  val exn_trace: (unit -> 'a) -> 'a
wenzelm@56303
    20
  val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
wenzelm@56303
    21
  val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
wenzelm@33603
    22
  val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
wenzelm@56303
    23
  val toplevel_program: (unit -> 'a) -> 'a
wenzelm@31476
    24
end;
wenzelm@31476
    25
wenzelm@31476
    26
structure Runtime: RUNTIME =
wenzelm@31476
    27
struct
wenzelm@31476
    28
wenzelm@31476
    29
(** exceptions **)
wenzelm@31476
    30
wenzelm@31476
    31
exception UNDEF;
wenzelm@31476
    32
exception EXCURSION_FAIL of exn * string;
wenzelm@31476
    33
exception TOPLEVEL_ERROR;
wenzelm@31476
    34
wenzelm@31476
    35
wenzelm@31476
    36
(* exn_context *)
wenzelm@31476
    37
wenzelm@31476
    38
exception CONTEXT of Proof.context * exn;
wenzelm@31476
    39
wenzelm@31476
    40
fun exn_context NONE exn = exn
wenzelm@39285
    41
  | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
wenzelm@31476
    42
wenzelm@31476
    43
wenzelm@31476
    44
(* exn_message *)
wenzelm@31476
    45
wenzelm@51285
    46
type error = ((serial * string) * string option);
wenzelm@51285
    47
wenzelm@50914
    48
local
wenzelm@50914
    49
wenzelm@52686
    50
fun robust f x =
wenzelm@52686
    51
  (case try f x of
wenzelm@52686
    52
    SOME s => s
wenzelm@52686
    53
  | NONE => Markup.markup Markup.intensify "<malformed>");
wenzelm@52686
    54
wenzelm@52686
    55
fun robust2 f x y = robust (fn () => f x y) ();
wenzelm@52686
    56
wenzelm@52686
    57
fun robust_context NONE _ _ = []
wenzelm@52686
    58
  | robust_context (SOME ctxt) f xs = map (robust2 f ctxt) xs;
wenzelm@31476
    59
wenzelm@50914
    60
fun identify exn =
wenzelm@31476
    61
  let
wenzelm@50914
    62
    val exn' = Par_Exn.identify [] exn;
wenzelm@50914
    63
    val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
wenzelm@51242
    64
    val i = Par_Exn.the_serial exn' handle Option.Option => serial ();
wenzelm@51242
    65
  in ((i, exn'), exec_id) end;
wenzelm@50911
    66
wenzelm@50914
    67
fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
wenzelm@50914
    68
  | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
wenzelm@50914
    69
  | flatten context exn =
wenzelm@50914
    70
      (case Par_Exn.dest exn of
wenzelm@50914
    71
        SOME exns => maps (flatten context) exns
wenzelm@50914
    72
      | NONE => [(context, identify exn)]);
wenzelm@50911
    73
wenzelm@50914
    74
in
wenzelm@50914
    75
wenzelm@56303
    76
fun exn_messages_ids e =
wenzelm@50914
    77
  let
wenzelm@31476
    78
    fun raised exn name msgs =
wenzelm@56303
    79
      let val pos = Position.here (Exn_Output.position exn) in
wenzelm@31476
    80
        (case msgs of
wenzelm@31476
    81
          [] => "exception " ^ name ^ " raised" ^ pos
wenzelm@31476
    82
        | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
wenzelm@51653
    83
        | _ =>
wenzelm@51653
    84
            cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") ::
wenzelm@51653
    85
              map (Markup.markup Markup.item) msgs))
wenzelm@31476
    86
      end;
wenzelm@31476
    87
wenzelm@50914
    88
    fun exn_msgs (context, ((i, exn), id)) =
wenzelm@44270
    89
      (case exn of
wenzelm@44270
    90
        EXCURSION_FAIL (exn, loc) =>
wenzelm@50914
    91
          map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
wenzelm@44270
    92
            (sorted_msgs context exn)
wenzelm@44270
    93
      | _ =>
wenzelm@44270
    94
        let
wenzelm@44270
    95
          val msg =
wenzelm@44247
    96
            (case exn of
wenzelm@59055
    97
              TimeLimit.TimeOut => "Timeout"
wenzelm@44270
    98
            | TOPLEVEL_ERROR => "Error"
wenzelm@57831
    99
            | ERROR "" => "Error"
wenzelm@44270
   100
            | ERROR msg => msg
wenzelm@44270
   101
            | Fail msg => raised exn "Fail" [msg]
wenzelm@44247
   102
            | THEORY (msg, thys) =>
wenzelm@52686
   103
                raised exn "THEORY" (msg :: map (robust Context.str_of_thy) thys)
wenzelm@44247
   104
            | Ast.AST (msg, asts) =>
wenzelm@52686
   105
                raised exn "AST" (msg :: map (robust (Pretty.string_of o Ast.pretty_ast)) asts)
wenzelm@44247
   106
            | TYPE (msg, Ts, ts) =>
wenzelm@44270
   107
                raised exn "TYPE" (msg ::
wenzelm@52686
   108
                  (robust_context context Syntax.string_of_typ Ts @
wenzelm@52686
   109
                    robust_context context Syntax.string_of_term ts))
wenzelm@44247
   110
            | TERM (msg, ts) =>
wenzelm@52686
   111
                raised exn "TERM" (msg :: robust_context context Syntax.string_of_term ts)
wenzelm@51640
   112
            | CTERM (msg, cts) =>
wenzelm@51640
   113
                raised exn "CTERM"
wenzelm@52686
   114
                  (msg :: robust_context context Syntax.string_of_term (map term_of cts))
wenzelm@44247
   115
            | THM (msg, i, thms) =>
wenzelm@45487
   116
                raised exn ("THM " ^ string_of_int i)
wenzelm@52686
   117
                  (msg :: robust_context context Display.string_of_thm thms)
wenzelm@56303
   118
            | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
wenzelm@50914
   119
        in [((i, msg), id)] end)
wenzelm@44270
   120
      and sorted_msgs context exn =
wenzelm@50914
   121
        sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
wenzelm@44270
   122
wenzelm@44270
   123
  in sorted_msgs NONE e end;
wenzelm@38874
   124
wenzelm@50914
   125
end;
wenzelm@50914
   126
wenzelm@56303
   127
fun exn_messages exn = map #1 (exn_messages_ids exn);
wenzelm@50914
   128
wenzelm@56303
   129
fun exn_message exn =
wenzelm@56303
   130
  (case exn_messages exn of
wenzelm@38875
   131
    [] => "Interrupt"
wenzelm@44270
   132
  | msgs => cat_lines (map snd msgs));
wenzelm@31476
   133
wenzelm@56303
   134
val exn_error_message = Output.error_message o exn_message;
wenzelm@57975
   135
val exn_system_message = Output.system_message o exn_message;
wenzelm@59055
   136
fun exn_trace e = print_exception_trace exn_message tracing e;
wenzelm@56303
   137
wenzelm@56303
   138
wenzelm@31476
   139
wenzelm@31476
   140
(** controlled execution **)
wenzelm@31476
   141
wenzelm@56303
   142
fun debugging opt_context f x =
wenzelm@56303
   143
  if ML_Options.exception_trace_enabled opt_context
wenzelm@59055
   144
  then exn_trace (fn () => f x) else f x;
wenzelm@31476
   145
wenzelm@56303
   146
fun controlled_execution opt_context f x =
wenzelm@56303
   147
  (f |> debugging opt_context |> Future.interruptible_task) x;
wenzelm@31476
   148
wenzelm@39238
   149
fun toplevel_error output_exn f x = f x
wenzelm@39238
   150
  handle exn =>
wenzelm@39238
   151
    if Exn.is_interrupt exn then reraise exn
wenzelm@39238
   152
    else
wenzelm@39238
   153
      let
wenzelm@45197
   154
        val opt_ctxt =
wenzelm@45197
   155
          (case Context.thread_data () of
wenzelm@45197
   156
            NONE => NONE
wenzelm@45197
   157
          | SOME context => try Context.proof_of context);
wenzelm@45197
   158
        val _ = output_exn (exn_context opt_ctxt exn);
wenzelm@39238
   159
      in raise TOPLEVEL_ERROR end;
wenzelm@31476
   160
wenzelm@56303
   161
fun toplevel_program body =
wenzelm@56303
   162
  (body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
wenzelm@56303
   163
wenzelm@31476
   164
end;
wenzelm@31476
   165