--- a/src/Pure/Isar/toplevel.ML Wed Oct 11 00:27:37 2006 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Oct 11 00:27:38 2006 +0200
@@ -8,11 +8,12 @@
signature TOPLEVEL =
sig
exception UNDEF
+ type generic_theory
type node
- val theory_node: node -> theory option
+ val theory_node: node -> generic_theory option
val proof_node: node -> ProofHistory.T option
- val cases_node: (theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
- val body_context_node: node option -> xstring option -> Proof.context
+ val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
+ val presentation_context: node option -> xstring option -> Proof.context
type state
val toplevel: state
val is_toplevel: state -> bool
@@ -22,7 +23,7 @@
val assert: bool -> unit
val node_history_of: state -> node History.T
val node_of: state -> node
- val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
+ val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
val context_of: state -> Context.generic
val theory_of: state -> theory
val proof_of: state -> Proof.state
@@ -47,7 +48,6 @@
val exn_message: exn -> string
val program: (unit -> 'a) -> 'a
val checkpoint: state -> state
- val copy: state -> state
type transition
val undo_limit: bool -> int option
val empty: transition
@@ -74,9 +74,10 @@
-> transition -> transition
val theory: (theory -> theory) -> transition -> transition
val theory': (bool -> theory -> theory) -> transition -> transition
- val theory_context: (theory -> Proof.context * theory) -> transition -> transition
- val local_theory: xstring option -> (local_theory -> local_theory) ->
- transition -> transition
+ val exit_local_theory: transition -> transition
+ val begin_local_theory: bool -> (theory -> string * local_theory) -> transition -> transition
+ val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
+ val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
val theory_to_proof: (theory -> Proof.state) -> transition -> transition
val proof: (Proof.state -> Proof.state) -> transition -> transition
val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
@@ -84,13 +85,9 @@
val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
val actual_proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
val skip_proof: (int History.T -> int History.T) -> transition -> transition
- val proof_to_theory: (Proof.state -> theory) -> transition -> transition
- val proof_to_theory': (bool -> Proof.state -> theory) -> transition -> transition
- val proof_to_theory_context: (bool -> Proof.state -> Proof.context * theory)
- -> transition -> transition
val skip_proof_to_theory: (int -> bool) -> transition -> transition
val forget_proof: transition -> transition
- val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
+ val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
val present_proof: (bool -> node -> unit) -> transition -> transition
val unknown_theory: transition -> transition
val unknown_proof: transition -> transition
@@ -110,7 +107,6 @@
structure Toplevel: TOPLEVEL =
struct
-
(** toplevel state **)
exception UNDEF;
@@ -118,25 +114,26 @@
(* datatype state *)
+type generic_theory = Context.generic; (*theory or local_theory*)
+
datatype node =
- Theory of theory * Proof.context option | (*theory with optional body context*)
- Proof of ProofHistory.T * theory | (*history of proof states, original theory*)
- SkipProof of (int History.T * theory) * theory;
+ Theory of generic_theory * Proof.context option | (*theory with presentation context*)
+ Proof of ProofHistory.T * generic_theory | (*history of proof states, original theory*)
+ SkipProof of (int History.T * generic_theory) * generic_theory;
(*history of proof depths, resulting theory, original theory*)
-val theory_node = fn Theory (thy, _) => SOME thy | _ => NONE;
+val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
-fun cases_node f _ (Theory (thy, _)) = f thy
+fun cases_node f _ (Theory (gthy, _)) = f gthy
| cases_node _ g (Proof (prf, _)) = g (ProofHistory.current prf)
- | cases_node f _ (SkipProof ((_, thy), _)) = f thy;
+ | cases_node f _ (SkipProof ((_, gthy), _)) = f gthy;
-fun body_context_node (SOME (Theory (_, SOME ctxt))) NONE = ctxt
- | body_context_node (SOME node) loc =
- node |> cases_node (TheoryTarget.init loc)
- (if is_some loc then TheoryTarget.init loc o Proof.theory_of
- else Proof.context_of)
- | body_context_node NONE _ = raise UNDEF;
+fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt
+ | presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node
+ | presentation_context (SOME node) (SOME loc) =
+ TheoryTarget.init (SOME loc) (cases_node Context.theory_of Proof.theory_of node)
+ | presentation_context NONE _ = raise UNDEF;
datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;
@@ -148,14 +145,16 @@
fun level (State NONE) = 0
| level (State (SOME (node, _))) =
(case History.current node of
- Theory _ => 0
- | Proof (prf, _) => Proof.level (ProofHistory.current prf)
- | SkipProof ((h, _), _) => History.current h + 1); (*different notion of proof depth!*)
+ Theory (Context.Theory _, _) => 0
+ | Theory (Context.Proof _, _) => 1
+ | Proof (prf, _) => Proof.level (ProofHistory.current prf) + 1
+ | SkipProof ((h, _), _) => History.current h + 2); (*different notion of proof depth!*)
fun str_of_state (State NONE) = "at top level"
| str_of_state (State (SOME (node, _))) =
(case History.current node of
- Theory _ => "in theory mode"
+ Theory (Context.Theory _, _) => "in theory mode"
+ | Theory (Context.Proof _, _) => "in local theory mode"
| Proof _ => "in proof mode"
| SkipProof _ => "in skipped proof mode");
@@ -175,8 +174,8 @@
fun node_case f g state = cases_node f g (node_of state);
-val context_of = node_case Context.Theory (Context.Proof o Proof.context_of);
-val theory_of = node_case I Proof.theory_of;
+val context_of = node_case I (Context.Proof o Proof.context_of);
+val theory_of = node_case Context.theory_of Proof.theory_of;
val proof_of = node_case (fn _ => raise UNDEF) I;
fun proof_position_of state =
@@ -184,7 +183,7 @@
Proof (prf, _) => ProofHistory.position prf
| _ => raise UNDEF);
-val enter_forward_proof = node_case (Proof.init o ProofContext.init) Proof.enter_forward;
+val enter_forward_proof = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
(* prompt state *)
@@ -197,15 +196,13 @@
(* print state *)
-fun pretty_context thy = [Pretty.block
- [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
- Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
+val pretty_context = LocalTheory.pretty o Context.cases (TheoryTarget.init NONE) I;
fun pretty_state_context state =
- (case try theory_of state of NONE => []
- | SOME thy => pretty_context thy);
+ (case try context_of state of NONE => []
+ | SOME gthy => pretty_context gthy);
-fun pretty_node prf_only (Theory (thy, _)) = if prf_only then [] else pretty_context thy
+fun pretty_node prf_only (Theory (gthy, _)) = if prf_only then [] else pretty_context gthy
| pretty_node _ (Proof (prf, _)) =
Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
| pretty_node _ (SkipProof ((h, _), _)) =
@@ -343,12 +340,10 @@
val stale_theory = ERROR "Stale theory encountered after succesful execution!";
-fun checkpoint_node (Theory (thy, _)) = Theory (Theory.checkpoint thy, NONE)
+fun checkpoint_node (Theory (gthy, _)) = Theory
+ (Context.mapping Theory.checkpoint (LocalTheory.raw_theory Theory.checkpoint) gthy, NONE)
| checkpoint_node node = node;
-fun copy_node (Theory (thy, _)) = Theory (Theory.copy thy, NONE)
- | copy_node node = node;
-
fun return (result, NONE) = result
| return (result, SOME exn) = raise FAILURE (result, exn);
@@ -357,7 +352,7 @@
fun transaction hist f (node, term) =
let
val cont_node = History.map checkpoint_node node;
- val back_node = History.map copy_node cont_node;
+ val back_node = History.map checkpoint_node cont_node;
fun state nd = State (SOME (nd, term));
fun normal_state nd = (state nd, NONE);
fun error_state nd exn = (state nd, SOME exn);
@@ -365,7 +360,7 @@
val (result, err) =
cont_node
|> (f
- |> (if hist then History.apply_copy copy_node else History.map)
+ |> (if hist then History.apply_copy checkpoint_node else History.map)
|> controlled_execution)
|> normal_state
handle exn => error_state cont_node exn;
@@ -379,7 +374,6 @@
| mapping _ state = state;
val checkpoint = mapping checkpoint_node;
-val copy = mapping copy_node;
end;
@@ -518,26 +512,51 @@
fun imperative f = keep (fn _ => f ());
fun init_theory f exit kill =
- init (fn int => Theory (f int, NONE))
- (fn Theory (thy, _) => exit thy | _ => raise UNDEF)
- (fn Theory (thy, _) => kill thy | _ => raise UNDEF);
+ init (fn int => Theory (Context.Theory (f int), NONE))
+ (fn Theory (Context.Theory thy, _) => exit thy | _ => raise UNDEF)
+ (fn Theory (Context.Theory thy, _) => kill thy | _ => raise UNDEF);
(* typed transitions *)
-fun theory f = app_current
- (K (fn Theory (thy, _) => Theory (f thy, NONE) | _ => raise UNDEF));
+fun theory' f = app_current (fn int =>
+ (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
+ | _ => raise UNDEF));
+
+fun theory f = theory' (K f);
+
+val exit_local_theory = app_current (fn _ =>
+ (fn Theory (Context.Proof lthy, _) =>
+ let val (ctxt', thy') = TheoryTarget.exit lthy
+ in Theory (Context.Theory thy', SOME ctxt') end
+ | _ => raise UNDEF));
-fun theory' f = app_current (fn int =>
- (fn Theory (thy, _) => Theory (f int thy, NONE) | _ => raise UNDEF));
+fun begin_local_theory begin f = app_current (fn _ =>
+ (fn Theory (Context.Theory thy, _) =>
+ let
+ val lthy = thy |> f |-> TheoryTarget.begin;
+ val (ctxt, gthy) =
+ if begin then (lthy, Context.Proof lthy)
+ else lthy |> TheoryTarget.exit ||> Context.Theory;
+ in Theory (gthy, SOME ctxt) end
+ | _ => raise UNDEF));
-fun theory_context f = app_current
- (K (fn Theory (thy, _) => Theory (swap (apfst SOME (f thy))) | _ => raise UNDEF));
+fun local_theory_presentation loc f g = app_current (fn int =>
+ (fn Theory (Context.Theory thy, _) =>
+ let val (ctxt', thy') = TheoryTarget.mapping loc f thy
+ in Theory (Context.Theory thy', SOME ctxt') end
+ | Theory (Context.Proof lthy, _) =>
+ let val (ctxt', lthy') =
+ if is_none loc then f lthy |> (fn lthy' => (lthy', LocalTheory.reinit lthy'))
+ else lthy |> LocalTheory.raw_theory_result (TheoryTarget.mapping loc f)
+ in Theory (Context.Proof lthy', SOME ctxt') end
+ | _ => raise UNDEF) #> tap (g int));
-fun local_theory loc f = theory_context (TheoryTarget.mapping loc f);
+fun local_theory loc f = local_theory_presentation loc f (K I);
+fun present_local_theory loc g = local_theory_presentation loc I g;
fun theory_to_proof f = app_current (fn int =>
- (fn Theory (thy, _) =>
+ (fn Theory (gthy as Context.Theory thy, _) =>
let
val prf = f thy;
val schematic = Proof.schematic_goal prf;
@@ -547,14 +566,14 @@
else ();
if ! skip_proofs andalso not schematic then
SkipProof ((History.init (undo_limit int) 0,
- ProofContext.theory_of (Proof.global_skip_proof int prf)), thy)
- else Proof (ProofHistory.init (undo_limit int) prf, thy)
+ Context.Theory (ProofContext.theory_of (Proof.global_skip_proof int prf))), gthy)
+ else Proof (ProofHistory.init (undo_limit int) prf, gthy)
end
| _ => raise UNDEF));
fun proofs' f = map_current (fn int =>
- (fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy)
- | SkipProof ((h, thy), orig_thy) => SkipProof ((History.apply I h, thy), orig_thy)
+ (fn Proof (prf, orig_gthy) => Proof (ProofHistory.applys (f int) prf, orig_gthy)
+ | SkipProof ((h, gthy), orig_gthy) => SkipProof ((History.apply I h, gthy), orig_gthy)
| _ => raise UNDEF));
fun proof' f = proofs' (Seq.single oo f);
@@ -562,34 +581,40 @@
val proof = proof' o K;
fun actual_proof f = map_current (fn _ =>
- (fn Proof (prf, orig_thy) => Proof (f prf, orig_thy) | _ => raise UNDEF));
+ (fn Proof (prf, orig_gthy) => Proof (f prf, orig_gthy)
+ | _ => raise UNDEF));
fun skip_proof f = map_current (fn _ =>
- (fn SkipProof ((h, thy), orig_thy) => SkipProof ((f h, thy), orig_thy) | _ => raise UNDEF));
-
-fun end_proof f = map_current (fn int =>
- (fn Proof (prf, _) => Theory (f int (ProofHistory.current prf))
- | SkipProof ((h, thy), _) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF
+ (fn SkipProof ((h, gthy), orig_gthy) => SkipProof ((f h, gthy), orig_gthy)
| _ => raise UNDEF));
-val forget_proof = map_current (fn _ =>
- (fn Proof (_, orig_thy) => Theory (orig_thy, NONE)
- | SkipProof (_, orig_thy) => Theory (orig_thy, NONE)
- | _ => raise UNDEF));
-
-fun proof_to_theory' f = end_proof (rpair NONE oo f);
-fun proof_to_theory f = proof_to_theory' (K f);
-fun proof_to_theory_context f = end_proof ((swap o apfst SOME) oo f);
-
fun skip_proof_to_theory p = map_current (fn _ =>
(fn SkipProof ((h, thy), _) =>
if p (History.current h) then Theory (thy, NONE)
else raise UNDEF
| _ => raise UNDEF));
-fun present_local_theory loc f = app_current (fn int =>
- (fn Theory (thy, _) => Theory (swap (apfst SOME (TheoryTarget.mapping loc I thy)))
- | _ => raise UNDEF) #> tap (f int));
+val forget_proof = map_current (fn _ =>
+ (fn Proof (_, orig_gthy) => Theory (orig_gthy, NONE)
+ | SkipProof (_, orig_gthy) => Theory (orig_gthy, NONE)
+ | _ => raise UNDEF));
+
+fun end_proof f = map_current (fn int =>
+ (fn Proof (prf, orig_gthy) =>
+ let val state = ProofHistory.current prf in
+ if can (Proof.assert_bottom true) state then
+ let
+ val ctxt' = f int state;
+ val gthy' =
+ if can Context.the_theory orig_gthy
+ then Context.Theory (ProofContext.theory_of ctxt')
+ else Context.Proof (LocalTheory.reinit ctxt');
+ in Theory (gthy', SOME ctxt') end
+ else raise UNDEF
+ end
+ | SkipProof ((h, gthy), _) =>
+ if History.current h = 0 then Theory (gthy, NONE) else raise UNDEF
+ | _ => raise UNDEF));
fun present_proof f = map_current (fn int =>
(fn node as Proof _ => node | _ => raise UNDEF) #> tap (f int));