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