6 V & ::= & & \mbox{(\bf values)} \\
7 & & \verb+Term+~T & \mbox{(term)} \\
8 & | & \verb+String+~s & \mbox{(string)} \\
9 & | & \verb+Number+~n & \mbox{(number)} \\
10 & | & \verb+None+ & \mbox{(optional value)} \\
11 & | & \verb+Some+~V & \mbox{(optional value)} \\
12 & | & [V_1,\dots,V_n] & \mbox{(list value)} \\[2ex]
16 An environment is a map $\mathcal E : \mathit{Name} -> V$.
18 \section{Level 1: concrete syntax}
21 \caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut}
25 P & ::= & & \mbox{(\bf patterns)} \\
27 S & ::= & & \mbox{(\bf simple patterns)} \\
29 & | & S~\verb+\sub+~S\\
30 & | & S~\verb+\sup+~S\\
31 & | & S~\verb+\below+~S\\
32 & | & S~\verb+\atop+~S\\
33 & | & S~\verb+\over+~S\\
34 & | & S~\verb+\atop+~S\\
35 & | & \verb+\frac+~S~S \\
36 & | & \verb+\sqrt+~S \\
37 & | & \verb+\root+~S~\verb+\of+~S \\
38 & | & \verb+(+~P~\verb+)+ \\
39 & | & \verb+hbox (+~P~\verb+)+ \\
40 & | & \verb+vbox (+~P~\verb+)+ \\
41 & | & \verb+hvbox (+~P~\verb+)+ \\
42 & | & \verb+hovbox (+~P~\verb+)+ \\
44 & | & \verb+list0+~S~[\verb+sep+~l] \\
45 & | & \verb+list1+~S~[\verb+sep+~l] \\
47 & | & [\verb+term+]~x \\
48 & | & \verb+number+~x \\
49 & | & \verb+ident+~x \\
55 Rationale: while the layout schemata can occur in the concrete syntax
56 used by user, the box schemata and the magic patterns can only occur
57 when defining the notation. This is why the layout schemata are
58 ``escaped'' with a backslash, so that they cannot be confused with
59 plain identifiers, wherease the others are not. Alternatively, they
60 could be defined as keywords, but this would prevent their names to be
61 used in different contexts.
64 \caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut}
67 \begin{array}{@{}ll@{}}
68 \begin{array}[t]{rcll}
69 T & ::= & & \mbox{(\bf terms)} \\
70 & & L_\kappa[T_1,\dots,T_n] & \mbox{(layout)} \\
71 & | & B_\kappa^{ab}[T_1\cdots T_n] & \mbox{(box)} \\
72 & | & \BREAK & \mbox{(breakpoint)} \\
73 & | & \FENCED{T_1\cdots T_n} & \mbox{(fenced)} \\
74 & | & l & \mbox{(literal)} \\[2ex]
75 P & ::= & & \mbox{(\bf patterns)} \\
76 & & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
77 & | & B_\kappa^{ab}[P_1\cdots P_n] & \mbox{(box)} \\
78 & | & \BREAK & \mbox{(breakpoint)} \\
79 & | & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
80 & | & M & \mbox{(magic)} \\
81 & | & V & \mbox{(variable)} \\
82 & | & l & \mbox{(literal)} \\
84 \begin{array}[t]{rcll}
85 V & ::= & & \mbox{(\bf variables)} \\
86 & & \TVAR{x} & \mbox{(term variable)} \\
87 & | & \NVAR{x} & \mbox{(number variable)} \\
88 & | & \IVAR{x} & \mbox{(name variable)} \\[2ex]
89 M & ::= & & \mbox{(\bf magic patterns)} \\
90 & & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
91 & | & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
92 & | & \verb+opt+~P & \mbox{(option)} \\[2ex]
100 \ITO{\cdot}{{}} : P -> \mathit{Env} -> T
104 \caption{\label{tab:il1f2} Instantiation of level 1 patterns from level 2.\strut}
108 \ITO{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\ITO{(P_1)}{E},\dots,\ITO{(P_n)}{E} ] \\
109 \ITO{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
110 \ITO{\BREAK}{E} & = & \BREAK \\
111 \ITO{(P)}{E} & = & \ITO{P}{E} \\
112 \ITO{(P_1\cdots P_n)}{E} & = & B_H^{00}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
113 \ITO{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
114 \ITO{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
115 \ITO{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
116 \ITO{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\
117 \ITO{\mathtt{opt}~P}{E} & = & \ITO{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
118 & & & \mathcal{E}'(x)=\left\{
120 v, & \mathcal{E}(x) = \mathtt{Some}~v \\
121 \mathcal{E}(x), & \mbox{otherwise}
124 \ITO{\mathtt{list}k~P~l?}{E} & = & \ITO{P}{{E}_1}~{l?}\cdots {l?}~\ITO{P}{{E}_n} &
125 \mathcal{E}(\NAMES(P)) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\
127 & & & \mathcal{E}_i(x) = \left\{
129 v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\
130 \mathcal{E}(x), & \mbox{otherwise}
133 \ITO{l}{E} & = & l \\
135 %% & | & (P) & \mbox{(fenced)} \\
136 %% & | & M & \mbox{(magic)} \\
137 %% & | & V & \mbox{(variable)} \\
138 %% & | & l & \mbox{(literal)} \\[2ex]
139 %% V & ::= & & \mbox{(\bf variables)} \\
140 %% & & \TVAR{x} & \mbox{(term variable)} \\
141 %% & | & \NVAR{x} & \mbox{(number variable)} \\
142 %% & | & \IVAR{x} & \mbox{(name variable)} \\[2ex]
143 %% M & ::= & & \mbox{(\bf magic patterns)} \\
144 %% & & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
145 %% & | & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
146 %% & | & \verb+opt+~S & \mbox{(option)} \\[2ex]
153 \caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut}
156 \renewcommand{\arraystretch}{3.5}
157 \begin{array}[t]{@{}c@{}}
158 \inference[\sc layout]
159 {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
160 {L_\kappa[P_1,\dots,P_n] :: D_1\oplus\cdots\oplus D_n}
163 {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
164 {B_\kappa^{ab}[P_1\cdots P_n] :: D_1\oplus\cdots\oplus D_n}
166 \inference[\sc fenced]
167 {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
168 {\FENCED{P_1\cdots P_n} :: D_1\oplus\cdots\oplus D_n}
170 \inference[\sc breakpoint]
172 {\BREAK :: \emptyset}
174 \inference[\sc literal]
180 {\TVAR{x} :: \TVAR{x}}
184 {\NVAR{x} :: \NVAR{x}}
188 {\IVAR{x} :: \IVAR{x}}
190 \inference[\sc list0]
191 {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
192 {\mathtt{list0}~P~l? :: D'}
194 \inference[\sc list1]
195 {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
196 {\mathtt{list1}~P~l? :: D'}
199 {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}}
200 {\mathtt{opt}~P :: D'}
206 \newcommand{\ATTRS}[1]{\langle#1\rangle}
207 \newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}}
210 \caption{\label{tab:addparens} Can't read the AST and need parentheses? Here you go!.\strut}
214 \ADDPARENS{l}{n} & = & l \\
215 \ADDPARENS{\BREAK}{n} & = & \BREAK \\
216 \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \ADDPARENS{T}{m} & n < m \\
217 \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} & n > m \\
218 \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=L,\mathit{pos}=R}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
219 \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=R,\mathit{pos}=L}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
220 \ADDPARENS{\ATTRS{\cdots}T}{n} & = & \ADDPARENS{T}{n} \\
221 \ADDPARENS{L_\kappa[T_1,\dots,\underline{T_k},\dots,T_m]}{n} & = & L_\kappa[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_k}{\bot},\dots,\ADDPARENS{T_m}{n}] \\
222 \ADDPARENS{B_\kappa^{ab}[T_1,\dots,T_m]}{n} & = & B_\kappa^{ab}[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_m}{n}]
229 \caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut}
233 \ANNPOS{l}{p,q} & = & l \\
234 \ANNPOS{\BREAK}{p,q} & = & \BREAK \\
235 \ANNPOS{x}{1,0} & = & \ATTRS{\mathit{pos}=L}{x} \\
236 \ANNPOS{x}{0,1} & = & \ATTRS{\mathit{pos}=R}{x} \\
237 \ANNPOS{x}{p,q} & = & \ATTRS{\mathit{pos}=I}{x} \\
238 \ANNPOS{B_\kappa^{ab}[P]}{p,q} & = & B_\kappa^{ab}[\ANNPOS{P}{p,q}] \\
239 \ANNPOS{B_\kappa^{ab}[\{\BREAK\} P_1\cdots P_n\{\BREAK\}]}{p,q} & = & B_\kappa^{ab}[\begin{array}[t]{@{}l}
240 \{\BREAK\} \ANNPOS{P_1}{p,0} \\
241 \ANNPOS{P_2}{0,0}\cdots\ANNPOS{P_{n-1}}{0,0} \\
242 \ANNPOS{P_n}{0,q}\{\BREAK\}]
245 %% & & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
246 %% & | & \BREAK & \mbox{(breakpoint)} \\
247 %% & | & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
248 %% V & ::= & & \mbox{(\bf variables)} \\
249 %% & & \TVAR{x} & \mbox{(term variable)} \\
250 %% & | & \NVAR{x} & \mbox{(number variable)} \\
251 %% & | & \IVAR{x} & \mbox{(name variable)} \\[2ex]
252 %% M & ::= & & \mbox{(\bf magic patterns)} \\
253 %% & & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
254 %% & | & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
255 %% & | & \verb+opt+~P & \mbox{(option)} \\[2ex]
261 \section{Level 2: abstract syntax}
263 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
266 \caption{\label{tab:synl2} Concrete syntax of level 2 patterns.\strut}
269 \begin{array}{@{}rcll@{}}
270 \NT{term} & ::= & & \mbox{\bf terms} \\
271 & & x & \mbox{(identifier)} \\
272 & | & n & \mbox{(number)} \\
273 & | & s & \mbox{(symbol)} \\
274 & | & \mathrm{URI} & \mbox{(URI)} \\
275 & | & \verb+?+ & \mbox{(implicit)} \\
276 & | & \verb+%+ & \mbox{(placeholder)} \\
277 & | & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
278 & | & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
279 & | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
280 & | & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
281 & | & \NT{term}~\NT{term} & \mbox{(application)} \\
282 & | & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
283 & | & [\verb+[+~\NT{term}~\verb+]+]~\verb+match+~\NT{term}~\verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \mbox{(pattern match)} \\
284 & | & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
285 & | & \verb+(+~\NT{term}~\verb+)+ \\
286 & | & \BLOB(\NT{meta},\dots,\NT{meta}) & \mbox{(meta blob)} \\
287 \NT{defs} & ::= & & \mbox{\bf mutual definitions} \\
288 & & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
289 \NT{fun} & ::= & & \mbox{\bf functions} \\
290 & & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
291 \NT{binder} & ::= & & \mbox{\bf binders} \\
292 & & \verb+\Pi+ \mid \verb+\exists+ \mid \verb+\forall+ \mid \verb+\lambda+ \\
293 \NT{arg} & ::= & & \mbox{\bf single argument} \\
294 & & \verb+_+ \mid x \mid \BLOB(\NT{meta},\dots,\NT{meta}) \\
295 \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
297 & | & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
298 \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
300 & | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
301 \NT{kind} & ::= & & \mbox{\bf induction kind} \\
302 & & \verb+rec+ \mid \verb+corec+ \\
303 \NT{rule} & ::= & & \mbox{\bf rules} \\
304 & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]
306 \NT{meta} & ::= & & \mbox{\bf meta} \\
307 & & \BLOB(\NT{term},\dots,\NT{term}) & \mbox{(term blob)} \\
308 & | & [\verb+term+]~x \\
309 & | & \verb+number+~x \\
310 & | & \verb+ident+~x \\
311 & | & \verb+fresh+~x \\
312 & | & \verb+anonymous+ \\
313 & | & \verb+fold+~[\verb+left+\mid\verb+right+]~\NT{meta}~\verb+rec+~x~\NT{meta} \\
314 & | & \verb+default+~\NT{meta}~\NT{meta} \\
315 & | & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
323 \caption{\label{tab:wfl2} Well-formedness rules for level 2 patterns.\strut}
326 \renewcommand{\arraystretch}{3.5}
327 \begin{array}{@{}c@{}}
328 \inference[\sc Constr]
330 {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\
331 \inference[\sc TermVar]
333 {\mathtt{term}~x :: x : \mathtt{Term}}
335 \inference[\sc NumVar]
337 {\mathtt{number}~x :: x : \mathtt{Number}}
339 \inference[\sc IdentVar]
341 {\mathtt{ident}~x :: x : \mathtt{String}}
343 \inference[\sc FreshVar]
345 {\mathtt{fresh}~x :: x : \mathtt{String}}
347 \inference[\sc Success]
349 {\mathtt{anonymous} :: \emptyset}
352 {P_1 :: D_1 & P_2 :: D_2 \oplus (x : \mathtt{Term}) & \DOMAIN(D_2)\ne\emptyset & \DOMAIN(D_1)\cap\DOMAIN(D_2)=\emptyset}
353 {\mathtt{fold}~P_1~\mathtt{rec}~x~P_2 :: D_1 \oplus D_2~\mathtt{List}}
355 \inference[\sc Default]
356 {P_1 :: D \oplus D_1 & P_2 :: D & \DOMAIN(D_1) \ne \emptyset & \DOMAIN(D) \cap \DOMAIN(D_1) = \emptyset}
357 {\mathtt{default}~P_1~P_2 :: D \oplus D_1~\mathtt{Option}}
360 {P_1 :: \emptyset & P_2 :: D & P_3 :: D }
361 {\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 :: D}
365 {\mathtt{fail} :: \emptyset}
366 %% & | & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
374 \caption{\label{tab:il2f1} Instantiation of level 2 patterns from level 1.
380 \IOT{C[t_1,\dots,t_n]}{\mathcal{E}} & =
381 & C[\IOT{t_1}{\mathcal{E}},\dots,\IOT{t_n}{\mathcal{E}}] \\
383 \IOT{\mathtt{term}~x}{\mathcal{E}} & = & t & \mathcal{E}(x) = \mathtt{Term}~t \\
385 \IOT{\mathtt{number}~x}{\mathcal{E}} & =
386 & n & \mathcal{E}(x) = \mathtt{Number}~n \\
388 \IOT{\mathtt{ident}~x}{\mathcal{E}} & =
389 & y & \mathcal{E}(x) = \mathtt{String}~y \\
391 \IOT{\mathtt{fresh}~x}{\mathcal{E}} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\
393 \IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & =
394 & \IOT{P_1}{\UPDATE{\mathcal{E}}{x_i|->v_i}}
395 & \mathcal{E}(x_i)=\mathtt{Some}~v_i \\
396 & & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\
398 \IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & =
399 & \IOT{P_2}{\UPDATE{\mathcal{E}}{x_i|->\bot}}
400 & \mathcal{E}(x_i)=\mathtt{None} \\
401 & & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\
403 \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
405 & \IOT{P_1}{\mathcal{E}'}
406 & \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[],\dots,[]\} \\
407 & & \multicolumn{2}{l}{\mathcal{E}'=\UPDATE{\mathcal{E}}{\NAMES(P_2)\setminus\{x\}|->\bot}}
410 \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
412 & \IOT{P_2}{\mathcal{E}'}
413 & \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\
414 & & & \NAMES(P_2)\setminus\{x\}=\{y_1,\dots,y_m\} \\
415 & & \multicolumn{2}{l}{\mathcal{E}'(y) =
418 \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_e}{\mathcal{E}''}
421 \mathcal{E}(y) & \mbox{otherwise} \\
424 & & \multicolumn{2}{l}{\mathcal{E}''(y) =
427 [v_{i2};\dots;v_{in}] & y=y_i \\
428 \mathcal{E}(y) & \mbox{otherwise} \\
432 \IOT{\mathtt{fold}~\mathtt{left}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
434 & \mathit{eval\_fold}(x,P_2,\mathcal{E}')
436 & & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->
437 \IOT{P_1}{\UPDATE{\mathcal{E}}{\NAMES(P_2)|->\bot}}}} \\
439 \mathit{eval\_fold}(x,P,\mathcal{E})
442 & \mathcal{E}(\NAMES(P)\setminus\{x\})=\{[],\dots,[]\} \\
444 \mathit{eval\_fold}(x,P,\mathcal{E})
446 & \mathit{eval\_fold}(x,P,\mathcal{E}')
447 & \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\
448 & & & \NAMES(P)\setminus{x}=\{y_1,\dots,y_m\} \\
450 & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->\IOT{P}{\mathcal{E}''}; ~ y_i |-> [v_{i2};\dots;v_{in_i}]}}
453 & \multicolumn{2}{l}{\mathcal{E}''(y) =
456 v_1 & y\in \NAMES(P)\setminus\{x\} \\
457 \mathcal{E}(x) & y=x \\
458 \bot & \mathit{otherwise} \\
469 \caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
472 \renewcommand{\arraystretch}{3.5}
473 \begin{array}{@{}c@{}}
474 \inference[\sc Constr]
475 {t_i \in P_i ~> \mathcal E_i & i\ne j => \DOMAIN(\mathcal E_i)\cap\DOMAIN(\mathcal E_j)=\emptyset}
476 {C[t_1,\dots,t_n] \in C[P_1,\dots,P_n] ~> \mathcal E_1 \oplus \cdots \oplus \mathcal E_n}
478 \inference[\sc TermVar]
480 {t \in [\mathtt{term}]~x ~> [x |-> \mathtt{Term}~t]}
482 \inference[\sc NumVar]
484 {n \in \mathtt{number}~x ~> [x |-> \mathtt{Number}~n]}
486 \inference[\sc IdentVar]
488 {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
490 \inference[\sc FreshVar]
492 {x \in \mathtt{fresh}~x ~> [x |-> \mathtt{String}~x]}
494 \inference[\sc Success]
496 {t \in \mathtt{anonymous} ~> \emptyset}
498 \inference[\sc DefaultT]
499 {t \in P_1 ~> \mathcal E}
500 {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
502 \mathcal E'(x) = \left\{
503 \renewcommand{\arraystretch}{1}
505 \mathtt{Some}~\mathcal{E}(x) & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
506 \mathcal{E}(x) & \mbox{otherwise}
510 \inference[\sc DefaultF]
511 {t \not\in P_1 & t \in P_2 ~> \mathcal E}
512 {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
514 \mathcal E'(x) = \left\{
515 \renewcommand{\arraystretch}{1}
517 \mathtt{None} & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
518 \mathcal{E}(x) & \mbox{otherwise}
523 {t \in P_1 ~> \mathcal E' & t \in P_2 ~> \mathcal E}
524 {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
527 {t \not\in P_1 & t \in P_3 ~> \mathcal E}
528 {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
530 \inference[\sc FoldRec]
531 {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
532 {t \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
534 \mbox{where}~\mathcal{E}''(y) = \left\{
535 \renewcommand{\arraystretch}{1}
537 \mathcal{E}(y)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{right} \\
538 \mathcal{E}'(y)@[\mathcal{E}(y)] & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{left} \\
539 \mathcal{E}'(y) & \mbox{otherwise}
543 \inference[\sc FoldBase]
544 {t \not\in P_2 & t \in P_1 ~> \mathcal E}
545 {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
547 \mathcal E'(y) = \left\{
548 \renewcommand{\arraystretch}{1}
550 [] & y \in \NAMES(P_2) \setminus \{x\} \\
551 \mathcal{E}(y) & \mbox{otherwise}
560 \caption{\label{tab:synl3} Abstract syntax of level 3 terms and patterns.}
563 \begin{array}{@{}ll@{}}
564 \begin{array}[t]{rcll}
565 T & : := & & \mbox{(\bf terms)} \\
566 & & u & \mbox{(uri)} \\
567 & | & \lambda x.T & \mbox{($\lambda$-abstraction)} \\
568 & | & (T_1 \dots T_n) & \mbox{(application)} \\
571 \begin{array}[t]{rcll}
572 P & : := & & \mbox{(\bf patterns)} \\
573 & & u & \mbox{(uri)} \\
574 & | & V & \mbox{(variable)} \\
575 & | & (P_1 \dots P_n) & \mbox{(application)} \\[2ex]
576 V & : := & & \mbox{(\bf variables)} \\
577 & & \TVAR{x} & \mbox{(term variable)} \\
578 & | & \IMPVAR & \mbox{(implicit variable)} \\
586 \caption{\label{tab:wfl3} Well-formedness rules for level 3 patterns.\strut}
589 \renewcommand{\arraystretch}{3.5}
590 \begin{array}{@{}c@{}}
591 \inference[\sc Uri] {} {u :: \emptyset} \quad
592 \inference[\sc ImpVar] {} {\TVAR{x} :: \emptyset} \quad
593 \inference[\sc TermVar] {} {\TVAR{x} :: x:\mathtt{Term}} \\
596 \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset}
597 {P_1\cdots P_n :: D_1\oplus\cdots\oplus D_n} \\
604 \caption{\label{tab:synargp} Abstract syntax of applicative symbol patterns.}
608 P & : := & & \mbox{(\bf patterns)} \\
609 & & s ~ \{ \mathit{arg} \} & \mbox{(symbol pattern)} \\[2ex]
610 \mathit{arg} & : := & & \mbox{(\bf argument)} \\
611 & & \TVAR{x} & \mbox{(term variable)} \\
612 & | & \eta.\mathit{arg} & \mbox{($\eta$-abstraction)} \\
619 \caption{\label{tab:wfargp} Well-formedness rules for applicative symbol
623 \renewcommand{\arraystretch}{3.5}
624 \begin{array}{@{}c@{}}
625 \inference[\sc Pattern]
626 {\mathit{arg}_i :: D_i
627 \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset}
628 {s~\mathit{arg}_1\cdots\mathit{arg}_n :: D_1\oplus\cdots\oplus D_n} \\
629 \inference[\sc TermVar]
631 {\TVAR{x} :: x : \mathtt{Term}}
633 \inference[\sc EtaAbs]
635 {\eta.\mathit{arg} :: D}
643 \caption{\label{tab:l3match} Pattern matching of level 3 terms.\strut}
646 \renewcommand{\arraystretch}{3.5}
647 \begin{array}{@{}c@{}}
648 \inference[\sc Uri] {} {u\in u ~> []} \quad
649 \inference[\sc Appl] {t_i\in P_i ~> \mathcal{E}_i}
650 {(t_1\dots t_n)\in(P_1\dots P_n) ~>
651 \mathcal{E}_1\oplus\cdots\oplus\mathcal{E}_n} \\
652 \inference[\sc TermVar] {} {t\in \TVAR{x} ~> [x |-> \mathtt{Term}~t]} \quad
653 \inference[\sc ImpVar] {} {t\in \IMPVAR ~> []} \\
660 \caption{\label{tab:iapf3} Instantiation of applicative symbol patterns (from
665 \IAP{s~a_1\cdots a_n}{\mathcal{E}} & = &
666 (s~\IAPP{a_1}{\mathcal{E}}{0}\cdots\IAPP{a_n}{\mathcal{E}}{0}) & \\
667 \IAPP{\TVAR{x}}{\mathcal{E}}{0} & = & t & \mathcal{E}(x)=\mathtt{Term}~t \\
668 \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & = & \lambda y.\IAPP{t}{\mathcal{E}}{i}
669 & \mathcal{E}(x)=\mathtt{Term}~\lambda y.t \\
670 \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & =
671 & \lambda y_1.\cdots.\lambda y_{i+1}.t~y_1\cdots y_{i+1}
672 & \mathcal{E}(x)=\mathtt{Term}~t\wedge\forall y,t\neq\lambda y.t \\
673 \IAPP{\eta.a}{\mathcal{E}}{i} & = & \IAPP{a}{\mathcal{E}}{i+1} \\
679 \section{Type checking}
681 \subsection{Level 1 $<->$ Level 2}
683 \newcommand{\GUARDED}{\mathit{guarded}}
684 \newcommand{\TRUE}{\mathit{true}}
685 \newcommand{\FALSE}{\mathit{false}}
687 \newcommand{\TN}{\mathit{tn}}
690 \caption{\label{tab:guarded} Guarded condition of level 2
691 pattern. Note that the recursive case of the \texttt{fold} magic is
692 not explicitly required to be guarded. The point is that it must
693 contain at least two distinct names, and this guarantees that whatever
694 is matched by the recursive pattern, the terms matched by those two
695 names will be smaller than the whole matched term.\strut} \hrule
698 \GUARDED(C(M(P))) & = & \GUARDED(P) \\
699 \GUARDED(C(t_1,\dots,t_n)) & = & \TRUE \\
700 \GUARDED(\mathtt{term}~x) & = & \FALSE \\
701 \GUARDED(\mathtt{number}~x) & = & \FALSE \\
702 \GUARDED(\mathtt{ident}~x) & = & \FALSE \\
703 \GUARDED(\mathtt{fresh}~x) & = & \FALSE \\
704 \GUARDED(\mathtt{anonymous}) & = & \TRUE \\
705 \GUARDED(\mathtt{default}~P_1~P_2) & = & \GUARDED(P_1) \wedge \GUARDED(P_2) \\
706 \GUARDED(\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3) & = & \GUARDED(P_2) \wedge \GUARDED(P_3) \\
707 \GUARDED(\mathtt{fail}) & = & \TRUE \\
708 \GUARDED(\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2) & = & \GUARDED(P_1)
714 %% Assume that we have two corresponding patterns $P_1$ (level 1) and
715 %% $P_2$ (level 2) and that we have to check whether they are
716 %% ``correct''. First we define the notion of \emph{top-level names} of
717 %% $P_1$ and $P_2$, as follows:
719 %% \begin{array}{rcl}
720 %% \TN(C_1[P'_1,\dots,P'_2]) & = & \TN(P'_1) \cup \cdots \cup \TN(P'_2) \\
721 %% \TN(\TVAR{x}) & = & \{x\} \\
722 %% \TN(\NVAR{x}) & = & \{x\} \\
723 %% \TN(\IVAR{x}) & = & \{x\} \\
724 %% \TN(\mathtt{list0}~P'~l?) & = & \emptyset \\
725 %% \TN(\mathtt{list1}~P'~l?) & = & \emptyset \\
726 %% \TN(\mathtt{opt}~P') & = & \emptyset \\[3ex]
727 %% \TN(\BLOB(P''_1,\dots,P''_2)) & = & \TN(P''_1) \cup \cdots \cup \TN(P''_2) \\
728 %% \TN(\mathtt{term}~x) & = & \{x\} \\
729 %% \TN(\mathtt{number}~x) & = & \{x\} \\
730 %% \TN(\mathtt{ident}~x) & = & \{x\} \\
731 %% \TN(\mathtt{fresh}~x) & = & \{x\} \\
732 %% \TN(\mathtt{anonymous}) & = & \emptyset \\
733 %% \TN(\mathtt{fold}~P''_1~\mathtt{rec}~x~P''_2) & = & \TN(P''_1) \\
734 %% \TN(\mathtt{default}~P''_1~P''_2) & = & \TN(P''_1) \cap \TN(P''_2) \\
735 %% \TN(\mathtt{if}~P''_1~\mathtt{then}~P''_2~\mathtt{else}~P''_3) & = & \TN(P''_2) \\
736 %% \TN(\mathtt{fail}) & = & \emptyset
740 We say that a \emph{bidirectional transformation}
746 \item $P_1$ is a well-formed \emph{level 1 pattern} in some context $D$ and
747 $P_2$ is a well-formed \emph{level 2 pattern} in the very same context $D$,
748 that is $P_1 :: D$ and $P_2 :: D$;
749 \item the pattern $P_2$ is guarded, that is $\GUARDED(P_2)=\TRUE$;
750 \item for any direct sub-pattern $\mathtt{opt}~P'_1$ of $P_1$ such
751 that $\mathtt{opt}~P'_1 :: X$ there is a sub-pattern
752 $\mathtt{default}~P'_2~P''_2$ of $P_2$ such that
753 $\mathtt{default}~P'_2~P''_2 :: X \oplus Y$ for some context $Y$;
754 \item for any direct sub-pattern $\mathtt{list}~P'_1~l?$ of $P_1$
755 such that $\mathtt{list}~P'_1~l? :: X$ there is a sub-pattern
756 $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2$ of $P_2$ such that
757 $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2 :: X \oplus Y$ for some
761 A \emph{left-to-right transformation}
765 is well-formed if $P_2$ does not contain \texttt{if}, \texttt{fail},
766 or \texttt{anonymous} meta patterns.
768 Note that the transformations are in a sense asymmetric. Moving from
769 the concrete syntax (level 1) to the abstract syntax (level 2) we
770 forget about syntactic details. Moving from the abstract syntax to the
771 concrete syntax we may want to forget about redundant structure
774 Relationship with grammatical frameworks?
776 \subsection{Level 2 $<->$ Level 3}
778 We say that an \emph{interpretation}
784 \item $P_2$ is a well-formed \emph{applicative symbol pattern} in some context
785 $D$ and $P_3$ is a well-formed \emph{level 3 pattern} in the very same
786 context $D$, that is $P_2 :: D$ and $P_3 :: D$.