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