helm/ocaml/cic_notation/doc/main.tex

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