# HG changeset patch # User wenzelm # Date 1157038435 -7200 # Node ID f8a7a8236c689a31d00fbb038b0d770ef54bfa3d # Parent 8aa6ff178f367b6e986eb21f25f52fd225cfd865 more stuff; diff -r 8aa6ff178f36 -r f8a7a8236c68 doc-src/IsarImplementation/Thy/document/prelim.tex --- a/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 17:33:48 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 17:33:55 2006 +0200 @@ -202,10 +202,8 @@ valid theory --- updates on the original are propagated automatically. - \item \verb|Theory.self_ref| and \verb|Theory.deref| convert - between \verb|theory| and \verb|theory_ref|. As the - referenced theory evolves monotonically over time, later invocations - of \verb|Theory.deref| may refer to larger contexts. + \item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|. As the referenced theory + evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to larger contexts. \end{description}% \end{isamarkuptext}% @@ -231,12 +229,13 @@ Arbritrary auxiliary context data may be adjoined.} A proof context is a container for pure data with a back-reference - to the theory it belongs to. Modifications to draft theories are - propagated automatically as usual, but there is also an explicit - \isa{transfer} operation to resynchronize with more substantial - updates to the underlying theory. The actual context data does not - require any special bookkeeping, thanks to the lack of destructive - features. + to the theory it belongs to. The \isa{init} operation creates a + proof context derived from a given theory. Modifications to draft + theories are propagated to the proof context as usual, but there is + also an explicit \isa{transfer} operation to force + resynchronization with more substantial updates to the underlying + theory. The actual context data does not require any special + bookkeeping, thanks to the lack of destructive features. Entities derived in a proof context need to record inherent logical requirements explicitly, since there is no separate context @@ -263,7 +262,29 @@ \isatagmlref % \begin{isamarkuptext}% -FIXME% +\begin{mldecls} + \indexmltype{Proof.context}\verb|type Proof.context| \\ + \indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\ + \indexml{ProofContext.theory-of}\verb|ProofContext.theory_of: Proof.context -> theory| \\ + \indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\ + \end{mldecls} + + \begin{description} + + \item \verb|Proof.context| represents proof contexts. Elements + of this type are essentially pure values, with a sliding reference + to the background theory. + + \item \verb|ProofContext.init|~\isa{thy} produces a proof context + derived from \isa{thy}, initializing all data. + + \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the + background theory from \isa{ctxt}. + + \item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the + background theory of \isa{ctxt} to the super theory \isa{thy}. + + \end{description}% \end{isamarkuptext}% \isamarkuptrue% % @@ -279,7 +300,16 @@ \isamarkuptrue% % \begin{isamarkuptext}% -FIXME% +A generic context is the disjoint sum of either a theory or proof + context. Occasionally, this simplifies uniform treatment of generic + context data, typically extralogical information. Operations on + generic contexts include the usual injections, partial selections, + and combinators for lifting operations on either component of the + disjoint sum. + + Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory + can always be selected, while a proof context may have to be + constructed by an ad-hoc \isa{init} operation.% \end{isamarkuptext}% \isamarkuptrue% % @@ -290,7 +320,25 @@ \isatagmlref % \begin{isamarkuptext}% -FIXME% +\begin{mldecls} + \indexmltype{Context.generic}\verb|type Context.generic| \\ + \indexml{Context.theory-of}\verb|Context.theory_of: Context.generic -> theory| \\ + \indexml{Context.proof-of}\verb|Context.proof_of: Context.generic -> Proof.context| \\ + \end{mldecls} + + \begin{description} + + \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with datatype constructors + \verb|Context.Theory| and \verb|Context.Proof|. + + \item \verb|Context.theory_of|~\isa{context} always produces a + theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required. + + \item \verb|Context.proof_of|~\isa{context} always produces a + proof context from the generic \isa{context}, using \verb|ProofContext.init| as required. Note that this re-initializes the + context data with each invocation. + + \end{description}% \end{isamarkuptext}% \isamarkuptrue% % @@ -306,7 +354,78 @@ \isamarkuptrue% % \begin{isamarkuptext}% -% +Both theory and proof contexts manage arbitrary data, which is the + main purpose of contexts in the first place. Data can be declared + incrementally at compile --- Isabelle/Pure and major object-logics + are bootstrapped that way. + + \paragraph{Theory data} may refer to destructive entities, which are + maintained in correspondence to the linear evolution of theory + values, or explicit copies.\footnote{Most existing instances of + destructive theory data are merely historical relics (e.g.\ the + destructive theorem storage, and destructive hints for the + Simplifier and Classical rules).} A theory data declaration needs to + provide the following information: + + \medskip + \begin{tabular}{ll} + \isa{name{\isacharcolon}\ string} \\ + \isa{T} & the ML type \\ + \isa{empty{\isacharcolon}\ T} & initial value \\ + \isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\ + \isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\ + \isa{merge{\isacharcolon}\ T\ {\isasymtimes}\ T\ {\isasymrightarrow}\ T} & join on import \\ + \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\ + \end{tabular} + \medskip + + \noindent The \isa{name} acts as a comment for diagnostic + messages; \isa{copy} is just the identity for pure data; \isa{extend} is acts like a unitary version of \isa{merge}, both + should also include the functionality of \isa{copy} for impure + data. + + \paragraph{Proof context data} is purely functional. It is declared + by providing the following information: + + \medskip + \begin{tabular}{ll} + \isa{name{\isacharcolon}\ string} \\ + \isa{T} & the ML type \\ + \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\ + \isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\ + \end{tabular} + \medskip + + \noindent The \isa{init} operation is supposed to produce a pure + value from the given background theory. The rest is analogous to + (pure) theory data. + + \paragraph{Generic data} provides a hybrid interface for both kinds. + The declaration is essentially the same as for pure theory data, + without \isa{copy} (it is always the identity). The \isa{init} operation for proof contexts selects the current data value + from the background theory. + + \bigskip In any case, a data declaration of type \isa{T} results + in the following interface: + + \medskip + \begin{tabular}{ll} + \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\ + \isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\ + \isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\ + \isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\ + \isa{print{\isacharcolon}\ context\ {\isasymrightarrow}\ unit} + \end{tabular} + \medskip + + \noindent Here \isa{init} needs to be applied to the current + theory context once, in order to register the initial setup. The + other operations provide access for the particular kind of context + (theory, proof, or generic context). Note that this is a safe + interface: there is no other way to access the corresponding data + slot within a context. By keeping these operations private, a + component may maintain abstract values authentically, without other + components interfering.% \end{isamarkuptext}% \isamarkuptrue% % diff -r 8aa6ff178f36 -r f8a7a8236c68 doc-src/IsarImplementation/Thy/prelim.thy --- a/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 17:33:48 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 17:33:55 2006 +0200 @@ -176,10 +176,11 @@ valid theory --- updates on the original are propagated automatically. - \item @{ML "Theory.self_ref"} and @{ML "Theory.deref"} convert - between @{ML_type "theory"} and @{ML_type "theory_ref"}. As the - referenced theory evolves monotonically over time, later invocations - of @{ML "Theory.deref"} may refer to larger contexts. + \item @{ML "Theory.self_ref"}~@{text "thy"} and @{ML + "Theory.deref"}~@{text "thy_ref"} convert between @{ML_type + "theory"} and @{ML_type "theory_ref"}. As the referenced theory + evolves monotonically over time, later invocations of @{ML + "Theory.deref"} may refer to larger contexts. \end{description} *} @@ -196,12 +197,13 @@ Arbritrary auxiliary context data may be adjoined.} A proof context is a container for pure data with a back-reference - to the theory it belongs to. Modifications to draft theories are - propagated automatically as usual, but there is also an explicit - @{text "transfer"} operation to resynchronize with more substantial - updates to the underlying theory. The actual context data does not - require any special bookkeeping, thanks to the lack of destructive - features. + to the theory it belongs to. The @{text "init"} operation creates a + proof context derived from a given theory. Modifications to draft + theories are propagated to the proof context as usual, but there is + also an explicit @{text "transfer"} operation to force + resynchronization with more substantial updates to the underlying + theory. The actual context data does not require any special + bookkeeping, thanks to the lack of destructive features. Entities derived in a proof context need to record inherent logical requirements explicitly, since there is no separate context @@ -220,19 +222,153 @@ contexts, cf.\ \secref{isar-proof-state}. *} -text %mlref {* FIXME *} +text %mlref {* + \begin{mldecls} + @{index_ML_type Proof.context} \\ + @{index_ML ProofContext.init: "theory -> Proof.context"} \\ + @{index_ML ProofContext.theory_of: "Proof.context -> theory"} \\ + @{index_ML ProofContext.transfer: "theory -> Proof.context -> Proof.context"} \\ + \end{mldecls} + + \begin{description} + + \item @{ML_type Proof.context} represents proof contexts. Elements + of this type are essentially pure values, with a sliding reference + to the background theory. + + \item @{ML ProofContext.init}~@{text "thy"} produces a proof context + derived from @{text "thy"}, initializing all data. + + \item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the + background theory from @{text "ctxt"}. + + \item @{ML ProofContext.transfer}~@{text "thy ctxt"} promotes the + background theory of @{text "ctxt"} to the super theory @{text + "thy"}. + + \end{description} +*} + subsection {* Generic contexts *} -text FIXME +text {* + A generic context is the disjoint sum of either a theory or proof + context. Occasionally, this simplifies uniform treatment of generic + context data, typically extralogical information. Operations on + generic contexts include the usual injections, partial selections, + and combinators for lifting operations on either component of the + disjoint sum. + + Moreover, there are total operations @{text "theory_of"} and @{text + "proof_of"} to convert a generic context into either kind: a theory + can always be selected, while a proof context may have to be + constructed by an ad-hoc @{text "init"} operation. +*} -text %mlref {* FIXME *} +text %mlref {* + \begin{mldecls} + @{index_ML_type Context.generic} \\ + @{index_ML Context.theory_of: "Context.generic -> theory"} \\ + @{index_ML Context.proof_of: "Context.generic -> Proof.context"} \\ + \end{mldecls} + + \begin{description} + \item @{ML_type Context.generic} is the direct sum of @{ML_type + "theory"} and @{ML_type "Proof.context"}, with datatype constructors + @{ML "Context.Theory"} and @{ML "Context.Proof"}. + + \item @{ML Context.theory_of}~@{text "context"} always produces a + theory from the generic @{text "context"}, using @{ML + "ProofContext.theory_of"} as required. + + \item @{ML Context.proof_of}~@{text "context"} always produces a + proof context from the generic @{text "context"}, using @{ML + "ProofContext.init"} as required. Note that this re-initializes the + context data with each invocation. + + \end{description} +*} subsection {* Context data *} text {* + Both theory and proof contexts manage arbitrary data, which is the + main purpose of contexts in the first place. Data can be declared + incrementally at compile --- Isabelle/Pure and major object-logics + are bootstrapped that way. + + \paragraph{Theory data} may refer to destructive entities, which are + maintained in correspondence to the linear evolution of theory + values, or explicit copies.\footnote{Most existing instances of + destructive theory data are merely historical relics (e.g.\ the + destructive theorem storage, and destructive hints for the + Simplifier and Classical rules).} A theory data declaration needs to + provide the following information: + + \medskip + \begin{tabular}{ll} + @{text "name: string"} \\ + @{text "T"} & the ML type \\ + @{text "empty: T"} & initial value \\ + @{text "copy: T \ T"} & refresh impure data \\ + @{text "extend: T \ T"} & re-initialize on import \\ + @{text "merge: T \ T \ T"} & join on import \\ + @{text "print: T \ unit"} & diagnostic output \\ + \end{tabular} + \medskip + + \noindent The @{text "name"} acts as a comment for diagnostic + messages; @{text "copy"} is just the identity for pure data; @{text + "extend"} is acts like a unitary version of @{text "merge"}, both + should also include the functionality of @{text "copy"} for impure + data. + + \paragraph{Proof context data} is purely functional. It is declared + by providing the following information: + + \medskip + \begin{tabular}{ll} + @{text "name: string"} \\ + @{text "T"} & the ML type \\ + @{text "init: theory \ T"} & produce initial value \\ + @{text "print: T \ unit"} & diagnostic output \\ + \end{tabular} + \medskip + + \noindent The @{text "init"} operation is supposed to produce a pure + value from the given background theory. The rest is analogous to + (pure) theory data. + + \paragraph{Generic data} provides a hybrid interface for both kinds. + The declaration is essentially the same as for pure theory data, + without @{text "copy"} (it is always the identity). The @{text + "init"} operation for proof contexts selects the current data value + from the background theory. + + \bigskip In any case, a data declaration of type @{text "T"} results + in the following interface: + + \medskip + \begin{tabular}{ll} + @{text "init: theory \ theory"} \\ + @{text "get: context \ T"} \\ + @{text "put: T \ context \ context"} \\ + @{text "map: (T \ T) \ context \ context"} \\ + @{text "print: context \ unit"} + \end{tabular} + \medskip + + \noindent Here @{text "init"} needs to be applied to the current + theory context once, in order to register the initial setup. The + other operations provide access for the particular kind of context + (theory, proof, or generic context). Note that this is a safe + interface: there is no other way to access the corresponding data + slot within a context. By keeping these operations private, a + component may maintain abstract values authentically, without other + components interfering. *}