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