src/Pure/Isar/toplevel.ML
author wenzelm
Wed Mar 15 18:32:41 2000 +0100 (2000-03-15)
changeset 8465 df6549f5a01f
parent 7732 d62523296573
child 8561 2675e2f4dc61
permissions -rw-r--r--
eliminated toplevel stack;
     1 (*  Title:      Pure/Isar/toplevel.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 The Isabelle/Isar toplevel.
     6 *)
     7 
     8 signature TOPLEVEL =
     9 sig
    10   datatype node = Theory of theory | Proof of ProofHistory.T
    11   type state
    12   val toplevel: state
    13   val is_toplevel: state -> bool
    14   val prompt_state_default: state -> string
    15   val prompt_state_fn: (state -> string) ref
    16   val print_state_context: state -> unit
    17   val print_state_default: state -> unit
    18   val print_state_fn: (state -> unit) ref
    19   val print_state: state -> unit
    20   exception UNDEF
    21   val node_history_of: state -> node History.T
    22   val node_of: state -> node
    23   val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    24   val theory_of: state -> theory
    25   val sign_of: state -> Sign.sg
    26   val context_of: state -> Proof.context
    27   val proof_of: state -> Proof.state
    28   type transition
    29   exception TERMINATE
    30   exception RESTART
    31   val undo_limit: bool -> int option
    32   val empty: transition
    33   val name: string -> transition -> transition
    34   val position: Position.T -> transition -> transition
    35   val interactive: bool -> transition -> transition
    36   val print: transition -> transition
    37   val reset: transition -> transition
    38   val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
    39   val exit: transition -> transition
    40   val kill: transition -> transition
    41   val keep: (state -> unit) -> transition -> transition
    42   val keep': (bool -> state -> unit) -> transition -> transition
    43   val history: (node History.T -> node History.T) -> transition -> transition
    44   val imperative: (unit -> unit) -> transition -> transition
    45   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
    46     -> transition -> transition
    47   val theory: (theory -> theory) -> transition -> transition
    48   val theory': (bool -> theory -> theory) -> transition -> transition
    49   val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
    50   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    51   val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
    52   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
    53   val quiet: bool ref
    54   val trace: bool ref
    55   val exn_message: exn -> string
    56   val apply: bool -> transition -> state -> (state * (exn * string) option) option
    57   val excursion: transition list -> unit
    58   val excursion_error: transition list -> unit
    59   val set_state: state -> unit
    60   val get_state: unit -> state
    61   val exn: unit -> (exn * string) option
    62   val >> : transition -> bool
    63   type isar
    64   val loop: isar -> unit
    65 end;
    66 
    67 structure Toplevel: TOPLEVEL =
    68 struct
    69 
    70 
    71 (** toplevel state **)
    72 
    73 (* datatype node *)
    74 
    75 datatype node =
    76   Theory of theory |
    77   Proof of ProofHistory.T;
    78 
    79 fun str_of_node (Theory _) = "in theory mode"
    80   | str_of_node (Proof _) = "in proof mode";
    81 
    82 fun print_ctxt thy = Pretty.writeln (Pretty.block
    83   [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
    84     Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]);
    85 
    86 fun print_node_ctxt (Theory thy) = print_ctxt thy
    87   | print_node_ctxt (Proof prf) = print_ctxt (Proof.theory_of (ProofHistory.current prf));
    88 
    89 fun print_node (Theory thy) = print_ctxt thy
    90   | print_node (Proof prf) = Proof.print_state (ProofHistory.position prf)
    91       (ProofHistory.current prf);
    92 
    93 
    94 (* datatype state *)
    95 
    96 datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;
    97 
    98 val toplevel = State None;
    99 
   100 fun is_toplevel (State None) = true
   101   | is_toplevel _ = false;
   102 
   103 fun str_of_state (State None) = "at top level"
   104   | str_of_state (State (Some (node, _))) = str_of_node (History.current node);
   105 
   106 
   107 (* prompt_state hook *)
   108 
   109 fun prompt_state_default (State _) = Source.default_prompt;
   110 
   111 val prompt_state_fn = ref prompt_state_default;
   112 fun prompt_state state = ! prompt_state_fn state;
   113 
   114 
   115 (* print state *)
   116 
   117 fun print_current_node _ (State None) = ()
   118   | print_current_node prt (State (Some (node, _))) = prt (History.current node);
   119 
   120 val print_state_context = print_current_node print_node_ctxt;
   121 
   122 fun print_state_default state =
   123   let val ref (begin_state, end_state, _) = Goals.current_goals_markers in
   124     if begin_state = "" then () else writeln begin_state;
   125     print_current_node print_node state;
   126     if end_state = "" then () else writeln end_state
   127   end;
   128 
   129 val print_state_fn = ref print_state_default;
   130 fun print_state state = ! print_state_fn state;
   131 
   132 
   133 (* top node *)
   134 
   135 exception UNDEF;
   136 
   137 fun node_history_of (State None) = raise UNDEF
   138   | node_history_of (State (Some (node, _))) = node;
   139 
   140 val node_of = History.current o node_history_of;
   141 
   142 fun node_case f g state =
   143   (case node_of state of
   144     Theory thy => f thy
   145   | Proof prf => g (ProofHistory.current prf));
   146 
   147 val theory_of = node_case I Proof.theory_of;
   148 val context_of = node_case ProofContext.init Proof.context_of;
   149 val sign_of = Theory.sign_of o theory_of;
   150 val proof_of = node_case (fn _ => raise UNDEF) I;
   151 
   152 
   153 
   154 (** toplevel transitions **)
   155 
   156 exception TERMINATE;
   157 exception RESTART;
   158 exception EXCURSION_FAIL of exn * string;
   159 exception FAILURE of state * exn;
   160 
   161 
   162 (* recovery from stale signatures *)
   163 
   164 (*note: proof commands should be non-destructive!*)
   165 
   166 local
   167 
   168 fun is_stale state = Sign.is_stale (sign_of state) handle UNDEF => false;
   169 
   170 fun checkpoint_node true (Theory thy) = Theory (PureThy.checkpoint thy)
   171   | checkpoint_node _ node = node;
   172 
   173 fun copy_node true (Theory thy) = Theory (Theory.copy thy)
   174   | copy_node _ node = node;
   175 
   176 fun interruptible f x =
   177   let val y = ref (None: node History.T option);
   178   in exhibit_interrupt (fn () => y := Some (f x)) (); the (! y) end;
   179 
   180 val rollback = ERROR_MESSAGE "Stale signature encountered after succesful execution!";
   181 
   182 fun return (result, None) = result
   183   | return (result, Some exn) = raise FAILURE (result, exn);
   184 
   185 in
   186 
   187 fun node_trans _ _ _ (State None) = raise UNDEF
   188   | node_trans int hist f (State (Some (node, term))) =
   189       let
   190         fun mk_state nd = State (Some (nd, term));
   191 
   192         val cont_node = History.map (checkpoint_node int) node;
   193         val back_node = History.map (copy_node int) cont_node;
   194 
   195         val trans = if hist then History.apply_copy (copy_node int) else History.map;
   196         val (result, opt_exn) =
   197           (mk_state (transform_error (interruptible (trans (f int))) cont_node), None)
   198             handle exn => (mk_state cont_node, Some exn);
   199       in
   200         if is_stale result then return (mk_state back_node, Some (if_none opt_exn rollback))
   201         else return (result, opt_exn)
   202       end;
   203 
   204 fun check_stale state =
   205   if not (is_stale state) then ()
   206   else warning "Stale signature encountered!  Should restart current theory.";
   207 
   208 end;
   209 
   210 
   211 (* primitive transitions *)
   212 
   213 (*Important note: recovery from stale signatures is provided only for
   214   theory-level operations via MapCurrent and AppCurrent.  Other node
   215   or state operations should not touch signatures at all.
   216 
   217   Also note that interrupts are enabled for Keep, MapCurrent, and
   218   AppCurrent only.*)
   219 
   220 datatype trans =
   221   Reset |                                       (*empty toplevel*)
   222   Init of (bool -> node) * ((node -> unit) * (node -> unit)) |
   223     (*init node; provide exit/kill operation*)
   224   Exit |                                        (*conclude node*)
   225   Kill |                                        (*abort node*)
   226   Keep of bool -> state -> unit |               (*peek at state*)
   227   History of node History.T -> node History.T | (*history operation (undo etc.)*)
   228   MapCurrent of bool -> node -> node |          (*change node, bypassing history*)
   229   AppCurrent of bool -> node -> node;           (*change node, recording history*)
   230 
   231 fun undo_limit int = if int then None else Some 0;
   232 
   233 local
   234 
   235 fun apply_tr _ Reset _ = toplevel
   236   | apply_tr int (Init (f, term)) (State None) =
   237       State (Some (History.init (undo_limit int) (f int), term))
   238   | apply_tr _ (Init _ ) (State (Some _)) = raise UNDEF
   239   | apply_tr _ Exit (State None) = raise UNDEF
   240   | apply_tr _ Exit (State (Some (node, (exit, _)))) =
   241       (exit (History.current node); State None)
   242   | apply_tr _ Kill (State None) = raise UNDEF
   243   | apply_tr _ Kill (State (Some (node, (_, kill)))) =
   244       (kill (History.current node); State None)
   245   | apply_tr int (Keep f) state = (exhibit_interrupt (f int) state; state)
   246   | apply_tr _ (History _) (State None) = raise UNDEF
   247   | apply_tr _ (History f) (State (Some (node, term))) = State (Some (f node, term))
   248   | apply_tr int (MapCurrent f) state = node_trans int false f state
   249   | apply_tr int (AppCurrent f) state = node_trans int true f state;
   250 
   251 fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   252   | apply_union int (tr :: trs) state =
   253       transform_error (apply_tr int tr) state
   254         handle UNDEF => apply_union int trs state
   255           | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
   256           | exn as FAILURE _ => raise exn
   257           | exn => raise FAILURE (state, exn);
   258 
   259 in
   260 
   261 fun apply_trans int trs state = (apply_union int trs state, None)
   262   handle FAILURE (alt_state, exn) => (alt_state, Some exn) | exn => (state, Some exn);
   263 
   264 end;
   265 
   266 
   267 (* datatype transition *)
   268 
   269 datatype transition = Transition of
   270  {name: string,
   271   pos: Position.T,
   272   int_only: bool,
   273   print: bool,
   274   trans: trans list};
   275 
   276 fun make_transition (name, pos, int_only, print, trans) =
   277   Transition {name = name, pos = pos, int_only = int_only, print = print, trans = trans};
   278 
   279 fun map_transition f (Transition {name, pos, int_only, print, trans}) =
   280   make_transition (f (name, pos, int_only, print, trans));
   281 
   282 val empty = make_transition ("<unknown>", Position.none, false, false, []);
   283 
   284 
   285 (* diagnostics *)
   286 
   287 fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
   288 
   289 fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr;
   290 fun at_command tr = command_msg "At " tr ^ ".";
   291 
   292 fun type_error tr state =
   293   ERROR_MESSAGE (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
   294 
   295 
   296 (* modify transitions *)
   297 
   298 fun name nm = map_transition
   299   (fn (_, pos, int_only, print, trans) => (nm, pos, int_only, print, trans));
   300 
   301 fun position pos = map_transition
   302   (fn (name, _, int_only, print, trans) => (name, pos, int_only, print, trans));
   303 
   304 fun interactive int_only = map_transition
   305   (fn (name, pos, _, print, trans) => (name, pos, int_only, print, trans));
   306 
   307 val print = map_transition
   308   (fn (name, pos, int_only, _, trans) => (name, pos, int_only, true, trans));
   309 
   310 fun add_trans tr = map_transition
   311   (fn (name, pos, int_only, print, trans) => (name, pos, int_only, print, trans @ [tr]));
   312 
   313 
   314 (* build transitions *)
   315 
   316 val reset = add_trans Reset;
   317 fun init f exit kill = add_trans (Init (f, (exit, kill)));
   318 val exit = add_trans Exit;
   319 val kill = add_trans Kill;
   320 val keep' = add_trans o Keep;
   321 val history = add_trans o History;
   322 val map_current = add_trans o MapCurrent;
   323 val app_current = add_trans o AppCurrent;
   324 
   325 fun keep f = add_trans (Keep (fn _ => f));
   326 fun imperative f = keep (fn _ => f ());
   327 
   328 fun init_theory f exit kill =
   329   init (fn int => Theory (f int))
   330     (fn Theory thy => exit thy | _ => raise UNDEF)
   331     (fn Theory thy => kill thy | _ => raise UNDEF);
   332 
   333 fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
   334 fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));
   335 fun theory_to_proof f =
   336   app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF));
   337 fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF));
   338 val proof = proof' o K;
   339 fun proof_to_theory f = map_current (fn _ => (fn Proof prf => Theory (f prf) | _ => raise UNDEF));
   340 
   341 
   342 
   343 (** toplevel transactions **)
   344 
   345 val quiet = ref false;
   346 val trace = ref false;
   347 
   348 
   349 (* print exceptions *)
   350 
   351 fun raised name = "exception " ^ name ^ " raised";
   352 fun raised_msg name msg = raised name ^ ": " ^ msg;
   353 
   354 fun exn_message TERMINATE = "Exit."
   355   | exn_message RESTART = "Restart."
   356   | exn_message (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
   357   | exn_message Interrupt = "Interrupt."
   358   | exn_message ERROR = "ERROR."
   359   | exn_message (ERROR_MESSAGE msg) = msg
   360   | exn_message (THEORY (msg, _)) = msg
   361   | exn_message (ProofContext.CONTEXT (msg, _)) = msg
   362   | exn_message (Proof.STATE (msg, _)) = msg
   363   | exn_message (ProofHistory.FAIL msg) = msg
   364   | exn_message (Attrib.ATTRIB_FAIL info) = fail_message "attribute" info
   365   | exn_message (Method.METHOD_FAIL info) = fail_message "method" info
   366   | exn_message (Syntax.AST (msg, _)) = raised_msg "AST" msg
   367   | exn_message (TYPE (msg, _, _)) = raised_msg "TYPE" msg
   368   | exn_message (TERM (msg, _)) = raised_msg "TERM" msg
   369   | exn_message (THM (msg, _, _)) = raised_msg "THM" msg
   370   | exn_message Library.OPTION = raised "Library.OPTION"
   371   | exn_message (Library.LIST msg) = raised_msg "Library.LIST" msg
   372   | exn_message exn = General.exnMessage exn
   373 and fail_message kind ((name, pos), exn) =
   374   "Error in " ^ kind ^ " " ^ name ^ Position.str_of pos ^ ":\n" ^ exn_message exn;
   375 
   376 fun print_exn None = ()
   377   | print_exn (Some (exn, s)) = error_msg (cat_lines [exn_message exn, s]);
   378 
   379 
   380 (* apply transitions *)
   381 
   382 local
   383 
   384 fun app int (tr as Transition {trans, int_only, print, ...}) state =
   385   let
   386     val _ =
   387       if int orelse not int_only then ()
   388       else warning (command_msg "Executing interactive-only " tr);
   389     val (result, opt_exn) =
   390       (if ! trace then (writeln (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
   391     val _ = if int andalso print andalso not (! quiet) then print_state result else ();
   392   in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
   393 
   394 in
   395 
   396 fun apply int tr st =
   397   (case app int tr st of
   398     (_, Some TERMINATE) => None
   399   | (_, Some RESTART) => Some (toplevel, None)
   400   | (state', Some (EXCURSION_FAIL exn_info)) => Some (state', Some exn_info)
   401   | (state', Some exn) => Some (state', Some (exn, at_command tr))
   402   | (state', None) => Some (state', None));
   403 
   404 end;
   405 
   406 
   407 (* excursion: toplevel -- apply transformers -- toplevel *)
   408 
   409 local
   410 
   411 fun excur [] x = x
   412   | excur (tr :: trs) x =
   413       (case apply false tr x of
   414         Some (x', None) => excur trs x'
   415       | Some (x', Some exn_info) => raise EXCURSION_FAIL exn_info
   416       | None => raise EXCURSION_FAIL (TERMINATE, at_command tr));
   417 
   418 in
   419 
   420 fun excursion trs =
   421   (case excur trs (State None) of
   422     State None => ()
   423   | _ => raise ERROR_MESSAGE "Unfinished development at end of input");
   424 
   425 fun excursion_error trs =
   426   excursion trs handle exn => error (exn_message exn);
   427 
   428 end;
   429 
   430 
   431 
   432 (** interactive transformations **)
   433 
   434 (* the global state reference *)
   435 
   436 val global_state = ref (toplevel, None: (exn * string) option);
   437 
   438 fun set_state state = global_state := (state, None);
   439 fun get_state () = fst (! global_state);
   440 fun exn () = snd (! global_state);
   441 
   442 
   443 (* the Isar source of transitions *)
   444 
   445 type isar =
   446   (transition, (transition option,
   447     (OuterLex.token, (OuterLex.token,
   448       Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
   449           Source.source) Source.source) Source.source) Source.source;
   450 
   451 
   452 (* apply transformers to global state *)
   453 
   454 nonfix >>;
   455 
   456 fun >> tr =
   457   (case apply true tr (get_state ()) of
   458     None => false
   459   | Some (state', exn_info) =>
   460       (global_state := (state', exn_info);
   461         check_stale state'; print_exn exn_info;
   462         true));
   463 
   464 (*Note: this is for Poly/ML only, we really do not intend to exhibit
   465   interrupts here*)
   466 fun get_interrupt src = Some (Source.get_single src) handle Interrupt => None;
   467 
   468 fun raw_loop src =
   469   (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
   470     None => (writeln "\nInterrupt."; raw_loop src)
   471   | Some None => ()
   472   | Some (Some (tr, src')) => if >> tr then raw_loop src' else ());
   473 
   474 
   475 fun loop src = mask_interrupt raw_loop src;
   476 
   477 
   478 end;