helm/ocaml/cic_notation/doc/body.tex

   1
   2 \section{Environment}
   3
   4 \[
   5 \begin{array}{rcll}
   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]
  13 \end{array}
  14 \]
  15
  16 An environment is a map $\mathcal E : \mathit{Name} -> V$.
  17
  18 \section{Level 1: concrete syntax}
  19
  20 \begin{table}
  21 \caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut}
  22 \hrule
  23 \[
  24 \begin{array}{rcll}
  25   P & ::= & & \mbox{(\bf patterns)} \\
  26     &     & S^{+} \\[2ex]
  27   S & ::= & & \mbox{(\bf simple patterns)} \\
  28     &     & l \\
  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+)+ \\
  43     &  |  & \verb+break+ \\
  44     &  |  & \verb+list0+~S~[\verb+sep+~l] \\
  45     &  |  & \verb+list1+~S~[\verb+sep+~l] \\
  46     &  |  & \verb+opt+~S \\
  47     &  |  & [\verb+term+]~x \\
  48     &  |  & \verb+number+~x \\
  49     &  |  & \verb+ident+~x \\
  50 \end{array}
  51 \]
  52 \hrule
  53 \end{table}
  54
  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.
  62
  63 \begin{table}
  64 \caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut}
  65 \hrule
  66 \[
  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)} \\
  83 \end{array} &
  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]
  93 \end{array}
  94 \end{array}
  95 \]
  96 \hrule
  97 \end{table}
  98
  99 \[
 100 \ITO{\cdot}{{}} : P -> \mathit{Env} -> T
 101 \]
 102
 103 \begin{table}
 104 \caption{\label{tab:il1f2} Instantiation of level 1 patterns from level 2.\strut}
 105 \hrule
 106 \[
 107 \begin{array}{rcll}
 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\{
 119   \begin{array}{@{}ll}
 120     v, & \mathcal{E}(x) = \mathtt{Some}~v \\
 121     \mathcal{E}(x), & \mbox{otherwise}
 122   \end{array}
 123   \right. \\
 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}]\} \\
 126     & & & n\ge k \\
 127   & & & \mathcal{E}_i(x) = \left\{
 128   \begin{array}{@{}ll}
 129     v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\
 130     \mathcal{E}(x), & \mbox{otherwise}
 131   \end{array}
 132   \right. \\
 133   \ITO{l}{E} & = & l \\
 134
 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]
 147 \end{array}
 148 \]
 149 \hrule
 150 \end{table}
 151
 152 \begin{table}
 153 \caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut}
 154 \hrule
 155 \[
 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}
 161   \\
 162   \inference[\sc box]
 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}
 165   \\
 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}
 169   \\
 170   \inference[\sc breakpoint]
 171     {}
 172     {\BREAK :: \emptyset}
 173   \qquad
 174   \inference[\sc literal]
 175     {}
 176     {l :: \emptyset}
 177   \qquad
 178   \inference[\sc tvar]
 179     {}
 180     {\TVAR{x} :: \TVAR{x}}
 181   \\
 182   \inference[\sc nvar]
 183     {}
 184     {\NVAR{x} :: \NVAR{x}}
 185   \qquad
 186   \inference[\sc ivar]
 187     {}
 188     {\IVAR{x} :: \IVAR{x}}
 189   \\
 190   \inference[\sc list0]
 191     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
 192     {\mathtt{list0}~P~l? :: D'}
 193   \\
 194   \inference[\sc list1]
 195     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
 196     {\mathtt{list1}~P~l? :: D'}
 197   \\
 198   \inference[\sc opt]
 199     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}}
 200     {\mathtt{opt}~P :: D'}
 201 \end{array}
 202 \]
 203 \hrule
 204 \end{table}
 205
 206 \newcommand{\ATTRS}[1]{\langle#1\rangle}
 207 \newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}}
 208
 209 \begin{table}
 210 \caption{\label{tab:addparens} Can't read the AST and need parentheses? Here you go!.\strut}
 211 \hrule
 212 \[
 213 \begin{array}{rcll}
 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}]
 223 \end{array}
 224 \]
 225 \hrule
 226 \end{table}
 227
 228 \begin{table}
 229 \caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut}
 230 \hrule
 231 \[
 232 \begin{array}{rcll}
 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\}]
 243   \end{array}
 244
 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]
 256 \end{array}
 257 \]
 258 \hrule
 259 \end{table}
 260
 261 \section{Level 2: abstract syntax}
 262
 263 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
 264
 265 \begin{table}
 266 \caption{\label{tab:synl2} Concrete syntax of level 2 patterns.\strut}
 267 \hrule
 268 \[
 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} \\
 296     &     & \NT{arg} \\
 297     &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
 298   \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
 299     &     & \NT{arg} \\
 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]
 305
 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} \\
 316     &  |  & \verb+fail+
 317 \end{array}
 318 \]
 319 \hrule
 320 \end{table}
 321
 322 \begin{table}
 323 \caption{\label{tab:wfl2} Well-formedness rules for level 2 patterns.\strut}
 324 \hrule
 325 \[
 326 \renewcommand{\arraystretch}{3.5}
 327 \begin{array}{@{}c@{}}
 328   \inference[\sc Constr]
 329     {P_i :: D_i}
 330     {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\
 331   \inference[\sc TermVar]
 332     {}
 333     {\mathtt{term}~x :: x : \mathtt{Term}}
 334   \quad
 335   \inference[\sc NumVar]
 336     {}
 337     {\mathtt{number}~x :: x : \mathtt{Number}}
 338   \\
 339   \inference[\sc IdentVar]
 340     {}
 341     {\mathtt{ident}~x :: x : \mathtt{String}}
 342   \quad
 343   \inference[\sc FreshVar]
 344     {}
 345     {\mathtt{fresh}~x :: x : \mathtt{String}}
 346   \\
 347   \inference[\sc Success]
 348     {}
 349     {\mathtt{anonymous} :: \emptyset}
 350   \\
 351   \inference[\sc Fold]
 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}}
 354   \\
 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}}
 358   \\
 359   \inference[\sc If]
 360     {P_1 :: \emptyset & P_2 :: D & P_3 :: D }
 361     {\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 :: D}
 362   \qquad
 363   \inference[\sc Fail]
 364     {}
 365     {\mathtt{fail} :: \emptyset}
 366 %%     &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
 367 %%     &  |  & \verb+fail+
 368 \end{array}
 369 \]
 370 \hrule
 371 \end{table}
 372
 373 \begin{table}
 374  \caption{\label{tab:il2f1} Instantiation of level 2 patterns from level 1.
 375  \strut}
 376 \hrule
 377 \[
 378 \begin{array}{rcll}
 379
 380 \IOT{C[t_1,\dots,t_n]}{\mathcal{E}} & =
 381 & C[\IOT{t_1}{\mathcal{E}},\dots,\IOT{t_n}{\mathcal{E}}] \\
 382
 383 \IOT{\mathtt{term}~x}{\mathcal{E}} & = & t & \mathcal{E}(x) = \mathtt{Term}~t \\
 384
 385 \IOT{\mathtt{number}~x}{\mathcal{E}} & =
 386 & n & \mathcal{E}(x) = \mathtt{Number}~n \\
 387
 388 \IOT{\mathtt{ident}~x}{\mathcal{E}} & =
 389 & y & \mathcal{E}(x) = \mathtt{String}~y \\
 390
 391 \IOT{\mathtt{fresh}~x}{\mathcal{E}} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\
 392
 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\} \\
 397
 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\} \\
 402
 403 \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
 404 & =
 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}}
 408 \\
 409
 410 \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
 411 & =
 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) =
 416  \left\{
 417  \begin{array}{@{}ll}
 418  \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_e}{\mathcal{E}''}
 419                 & y=x \\
 420  v_{i1}         & y=y_i \\
 421  \mathcal{E}(y) & \mbox{otherwise} \\
 422  \end{array}
 423  \right.} \\
 424 & & \multicolumn{2}{l}{\mathcal{E}''(y) =
 425  \left\{
 426  \begin{array}{@{}ll}
 427  [v_{i2};\dots;v_{in}] & y=y_i \\
 428  \mathcal{E}(y)        & \mbox{otherwise} \\
 429  \end{array}
 430  \right.} \\
 431
 432 \IOT{\mathtt{fold}~\mathtt{left}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
 433 & =
 434 & \mathit{eval\_fold}(x,P_2,\mathcal{E}')
 435 & \\
 436 & & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->
 437 \IOT{P_1}{\UPDATE{\mathcal{E}}{\NAMES(P_2)|->\bot}}}} \\
 438
 439 \mathit{eval\_fold}(x,P,\mathcal{E})
 440 & =
 441 & \mathcal{E}(x)
 442 & \mathcal{E}(\NAMES(P)\setminus\{x\})=\{[],\dots,[]\} \\
 443
 444 \mathit{eval\_fold}(x,P,\mathcal{E})
 445 & =
 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\} \\
 449 &
 450 & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->\IOT{P}{\mathcal{E}''}; ~ y_i |-> [v_{i2};\dots;v_{in_i}]}}
 451 \\
 452 &
 453 & \multicolumn{2}{l}{\mathcal{E}''(y) =
 454 \left\{
 455 \begin{array}{ll}
 456  v_1            & y\in \NAMES(P)\setminus\{x\} \\
 457  \mathcal{E}(x) & y=x \\
 458  \bot           & \mathit{otherwise} \\
 459 \end{array}
 460 \right.
 461 }
 462 \\
 463
 464 \end{array} \\
 465 \]
 466 \end{table}
 467
 468 \begin{table}
 469 \caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
 470 \hrule
 471 \[
 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}
 477   \\
 478   \inference[\sc TermVar]
 479     {}
 480     {t \in [\mathtt{term}]~x ~> [x |-> \mathtt{Term}~t]}
 481   \quad
 482   \inference[\sc NumVar]
 483     {}
 484     {n \in \mathtt{number}~x ~> [x |-> \mathtt{Number}~n]}
 485   \\
 486   \inference[\sc IdentVar]
 487     {}
 488     {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
 489   \quad
 490   \inference[\sc FreshVar]
 491     {}
 492     {x \in \mathtt{fresh}~x ~> [x |-> \mathtt{String}~x]}
 493   \\
 494   \inference[\sc Success]
 495     {}
 496     {t \in \mathtt{anonymous} ~> \emptyset}
 497   \\
 498   \inference[\sc DefaultT]
 499     {t \in P_1 ~> \mathcal E}
 500     {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
 501     \quad
 502     \mathcal E'(x) = \left\{
 503     \renewcommand{\arraystretch}{1}
 504     \begin{array}{ll}
 505       \mathtt{Some}~\mathcal{E}(x) & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
 506       \mathcal{E}(x) & \mbox{otherwise}
 507     \end{array}
 508     \right.
 509   \\
 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'}
 513     \quad
 514     \mathcal E'(x) = \left\{
 515     \renewcommand{\arraystretch}{1}
 516     \begin{array}{ll}
 517       \mathtt{None} & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
 518       \mathcal{E}(x) & \mbox{otherwise}
 519     \end{array}
 520     \right.
 521   \\
 522   \inference[\sc IfT]
 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}
 525   \quad
 526   \inference[\sc IfF]
 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}
 529   \\
 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''}
 533   \\
 534   \mbox{where}~\mathcal{E}''(y) = \left\{
 535     \renewcommand{\arraystretch}{1}
 536     \begin{array}{ll}
 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}
 540     \end{array}
 541   \right.
 542   \\
 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'}
 546   \quad
 547   \mathcal E'(y) = \left\{
 548     \renewcommand{\arraystretch}{1}
 549     \begin{array}{ll}
 550       [] & y \in \NAMES(P_2) \setminus \{x\} \\
 551       \mathcal{E}(y) & \mbox{otherwise}
 552     \end{array}
 553   \right.
 554 \end{array}
 555 \]
 556 \hrule
 557 \end{table}
 558
 559 \begin{table}
 560  \caption{\label{tab:synl3} Abstract syntax of level 3 terms and patterns.}
 561  \hrule
 562  \[
 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)} \\
 569      &  |   & \dots \\[2ex]
 570   \end{array} &
 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)} \\
 579   \end{array} \\
 580  \end{array}
 581  \]
 582  \hrule
 583 \end{table}
 584
 585 \begin{table}
 586 \caption{\label{tab:wfl3} Well-formedness rules for level 3 patterns.\strut}
 587 \hrule
 588 \[
 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}} \\
 594  \inference[\sc Appl]
 595   {P_i :: D_i
 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} \\
 598 \end{array}
 599 \]
 600 \hrule
 601 \end{table}
 602
 603 \begin{table}
 604  \caption{\label{tab:synargp} Abstract syntax of applicative symbol patterns.}
 605  \hrule
 606  \[
 607  \begin{array}{rcll}
 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)} \\
 613  \end{array}
 614  \]
 615  \hrule
 616 \end{table}
 617
 618 \begin{table}
 619 \caption{\label{tab:wfargp} Well-formedness rules for applicative symbol
 620 patterns.\strut}
 621 \hrule
 622 \[
 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]
 630   {}
 631   {\TVAR{x} :: x : \mathtt{Term}}
 632  \quad
 633  \inference[\sc EtaAbs]
 634   {\mathit{arg} :: D}
 635   {\eta.\mathit{arg} :: D}
 636  \\
 637 \end{array}
 638 \]
 639 \hrule
 640 \end{table}
 641
 642 \begin{table}
 643 \caption{\label{tab:l3match} Pattern matching of level 3 terms.\strut}
 644 \hrule
 645 \[
 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 ~> []} \\
 654 \end{array}
 655 \]
 656 \hrule
 657 \end{table}
 658
 659 \begin{table}
 660 \caption{\label{tab:iapf3} Instantiation of applicative symbol patterns (from
 661 level 3).\strut}
 662 \hrule
 663 \[
 664 \begin{array}{rcll}
 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} \\
 674 \end{array}
 675 \]
 676 \hrule
 677 \end{table}
 678
 679 \section{Type checking}
 680
 681 \subsection{Level 1 $<->$ Level 2}
 682
 683 \newcommand{\GUARDED}{\mathit{guarded}}
 684 \newcommand{\TRUE}{\mathit{true}}
 685 \newcommand{\FALSE}{\mathit{false}}
 686
 687 \newcommand{\TN}{\mathit{tn}}
 688
 689 \begin{table}
 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
 696 \[
 697 \begin{array}{rcll}
 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)
 709 \end{array}
 710 \]
 711 \hrule
 712 \end{table}
 713
 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:
 718 %% \[
 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
 737 %% \end{array}
 738 %% \]
 739
 740 We say that a \emph{bidirectional transformation}
 741 \[
 742   P_1 <=> P_2
 743 \]
 744 is well-formed if:
 745 \begin{itemize}
 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
 758     context $Y$.
 759 \end{itemize}
 760
 761 A \emph{left-to-right transformation}
 762 \[
 763   P_1 => P_2
 764 \]
 765 is well-formed if $P_2$ does not contain \texttt{if}, \texttt{fail},
 766 or \texttt{anonymous} meta patterns.
 767
 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
 772 (types).
 773
 774 Relationship with grammatical frameworks?
 775
 776 \subsection{Level 2 $<->$ Level 3}
 777
 778 We say that an \emph{interpretation}
 779 \[
 780  P_2 <=> P_3
 781 \]
 782 is well-formed if:
 783 \begin{itemize}
 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$.
 787 \end{itemize}
 788