382 A mixfix annotation defines a production of the priority grammar. It |
382 A mixfix annotation defines a production of the priority grammar. It |
383 describes the concrete syntax, the translation to abstract syntax, and the |
383 describes the concrete syntax, the translation to abstract syntax, and the |
384 pretty printing. Special case annotations provide a simple means of |
384 pretty printing. Special case annotations provide a simple means of |
385 specifying infix operators and binders. |
385 specifying infix operators and binders. |
386 |
386 |
387 |
|
388 %% FIXME remove |
|
389 %\subsection{Grammar productions}\label{sec:grammar}\index{productions} |
|
390 % |
|
391 %Let us examine the treatment of the production |
|
392 %\[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\, A@2^{(p@2)}\, \ldots\, |
|
393 % A@n^{(p@n)}\, w@n. \] |
|
394 %Here $A@i^{(p@i)}$ is a nonterminal with priority~$p@i$ for $i=1$, |
|
395 %\ldots,~$n$, while $w@0$, \ldots,~$w@n$ are strings of terminals. |
|
396 %In the corresponding mixfix annotation, the priorities are given separately |
|
397 %as $[p@1,\ldots,p@n]$ and~$p$. The nonterminal symbols are derived from |
|
398 %types~$\tau$, $\tau@1$, \ldots,~$\tau@n$ respectively, and the production's |
|
399 %effect on nonterminals is expressed as the function type |
|
400 %\[ [\tau@1, \ldots, \tau@n]\To \tau. \] |
|
401 %Finally, the template |
|
402 %\[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n \] |
|
403 %describes the strings of terminals. |
|
404 |
|
405 |
|
406 \subsection{The general mixfix form} |
387 \subsection{The general mixfix form} |
407 Here is a detailed account of mixfix declarations. Suppose the following |
388 Here is a detailed account of mixfix declarations. Suppose the following |
408 line occurs within a {\tt consts} or {\tt syntax} section of a {\tt .thy} |
389 line occurs within a {\tt consts} or {\tt syntax} section of a {\tt .thy} |
409 file: |
390 file: |
410 \begin{center} |
391 \begin{center} |
625 \end{ttbox} |
606 \end{ttbox} |
626 introduces a constant~$c$ of type~$\sigma$, which must have the form |
607 introduces a constant~$c$ of type~$\sigma$, which must have the form |
627 $(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where |
608 $(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where |
628 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$ |
609 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$ |
629 and the whole term has type~$\tau@3$. The optional integer $pb$ |
610 and the whole term has type~$\tau@3$. The optional integer $pb$ |
630 specifies the body's priority which defaults to 0. Special characters |
611 specifies the body's priority, by default~$p$. Special characters |
631 in $\Q$ must be escaped using a single quote. |
612 in $\Q$ must be escaped using a single quote. |
632 |
613 |
633 The declaration is expanded internally to something like |
614 The declaration is expanded internally to something like |
634 \begin{ttbox} |
615 \begin{ttbox} |
635 \(c\) :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)" |
616 \(c\) :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)" |