--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sun Feb 05 18:11:19 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sun Feb 05 21:00:38 2012 +0100
@@ -382,10 +382,12 @@
Altogether this determines a production for a context-free priority
grammar, where for each argument @{text "i"} the syntactic category
- is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and
- the result category is determined from @{text "\<tau>"} (with
- priority @{text "p"}). Priority specifications are optional, with
- default 0 for arguments and 1000 for the result.
+ is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and the
+ result category is determined from @{text "\<tau>"} (with priority @{text
+ "p"}). Priority specifications are optional, with default 0 for
+ arguments and 1000 for the result.\footnote{Omitting priorities is
+ prone to syntactic ambiguities unless the delimiter tokens determine
+ fully bracketed notation, as in @{text "if _ then _ else _ fi"}.}
Since @{text "\<tau>"} may be again a function type, the constant
type scheme may have more argument positions than the mixfix
@@ -462,23 +464,23 @@
\begin{center}
\begin{tabular}{lll}
- @{verbatim "("}@{keyword "infix"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+ @{verbatim "("}@{keyword_def "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 ")"}
+ @{verbatim "("}@{keyword_def "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 ")"}
+ @{verbatim "("}@{keyword_def "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 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
@@ -492,8 +494,8 @@
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:
+ operators may be annotated with @{keyword_def "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 ")"}
@@ -1024,6 +1026,15 @@
@{command_def "no_translations"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
+ Unlike mixfix notation for existing formal entities
+ (\secref{sec:notation}), raw syntax declarations provide full access
+ to the priority grammar of the inner syntax. This includes
+ additional syntactic categories (via @{command nonterminal}) and
+ free-form grammar productions (via @{command syntax}). Additional
+ syntax translations (or macros, via @{command translations}) are
+ required to turn resulting parse trees into proper representations
+ of formal entities again.
+
@{rail "
@@{command nonterminal} (@{syntax name} + @'and')
;
@@ -1044,14 +1055,53 @@
constructor @{text c} (without arguments) to act as purely syntactic
type: a nonterminal symbol of the inner syntax.
- \item @{command "syntax"}~@{text "(mode) decls"} is similar to
- @{command "consts"}~@{text decls}, except that the actual logical
- signature extension is omitted. Thus the context free grammar of
- Isabelle's inner syntax may be augmented in arbitrary ways,
- independently of the logic. The @{text mode} argument refers to the
- print mode that the grammar rules belong; unless the @{keyword_ref
- "output"} indicator is given, all productions are added both to the
- input and output grammar.
+ \item @{command "syntax"}~@{text "(mode) c :: \<sigma> (mx)"} augments the
+ priority grammar and the pretty printer table for the given print
+ mode (default @{verbatim "\"\""}). An optional keyword @{keyword_ref
+ "output"} means that only the pretty printer table is affected.
+
+ Following \secref{sec:mixfix}, the mixfix annotation @{text "mx =
+ template ps q"} together with type @{text "\<sigma> = \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} and
+ specify a grammar production. The @{text template} contains
+ delimiter tokens that surround @{text "n"} argument positions
+ (@{verbatim "_"}). The latter correspond to nonterminal symbols
+ @{text "A\<^sub>i"} derived from the argument types @{text "\<tau>\<^sub>i"} as
+ follows:
+ \begin{itemize}
+
+ \item @{text "prop"} if @{text "\<tau>\<^sub>i = prop"}
+
+ \item @{text "logic"} if @{text "\<tau>\<^sub>i = (\<dots>)\<kappa>"} for logical type
+ constructor @{text "\<kappa> \<noteq> prop"}
+
+ \item @{text any} if @{text "\<tau>\<^sub>i = \<alpha>"} for type variables
+
+ \item @{text "\<kappa>"} if @{text "\<tau>\<^sub>i = \<kappa>"} for nonterminal @{text "\<kappa>"}
+ (syntactic type constructor)
+
+ \end{itemize}
+
+ Each @{text "A\<^sub>i"} is decorated by priority @{text "p\<^sub>i"} from the
+ given list @{text "ps"}; misssing priorities default to 0.
+
+ The resulting nonterminal of the production is determined similarly
+ from type @{text "\<tau>"}, with priority @{text "q"} and default 1000.
+
+ \medskip Parsing via this production produces parse trees @{text
+ "t\<^sub>1, \<dots>, t\<^sub>n"} for the argument slots. The resulting parse tree is
+ composed as @{text "c t\<^sub>1 \<dots> t\<^sub>n"}, by using the syntax constant @{text
+ "c"} of the syntax declaration.
+
+ Such syntactic constants are invented on the spot, without formal
+ check wrt.\ existing declarations. It is conventional to use plain
+ identifiers prefixed by a single underscore (e.g.\ @{text
+ "_foobar"}). Names should be chosen with care, to avoid clashes
+ with unrelated syntax declarations.
+
+ \medskip The special case of copy production is specified by @{text
+ "c = "}@{verbatim "\"\""} (empty string). It means that the
+ resulting parse tree @{text "t"} is copied directly, without any
+ further decoration.
\item @{command "no_syntax"}~@{text "(mode) decls"} removes grammar
declarations (and translations) resulting from @{text decls}, which
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Feb 05 18:11:19 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Feb 05 21:00:38 2012 +0100
@@ -508,10 +508,11 @@
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
- is determined by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} (with priority \isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}}), and
- the result category is determined from \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} (with
- priority \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}). Priority specifications are optional, with
- default 0 for arguments and 1000 for the result.
+ is determined by \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} (with priority \isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}}), and the
+ result category is determined from \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} (with priority \isa{{\isaliteral{22}{\isachardoublequote}}p{\isaliteral{22}{\isachardoublequote}}}). Priority specifications are optional, with default 0 for
+ arguments and 1000 for the result.\footnote{Omitting priorities is
+ prone to syntactic ambiguities unless the delimiter tokens determine
+ fully bracketed notation, as in \isa{{\isaliteral{22}{\isachardoublequote}}if\ {\isaliteral{5F}{\isacharunderscore}}\ then\ {\isaliteral{5F}{\isacharunderscore}}\ else\ {\isaliteral{5F}{\isacharunderscore}}\ fi{\isaliteral{22}{\isachardoublequote}}}.}
Since \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} may be again a function type, the constant
type scheme may have more argument positions than the mixfix
@@ -591,23 +592,23 @@
\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|)|
+ \verb|(|\indexdef{}{keyword}{infix}\hypertarget{keyword.infix}{\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|)|
+ \verb|(|\indexdef{}{keyword}{infixl}\hypertarget{keyword.infixl}{\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|)|
+ \verb|(|\indexdef{}{keyword}{infixr}\hypertarget{keyword.infixr}{\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 mixfix template \verb|"(_ |\isa{sy}\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
@@ -623,8 +624,8 @@
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:
+ operators may be annotated with \indexdef{}{keyword}{binder}\hypertarget{keyword.binder}{\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|)|
@@ -1201,6 +1202,15 @@
\indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}translations}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\end{matharray}
+ Unlike mixfix notation for existing formal entities
+ (\secref{sec:notation}), raw syntax declarations provide full access
+ to the priority grammar of the inner syntax. This includes
+ additional syntactic categories (via \hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}) and
+ free-form grammar productions (via \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}). Additional
+ syntax translations (or macros, via \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}) are
+ required to turn resulting parse trees into proper representations
+ of formal entities again.
+
\begin{railoutput}
\rail@begin{2}{}
\rail@term{\hyperlink{command.nonterminal}{\mbox{\isa{\isacommand{nonterminal}}}}}[]
@@ -1280,13 +1290,47 @@
constructor \isa{c} (without arguments) to act as purely syntactic
type: a nonterminal symbol of the inner syntax.
- \item \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}\ decls{\isaliteral{22}{\isachardoublequote}}} is similar to
- \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical
- signature extension is omitted. Thus the context free grammar of
- Isabelle's inner syntax may be augmented in arbitrary ways,
- independently of the logic. The \isa{mode} argument refers to the
- print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the
- input and output grammar.
+ \item \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}\ c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{28}{\isacharparenleft}}mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} augments the
+ priority grammar and the pretty printer table for the given print
+ mode (default \verb|""|). An optional keyword \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} means that only the pretty printer table is affected.
+
+ Following \secref{sec:mixfix}, the mixfix annotation \isa{{\isaliteral{22}{\isachardoublequote}}mx\ {\isaliteral{3D}{\isacharequal}}\ template\ ps\ q{\isaliteral{22}{\isachardoublequote}}} together with type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{3D}{\isacharequal}}\ {\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}}} and
+ specify a grammar production. The \isa{template} contains
+ delimiter tokens that surround \isa{{\isaliteral{22}{\isachardoublequote}}n{\isaliteral{22}{\isachardoublequote}}} argument positions
+ (\verb|_|). The latter correspond to nonterminal symbols
+ \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} derived from the argument types \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} as
+ follows:
+ \begin{itemize}
+
+ \item \isa{{\isaliteral{22}{\isachardoublequote}}prop{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ prop{\isaliteral{22}{\isachardoublequote}}}
+
+ \item \isa{{\isaliteral{22}{\isachardoublequote}}logic{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} for logical type
+ constructor \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ prop{\isaliteral{22}{\isachardoublequote}}}
+
+ \item \isa{any} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}} for type variables
+
+ \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}} for nonterminal \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{22}{\isachardoublequote}}}
+ (syntactic type constructor)
+
+ \end{itemize}
+
+ Each \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} is decorated by priority \isa{{\isaliteral{22}{\isachardoublequote}}p\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} from the
+ given list \isa{{\isaliteral{22}{\isachardoublequote}}ps{\isaliteral{22}{\isachardoublequote}}}; misssing priorities default to 0.
+
+ The resulting nonterminal of the production is determined similarly
+ from type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}}, with priority \isa{{\isaliteral{22}{\isachardoublequote}}q{\isaliteral{22}{\isachardoublequote}}} and default 1000.
+
+ \medskip Parsing via this production produces parse trees \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} for the argument slots. The resulting parse tree is
+ composed as \isa{{\isaliteral{22}{\isachardoublequote}}c\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, by using the syntax constant \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} of the syntax declaration.
+
+ Such syntactic constants are invented on the spot, without formal
+ check wrt.\ existing declarations. It is conventional to use plain
+ identifiers prefixed by a single underscore (e.g.\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}foobar{\isaliteral{22}{\isachardoublequote}}}). Names should be chosen with care, to avoid clashes
+ with unrelated syntax declarations.
+
+ \medskip The special case of copy production is specified by \isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}}\verb|""| (empty string). It means that the
+ resulting parse tree \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} is copied directly, without any
+ further decoration.
\item \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isaliteral{5F}{\isacharunderscore}}syntax}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}\ decls{\isaliteral{22}{\isachardoublequote}}} removes grammar
declarations (and translations) resulting from \isa{decls}, which
--- a/doc-src/Ref/defining.tex Sun Feb 05 18:11:19 2012 +0100
+++ b/doc-src/Ref/defining.tex Sun Feb 05 21:00:38 2012 +0100
@@ -3,60 +3,6 @@
\section{Mixfix declarations} \label{sec:mixfix}
-\subsection{The general mixfix form}
-Here is a detailed account of mixfix declarations. Suppose the following
-line occurs within a {\tt consts} or {\tt syntax} section of a {\tt .thy}
-file:
-\begin{center}
- {\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)}
-\end{center}
-This constant declaration and mixfix annotation are interpreted as follows:
-\begin{itemize}\index{productions}
-\item The string {\tt $c$} is the name of the constant associated with the
- production; unless it is a valid identifier, it must be enclosed in
- quotes. If $c$ is empty (given as~{\tt ""}) then this is a copy
- production.\index{productions!copy} Otherwise, parsing an instance of the
- phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$
- $a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th
- argument.
-
- \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
- $\sigma = [\tau@1, \dots, \tau@n] \To \tau$. Nonterminal symbols are
- derived from the types $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described
- below. Any of these may be function types.
-
-\end{itemize}
-%
-The resulting production is \[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\,
-A@2^{(p@2)}\, \dots\, A@n^{(p@n)}\, w@n \] where $A$ and the $A@i$ are the
-nonterminals corresponding to the types $\tau$ and $\tau@i$ respectively.
-The nonterminal symbol associated with a type $(\ldots)ty$ is {\tt logic}, if
-this is a logical type (namely one of class {\tt logic} excluding {\tt
-prop}). Otherwise it is $ty$ (note that only the outermost type constructor
-is taken into account). Finally, the nonterminal of a type variable is {\tt
-any}.
-
-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
-of the function's $n$ arguments. The constant's name, in this case~$f$, will
-also serve as the label in the abstract syntax tree.
-
-You may also declare mixfix syntax without adding constants to the theory's
-signature, by using a {\tt syntax} section instead of {\tt consts}. Thus a
-production need not map directly to a logical function (this typically
-requires additional syntactic translations, see also
-Chapter~\ref{chap:syntax}).
-
-
-\medskip
-Omitting priorities is prone to syntactic ambiguities unless
-the production's right-hand side is fully bracketed, as in
-\verb|"if _ then _ else _ fi"|.
-
-
\subsection{Example: arithmetic expressions}
\index{examples!of mixfix declarations}
This theory specification contains a {\tt syntax} section with mixfix