src/Pure/Isar/runtime.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62878 1cec457e0a03
child 65948 de7888573ed7
permissions -rw-r--r--
clarified modules;
tuned signature;
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@62516
    12
  val pretty_exn: exn -> Pretty.T
wenzelm@31476
    13
  val exn_context: Proof.context option -> exn -> exn
wenzelm@61077
    14
  val thread_context: exn -> exn
wenzelm@51285
    15
  type error = ((serial * string) * string option)
wenzelm@56303
    16
  val exn_messages_ids: exn -> error list
wenzelm@56303
    17
  val exn_messages: exn -> (serial * string) list
wenzelm@56303
    18
  val exn_message: exn -> string
wenzelm@56303
    19
  val exn_error_message: exn -> unit
wenzelm@57975
    20
  val exn_system_message: exn -> unit
wenzelm@56303
    21
  val exn_trace: (unit -> 'a) -> 'a
wenzelm@59056
    22
  val exn_trace_system: (unit -> 'a) -> 'a
wenzelm@62498
    23
  val exn_debugger: (unit -> 'a) -> 'a
wenzelm@62498
    24
  val exn_debugger_system: (unit -> 'a) -> 'a
wenzelm@56303
    25
  val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
wenzelm@56303
    26
  val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
wenzelm@33603
    27
  val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
wenzelm@56303
    28
  val toplevel_program: (unit -> 'a) -> 'a
wenzelm@31476
    29
end;
wenzelm@31476
    30
wenzelm@31476
    31
structure Runtime: RUNTIME =
wenzelm@31476
    32
struct
wenzelm@31476
    33
wenzelm@31476
    34
(** exceptions **)
wenzelm@31476
    35
wenzelm@31476
    36
exception UNDEF;
wenzelm@31476
    37
exception EXCURSION_FAIL of exn * string;
wenzelm@31476
    38
exception TOPLEVEL_ERROR;
wenzelm@31476
    39
wenzelm@31476
    40
wenzelm@62516
    41
(* pretty *)
wenzelm@62516
    42
wenzelm@62516
    43
fun pretty_exn (exn: exn) =
wenzelm@62516
    44
  Pretty.from_ML
wenzelm@62516
    45
    (ML_Pretty.from_polyml
wenzelm@62878
    46
      (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))));
wenzelm@62516
    47
wenzelm@62516
    48
wenzelm@31476
    49
(* exn_context *)
wenzelm@31476
    50
wenzelm@31476
    51
exception CONTEXT of Proof.context * exn;
wenzelm@31476
    52
wenzelm@31476
    53
fun exn_context NONE exn = exn
wenzelm@39285
    54
  | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
wenzelm@31476
    55
wenzelm@61077
    56
fun thread_context exn =
wenzelm@62889
    57
  exn_context (Option.map Context.proof_of (Context.get_generic_context ())) exn;
wenzelm@61077
    58
wenzelm@31476
    59
wenzelm@31476
    60
(* exn_message *)
wenzelm@31476
    61
wenzelm@51285
    62
type error = ((serial * string) * string option);
wenzelm@51285
    63
wenzelm@50914
    64
local
wenzelm@50914
    65
wenzelm@52686
    66
fun robust f x =
wenzelm@52686
    67
  (case try f x of
wenzelm@52686
    68
    SOME s => s
wenzelm@52686
    69
  | NONE => Markup.markup Markup.intensify "<malformed>");
wenzelm@52686
    70
wenzelm@52686
    71
fun robust2 f x y = robust (fn () => f x y) ();
wenzelm@52686
    72
wenzelm@52686
    73
fun robust_context NONE _ _ = []
wenzelm@52686
    74
  | robust_context (SOME ctxt) f xs = map (robust2 f ctxt) xs;
wenzelm@31476
    75
wenzelm@50914
    76
fun identify exn =
wenzelm@31476
    77
  let
wenzelm@50914
    78
    val exn' = Par_Exn.identify [] exn;
wenzelm@50914
    79
    val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
wenzelm@51242
    80
    val i = Par_Exn.the_serial exn' handle Option.Option => serial ();
wenzelm@51242
    81
  in ((i, exn'), exec_id) end;
wenzelm@50911
    82
wenzelm@50914
    83
fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
wenzelm@50914
    84
  | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
wenzelm@50914
    85
  | flatten context exn =
wenzelm@50914
    86
      (case Par_Exn.dest exn of
wenzelm@50914
    87
        SOME exns => maps (flatten context) exns
wenzelm@50914
    88
      | NONE => [(context, identify exn)]);
wenzelm@50911
    89
wenzelm@61878
    90
val print_thy = Pretty.unformatted_string_of o Context.pretty_abbrev_thy;
wenzelm@61878
    91
wenzelm@50914
    92
in
wenzelm@50914
    93
wenzelm@56303
    94
fun exn_messages_ids e =
wenzelm@50914
    95
  let
wenzelm@31476
    96
    fun raised exn name msgs =
wenzelm@62516
    97
      let val pos = Position.here (Exn_Properties.position exn) in
wenzelm@31476
    98
        (case msgs of
wenzelm@31476
    99
          [] => "exception " ^ name ^ " raised" ^ pos
wenzelm@31476
   100
        | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
wenzelm@51653
   101
        | _ =>
wenzelm@51653
   102
            cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") ::
wenzelm@51653
   103
              map (Markup.markup Markup.item) msgs))
wenzelm@31476
   104
      end;
wenzelm@31476
   105
wenzelm@50914
   106
    fun exn_msgs (context, ((i, exn), id)) =
wenzelm@44270
   107
      (case exn of
wenzelm@44270
   108
        EXCURSION_FAIL (exn, loc) =>
wenzelm@50914
   109
          map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
wenzelm@44270
   110
            (sorted_msgs context exn)
wenzelm@44270
   111
      | _ =>
wenzelm@44270
   112
        let
wenzelm@44270
   113
          val msg =
wenzelm@44247
   114
            (case exn of
wenzelm@62519
   115
              Timeout.TIMEOUT t => Timeout.print t
wenzelm@44270
   116
            | TOPLEVEL_ERROR => "Error"
wenzelm@57831
   117
            | ERROR "" => "Error"
wenzelm@44270
   118
            | ERROR msg => msg
wenzelm@44270
   119
            | Fail msg => raised exn "Fail" [msg]
wenzelm@61878
   120
            | THEORY (msg, thys) => raised exn "THEORY" (msg :: map (robust print_thy) thys)
wenzelm@44247
   121
            | Ast.AST (msg, asts) =>
wenzelm@52686
   122
                raised exn "AST" (msg :: map (robust (Pretty.string_of o Ast.pretty_ast)) asts)
wenzelm@44247
   123
            | TYPE (msg, Ts, ts) =>
wenzelm@44270
   124
                raised exn "TYPE" (msg ::
wenzelm@52686
   125
                  (robust_context context Syntax.string_of_typ Ts @
wenzelm@52686
   126
                    robust_context context Syntax.string_of_term ts))
wenzelm@44247
   127
            | TERM (msg, ts) =>
wenzelm@52686
   128
                raised exn "TERM" (msg :: robust_context context Syntax.string_of_term ts)
wenzelm@51640
   129
            | CTERM (msg, cts) =>
wenzelm@51640
   130
                raised exn "CTERM"
wenzelm@59582
   131
                  (msg :: robust_context context Syntax.string_of_term (map Thm.term_of cts))
wenzelm@44247
   132
            | THM (msg, i, thms) =>
wenzelm@45487
   133
                raised exn ("THM " ^ string_of_int i)
wenzelm@61268
   134
                  (msg :: robust_context context Thm.string_of_thm thms)
wenzelm@62516
   135
            | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
wenzelm@50914
   136
        in [((i, msg), id)] end)
wenzelm@44270
   137
      and sorted_msgs context exn =
wenzelm@59058
   138
        sort_distinct (int_ord o apply2 (fst o fst)) (maps exn_msgs (flatten context exn));
wenzelm@44270
   139
wenzelm@44270
   140
  in sorted_msgs NONE e end;
wenzelm@38874
   141
wenzelm@50914
   142
end;
wenzelm@50914
   143
wenzelm@56303
   144
fun exn_messages exn = map #1 (exn_messages_ids exn);
wenzelm@50914
   145
wenzelm@56303
   146
fun exn_message exn =
wenzelm@56303
   147
  (case exn_messages exn of
wenzelm@38875
   148
    [] => "Interrupt"
wenzelm@44270
   149
  | msgs => cat_lines (map snd msgs));
wenzelm@31476
   150
wenzelm@56303
   151
val exn_error_message = Output.error_message o exn_message;
wenzelm@57975
   152
val exn_system_message = Output.system_message o exn_message;
wenzelm@62505
   153
fun exn_trace e = Exn.trace exn_message tracing e;
wenzelm@62505
   154
fun exn_trace_system e = Exn.trace exn_message Output.system_message e;
wenzelm@56303
   155
wenzelm@56303
   156
wenzelm@62498
   157
(* exception debugger *)
wenzelm@62498
   158
wenzelm@62498
   159
local
wenzelm@62498
   160
wenzelm@62498
   161
fun print_entry (name, loc) =
wenzelm@62821
   162
  Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_polyml_location loc));
wenzelm@62498
   163
wenzelm@62498
   164
fun exception_debugger output e =
wenzelm@62498
   165
  let
wenzelm@62498
   166
    val (trace, result) = Exn_Debugger.capture_exception_trace e;
wenzelm@62498
   167
    val _ =
wenzelm@62498
   168
      (case (trace, result) of
wenzelm@62498
   169
        (_ :: _, Exn.Exn exn) =>
wenzelm@62498
   170
          output (cat_lines ("Exception trace - " ^ exn_message exn :: map print_entry trace))
wenzelm@62498
   171
      | _ => ());
wenzelm@62498
   172
  in Exn.release result end;
wenzelm@62498
   173
wenzelm@62498
   174
in
wenzelm@62498
   175
wenzelm@62498
   176
fun exn_debugger e = exception_debugger tracing e;
wenzelm@62498
   177
fun exn_debugger_system e = exception_debugger Output.system_message e;
wenzelm@62498
   178
wenzelm@62498
   179
end;
wenzelm@62498
   180
wenzelm@62498
   181
wenzelm@31476
   182
wenzelm@31476
   183
(** controlled execution **)
wenzelm@31476
   184
wenzelm@62498
   185
fun debugging1 opt_context f x =
wenzelm@56303
   186
  if ML_Options.exception_trace_enabled opt_context
wenzelm@59055
   187
  then exn_trace (fn () => f x) else f x;
wenzelm@31476
   188
wenzelm@62498
   189
fun debugging2 opt_context f x =
wenzelm@62498
   190
  if ML_Options.exception_debugger_enabled opt_context
wenzelm@62498
   191
  then exn_debugger (fn () => f x) else f x;
wenzelm@62498
   192
wenzelm@62498
   193
fun debugging opt_context f =
wenzelm@62498
   194
  f |> debugging1 opt_context |> debugging2 opt_context;
wenzelm@62498
   195
wenzelm@56303
   196
fun controlled_execution opt_context f x =
wenzelm@56303
   197
  (f |> debugging opt_context |> Future.interruptible_task) x;
wenzelm@31476
   198
wenzelm@39238
   199
fun toplevel_error output_exn f x = f x
wenzelm@39238
   200
  handle exn =>
wenzelm@62505
   201
    if Exn.is_interrupt exn then Exn.reraise exn
wenzelm@39238
   202
    else
wenzelm@39238
   203
      let
wenzelm@45197
   204
        val opt_ctxt =
wenzelm@62889
   205
          (case Context.get_generic_context () of
wenzelm@45197
   206
            NONE => NONE
wenzelm@45197
   207
          | SOME context => try Context.proof_of context);
wenzelm@45197
   208
        val _ = output_exn (exn_context opt_ctxt exn);
wenzelm@39238
   209
      in raise TOPLEVEL_ERROR end;
wenzelm@31476
   210
wenzelm@56303
   211
fun toplevel_program body =
wenzelm@56303
   212
  (body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
wenzelm@56303
   213
wenzelm@31476
   214
end;