1.1 --- a/src/Doc/Implementation/Integration.thy Thu Jul 03 11:31:25 2014 +0200
1.2 +++ b/src/Doc/Implementation/Integration.thy Thu Jul 03 12:17:55 2014 +0200
1.3 @@ -13,9 +13,9 @@
1.4 is transformed by a sequence of transitions (commands) within a theory body.
1.5 This is a pure value with pure functions acting on it in a timeless and
1.6 stateless manner. Historically, the sequence of transitions was wrapped up
1.7 - as sequential command loop, such that commands are applied sequentially
1.8 - one-by-one. In contemporary Isabelle/Isar, processing toplevel commands
1.9 - usually works in parallel in multi-threaded Isabelle/ML.
1.10 + as sequential command loop, such that commands are applied one-by-one. In
1.11 + contemporary Isabelle/Isar, processing toplevel commands usually works in
1.12 + parallel in multi-threaded Isabelle/ML \cite{Wenzel:2009,Wenzel:2013:ITP}.
1.13 *}
1.14
1.15
1.16 @@ -28,10 +28,10 @@
1.17 commands such as @{command definition}, or state a @{command theorem} to be
1.18 proven. A proof state accepts a rich collection of Isar proof commands for
1.19 structured proof composition, or unstructured proof scripts. When the proof
1.20 - is concluded we get back to the theory, which is then updated by defining
1.21 - the resulting fact. Further theory declarations or theorem statements with
1.22 - proofs may follow, until we eventually conclude the theory development by
1.23 - issuing @{command end} to get back to the empty toplevel.
1.24 + is concluded we get back to the (local) theory, which is then updated by
1.25 + defining the resulting fact. Further theory declarations or theorem
1.26 + statements with proofs may follow, until we eventually conclude the theory
1.27 + development by issuing @{command end} to get back to the empty toplevel.
1.28 *}
1.29
1.30 text %mlref {*
1.31 @@ -41,8 +41,6 @@
1.32 @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
1.33 @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
1.34 @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
1.35 - @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
1.36 - @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
1.37 \end{mldecls}
1.38
1.39 \begin{description}
1.40 @@ -59,19 +57,11 @@
1.41 toplevel state.
1.42
1.43 \item @{ML Toplevel.theory_of}~@{text "state"} selects the
1.44 - background theory of @{text "state"}, raises @{ML Toplevel.UNDEF}
1.45 + background theory of @{text "state"}, it raises @{ML Toplevel.UNDEF}
1.46 for an empty toplevel state.
1.47
1.48 \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
1.49 - state if available, otherwise raises @{ML Toplevel.UNDEF}.
1.50 -
1.51 - \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
1.52 - information for each Isar command being executed.
1.53 -
1.54 - \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls
1.55 - low-level profiling of the underlying ML runtime system. For
1.56 - Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
1.57 - profiling.
1.58 + state if available, otherwise it raises @{ML Toplevel.UNDEF}.
1.59
1.60 \end{description}
1.61 *}
1.62 @@ -104,15 +94,14 @@
1.63 list of partial functions, which are tried in turn until the first
1.64 one succeeds. This acts like an outer case-expression for various
1.65 alternative state transitions. For example, \isakeyword{qed} works
1.66 - differently for a local proofs vs.\ the global ending of the main
1.67 + differently for a local proofs vs.\ the global ending of an outermost
1.68 proof.
1.69
1.70 - Toplevel transitions are composed via transition transformers.
1.71 - Internally, Isar commands are put together from an empty transition
1.72 - extended by name and source position. It is then left to the
1.73 - individual command parser to turn the given concrete syntax into a
1.74 - suitable transition transformer that adjoins actual operations on a
1.75 - theory or proof state etc.
1.76 + Transitions are composed via transition transformers. Internally, Isar
1.77 + commands are put together from an empty transition extended by name and
1.78 + source position. It is then left to the individual command parser to turn
1.79 + the given concrete syntax into a suitable transition transformer that
1.80 + adjoins actual operations on a theory or proof state.
1.81 *}
1.82
1.83 text %mlref {*
1.84 @@ -154,8 +143,8 @@
1.85 list).
1.86
1.87 \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding
1.88 - proof command, that returns the resulting theory, after storing the
1.89 - resulting facts in the context etc.
1.90 + proof command, that returns the resulting theory, after applying the
1.91 + resulting facts to the target context.
1.92
1.93 \end{description}
1.94 *}
1.95 @@ -175,7 +164,7 @@
1.96 text %mlref {*
1.97 \begin{mldecls}
1.98 @{index_ML use_thy: "string -> unit"} \\
1.99 - @{index_ML use_thys: "string list -> unit"} \\
1.100 + @{index_ML use_thys: "string list -> unit"} \\[0.5ex]
1.101 @{index_ML Thy_Info.get_theory: "string -> theory"} \\
1.102 @{index_ML Thy_Info.remove_thy: "string -> unit"} \\
1.103 @{index_ML Thy_Info.register_thy: "theory -> unit"} \\
1.104 @@ -184,8 +173,8 @@
1.105 \begin{description}
1.106
1.107 \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
1.108 - up-to-date wrt.\ the external file store, reloading outdated ancestors as
1.109 - required.
1.110 + up-to-date wrt.\ the external file store; outdated ancestors are reloaded on
1.111 + demand.
1.112
1.113 \item @{ML use_thys} is similar to @{ML use_thy}, but handles several
1.114 theories simultaneously. Thus it acts like processing the import header of a
1.115 @@ -193,6 +182,8 @@
1.116 sub-graph of theories, the intrinsic parallelism can be exploited by the
1.117 system to speedup loading.
1.118
1.119 + This variant is used by default in @{tool build} \cite{isabelle-sys}.
1.120 +
1.121 \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
1.122 presently associated with name @{text A}. Note that the result might be
1.123 outdated wrt.\ the file-system content.
1.124 @@ -202,7 +193,7 @@
1.125
1.126 \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an existing
1.127 theory value with the theory loader database and updates source version
1.128 - information according to the current file-system state.
1.129 + information according to the file store.
1.130
1.131 \end{description}
1.132 *}
2.1 --- a/src/Doc/Implementation/Syntax.thy Thu Jul 03 11:31:25 2014 +0200
2.2 +++ b/src/Doc/Implementation/Syntax.thy Thu Jul 03 12:17:55 2014 +0200
2.3 @@ -12,18 +12,18 @@
2.4 additional means for reading and printing of terms and types. This
2.5 important add-on outside the logical core is called \emph{inner
2.6 syntax} in Isabelle jargon, as opposed to the \emph{outer syntax} of
2.7 - the theory and proof language (cf.\ \cite{isabelle-isar-ref}).
2.8 + the theory and proof language \cite{isabelle-isar-ref}.
2.9
2.10 - For example, according to \cite{church40} quantifiers are
2.11 - represented as higher-order constants @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow>
2.12 - bool"} such that @{text "All (\<lambda>x::'a. B x)"} faithfully represents
2.13 - the idea that is displayed as @{text "\<forall>x::'a. B x"} via @{keyword
2.14 - "binder"} notation. Moreover, type-inference in the style of
2.15 - Hindley-Milner \cite{hindleymilner} (and extensions) enables users
2.16 - to write @{text "\<forall>x. B x"} concisely, when the type @{text "'a"} is
2.17 - already clear from the context.\footnote{Type-inference taken to the
2.18 - extreme can easily confuse users, though. Beginners often stumble
2.19 - over unexpectedly general types inferred by the system.}
2.20 + For example, according to \cite{church40} quantifiers are represented as
2.21 + higher-order constants @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} such that @{text
2.22 + "All (\<lambda>x::'a. B x)"} faithfully represents the idea that is displayed in
2.23 + Isabelle as @{text "\<forall>x::'a. B x"} via @{keyword "binder"} notation.
2.24 + Moreover, type-inference in the style of Hindley-Milner \cite{hindleymilner}
2.25 + (and extensions) enables users to write @{text "\<forall>x. B x"} concisely, when
2.26 + the type @{text "'a"} is already clear from the
2.27 + context.\footnote{Type-inference taken to the extreme can easily confuse
2.28 + users. Beginners often stumble over unexpectedly general types inferred by
2.29 + the system.}
2.30
2.31 \medskip The main inner syntax operations are \emph{read} for
2.32 parsing together with type-checking, and \emph{pretty} for formatted
2.33 @@ -43,18 +43,17 @@
2.34
2.35 \end{itemize}
2.36
2.37 - Some specification package might thus intercept syntax processing at
2.38 - a well-defined stage after @{text "parse"}, to a augment the
2.39 - resulting pre-term before full type-reconstruction is performed by
2.40 - @{text "check"}, for example. Note that the formal status of bound
2.41 - variables, versus free variables, versus constants must not be
2.42 - changed between these phases!
2.43 + For example, some specification package might thus intercept syntax
2.44 + processing at a well-defined stage after @{text "parse"}, to a augment the
2.45 + resulting pre-term before full type-reconstruction is performed by @{text
2.46 + "check"}. Note that the formal status of bound variables, versus free
2.47 + variables, versus constants must not be changed between these phases.
2.48
2.49 \medskip In general, @{text check} and @{text uncheck} operate
2.50 simultaneously on a list of terms. This is particular important for
2.51 type-checking, to reconstruct types for several terms of the same context
2.52 and scope. In contrast, @{text parse} and @{text unparse} operate separately
2.53 - in single terms.
2.54 + on single terms.
2.55
2.56 There are analogous operations to read and print types, with the same
2.57 sub-division into phases.
2.58 @@ -63,14 +62,15 @@
2.59
2.60 section {* Reading and pretty printing \label{sec:read-print} *}
2.61
2.62 -text {* Read and print operations are roughly dual to each other, such
2.63 - that for the user @{text "s' = pretty (read s)"} looks similar to
2.64 - the original source text @{text "s"}, but the details depend on many
2.65 - side-conditions. There are also explicit options to control
2.66 - suppressing of type information in the output. The default
2.67 - configuration routinely looses information, so @{text "t' = read
2.68 - (pretty t)"} might fail, or produce a differently typed term, or a
2.69 - completely different term in the face of syntactic overloading! *}
2.70 +text {*
2.71 + Read and print operations are roughly dual to each other, such that for the
2.72 + user @{text "s' = pretty (read s)"} looks similar to the original source
2.73 + text @{text "s"}, but the details depend on many side-conditions. There are
2.74 + also explicit options to control the removal of type information in the
2.75 + output. The default configuration routinely looses information, so @{text
2.76 + "t' = read (pretty t)"} might fail, or produce a differently typed term, or
2.77 + a completely different term in the face of syntactic overloading.
2.78 +*}
2.79
2.80 text %mlref {*
2.81 \begin{mldecls}
2.82 @@ -98,26 +98,27 @@
2.83
2.84 If particular type-constraints are required for some of the arguments, the
2.85 read operations needs to be split into its parse and check phases. Then it
2.86 - is possible to use @{ML Type.constraint} on the intermediate pre-terms.
2.87 + is possible to use @{ML Type.constraint} on the intermediate pre-terms
2.88 + \secref{sec:term-check}.
2.89
2.90 \item @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a
2.91 simultaneous list of source strings as terms of the logic, with an implicit
2.92 type-constraint for each argument to enforce type @{typ prop}; this also
2.93 - affects the inner syntax for parsing. The remaining type-reconstructions
2.94 - works as for @{ML Syntax.read_terms} above.
2.95 + affects the inner syntax for parsing. The remaining type-reconstruction
2.96 + works as for @{ML Syntax.read_terms}.
2.97
2.98 \item @{ML Syntax.read_typ}, @{ML Syntax.read_term}, @{ML Syntax.read_prop}
2.99 - are like the simultaneous versions above, but operate on a single argument
2.100 - only. This convenient shorthand is adequate in situations where a single
2.101 - item in its own scope is processed. Do not use @{ML "map o
2.102 - Syntax.read_term"} where @{ML Syntax.read_terms} is actually intended!
2.103 + are like the simultaneous versions, but operate on a single argument only.
2.104 + This convenient shorthand is adequate in situations where a single item in
2.105 + its own scope is processed. Do not use @{ML "map o Syntax.read_term"} where
2.106 + @{ML Syntax.read_terms} is actually intended!
2.107
2.108 \item @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML
2.109 Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type
2.110 or term, respectively. Although the uncheck phase acts on a simultaneous
2.111 - list as well, this is rarely relevant in practice, so only the singleton
2.112 - case is provided as combined pretty operation. There is no distinction of
2.113 - term vs.\ proposition.
2.114 + list as well, this is rarely used in practice, so only the singleton case is
2.115 + provided as combined pretty operation. There is no distinction of term vs.\
2.116 + proposition.
2.117
2.118 \item @{ML Syntax.string_of_typ} and @{ML Syntax.string_of_term} are
2.119 convenient compositions of @{ML Syntax.pretty_typ} and @{ML
2.120 @@ -130,11 +131,11 @@
2.121 @{ML Syntax.read_term}, @{ML Syntax.read_prop}, and @{ML
2.122 Syntax.string_of_term} are the most important operations in practice.
2.123
2.124 - \medskip Note that the string values that are passed in and out here are
2.125 + \medskip Note that the string values that are passed in and out are
2.126 annotated by the system, to carry further markup that is relevant for the
2.127 Prover IDE \cite{isabelle-jedit}. User code should neither compose its own
2.128 input strings, nor try to analyze the output strings. Conceptually this is
2.129 - an abstract datatype, encoded into a concrete string for historical reasons.
2.130 + an abstract datatype, encoded as concrete string for historical reasons.
2.131
2.132 The standard way to provide the required position markup for input works via
2.133 the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already
2.134 @@ -147,47 +148,46 @@
2.135
2.136 section {* Parsing and unparsing \label{sec:parse-unparse} *}
2.137
2.138 -text {* Parsing and unparsing converts between actual source text and
2.139 - a certain \emph{pre-term} format, where all bindings and scopes are
2.140 - resolved faithfully. Thus the names of free variables or constants
2.141 - are already determined in the sense of the logical context, but type
2.142 - information might be still missing. Pre-terms support an explicit
2.143 - language of \emph{type constraints} that may be augmented by user
2.144 - code to guide the later \emph{check} phase.
2.145 +text {*
2.146 + Parsing and unparsing converts between actual source text and a certain
2.147 + \emph{pre-term} format, where all bindings and scopes are already resolved
2.148 + faithfully. Thus the names of free variables or constants are determined in
2.149 + the sense of the logical context, but type information might be still
2.150 + missing. Pre-terms support an explicit language of \emph{type constraints}
2.151 + that may be augmented by user code to guide the later \emph{check} phase.
2.152
2.153 - Actual parsing is based on traditional lexical analysis and Earley
2.154 - parsing for arbitrary context-free grammars. The user can specify
2.155 - the grammar via mixfix annotations. Moreover, there are \emph{syntax
2.156 - translations} that can be augmented by the user, either
2.157 - declaratively via @{command translations} or programmatically via
2.158 - @{command parse_translation}, @{command print_translation} etc. The
2.159 - final scope-resolution is performed by the system, according to name
2.160 - spaces for types, term variables and constants etc.\ determined by
2.161 - the context.
2.162 + Actual parsing is based on traditional lexical analysis and Earley parsing
2.163 + for arbitrary context-free grammars. The user can specify the grammar
2.164 + declaratively via mixfix annotations. Moreover, there are \emph{syntax
2.165 + translations} that can be augmented by the user, either declaratively via
2.166 + @{command translations} or programmatically via @{command
2.167 + parse_translation}, @{command print_translation} \cite{isabelle-isar-ref}.
2.168 + The final scope-resolution is performed by the system, according to name
2.169 + spaces for types, term variables and constants determined by the context.
2.170 *}
2.171
2.172 text %mlref {*
2.173 \begin{mldecls}
2.174 @{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\
2.175 @{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\
2.176 - @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\
2.177 + @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\[0.5ex]
2.178 @{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\
2.179 @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
2.180 \end{mldecls}
2.181
2.182 \begin{description}
2.183
2.184 - \item @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source strings as
2.185 + \item @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source string as
2.186 pre-type that is ready to be used with subsequent check operations.
2.187
2.188 - \item @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source strings as
2.189 + \item @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source string as
2.190 pre-term that is ready to be used with subsequent check operations.
2.191
2.192 - \item @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source strings as
2.193 + \item @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source string as
2.194 pre-term that is ready to be used with subsequent check operations. The
2.195 inner syntax category is @{typ prop} and a suitable type-constraint is
2.196 - included to ensure that this information is preserved during the check
2.197 - phase.
2.198 + included to ensure that this information is observed in subsequent type
2.199 + reconstruction.
2.200
2.201 \item @{ML Syntax.unparse_typ}~@{text "ctxt T"} unparses a type after
2.202 uncheck operations, to turn it into a pretty tree.
2.203 @@ -198,8 +198,8 @@
2.204
2.205 \end{description}
2.206
2.207 - These operations always operate on single items; use the combinator @{ML
2.208 - map} to apply them to a list of items.
2.209 + These operations always operate on a single item; use the combinator @{ML
2.210 + map} to apply them to a list.
2.211 *}
2.212
2.213
2.214 @@ -216,14 +216,14 @@
2.215 before pretty printing.
2.216
2.217 A typical add-on for the check/uncheck syntax layer is the @{command
2.218 - abbreviation} mechanism. Here the user specifies syntactic
2.219 - definitions that are managed by the system as polymorphic @{text
2.220 - "let"} bindings. These are expanded during the @{text "check"}
2.221 - phase, and contracted during the @{text "uncheck"} phase, without
2.222 - affecting the type-assignment of the given terms.
2.223 + abbreviation} mechanism \cite{isabelle-isar-ref}. Here the user specifies
2.224 + syntactic definitions that are managed by the system as polymorphic @{text
2.225 + "let"} bindings. These are expanded during the @{text "check"} phase, and
2.226 + contracted during the @{text "uncheck"} phase, without affecting the
2.227 + type-assignment of the given terms.
2.228
2.229 - \medskip The precise meaning of type checking depends on the context
2.230 - --- additional check/uncheck plugins might be defined in user space.
2.231 + \medskip The precise meaning of type checking depends on the context ---
2.232 + additional check/uncheck modules might be defined in user space.
2.233
2.234 For example, the @{command class} command defines a context where
2.235 @{text "check"} treats certain type instances of overloaded
2.236 @@ -237,7 +237,7 @@
2.237 \begin{mldecls}
2.238 @{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\
2.239 @{index_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\
2.240 - @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\
2.241 + @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\[0.5ex]
2.242 @{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\
2.243 @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
2.244 \end{mldecls}
2.245 @@ -256,7 +256,7 @@
2.246 Applications sometimes need to check several types and terms together. The
2.247 standard approach uses @{ML Logic.mk_type} to embed the language of types
2.248 into that of terms; all arguments are appended into one list of terms that
2.249 - is checked; afterwards the original type arguments are recovered with @{ML
2.250 + is checked; afterwards the type arguments are recovered with @{ML
2.251 Logic.dest_type}.
2.252
2.253 \item @{ML Syntax.check_props}~@{text "ctxt ts"} checks a simultaneous list
2.254 @@ -273,8 +273,8 @@
2.255
2.256 \end{description}
2.257
2.258 - These operations always operate simultaneously on multiple items; use the
2.259 - combinator @{ML singleton} to apply them to a single item.
2.260 + These operations always operate simultaneously on a list; use the combinator
2.261 + @{ML singleton} to apply them to a single item.
2.262 *}
2.263
2.264 end