added print_state_hook;
authorwenzelm
Wed Jul 13 16:07:37 2005 +0200 (2005-07-13)
changeset 1681513d20ed9086c
parent 16814 b829a6c9a87a
child 16816 ccf39b7ca3b7
added print_state_hook;
renamed proof'' to actual_proof;
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Jul 13 16:07:36 2005 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Jul 13 16:07:37 2005 +0200
     1.3 @@ -7,17 +7,11 @@
     1.4  
     1.5  signature TOPLEVEL =
     1.6  sig
     1.7 -  datatype node = Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory
     1.8 +  datatype node =
     1.9 +    Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory
    1.10    type state
    1.11    val toplevel: state
    1.12    val is_toplevel: state -> bool
    1.13 -  val prompt_state_default: state -> string
    1.14 -  val prompt_state_fn: (state -> string) ref
    1.15 -  val print_state_context: state -> unit
    1.16 -  val print_state_default: bool -> state -> unit
    1.17 -  val print_state_fn: (bool -> state -> unit) ref
    1.18 -  val print_state: bool -> state -> unit
    1.19 -  val pretty_state: bool -> state -> Pretty.T list
    1.20    exception UNDEF
    1.21    val node_history_of: state -> node History.T
    1.22    val node_of: state -> node
    1.23 @@ -27,10 +21,19 @@
    1.24    val context_of: state -> Proof.context
    1.25    val proof_of: state -> Proof.state
    1.26    val enter_forward_proof: state -> Proof.state
    1.27 +  val prompt_state_default: state -> string
    1.28 +  val prompt_state_fn: (state -> string) ref
    1.29 +  val print_state_context: state -> unit
    1.30 +  val print_state_default: bool -> state -> unit
    1.31 +  val print_state_hook: (bool -> state -> unit) -> unit
    1.32 +  val print_state_fn: (bool -> state -> unit) ref
    1.33 +  val print_state: bool -> state -> unit
    1.34 +  val pretty_state: bool -> state -> Pretty.T list
    1.35    val quiet: bool ref
    1.36    val debug: bool ref
    1.37    val timing: bool ref
    1.38    val profiling: int ref
    1.39 +  val skip_proofs: bool ref
    1.40    exception TERMINATE
    1.41    exception RESTART
    1.42    type transition
    1.43 @@ -55,16 +58,15 @@
    1.44    val imperative: (unit -> unit) -> transition -> transition
    1.45    val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
    1.46      -> transition -> transition
    1.47 -  val skip_proofs: bool ref
    1.48    val theory: (theory -> theory) -> transition -> transition
    1.49    val theory': (bool -> theory -> theory) -> transition -> transition
    1.50    val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
    1.51    val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    1.52    val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
    1.53 -  val proof'': (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    1.54 +  val actual_proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    1.55 +  val skip_proof: (int History.T -> int History.T) -> transition -> transition
    1.56    val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
    1.57    val proof_to_theory': (bool -> ProofHistory.T -> theory) -> transition -> transition
    1.58 -  val skip_proof: (int History.T -> int History.T) -> transition -> transition
    1.59    val skip_proof_to_theory: (int History.T -> bool) -> transition -> transition
    1.60    val unknown_theory: transition -> transition
    1.61    val unknown_proof: transition -> transition
    1.62 @@ -88,32 +90,12 @@
    1.63  
    1.64  (** toplevel state **)
    1.65  
    1.66 -(* datatype node *)
    1.67 +(* datatype state *)
    1.68  
    1.69  datatype node =
    1.70    Theory of theory |
    1.71 -  Proof of ProofHistory.T |
    1.72 -  SkipProof of int History.T * theory;
    1.73 -
    1.74 -fun str_of_node (Theory _) = "in theory mode"
    1.75 -  | str_of_node _ = "in proof mode";
    1.76 -
    1.77 -fun pretty_context thy = [Pretty.block
    1.78 -  [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
    1.79 -    Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
    1.80 -
    1.81 -fun pretty_prf prf = Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf);
    1.82 -
    1.83 -fun pretty_node_context (Theory thy) = pretty_context thy
    1.84 -  | pretty_node_context (Proof prf) = pretty_context (Proof.theory_of (ProofHistory.current prf))
    1.85 -  | pretty_node_context _ = [];
    1.86 -
    1.87 -fun pretty_node prf_only (Theory thy) = if prf_only then [] else pretty_context thy
    1.88 -  | pretty_node _ (Proof prf) = pretty_prf prf
    1.89 -  | pretty_node _ _ = [];
    1.90 -
    1.91 -
    1.92 -(* datatype state *)
    1.93 +  Proof of ProofHistory.T |              (*history of proof states*)
    1.94 +  SkipProof of int History.T * theory;   (*history of proof depths*)
    1.95  
    1.96  datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;
    1.97  
    1.98 @@ -123,36 +105,11 @@
    1.99    | is_toplevel _ = false;
   1.100  
   1.101  fun str_of_state (State NONE) = "at top level"
   1.102 -  | str_of_state (State (SOME (node, _))) = str_of_node (History.current node);
   1.103 -
   1.104 -
   1.105 -(* prompt_state hook *)
   1.106 -
   1.107 -fun prompt_state_default (State _) = Source.default_prompt;
   1.108 -
   1.109 -val prompt_state_fn = ref prompt_state_default;
   1.110 -fun prompt_state state = ! prompt_state_fn state;
   1.111 -
   1.112 -
   1.113 -(* print state *)
   1.114 -
   1.115 -fun pretty_current_node _ (State NONE) = []
   1.116 -  | pretty_current_node prt (State (SOME (node, _))) = prt (History.current node);
   1.117 -
   1.118 -val print_state_context =
   1.119 -  Pretty.writeln o Pretty.chunks o pretty_current_node pretty_node_context;
   1.120 -
   1.121 -fun pretty_state prf_only state =
   1.122 -  let val ref (begin_state, end_state, _) = Display.current_goals_markers in
   1.123 -    (case pretty_current_node (pretty_node prf_only) state of [] => []
   1.124 -    | prts =>
   1.125 -        (if begin_state = "" then [] else [Pretty.str begin_state]) @ prts @
   1.126 -        (if end_state = "" then [] else [Pretty.str end_state]))
   1.127 -  end;
   1.128 -
   1.129 -fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state);
   1.130 -val print_state_fn = ref print_state_default;
   1.131 -fun print_state state = ! print_state_fn state;
   1.132 +  | str_of_state (State (SOME (node, _))) =
   1.133 +      (case History.current node of
   1.134 +        Theory _ => "in theory mode"
   1.135 +      | Proof _ => "in proof mode"
   1.136 +      | SkipProof _ => "in skipped proof mode");
   1.137  
   1.138  
   1.139  (* top node *)
   1.140 @@ -167,8 +124,8 @@
   1.141  fun node_case f g state =
   1.142    (case node_of state of
   1.143      Theory thy => f thy
   1.144 -  | SkipProof (i, thy) => f thy
   1.145 -  | Proof prf => g (ProofHistory.current prf));
   1.146 +  | Proof prf => g (ProofHistory.current prf)
   1.147 +  | SkipProof (_, thy) => f thy);
   1.148  
   1.149  val theory_of = node_case I Proof.theory_of;
   1.150  val sign_of = theory_of;
   1.151 @@ -178,6 +135,51 @@
   1.152  val enter_forward_proof = node_case Proof.init_state Proof.enter_forward;
   1.153  
   1.154  
   1.155 +(* prompt state *)
   1.156 +
   1.157 +fun prompt_state_default (State _) = Source.default_prompt;
   1.158 +
   1.159 +val prompt_state_fn = ref prompt_state_default;
   1.160 +fun prompt_state state = ! prompt_state_fn state;
   1.161 +
   1.162 +
   1.163 +(* print state *)
   1.164 +
   1.165 +fun pretty_context thy = [Pretty.block
   1.166 +  [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
   1.167 +    Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
   1.168 +
   1.169 +fun pretty_state_context state =
   1.170 +  (case try theory_of state of NONE => []
   1.171 +  | SOME thy => pretty_context thy);
   1.172 +
   1.173 +fun pretty_node prf_only (Theory thy) = if prf_only then [] else pretty_context thy
   1.174 +  | pretty_node _ (Proof prf) =
   1.175 +      Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
   1.176 +  | pretty_node _ (SkipProof (h, _)) =
   1.177 +      [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))];
   1.178 +
   1.179 +fun pretty_state prf_only state =
   1.180 +  let val ref (begin_state, end_state, _) = Display.current_goals_markers in
   1.181 +    (case try node_of state of NONE => []
   1.182 +    | SOME node =>
   1.183 +        (if begin_state = "" then [] else [Pretty.str begin_state]) @
   1.184 +        pretty_node prf_only node @
   1.185 +        (if end_state = "" then [] else [Pretty.str end_state]))
   1.186 +  end;
   1.187 +
   1.188 +val print_state_context = Pretty.writelns o pretty_state_context;
   1.189 +fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state);
   1.190 +
   1.191 +val print_state_hooks = ref ([]: (bool -> state -> unit) list);
   1.192 +fun print_state_hook f = change print_state_hooks (cons f);
   1.193 +val print_state_fn = ref print_state_default;
   1.194 +
   1.195 +fun print_state prf_only state =
   1.196 + (List.app (fn f => (try (fn () => f prf_only state) (); ())) (! print_state_hooks);
   1.197 +  ! print_state_fn prf_only state);
   1.198 +
   1.199 +
   1.200  
   1.201  (** toplevel transitions **)
   1.202  
   1.203 @@ -185,6 +187,7 @@
   1.204  val debug = ref false;
   1.205  val timing = Output.timing;
   1.206  val profiling = ref 0;
   1.207 +val skip_proofs = ref false;
   1.208  
   1.209  exception TERMINATE;
   1.210  exception RESTART;
   1.211 @@ -192,31 +195,29 @@
   1.212  exception FAILURE of state * exn;
   1.213  
   1.214  
   1.215 -(* recovery from stale theories *)
   1.216 +(* node transactions and recovery from stale theories *)
   1.217  
   1.218 -(*note: proof commands should be non-destructive!*)
   1.219 +(*NB: proof commands should be non-destructive!*)
   1.220  
   1.221  local
   1.222  
   1.223  fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
   1.224  
   1.225 +val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
   1.226 +
   1.227  fun checkpoint_node true (Theory thy) = Theory (Theory.checkpoint thy)
   1.228    | checkpoint_node _ node = node;
   1.229  
   1.230  fun copy_node true (Theory thy) = Theory (Theory.copy thy)
   1.231    | copy_node _ node = node;
   1.232  
   1.233 -val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
   1.234 -
   1.235  fun return (result, NONE) = result
   1.236    | return (result, SOME exn) = raise FAILURE (result, exn);
   1.237  
   1.238  fun debug_trans f x =
   1.239    if ! debug then
   1.240 -    let val y = ref x in
   1.241 -      setmp Output.transform_exceptions false
   1.242 -        exception_trace (fn () => y := f x); ! y
   1.243 -    end
   1.244 +    setmp Output.transform_exceptions false
   1.245 +      exception_trace (fn () => f x)
   1.246    else f x;
   1.247  
   1.248  fun interruptible f x =
   1.249 @@ -225,8 +226,8 @@
   1.250  
   1.251  in
   1.252  
   1.253 -fun node_trans _ _ _ (State NONE) = raise UNDEF
   1.254 -  | node_trans int hist f (State (SOME (node, term))) =
   1.255 +fun transaction _ _ _ (State NONE) = raise UNDEF
   1.256 +  | transaction int hist f (State (SOME (node, term))) =
   1.257        let
   1.258          val cont_node = History.map (checkpoint_node int) node;
   1.259          val back_node = History.map (copy_node int) cont_node;
   1.260 @@ -254,12 +255,11 @@
   1.261  
   1.262  (* primitive transitions *)
   1.263  
   1.264 -(*Important note: recovery from stale theories is provided only for
   1.265 -  theory-level operations via MapCurrent and AppCurrent.  Other node
   1.266 -  or state operations should not touch theories at all.
   1.267 +(*NB: recovery from stale theories is provided only for theory-level
   1.268 +  operations via MapCurrent and AppCurrent.  Other node or state
   1.269 +  operations should not touch theories at all.
   1.270  
   1.271 -  Also note that interrupts are enabled for Keep, MapCurrent, and
   1.272 -  AppCurrent only.*)
   1.273 +  Interrupts are enabled only for Keep, MapCurrent, and AppCurrent.*)
   1.274  
   1.275  datatype trans =
   1.276    Reset |                                       (*empty toplevel*)
   1.277 @@ -289,8 +289,8 @@
   1.278    | apply_tr int (Keep f) state = (raise_interrupt (f int) state; state)
   1.279    | apply_tr _ (History _) (State NONE) = raise UNDEF
   1.280    | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
   1.281 -  | apply_tr int (MapCurrent f) state = node_trans int false f state
   1.282 -  | apply_tr int (AppCurrent f) state = node_trans int true f state;
   1.283 +  | apply_tr int (MapCurrent f) state = transaction int false f state
   1.284 +  | apply_tr int (AppCurrent f) state = transaction int true f state;
   1.285  
   1.286  fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   1.287    | apply_union int (tr :: trs) state =
   1.288 @@ -311,13 +311,13 @@
   1.289  (* datatype transition *)
   1.290  
   1.291  datatype transition = Transition of
   1.292 - {name: string,
   1.293 -  pos: Position.T,
   1.294 -  source: OuterLex.token list option,
   1.295 -  int_only: bool,
   1.296 -  print: string list,
   1.297 -  no_timing: bool,
   1.298 -  trans: trans list};
   1.299 + {name: string,                        (*command name*)
   1.300 +  pos: Position.T,                     (*source position*)
   1.301 +  source: OuterLex.token list option,  (*source text*)
   1.302 +  int_only: bool,                      (*interactive-only*)
   1.303 +  print: string list,                  (*print modes (union)*)
   1.304 +  no_timing: bool,                     (*suppress timing*)
   1.305 +  trans: trans list};                  (*primitive transitions (union)*)
   1.306  
   1.307  fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
   1.308    Transition {name = name, pos = pos, source = source,
   1.309 @@ -391,14 +391,6 @@
   1.310  
   1.311  (* typed transitions *)
   1.312  
   1.313 -(*The skip_proofs flag allows proof scripts to be skipped during
   1.314 -  interactive proof in order to speed up processing of large
   1.315 -  theories. While in skipping mode, states are represented as
   1.316 -  SkipProof (h, thy), where h contains a counter for the number of
   1.317 -  open proof blocks.*)
   1.318 -
   1.319 -val skip_proofs = ref false;
   1.320 -
   1.321  fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
   1.322  fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));
   1.323  
   1.324 @@ -409,13 +401,18 @@
   1.325          else Proof (f int thy)
   1.326      | _ => raise UNDEF));
   1.327  
   1.328 -fun proof''' b f = map_current (fn int => (fn Proof prf => Proof (f int prf)
   1.329 -  | SkipProof (h, thy) => if b then SkipProof (History.apply I h, thy) else raise UNDEF
   1.330 -  | _ => raise UNDEF));
   1.331 +fun proof' f = map_current (fn int =>
   1.332 +  (fn Proof prf => Proof (f int prf)
   1.333 +    | SkipProof (h, thy) => SkipProof (History.apply I h, thy)   (*approximate f*)
   1.334 +    | _ => raise UNDEF));
   1.335  
   1.336 -val proof' = proof''' true;
   1.337  val proof = proof' o K;
   1.338 -val proof'' = proof''' false o K;
   1.339 +
   1.340 +fun actual_proof f = map_current (fn _ =>
   1.341 +  (fn Proof prf => Proof (f prf) | _ => raise UNDEF));
   1.342 +
   1.343 +fun skip_proof f = map_current (fn _ =>
   1.344 +  (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF));
   1.345  
   1.346  fun proof_to_theory' f =
   1.347    map_current (fn int => (fn Proof prf => Theory (f int prf)
   1.348 @@ -424,10 +421,7 @@
   1.349  
   1.350  val proof_to_theory = proof_to_theory' o K;
   1.351  
   1.352 -fun skip_proof f = map_current (fn int =>
   1.353 -  (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF));
   1.354 -
   1.355 -fun skip_proof_to_theory p = map_current (fn int =>
   1.356 +fun skip_proof_to_theory p = map_current (fn _ =>
   1.357    (fn SkipProof (h, thy) => if p h then Theory thy else raise UNDEF | _ => raise UNDEF));
   1.358  
   1.359  val unknown_theory = imperative (fn () => warning "Unknown theory context");
   1.360 @@ -500,8 +494,6 @@
   1.361  
   1.362  (* apply transitions *)
   1.363  
   1.364 -val quiet = ref false;
   1.365 -
   1.366  local
   1.367  
   1.368  fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =