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