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