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