src/Pure/Isar/toplevel.ML

debug: exception_trace;
tuned;

(*  Title:      Pure/Isar/toplevel.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

The Isabelle/Isar toplevel.
*)

signature TOPLEVEL =
sig
  datatype node = Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory
  type state
  val toplevel: state
  val is_toplevel: state -> bool
  val prompt_state_default: state -> string
  val prompt_state_fn: (state -> string) ref
  val print_state_context: state -> unit
  val print_state_default: bool -> state -> unit
  val print_state_fn: (bool -> state -> unit) ref
  val print_state: bool -> state -> unit
  val pretty_state: bool -> state -> Pretty.T list
  exception UNDEF
  val node_history_of: state -> node History.T
  val node_of: state -> node
  val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
  val theory_of: state -> theory
  val sign_of: state -> theory    (*obsolete*)
  val context_of: state -> Proof.context
  val proof_of: state -> Proof.state
  val enter_forward_proof: state -> Proof.state
  val quiet: bool ref
  val debug: bool ref
  val timing: bool ref
  val profiling: int ref
  exception TERMINATE
  exception RESTART
  type transition
  val undo_limit: bool -> int option
  val empty: transition
  val name_of: transition -> string
  val source_of: transition -> OuterLex.token list option
  val name: string -> transition -> transition
  val position: Position.T -> transition -> transition
  val source: OuterLex.token list -> transition -> transition
  val interactive: bool -> transition -> transition
  val print: transition -> transition
  val print': string -> transition -> transition
  val no_timing: transition -> transition
  val reset: transition -> transition
  val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
  val exit: transition -> transition
  val kill: transition -> transition
  val keep: (state -> unit) -> transition -> transition
  val keep': (bool -> state -> unit) -> transition -> transition
  val history: (node History.T -> node History.T) -> transition -> transition
  val imperative: (unit -> unit) -> transition -> transition
  val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
    -> transition -> transition
  val skip_proofs: bool ref
  val theory: (theory -> theory) -> transition -> transition
  val theory': (bool -> theory -> theory) -> transition -> transition
  val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
  val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
  val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
  val proof'': (ProofHistory.T -> ProofHistory.T) -> transition -> transition
  val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
  val proof_to_theory': (bool -> ProofHistory.T -> theory) -> transition -> transition
  val skip_proof: (int History.T -> int History.T) -> transition -> transition
  val skip_proof_to_theory: (int History.T -> bool) -> transition -> transition
  val unknown_theory: transition -> transition
  val unknown_proof: transition -> transition
  val unknown_context: transition -> transition
  val exn_message: exn -> string
  val apply: bool -> transition -> state -> (state * (exn * string) option) option
  val excursion_result: ((transition * (state -> state -> 'a -> 'a)) list * 'a) -> 'a
  val excursion: transition list -> unit
  val set_state: state -> unit
  val get_state: unit -> state
  val exn: unit -> (exn * string) option
  val >> : transition -> bool
  val >>> : transition list -> unit
  type 'a isar
  val loop: 'a isar -> unit
end;

structure Toplevel: TOPLEVEL =
struct


(** toplevel state **)

(* datatype node *)

datatype node =
  Theory of theory |
  Proof of ProofHistory.T |
  SkipProof of int History.T * theory;

fun str_of_node (Theory _) = "in theory mode"
  | str_of_node _ = "in proof mode";

fun pretty_context thy = [Pretty.block
  [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
    Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];

fun pretty_prf prf = Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf);

fun pretty_node_context (Theory thy) = pretty_context thy
  | pretty_node_context (Proof prf) = pretty_context (Proof.theory_of (ProofHistory.current prf))
  | pretty_node_context _ = [];

fun pretty_node prf_only (Theory thy) = if prf_only then [] else pretty_context thy
  | pretty_node _ (Proof prf) = pretty_prf prf
  | pretty_node _ _ = [];


(* datatype state *)

datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;

val toplevel = State NONE;

fun is_toplevel (State NONE) = true
  | is_toplevel _ = false;

fun str_of_state (State NONE) = "at top level"
  | str_of_state (State (SOME (node, _))) = str_of_node (History.current node);


(* prompt_state hook *)

fun prompt_state_default (State _) = Source.default_prompt;

val prompt_state_fn = ref prompt_state_default;
fun prompt_state state = ! prompt_state_fn state;


(* print state *)

fun pretty_current_node _ (State NONE) = []
  | pretty_current_node prt (State (SOME (node, _))) = prt (History.current node);

val print_state_context =
  Pretty.writeln o Pretty.chunks o pretty_current_node pretty_node_context;

fun pretty_state prf_only state =
  let val ref (begin_state, end_state, _) = Display.current_goals_markers in
    (case pretty_current_node (pretty_node prf_only) state of [] => []
    | prts =>
        (if begin_state = "" then [] else [Pretty.str begin_state]) @ prts @
        (if end_state = "" then [] else [Pretty.str end_state]))
  end;

fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state);
val print_state_fn = ref print_state_default;
fun print_state state = ! print_state_fn state;


(* top node *)

exception UNDEF;

fun node_history_of (State NONE) = raise UNDEF
  | node_history_of (State (SOME (node, _))) = node;

val node_of = History.current o node_history_of;

fun node_case f g state =
  (case node_of state of
    Theory thy => f thy
  | SkipProof (i, thy) => f thy
  | Proof prf => g (ProofHistory.current prf));

val theory_of = node_case I Proof.theory_of;
val sign_of = theory_of;
val context_of = node_case ProofContext.init Proof.context_of;
val proof_of = node_case (fn _ => raise UNDEF) I;

val enter_forward_proof = node_case Proof.init_state Proof.enter_forward;



(** toplevel transitions **)

val quiet = ref false;
val debug = ref false;
val timing = Output.timing;
val profiling = ref 0;

exception TERMINATE;
exception RESTART;
exception EXCURSION_FAIL of exn * string;
exception FAILURE of state * exn;


(* recovery from stale theories *)

(*note: proof commands should be non-destructive!*)

local

fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;

fun checkpoint_node true (Theory thy) = Theory (Theory.checkpoint thy)
  | checkpoint_node _ node = node;

fun copy_node true (Theory thy) = Theory (Theory.copy thy)
  | copy_node _ node = node;

val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";

fun return (result, NONE) = result
  | return (result, SOME exn) = raise FAILURE (result, exn);

fun debug_trans f x =
  if ! debug then
    let val y = ref x in
      setmp Output.transform_exceptions false
        exception_trace (fn () => y := f x); ! y
    end
  else f x;

fun interruptible f x =
  let val y = ref x
  in raise_interrupt (fn () => y := f x) (); ! y end;

in

fun node_trans _ _ _ (State NONE) = raise UNDEF
  | node_trans int hist f (State (SOME (node, term))) =
      let
        val cont_node = History.map (checkpoint_node int) node;
        val back_node = History.map (copy_node int) cont_node;
        fun state nd = State (SOME (nd, term));
        fun normal_state nd = (state nd, NONE);
        fun error_state nd exn = (state nd, SOME exn);

        val (result, err) =
          cont_node
          |> ((fn nd => f int nd)
              |> (if hist then History.apply_copy (copy_node int) else History.map)
              |> debug_trans
              |> interruptible
              |> transform_error)
          |> normal_state
          handle exn => error_state cont_node exn;
      in
        if is_stale result
        then return (error_state back_node (if_none err stale_theory))
        else return (result, err)
      end;

end;


(* primitive transitions *)

(*Important note: recovery from stale theories is provided only for
  theory-level operations via MapCurrent and AppCurrent.  Other node
  or state operations should not touch theories at all.

  Also note that interrupts are enabled for Keep, MapCurrent, and
  AppCurrent only.*)

datatype trans =
  Reset |                                       (*empty toplevel*)
  Init of (bool -> node) * ((node -> unit) * (node -> unit)) |
    (*init node; provide exit/kill operation*)
  Exit |                                        (*conclude node*)
  Kill |                                        (*abort node*)
  Keep of bool -> state -> unit |               (*peek at state*)
  History of node History.T -> node History.T | (*history operation (undo etc.)*)
  MapCurrent of bool -> node -> node |          (*change node, bypassing history*)
  AppCurrent of bool -> node -> node;           (*change node, recording history*)

fun undo_limit int = if int then NONE else SOME 0;

local

fun apply_tr _ Reset _ = toplevel
  | apply_tr int (Init (f, term)) (State NONE) =
      State (SOME (History.init (undo_limit int) (f int), term))
  | apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF
  | apply_tr _ Exit (State NONE) = raise UNDEF
  | apply_tr _ Exit (State (SOME (node, (exit, _)))) =
      (exit (History.current node); State NONE)
  | apply_tr _ Kill (State NONE) = raise UNDEF
  | apply_tr _ Kill (State (SOME (node, (_, kill)))) =
      (kill (History.current node); State NONE)
  | apply_tr int (Keep f) state = (raise_interrupt (f int) state; state)
  | apply_tr _ (History _) (State NONE) = raise UNDEF
  | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
  | apply_tr int (MapCurrent f) state = node_trans int false f state
  | apply_tr int (AppCurrent f) state = node_trans int true f state;

fun apply_union _ [] state = raise FAILURE (state, UNDEF)
  | apply_union int (tr :: trs) state =
      transform_error (apply_tr int tr) state
        handle UNDEF => apply_union int trs state
          | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
          | exn as FAILURE _ => raise exn
          | exn => raise FAILURE (state, exn);

in

fun apply_trans int trs state = (apply_union int trs state, NONE)
  handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);

end;


(* datatype transition *)

datatype transition = Transition of
 {name: string,
  pos: Position.T,
  source: OuterLex.token list option,
  int_only: bool,
  print: string list,
  no_timing: bool,
  trans: trans list};

fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
  Transition {name = name, pos = pos, source = source,
    int_only = int_only, print = print, no_timing = no_timing, trans = trans};

fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) =
  make_transition (f (name, pos, source, int_only, print, no_timing, trans));

val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []);

fun name_of (Transition {name, ...}) = name;
fun source_of (Transition {source, ...}) = source;


(* diagnostics *)

fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;

fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr;
fun at_command tr = command_msg "At " tr ^ ".";

fun type_error tr state =
  ERROR_MESSAGE (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);


(* modify transitions *)

fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) =>
  (nm, pos, source, int_only, print, no_timing, trans));

fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) =>
  (name, pos, source, int_only, print, no_timing, trans));

fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) =>
  (name, pos, SOME src, int_only, print, no_timing, trans));

fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) =>
  (name, pos, source, int_only, print, no_timing, trans));

fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
  (name, pos, source, int_only, insert (op =) mode print, no_timing, trans));

val print = print' "";

val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) =>
  (name, pos, source, int_only, print, true, trans));

fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
  (name, pos, source, int_only, print, no_timing, trans @ [tr]));


(* build transitions *)

val reset = add_trans Reset;
fun init f exit kill = add_trans (Init (f, (exit, kill)));
val exit = add_trans Exit;
val kill = add_trans Kill;
val keep' = add_trans o Keep;
val history = add_trans o History;
val map_current = add_trans o MapCurrent;
val app_current = add_trans o AppCurrent;

fun keep f = add_trans (Keep (fn _ => f));
fun imperative f = keep (fn _ => f ());

fun init_theory f exit kill =
  init (fn int => Theory (f int))
    (fn Theory thy => exit thy | _ => raise UNDEF)
    (fn Theory thy => kill thy | _ => raise UNDEF);


(* typed transitions *)

(*The skip_proofs flag allows proof scripts to be skipped during
  interactive proof in order to speed up processing of large
  theories. While in skipping mode, states are represented as
  SkipProof (h, thy), where h contains a counter for the number of
  open proof blocks.*)

val skip_proofs = ref false;

fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));

fun theory_to_proof f = app_current (fn int =>
  (fn Theory thy =>
        if ! skip_proofs then SkipProof (History.init (undo_limit int) 0,
          fst (SkipProof.global_skip_proof int (ProofHistory.current (f int thy))))
        else Proof (f int thy)
    | _ => raise UNDEF));

fun proof''' b f = map_current (fn int => (fn Proof prf => Proof (f int prf)
  | SkipProof (h, thy) => if b then SkipProof (History.apply I h, thy) else raise UNDEF
  | _ => raise UNDEF));

val proof' = proof''' true;
val proof = proof' o K;
val proof'' = proof''' false o K;

fun proof_to_theory' f =
  map_current (fn int => (fn Proof prf => Theory (f int prf)
    | SkipProof (h, thy) => if History.current h = 0 then Theory thy else raise UNDEF
    | _ => raise UNDEF));

val proof_to_theory = proof_to_theory' o K;

fun skip_proof f = map_current (fn int =>
  (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF));

fun skip_proof_to_theory p = map_current (fn int =>
  (fn SkipProof (h, thy) => if p h then Theory thy else raise UNDEF | _ => raise UNDEF));

val unknown_theory = imperative (fn () => warning "Unknown theory context");
val unknown_proof = imperative (fn () => warning "Unknown proof context");
val unknown_context = imperative (fn () => warning "Unknown context");



(** toplevel transactions **)

(* print exceptions *)

local

fun with_context f xs =
  (case Context.get_context () of NONE => []
  | SOME thy => map (f thy) xs);

fun raised name [] = "exception " ^ name ^ " raised"
  | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
  | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs);

fun exn_msg _ TERMINATE = "Exit."
  | exn_msg _ RESTART = "Restart."
  | exn_msg _ Interrupt = "Interrupt."
  | exn_msg _ ERROR = "ERROR."
  | exn_msg _ (ERROR_MESSAGE msg) = msg
  | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
  | exn_msg detailed (Context.DATA_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
  | exn_msg detailed (Syntax.TRANSLATION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
  | exn_msg false (THEORY (msg, _)) = msg
  | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)
  | exn_msg _ (ProofContext.CONTEXT (msg, _)) = msg
  | exn_msg _ (Proof.STATE (msg, _)) = msg
  | exn_msg _ (ProofHistory.FAIL msg) = msg
  | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
      fail_msg detailed "simproc" ((name, Position.none), exn)
  | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info
  | exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info
  | exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info
  | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg]
  | exn_msg true (Syntax.AST (msg, asts)) =
      raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
  | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
  | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
        with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts)
  | exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
  | exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts)
  | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
  | exn_msg true (THM (msg, i, thms)) =
      raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms)
  | exn_msg _ Option = raised "Option" []
  | exn_msg _ UnequalLengths = raised "UnequalLengths" []
  | exn_msg _ Empty = raised "Empty" []
  | exn_msg _ Subscript = raised "Subscript" []
  | exn_msg _ (Fail msg) = raised "Fail" [msg]
  | exn_msg _ exn = General.exnMessage exn
and fail_msg detailed kind ((name, pos), exn) =
  "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn;

in

fun exn_message exn = exn_msg (! debug) exn;

fun print_exn NONE = ()
  | print_exn (SOME (exn, s)) = error_msg (cat_lines [exn_message exn, s]);

end;


(* apply transitions *)

val quiet = ref false;

local

fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =
  let
    val _ = conditional (not int andalso int_only) (fn () =>
      warning (command_msg "Interactive-only " tr));

    fun do_timing f x = (info (command_msg "" tr); timeap f x);
    fun do_profiling f x = profile (! profiling) f x;

    val (result, opt_exn) =
       state |> (apply_trans int trans
        |> (if ! profiling > 0 then do_profiling else I)
        |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
    val _ = conditional (int andalso not (! quiet) andalso
        exists (fn m => m mem_string print) ("" :: ! print_mode))
      (fn () => print_state false result);
  in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;

in

fun apply int tr st =
  (case app int tr st of
    (_, SOME TERMINATE) => NONE
  | (_, SOME RESTART) => SOME (toplevel, NONE)
  | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
  | (state', SOME exn) => SOME (state', SOME (exn, at_command tr))
  | (state', NONE) => SOME (state', NONE));

end;


(* excursion: toplevel -- apply transformers -- toplevel *)

local

fun excur [] x = x
  | excur ((tr, f) :: trs) (st, res) =
      (case apply false tr st of
        SOME (st', NONE) =>
          excur trs (st', transform_error (fn () => f st st' res) () handle exn =>
            raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr))
      | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info
      | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));

in

fun excursion_result (trs, res) =
  (case excur trs (State NONE, res) of
    (State NONE, res') => res'
  | _ => raise ERROR_MESSAGE "Unfinished development at end of input")
  handle exn => error (exn_message exn);

fun excursion trs =
  excursion_result (map (fn tr => (tr, fn _ => fn _ => fn _ => ())) trs, ());

end;



(** interactive transformations **)

(* the global state reference *)

val global_state = ref (toplevel, NONE: (exn * string) option);

fun set_state state = global_state := (state, NONE);
fun get_state () = fst (! global_state);
fun exn () = snd (! global_state);


(* the Isar source of transitions *)

type 'a isar =
  (transition, (transition option,
    (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
      Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
          Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;


(* apply transformers to global state *)

nonfix >> >>>;

fun >> tr =
  (case apply true tr (get_state ()) of
    NONE => false
  | SOME (state', exn_info) =>
      (global_state := (state', exn_info);
        print_exn exn_info;
        true));

fun >>> [] = ()
  | >>> (tr :: trs) = if >> tr then >>> trs else ();

(*Note: this is for Poly/ML only, we really do not intend to exhibit
  interrupts here*)
fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;

fun raw_loop src =
  (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
    NONE => (writeln "\nInterrupt."; raw_loop src)
  | SOME NONE => ()
  | SOME (SOME (tr, src')) => if >> tr then raw_loop src' else ());

fun loop src = ignore_interrupt raw_loop src;

end;