Some changes to allow skipping of proof scripts.
authorberghofe
Mon Oct 11 10:51:19 2004 +0200 (2004-10-11)
changeset 15237250e9be7a09d
parent 15236 f289e8ba2bb3
child 15238 cb559bd0b03c
Some changes to allow skipping of proof scripts.
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Oct 11 07:42:22 2004 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Oct 11 10:51:19 2004 +0200
     1.3 @@ -129,15 +129,18 @@
     1.4  
     1.5  fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
     1.6  val clear_undos_theory = Toplevel.history o History.clear;
     1.7 -val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
     1.8 +val redo = Toplevel.history History.redo o Toplevel.proof'' ProofHistory.redo o
     1.9 +  Toplevel.skip_proof History.redo;
    1.10  
    1.11 -fun undos_proof n = Toplevel.proof (fn prf =>
    1.12 -  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf);
    1.13 +fun undos_proof n = Toplevel.proof'' (fn prf =>
    1.14 +    if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o
    1.15 +  Toplevel.skip_proof (fn h =>
    1.16 +    if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h);
    1.17  
    1.18  fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist =>
    1.19    (case History.current hist of
    1.20      Toplevel.Theory _ => raise Toplevel.UNDEF
    1.21 -  | Toplevel.Proof _ => (f (); History.undo hist)));
    1.22 +  | _ => (f (); History.undo hist)));
    1.23  
    1.24  val kill_proof = kill_proof_notify (K ());
    1.25  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Oct 11 07:42:22 2004 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Oct 11 10:51:19 2004 +0200
     2.3 @@ -483,7 +483,8 @@
     2.4  
     2.5  val proofP =
     2.6    OuterSyntax.command "proof" "backward proof" K.prf_block
     2.7 -    (Scan.option P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
     2.8 +    (Scan.option P.method >> (fn m => Toplevel.print o Toplevel.proof (IsarThy.proof m) o
     2.9 +      Toplevel.skip_proof (History.apply (fn i => i + 1))));
    2.10  
    2.11  
    2.12  (* calculational proof commands *)
     3.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Oct 11 07:42:22 2004 +0200
     3.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Oct 11 10:51:19 2004 +0200
     3.3 @@ -446,6 +446,8 @@
     3.4  (* local endings *)
     3.5  
     3.6  val local_qed = proof'' o (ProofHistory.applys oo Method.local_qed true);
     3.7 +val skip_local_qed =
     3.8 +  Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF));
     3.9  val local_terminal_proof = proof'' o (ProofHistory.applys oo Method.local_terminal_proof);
    3.10  val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
    3.11  val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
    3.12 @@ -469,6 +471,7 @@
    3.13    end);
    3.14  
    3.15  fun global_qed m = global_result (K (Method.global_qed true m));
    3.16 +val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1 o History.current);
    3.17  fun global_terminal_proof m = global_result (K (Method.global_terminal_proof m));
    3.18  val global_default_proof = global_result (K Method.global_default_proof);
    3.19  val global_immediate_proof = global_result (K Method.global_immediate_proof);
    3.20 @@ -478,13 +481,14 @@
    3.21  
    3.22  (* common endings *)
    3.23  
    3.24 -fun qed meth = local_qed meth o global_qed meth;
    3.25 +fun qed meth = local_qed meth o global_qed meth o skip_local_qed o skip_global_qed;
    3.26  fun terminal_proof meths = local_terminal_proof meths o global_terminal_proof meths;
    3.27  val default_proof = local_default_proof o global_default_proof;
    3.28  val immediate_proof = local_immediate_proof o global_immediate_proof;
    3.29  val done_proof = local_done_proof o global_done_proof;
    3.30  val skip_proof = local_skip_proof o global_skip_proof;
    3.31 -val forget_proof = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
    3.32 +val forget_proof = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current) o
    3.33 +  Toplevel.skip_proof_to_theory (K true);
    3.34  
    3.35  
    3.36  (* calculational proof commands *)
     4.1 --- a/src/Pure/Isar/toplevel.ML	Mon Oct 11 07:42:22 2004 +0200
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Oct 11 10:51:19 2004 +0200
     4.3 @@ -8,6 +8,7 @@
     4.4  signature TOPLEVEL =
     4.5  sig
     4.6    datatype node = Theory of theory | Proof of ProofHistory.T
     4.7 +    | SkipProof of int History.T * theory
     4.8    type state
     4.9    val toplevel: state
    4.10    val is_toplevel: state -> bool
    4.11 @@ -50,13 +51,17 @@
    4.12    val imperative: (unit -> unit) -> transition -> transition
    4.13    val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
    4.14      -> transition -> transition
    4.15 +  val skip_proofs: bool ref
    4.16    val theory: (theory -> theory) -> transition -> transition
    4.17    val theory': (bool -> theory -> theory) -> transition -> transition
    4.18    val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
    4.19    val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    4.20    val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
    4.21 +  val proof'': (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    4.22    val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
    4.23    val proof_to_theory': (bool -> ProofHistory.T -> theory) -> transition -> transition
    4.24 +  val skip_proof: (int History.T -> int History.T) -> transition -> transition
    4.25 +  val skip_proof_to_theory: (int History.T -> bool) -> transition -> transition
    4.26    val unknown_theory: transition -> transition
    4.27    val unknown_proof: transition -> transition
    4.28    val unknown_context: transition -> transition
    4.29 @@ -84,10 +89,11 @@
    4.30  
    4.31  datatype node =
    4.32    Theory of theory |
    4.33 -  Proof of ProofHistory.T;
    4.34 +  Proof of ProofHistory.T |
    4.35 +  SkipProof of int History.T * theory;
    4.36  
    4.37  fun str_of_node (Theory _) = "in theory mode"
    4.38 -  | str_of_node (Proof _) = "in proof mode";
    4.39 +  | str_of_node _ = "in proof mode";
    4.40  
    4.41  fun pretty_context thy = [Pretty.block
    4.42    [Pretty.str "theory", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
    4.43 @@ -96,10 +102,12 @@
    4.44  fun pretty_prf prf = Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf);
    4.45  
    4.46  fun pretty_node_context (Theory thy) = pretty_context thy
    4.47 -  | pretty_node_context (Proof prf) = pretty_context (Proof.theory_of (ProofHistory.current prf));
    4.48 +  | pretty_node_context (Proof prf) = pretty_context (Proof.theory_of (ProofHistory.current prf))
    4.49 +  | pretty_node_context _ = [];
    4.50  
    4.51  fun pretty_node prf_only (Theory thy) = if prf_only then [] else pretty_context thy
    4.52 -  | pretty_node _ (Proof prf) = pretty_prf prf;
    4.53 +  | pretty_node _ (Proof prf) = pretty_prf prf
    4.54 +  | pretty_node _ _ = [];
    4.55  
    4.56  
    4.57  (* datatype state *)
    4.58 @@ -156,6 +164,7 @@
    4.59  fun node_case f g state =
    4.60    (case node_of state of
    4.61      Theory thy => f thy
    4.62 +  | SkipProof (i, thy) => f thy
    4.63    | Proof prf => g (ProofHistory.current prf));
    4.64  
    4.65  val theory_of = node_case I Proof.theory_of;
    4.66 @@ -357,15 +366,38 @@
    4.67      (fn Theory thy => exit thy | _ => raise UNDEF)
    4.68      (fn Theory thy => kill thy | _ => raise UNDEF);
    4.69  
    4.70 +(*
    4.71 +The skip_proofs flag allows proof scripts to be skipped during interactive
    4.72 +proof in order to speed up processing of large theories. While in skipping
    4.73 +mode, states are represented as SkipProof (h, thy), where h contains a
    4.74 +counter for the number of open proof blocks.
    4.75 +*)
    4.76 +
    4.77 +val skip_proofs = ref false;
    4.78 +
    4.79  fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
    4.80  fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));
    4.81 -fun theory_to_proof f =
    4.82 -  app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF));
    4.83 -fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF));
    4.84 +fun theory_to_proof f = app_current (fn int =>
    4.85 +  (fn Theory thy =>
    4.86 +        if !skip_proofs then SkipProof (History.init (undo_limit int) 0,
    4.87 +          fst (SkipProof.global_skip_proof int (ProofHistory.current (f int thy))))
    4.88 +        else Proof (f int thy)
    4.89 +    | _ => raise UNDEF));
    4.90 +fun proof''' b f = map_current (fn int => (fn Proof prf => Proof (f int prf)
    4.91 +  | SkipProof (h, thy) => if b then SkipProof (History.apply I h, thy) else raise UNDEF
    4.92 +  | _ => raise UNDEF));
    4.93 +val proof' = proof''' true;
    4.94  val proof = proof' o K;
    4.95 +val proof'' = proof''' false o K;
    4.96  fun proof_to_theory' f =
    4.97 -  map_current (fn int => (fn Proof prf => Theory (f int prf) | _ => raise UNDEF));
    4.98 +  map_current (fn int => (fn Proof prf => Theory (f int prf)
    4.99 +    | SkipProof (h, thy) => if History.current h = 0 then Theory thy else raise UNDEF
   4.100 +    | _ => raise UNDEF));
   4.101  val proof_to_theory = proof_to_theory' o K;
   4.102 +fun skip_proof f = map_current (fn int =>
   4.103 +  (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF));
   4.104 +fun skip_proof_to_theory p = map_current (fn int =>
   4.105 +  (fn SkipProof (h, thy) => if p h then Theory thy else raise UNDEF | _ => raise UNDEF));
   4.106  
   4.107  val unknown_theory = imperative (fn () => warning "Unknown theory context");
   4.108  val unknown_proof = imperative (fn () => warning "Unknown proof context");