backpatching of structure Proof and ProofContext -- avoid odd aliases;
renamed transfer_proof to raw_transfer;
indicate firm naming conventions for theory, Proof.context, Context.generic;
--- a/src/Pure/Isar/proof.ML Tue Oct 20 21:22:37 2009 +0200
+++ b/src/Pure/Isar/proof.ML Tue Oct 20 21:26:45 2009 +0200
@@ -7,7 +7,7 @@
signature PROOF =
sig
- type context = Context.proof
+ type context = Proof.context
type method = Method.method
type state
val init: context -> state
@@ -121,7 +121,7 @@
structure Proof: PROOF =
struct
-type context = Context.proof;
+type context = Proof.context;
type method = Method.method;
--- a/src/Pure/Isar/proof_context.ML Tue Oct 20 21:22:37 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Oct 20 21:26:45 2009 +0200
@@ -142,8 +142,7 @@
structure ProofContext: PROOF_CONTEXT =
struct
-val theory_of = Context.theory_of_proof;
-val init = Context.init_proof;
+open ProofContext;
(** inner syntax mode **)
@@ -259,7 +258,7 @@
else (Consts.merge (local_consts, thy_consts), thy_consts)
end);
-fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
+fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
fun theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
--- a/src/Pure/context.ML Tue Oct 20 21:22:37 2009 +0200
+++ b/src/Pure/context.ML Tue Oct 20 21:26:45 2009 +0200
@@ -4,6 +4,11 @@
Generic theory contexts with unique identity, arbitrarily typed data,
monotonic development graph and history support. Generic proof
contexts with arbitrarily typed data.
+
+Firm naming conventions:
+ thy, thy', thy1, thy2: theory
+ ctxt, ctxt', ctxt1, ctxt2: Proof.context
+ context: Context.generic
*)
signature BASIC_CONTEXT =
@@ -11,6 +16,12 @@
type theory
type theory_ref
exception THEORY of string * theory list
+ structure Proof: sig type context end
+ structure ProofContext:
+ sig
+ val theory_of: Proof.context -> theory
+ val init: theory -> Proof.context
+ end
end;
signature CONTEXT =
@@ -41,25 +52,23 @@
val finish_thy: theory -> theory
val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
(*proof context*)
- type proof
- val theory_of_proof: proof -> theory
- val transfer_proof: theory -> proof -> proof
- val init_proof: theory -> proof
+ val raw_transfer: theory -> Proof.context -> Proof.context
(*generic context*)
- datatype generic = Theory of theory | Proof of proof
- val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a
- val mapping: (theory -> theory) -> (proof -> proof) -> generic -> generic
- val mapping_result: (theory -> 'a * theory) -> (proof -> 'a * proof) -> generic -> 'a * generic
+ datatype generic = Theory of theory | Proof of Proof.context
+ val cases: (theory -> 'a) -> (Proof.context -> 'a) -> generic -> 'a
+ val mapping: (theory -> theory) -> (Proof.context -> Proof.context) -> generic -> generic
+ val mapping_result: (theory -> 'a * theory) -> (Proof.context -> 'a * Proof.context) ->
+ generic -> 'a * generic
val the_theory: generic -> theory
- val the_proof: generic -> proof
+ val the_proof: generic -> Proof.context
val map_theory: (theory -> theory) -> generic -> generic
- val map_proof: (proof -> proof) -> generic -> generic
+ val map_proof: (Proof.context -> Proof.context) -> generic -> generic
val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic
- val map_proof_result: (proof -> 'a * proof) -> generic -> 'a * generic
+ val map_proof_result: (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic
val theory_map: (generic -> generic) -> theory -> theory
- val proof_map: (generic -> generic) -> proof -> proof
- val theory_of: generic -> theory (*total*)
- val proof_of: generic -> proof (*total*)
+ val proof_map: (generic -> generic) -> Proof.context -> Proof.context
+ val theory_of: generic -> theory (*total*)
+ val proof_of: generic -> Proof.context (*total*)
(*thread data*)
val thread_data: unit -> generic option
val the_thread_data: unit -> generic
@@ -82,8 +91,8 @@
structure ProofData:
sig
val declare: (theory -> Object.T) -> serial
- val get: serial -> (Object.T -> 'a) -> proof -> 'a
- val put: serial -> ('a -> Object.T) -> 'a -> proof -> proof
+ val get: serial -> (Object.T -> 'a) -> Proof.context -> 'a
+ val put: serial -> ('a -> Object.T) -> 'a -> Proof.context -> Proof.context
end
end;
@@ -204,7 +213,8 @@
val is_draft = #draft o identity_of;
fun reject_draft thy =
- if is_draft thy then raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy])
+ if is_draft thy then
+ raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy])
else thy;
@@ -425,13 +435,16 @@
(*** proof context ***)
-(* datatype proof *)
-
-datatype proof = Prf of Object.T Datatab.table * theory_ref;
+(* datatype Proof.context *)
-fun theory_of_proof (Prf (_, thy_ref)) = deref thy_ref;
-fun data_of_proof (Prf (data, _)) = data;
-fun map_prf f (Prf (data, thy_ref)) = Prf (f data, thy_ref);
+structure Proof =
+struct
+ datatype context = Context of Object.T Datatab.table * theory_ref;
+end;
+
+fun theory_of_proof (Proof.Context (_, thy_ref)) = deref thy_ref;
+fun data_of_proof (Proof.Context (data, _)) = data;
+fun map_prf f (Proof.Context (data, thy_ref)) = Proof.Context (f data, thy_ref);
(* proof data kinds *)
@@ -453,17 +466,20 @@
in
-fun init_proof thy = Prf (init_data thy, check_thy thy);
-
-fun transfer_proof thy' (Prf (data, thy_ref)) =
+fun raw_transfer thy' (Proof.Context (data, thy_ref)) =
let
val thy = deref thy_ref;
val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
val _ = check_thy thy;
val data' = init_new_data data thy';
val thy_ref' = check_thy thy';
- in Prf (data', thy_ref') end;
+ in Proof.Context (data', thy_ref') end;
+structure ProofContext =
+struct
+ val theory_of = theory_of_proof;
+ fun init thy = Proof.Context (init_data thy, check_thy thy);
+end;
structure ProofData =
struct
@@ -477,7 +493,7 @@
fun get k dest prf =
dest (case Datatab.lookup (data_of_proof prf) k of
SOME x => x
- | NONE => invoke_init k (theory_of_proof prf)); (*adhoc value*)
+ | NONE => invoke_init k (ProofContext.theory_of prf)); (*adhoc value*)
fun put k mk x = map_prf (Datatab.update (k, mk x));
@@ -489,7 +505,7 @@
(*** generic context ***)
-datatype generic = Theory of theory | Proof of proof;
+datatype generic = Theory of theory | Proof of Proof.context;
fun cases f _ (Theory thy) = f thy
| cases _ g (Proof prf) = g prf;
@@ -509,8 +525,8 @@
fun theory_map f = the_theory o f o Theory;
fun proof_map f = the_proof o f o Proof;
-val theory_of = cases I theory_of_proof;
-val proof_of = cases init_proof I;
+val theory_of = cases I ProofContext.theory_of;
+val proof_of = cases ProofContext.init I;
@@ -546,8 +562,8 @@
end;
-structure BasicContext: BASIC_CONTEXT = Context;
-open BasicContext;
+structure Basic_Context: BASIC_CONTEXT = Context;
+open Basic_Context;
@@ -608,9 +624,9 @@
signature PROOF_DATA =
sig
type T
- val get: Context.proof -> T
- val put: T -> Context.proof -> Context.proof
- val map: (T -> T) -> Context.proof -> Context.proof
+ val get: Proof.context -> T
+ val put: T -> Proof.context -> Proof.context
+ val map: (T -> T) -> Proof.context -> Proof.context
end;
functor ProofDataFun(Data: PROOF_DATA_ARGS): PROOF_DATA =
@@ -670,7 +686,3 @@
(*hide private interface*)
structure Context: CONTEXT = Context;
-(*fake predeclarations*)
-structure Proof = struct type context = Context.proof end;
-structure ProofContext =
-struct val theory_of = Context.theory_of_proof val init = Context.init_proof end;
--- a/src/Pure/meta_simplifier.ML Tue Oct 20 21:22:37 2009 +0200
+++ b/src/Pure/meta_simplifier.ML Tue Oct 20 21:26:45 2009 +0200
@@ -346,7 +346,7 @@
fun activate_context thy ss =
let
val ctxt = the_context ss;
- val ctxt' = Context.transfer_proof (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt;
+ val ctxt' = Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt;
in context ctxt' ss end;