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{\NVAR}[1]{#1:\mathtt{number}}
  22 \newcommand{\IVAR}[1]{#1:\mathtt{name}}
  23 \newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
  24 \newcommand{\ITO}[2]{|[#1|]_{\mathcal#2}^1}
  25 \newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^2}
  26 \newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
  27 \newcommand{\NAMES}{\mathit{names}}
  28 \newcommand{\DOMAIN}{\mathit{domain}}
  29
  30 \mathlig{~>}{\leadsto}
  31 \mathlig{|->}{\mapsto}
  32
  33 \begin{document}
  34   \maketitle
  35
  36 \section{Environment}
  37
  38 \[
  39 \begin{array}{rcll}
  40   V & ::= & & \mbox{(\bf values)} \\
  41     &     & \verb+Term+~T & \mbox{(term)} \\
  42     &  |  & \verb+String+~s & \mbox{(string)} \\
  43     &  |  & \verb+Number+~n & \mbox{(number)} \\
  44     &  |  & \verb+None+ & \mbox{(optional value)} \\
  45     &  |  & \verb+Some+~V & \mbox{(optional value)} \\
  46     &  |  & [V_1,\dots,V_n] & \mbox{(list value)} \\[2ex]
  47 \end{array}
  48 \]
  49
  50 An environment is a map $\mathcal E : \mathit{Name} -> V$.
  51
  52 \section{Level 1: concrete syntax}
  53
  54 \begin{table}
  55 \caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut}
  56 \hrule
  57 \[
  58 \begin{array}{rcll}
  59   P & ::= & & \mbox{(\bf patterns)} \\
  60     &     & S^{+} \\[2ex]
  61   S & ::= & & \mbox{(\bf simple patterns)} \\
  62     &     & l \\
  63     &  |  & S~\verb+\sub+~S\\
  64     &  |  & S~\verb+\sup+~S\\
  65     &  |  & S~\verb+\below+~S\\
  66     &  |  & S~\verb+\atop+~S\\
  67     &  |  & S~\verb+\over+~S\\
  68     &  |  & S~\verb+\atop+~S\\
  69     &  |  & \verb+\frac+~S~S \\
  70     &  |  & \verb+\sqrt+~S \\
  71     &  |  & \verb+\root+~S~\verb+\of+~S \\
  72     &  |  & \verb+(+~P~\verb+)+ \\
  73     &  |  & \verb+hbox (+~P~\verb+)+ \\
  74     &  |  & \verb+vbox (+~P~\verb+)+ \\
  75     &  |  & \verb+hvbox (+~P~\verb+)+ \\
  76     &  |  & \verb+hovbox (+~P~\verb+)+ \\
  77     &  |  & \verb+break+ \\
  78     &  |  & \verb+list0+~S~[\verb+sep+~l] \\
  79     &  |  & \verb+list1+~S~[\verb+sep+~l] \\
  80     &  |  & \verb+opt+~S \\
  81     &  |  & [\verb+term+]~x \\
  82     &  |  & \verb+number+~x \\
  83     &  |  & \verb+ident+~x \\
  84 \end{array}
  85 \]
  86 \hrule
  87 \end{table}
  88
  89 Rationale: while the layout schemata can occur in the concrete syntax
  90 used by user, the box schemata and the magic patterns can only occur
  91 when defining the notation. This is why the layout schemata are
  92 ``escaped'' with a backslash, so that they cannot be confused with
  93 plain identifiers, wherease the others are not. Alternatively, they
  94 could be defined as keywords, but this would prevent their names to be
  95 used in different contexts.
  96
  97 \begin{table}
  98 \caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut}
  99 \hrule
 100 \[
 101 \begin{array}{@{}ll@{}}
 102 \begin{array}[t]{rcll}
 103   T & ::= & & \mbox{(\bf terms)} \\
 104     &     & L_\kappa[T_1,\dots,T_n] & \mbox{(layout)} \\
 105     &  |  & B_\kappa^{ab}[T_1\cdots T_n] & \mbox{(box)} \\
 106     &  |  & \BREAK & \mbox{(breakpoint)} \\
 107     &  |  & \FENCED{T_1\cdots T_n} & \mbox{(fenced)} \\
 108     &  |  & l & \mbox{(literal)} \\[2ex]
 109   P & ::= & & \mbox{(\bf patterns)} \\
 110     &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
 111     &  |  & B_\kappa^{ab}[P_1\cdots P_n] & \mbox{(box)} \\
 112     &  |  & \BREAK & \mbox{(breakpoint)} \\
 113     &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
 114     &  |  & M & \mbox{(magic)} \\
 115     &  |  & V & \mbox{(variable)} \\
 116     &  |  & l & \mbox{(literal)} \\
 117 \end{array} &
 118 \begin{array}[t]{rcll}
 119   V & ::= & & \mbox{(\bf variables)} \\
 120     &     & \TVAR{x} & \mbox{(term variable)} \\
 121     &  |  & \NVAR{x} & \mbox{(number variable)} \\
 122     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
 123   M & ::= & & \mbox{(\bf magic patterns)} \\
 124     &     & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
 125     &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
 126     &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
 127 \end{array}
 128 \end{array}
 129 \]
 130 \hrule
 131 \end{table}
 132
 133 \[
 134 \ITO{\cdot}{{}} : P -> \mathit{Env} -> T
 135 \]
 136
 137 \begin{table}
 138 \caption{\label{tab:il1} Instantiation of level 1 patterns.\strut}
 139 \hrule
 140 \[
 141 \begin{array}{rcll}
 142   \ITO{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\ITO{(P_1)}{E},\dots,\ITO{(P_n)}{E} ] \\
 143   \ITO{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
 144   \ITO{\BREAK}{E} & = & \BREAK \\
 145   \ITO{(P)}{E} & = & \ITO{P}{E} \\
 146   \ITO{(P_1\cdots P_n)}{E} & = & B_H^{00}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
 147   \ITO{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
 148   \ITO{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
 149   \ITO{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
 150   \ITO{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\
 151   \ITO{\mathtt{opt}~P}{E} & = & \ITO{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
 152   & & & \mathcal{E}'(x)=\left\{
 153   \begin{array}{@{}ll}
 154     v, & \mathcal{E}(x) = \mathtt{Some}~v \\
 155     \mathcal{E}(x), & \mbox{otherwise}
 156   \end{array}
 157   \right. \\
 158   \ITO{\mathtt{list}k~P~l?}{E} & = & \ITO{P}{{E}_1}~{l?}\cdots {l?}~\ITO{P}{{E}_n} &
 159     \mathcal{E}(\NAMES(P)) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\
 160     & & & n\ge k \\
 161   & & & \mathcal{E}_i(x) = \left\{
 162   \begin{array}{@{}ll}
 163     v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\
 164     \mathcal{E}(x), & \mbox{otherwise}
 165   \end{array}
 166   \right. \\
 167   \ITO{l}{E} & = & l \\
 168
 169 %%     &  |  & (P) & \mbox{(fenced)} \\
 170 %%     &  |  & M & \mbox{(magic)} \\
 171 %%     &  |  & V & \mbox{(variable)} \\
 172 %%     &  |  & l & \mbox{(literal)} \\[2ex]
 173 %%   V & ::= & & \mbox{(\bf variables)} \\
 174 %%     &     & \TVAR{x} & \mbox{(term variable)} \\
 175 %%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
 176 %%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
 177 %%   M & ::= & & \mbox{(\bf magic patterns)} \\
 178 %%     &     & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
 179 %%     &  |  & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
 180 %%     &  |  & \verb+opt+~S & \mbox{(option)} \\[2ex]
 181 \end{array}
 182 \]
 183 \hrule
 184 \end{table}
 185
 186 \begin{table}
 187 \caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut}
 188 \hrule
 189 \[
 190 \renewcommand{\arraystretch}{3.5}
 191 \begin{array}[t]{@{}c@{}}
 192   \inference[\sc layout]
 193     {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
 194     {L_\kappa[P_1,\dots,P_n] :: D_1\oplus\cdots\oplus D_n}
 195   \\
 196   \inference[\sc box]
 197     {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
 198     {B_\kappa^{ab}[P_1\cdots P_n] :: D_1\oplus\cdots\oplus D_n}
 199   \\
 200   \inference[\sc fenced]
 201     {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
 202     {\FENCED{P_1\cdots P_n} :: D_1\oplus\cdots\oplus D_n}
 203   \\
 204   \inference[\sc breakpoint]
 205     {}
 206     {\BREAK :: \emptyset}
 207   \qquad
 208   \inference[\sc literal]
 209     {}
 210     {l :: \emptyset}
 211   \qquad
 212   \inference[\sc tvar]
 213     {}
 214     {\TVAR{x} :: \TVAR{x}}
 215   \\
 216   \inference[\sc nvar]
 217     {}
 218     {\NVAR{x} :: \NVAR{x}}
 219   \qquad
 220   \inference[\sc ivar]
 221     {}
 222     {\IVAR{x} :: \IVAR{x}}
 223   \\
 224   \inference[\sc list0]
 225     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
 226     {\mathtt{list0}~P~l? :: D'}
 227   \\
 228   \inference[\sc list1]
 229     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
 230     {\mathtt{list1}~P~l? :: D'}
 231   \\
 232   \inference[\sc opt]
 233     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}}
 234     {\mathtt{opt}~P :: D'}
 235 \end{array}
 236 \]
 237 \hrule
 238 \end{table}
 239
 240 \newcommand{\ATTRS}[1]{\langle#1\rangle}
 241 \newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}}
 242
 243 \begin{table}
 244 \caption{\label{tab:addparens} Can't read the AST and need parentheses? Here you go!.\strut}
 245 \hrule
 246 \[
 247 \begin{array}{rcll}
 248   \ADDPARENS{l}{n} & = & l \\
 249   \ADDPARENS{\BREAK}{n} & = & \BREAK \\
 250   \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \ADDPARENS{T}{m} & n < m \\
 251   \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} & n > m \\
 252   \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=L,\mathit{pos}=R}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
 253   \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=R,\mathit{pos}=L}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
 254   \ADDPARENS{\ATTRS{\cdots}T}{n} & = & \ADDPARENS{T}{n} \\
 255   \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}] \\
 256   \ADDPARENS{B_\kappa^{ab}[T_1,\dots,T_m]}{n} & = & B_\kappa^{ab}[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_m}{n}]
 257 \end{array}
 258 \]
 259 \hrule
 260 \end{table}
 261
 262 \begin{table}
 263 \caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut}
 264 \hrule
 265 \[
 266 \begin{array}{rcll}
 267   \ANNPOS{l}{p,q} & = & l \\
 268   \ANNPOS{\BREAK}{p,q} & = & \BREAK \\
 269   \ANNPOS{x}{1,0} & = & \ATTRS{\mathit{pos}=L}{x} \\
 270   \ANNPOS{x}{0,1} & = & \ATTRS{\mathit{pos}=R}{x} \\
 271   \ANNPOS{x}{p,q} & = & \ATTRS{\mathit{pos}=I}{x} \\
 272   \ANNPOS{B_\kappa^{ab}[P]}{p,q} & = & B_\kappa^{ab}[\ANNPOS{P}{p,q}] \\
 273   \ANNPOS{B_\kappa^{ab}[\{\BREAK\} P_1\cdots P_n\{\BREAK\}]}{p,q} & = & B_\kappa^{ab}[\begin{array}[t]{@{}l}
 274       \{\BREAK\} \ANNPOS{P_1}{p,0} \\
 275       \ANNPOS{P_2}{0,0}\cdots\ANNPOS{P_{n-1}}{0,0} \\
 276       \ANNPOS{P_n}{0,q}\{\BREAK\}]
 277   \end{array}
 278
 279 %%     &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
 280 %%     &  |  & \BREAK & \mbox{(breakpoint)} \\
 281 %%     &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
 282 %%   V & ::= & & \mbox{(\bf variables)} \\
 283 %%     &     & \TVAR{x} & \mbox{(term variable)} \\
 284 %%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
 285 %%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
 286 %%   M & ::= & & \mbox{(\bf magic patterns)} \\
 287 %%     &     & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
 288 %%     &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
 289 %%     &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
 290 \end{array}
 291 \]
 292 \hrule
 293 \end{table}
 294
 295 \section{Level 2: abstract syntax}
 296
 297 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
 298
 299 \begin{table}
 300 \caption{\label{tab:synl2} Concrete syntax of level 2 patterns.\strut}
 301 \hrule
 302 \[
 303 \begin{array}{@{}rcll@{}}
 304   \NT{term} & ::= & & \mbox{\bf terms} \\
 305     &     & x & \mbox{(identifier)} \\
 306     &  |  & n & \mbox{(number)} \\
 307     &  |  & \mathrm{URI} & \mbox{(URI)} \\
 308     &  |  & \verb+?+ & \mbox{(implicit)} \\
 309     &  |  & \verb+%+ & \mbox{(placeholder)} \\
 310     &  |  & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
 311     &  |  & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
 312     &  |  & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
 313     &  |  & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
 314     &  |  & \NT{term}~\NT{term} & \mbox{(application)} \\
 315     &  |  & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
 316     &  |  & [\verb+[+~\NT{term}~\verb+]+]~\verb+match+~\NT{term}~\verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \mbox{(pattern match)} \\
 317     &  |  & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
 318     &  |  & \verb+(+~\NT{term}~\verb+)+ \\
 319     &  |  & \BLOB(\NT{meta},\dots,\NT{meta}) & \mbox{(meta blob)} \\
 320   \NT{defs}  & ::= & & \mbox{\bf mutual definitions} \\
 321     &     & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
 322   \NT{fun} & ::= & & \mbox{\bf functions} \\
 323     &     & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
 324   \NT{binder} & ::= & & \mbox{\bf binders} \\
 325     &     & \verb+\Pi+ \mid \verb+\exists+ \mid \verb+\forall+ \mid \verb+\lambda+ \\
 326   \NT{arg} & ::= & & \mbox{\bf single argument} \\
 327     &     & \verb+_+ \mid x \mid \BLOB(\NT{meta},\dots,\NT{meta}) \\
 328   \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
 329     &     & \NT{arg} \\
 330     &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
 331   \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
 332     &     & \NT{arg} \\
 333     &  |  & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
 334   \NT{kind} & ::= & & \mbox{\bf induction kind} \\
 335     &     & \verb+rec+ \mid \verb+corec+ \\
 336   \NT{rule} & ::= & & \mbox{\bf rules} \\
 337     &     & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]
 338
 339   \NT{meta} & ::= & & \mbox{\bf meta} \\
 340     &     & \BLOB(\NT{term},\dots,\NT{term}) & \mbox{(term blob)} \\
 341     &  |  & [\verb+term+]~x \\
 342     &  |  & \verb+number+~x \\
 343     &  |  & \verb+ident+~x \\
 344     &  |  & \verb+fresh+~x \\
 345     &  |  & \verb+anonymous+ \\
 346     &  |  & \verb+fold+~[\verb+left+\mid\verb+right+]~\NT{meta}~\verb+rec+~x~\NT{meta} \\
 347     &  |  & \verb+default+~\NT{meta}~\NT{meta} \\
 348     &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
 349     &  |  & \verb+fail+
 350 \end{array}
 351 \]
 352 \hrule
 353 \end{table}
 354
 355 \begin{table}
 356 \caption{\label{tab:wfl2} Well-formedness rules for level 2 patterns.\strut}
 357 \hrule
 358 \[
 359 \renewcommand{\arraystretch}{3.5}
 360 \begin{array}{@{}c@{}}
 361   \inference[\sc Constr]
 362     {P_i :: D_i}
 363     {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\
 364   \inference[\sc TermVar]
 365     {}
 366     {\mathtt{term}~x :: x : \mathtt{Term}}
 367   \quad
 368   \inference[\sc NumVar]
 369     {}
 370     {\mathtt{number}~x :: x : \mathtt{Number}}
 371   \\
 372   \inference[\sc IdentVar]
 373     {}
 374     {\mathtt{ident}~x :: x : \mathtt{String}}
 375   \quad
 376   \inference[\sc FreshVar]
 377     {}
 378     {\mathtt{fresh}~x :: x : \mathtt{String}}
 379   \\
 380   \inference[\sc Success]
 381     {}
 382     {\mathtt{anonymous} :: \emptyset}
 383   \\
 384   \inference[\sc Fold]
 385     {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}
 386     {\mathtt{fold}~P_1~\mathtt{rec}~x~P_2 :: D_1 \oplus D_2~\mathtt{List}}
 387   \\
 388   \inference[\sc Default]
 389     {P_1 :: D \oplus D_1 & P_2 :: D & \DOMAIN(D_1) \ne \emptyset & \DOMAIN(D) \cap \DOMAIN(D_1) = \emptyset}
 390     {\mathtt{default}~P_1~P_2 :: D \oplus D_1~\mathtt{Option}}
 391   \\
 392   \inference[\sc If]
 393     {P_1 :: \emptyset & P_2 :: D & P_3 :: D }
 394     {\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 :: D}
 395   \qquad
 396   \inference[\sc Fail]
 397     {}
 398     {\mathtt{fail} :: \emptyset}
 399 %%     &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
 400 %%     &  |  & \verb+fail+
 401 \end{array}
 402 \]
 403 \hrule
 404 \end{table}
 405
 406 \begin{table}
 407 \caption{...}
 408 \hrule
 409 \[
 410 \begin{array}{rcll}
 411 \IOT{C[t_1,\dots,t_n]}{E} & = & C[\IOT{t_1}{E},\dots,\IOT{t_n}{E}] \\
 412 \IOT{\mathtt{term}~x}{E} & = & t & \mathcal{E}(x) = \mathtt{Term}~t \\
 413 \IOT{\mathtt{number}~x}{E} & = & n & \mathcal{E}(x) = \mathtt{Number}~n \\
 414 \IOT{\mathtt{ident}~x}{E} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\
 415 \IOT{\mathtt{fresh}~x}{E} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\
 416 \IOT{\mathtt{default}~P_1~P_2}{E} & = & \IOT{P_2}{E'} & \mathcal{E}(\NAMES(P_1)\setminus\NAMES(P_2)))=\{\mathtt{None}\} \\
 417 & & & \mathcal{E}'(x) =
 418  \left\{
 419  \begin{array}{@{}ll}
 420  \bot & x \in \NAMES(P_1)\setminus\NAMES(P_2) \\
 421  \mathcal{E}(x) & \mbox{otherwise} \\
 422  \end{array}
 423  \right. \\
 424 \IOT{\mathtt{default}~P_1~P_2}{E} & = & \IOT{P_2}{E'} & \mathcal{E}(\NAMES(P_1)\setminus\NAMES(P_2)))=\{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
 425 & & & \mathcal{E}'(x) =
 426  \left\{
 427  \begin{array}{@{}ll}
 428  v & x \in \NAMES(P_1)\setminus\NAMES(P_2) \wedge \mathcal{E}(x) = \mathtt{Some}~v\\
 429  \mathcal{E}(x) & \mbox{otherwise}
 430  \end{array}
 431  \right. \\
 432 \IOT{\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2}{E}
 433 & =
 434 & \IOT{P_2}{E'}
 435 & \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[]\} \\
 436 & & & \mathcal{E}'(y) =
 437  \left\{
 438  \begin{array}{@{}ll}
 439  \bot & y \in \NAMES(P_2)\setminus\{x\} \\
 440  \mathcal{E}(y) & \mbox{otherwise} \\
 441  \end{array}
 442  \right. \\
 443 \IOT{\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2}{E}
 444 & =
 445 & \IOT{P_2}{E'}
 446 & \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\
 447 & & & \mathcal{E}'(y) =
 448  \left\{
 449  \begin{array}{@{}ll}
 450  \IOT{\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_e}{E''} & y = x \\
 451  v_1 & y\in\NAMES(P_2)\setminus\{x\} \wedge \mathcal{E}(y)=[v_1;\dots;v_n] \\
 452  \mathcal{E}(y) & \mbox{otherwise} \\
 453  \end{array}
 454  \right. \\
 455 & & & \mathcal{E}''(y) =
 456  \left\{
 457  \begin{array}{@{}ll}
 458  [v_2;\dots;v_n] & y\in\NAMES(P_2)\setminus\{x\} \wedge \mathcal{E}(y)=[v_1;\dots;v_n] \\
 459  \mathcal{E}(y) & \mbox{otherwise} \\
 460  \end{array}
 461  \right. \\
 462 \end{array} \\
 463 \]
 464 \end{table}
 465
 466 \begin{table}
 467 \caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
 468 \hrule
 469 \[
 470 \renewcommand{\arraystretch}{3.5}
 471 \begin{array}{@{}c@{}}
 472   \inference[\sc Constr]
 473     {t_i \in P_i ~> \mathcal E_i & i\ne j => \DOMAIN(\mathcal E_i)\cap\DOMAIN(\mathcal E_j)=\emptyset}
 474     {C[t_1,\dots,t_n] \in C[P_1,\dots,P_n] ~> \mathcal E_1 \oplus \cdots \oplus \mathcal E_n}
 475   \\
 476   \inference[\sc TermVar]
 477     {}
 478     {t \in [\mathtt{term}]~x ~> [x |-> \mathtt{Term}~t]}
 479   \quad
 480   \inference[\sc NumVar]
 481     {}
 482     {n \in \mathtt{number}~x ~> [x |-> \mathtt{Number}~n]}
 483   \\
 484   \inference[\sc IdentVar]
 485     {}
 486     {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
 487   \quad
 488   \inference[\sc FreshVar]
 489     {}
 490     {x \in \mathtt{fresh}~x ~> [x |-> \mathtt{String}~x]}
 491   \\
 492   \inference[\sc Success]
 493     {}
 494     {t \in \mathtt{anonymous} ~> \emptyset}
 495   \\
 496   \inference[\sc DefaultT]
 497     {t \in P_1 ~> \mathcal E}
 498     {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
 499     \quad
 500     \mathcal E'(x) = \left\{
 501     \renewcommand{\arraystretch}{1}
 502     \begin{array}{ll}
 503       \mathtt{Some}~\mathcal{E}(x) & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
 504       \mathcal{E}(x) & \mbox{otherwise}
 505     \end{array}
 506     \right.
 507   \\
 508   \inference[\sc DefaultF]
 509     {t \not\in P_1 & t \in P_2 ~> \mathcal E}
 510     {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
 511     \quad
 512     \mathcal E'(x) = \left\{
 513     \renewcommand{\arraystretch}{1}
 514     \begin{array}{ll}
 515       \mathtt{None} & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
 516       \mathcal{E}(x) & \mbox{otherwise}
 517     \end{array}
 518     \right.
 519   \\
 520   \inference[\sc IfT]
 521     {t \in P_1 ~> \mathcal E' & t \in P_2 ~> \mathcal E}
 522     {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
 523   \quad
 524   \inference[\sc IfF]
 525     {t \not\in P_1 & t \in P_3 ~> \mathcal E}
 526     {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
 527   \\
 528   \inference[\sc FoldRec]
 529     {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
 530     {t \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
 531   \\
 532   \mbox{where}~\mathcal{E}''(y) = \left\{
 533     \renewcommand{\arraystretch}{1}
 534     \begin{array}{ll}
 535       \mathcal{E}(y)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{right} \\
 536       \mathcal{E}'(y)@[\mathcal{E}(y)] & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{left} \\
 537       \mathcal{E}'(y) & \mbox{otherwise}
 538     \end{array}
 539   \right.
 540   \\
 541   \inference[\sc FoldBase]
 542     {t \not\in P_2 & t \in P_1 ~> \mathcal E}
 543     {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
 544   \quad
 545   \mathcal E'(y) = \left\{
 546     \renewcommand{\arraystretch}{1}
 547     \begin{array}{ll}
 548       [] & y \in \NAMES(P_2) \setminus \{x\} \\
 549       \mathcal{E}(y) & \mbox{otherwise}
 550     \end{array}
 551   \right.
 552 \end{array}
 553 \]
 554 \hrule
 555 \end{table}
 556
 557 \section{Type checking}
 558
 559 \newcommand{\GUARDED}{\mathit{guarded}}
 560 \newcommand{\TRUE}{\mathit{true}}
 561 \newcommand{\FALSE}{\mathit{false}}
 562
 563 \newcommand{\TN}{\mathit{tn}}
 564
 565 \begin{table}
 566 \caption{\label{tab:guarded} Guarded condition of level 2
 567 pattern. Note that the recursive case of the \texttt{fold} magic is
 568 not explicitly required to be guarded. The point is that it must
 569 contain at least two distinct names, and this guarantees that whatever
 570 is matched by the recursive pattern, the terms matched by those two
 571 names will be smaller than the whole matched term.\strut} \hrule
 572 \[
 573 \begin{array}{rcll}
 574   \GUARDED(C(M(P))) & = & \GUARDED(P) \\
 575   \GUARDED(C(t_1,\dots,t_n)) & = & \TRUE \\
 576   \GUARDED(\mathtt{term}~x) & = & \FALSE \\
 577   \GUARDED(\mathtt{number}~x) & = & \FALSE \\
 578   \GUARDED(\mathtt{ident}~x) & = & \FALSE \\
 579   \GUARDED(\mathtt{fresh}~x) & = & \FALSE \\
 580   \GUARDED(\mathtt{anonymous}) & = & \TRUE \\
 581   \GUARDED(\mathtt{default}~P_1~P_2) & = & \GUARDED(P_1) \wedge \GUARDED(P_2) \\
 582   \GUARDED(\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3) & = & \GUARDED(P_2) \wedge \GUARDED(P_3) \\
 583   \GUARDED(\mathtt{fail}) & = & \TRUE \\
 584   \GUARDED(\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2) & = & \GUARDED(P_2)
 585 \end{array}
 586 \]
 587 \hrule
 588 \end{table}
 589
 590 %% Assume that we have two corresponding patterns $P_1$ (level 1) and
 591 %% $P_2$ (level 2) and that we have to check whether they are
 592 %% ``correct''. First we define the notion of \emph{top-level names} of
 593 %% $P_1$ and $P_2$, as follows:
 594 %% \[
 595 %% \begin{array}{rcl}
 596 %%   \TN(C_1[P'_1,\dots,P'_2]) & = & \TN(P'_1) \cup \cdots \cup \TN(P'_2) \\
 597 %%   \TN(\TVAR{x}) & = & \{x\} \\
 598 %%   \TN(\NVAR{x}) & = & \{x\} \\
 599 %%   \TN(\IVAR{x}) & = & \{x\} \\
 600 %%   \TN(\mathtt{list0}~P'~l?) & = & \emptyset \\
 601 %%   \TN(\mathtt{list1}~P'~l?) & = & \emptyset \\
 602 %%   \TN(\mathtt{opt}~P') & = & \emptyset \\[3ex]
 603 %%   \TN(\BLOB(P''_1,\dots,P''_2)) & = & \TN(P''_1) \cup \cdots \cup \TN(P''_2) \\
 604 %%   \TN(\mathtt{term}~x) & = & \{x\} \\
 605 %%   \TN(\mathtt{number}~x) & = & \{x\} \\
 606 %%   \TN(\mathtt{ident}~x) & = & \{x\} \\
 607 %%   \TN(\mathtt{fresh}~x) & = & \{x\} \\
 608 %%   \TN(\mathtt{anonymous}) & = & \emptyset \\
 609 %%   \TN(\mathtt{fold}~P''_1~\mathtt{rec}~x~P''_2) & = & \TN(P''_1) \\
 610 %%   \TN(\mathtt{default}~P''_1~P''_2) & = & \TN(P''_1) \cap \TN(P''_2) \\
 611 %%   \TN(\mathtt{if}~P''_1~\mathtt{then}~P''_2~\mathtt{else}~P''_3) & = & \TN(P''_2) \\
 612 %%   \TN(\mathtt{fail}) & = & \emptyset
 613 %% \end{array}
 614 %% \]
 615
 616 We say that a \emph{bidirectional transformation}
 617 \[
 618   P_1 <=> P_2
 619 \]
 620 is well-formed if:
 621 \begin{itemize}
 622   \item the pattern $P_2$ is guarded, that is $\GUARDED(P_2)=\TRUE$;
 623   \item the two patterns are well-formed in the same context $D$, that
 624     is $P_1 :: D$ and $P_2 :: D$;
 625   \item for any direct sub-pattern $\mathtt{opt}~P'_1$ of $P_1$ such
 626     that $\mathtt{opt}~P'_1 :: X$ there is a sub-pattern
 627     $\mathtt{default}~P'_2~P''_2$ of $P_2$ such that
 628     $\mathtt{default}~P'_2~P''_2 :: X \oplus Y$ for some context $Y$;
 629   \item for any direct sub-pattern $\mathtt{list}~P'_1~l?$ of $P_1$
 630     such that $\mathtt{list}~P'_1~l? :: X$ there is a sub-pattern
 631     $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2$ of $P_2$ such that
 632     $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2 :: X \oplus Y$ for some
 633     context $Y$.
 634 \end{itemize}
 635
 636 A \emph{left-to-right transformation}
 637 \[
 638   P_1 => P_2
 639 \]
 640 is well-formed if $P_2$ does not contain \texttt{if}, \texttt{fail},
 641 or \texttt{anonymous} meta patterns.
 642
 643 Note that the transformations are in a sense asymmetric. Moving from
 644 the concrete syntax (level 1) to the abstract syntax (level 2) we
 645 forget about syntactic details. Moving from the abstract syntax to the
 646 concrete syntax we may want to forget about redundant structure
 647 (types).
 648
 649 Relationship with grammatical frameworks?
 650
 651 \end{document}