--- a/doc-src/IsarImplementation/Thy/Syntax.thy Sun Oct 23 16:03:59 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy Sun Oct 23 23:11:53 2011 +0200
@@ -4,11 +4,61 @@
chapter {* Concrete syntax and type-checking *}
-text FIXME
+text {* Pure @{text "\<lambda>"}-calculus as introduced in \chref{ch:logic} is
+ an adequate foundation for logical languages --- in the tradition of
+ \emph{higher-order abstract syntax} --- but end-users require
+ 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.\ \chref{FIXME}).
+
+ 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 as @{text "\<forall>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 "\<forall>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.}
+
+ \medskip The main inner syntax operations are \emph{read} for
+ parsing together with type-checking, and \emph{pretty} for formatted
+ output. See also \secref{sec:read-print}.
+
+ Furthermore, the input and output syntax layers are sub-divided into
+ separate phases for \emph{concrete syntax} versus \emph{abstract
+ syntax}, see also \secref{sec:parse-unparse} and
+ \secref{sec:term-check}, respectively. This results in the
+ following decomposition of the main operations:
+
+ \begin{itemize}
+
+ \item @{text "read = parse; check"}
+
+ \item @{text "pretty = uncheck; unparse"}
+
+ \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 here! *}
+
section {* Reading and pretty printing \label{sec:read-print} *}
-text FIXME
+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, produce a differently typed term, or a
+ completely different term in the face of syntactic overloading! *}
text %mlref {*
\begin{mldecls}
@@ -29,7 +79,23 @@
section {* Parsing and unparsing \label{sec:parse-unparse} *}
-text FIXME
+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 is 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, for example.
+
+ Actual parsing is based on traditional lexical analysis and Earley
+ parsing for arbitrary context-free grammars. The user can specify
+ this 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, constants etc.\ determined by the context.
+*}
text %mlref {*
\begin{mldecls}
@@ -50,7 +116,33 @@
section {* Checking and unchecking \label{sec:term-check} *}
-text FIXME
+text {* These operations define the transition from pre-terms and
+ fully-annotated terms in the sense of the logical core
+ (\chref{ch:logic}).
+
+ The \emph{check} phase is meant to subsume a variety of mechanisms
+ in the manner of ``type-inference'' or ``type-reconstruction'' or
+ ``type-improvement'', not just type-checking in the narrow sense.
+ The \emph{uncheck} phase is roughly dual, it prunes type-information
+ 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.
+
+ \medskip The precise meaning of type checking depends on the context
+ --- additional check/unckeck plugins might be defined in user space!
+
+ For example, the @{command class} command defines a context where
+ @{text "check"} 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
+ certain locale parameters. See also \cite{Haftmann-Wenzel:2009}.
+*}
text %mlref {*
\begin{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex Sun Oct 23 16:03:59 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex Sun Oct 23 23:11:53 2011 +0200
@@ -23,7 +23,47 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+Pure \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus as introduced in \chref{ch:logic} is
+ an adequate foundation for logical languages --- in the tradition of
+ \emph{higher-order abstract syntax} --- but end-users require
+ 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.\ \chref{FIXME}).
+
+ For example, according to \cite{church40} quantifiers are
+ represented as higher-order constants \isa{All\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} such that \isa{All\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{29}{\isacharparenright}}} faithfully represents
+ the idea that is displayed as \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2E}{\isachardot}}\ B\ x} via \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} notation. Moreover, type-inference in the style of
+ Hindley-Milner \cite{hindleymilner} (and extensions) enables users
+ to write \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ B\ x} concisely, when the type \isa{{\isaliteral{27}{\isacharprime}}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.}
+
+ \medskip The main inner syntax operations are \emph{read} for
+ parsing together with type-checking, and \emph{pretty} for formatted
+ output. See also \secref{sec:read-print}.
+
+ Furthermore, the input and output syntax layers are sub-divided into
+ separate phases for \emph{concrete syntax} versus \emph{abstract
+ syntax}, see also \secref{sec:parse-unparse} and
+ \secref{sec:term-check}, respectively. This results in the
+ following decomposition of the main operations:
+
+ \begin{itemize}
+
+ \item \isa{read\ {\isaliteral{3D}{\isacharequal}}\ parse{\isaliteral{3B}{\isacharsemicolon}}\ check}
+
+ \item \isa{pretty\ {\isaliteral{3D}{\isacharequal}}\ uncheck{\isaliteral{3B}{\isacharsemicolon}}\ unparse}
+
+ \end{itemize}
+
+ Some specification package might thus intercept syntax processing at
+ a well-defined stage after \isa{parse}, to a augment the
+ resulting pre-term before full type-reconstruction is performed by
+ \isa{check}, for example. Note that the formal status of bound
+ variables, versus free variables, versus constants must not be
+ changed here!%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -32,7 +72,13 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+Read and print operations are roughly dual to each other, such
+ that for the user \isa{s{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ pretty\ {\isaliteral{28}{\isacharparenleft}}read\ s{\isaliteral{29}{\isacharparenright}}} looks similar to
+ the original source text \isa{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 \isa{t{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ read\ {\isaliteral{28}{\isacharparenleft}}pretty\ t{\isaliteral{29}{\isacharparenright}}} might fail, produce a differently typed term, or a
+ completely different term in the face of syntactic overloading!%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -71,7 +117,22 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+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 is 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, for example.
+
+ Actual parsing is based on traditional lexical analysis and Earley
+ parsing for arbitrary context-free grammars. The user can specify
+ this via mixfix annotations. Moreover, there are \emph{syntax
+ translations} that can be augmented by the user, either
+ declaratively via \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} or programmatically via
+ \hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}}, \hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}translation}}}} etc. The
+ final scope resolution is performed by the system, according to name
+ spaces for types, constants etc.\ determined by the context.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -110,7 +171,30 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+These operations define the transition from pre-terms and
+ fully-annotated terms in the sense of the logical core
+ (\chref{ch:logic}).
+
+ The \emph{check} phase is meant to subsume a variety of mechanisms
+ in the manner of ``type-inference'' or ``type-reconstruction'' or
+ ``type-improvement'', not just type-checking in the narrow sense.
+ The \emph{uncheck} phase is roughly dual, it prunes type-information
+ before pretty printing.
+
+ A typical add-on for the check/uncheck syntax layer is the \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}} mechanism. Here the user specifies syntactic
+ definitions that are managed by the system as polymorphic \isa{let} bindings. These are expanded during the \isa{check}
+ phase, and contracted during the \isa{uncheck} phase, without
+ affecting the type-assignment of the given terms.
+
+ \medskip The precise meaning of type checking depends on the context
+ --- additional check/unckeck plugins might be defined in user space!
+
+ For example, the \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} command defines a context where
+ \isa{check} 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
+ certain locale parameters. See also \cite{Haftmann-Wenzel:2009}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/manual.bib Sun Oct 23 16:03:59 2011 +0200
+++ b/doc-src/manual.bib Sun Oct 23 23:11:53 2011 +0200
@@ -628,6 +628,13 @@
year = {2009}
}
+@inproceedings{hindleymilner,
+ author = {L. Damas and H. Milner},
+ title = {Principal type schemes for functional programs},
+ booktitle = {ACM Symp. Principles of Programming Languages},
+ year = 1982
+}
+
@manual{isabelle-classes,
author = {Florian Haftmann},
title = {Haskell-style type classes with {Isabelle}/{Isar}},