# HG changeset patch # User wenzelm # Date 1160519258 -7200 # Node ID a7fd8f05a2bee7842ef91a9dd371945ca3c496cf # Parent e404275bff334ef4cd7932cbb793a6b7b6cd4ef5 added type global_theory -- theory or local_theory; added begin/exit_local_theory; removed theory_context; renamed body_context_node to presentation_context; removed copy (checkpoint twice instead -- avoids unrelated theories); diff -r e404275bff33 -r a7fd8f05a2be src/Pure/Isar/toplevel.ML --- 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));