\documentclass[a4paper]{article}

\usepackage{manfnt}
\usepackage{a4wide}
\usepackage{pifont}
\usepackage{semantic}
\usepackage{stmaryrd,latexsym}

\newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}

\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}

\title{Extensible notation for \MATITA}
\author{Luca Padovani \qquad Stefano Zacchiroli \\
\small Department of Computer Science, University of Bologna \\
\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
\small \{\texttt{lpadovan}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}

\newcommand{\BREAK}{\mathtt{break}}
\newcommand{\TVAR}[1]{#1:\mathtt{term}}
\newcommand{\NVAR}[1]{#1:\mathtt{number}}
\newcommand{\IVAR}[1]{#1:\mathtt{name}}
\newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
\newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^1}
\newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
\newcommand{\NAMES}{\mathit{names}}
\newcommand{\DOMAIN}{\mathit{domain}}

\mathlig{~>}{\leadsto}
\mathlig{|->}{\mapsto}

\begin{document}
  \maketitle

\section{Environment}

\[
\begin{array}{rcll}
  V & ::= & & \mbox{(\bf values)} \\
    &     & \verb+Term+~T & \mbox{(term)} \\
    &  |  & \verb+String+~s & \mbox{(string)} \\
    &  |  & \verb+Number+~n & \mbox{(number)} \\
    &  |  & \verb+None+ & \mbox{(optional value)} \\
    &  |  & \verb+Some+~V & \mbox{(optional value)} \\
    &  |  & [V_1,\dots,V_n] & \mbox{(list value)} \\[2ex]
\end{array}
\]

An environment is a map $\mathcal E : \mathit{Name} -> V$.

\section{Level 1: concrete syntax}

\begin{table}
\caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut}
\hrule
\[
\begin{array}{rcll}
  P & ::= & & \mbox{(\bf patterns)} \\
    &     & S^{+} \\[2ex]
  S & ::= & & \mbox{(\bf simple patterns)} \\
    &     & l \\
    &  |  & S~\verb+\sub+~S\\
    &  |  & S~\verb+\sup+~S\\
    &  |  & S~\verb+\below+~S\\
    &  |  & S~\verb+\atop+~S\\
    &  |  & S~\verb+\over+~S\\
    &  |  & S~\verb+\atop+~S\\
    &  |  & \verb+\frac+~S~S \\
    &  |  & \verb+\sqrt+~S \\
    &  |  & \verb+\root+~S~\verb+\of+~S \\
    &  |  & \verb+(+~P~\verb+)+ \\
    &  |  & \verb+hbox (+~P~\verb+)+ \\
    &  |  & \verb+vbox (+~P~\verb+)+ \\
    &  |  & \verb+hvbox (+~P~\verb+)+ \\
    &  |  & \verb+hovbox (+~P~\verb+)+ \\
    &  |  & \verb+break+ \\
    &  |  & \verb+list0+~S~[\verb+sep+~l] \\
    &  |  & \verb+list1+~S~[\verb+sep+~l] \\
    &  |  & \verb+opt+~S \\
    &  |  & [\verb+term+]~x \\
    &  |  & \verb+number+~x \\
    &  |  & \verb+ident+~x \\
\end{array}
\]
\hrule
\end{table}

Rationale: while the layout schemata can occur in the concrete syntax
used by user, the box schemata and the magic patterns can only occur
when defining the notation. This is why the layout schemata are
``escaped'' with a backslash, so that they cannot be confused with
plain identifiers, wherease the others are not. Alternatively, they
could be defined as keywords, but this would prevent their names to be
used in different contexts.

\begin{table}
\caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut}
\hrule
\[
\begin{array}{@{}ll@{}}
\begin{array}[t]{rcll}
  T & ::= & & \mbox{(\bf terms)} \\
    &     & L_\kappa[T_1,\dots,T_n] & \mbox{(layout)} \\
    &  |  & B_\kappa^{ab}[T_1\cdots T_n] & \mbox{(box)} \\
    &  |  & \BREAK & \mbox{(breakpoint)} \\
    &  |  & \FENCED{T_1\cdots T_n} & \mbox{(fenced)} \\
    &  |  & l & \mbox{(literal)} \\[2ex]
  P & ::= & & \mbox{(\bf patterns)} \\
    &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
    &  |  & B_\kappa^{ab}[P_1\cdots P_n] & \mbox{(box)} \\
    &  |  & \BREAK & \mbox{(breakpoint)} \\
    &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
    &  |  & M & \mbox{(magic)} \\
    &  |  & V & \mbox{(variable)} \\
    &  |  & l & \mbox{(literal)} \\
\end{array} &
\begin{array}[t]{rcll}
  V & ::= & & \mbox{(\bf variables)} \\
    &     & \TVAR{x} & \mbox{(term variable)} \\
    &  |  & \NVAR{x} & \mbox{(number variable)} \\
    &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
  M & ::= & & \mbox{(\bf magic patterns)} \\
    &     & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
    &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
    &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
\end{array}
\end{array}
\]
\hrule
\end{table}

\[
\IOT{\cdot}{{}} : P -> \mathit{Env} -> T
\]

\begin{table}
\caption{\label{tab:il1} Instantiation of level 1 patterns.\strut}
\hrule
\[
\begin{array}{rcll}
  \IOT{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\IOT{(P_1)}{E},\dots,\IOT{(P_n)}{E} ] \\
  \IOT{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\
  \IOT{\BREAK}{E} & = & \BREAK \\
  \IOT{(P)}{E} & = & \IOT{P}{E} \\
  \IOT{(P_1\cdots P_n)}{E} & = & B_H^{00}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\
  \IOT{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
  \IOT{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
  \IOT{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
  \IOT{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\
  \IOT{\mathtt{opt}~P}{E} & = & \IOT{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
  & & & \mathcal{E}'(x)=\left\{
  \begin{array}{@{}ll}
    v, & \mathcal{E}(x) = \mathtt{Some}~v \\
    \mathcal{E}(x), & \mbox{otherwise}
  \end{array}
  \right. \\
  \IOT{\mathtt{list}k~P~l?}{E} & = & \IOT{P}{{E}_1}~{l?}\cdots {l?}~\IOT{P}{{E}_n} &
    \mathcal{E}(\NAMES(P)) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\
    & & & n\ge k \\
  & & & \mathcal{E}_i(x) = \left\{
  \begin{array}{@{}ll}
    v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\
    \mathcal{E}(x), & \mbox{otherwise}
  \end{array}
  \right. \\
  \IOT{l}{E} & = & l \\

%%     &  |  & (P) & \mbox{(fenced)} \\
%%     &  |  & M & \mbox{(magic)} \\
%%     &  |  & V & \mbox{(variable)} \\
%%     &  |  & l & \mbox{(literal)} \\[2ex]
%%   V & ::= & & \mbox{(\bf variables)} \\
%%     &     & \TVAR{x} & \mbox{(term variable)} \\
%%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
%%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
%%   M & ::= & & \mbox{(\bf magic patterns)} \\
%%     &     & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
%%     &  |  & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
%%     &  |  & \verb+opt+~S & \mbox{(option)} \\[2ex]  
\end{array}
\]
\hrule
\end{table}

\begin{table}
\caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut}
\hrule
\[
\renewcommand{\arraystretch}{3.5}
\begin{array}[t]{@{}c@{}}
  \inference[\sc layout]
    {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
    {L_\kappa[P_1,\dots,P_n] :: D_1\oplus\cdots\oplus D_n}
  \\
  \inference[\sc box]
    {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
    {B_\kappa^{ab}[P_1\cdots P_n] :: D_1\oplus\cdots\oplus D_n}
  \\
  \inference[\sc fenced]
    {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
    {\FENCED{P_1\cdots P_n} :: D_1\oplus\cdots\oplus D_n}
  \\
  \inference[\sc breakpoint]
    {}
    {\BREAK :: \emptyset}
  \qquad
  \inference[\sc literal]
    {}
    {l :: \emptyset}
  \qquad
  \inference[\sc tvar]
    {}
    {\TVAR{x} :: \TVAR{x}}
  \\
  \inference[\sc nvar]
    {}
    {\NVAR{x} :: \NVAR{x}}
  \qquad
  \inference[\sc ivar]
    {}
    {\IVAR{x} :: \IVAR{x}}
  \\
  \inference[\sc list0]
    {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
    {\mathtt{list0}~P~l? :: D'}
  \\
  \inference[\sc list1]
    {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
    {\mathtt{list1}~P~l? :: D'}
  \\
  \inference[\sc opt]
    {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}}
    {\mathtt{opt}~P :: D'}
\end{array}
\]
\hrule
\end{table}

\newcommand{\ATTRS}[1]{\langle#1\rangle}
\newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}}

\begin{table}
\caption{\label{tab:addparens} Where are parentheses added? Look here.\strut}
\hrule
\[
\begin{array}{rcll}
  \ADDPARENS{l}{n} & = & l \\
  \ADDPARENS{\BREAK}{n} & = & \BREAK \\
  \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \ADDPARENS{T}{m} & n < m \\
  \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} & n > m \\
  \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=L,\mathit{pos}=R}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
  \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=R,\mathit{pos}=L}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
  \ADDPARENS{\ATTRS{\cdots}T}{n} & = & \ADDPARENS{T}{n} \\
  \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}] \\
  \ADDPARENS{B_\kappa^{ab}[T_1,\dots,T_m]}{n} & = & B_\kappa^{ab}[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_m}{n}]
\end{array}
\]
\hrule
\end{table}

\begin{table}
\caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut}
\hrule
\[
\begin{array}{rcll}
  \ANNPOS{l}{p,q} & = & l \\
  \ANNPOS{\BREAK}{p,q} & = & \BREAK \\
  \ANNPOS{x}{1,0} & = & \ATTRS{\mathit{pos}=L}{x} \\
  \ANNPOS{x}{0,1} & = & \ATTRS{\mathit{pos}=R}{x} \\
  \ANNPOS{x}{p,q} & = & \ATTRS{\mathit{pos}=I}{x} \\
  \ANNPOS{B_\kappa^{ab}[P]}{p,q} & = & B_\kappa^{ab}[\ANNPOS{P}{p,q}] \\
  \ANNPOS{B_\kappa^{ab}[\{\BREAK\} P_1\cdots P_n\{\BREAK\}]}{p,q} & = & B_\kappa^{ab}[\begin{array}[t]{@{}l}
      \{\BREAK\} \ANNPOS{P_1}{p,0} \\
      \ANNPOS{P_2}{0,0}\cdots\ANNPOS{P_{n-1}}{0,0} \\
      \ANNPOS{P_n}{0,q}\{\BREAK\}]
  \end{array}

%%     &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
%%     &  |  & \BREAK & \mbox{(breakpoint)} \\
%%     &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
%%   V & ::= & & \mbox{(\bf variables)} \\
%%     &     & \TVAR{x} & \mbox{(term variable)} \\
%%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
%%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
%%   M & ::= & & \mbox{(\bf magic patterns)} \\
%%     &     & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
%%     &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
%%     &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
\end{array}
\]
\hrule
\end{table}

\section{Level 2: abstract syntax}

\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}

\begin{table}
\[
\begin{array}{@{}rcll@{}}
  \NT{term} & ::= & & \mbox{\bf terms} \\
    &     & x & \mbox{(identifier)} \\
    &  |  & n & \mbox{(number)} \\
    &  |  & \mathrm{URI} & \mbox{(URI)} \\
    &  |  & \verb+?+ & \mbox{(implicit)} \\
    &  |  & \verb+%+ & \mbox{(placeholder)} \\
    &  |  & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
    &  |  & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
    &  |  & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
    &  |  & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
    &  |  & \NT{term}~\NT{term} & \mbox{(application)} \\
    &  |  & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
    &  |  & [\verb+[+~\NT{term}~\verb+]+]~\verb+match+~\NT{term}~\verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \mbox{(pattern match)} \\
    &  |  & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
    &  |  & \verb+(+~\NT{term}~\verb+)+ \\
    &  |  & \BLOB(\NT{meta},\dots,\NT{meta}) & \mbox{(meta blob)} \\
  \NT{defs}  & ::= & & \mbox{\bf mutual definitions} \\
    &     & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
  \NT{fun} & ::= & & \mbox{\bf functions} \\
    &     & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
  \NT{binder} & ::= & & \mbox{\bf binders} \\
    &     & \verb+\Pi+ \mid \verb+\exists+ \mid \verb+\forall+ \mid \verb+\lambda+ \\
  \NT{arg} & ::= & & \mbox{\bf single argument} \\
    &     & \verb+_+ \mid x \mid \BLOB(\NT{meta},\dots,\NT{meta}) \\
  \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
    &     & \NT{arg} \\
    &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
  \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
    &     & \NT{arg} \\
    &  |  & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
  \NT{kind} & ::= & & \mbox{\bf induction kind} \\
    &     & \verb+rec+ \mid \verb+corec+ \\
  \NT{rule} & ::= & & \mbox{\bf rules} \\
    &     & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]

  \NT{meta} & ::= & & \mbox{\bf meta} \\
    &     & \BLOB(\NT{term},\dots,\NT{term}) & (term blob) \\
    &  |  & [\verb+term+]~x \\
    &  |  & \verb+number+~x \\
    &  |  & \verb+ident+~x \\
    &  |  & \verb+fresh+~x \\
    &  |  & \verb+anonymous+ \\
    &  |  & \verb+fold+~[\verb+left+\mid\verb+right+]~\NT{meta}~\verb+rec+~x~\NT{meta} \\
    &  |  & \verb+default+~\NT{meta}~\NT{meta} \\
    &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
    &  |  & \verb+fail+ 
\end{array}
\]
\end{table}

\begin{table}
\caption{\label{tab:wfl2} Well-formedness rules for level 2 patterns.\strut}
\hrule
\[
\renewcommand{\arraystretch}{3.5}
\begin{array}{@{}c@{}}
  \inference[\sc Constr]
    {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
    {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\
  \inference[\sc TermVar]
    {}
    {[\mathtt{term}]~x :: x : \mathtt{Term}}
  \quad
  \inference[\sc NumVar]
    {}
    {\mathtt{number}~x :: x : \mathtt{Number}}
  \\
  \inference[\sc IdentVar]
    {}
    {\mathtt{ident}~x :: x : \mathtt{String}}
  \quad
  \inference[\sc FreshVar]
    {}
    {\mathtt{fresh}~x :: x : \mathtt{String}}
  \\
  \inference[\sc Success]
    {}
    {\mathtt{anonymous} :: \emptyset}
  \\
  \inference[\sc Fold]
    {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}
    {\mathtt{fold}~P_1~\mathtt{rec}~x~P_2 :: D_1 \oplus D_2~\mathtt{List}}
  \\
  \inference[\sc Default]
    {P_1 :: D \oplus D_1 & P_2 :: D & \DOMAIN(D_1) \ne \emptyset & \DOMAIN(D) \cap \DOMAIN(D_1) = \emptyset}
    {\mathtt{default}~P_1~P_2 :: D \oplus D_1~\mathtt{Option}}
  \\
  \inference[\sc If]
    {P_1 :: \emptyset & P_2 :: D & P_3 :: D }
    {\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 :: D}
  \qquad
  \inference[\sc Fail]
    {}
    {\mathtt{fail} : \emptyset}
%%     &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
%%     &  |  & \verb+fail+ 
\end{array}
\]
\hrule
\end{table}

\begin{table}
\caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
\hrule
\[
\renewcommand{\arraystretch}{3.5}
\begin{array}{@{}c@{}}
  \inference[\sc Constr]
    {t_i \in P_i ~> \mathcal E_i & i\ne j => \DOMAIN(\mathcal E_i)\cap\DOMAIN(\mathcal E_j)=\emptyset}
    {C[t_1,\dots,t_n] \in C[P_1,\dots,P_n] ~> \mathcal E_1 \oplus \cdots \oplus \mathcal E_n}
  \\
  \inference[\sc TermVar]
    {}
    {t \in [\mathtt{term}]~x ~> [x |-> \mathtt{Term}~t]}
  \quad
  \inference[\sc NumVar]
    {}
    {n \in \mathtt{number}~x ~> [x |-> \mathtt{Number}~n]}
  \\
  \inference[\sc IdentVar]
    {}
    {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
  \quad
  \inference[\sc FreshVar]
    {}
    {x \in \mathtt{fresh}~x ~> [x |-> \mathtt{String}~x]}
  \\
  \inference[\sc Success]
    {}
    {t \in \mathtt{anonymous} ~> \emptyset}
  \\
  \inference[\sc DefaultT]
    {t \in P_1 ~> \mathcal E}
    {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
    \quad
    \mathcal E'(x) = \left\{
    \renewcommand{\arraystretch}{1}
    \begin{array}{ll}
      \mathtt{Some}~\mathcal{E}(x) & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
      \mathcal{E}(x) & \mbox{otherwise}
    \end{array}
    \right.
  \\
  \inference[\sc DefaultF]
    {t \not\in P_1 & t \in P_2 ~> \mathcal E}
    {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
    \quad
    \mathcal E'(x) = \left\{
    \renewcommand{\arraystretch}{1}
    \begin{array}{ll}
      \mathtt{None} & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
      \mathcal{E}(x) & \mbox{otherwise}
    \end{array}
    \right.
  \\
  \inference[\sc IfT]
    {t \in P_1 ~> \mathcal E' & t \in P_2 ~> \mathcal E}
    {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
  \quad
  \inference[\sc IfF]
    {t \not\in P_1 & t \in P_3 ~> \mathcal E}
    {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
  \\
  \inference[\sc FoldR]
    {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
    {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
  \quad
  \mathcal E''(y) = \left\{
    \renewcommand{\arraystretch}{1}
    \begin{array}{ll}
      \mathcal{E}(y)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \\
      \mathcal{E}'(y) & \mbox{otherwise}
    \end{array}  
  \right.
  \\
  \inference[\sc FoldB]
    {t \not\in P_2 & t \in P_1 ~> \mathcal E}
    {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
  \quad
  \mathcal E'(y) = \left\{
    \renewcommand{\arraystretch}{1}
    \begin{array}{ll}
      [] & y \in \NAMES(P_2) \setminus \{x\} \\
      \mathcal{E}(y) & \mbox{otherwise}
    \end{array}  
  \right.
\end{array}
\]
\hrule
\end{table}

\section{Type checking}

\newcommand{\TN}{\mathit{tn}}

Assume that we have two corresponding patterns $P_1$ (level 1) and
$P_2$ (level 2) and that we have to check whether they are
``correct''. First we define the notion of \emph{top-level names} of
$P_1$ and $P_2$, as follows:
\[
\begin{array}{rcl}
  \TN(C_1[P'_1,\dots,P'_2]) & = & \TN(P'_1) \cup \cdots \cup \TN(P'_2) \\
  \TN(\TVAR{x}) & = & \{x\} \\
  \TN(\NVAR{x}) & = & \{x\} \\
  \TN(\IVAR{x}) & = & \{x\} \\
  \TN(\mathtt{list0}~P'~l?) & = & \emptyset \\
  \TN(\mathtt{list1}~P'~l?) & = & \emptyset \\
  \TN(\mathtt{opt}~P') & = & \emptyset \\[3ex]

  \TN(\BLOB(P''_1,\dots,P''_2)) & = & \TN(P''_1) \cup \cdots \cup \TN(P''_2) \\
  \TN(\mathtt{term}~x) & = & \{x\} \\
  \TN(\mathtt{number}~x) & = & \{x\} \\
  \TN(\mathtt{ident}~x) & = & \{x\} \\
  \TN(\mathtt{fresh}~x) & = & \{x\} \\
  \TN(\mathtt{anonymous}) & = & \emptyset \\
  \TN(\mathtt{fold}~P''_1~\mathtt{rec}~x~P''_2) & = & \TN(P''_1) \\
  \TN(\mathtt{default}~P''_1~P''_2) & = & \TN(P''_1) \cap \TN(P''_2) \\
  \TN(\mathtt{if}~P''_1~\mathtt{then}~P''_2~\mathtt{else}~P''_3) & = & \TN(P''_2) \\
  \TN(\mathtt{fail}) & = & \emptyset
\end{array}
\]

We say that a \emph{bidirectional transformation}
\[
  P_1 <=> P_2
\]
is well-formed if:
\begin{itemize}
  \item the two patterns are well-formed in the same context $D$, that
    is $P_1 :: D$ and $P_2 :: D$;
  \item for any direct sub-pattern $\mathtt{opt}~P'_1$ of $P_1$ such
    that $\mathtt{opt}~P'_1 :: X$ there is a sub-pattern
    $\mathtt{default}~P'_2~P''_2$ of $P_2$ such that
    $\mathtt{default}~P'_2~P''_2 :: X \oplus Y$ for some context $Y$;
  \item for any direct sub-pattern $\mathtt{list}~P'_1~l?$ of $P_1$
    such that $\mathtt{list}~P'_1~l? :: X$ there is a sub-pattern
    $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2$ of $P_2$ such that
    $\mathtt{fold}~P'_2~\mathtt{rec}~x~P''_2 :: X \oplus Y$ for some
    context $Y$.
\end{itemize}

A \emph{left-to-right transformation}
\[
  P_1 => P_2
\]
is well-formed if $P_2$ does not contain \texttt{if}, \texttt{fail},
or \texttt{anonymous} meta patterns.

Note that the transformations are in a sense asymmetric. Moving from
the concrete syntax (level 1) to the abstract syntax (level 2) we
forget about syntactic details. Moving from the abstract syntax to the
concrete syntax we may want to forget about redundant structure
(types).

Relationship with grammatical frameworks?

\end{document}