# HG changeset patch # User wenzelm # Date 1404382675 -7200 # Node ID 94596c573b384140b6a713a023035dd3468a5ec0 # Parent b627e76cc5cc5fa1a458f14081a7be629c16f95d misc tuning; diff -r b627e76cc5cc -r 94596c573b38 src/Doc/Implementation/Integration.thy --- a/src/Doc/Implementation/Integration.thy Thu Jul 03 11:31:25 2014 +0200 +++ b/src/Doc/Implementation/Integration.thy Thu Jul 03 12:17:55 2014 +0200 @@ -13,9 +13,9 @@ is transformed by a sequence of transitions (commands) within a theory body. This is a pure value with pure functions acting on it in a timeless and stateless manner. Historically, the sequence of transitions was wrapped up - as sequential command loop, such that commands are applied sequentially - one-by-one. In contemporary Isabelle/Isar, processing toplevel commands - usually works in parallel in multi-threaded Isabelle/ML. + as sequential command loop, such that commands are applied one-by-one. In + contemporary Isabelle/Isar, processing toplevel commands usually works in + parallel in multi-threaded Isabelle/ML \cite{Wenzel:2009,Wenzel:2013:ITP}. *} @@ -28,10 +28,10 @@ commands such as @{command definition}, or state a @{command theorem} to be proven. A proof state accepts a rich collection of Isar proof commands for structured proof composition, or unstructured proof scripts. When the proof - is concluded we get back to the theory, which is then updated by defining - the resulting fact. Further theory declarations or theorem statements with - proofs may follow, until we eventually conclude the theory development by - issuing @{command end} to get back to the empty toplevel. + is concluded we get back to the (local) theory, which is then updated by + defining the resulting fact. Further theory declarations or theorem + statements with proofs may follow, until we eventually conclude the theory + development by issuing @{command end} to get back to the empty toplevel. *} text %mlref {* @@ -41,8 +41,6 @@ @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\ @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\ @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ - @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\ - @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\ \end{mldecls} \begin{description} @@ -59,19 +57,11 @@ toplevel state. \item @{ML Toplevel.theory_of}~@{text "state"} selects the - background theory of @{text "state"}, raises @{ML Toplevel.UNDEF} + background theory of @{text "state"}, it raises @{ML Toplevel.UNDEF} for an empty toplevel state. \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof - state if available, otherwise raises @{ML Toplevel.UNDEF}. - - \item @{ML "Toplevel.timing := true"} makes the toplevel print timing - information for each Isar command being executed. - - \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls - low-level profiling of the underlying ML runtime system. For - Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space - profiling. + state if available, otherwise it raises @{ML Toplevel.UNDEF}. \end{description} *} @@ -104,15 +94,14 @@ list of partial functions, which are tried in turn until the first one succeeds. This acts like an outer case-expression for various alternative state transitions. For example, \isakeyword{qed} works - differently for a local proofs vs.\ the global ending of the main + differently for a local proofs vs.\ the global ending of an outermost proof. - Toplevel transitions are composed via transition transformers. - Internally, Isar commands are put together from an empty transition - extended by name and source position. It is then left to the - individual command parser to turn the given concrete syntax into a - suitable transition transformer that adjoins actual operations on a - theory or proof state etc. + Transitions are composed via transition transformers. Internally, Isar + commands are put together from an empty transition extended by name and + source position. It is then left to the individual command parser to turn + the given concrete syntax into a suitable transition transformer that + adjoins actual operations on a theory or proof state. *} text %mlref {* @@ -154,8 +143,8 @@ list). \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding - proof command, that returns the resulting theory, after storing the - resulting facts in the context etc. + proof command, that returns the resulting theory, after applying the + resulting facts to the target context. \end{description} *} @@ -175,7 +164,7 @@ text %mlref {* \begin{mldecls} @{index_ML use_thy: "string -> unit"} \\ - @{index_ML use_thys: "string list -> unit"} \\ + @{index_ML use_thys: "string list -> unit"} \\[0.5ex] @{index_ML Thy_Info.get_theory: "string -> theory"} \\ @{index_ML Thy_Info.remove_thy: "string -> unit"} \\ @{index_ML Thy_Info.register_thy: "theory -> unit"} \\ @@ -184,8 +173,8 @@ \begin{description} \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully - up-to-date wrt.\ the external file store, reloading outdated ancestors as - required. + up-to-date wrt.\ the external file store; outdated ancestors are reloaded on + demand. \item @{ML use_thys} is similar to @{ML use_thy}, but handles several theories simultaneously. Thus it acts like processing the import header of a @@ -193,6 +182,8 @@ sub-graph of theories, the intrinsic parallelism can be exploited by the system to speedup loading. + This variant is used by default in @{tool build} \cite{isabelle-sys}. + \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value presently associated with name @{text A}. Note that the result might be outdated wrt.\ the file-system content. @@ -202,7 +193,7 @@ \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an existing theory value with the theory loader database and updates source version - information according to the current file-system state. + information according to the file store. \end{description} *} diff -r b627e76cc5cc -r 94596c573b38 src/Doc/Implementation/Syntax.thy --- a/src/Doc/Implementation/Syntax.thy Thu Jul 03 11:31:25 2014 +0200 +++ b/src/Doc/Implementation/Syntax.thy Thu Jul 03 12:17:55 2014 +0200 @@ -12,18 +12,18 @@ additional means for reading and printing of terms and types. This important add-on outside the logical core is called \emph{inner syntax} in Isabelle jargon, as opposed to the \emph{outer syntax} of - the theory and proof language (cf.\ \cite{isabelle-isar-ref}). + the theory and proof language \cite{isabelle-isar-ref}. - For example, according to \cite{church40} quantifiers are - represented as higher-order constants @{text "All :: ('a \ bool) \ - bool"} such that @{text "All (\x::'a. B x)"} faithfully represents - the idea that is displayed as @{text "\x::'a. B x"} via @{keyword - "binder"} notation. Moreover, type-inference in the style of - Hindley-Milner \cite{hindleymilner} (and extensions) enables users - to write @{text "\x. B x"} concisely, when the type @{text "'a"} is - already clear from the context.\footnote{Type-inference taken to the - extreme can easily confuse users, though. Beginners often stumble - over unexpectedly general types inferred by the system.} + For example, according to \cite{church40} quantifiers are represented as + higher-order constants @{text "All :: ('a \ bool) \ bool"} such that @{text + "All (\x::'a. B x)"} faithfully represents the idea that is displayed in + Isabelle as @{text "\x::'a. B x"} via @{keyword "binder"} notation. + Moreover, type-inference in the style of Hindley-Milner \cite{hindleymilner} + (and extensions) enables users to write @{text "\x. B x"} concisely, when + the type @{text "'a"} is already clear from the + context.\footnote{Type-inference taken to the extreme can easily confuse + users. Beginners often stumble over unexpectedly general types inferred by + the system.} \medskip The main inner syntax operations are \emph{read} for parsing together with type-checking, and \emph{pretty} for formatted @@ -43,18 +43,17 @@ \end{itemize} - Some specification package might thus intercept syntax processing at - a well-defined stage after @{text "parse"}, to a augment the - resulting pre-term before full type-reconstruction is performed by - @{text "check"}, for example. Note that the formal status of bound - variables, versus free variables, versus constants must not be - changed between these phases! + For example, some specification package might thus intercept syntax + processing at a well-defined stage after @{text "parse"}, to a augment the + resulting pre-term before full type-reconstruction is performed by @{text + "check"}. Note that the formal status of bound variables, versus free + variables, versus constants must not be changed between these phases. \medskip In general, @{text check} and @{text uncheck} operate simultaneously on a list of terms. This is particular important for type-checking, to reconstruct types for several terms of the same context and scope. In contrast, @{text parse} and @{text unparse} operate separately - in single terms. + on single terms. There are analogous operations to read and print types, with the same sub-division into phases. @@ -63,14 +62,15 @@ section {* Reading and pretty printing \label{sec:read-print} *} -text {* Read and print operations are roughly dual to each other, such - that for the user @{text "s' = pretty (read s)"} looks similar to - the original source text @{text "s"}, but the details depend on many - side-conditions. There are also explicit options to control - suppressing of type information in the output. The default - configuration routinely looses information, so @{text "t' = read - (pretty t)"} might fail, or produce a differently typed term, or a - completely different term in the face of syntactic overloading! *} +text {* + Read and print operations are roughly dual to each other, such that for the + user @{text "s' = pretty (read s)"} looks similar to the original source + text @{text "s"}, but the details depend on many side-conditions. There are + also explicit options to control the removal of type information in the + output. The default configuration routinely looses information, so @{text + "t' = read (pretty t)"} might fail, or produce a differently typed term, or + a completely different term in the face of syntactic overloading. +*} text %mlref {* \begin{mldecls} @@ -98,26 +98,27 @@ If particular type-constraints are required for some of the arguments, the read operations needs to be split into its parse and check phases. Then it - is possible to use @{ML Type.constraint} on the intermediate pre-terms. + is possible to use @{ML Type.constraint} on the intermediate pre-terms + \secref{sec:term-check}. \item @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a simultaneous list of source strings as terms of the logic, with an implicit type-constraint for each argument to enforce type @{typ prop}; this also - affects the inner syntax for parsing. The remaining type-reconstructions - works as for @{ML Syntax.read_terms} above. + affects the inner syntax for parsing. The remaining type-reconstruction + works as for @{ML Syntax.read_terms}. \item @{ML Syntax.read_typ}, @{ML Syntax.read_term}, @{ML Syntax.read_prop} - are like the simultaneous versions above, but operate on a single argument - only. This convenient shorthand is adequate in situations where a single - item in its own scope is processed. Do not use @{ML "map o - Syntax.read_term"} where @{ML Syntax.read_terms} is actually intended! + are like the simultaneous versions, but operate on a single argument only. + This convenient shorthand is adequate in situations where a single item in + its own scope is processed. Do not use @{ML "map o Syntax.read_term"} where + @{ML Syntax.read_terms} is actually intended! \item @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type or term, respectively. Although the uncheck phase acts on a simultaneous - list as well, this is rarely relevant in practice, so only the singleton - case is provided as combined pretty operation. There is no distinction of - term vs.\ proposition. + list as well, this is rarely used in practice, so only the singleton case is + provided as combined pretty operation. There is no distinction of term vs.\ + proposition. \item @{ML Syntax.string_of_typ} and @{ML Syntax.string_of_term} are convenient compositions of @{ML Syntax.pretty_typ} and @{ML @@ -130,11 +131,11 @@ @{ML Syntax.read_term}, @{ML Syntax.read_prop}, and @{ML Syntax.string_of_term} are the most important operations in practice. - \medskip Note that the string values that are passed in and out here are + \medskip Note that the string values that are passed in and out are annotated by the system, to carry further markup that is relevant for the Prover IDE \cite{isabelle-jedit}. User code should neither compose its own input strings, nor try to analyze the output strings. Conceptually this is - an abstract datatype, encoded into a concrete string for historical reasons. + an abstract datatype, encoded as concrete string for historical reasons. The standard way to provide the required position markup for input works via the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already @@ -147,47 +148,46 @@ section {* Parsing and unparsing \label{sec:parse-unparse} *} -text {* Parsing and unparsing converts between actual source text and - a certain \emph{pre-term} format, where all bindings and scopes are - resolved faithfully. Thus the names of free variables or constants - are already determined in the sense of the logical context, but type - information might be still missing. Pre-terms support an explicit - language of \emph{type constraints} that may be augmented by user - code to guide the later \emph{check} phase. +text {* + Parsing and unparsing converts between actual source text and a certain + \emph{pre-term} format, where all bindings and scopes are already resolved + faithfully. Thus the names of free variables or constants are determined in + the sense of the logical context, but type information might be still + missing. Pre-terms support an explicit language of \emph{type constraints} + that may be augmented by user code to guide the later \emph{check} phase. - Actual parsing is based on traditional lexical analysis and Earley - parsing for arbitrary context-free grammars. The user can specify - the grammar via mixfix annotations. Moreover, there are \emph{syntax - translations} that can be augmented by the user, either - declaratively via @{command translations} or programmatically via - @{command parse_translation}, @{command print_translation} etc. The - final scope-resolution is performed by the system, according to name - spaces for types, term variables and constants etc.\ determined by - the context. + Actual parsing is based on traditional lexical analysis and Earley parsing + for arbitrary context-free grammars. The user can specify the grammar + declaratively via mixfix annotations. Moreover, there are \emph{syntax + translations} that can be augmented by the user, either declaratively via + @{command translations} or programmatically via @{command + parse_translation}, @{command print_translation} \cite{isabelle-isar-ref}. + The final scope-resolution is performed by the system, according to name + spaces for types, term variables and constants determined by the context. *} text %mlref {* \begin{mldecls} @{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\ @{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\ - @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\ + @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\[0.5ex] @{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\ @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ \end{mldecls} \begin{description} - \item @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source strings as + \item @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source string as pre-type that is ready to be used with subsequent check operations. - \item @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source strings as + \item @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source string as pre-term that is ready to be used with subsequent check operations. - \item @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source strings as + \item @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source string as pre-term that is ready to be used with subsequent check operations. The inner syntax category is @{typ prop} and a suitable type-constraint is - included to ensure that this information is preserved during the check - phase. + included to ensure that this information is observed in subsequent type + reconstruction. \item @{ML Syntax.unparse_typ}~@{text "ctxt T"} unparses a type after uncheck operations, to turn it into a pretty tree. @@ -198,8 +198,8 @@ \end{description} - These operations always operate on single items; use the combinator @{ML - map} to apply them to a list of items. + These operations always operate on a single item; use the combinator @{ML + map} to apply them to a list. *} @@ -216,14 +216,14 @@ before pretty printing. A typical add-on for the check/uncheck syntax layer is the @{command - abbreviation} mechanism. Here the user specifies syntactic - definitions that are managed by the system as polymorphic @{text - "let"} bindings. These are expanded during the @{text "check"} - phase, and contracted during the @{text "uncheck"} phase, without - affecting the type-assignment of the given terms. + abbreviation} mechanism \cite{isabelle-isar-ref}. Here the user specifies + syntactic definitions that are managed by the system as polymorphic @{text + "let"} bindings. These are expanded during the @{text "check"} phase, and + contracted during the @{text "uncheck"} phase, without affecting the + type-assignment of the given terms. - \medskip The precise meaning of type checking depends on the context - --- additional check/uncheck plugins might be defined in user space. + \medskip The precise meaning of type checking depends on the context --- + additional check/uncheck modules might be defined in user space. For example, the @{command class} command defines a context where @{text "check"} treats certain type instances of overloaded @@ -237,7 +237,7 @@ \begin{mldecls} @{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\ @{index_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\ - @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\ + @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\[0.5ex] @{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\ @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ \end{mldecls} @@ -256,7 +256,7 @@ Applications sometimes need to check several types and terms together. The standard approach uses @{ML Logic.mk_type} to embed the language of types into that of terms; all arguments are appended into one list of terms that - is checked; afterwards the original type arguments are recovered with @{ML + is checked; afterwards the type arguments are recovered with @{ML Logic.dest_type}. \item @{ML Syntax.check_props}~@{text "ctxt ts"} checks a simultaneous list @@ -273,8 +273,8 @@ \end{description} - These operations always operate simultaneously on multiple items; use the - combinator @{ML singleton} to apply them to a single item. + These operations always operate simultaneously on a list; use the combinator + @{ML singleton} to apply them to a single item. *} end