--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Feb 04 16:08:19 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Feb 04 18:33:04 2012 +0100
@@ -335,8 +335,15 @@
text {* Mixfix annotations specify concrete \emph{inner syntax} of
Isabelle types and terms. Locally fixed parameters in toplevel
- theorem statements, locale specifications etc.\ also admit mixfix
- annotations.
+ theorem statements, locale and class specifications also admit
+ mixfix annotations in a fairly uniform manner. A mixfix annotation
+ describes describes the concrete syntax, the translation to abstract
+ syntax, and the pretty printing. Special case annotations provide a
+ simple means of specifying infix operators and binders.
+
+ Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}. It allows
+ to specify any context-free priority grammar, which is more general
+ than the fixity declarations of ML and Prolog.
@{rail "
@{syntax_def mixfix}: '(' mfix ')'
@@ -344,29 +351,34 @@
@{syntax_def struct_mixfix}: '(' ( mfix | @'structure' ) ')'
;
- mfix: @{syntax string} prios? @{syntax nat}? |
- (@'infix' | @'infixl' | @'infixr') @{syntax string} @{syntax nat} |
- @'binder' @{syntax string} prios? @{syntax nat}
+ mfix: @{syntax template} prios? @{syntax nat}? |
+ (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
+ @'binder' @{syntax template} prios? @{syntax nat}
+ ;
+ template: string
;
prios: '[' (@{syntax nat} + ',') ']'
"}
- Here the @{syntax string} specifications refer to the actual mixfix
- template, which may include literal text, spacing, blocks, and
- arguments (denoted by ``@{text _}''); the special symbol
- ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
- argument that specifies an implicit structure reference (see also
- \secref{sec:locale}). Infix and binder declarations provide common
- abbreviations for particular mixfix declarations. So in practice,
- mixfix templates mostly degenerate to literal text for concrete
- syntax, such as ``@{verbatim "++"}'' for an infix symbol.
+ The string given as @{text template} may include literal text,
+ spacing, blocks, and arguments (denoted by ``@{text _}''); the
+ special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
+ represents an index argument that specifies an implicit structure
+ reference (see also \secref{sec:locale}). Infix and binder
+ declarations provide common abbreviations for particular mixfix
+ declarations. So in practice, mixfix templates mostly degenerate to
+ literal text for concrete syntax, such as ``@{verbatim "++"}'' for
+ an infix symbol.
+*}
- \medskip In full generality, mixfix declarations work as follows.
- Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is
- annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text
- "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of
- delimiters that surround argument positions as indicated by
- underscores.
+
+subsection {* The general mixfix form *}
+
+text {* In full generality, mixfix declarations work as follows.
+ Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is annotated by
+ @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text "mixfix"} is a string
+ @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of delimiters that surround
+ argument positions as indicated by underscores.
Altogether this determines a production for a context-free priority
grammar, where for each argument @{text "i"} the syntactic category
@@ -437,16 +449,84 @@
\end{description}
- For example, the template @{verbatim "(_ +/ _)"} specifies an infix
- operator. There are two argument positions; the delimiter
- @{verbatim "+"} is preceded by a space and followed by a space or
- line break; the entire phrase is a pretty printing block.
-
The general idea of pretty printing with blocks and breaks is also
described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}.
*}
+subsection {* Infixes *}
+
+text {* Infix operators are specified by convenient short forms that
+ abbreviate general mixfix annotations as follows:
+
+ \begin{center}
+ \begin{tabular}{lll}
+
+ @{verbatim "("}@{keyword "infix"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+ & @{text "\<mapsto>"} &
+ @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
+ @{verbatim "("}@{keyword "infixl"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+ & @{text "\<mapsto>"} &
+ @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
+ @{verbatim "("}@{keyword "infixr"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+ & @{text "\<mapsto>"} &
+ @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
+
+ \end{tabular}
+ \end{center}
+
+ The mixfix template @{verbatim "\"(_ "}@{text sy}@{verbatim "/
+ _)\""} specifies two argument positions; the delimiter is preceded
+ by a space and followed by a space or line break; the entire phrase
+ is a pretty printing block.
+
+ The alternative notation @{verbatim "op"}~@{text sy} is introduced
+ in addition. Thus any infix operator may be written in prefix form
+ (as in ML), independently of the number of arguments in the term.
+*}
+
+
+subsection {* Binders *}
+
+text {* A \emph{binder} is a variable-binding construct such as a
+ quantifier. The idea to formalize @{text "\<forall>x. b"} as @{text "All
+ (\<lambda>x. b)"} for @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} already goes back
+ to \cite{church40}. Isabelle declarations of certain higher-order
+ operators may be annotated with @{keyword "binder"} annotations as
+ follows:
+
+ \begin{center}
+ @{text "c :: "}@{verbatim "\""}@{text "(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\" ("}@{keyword "binder"}@{verbatim " \""}@{text "sy"}@{verbatim "\" ["}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
+ \end{center}
+
+ This introduces concrete binder syntax @{text "sy x. b"}, where
+ @{text x} is a bound variable of type @{text "\<tau>\<^sub>1"}, the body @{text
+ b} has type @{text "\<tau>\<^sub>2"} and the whole term has type @{text "\<tau>\<^sub>3"}.
+ The optional integer @{text p} specifies the syntactic priority of
+ the body; the default is @{text "q"}, which is also the priority of
+ the whole construct.
+
+ Internally, the binder syntax is expanded to something like this:
+ \begin{center}
+ @{text "c_binder :: "}@{verbatim "\""}@{text "idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\" (\"(3"}@{text sy}@{verbatim "_./ _)\" [0, "}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
+ \end{center}
+
+ Here @{syntax (inner) idts} is the nonterminal symbol for a list of
+ identifiers with optional type constraints (see also
+ \secref{sec:pure-grammar}). The mixfix template @{verbatim
+ "\"(3"}@{text sy}@{verbatim "_./ _)\""} defines argument positions
+ for the bound identifiers and the body, separated by a dot with
+ optional line break; the entire phrase is a pretty printing block of
+ indentation level 3. Note that there is no extra space after @{text
+ "sy"}, so it needs to be included user specification if the binder
+ syntax ends with a token that may be continued by an identifier
+ token at the start of @{syntax (inner) idts}.
+
+ Furthermore, a syntax translation to transforms @{text "c_binder x\<^sub>1
+ \<dots> x\<^sub>n b"} into iterated application @{text "c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)"}.
+ This works in both directions, for parsing and printing. *}
+
+
section {* Explicit notation \label{sec:notation} *}
text {*
@@ -630,7 +710,7 @@
*}
-subsection {* The Pure grammar *}
+subsection {* The Pure grammar \label{sec:pure-grammar} *}
text {* The priority grammar of the @{text "Pure"} theory is defined
approximately like this:
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 16:08:19 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 18:33:04 2012 +0100
@@ -412,8 +412,15 @@
\begin{isamarkuptext}%
Mixfix annotations specify concrete \emph{inner syntax} of
Isabelle types and terms. Locally fixed parameters in toplevel
- theorem statements, locale specifications etc.\ also admit mixfix
- annotations.
+ theorem statements, locale and class specifications also admit
+ mixfix annotations in a fairly uniform manner. A mixfix annotation
+ describes describes the concrete syntax, the translation to abstract
+ syntax, and the pretty printing. Special case annotations provide a
+ simple means of specifying infix operators and binders.
+
+ Isabelle mixfix syntax is inspired by {\OBJ} \cite{OBJ}. It allows
+ to specify any context-free priority grammar, which is more general
+ than the fixity declarations of ML and Prolog.
\begin{railoutput}
\rail@begin{1}{\indexdef{}{syntax}{mixfix}\hypertarget{syntax.mixfix}{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}}
@@ -432,7 +439,7 @@
\rail@end
\rail@begin{7}{\isa{mfix}}
\rail@bar
-\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
+\rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\isa{prios}}[]
@@ -449,11 +456,11 @@
\rail@nextbar{4}
\rail@term{\isa{\isakeyword{infixr}}}[]
\rail@endbar
-\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
+\rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[]
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@nextbar{5}
\rail@term{\isa{\isakeyword{binder}}}[]
-\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
+\rail@nont{\hyperlink{syntax.template}{\mbox{\isa{template}}}}[]
\rail@bar
\rail@nextbar{6}
\rail@nont{\isa{prios}}[]
@@ -461,6 +468,9 @@
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@end
+\rail@begin{1}{\isa{template}}
+\rail@nont{\isa{string}}[]
+\rail@end
\rail@begin{2}{\isa{prios}}
\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
\rail@plus
@@ -473,21 +483,28 @@
\end{railoutput}
- Here the \hyperlink{syntax.string}{\mbox{\isa{string}}} specifications refer to the actual mixfix
- template, which may include literal text, spacing, blocks, and
- arguments (denoted by ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''); the special symbol
- ``\verb|\<index>|'' (printed as ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}}'') represents an index
- argument that specifies an implicit structure reference (see also
- \secref{sec:locale}). Infix and binder declarations provide common
- abbreviations for particular mixfix declarations. So in practice,
- mixfix templates mostly degenerate to literal text for concrete
- syntax, such as ``\verb|++|'' for an infix symbol.
-
- \medskip In full generality, mixfix declarations work as follows.
- Suppose a constant \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} is
- annotated by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mixfix\ {\isaliteral{5B}{\isacharbrackleft}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}mixfix{\isaliteral{22}{\isachardoublequote}}} is a string \isa{{\isaliteral{22}{\isachardoublequote}}d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} consisting of
- delimiters that surround argument positions as indicated by
- underscores.
+ The string given as \isa{template} may include literal text,
+ spacing, blocks, and arguments (denoted by ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''); the
+ special symbol ``\verb|\<index>|'' (printed as ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}}'')
+ represents an index argument that specifies an implicit structure
+ reference (see also \secref{sec:locale}). Infix and binder
+ declarations provide common abbreviations for particular mixfix
+ declarations. So in practice, mixfix templates mostly degenerate to
+ literal text for concrete syntax, such as ``\verb|++|'' for
+ an infix symbol.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The general mixfix form%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In full generality, mixfix declarations work as follows.
+ Suppose a constant \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} is annotated by
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mixfix\ {\isaliteral{5B}{\isacharbrackleft}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ p\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}mixfix{\isaliteral{22}{\isachardoublequote}}} is a string
+ \isa{{\isaliteral{22}{\isachardoublequote}}d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5F}{\isacharunderscore}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} consisting of delimiters that surround
+ argument positions as indicated by underscores.
Altogether this determines a production for a context-free priority
grammar, where for each argument \isa{{\isaliteral{22}{\isachardoublequote}}i{\isaliteral{22}{\isachardoublequote}}} the syntactic category
@@ -558,16 +575,86 @@
\end{description}
- For example, the template \verb|(_ +/ _)| specifies an infix
- operator. There are two argument positions; the delimiter
- \verb|+| is preceded by a space and followed by a space or
- line break; the entire phrase is a pretty printing block.
-
The general idea of pretty printing with blocks and breaks is also
described in \cite{paulson-ml2}; it goes back to \cite{Oppen:1980}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Infixes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Infix operators are specified by convenient short forms that
+ abbreviate general mixfix annotations as follows:
+
+ \begin{center}
+ \begin{tabular}{lll}
+
+ \verb|(|\hyperlink{keyword.infix}{\mbox{\isa{\isakeyword{infix}}}}~\verb|"|\isa{sy}\verb|"| \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|)|
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} &
+ \verb|("(_ |\isa{sy}\verb|/ _)" [|\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|, |\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|]|\isa{{\isaliteral{22}{\isachardoublequote}}\ p{\isaliteral{22}{\isachardoublequote}}}\verb|)| \\
+ \verb|(|\hyperlink{keyword.infixl}{\mbox{\isa{\isakeyword{infixl}}}}~\verb|"|\isa{sy}\verb|"| \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|)|
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} &
+ \verb|("(_ |\isa{sy}\verb|/ _)" [|\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|, |\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|]|\isa{{\isaliteral{22}{\isachardoublequote}}\ p{\isaliteral{22}{\isachardoublequote}}}\verb|)| \\
+ \verb|(|\hyperlink{keyword.infixr}{\mbox{\isa{\isakeyword{infixr}}}}~\verb|"|\isa{sy}\verb|"| \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|)|
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}{\isaliteral{22}{\isachardoublequote}}} &
+ \verb|("(_ |\isa{sy}\verb|/ _)" [|\isa{{\isaliteral{22}{\isachardoublequote}}p\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}\verb|, |\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|]|\isa{{\isaliteral{22}{\isachardoublequote}}\ p{\isaliteral{22}{\isachardoublequote}}}\verb|)| \\
+
+ \end{tabular}
+ \end{center}
+
+ The mixfix template \verb|"(_ |\isa{sy}\verb|/|\isasep\isanewline%
+\verb| _)"| specifies two argument positions; the delimiter is preceded
+ by a space and followed by a space or line break; the entire phrase
+ is a pretty printing block.
+
+ The alternative notation \verb|op|~\isa{sy} is introduced
+ in addition. Thus any infix operator may be written in prefix form
+ (as in ML), independently of the number of arguments in the term.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Binders%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A \emph{binder} is a variable-binding construct such as a
+ quantifier. The idea to formalize \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{22}{\isachardoublequote}}} as \isa{{\isaliteral{22}{\isachardoublequote}}All\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} for \isa{{\isaliteral{22}{\isachardoublequote}}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{\isaliteral{22}{\isachardoublequote}}} already goes back
+ to \cite{church40}. Isabelle declarations of certain higher-order
+ operators may be annotated with \hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}} annotations as
+ follows:
+
+ \begin{center}
+ \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|"|\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}\verb|" (|\hyperlink{keyword.binder}{\mbox{\isa{\isakeyword{binder}}}}\verb| "|\isa{{\isaliteral{22}{\isachardoublequote}}sy{\isaliteral{22}{\isachardoublequote}}}\verb|" [|\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|] |\isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}\verb|)|
+ \end{center}
+
+ This introduces concrete binder syntax \isa{{\isaliteral{22}{\isachardoublequote}}sy\ x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{22}{\isachardoublequote}}}, where
+ \isa{x} is a bound variable of type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, the body \isa{b} has type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} and the whole term has type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}.
+ The optional integer \isa{p} specifies the syntactic priority of
+ the body; the default is \isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}, which is also the priority of
+ the whole construct.
+
+ Internally, the binder syntax is expanded to something like this:
+ \begin{center}
+ \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}binder\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|"|\isa{{\isaliteral{22}{\isachardoublequote}}idts\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}}\verb|" ("(3|\isa{sy}\verb|_./ _)" [0, |\isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}\verb|] |\isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}}\verb|)|
+ \end{center}
+
+ Here \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}} is the nonterminal symbol for a list of
+ identifiers with optional type constraints (see also
+ \secref{sec:pure-grammar}). The mixfix template \verb|"(3|\isa{sy}\verb|_./ _)"| defines argument positions
+ for the bound identifiers and the body, separated by a dot with
+ optional line break; the entire phrase is a pretty printing block of
+ indentation level 3. Note that there is no extra space after \isa{{\isaliteral{22}{\isachardoublequote}}sy{\isaliteral{22}{\isachardoublequote}}}, so it needs to be included user specification if the binder
+ syntax ends with a token that may be continued by an identifier
+ token at the start of \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}.
+
+ Furthermore, a syntax translation to transforms \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5F}{\isacharunderscore}}binder\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ b{\isaliteral{22}{\isachardoublequote}}} into iterated application \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
+ This works in both directions, for parsing and printing.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Explicit notation \label{sec:notation}%
}
\isamarkuptrue%
@@ -805,7 +892,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{The Pure grammar%
+\isamarkupsubsection{The Pure grammar \label{sec:pure-grammar}%
}
\isamarkuptrue%
%
--- a/doc-src/Ref/defining.tex Sat Feb 04 16:08:19 2012 +0100
+++ b/doc-src/Ref/defining.tex Sat Feb 04 18:33:04 2012 +0100
@@ -2,19 +2,6 @@
\chapter{Defining Logics} \label{Defining-Logics}
\section{Mixfix declarations} \label{sec:mixfix}
-\index{mixfix declarations|(}
-
-When defining a theory, you declare new constants by giving their names,
-their type, and an optional {\bf mixfix annotation}. Mixfix annotations
-allow you to extend Isabelle's basic $\lambda$-calculus syntax with
-readable notation. They can express any context-free priority grammar.
-Isabelle syntax definitions are inspired by \OBJ~\cite{OBJ}; they are more
-general than the priority declarations of \ML\ and Prolog.
-
-A mixfix annotation defines a production of the priority grammar. It
-describes the concrete syntax, the translation to abstract syntax, and the
-pretty printing. Special case annotations provide a simple means of
-specifying infix operators and binders.
\subsection{The general mixfix form}
Here is a detailed account of mixfix declarations. Suppose the following
@@ -33,18 +20,6 @@
$a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th
argument.
- \item The constant $c$, if non-empty, is declared to have type $\sigma$
- ({\tt consts} section only).
-
- \item The string $template$ specifies the right-hand side of
- the production. It has the form
- \[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n, \]
- where each occurrence of {\tt_} denotes an argument position and
- the~$w@i$ do not contain~{\tt _}. (If you want a literal~{\tt _} in
- the concrete syntax, you must escape it as described below.) The $w@i$
- may consist of \rmindex{delimiters}, spaces or
- \rmindex{pretty printing} annotations (see below).
-
\item The type $\sigma$ specifies the production's nonterminal symbols
(or name tokens). If $template$ is of the form above then $\sigma$
must be a function type with at least~$n$ argument positions, say
@@ -52,15 +27,6 @@
derived from the types $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described
below. Any of these may be function types.
- \item The optional list~$ps$ may contain at most $n$ integers, say {\tt
- [$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal
- priority\indexbold{priorities} required of any phrase that may appear
- as the $i$-th argument. Missing priorities default to~0.
-
- \item The integer $p$ is the priority of this production. If
- omitted, it defaults to the maximal priority. Priorities range
- between 0 and \ttindexbold{max_pri} (= 1000).
-
\end{itemize}
%
The resulting production is \[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\,
@@ -72,15 +38,6 @@
is taken into account). Finally, the nonterminal of a type variable is {\tt
any}.
-\begin{warn}
- Theories must sometimes declare types for purely syntactic purposes ---
- merely playing the role of nonterminals. One example is \tydx{type}, the
- built-in type of types. This is a `type of all types' in the syntactic
- sense only. Do not declare such types under {\tt arities} as belonging to
- class {\tt logic}\index{*logic class}, for that would make them useless as
- separate nonterminal symbols.
-\end{warn}
-
Associating nonterminals with types allows a constant's type to specify
syntax as well. We can declare the function~$f$ to have type $[\tau@1,
\ldots, \tau@n]\To \tau$ and, through a mixfix annotation, specify the layout
@@ -95,20 +52,10 @@
\medskip
-As a special case of the general mixfix declaration, the form
-\begin{center}
- {\tt $c$ ::\ "$\sigma$" ("$template$")}
-\end{center}
-specifies no priorities. The resulting production puts no priority
-constraints on any of its arguments and has maximal priority itself.
-Omitting priorities in this manner is prone to syntactic ambiguities unless
+Omitting priorities is prone to syntactic ambiguities unless
the production's right-hand side is fully bracketed, as in
\verb|"if _ then _ else _ fi"|.
-Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"},
-is sensible only if~$c$ is an identifier. Otherwise you will be unable to
-write terms involving~$c$.
-
\subsection{Example: arithmetic expressions}
\index{examples!of mixfix declarations}
@@ -136,93 +83,6 @@
{\out exp = "-" exp[3] => "-" (3)}
\end{ttbox}
-Note that because {\tt exp} is not of class {\tt logic}, it has been
-retained as a separate nonterminal. This also entails that the syntax
-does not provide for identifiers or paranthesized expressions.
-Normally you would also want to add the declaration {\tt arities
- exp::logic} after {\tt types} and use {\tt consts} instead of {\tt
- syntax}. Try this as an exercise and study the changes in the
-grammar.
-
-
-\subsection{Infixes}
-\indexbold{infixes}
-
-Infix operators associating to the left or right can be declared using
-{\tt infixl} or {\tt infixr}. Basically, the form {\tt $c$ ::\
- $\sigma$ (infixl $p$)} abbreviates the mixfix declarations
-\begin{ttbox}
-"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
-"op \(c\)" :: \(\sigma\) ("op \(c\)")
-\end{ttbox}
-and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations
-\begin{ttbox}
-"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
-"op \(c\)" :: \(\sigma\) ("op \(c\)")
-\end{ttbox}
-The infix operator is declared as a constant with the prefix {\tt op}.
-Thus, prefixing infixes with \sdx{op} makes them behave like ordinary
-function symbols, as in \ML. Special characters occurring in~$c$ must be
-escaped, as in delimiters, using a single quote.
-
-A slightly more general form of infix declarations allows constant
-names to be independent from their concrete syntax, namely \texttt{$c$
- ::\ $\sigma$\ (infixl "$sy$" $p$)}, the same for \texttt{infixr}. As
-an example consider:
-\begin{ttbox}
-and :: [bool, bool] => bool (infixr "&" 35)
-\end{ttbox}
-The internal constant name will then be just \texttt{and}, without any
-\texttt{op} prefixed.
-
-
-\subsection{Binders}
-\indexbold{binders}
-\begingroup
-\def\Q{{\cal Q}}
-A {\bf binder} is a variable-binding construct such as a quantifier. The
-constant declaration
-\begin{ttbox}
-\(c\) :: \(\sigma\) (binder "\(\Q\)" [\(pb\)] \(p\))
-\end{ttbox}
-introduces a constant~$c$ of type~$\sigma$, which must have the form
-$(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where
-$x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
-and the whole term has type~$\tau@3$. The optional integer $pb$
-specifies the body's priority, by default~$p$. Special characters
-in $\Q$ must be escaped using a single quote.
-
-The declaration is expanded internally to something like
-\begin{ttbox}
-\(c\)\hskip3pt :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)
-"\(\Q\)" :: [idts, \(\tau@2\)] => \(\tau@3\) ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
-\end{ttbox}
-Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
-\index{type constraints}
-optional type constraints (see Fig.\ts\ref{fig:pure_gram}). The
-declaration also installs a parse translation\index{translations!parse}
-for~$\Q$ and a print translation\index{translations!print} for~$c$ to
-translate between the internal and external forms.
-
-A binder of type $(\sigma \To \tau) \To \tau$ can be nested by giving a
-list of variables. The external form $\Q~x@1~x@2 \ldots x@n. P$
-corresponds to the internal form
-\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \]
-
-\medskip
-For example, let us declare the quantifier~$\forall$:\index{quantifiers}
-\begin{ttbox}
-All :: ('a => o) => o (binder "ALL " 10)
-\end{ttbox}
-This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
- $x$.$P$}. When printing, Isabelle prefers the latter form, but must fall
-back on ${\tt All}(P)$ if $P$ is not an abstraction. Both $P$ and {\tt ALL
- $x$.$P$} have type~$o$, the type of formulae, while the bound variable
-can be polymorphic.
-\endgroup
-
-\index{mixfix declarations|)}
-
\section{Ambiguity of parsed expressions} \label{sec:ambiguity}
\index{ambiguity!of parsed expressions}