# HG changeset patch # User wenzelm # Date 1264805943 -3600 # Node ID 520727474bbe52702488e5d6b7ed8a24fbd912bc # Parent e59915c6a552ba2526106e9820dad0dc40446026 theory data example; diff -r e59915c6a552 -r 520727474bbe doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Fri Jan 29 23:57:57 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Fri Jan 29 23:59:03 2010 +0100 @@ -209,6 +209,85 @@ \end{description} *} +text %mlex {* + The following artificial example demonstrates theory + data: we maintain a set of terms that are supposed to be wellformed + wrt.\ the enclosing theory. The public interface is as follows: +*} + +ML {* +signature WELLFORMED_TERMS = +sig + val get: theory -> term list + val add: term -> theory -> theory +end; +*} + +text {* \noindent The implementation uses private theory data + internally, and only exposes an operation that involves explicit + argument checking wrt.\ the given theory. *} + +ML {* +structure Wellformed_Terms: WELLFORMED_TERMS = +struct + +structure Terms = Theory_Data +( + type T = term OrdList.T; + val empty = []; + val extend = I; + fun merge (ts1, ts2) = + OrdList.union TermOrd.fast_term_ord ts1 ts2; +) + +val get = Terms.get; + +fun add raw_t thy = + let val t = Sign.cert_term thy raw_t + in Terms.map (OrdList.insert TermOrd.fast_term_ord t) thy end; + +end; +*} + +text {* We use @{ML_type "term OrdList.T"} for reasonably efficient + representation of a set of terms: all operations are linear in the + number of stored elements. Here we assume that our users do not + care about the declaration order, since that data structure forces + its own arrangement of elements. + + Observe how the @{verbatim merge} operation joins the data slots of + the two constituents: @{ML OrdList.union} prevents duplication of + common data from different branches, thus avoiding the danger of + exponential blowup. (Plain list append etc.\ must never be used for + theory data merges.) + + \medskip Our intended invariant is achieved as follows: + \begin{enumerate} + + \item @{ML Wellformed_Terms.add} only admits terms that have passed + the @{ML Sign.cert_term} check of the given theory at that point. + + \item Wellformedness in the sense of @{ML Sign.cert_term} is + monotonic wrt.\ the sub-theory relation. So our data can move + upwards in the hierarchy (via extension or merges), and maintain + wellformedness without further checks. + + \end{enumerate} + + Note that all basic operations of the inference kernel (which + includes @{ML Sign.cert_term}) observe this monotonicity principle, + but other user-space tools don't. For example, fully-featured + type-inference via @{ML Syntax.check_term} (cf.\ + \secref{sec:term-check}) is not necessarily monotonic wrt.\ the + background theory, since constraints of term constants can be + strengthened by later declarations, for example. + + In most cases, user-space context data does not have to take such + invariants too seriously. The situation is different in the + implementation of the inference kernel itself, which uses the very + same data mechanisms for types, constants, axioms etc. +*} + subsection {* Proof context \label{sec:context-proof} *} diff -r e59915c6a552 -r 520727474bbe doc-src/IsarImplementation/Thy/Syntax.thy --- a/doc-src/IsarImplementation/Thy/Syntax.thy Fri Jan 29 23:57:57 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Syntax.thy Fri Jan 29 23:59:03 2010 +0100 @@ -2,8 +2,14 @@ imports Base begin -chapter {* Syntax and type-checking *} +chapter {* Concrete syntax and type-checking *} text FIXME +section {* Parsing and printing *} + +text FIXME + +section {* Checking and unchecking \label{sec:term-check} *} + end