]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_notation/doc/main.tex
tex macros, checked in disambiguation section from whelp paper
[helm.git] / helm / ocaml / cic_notation / doc / main.tex
1 \documentclass[a4paper,draft]{article}
2
3 \usepackage{manfnt}
4 \usepackage{a4wide}
5 \usepackage{pifont}
6 \usepackage{semantic}
7 \usepackage{stmaryrd,latexsym}
8
9 \newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}
10
11 \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
12
13 \title{Extensible notation for \MATITA}
14 \author{Luca Padovani \qquad Stefano Zacchiroli \\
15 \small Department of Computer Science, University of Bologna \\
16 \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
17 \small \{\texttt{lpadovan}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
18
19 \newcommand{\BREAK}{\mathtt{break}}
20 \newcommand{\TVAR}[1]{#1:\mathtt{term}}
21 \newcommand{\IMPVAR}{\TVAR{\_}}
22 \newcommand{\NVAR}[1]{#1:\mathtt{number}}
23 \newcommand{\IVAR}[1]{#1:\mathtt{name}}
24 \newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
25 \newcommand{\ITO}[2]{|[#1|]_{\mathcal#2}^1}
26 \newcommand{\IOT}[2]{|[#1|]_{#2}^2}
27 \newcommand{\IAP}[2]{|[#1|]_{#2}^a}
28 \newcommand{\IAPP}[3]{|[#1|]_{#2,#3}^a}
29 \newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
30 \newcommand{\NAMES}{\mathit{names}}
31 \newcommand{\DOMAIN}{\mathit{domain}}
32 \newcommand{\UPDATE}[2]{#1[#2]}
33
34 \mathlig{~>}{\leadsto}
35 \mathlig{|->}{\mapsto}
36
37 \begin{document}
38   \maketitle
39
40 \section{Environment}
41
42 \[
43 \begin{array}{rcll}
44   V & ::= & & \mbox{(\bf values)} \\
45     &     & \verb+Term+~T & \mbox{(term)} \\
46     &  |  & \verb+String+~s & \mbox{(string)} \\
47     &  |  & \verb+Number+~n & \mbox{(number)} \\
48     &  |  & \verb+None+ & \mbox{(optional value)} \\
49     &  |  & \verb+Some+~V & \mbox{(optional value)} \\
50     &  |  & [V_1,\dots,V_n] & \mbox{(list value)} \\[2ex]
51 \end{array}
52 \]
53
54 An environment is a map $\mathcal E : \mathit{Name} -> V$.
55
56 \section{Level 1: concrete syntax}
57
58 \begin{table}
59 \caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut}
60 \hrule
61 \[
62 \begin{array}{rcll}
63   P & ::= & & \mbox{(\bf patterns)} \\
64     &     & S^{+} \\[2ex]
65   S & ::= & & \mbox{(\bf simple patterns)} \\
66     &     & l \\
67     &  |  & S~\verb+\sub+~S\\
68     &  |  & S~\verb+\sup+~S\\
69     &  |  & S~\verb+\below+~S\\
70     &  |  & S~\verb+\atop+~S\\
71     &  |  & S~\verb+\over+~S\\
72     &  |  & S~\verb+\atop+~S\\
73     &  |  & \verb+\frac+~S~S \\
74     &  |  & \verb+\sqrt+~S \\
75     &  |  & \verb+\root+~S~\verb+\of+~S \\
76     &  |  & \verb+(+~P~\verb+)+ \\
77     &  |  & \verb+hbox (+~P~\verb+)+ \\
78     &  |  & \verb+vbox (+~P~\verb+)+ \\
79     &  |  & \verb+hvbox (+~P~\verb+)+ \\
80     &  |  & \verb+hovbox (+~P~\verb+)+ \\
81     &  |  & \verb+break+ \\
82     &  |  & \verb+list0+~S~[\verb+sep+~l] \\
83     &  |  & \verb+list1+~S~[\verb+sep+~l] \\
84     &  |  & \verb+opt+~S \\
85     &  |  & [\verb+term+]~x \\
86     &  |  & \verb+number+~x \\
87     &  |  & \verb+ident+~x \\
88 \end{array}
89 \]
90 \hrule
91 \end{table}
92
93 Rationale: while the layout schemata can occur in the concrete syntax
94 used by user, the box schemata and the magic patterns can only occur
95 when defining the notation. This is why the layout schemata are
96 ``escaped'' with a backslash, so that they cannot be confused with
97 plain identifiers, wherease the others are not. Alternatively, they
98 could be defined as keywords, but this would prevent their names to be
99 used in different contexts.
100
101 \begin{table}
102 \caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut}
103 \hrule
104 \[
105 \begin{array}{@{}ll@{}}
106 \begin{array}[t]{rcll}
107   T & ::= & & \mbox{(\bf terms)} \\
108     &     & L_\kappa[T_1,\dots,T_n] & \mbox{(layout)} \\
109     &  |  & B_\kappa^{ab}[T_1\cdots T_n] & \mbox{(box)} \\
110     &  |  & \BREAK & \mbox{(breakpoint)} \\
111     &  |  & \FENCED{T_1\cdots T_n} & \mbox{(fenced)} \\
112     &  |  & l & \mbox{(literal)} \\[2ex]
113   P & ::= & & \mbox{(\bf patterns)} \\
114     &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
115     &  |  & B_\kappa^{ab}[P_1\cdots P_n] & \mbox{(box)} \\
116     &  |  & \BREAK & \mbox{(breakpoint)} \\
117     &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
118     &  |  & M & \mbox{(magic)} \\
119     &  |  & V & \mbox{(variable)} \\
120     &  |  & l & \mbox{(literal)} \\
121 \end{array} &
122 \begin{array}[t]{rcll}
123   V & ::= & & \mbox{(\bf variables)} \\
124     &     & \TVAR{x} & \mbox{(term variable)} \\
125     &  |  & \NVAR{x} & \mbox{(number variable)} \\
126     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
127   M & ::= & & \mbox{(\bf magic patterns)} \\
128     &     & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
129     &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
130     &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
131 \end{array}
132 \end{array}
133 \]
134 \hrule
135 \end{table}
136
137 \[
138 \ITO{\cdot}{{}} : P -> \mathit{Env} -> T
139 \]
140
141 \begin{table}
142 \caption{\label{tab:il1f2} Instantiation of level 1 patterns from level 2.\strut}
143 \hrule
144 \[
145 \begin{array}{rcll}
146   \ITO{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\ITO{(P_1)}{E},\dots,\ITO{(P_n)}{E} ] \\
147   \ITO{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
148   \ITO{\BREAK}{E} & = & \BREAK \\
149   \ITO{(P)}{E} & = & \ITO{P}{E} \\
150   \ITO{(P_1\cdots P_n)}{E} & = & B_H^{00}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
151   \ITO{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
152   \ITO{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
153   \ITO{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
154   \ITO{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\
155   \ITO{\mathtt{opt}~P}{E} & = & \ITO{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
156   & & & \mathcal{E}'(x)=\left\{
157   \begin{array}{@{}ll}
158     v, & \mathcal{E}(x) = \mathtt{Some}~v \\
159     \mathcal{E}(x), & \mbox{otherwise}
160   \end{array}
161   \right. \\
162   \ITO{\mathtt{list}k~P~l?}{E} & = & \ITO{P}{{E}_1}~{l?}\cdots {l?}~\ITO{P}{{E}_n} &
163     \mathcal{E}(\NAMES(P)) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\
164     & & & n\ge k \\
165   & & & \mathcal{E}_i(x) = \left\{
166   \begin{array}{@{}ll}
167     v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\
168     \mathcal{E}(x), & \mbox{otherwise}
169   \end{array}
170   \right. \\
171   \ITO{l}{E} & = & l \\
172
173 %%     &  |  & (P) & \mbox{(fenced)} \\
174 %%     &  |  & M & \mbox{(magic)} \\
175 %%     &  |  & V & \mbox{(variable)} \\
176 %%     &  |  & l & \mbox{(literal)} \\[2ex]
177 %%   V & ::= & & \mbox{(\bf variables)} \\
178 %%     &     & \TVAR{x} & \mbox{(term variable)} \\
179 %%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
180 %%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
181 %%   M & ::= & & \mbox{(\bf magic patterns)} \\
182 %%     &     & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
183 %%     &  |  & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
184 %%     &  |  & \verb+opt+~S & \mbox{(option)} \\[2ex]  
185 \end{array}
186 \]
187 \hrule
188 \end{table}
189
190 \begin{table}
191 \caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut}
192 \hrule
193 \[
194 \renewcommand{\arraystretch}{3.5}
195 \begin{array}[t]{@{}c@{}}
196   \inference[\sc layout]
197     {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
198     {L_\kappa[P_1,\dots,P_n] :: D_1\oplus\cdots\oplus D_n}
199   \\
200   \inference[\sc box]
201     {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
202     {B_\kappa^{ab}[P_1\cdots P_n] :: D_1\oplus\cdots\oplus D_n}
203   \\
204   \inference[\sc fenced]
205     {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
206     {\FENCED{P_1\cdots P_n} :: D_1\oplus\cdots\oplus D_n}
207   \\
208   \inference[\sc breakpoint]
209     {}
210     {\BREAK :: \emptyset}
211   \qquad
212   \inference[\sc literal]
213     {}
214     {l :: \emptyset}
215   \qquad
216   \inference[\sc tvar]
217     {}
218     {\TVAR{x} :: \TVAR{x}}
219   \\
220   \inference[\sc nvar]
221     {}
222     {\NVAR{x} :: \NVAR{x}}
223   \qquad
224   \inference[\sc ivar]
225     {}
226     {\IVAR{x} :: \IVAR{x}}
227   \\
228   \inference[\sc list0]
229     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
230     {\mathtt{list0}~P~l? :: D'}
231   \\
232   \inference[\sc list1]
233     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
234     {\mathtt{list1}~P~l? :: D'}
235   \\
236   \inference[\sc opt]
237     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}}
238     {\mathtt{opt}~P :: D'}
239 \end{array}
240 \]
241 \hrule
242 \end{table}
243
244 \newcommand{\ATTRS}[1]{\langle#1\rangle}
245 \newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}}
246
247 \begin{table}
248 \caption{\label{tab:addparens} Can't read the AST and need parentheses? Here you go!.\strut}
249 \hrule
250 \[
251 \begin{array}{rcll}
252   \ADDPARENS{l}{n} & = & l \\
253   \ADDPARENS{\BREAK}{n} & = & \BREAK \\
254   \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \ADDPARENS{T}{m} & n < m \\
255   \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} & n > m \\
256   \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=L,\mathit{pos}=R}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
257   \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=R,\mathit{pos}=L}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
258   \ADDPARENS{\ATTRS{\cdots}T}{n} & = & \ADDPARENS{T}{n} \\
259   \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}] \\
260   \ADDPARENS{B_\kappa^{ab}[T_1,\dots,T_m]}{n} & = & B_\kappa^{ab}[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_m}{n}]
261 \end{array}
262 \]
263 \hrule
264 \end{table}
265
266 \begin{table}
267 \caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut}
268 \hrule
269 \[
270 \begin{array}{rcll}
271   \ANNPOS{l}{p,q} & = & l \\
272   \ANNPOS{\BREAK}{p,q} & = & \BREAK \\
273   \ANNPOS{x}{1,0} & = & \ATTRS{\mathit{pos}=L}{x} \\
274   \ANNPOS{x}{0,1} & = & \ATTRS{\mathit{pos}=R}{x} \\
275   \ANNPOS{x}{p,q} & = & \ATTRS{\mathit{pos}=I}{x} \\
276   \ANNPOS{B_\kappa^{ab}[P]}{p,q} & = & B_\kappa^{ab}[\ANNPOS{P}{p,q}] \\
277   \ANNPOS{B_\kappa^{ab}[\{\BREAK\} P_1\cdots P_n\{\BREAK\}]}{p,q} & = & B_\kappa^{ab}[\begin{array}[t]{@{}l}
278       \{\BREAK\} \ANNPOS{P_1}{p,0} \\
279       \ANNPOS{P_2}{0,0}\cdots\ANNPOS{P_{n-1}}{0,0} \\
280       \ANNPOS{P_n}{0,q}\{\BREAK\}]
281   \end{array}
282
283 %%     &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
284 %%     &  |  & \BREAK & \mbox{(breakpoint)} \\
285 %%     &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
286 %%   V & ::= & & \mbox{(\bf variables)} \\
287 %%     &     & \TVAR{x} & \mbox{(term variable)} \\
288 %%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
289 %%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
290 %%   M & ::= & & \mbox{(\bf magic patterns)} \\
291 %%     &     & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
292 %%     &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
293 %%     &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
294 \end{array}
295 \]
296 \hrule
297 \end{table}
298
299 \section{Level 2: abstract syntax}
300
301 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
302
303 \begin{table}
304 \caption{\label{tab:synl2} Concrete syntax of level 2 patterns.\strut}
305 \hrule
306 \[
307 \begin{array}{@{}rcll@{}}
308   \NT{term} & ::= & & \mbox{\bf terms} \\
309     &     & x & \mbox{(identifier)} \\
310     &  |  & n & \mbox{(number)} \\
311     &  |  & s & \mbox{(symbol)} \\
312     &  |  & \mathrm{URI} & \mbox{(URI)} \\
313     &  |  & \verb+?+ & \mbox{(implicit)} \\
314     &  |  & \verb+%+ & \mbox{(placeholder)} \\
315     &  |  & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
316     &  |  & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
317     &  |  & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
318     &  |  & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
319     &  |  & \NT{term}~\NT{term} & \mbox{(application)} \\
320     &  |  & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
321     &  |  & [\verb+[+~\NT{term}~\verb+]+]~\verb+match+~\NT{term}~\verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \mbox{(pattern match)} \\
322     &  |  & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
323     &  |  & \verb+(+~\NT{term}~\verb+)+ \\
324     &  |  & \BLOB(\NT{meta},\dots,\NT{meta}) & \mbox{(meta blob)} \\
325   \NT{defs}  & ::= & & \mbox{\bf mutual definitions} \\
326     &     & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
327   \NT{fun} & ::= & & \mbox{\bf functions} \\
328     &     & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
329   \NT{binder} & ::= & & \mbox{\bf binders} \\
330     &     & \verb+\Pi+ \mid \verb+\exists+ \mid \verb+\forall+ \mid \verb+\lambda+ \\
331   \NT{arg} & ::= & & \mbox{\bf single argument} \\
332     &     & \verb+_+ \mid x \mid \BLOB(\NT{meta},\dots,\NT{meta}) \\
333   \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
334     &     & \NT{arg} \\
335     &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
336   \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
337     &     & \NT{arg} \\
338     &  |  & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
339   \NT{kind} & ::= & & \mbox{\bf induction kind} \\
340     &     & \verb+rec+ \mid \verb+corec+ \\
341   \NT{rule} & ::= & & \mbox{\bf rules} \\
342     &     & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]
343
344   \NT{meta} & ::= & & \mbox{\bf meta} \\
345     &     & \BLOB(\NT{term},\dots,\NT{term}) & \mbox{(term blob)} \\
346     &  |  & [\verb+term+]~x \\
347     &  |  & \verb+number+~x \\
348     &  |  & \verb+ident+~x \\
349     &  |  & \verb+fresh+~x \\
350     &  |  & \verb+anonymous+ \\
351     &  |  & \verb+fold+~[\verb+left+\mid\verb+right+]~\NT{meta}~\verb+rec+~x~\NT{meta} \\
352     &  |  & \verb+default+~\NT{meta}~\NT{meta} \\
353     &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
354     &  |  & \verb+fail+ 
355 \end{array}
356 \]
357 \hrule
358 \end{table}
359
360 \begin{table}
361 \caption{\label{tab:wfl2} Well-formedness rules for level 2 patterns.\strut}
362 \hrule
363 \[
364 \renewcommand{\arraystretch}{3.5}
365 \begin{array}{@{}c@{}}
366   \inference[\sc Constr]
367     {P_i :: D_i}
368     {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\
369   \inference[\sc TermVar]
370     {}
371     {\mathtt{term}~x :: x : \mathtt{Term}}
372   \quad
373   \inference[\sc NumVar]
374     {}
375     {\mathtt{number}~x :: x : \mathtt{Number}}
376   \\
377   \inference[\sc IdentVar]
378     {}
379     {\mathtt{ident}~x :: x : \mathtt{String}}
380   \quad
381   \inference[\sc FreshVar]
382     {}
383     {\mathtt{fresh}~x :: x : \mathtt{String}}
384   \\
385   \inference[\sc Success]
386     {}
387     {\mathtt{anonymous} :: \emptyset}
388   \\
389   \inference[\sc Fold]
390     {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}
391     {\mathtt{fold}~P_1~\mathtt{rec}~x~P_2 :: D_1 \oplus D_2~\mathtt{List}}
392   \\
393   \inference[\sc Default]
394     {P_1 :: D \oplus D_1 & P_2 :: D & \DOMAIN(D_1) \ne \emptyset & \DOMAIN(D) \cap \DOMAIN(D_1) = \emptyset}
395     {\mathtt{default}~P_1~P_2 :: D \oplus D_1~\mathtt{Option}}
396   \\
397   \inference[\sc If]
398     {P_1 :: \emptyset & P_2 :: D & P_3 :: D }
399     {\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 :: D}
400   \qquad
401   \inference[\sc Fail]
402     {}
403     {\mathtt{fail} :: \emptyset}
404 %%     &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
405 %%     &  |  & \verb+fail+ 
406 \end{array}
407 \]
408 \hrule
409 \end{table}
410
411 \begin{table}
412  \caption{\label{tab:il2f1} Instantiation of level 2 patterns from level 1.
413  \strut}
414 \hrule
415 \[
416 \begin{array}{rcll}
417
418 \IOT{C[t_1,\dots,t_n]}{\mathcal{E}} & =
419 & C[\IOT{t_1}{\mathcal{E}},\dots,\IOT{t_n}{\mathcal{E}}] \\
420
421 \IOT{\mathtt{term}~x}{\mathcal{E}} & = & t & \mathcal{E}(x) = \mathtt{Term}~t \\
422
423 \IOT{\mathtt{number}~x}{\mathcal{E}} & =
424 & n & \mathcal{E}(x) = \mathtt{Number}~n \\
425
426 \IOT{\mathtt{ident}~x}{\mathcal{E}} & =
427 & y & \mathcal{E}(x) = \mathtt{String}~y \\
428
429 \IOT{\mathtt{fresh}~x}{\mathcal{E}} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\
430
431 \IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & =
432 & \IOT{P_1}{\UPDATE{\mathcal{E}}{x_i|->v_i}}
433 & \mathcal{E}(x_i)=\mathtt{Some}~v_i \\
434 & & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\
435
436 \IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & =
437 & \IOT{P_2}{\UPDATE{\mathcal{E}}{x_i|->\bot}}
438 & \mathcal{E}(x_i)=\mathtt{None} \\
439 & & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\
440
441 \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
442 & =
443 & \IOT{P_1}{\mathcal{E}'}
444 & \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[],\dots,[]\} \\
445 & & \multicolumn{2}{l}{\mathcal{E}'=\UPDATE{\mathcal{E}}{\NAMES(P_2)\setminus\{x\}|->\bot}}
446 \\
447
448 \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
449 & =
450 & \IOT{P_2}{\mathcal{E}'}
451 & \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\
452 & & & \NAMES(P_2)\setminus\{x\}=\{y_1,\dots,y_m\} \\
453 & & \multicolumn{2}{l}{\mathcal{E}'(y) =
454  \left\{
455  \begin{array}{@{}ll}
456  \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_e}{\mathcal{E}''}
457                 & y=x \\
458  v_{i1}         & y=y_i \\
459  \mathcal{E}(y) & \mbox{otherwise} \\
460  \end{array}
461  \right.} \\
462 & & \multicolumn{2}{l}{\mathcal{E}''(y) =
463  \left\{
464  \begin{array}{@{}ll}
465  [v_{i2};\dots;v_{in}] & y=y_i \\
466  \mathcal{E}(y)        & \mbox{otherwise} \\
467  \end{array}
468  \right.} \\
469
470 \IOT{\mathtt{fold}~\mathtt{left}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
471 & =
472 & \mathit{eval\_fold}(x,P_2,\mathcal{E}')
473 & \\
474 & & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->
475 \IOT{P_1}{\UPDATE{\mathcal{E}}{\NAMES(P_2)|->\bot}}}} \\
476
477 \mathit{eval\_fold}(x,P,\mathcal{E})
478 & =
479 & \mathcal{E}(x)
480 & \mathcal{E}(\NAMES(P)\setminus\{x\})=\{[],\dots,[]\} \\
481
482 \mathit{eval\_fold}(x,P,\mathcal{E})
483 & =
484 & \mathit{eval\_fold}(x,P,\mathcal{E}')
485 & \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\
486 & & & \NAMES(P)\setminus{x}=\{y_1,\dots,y_m\} \\
487 &
488 & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->\IOT{P}{\mathcal{E}''}; ~ y_i |-> [v_{i2};\dots;v_{in_i}]}}
489 \\
490 &
491 & \multicolumn{2}{l}{\mathcal{E}''(y) =
492 \left\{
493 \begin{array}{ll}
494  v_1            & y\in \NAMES(P)\setminus\{x\} \\
495  \mathcal{E}(x) & y=x \\
496  \bot           & \mathit{otherwise} \\
497 \end{array}
498 \right.
499 }
500 \\
501
502 \end{array} \\
503 \]
504 \end{table}
505
506 \begin{table}
507 \caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
508 \hrule
509 \[
510 \renewcommand{\arraystretch}{3.5}
511 \begin{array}{@{}c@{}}
512   \inference[\sc Constr]
513     {t_i \in P_i ~> \mathcal E_i & i\ne j => \DOMAIN(\mathcal E_i)\cap\DOMAIN(\mathcal E_j)=\emptyset}
514     {C[t_1,\dots,t_n] \in C[P_1,\dots,P_n] ~> \mathcal E_1 \oplus \cdots \oplus \mathcal E_n}
515   \\
516   \inference[\sc TermVar]
517     {}
518     {t \in [\mathtt{term}]~x ~> [x |-> \mathtt{Term}~t]}
519   \quad
520   \inference[\sc NumVar]
521     {}
522     {n \in \mathtt{number}~x ~> [x |-> \mathtt{Number}~n]}
523   \\
524   \inference[\sc IdentVar]
525     {}
526     {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
527   \quad
528   \inference[\sc FreshVar]
529     {}
530     {x \in \mathtt{fresh}~x ~> [x |-> \mathtt{String}~x]}
531   \\
532   \inference[\sc Success]
533     {}
534     {t \in \mathtt{anonymous} ~> \emptyset}
535   \\
536   \inference[\sc DefaultT]
537     {t \in P_1 ~> \mathcal E}
538     {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
539     \quad
540     \mathcal E'(x) = \left\{
541     \renewcommand{\arraystretch}{1}
542     \begin{array}{ll}
543       \mathtt{Some}~\mathcal{E}(x) & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
544       \mathcal{E}(x) & \mbox{otherwise}
545     \end{array}
546     \right.
547   \\
548   \inference[\sc DefaultF]
549     {t \not\in P_1 & t \in P_2 ~> \mathcal E}
550     {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
551     \quad
552     \mathcal E'(x) = \left\{
553     \renewcommand{\arraystretch}{1}
554     \begin{array}{ll}
555       \mathtt{None} & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
556       \mathcal{E}(x) & \mbox{otherwise}
557     \end{array}
558     \right.
559   \\
560   \inference[\sc IfT]
561     {t \in P_1 ~> \mathcal E' & t \in P_2 ~> \mathcal E}
562     {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
563   \quad
564   \inference[\sc IfF]
565     {t \not\in P_1 & t \in P_3 ~> \mathcal E}
566     {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
567   \\
568   \inference[\sc FoldRec]
569     {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
570     {t \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
571   \\
572   \mbox{where}~\mathcal{E}''(y) = \left\{
573     \renewcommand{\arraystretch}{1}
574     \begin{array}{ll}
575       \mathcal{E}(y)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{right} \\
576       \mathcal{E}'(y)@[\mathcal{E}(y)] & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{left} \\
577       \mathcal{E}'(y) & \mbox{otherwise}
578     \end{array}  
579   \right.
580   \\
581   \inference[\sc FoldBase]
582     {t \not\in P_2 & t \in P_1 ~> \mathcal E}
583     {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
584   \quad
585   \mathcal E'(y) = \left\{
586     \renewcommand{\arraystretch}{1}
587     \begin{array}{ll}
588       [] & y \in \NAMES(P_2) \setminus \{x\} \\
589       \mathcal{E}(y) & \mbox{otherwise}
590     \end{array}  
591   \right.
592 \end{array}
593 \]
594 \hrule
595 \end{table}
596
597 \begin{table}
598  \caption{\label{tab:synl3} Abstract syntax of level 3 terms and patterns.}
599  \hrule
600  \[
601  \begin{array}{@{}ll@{}}
602   \begin{array}[t]{rcll}
603    T & : := &   & \mbox{(\bf terms)} \\
604      &      & u & \mbox{(uri)} \\
605      &  |   & \lambda x.T & \mbox{($\lambda$-abstraction)} \\
606      &  |   & (T_1 \dots T_n) & \mbox{(application)} \\
607      &  |   & \dots \\[2ex]
608   \end{array} &
609   \begin{array}[t]{rcll}
610    P & : := &   & \mbox{(\bf patterns)} \\
611      &      & u & \mbox{(uri)} \\
612      &  |   & V & \mbox{(variable)} \\
613      &  |   & (P_1 \dots P_n) & \mbox{(application)} \\[2ex]
614    V & : := &   & \mbox{(\bf variables)} \\
615      &      & \TVAR{x} & \mbox{(term variable)} \\
616      &  |   & \IMPVAR & \mbox{(implicit variable)} \\
617   \end{array} \\
618  \end{array}
619  \]
620  \hrule
621 \end{table}
622
623 \begin{table}
624 \caption{\label{tab:wfl3} Well-formedness rules for level 3 patterns.\strut}
625 \hrule
626 \[
627 \renewcommand{\arraystretch}{3.5}
628 \begin{array}{@{}c@{}}
629  \inference[\sc Uri] {} {u :: \emptyset} \quad
630  \inference[\sc ImpVar] {} {\TVAR{x} :: \emptyset} \quad
631  \inference[\sc TermVar] {} {\TVAR{x} :: x:\mathtt{Term}} \\
632  \inference[\sc Appl]
633   {P_i :: D_i
634    \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset}
635   {P_1\cdots P_n :: D_1\oplus\cdots\oplus D_n} \\
636 \end{array}
637 \]
638 \hrule
639 \end{table}
640
641 \begin{table}
642  \caption{\label{tab:synargp} Abstract syntax of applicative symbol patterns.}
643  \hrule
644  \[
645  \begin{array}{rcll}
646   P & : := &           & \mbox{(\bf patterns)} \\
647     &      & s ~ \{ \mathit{arg} \} & \mbox{(symbol pattern)} \\[2ex]
648   \mathit{arg} & : := & & \mbox{(\bf argument)} \\
649     &      & \TVAR{x} & \mbox{(term variable)} \\
650     &  |   & \eta.\mathit{arg} & \mbox{($\eta$-abstraction)} \\
651  \end{array}
652  \]
653  \hrule
654 \end{table}
655
656 \begin{table}
657 \caption{\label{tab:wfargp} Well-formedness rules for applicative symbol
658 patterns.\strut}
659 \hrule
660 \[
661 \renewcommand{\arraystretch}{3.5}
662 \begin{array}{@{}c@{}}
663  \inference[\sc Pattern]
664   {\mathit{arg}_i :: D_i
665    \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset}
666   {s~\mathit{arg}_1\cdots\mathit{arg}_n :: D_1\oplus\cdots\oplus D_n} \\
667  \inference[\sc TermVar]
668   {}
669   {\TVAR{x} :: x : \mathtt{Term}}
670  \quad
671  \inference[\sc EtaAbs]
672   {\mathit{arg} :: D}
673   {\eta.\mathit{arg} :: D}
674  \\
675 \end{array}
676 \]
677 \hrule
678 \end{table}
679
680 \begin{table}
681 \caption{\label{tab:l3match} Pattern matching of level 3 terms.\strut}
682 \hrule
683 \[
684 \renewcommand{\arraystretch}{3.5}
685 \begin{array}{@{}c@{}}
686  \inference[\sc Uri] {} {u\in u ~> []} \quad
687  \inference[\sc Appl] {t_i\in P_i ~> \mathcal{E}_i}
688   {(t_1\dots t_n)\in(P_1\dots P_n) ~>
689    \mathcal{E}_1\oplus\cdots\oplus\mathcal{E}_n} \\
690  \inference[\sc TermVar] {} {t\in \TVAR{x} ~> [x |-> \mathtt{Term}~t]} \quad
691  \inference[\sc ImpVar] {} {t\in \IMPVAR ~> []} \\
692 \end{array}
693 \]
694 \hrule
695 \end{table}
696
697 \begin{table}
698 \caption{\label{tab:iapf3} Instantiation of applicative symbol patterns (from
699 level 3).\strut}
700 \hrule
701 \[
702 \begin{array}{rcll}
703  \IAP{s~a_1\cdots a_n}{\mathcal{E}} & = &
704   (s~\IAPP{a_1}{\mathcal{E}}{0}\cdots\IAPP{a_n}{\mathcal{E}}{0}) & \\
705  \IAPP{\TVAR{x}}{\mathcal{E}}{0} & = & t & \mathcal{E}(x)=\mathtt{Term}~t \\
706  \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & = & \lambda y.\IAPP{t}{\mathcal{E}}{i}
707   & \mathcal{E}(x)=\mathtt{Term}~\lambda y.t \\
708  \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & =
709   & \lambda y_1.\cdots.\lambda y_{i+1}.t~y_1\cdots y_{i+1}
710   & \mathcal{E}(x)=\mathtt{Term}~t\wedge\forall y,t\neq\lambda y.t \\
711  \IAPP{\eta.a}{\mathcal{E}}{i} & = & \IAPP{a}{\mathcal{E}}{i+1} \\
712 \end{array}
713 \]
714 \hrule
715 \end{table}
716
717 \section{Type checking}
718
719 \subsection{Level 1 $<->$ Level 2}
720
721 \newcommand{\GUARDED}{\mathit{guarded}}
722 \newcommand{\TRUE}{\mathit{true}}
723 \newcommand{\FALSE}{\mathit{false}}
724
725 \newcommand{\TN}{\mathit{tn}}
726
727 \begin{table}
728 \caption{\label{tab:guarded} Guarded condition of level 2
729 pattern. Note that the recursive case of the \texttt{fold} magic is
730 not explicitly required to be guarded. The point is that it must
731 contain at least two distinct names, and this guarantees that whatever
732 is matched by the recursive pattern, the terms matched by those two
733 names will be smaller than the whole matched term.\strut} \hrule
734 \[
735 \begin{array}{rcll}
736   \GUARDED(C(M(P))) & = & \GUARDED(P) \\
737   \GUARDED(C(t_1,\dots,t_n)) & = & \TRUE \\
738   \GUARDED(\mathtt{term}~x) & = & \FALSE \\
739   \GUARDED(\mathtt{number}~x) & = & \FALSE \\
740   \GUARDED(\mathtt{ident}~x) & = & \FALSE \\
741   \GUARDED(\mathtt{fresh}~x) & = & \FALSE \\
742   \GUARDED(\mathtt{anonymous}) & = & \TRUE \\
743   \GUARDED(\mathtt{default}~P_1~P_2) & = & \GUARDED(P_1) \wedge \GUARDED(P_2) \\
744   \GUARDED(\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3) & = & \GUARDED(P_2) \wedge \GUARDED(P_3) \\
745   \GUARDED(\mathtt{fail}) & = & \TRUE \\
746   \GUARDED(\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2) & = & \GUARDED(P_2)
747 \end{array}
748 \]
749 \hrule
750 \end{table}
751
752 %% Assume that we have two corresponding patterns $P_1$ (level 1) and
753 %% $P_2$ (level 2) and that we have to check whether they are
754 %% ``correct''. First we define the notion of \emph{top-level names} of
755 %% $P_1$ and $P_2$, as follows:
756 %% \[
757 %% \begin{array}{rcl}
758 %%   \TN(C_1[P'_1,\dots,P'_2]) & = & \TN(P'_1) \cup \cdots \cup \TN(P'_2) \\
759 %%   \TN(\TVAR{x}) & = & \{x\} \\
760 %%   \TN(\NVAR{x}) & = & \{x\} \\
761 %%   \TN(\IVAR{x}) & = & \{x\} \\
762 %%   \TN(\mathtt{list0}~P'~l?) & = & \emptyset \\
763 %%   \TN(\mathtt{list1}~P'~l?) & = & \emptyset \\
764 %%   \TN(\mathtt{opt}~P') & = & \emptyset \\[3ex]
765 %%   \TN(\BLOB(P''_1,\dots,P''_2)) & = & \TN(P''_1) \cup \cdots \cup \TN(P''_2) \\
766 %%   \TN(\mathtt{term}~x) & = & \{x\} \\
767 %%   \TN(\mathtt{number}~x) & = & \{x\} \\
768 %%   \TN(\mathtt{ident}~x) & = & \{x\} \\
769 %%   \TN(\mathtt{fresh}~x) & = & \{x\} \\
770 %%   \TN(\mathtt{anonymous}) & = & \emptyset \\
771 %%   \TN(\mathtt{fold}~P''_1~\mathtt{rec}~x~P''_2) & = & \TN(P''_1) \\
772 %%   \TN(\mathtt{default}~P''_1~P''_2) & = & \TN(P''_1) \cap \TN(P''_2) \\
773 %%   \TN(\mathtt{if}~P''_1~\mathtt{then}~P''_2~\mathtt{else}~P''_3) & = & \TN(P''_2) \\
774 %%   \TN(\mathtt{fail}) & = & \emptyset
775 %% \end{array}
776 %% \]
777
778 We say that a \emph{bidirectional transformation}
779 \[
780   P_1 <=> P_2
781 \]
782 is well-formed if:
783 \begin{itemize}
784   \item $P_1$ is a well-formed \emph{level 1 pattern} in some context $D$ and
785   $P_2$ is a well-formed \emph{level 2 pattern} in the very same context $D$,
786   that is $P_1 :: D$ and $P_2 :: D$;
787   \item the pattern $P_2$ is guarded, that is $\GUARDED(P_2)=\TRUE$;
788   \item for any direct sub-pattern $\mathtt{opt}~P'_1$ of $P_1$ such
789     that $\mathtt{opt}~P'_1 :: X$ there is a sub-pattern
790     $\mathtt{default}~P'_2~P''_2$ of $P_2$ such that
791     $\mathtt{default}~P'_2~P''_2 :: X \oplus Y$ for some context $Y$;
792   \item for any direct sub-pattern $\mathtt{list}~P'_1~l?$ of $P_1$
793     such that $\mathtt{list}~P'_1~l? :: X$ there is a sub-pattern
794     $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2$ of $P_2$ such that
795     $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2 :: X \oplus Y$ for some
796     context $Y$.
797 \end{itemize}
798
799 A \emph{left-to-right transformation}
800 \[
801   P_1 => P_2
802 \]
803 is well-formed if $P_2$ does not contain \texttt{if}, \texttt{fail},
804 or \texttt{anonymous} meta patterns.
805
806 Note that the transformations are in a sense asymmetric. Moving from
807 the concrete syntax (level 1) to the abstract syntax (level 2) we
808 forget about syntactic details. Moving from the abstract syntax to the
809 concrete syntax we may want to forget about redundant structure
810 (types).
811
812 Relationship with grammatical frameworks?
813
814 \subsection{Level 2 $<->$ Level 3}
815
816 We say that an \emph{interpretation}
817 \[
818  P_2 <=> P_3
819 \]
820 is well-formed if:
821 \begin{itemize}
822  \item $P_2$ is a well-formed \emph{applicative symbol pattern} in some context
823   $D$ and $P_3$ is a well-formed \emph{level 3 pattern} in the very same
824   context $D$, that is $P_2 :: D$ and $P_3 :: D$.
825 \end{itemize}
826
827 \end{document}
828