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