src/Pure/Isar/runtime.ML
author wenzelm
Tue Feb 26 19:58:27 2013 +0100 (2013-02-26 ago)
changeset 51285 0859bd338c9b
parent 51242 a8e664e4fb5f
child 51639 b7f908c99546
permissions -rw-r--r--
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 TERMINATE
wenzelm@31476
    11
  exception EXCURSION_FAIL of exn * string
wenzelm@31476
    12
  exception TOPLEVEL_ERROR
wenzelm@39513
    13
  val debug: bool Unsynchronized.ref
wenzelm@31476
    14
  val exn_context: Proof.context option -> exn -> exn
wenzelm@51285
    15
  type error = ((serial * string) * string option)
wenzelm@51285
    16
  val exn_messages_ids: (exn -> Position.T) -> exn -> error list
wenzelm@44270
    17
  val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
wenzelm@31476
    18
  val exn_message: (exn -> Position.T) -> exn -> string
wenzelm@31476
    19
  val debugging: ('a -> 'b) -> 'a -> 'b
wenzelm@31476
    20
  val controlled_execution: ('a -> 'b) -> 'a -> 'b
wenzelm@33603
    21
  val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
wenzelm@31476
    22
end;
wenzelm@31476
    23
wenzelm@31476
    24
structure Runtime: RUNTIME =
wenzelm@31476
    25
struct
wenzelm@31476
    26
wenzelm@31476
    27
(** exceptions **)
wenzelm@31476
    28
wenzelm@31476
    29
exception UNDEF;
wenzelm@31476
    30
exception TERMINATE;
wenzelm@31476
    31
exception EXCURSION_FAIL of exn * string;
wenzelm@31476
    32
exception TOPLEVEL_ERROR;
wenzelm@31476
    33
wenzelm@39513
    34
val debug = Unsynchronized.ref false;
wenzelm@39513
    35
wenzelm@31476
    36
wenzelm@31476
    37
(* exn_context *)
wenzelm@31476
    38
wenzelm@31476
    39
exception CONTEXT of Proof.context * exn;
wenzelm@31476
    40
wenzelm@31476
    41
fun exn_context NONE exn = exn
wenzelm@39285
    42
  | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
wenzelm@31476
    43
wenzelm@31476
    44
wenzelm@31476
    45
(* exn_message *)
wenzelm@31476
    46
wenzelm@51285
    47
type error = ((serial * string) * string option);
wenzelm@51285
    48
wenzelm@50914
    49
local
wenzelm@50914
    50
wenzelm@31476
    51
fun if_context NONE _ _ = []
wenzelm@31476
    52
  | if_context (SOME ctxt) f xs = map (f ctxt) xs;
wenzelm@31476
    53
wenzelm@50914
    54
fun identify exn =
wenzelm@31476
    55
  let
wenzelm@50914
    56
    val exn' = Par_Exn.identify [] exn;
wenzelm@50914
    57
    val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
wenzelm@51242
    58
    val i = Par_Exn.the_serial exn' handle Option.Option => serial ();
wenzelm@51242
    59
  in ((i, exn'), exec_id) end;
wenzelm@50911
    60
wenzelm@50914
    61
fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
wenzelm@50914
    62
  | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
wenzelm@50914
    63
  | flatten context exn =
wenzelm@50914
    64
      (case Par_Exn.dest exn of
wenzelm@50914
    65
        SOME exns => maps (flatten context) exns
wenzelm@50914
    66
      | NONE => [(context, identify exn)]);
wenzelm@50911
    67
wenzelm@50914
    68
in
wenzelm@50914
    69
wenzelm@50914
    70
fun exn_messages_ids exn_position e =
wenzelm@50914
    71
  let
wenzelm@31476
    72
    fun raised exn name msgs =
wenzelm@48992
    73
      let val pos = Position.here (exn_position exn) in
wenzelm@31476
    74
        (case msgs of
wenzelm@31476
    75
          [] => "exception " ^ name ^ " raised" ^ pos
wenzelm@31476
    76
        | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
wenzelm@31476
    77
        | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
wenzelm@31476
    78
      end;
wenzelm@31476
    79
wenzelm@50914
    80
    fun exn_msgs (context, ((i, exn), id)) =
wenzelm@44270
    81
      (case exn of
wenzelm@44270
    82
        EXCURSION_FAIL (exn, loc) =>
wenzelm@50914
    83
          map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
wenzelm@44270
    84
            (sorted_msgs context exn)
wenzelm@44270
    85
      | _ =>
wenzelm@44270
    86
        let
wenzelm@44270
    87
          val msg =
wenzelm@44247
    88
            (case exn of
wenzelm@44270
    89
              TERMINATE => "Exit"
wenzelm@44270
    90
            | TimeLimit.TimeOut => "Timeout"
wenzelm@44270
    91
            | TOPLEVEL_ERROR => "Error"
wenzelm@44270
    92
            | ERROR msg => msg
wenzelm@44270
    93
            | Fail msg => raised exn "Fail" [msg]
wenzelm@44247
    94
            | THEORY (msg, thys) =>
wenzelm@45487
    95
                raised exn "THEORY" (msg :: map Context.str_of_thy thys)
wenzelm@44247
    96
            | Ast.AST (msg, asts) =>
wenzelm@45487
    97
                raised exn "AST" (msg :: map (Pretty.string_of o Ast.pretty_ast) asts)
wenzelm@44247
    98
            | TYPE (msg, Ts, ts) =>
wenzelm@44270
    99
                raised exn "TYPE" (msg ::
wenzelm@45487
   100
                  (if_context context Syntax.string_of_typ Ts @
wenzelm@45487
   101
                    if_context context Syntax.string_of_term ts))
wenzelm@44247
   102
            | TERM (msg, ts) =>
wenzelm@45487
   103
                raised exn "TERM" (msg :: if_context context Syntax.string_of_term ts)
wenzelm@44247
   104
            | THM (msg, i, thms) =>
wenzelm@45487
   105
                raised exn ("THM " ^ string_of_int i)
wenzelm@45487
   106
                  (msg :: if_context context Display.string_of_thm thms)
wenzelm@44270
   107
            | _ => raised exn (General.exnMessage exn) []);
wenzelm@50914
   108
        in [((i, msg), id)] end)
wenzelm@44270
   109
      and sorted_msgs context exn =
wenzelm@50914
   110
        sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
wenzelm@44270
   111
wenzelm@44270
   112
  in sorted_msgs NONE e end;
wenzelm@38874
   113
wenzelm@50914
   114
end;
wenzelm@50914
   115
wenzelm@50914
   116
fun exn_messages exn_position exn =
wenzelm@50914
   117
  map #1 (exn_messages_ids exn_position exn);
wenzelm@50914
   118
wenzelm@38874
   119
fun exn_message exn_position exn =
wenzelm@38874
   120
  (case exn_messages exn_position exn of
wenzelm@38875
   121
    [] => "Interrupt"
wenzelm@44270
   122
  | msgs => cat_lines (map snd msgs));
wenzelm@31476
   123
wenzelm@31476
   124
wenzelm@31476
   125
(** controlled execution **)
wenzelm@31476
   126
wenzelm@31476
   127
fun debugging f x =
wenzelm@45486
   128
  if ! debug
wenzelm@45486
   129
  then exception_trace (fn () => f x)
wenzelm@31476
   130
  else f x;
wenzelm@31476
   131
wenzelm@41715
   132
fun controlled_execution f x =
wenzelm@44295
   133
  (f |> debugging |> Future.interruptible_task) x;
wenzelm@31476
   134
wenzelm@39238
   135
fun toplevel_error output_exn f x = f x
wenzelm@39238
   136
  handle exn =>
wenzelm@39238
   137
    if Exn.is_interrupt exn then reraise exn
wenzelm@39238
   138
    else
wenzelm@39238
   139
      let
wenzelm@45197
   140
        val opt_ctxt =
wenzelm@45197
   141
          (case Context.thread_data () of
wenzelm@45197
   142
            NONE => NONE
wenzelm@45197
   143
          | SOME context => try Context.proof_of context);
wenzelm@45197
   144
        val _ = output_exn (exn_context opt_ctxt exn);
wenzelm@39238
   145
      in raise TOPLEVEL_ERROR end;
wenzelm@31476
   146
wenzelm@31476
   147
end;
wenzelm@31476
   148