(*  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;

fun interruptible f x =

  let val y = ref (NONE: node History.T option);

  in raise_interrupt (fn () => y := SOME (f x)) (); the (! y) end;

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

fun return (result, NONE) = result

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

in

fun node_trans _ _ _ (State NONE) = raise UNDEF

  | node_trans int hist f (State (SOME (node, term))) =

      let

        fun mk_state nd = State (SOME (nd, term));

        val cont_node = History.map (checkpoint_node int) node;

        val back_node = History.map (copy_node int) cont_node;

        val trans = if hist then History.apply_copy (copy_node int) else History.map;

        val (result, opt_exn) =

          (mk_state (transform_error (interruptible (trans (f int))) cont_node), NONE)

            handle exn => (mk_state cont_node, SOME exn);

      in

        if is_stale result then return (mk_state back_node, SOME (if_none opt_exn rollback))

        else return (result, opt_exn)

      end;

fun check_stale state =

  conditional (is_stale state) (fn () => warning "Stale theory encountered!");

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

val debug = ref false;

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) =

      (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)

        ((if ! profiling > 0 then do_profiling else I) (apply_trans int trans)) state;

    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);

        check_stale state'; 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;