--- a/src/Doc/Implementation/Syntax.thy Tue Oct 20 23:03:46 2015 +0200
+++ b/src/Doc/Implementation/Syntax.thy Tue Oct 20 23:53:40 2015 +0200
@@ -6,7 +6,7 @@
chapter \<open>Concrete syntax and type-checking\<close>
-text \<open>Pure @{text "\<lambda>"}-calculus as introduced in \chref{ch:logic} is
+text \<open>Pure \<open>\<lambda>\<close>-calculus as introduced in \chref{ch:logic} is
an adequate foundation for logical languages --- in the tradition of
\<^emph>\<open>higher-order abstract syntax\<close> --- but end-users require
additional means for reading and printing of terms and types. This
@@ -15,12 +15,11 @@
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 \<Rightarrow> bool) \<Rightarrow> bool"} such that @{text
- "All (\<lambda>x::'a. B x)"} faithfully represents the idea that is displayed in
- Isabelle as @{text "\<forall>x::'a. B x"} via @{keyword "binder"} notation.
+ higher-order constants \<open>All :: ('a \<Rightarrow> bool) \<Rightarrow> bool\<close> such that \<open>All (\<lambda>x::'a. B x)\<close> faithfully represents the idea that is displayed in
+ Isabelle as \<open>\<forall>x::'a. B x\<close> via @{keyword "binder"} notation.
Moreover, type-inference in the style of Hindley-Milner @{cite hindleymilner}
- (and extensions) enables users to write @{text "\<forall>x. B x"} concisely, when
- the type @{text "'a"} is already clear from the
+ (and extensions) enables users to write \<open>\<forall>x. B x\<close> concisely, when
+ the type \<open>'a\<close> 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.}
@@ -36,22 +35,21 @@
\secref{sec:term-check}, respectively. This results in the
following decomposition of the main operations:
- \<^item> @{text "read = parse; check"}
+ \<^item> \<open>read = parse; check\<close>
- \<^item> @{text "pretty = uncheck; unparse"}
+ \<^item> \<open>pretty = uncheck; unparse\<close>
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
+ processing at a well-defined stage after \<open>parse\<close>, to a augment the
+ resulting pre-term before full type-reconstruction is performed by \<open>check\<close>. 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
+ In general, \<open>check\<close> and \<open>uncheck\<close> 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
+ and scope. In contrast, \<open>parse\<close> and \<open>unparse\<close> operate separately
on single terms.
There are analogous operations to read and print types, with the same
@@ -63,11 +61,10 @@
text \<open>
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
+ user \<open>s' = pretty (read s)\<close> looks similar to the original source
+ text \<open>s\<close>, 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
+ output. The default configuration routinely looses information, so \<open>t' = read (pretty t)\<close> might fail, or produce a differently typed term, or
a completely different term in the face of syntactic overloading.
\<close>
@@ -85,10 +82,10 @@
@{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\
\end{mldecls}
- \<^descr> @{ML Syntax.read_typs}~@{text "ctxt strs"} parses and checks a
+ \<^descr> @{ML Syntax.read_typs}~\<open>ctxt strs\<close> parses and checks a
simultaneous list of source strings as types of the logic.
- \<^descr> @{ML Syntax.read_terms}~@{text "ctxt strs"} parses and checks a
+ \<^descr> @{ML Syntax.read_terms}~\<open>ctxt strs\<close> parses and checks a
simultaneous list of source strings as terms of the logic.
Type-reconstruction puts all parsed terms into the same scope: types of
free variables ultimately need to coincide.
@@ -98,7 +95,7 @@
is possible to use @{ML Type.constraint} on the intermediate pre-terms
(\secref{sec:term-check}).
- \<^descr> @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a
+ \<^descr> @{ML Syntax.read_props}~\<open>ctxt strs\<close> 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-reconstruction
@@ -110,8 +107,8 @@
its own scope is processed. Do not use @{ML "map o Syntax.read_term"} where
@{ML Syntax.read_terms} is actually intended!
- \<^descr> @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML
- Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type
+ \<^descr> @{ML Syntax.pretty_typ}~\<open>ctxt T\<close> and @{ML
+ Syntax.pretty_term}~\<open>ctxt t\<close> uncheck and pretty-print the given type
or term, respectively. Although the uncheck phase acts on a simultaneous
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.\
@@ -173,22 +170,22 @@
@{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
\end{mldecls}
- \<^descr> @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source string as
+ \<^descr> @{ML Syntax.parse_typ}~\<open>ctxt str\<close> parses a source string as
pre-type that is ready to be used with subsequent check operations.
- \<^descr> @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source string as
+ \<^descr> @{ML Syntax.parse_term}~\<open>ctxt str\<close> parses a source string as
pre-term that is ready to be used with subsequent check operations.
- \<^descr> @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source string as
+ \<^descr> @{ML Syntax.parse_prop}~\<open>ctxt str\<close> 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 observed in subsequent type
reconstruction.
- \<^descr> @{ML Syntax.unparse_typ}~@{text "ctxt T"} unparses a type after
+ \<^descr> @{ML Syntax.unparse_typ}~\<open>ctxt T\<close> unparses a type after
uncheck operations, to turn it into a pretty tree.
- \<^descr> @{ML Syntax.unparse_term}~@{text "ctxt T"} unparses a term after
+ \<^descr> @{ML Syntax.unparse_term}~\<open>ctxt T\<close> unparses a term after
uncheck operations, to turn it into a pretty tree. There is no distinction
for propositions here.
@@ -212,9 +209,8 @@
A typical add-on for the check/uncheck syntax layer is the @{command
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
+ syntactic definitions that are managed by the system as polymorphic \<open>let\<close> bindings. These are expanded during the \<open>check\<close> phase, and
+ contracted during the \<open>uncheck\<close> phase, without affecting the
type-assignment of the given terms.
\<^medskip>
@@ -222,7 +218,7 @@
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
+ \<open>check\<close> treats certain type instances of overloaded
constants according to the ``dictionary construction'' of its
logical foundation. This involves ``type improvement''
(specialization of slightly too general types) and replacement by
@@ -238,11 +234,11 @@
@{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
\end{mldecls}
- \<^descr> @{ML Syntax.check_typs}~@{text "ctxt Ts"} checks a simultaneous list
+ \<^descr> @{ML Syntax.check_typs}~\<open>ctxt Ts\<close> checks a simultaneous list
of pre-types as types of the logic. Typically, this involves normalization
of type synonyms.
- \<^descr> @{ML Syntax.check_terms}~@{text "ctxt ts"} checks a simultaneous list
+ \<^descr> @{ML Syntax.check_terms}~\<open>ctxt ts\<close> checks a simultaneous list
of pre-terms as terms of the logic. Typically, this involves type-inference
and normalization term abbreviations. The types within the given terms are
treated in the same way as for @{ML Syntax.check_typs}.
@@ -253,15 +249,15 @@
is checked; afterwards the type arguments are recovered with @{ML
Logic.dest_type}.
- \<^descr> @{ML Syntax.check_props}~@{text "ctxt ts"} checks a simultaneous list
+ \<^descr> @{ML Syntax.check_props}~\<open>ctxt ts\<close> checks a simultaneous list
of pre-terms as terms of the logic, such that all terms are constrained by
type @{typ prop}. The remaining check operation works as @{ML
Syntax.check_terms} above.
- \<^descr> @{ML Syntax.uncheck_typs}~@{text "ctxt Ts"} unchecks a simultaneous
+ \<^descr> @{ML Syntax.uncheck_typs}~\<open>ctxt Ts\<close> unchecks a simultaneous
list of types of the logic, in preparation of pretty printing.
- \<^descr> @{ML Syntax.uncheck_terms}~@{text "ctxt ts"} unchecks a simultaneous
+ \<^descr> @{ML Syntax.uncheck_terms}~\<open>ctxt ts\<close> unchecks a simultaneous
list of terms of the logic, in preparation of pretty printing. There is no
distinction for propositions here.