(*  Title:      Pure/Isar/runtime.ML

    Author:     Makarius

Isar toplevel runtime support.

*)

signature RUNTIME =

sig

  exception UNDEF

  exception TERMINATE

  exception EXCURSION_FAIL of exn * string

  exception TOPLEVEL_ERROR

  val debug: bool Unsynchronized.ref

  val exn_context: Proof.context option -> exn -> exn

  val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list

  val exn_message: (exn -> Position.T) -> exn -> string

  val debugging: ('a -> 'b) -> 'a -> 'b

  val controlled_execution: ('a -> 'b) -> 'a -> 'b

  val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b

end;

structure Runtime: RUNTIME =

struct

(** exceptions **)

exception UNDEF;

exception TERMINATE;

exception EXCURSION_FAIL of exn * string;

exception TOPLEVEL_ERROR;

val debug = Unsynchronized.ref false;

(* exn_context *)

exception CONTEXT of Proof.context * exn;

fun exn_context NONE exn = exn

  | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);

(* exn_message *)

fun if_context NONE _ _ = []

  | if_context (SOME ctxt) f xs = map (f ctxt) xs;

fun exn_messages exn_position e =

  let

    fun raised exn name msgs =

      let val pos = Position.str_of (exn_position exn) in

        (case msgs of

          [] => "exception " ^ name ^ " raised" ^ pos

        | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg

        | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))

      end;

    val detailed = ! debug;

    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn

      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns

      | flatten context exn =

          (case Par_Exn.dest exn of

            SOME exns => maps (flatten context) exns

          | NONE => [(context, Par_Exn.serial exn)]);

    fun exn_msgs (context, (i, exn)) =

      (case exn of

        EXCURSION_FAIL (exn, loc) =>

          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))

            (sorted_msgs context exn)

      | _ =>

        let

          val msg =

            (case exn of

              TERMINATE => "Exit"

            | TimeLimit.TimeOut => "Timeout"

            | TOPLEVEL_ERROR => "Error"

            | ERROR msg => msg

            | Fail msg => raised exn "Fail" [msg]

            | THEORY (msg, thys) =>

                raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))

            | Ast.AST (msg, asts) =>

                raised exn "AST" (msg ::

                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))

            | TYPE (msg, Ts, ts) =>

                raised exn "TYPE" (msg ::

                  (if detailed then

                    if_context context Syntax.string_of_typ Ts @

                    if_context context Syntax.string_of_term ts

                   else []))

            | TERM (msg, ts) =>

                raised exn "TERM" (msg ::

                  (if detailed then if_context context Syntax.string_of_term ts else []))

            | THM (msg, i, thms) =>

                raised exn ("THM " ^ string_of_int i) (msg ::

                  (if detailed then if_context context Display.string_of_thm thms else []))

            | _ => raised exn (General.exnMessage exn) []);

        in [(i, msg)] end)

      and sorted_msgs context exn =

        sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));

  in sorted_msgs NONE e end;

fun exn_message exn_position exn =

  (case exn_messages exn_position exn of

    [] => "Interrupt"

  | msgs => cat_lines (map snd msgs));

(** controlled execution **)

fun debugging f x =

  if ! debug then

    Exn.release (exception_trace (fn () =>

      Exn.Res (f x) handle

        exn as UNDEF => Exn.Exn exn

      | exn as EXCURSION_FAIL _ => Exn.Exn exn))

  else f x;

fun controlled_execution f x =

  (f |> debugging |> Future.interruptible_task) x;

fun toplevel_error output_exn f x = f x

  handle exn =>

    if Exn.is_interrupt exn then reraise exn

    else

      let

        val ctxt = Option.map Context.proof_of (Context.thread_data ());

        val _ = output_exn (exn_context ctxt exn);

      in raise TOPLEVEL_ERROR end;

end;