helm/ocaml/cic_notation/doc/main.tex

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