1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Documents}% |
3 \def\isabellecontext{Documents}% |
4 \isamarkupfalse% |
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsection{Concrete syntax \label{sec:concrete-syntax}% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate infrastructure |
|
12 for concrete syntax is that of general \emph{mixfix |
|
13 annotations}\index{mixfix annotations|bold}. Associated with any |
|
14 kind of name and type declaration, mixfixes give rise both to |
|
15 grammar productions for the parser and output templates for the |
|
16 pretty printer. |
|
17 |
|
18 In full generality, the whole affair of parser and pretty printer |
|
19 configuration is rather subtle. Any syntax specifications given by |
|
20 end-users need to interact properly with the existing setup of |
|
21 Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further |
|
22 details. It is particularly important to get the precedence of new |
|
23 syntactic constructs right, avoiding ambiguities with existing |
|
24 elements. |
|
25 |
|
26 \medskip Subsequently we introduce a few simple declaration forms |
|
27 that already cover the most common situations fairly well.% |
|
28 \end{isamarkuptext}% |
|
29 \isamarkuptrue% |
|
30 % |
|
31 \isamarkupsubsection{Infixes% |
|
32 } |
|
33 \isamarkuptrue% |
|
34 % |
|
35 \begin{isamarkuptext}% |
|
36 Syntax annotations may be included wherever constants are declared |
|
37 directly or indirectly, including \isacommand{consts}, |
|
38 \isacommand{constdefs}, or \isacommand{datatype} (for the |
|
39 constructor operations). Type-constructors may be annotated as |
|
40 well, although this is less frequently encountered in practice |
|
41 (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind). |
|
42 |
|
43 Infix declarations\index{infix annotations|bold} provide a useful |
|
44 special case of mixfixes, where users need not care about the full |
|
45 details of priorities, nesting, spacing, etc. The subsequent |
|
46 example of the exclusive-or operation on boolean values illustrates |
|
47 typical infix declarations.% |
|
48 \end{isamarkuptext}% |
|
49 \isamarkuptrue% |
|
50 \isacommand{constdefs}\isanewline |
|
51 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
52 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
53 % |
|
54 \begin{isamarkuptext}% |
|
55 Any curried function with at least two arguments may be associated |
|
56 with infix syntax: \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to |
|
57 the same expression internally. In partial applications with less |
|
58 than two operands there is a special notation with \isa{op} prefix: |
|
59 \isa{xor} without arguments is represented as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; |
|
60 combined with plain prefix application this turns \isa{xor\ A} |
|
61 into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}. |
|
62 |
|
63 \medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above declaration |
|
64 refers to the bit of concrete syntax to represent the operator, |
|
65 while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the whole |
|
66 construct. |
|
67 |
|
68 As it happens, Isabelle/HOL already spends many popular combinations |
|
69 of ASCII symbols for its own use, including both \isa{{\isacharplus}} and |
|
70 \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the present |
|
71 \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. The current |
|
72 arrangement of inner syntax may be inspected via |
|
73 \commdx{print\protect\_syntax}, albeit its output is enormous. |
|
74 |
|
75 Operator precedence also needs some special considerations. The |
|
76 admissible range is 0--1000. Very low or high priorities are |
|
77 basically reserved for the meta-logic. Syntax of Isabelle/HOL |
|
78 mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is |
|
79 centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common |
|
80 HOL forms, or use the mostly unused range 100--900. |
|
81 |
|
82 \medskip The keyword \isakeyword{infixl} specifies an operator that |
|
83 is nested to the \emph{left}: in iterated applications the more |
|
84 complex expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly, |
|
85 \isakeyword{infixr} refers to nesting to the \emph{right}, which |
|
86 would turn \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} into \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. |
|
87 In contrast, a \emph{non-oriented} declaration via |
|
88 \isakeyword{infix} would always demand explicit parentheses. |
|
89 |
|
90 Many binary operations observe the associative law, so the exact |
|
91 grouping does not matter. Nevertheless, formal statements need be |
|
92 given in a particular format, associativity needs to be treated |
|
93 explicitly within the logic. Exclusive-or is happens to be |
|
94 associative, as shown below.% |
|
95 \end{isamarkuptext}% |
|
96 \isamarkuptrue% |
|
97 \isacommand{lemma}\ xor{\isacharunderscore}assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}{\isachardoublequote}\isanewline |
|
98 \ \ \isamarkupfalse% |
|
99 \isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
|
100 % |
|
101 \begin{isamarkuptext}% |
|
102 Such rules may be used in simplification to regroup nested |
|
103 expressions as required. Note that the system would actually print |
|
104 the above statement as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}} |
|
105 (due to nesting to the left). We have preferred to give the fully |
|
106 parenthesized form in the text for clarity.% |
|
107 \end{isamarkuptext}% |
|
108 \isamarkuptrue% |
|
109 \isamarkuptrue% |
|
110 \isamarkuptrue% |
|
111 \isamarkupfalse% |
|
112 \isamarkupfalse% |
|
113 \isamarkupfalse% |
|
114 \isamarkupfalse% |
|
115 \isamarkuptrue% |
|
116 \isamarkuptrue% |
|
117 \isamarkupfalse% |
|
118 \isamarkuptrue% |
|
119 \isamarkuptrue% |
|
120 \isamarkuptrue% |
|
121 \isamarkupfalse% |
|
122 \isamarkuptrue% |
|
123 \isamarkuptrue% |
|
124 \isamarkuptrue% |
|
125 \isamarkuptrue% |
|
126 \isamarkuptrue% |
|
127 \isamarkuptrue% |
|
128 \isamarkuptrue% |
5 \isamarkupfalse% |
129 \isamarkupfalse% |
6 \end{isabellebody}% |
130 \end{isabellebody}% |
7 %%% Local Variables: |
131 %%% Local Variables: |
8 %%% mode: latex |
132 %%% mode: latex |
9 %%% TeX-master: "root" |
133 %%% TeX-master: "root" |