# HG changeset patch # User wenzelm # Date 1264714691 -3600 # Node ID 008126f730a0ab544bcf6cb31b1442a017c9f86f # Parent 3343670206ebfa160e8c8ed9e24faa59c70a8789 formal markup of type aliases; updated/tuned/clarified contexts; misc tuning and clarification; diff -r 3343670206eb -r 008126f730a0 doc-src/IsarImplementation/Thy/Integration.thy --- a/doc-src/IsarImplementation/Thy/Integration.thy Thu Jan 28 22:19:27 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Integration.thy Thu Jan 28 22:38:11 2010 +0100 @@ -400,7 +400,7 @@ descendants from the theory database. \item @{ML ThyInfo.begin_theory} is the basic operation behind a - @{text \} header declaration. This is {\ML} functions is + @{text \} header declaration. This {\ML} function is normally not invoked directly. \item @{ML ThyInfo.end_theory} concludes the loading of a theory diff -r 3343670206eb -r 008126f730a0 doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Thu Jan 28 22:19:27 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Thu Jan 28 22:38:11 2010 +0100 @@ -116,9 +116,9 @@ text %mlref {* \begin{mldecls} - @{index_ML_type class} \\ - @{index_ML_type sort} \\ - @{index_ML_type arity} \\ + @{index_ML_type class: string} \\ + @{index_ML_type sort: "class list"} \\ + @{index_ML_type arity: "string * sort list * sort"} \\ @{index_ML_type typ} \\ @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\ @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\ @@ -136,15 +136,15 @@ \begin{description} - \item @{ML_type class} represents type classes; this is an alias for - @{ML_type string}. + \item @{ML_type class} represents type classes. - \item @{ML_type sort} represents sorts; this is an alias for - @{ML_type "class list"}. + \item @{ML_type sort} represents sorts, i.e.\ finite intersections + of classes. The empty list @{ML "[]: sort"} refers to the empty + class intersection, i.e.\ the ``full sort''. - \item @{ML_type arity} represents type arities; this is an alias for - triples of the form @{text "(\, \<^vec>s, s)"} for @{text "\ :: - (\<^vec>s)s"} described above. + \item @{ML_type arity} represents type arities. A triple @{text + "(\, \<^vec>s, s) : arity"} represents @{text "\ :: (\<^vec>s)s"} as + described above. \item @{ML_type typ} represents types; this is a datatype with constructors @{ML TFree}, @{ML TVar}, @{ML Type}. diff -r 3343670206eb -r 008126f730a0 doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jan 28 22:19:27 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jan 28 22:38:11 2010 +0100 @@ -73,41 +73,47 @@ subsection {* Theory context \label{sec:context-theory} *} -text {* - A \emph{theory} is a data container with explicit name and unique - identifier. Theories are related by a (nominal) sub-theory +text {* A \emph{theory} is a data container with explicit name and + unique identifier. Theories are related by a (nominal) sub-theory relation, which corresponds to the dependency graph of the original construction; each theory is derived from a certain sub-graph of - ancestor theories. - - The @{text "merge"} operation produces the least upper bound of two - theories, which actually degenerates into absorption of one theory - into the other (due to the nominal sub-theory relation). + ancestor theories. To this end, the system maintains a set of + symbolic ``identification stamps'' within each theory. - The @{text "begin"} operation starts a new theory by importing - several parent theories and entering a special @{text "draft"} mode, - which is sustained until the final @{text "end"} operation. A draft - theory acts like a linear type, where updates invalidate earlier - versions. An invalidated draft is called ``stale''. + In order to avoid the full-scale overhead of explicit sub-theory + identification of arbitrary intermediate stages, a theory is + switched into @{text "draft"} mode under certain circumstances. A + draft theory acts like a linear type, where updates invalidate + earlier versions. An invalidated draft is called \emph{stale}. - The @{text "checkpoint"} operation produces an intermediate stepping - stone that will survive the next update: both the original and the - changed theory remain valid and are related by the sub-theory - relation. Checkpointing essentially recovers purely functional - theory values, at the expense of some extra internal bookkeeping. + The @{text "checkpoint"} operation produces a safe stepping stone + that will survive the next update without becoming stale: both the + old and the new theory remain valid and are related by the + sub-theory relation. Checkpointing essentially recovers purely + functional theory values, at the expense of some extra internal + bookkeeping. The @{text "copy"} operation produces an auxiliary version that has the same data content, but is unrelated to the original: updates of the copy do not affect the original, neither does the sub-theory relation hold. + The @{text "merge"} operation produces the least upper bound of two + theories, which actually degenerates into absorption of one theory + into the other (according to the nominal sub-theory relation). + + The @{text "begin"} operation starts a new theory by importing + several parent theories and entering a special mode of nameless + incremental updates, until the final @{text "end"} operation is + performed. + \medskip The example in \figref{fig:ex-theory} below shows a theory graph derived from @{text "Pure"}, with theory @{text "Length"} importing @{text "Nat"} and @{text "List"}. The body of @{text "Length"} consists of a sequence of updates, working mostly on - drafts. Intermediate checkpoints may occur as well, due to the - history mechanism provided by the Isar top-level, cf.\ - \secref{sec:isar-toplevel}. + drafts internally, while transaction boundaries of Isar top-level + commands (\secref{sec:isar-toplevel}) are guaranteed to be safe + checkpoints. \begin{figure}[htb] \begin{center} @@ -147,9 +153,10 @@ \begin{mldecls} @{index_ML_type theory} \\ @{index_ML Theory.subthy: "theory * theory -> bool"} \\ - @{index_ML Theory.merge: "theory * theory -> theory"} \\ @{index_ML Theory.checkpoint: "theory -> theory"} \\ @{index_ML Theory.copy: "theory -> theory"} \\ + @{index_ML Theory.merge: "theory * theory -> theory"} \\ + @{index_ML Theory.begin_theory: "string -> theory list -> theory"} \\ \end{mldecls} \begin{mldecls} @{index_ML_type theory_ref} \\ @@ -160,25 +167,32 @@ \begin{description} \item @{ML_type theory} represents theory contexts. This is - essentially a linear type! Most operations destroy the original - version, which then becomes ``stale''. + essentially a linear type, with explicit runtime checking! Most + internal theory operations destroy the original version, which then + becomes ``stale''. - \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} - compares theories according to the inherent graph structure of the - construction. This sub-theory relation is a nominal approximation - of inclusion (@{text "\"}) of the corresponding content. - - \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} - absorbs one theory into the other. This fails for unrelated - theories! + \item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} compares theories + according to the intrinsic graph structure of the construction. + This sub-theory relation is a nominal approximation of inclusion + (@{text "\"}) of the corresponding content (according to the + semantics of the ML modules that implement the data). \item @{ML "Theory.checkpoint"}~@{text "thy"} produces a safe - stepping stone in the linear development of @{text "thy"}. The next - update will result in two related, valid theories. + stepping stone in the linear development of @{text "thy"}. This + changes the old theory, but the next update will result in two + related, valid theories. \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text - "thy"} with the same data. The result is not related to the - original; the original is unchanged. + "thy"} with the same data. The copy is not related to the original, + but the original is unchanged. + + \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} absorbs one theory + into the other, without changing @{text "thy\<^sub>1"} or @{text "thy\<^sub>2"}. + This version of ad-hoc theory merge fails for unrelated theories! + + \item @{ML "Theory.begin_theory"}~@{text "name parents"} constructs + a new theory based on the given parents. This {\ML} function is + normally not invoked directly. \item @{ML_type theory_ref} represents a sliding reference to an always valid theory; updates on the original are propagated @@ -198,31 +212,32 @@ subsection {* Proof context \label{sec:context-proof} *} -text {* - A proof context is a container for pure data with a back-reference - to the theory it belongs to. The @{text "init"} operation creates a - proof context 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. +text {* A proof context is a container for pure data with a + back-reference to the theory it belongs to. The @{text "init"} + operation creates a proof context 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. - Entities derived in a proof context need to record inherent logical + Entities derived in a proof context need to record logical requirements explicitly, since there is no separate context - identification as for theories. For example, hypotheses used in - primitive derivations (cf.\ \secref{sec:thms}) are recorded - separately within the sequent @{text "\ \ \"}, just to make double - sure. Results could still leak into an alien proof context due to - programming errors, but Isabelle/Isar includes some extra validity - checks in critical positions, notably at the end of a sub-proof. + identification or symbolic inclusion as for theories. For example, + hypotheses used in primitive derivations (cf.\ \secref{sec:thms}) + are recorded separately within the sequent @{text "\ \ \"}, just to + make double sure. Results could still leak into an alien proof + context due to programming errors, but Isabelle/Isar includes some + extra validity checks in critical positions, notably at the end of a + sub-proof. Proof contexts may be manipulated arbitrarily, although the common discipline is to follow block structure as a mental model: a given context is extended consecutively, and results are exported back - into the original context. Note that the Isar proof states model + into the original context. Note that an Isar proof state models block-structured reasoning explicitly, using a stack of proof - contexts internally. + contexts internally. For various technical reasons, the background + theory of an Isar proof state must not be changed while the proof is + still under construction! *} text %mlref {* @@ -267,7 +282,8 @@ 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 from the sum, while a proof context might - have to be constructed by an ad-hoc @{text "init"} operation. + have to be constructed by an ad-hoc @{text "init"} operation, which + incurs a small runtime overhead. *} text %mlref {* @@ -319,6 +335,16 @@ \emph{any} theory that does not declare actual data content; @{text "extend"} is acts like a unitary version of @{text "merge"}. + Implementing @{text "merge"} can be tricky. The general idea is + that @{text "merge (data\<^sub>1, data\<^sub>2)"} inserts those parts of @{text + "data\<^sub>2"} into @{text "data\<^sub>1"} that are not yet present, while + keeping the general order of things. The @{ML Library.merge} + function on plain lists may serve as canonical template. + + Particularly note that shared parts of the data must not be + duplicated by naive concatenation, or a theory graph that is like a + chain of diamonds would cause an exponential blowup! + \paragraph{Proof context data} declarations need to implement the following SML signature: @@ -330,15 +356,18 @@ \medskip \noindent The @{text "init"} operation is supposed to produce a pure - value from the given background theory. + value from the given background theory and should be somehow + ``immediate''. Whenever a proof context is initialized, which + happens frequently, the the system invokes the @{text "init"} + operation of \emph{all} theory data slots ever declared. \paragraph{Generic data} provides a hybrid interface for both theory and proof data. The @{text "init"} operation for proof contexts is predefined to select the current data value from the background theory. - \bigskip A data declaration of type @{text "T"} results in the - following interface: + \bigskip Any of these data declaration over type @{text "T"} result + in an ML structure with the following signature: \medskip \begin{tabular}{ll} @@ -348,12 +377,12 @@ \end{tabular} \medskip - \noindent These 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 of a context. By keeping these operations - private, a component may maintain abstract values authentically, - without other components interfering. + \noindent These other operations provide exclusive access for the + particular kind of context (theory, proof, or generic context). + This interface fully observes the ML discipline for types and + scopes: there is no other way to access the corresponding data slot + of a context. By keeping these operations private, an Isabelle/ML + module may maintain abstract values authentically. *} text %mlref {* @@ -447,7 +476,7 @@ text %mlref {* \begin{mldecls} - @{index_ML_type "Symbol.symbol"} \\ + @{index_ML_type "Symbol.symbol": string} \\ @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\ @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\ @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\ @@ -462,7 +491,7 @@ \begin{description} \item @{ML_type "Symbol.symbol"} represents individual Isabelle - symbols; this is an alias for @{ML_type "string"}. + symbols. \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list from the packed form. This function supercedes @{ML