
\section{Introduction}

Mathematical notation plays a fundamental role in mathematical practice: it
helps expressing in a concise symbolic fashion concepts of arbitrary complexity.
Its use in proof assistants like \MATITA{} is no exception. Formal mathematics
indeed often impose to encode mathematical concepts at a very high level of
details (e.g. Peano numbers, implicit arguments) having a restricted toolbox of
syntactic constructions in the calculus.

Consider for example one of the point reached while proving the distributivity
of times over minus on natural numbers included in the \MATITA{} standards
library. (Part of) the reached sequent can be seen in \MATITA{} both using the
notation for various arithmetical and relational operator or without using it.
The sequent rendered without using notation looks as follows:

\sequent{
\mathtt{H}: \mathtt{le} z y\\
\mathtt{Hcut}: \mathtt{eq} \mathtt{nat} (\mathtt{plus} (\mathtt{times} x (\mathtt{minus}
y z)) (\mathtt{times} x z))\\
(\mathtt{plus} (\mathtt{minus} (\mathtt{times} x y) (\mathtt{times} x z))
(\mathtt{times} x z))}{
\mathtt{eq} \mathtt{nat} (\mathtt{times} x (\mathtt{minus} y z)) (\mathtt{minus}
(\mathtt{times} x y) (\mathtt{times} x z))}

while the corresponding sequent rendered with notation enabled looks:

\sequent{
H: z\leq y\\
Hcut: x*(y-z)+x*z=x*y-x*z+x*z}{
x*(y-z)=x*y-x*z}

The latter representation is evidently more readable than the former helping
users both in concentrating on the key aspects of the proof (namely on choosing
the right strategy to proceed in the proof) and in reducing the amount of input
that need to be provided to the system when term input is required (assuming the
exists a correspondence among the rendered output and the textual input syntax
used by the user, as it happens in \MATITA).

In this section we present the \emph{extensible notation} mechanism implemented
in \MATITA. Its role may be looked at from two different point of view: the term
input phase and the term output --- or rendering --- phase. We arbitrarly
decided to call the former view ``from the left'' and the latter ``from the
right''. Looking from the point of view of the input phase it offers a mechanism
of dynamic extension of the term grammar enabling the user to define fancy
mathematical notations.  Looking from the point of view of rendering it enable
the reconstruction of such notations from CIC term and its rendering to various
presentation languages (at the time of writing supported languages are MathML
Presentation and the \MATITA{} concrete syntax for terms).

If you're wondering why the notation mechanisms need to be ``extensible'', the
answer lays in how notation is used in the development of formal mathematics
with proof assistants. When doing ordinary (i.e. non automatically checkable by
the mean of a proof checker) mathematics, notation is often confused with the
mathematical objects being defined. ``+'' may be thought as \emph{the} addition
(and is often termed as such in mathematical textbooks!), but is rather the
notation for one particolar kind of addition which may possibly be used in an
overloaded fashion elsewhere. When doing formal mathematics the difference is
tangible and users has to deal separately with all the actions we skimmed
through:

\begin{enumerate}

 \item definition of mathematical objects (e.g. addition over Peano numbers
  using the primitive recursion scheme);

 \item definition of new mathematical notation (e.g. infix use of the $+$ symbol
  as in $x + 3$);

 \item (incremental) definition of the meanings of a given notation (e.g. the
  use of the notation of (2) above for denoting the addition of (1)).

\end{enumerate}

Since all the points above are part of everyday life of proof assistants users
we know that mathematical notation in the system will change and we can't
provide a ``one-size fits all'' solution as is done for instance in mainstream
programming languages mathematical notation. For this reason \MATITA{} supports
all the above actions in a coherent manner in both term input and output.

\section{Looking from the left: term input}

\subsubsection{\MATITA{} input phase}

 \begin{table}
  \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in
  notation\strut}
 \hrule
 \[
 \begin{array}{@{}rcll@{}}
   \NT{term} & ::= & & \mbox{\bf terms} \\
     &     & x & \mbox{(identifier)} \\
     &  |  & n & \mbox{(number)} \\
     &  |  & s & \mbox{(symbol)} \\
     &  |  & \mathrm{URI} & \mbox{(URI)} \\
     &  |  & \verb+_+ & \mbox{(implicit)} \\
     &  |  & \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+match+~\NT{term}~ & \mbox{(pattern matching)} \\
     &     & ~ ~ [\verb+[+~\verb+in+~x~\verb+]+]
 	      ~ [\verb+[+~\verb+return+~\NT{term}~\verb+]+] \\
     &     & ~ ~ \verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \\
     &  |  & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
     &  |  & \verb+(+~\NT{term}~\verb+)+ \\
   \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+\forall+ \mid \verb+\lambda+ \\
   \NT{arg} & ::= & & \mbox{\bf single argument} \\
     &     & \verb+_+ \mid x \\
   \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}
 \end{array}
 \]
 \hrule
 \end{table}

The primary form of user interaction employed by \MATITA{} is textual script
editing: the user modifies it and evaluate step by step its composing
\emph{statements}. Examples of statements are inductive type definitions,
theorem declarations, LCF-style tacticals, and macros (e.g. \texttt{Check} can
be used to ask the system to refine a given term and pretty print the result).
Since many statements refer to terms of the underlying calculus, \MATITA{} needs
a concrete syntax able to encode terms of the Calculus of Inductive
Constructions.

Two of the requirements in the design of such a syntax are apparently in
contrast:

\begin{enumerate}

 \item the syntax should be as close as possible to common mathematical practice
  and implement widespread mathematical notations;

 \item each term described by the syntax should be non-ambiguous meaning that it
  should exists a function which associates to it a CIC term.

\end{enumerate}

These two requirements are addressed in \MATITA{} by the mean of two mechanisms
which work together: \emph{term disambiguation} and \emph{extensible notation}.
Their interaction is visible in the architecture of the \MATITA{} input phase,
depicted in Fig.~\ref{fig:inputphase}. The architecture is articulated as a
pipeline of three levels: the concrete syntax level (level 0) is the one the
user has to deal with when inserting CIC terms; the abstract syntax level (level
2) is an internal representation which intuitively encodes mathematical formulae
at the content level~\cite{adams}\cite{mkm-structure}; the last level is that of
CIC terms.

\begin{figure}[ht]
 \begin{center}
  \includegraphics[width=0.9\textwidth]{input_phase}
  \caption{\MATITA{} input phase}
 \end{center}
 \label{fig:inputphase}
\end{figure}

Requirement (1) is addressed by a built-in concrete syntax for terms, described
in Tab.~\ref{tab:termsyn}, and the extensible notation mechanisms which offers a
way for extending available mathematical notations and providing a parser for
the extended notation. Requirement (2) is addressed by the conjunct action of
that parsing function and disambiguation which provides a function from content
level terms to CIC terms.

\subsubsection{From concrete syntax to content level}

Content level terms are instances of what are commonly referred as Abstract
Syntax Trees (ASTs) in compilers literature. In this respect the mapping from
concrete syntax fo content level is nothing more than the pipelined application
of a lexer and a parser to the characters that form terms at the concrete syntax
level.

The plus offered by the notation mechanisms is the ability to dinamically extend
the parsing rules which build abstract syntax tree from stream of lexer tokens.
For example, in the standard library of \MATITA{} we found the following
statements which define the notation used for the ``+'' infix operator.

\begin{example}
\begin{Verbatim}
 notation "a + b" 
   left associative with precedence 50
 for @{ 'plus $a $b }.
\end{Verbatim}
\end{example}

The meaning of such a statement is to declare a bidirectional
mapping\footnote{in this section we only deal with the left to right part of the
mapping, but it is actually bidirectional} between a concrete syntax pattern
(the part of the statement inside double quotes) and a content level pattern
(the part of the statement which follows \texttt{for}). The syntax of concrete
syntax patterns and content level patterns can be found in Tab.~\ref{tab:l1c}
and Tab.~\ref{tab:l2c} respectively.

\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}

\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}

\begin{table}
\caption{\label{tab:synl2} Concrete syntax of level 2 patterns.\strut}
\hrule
\[
\begin{array}{@{}rcll@{}}
  \NT{term} & ::= & & \mbox{\bf terms} \\
    &     & x & \mbox{(identifier)} \\
    &  |  & n & \mbox{(number)} \\
    &  |  & s & \mbox{(symbol)} \\
    &  |  & \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}) & \mbox{(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}
\]
\hrule
\end{table}

Each time a \texttt{notation} statement is evaluated by \MATITA{} a new parsing
rule, extracted from the concrete syntax pattern, is added to the term parser
and a semantic action which build a content level term, extracted from the
content level pattern, is associated to it. We will now describe in turn what
can be part of a concrete syntax pattern and what can be part of a content level
pattern.

Concrete syntax patterns, whose abstract syntax can additionally be found in
Tab.~\ref{tab:l1a} can be made of several components. The most basic of which
are \emph{literal symbols} (like the ``+'' in the example above) and \emph{term
variables} (like ``a'' and ``b''). During the extraction of parsing rules
literal symbols are mapped to productions expecting those symbols verbatim as
input and term variables as production expecting other terms (instances of the
same parsing rule we are extending, possibly with different precedence and/or
associativity).

\ldots

\subsubsection{From content level to CIC}

Responsible of mapping content level terms to CIC terms is the disambiguation
algorithm implemented in \MATITA. Since it has already been described
elsewhere~\cite{disambiguation} we wont enter in too much details here. We only
give some highlights of its fundamental concepts.

\subsubsection{Sources of ambiguity}

The translation from content level terms to CIC terms is not straightforward
because some nodes of the content encoding admit more that one CIC encoding,
invalidating requirement (2).

\begin{example}
 \label{ex:disambiguation}

 Consider the term at the concrete syntax level \texttt{\TEXMACRO{forall} x. x +
 ln 1 = x} of Fig.~\ref{fig:inputphase}(a), it can be the type of a lemma the
 user may want to prove. Assuming that both \texttt{+} and \texttt{=} are parsed
 as infix operators, all the following questions are legitimate and must be
 answered before obtaining a CIC term from its content level encoding
 (Fig.~\ref{fig:inputphase}(b)):

 \begin{enumerate}

  \item Since \texttt{ln} is an unbound identifier, which CIC constants does it
   represent? Many different theorems in the library may share its (rather
   short) name \dots

  \item Which kind of number (\IN, \IR, \dots) the \texttt{1} literal stand for?
   Which encoding is used in CIC to represent it? E.g., assuming $1\in\IN$, is
   it an unary or a binary encoding?

  \item Which kind of equality the ``='' node represents? Is it Leibniz's
   polymorhpic equality? Is it a decidable equality over \IN, \IR, \dots?

 \end{enumerate}

\end{example}

In \MATITA, three \emph{sources of ambiguity} are admitted for content level
terms: unbound identifiers, literal numbers, and operators. Each instance of
ambiguity sources (ambiguous entity) occuring in a content level term is
associated to a \emph{disambiguation domain}. Intuitively a disambiguation
domain is a set of CIC terms which may be replaced for an ambiguous entity
during disambiguation. Each item of the domain is said to be an
\emph{interpretation} for the ambiguous entity.

\emph{Unbound identifiers} (question 1) are ambiguous entities since the
namespace of CIC objects is not flat and the same identifier may denote many
ofthem. For example the short name \texttt{plus\_assoc} in the \HELM{} library
is shared by three different theorems stating the associative property of
different additions.  This kind of ambiguity is avoidable if the user is willing
to use long names (in form of URIs in the \texttt{cic://} scheme) in the
concrete syntax, with the obvious drawbacks of obtaining long and unreadable
terms.

Given an unbound identifier, the corresponding disambiguation domain is computed
querying the library for all constants, inductive types, and inductive type
constructors having it as their short name (see the \LOCATE{} query in
Sect.~\ref{sec:metadata}).

\emph{Literal numbers} (question 2) are ambiguous entities as well since
different kinds of numbers can be encoded in CIC (\IN, \IR, \IZ, \dots) using
different encodings. Considering the restricted example of natural numbers we
can for instance encode them in CIC using inductive datatypes with a number of
constructor equal to the encoding base plus 1, obtaining one encoding for each
base.

For each possible way of mapping a literal number to a CIC term, \MATITA{} is
aware of a \emph{number intepretation function} which, when applied to the
natural number denoted by the literal\footnote{at the moment only literal
natural number are supported in the concrete syntax} returns a corresponding CIC
term. The disambiguation domain for a given literal number is built applying to
the literal all available number interpretation functions in turn.

Number interpretation functions can at the moment only be defined in OCaml, but
a mechanism to enable their definition directly in \MATITA{} is under
developement.

\emph{Operators} (question 3) are intuitively head of applications, as such they
are always applied to a (possiblt empty) sequence of arguments. Their ambiguity
is a need since it is often the case that some notation is used in an overloaded
fashion to hide the use of different CIC constants which encodes similar
concepts. For example, in the standard library of \MATITA{} the infix \texttt{+}
notation is available building a binary \texttt{Op(+)} node, whose
disambiguation domain may refer to different constants like the addition over
natural numbers \URI{cic:/matita/nat/plus/plus.con} or that over real numbers of
the \COQ{} standard library \URI{cic:/Coq/Reals/Rdefinitions/Rplus.con}.

For each possible way of mapping an operator application to a CIC term,
\MATITA{} knows an \emph{operator interpretation function} which, when applied
to an operator and its arguments, returns a CIC term. The disambiguation domain
for a given operator is built applying to the operator and its arguments all
available operator interpretation functions in turn.

Operator interpretation functions could be added using the
\texttt{interpretation} statement. For example, among the first line of the
script \texttt{matita/library/logic/equality.ma} from the \MATITA{} standard
library we read:

\begin{Verbatim}
interpretation "leibnitz's equality"
 'eq x y =
   (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
\end{Verbatim}

Evaluating it in \MATITA{} will add an operator interpretation function for the
binary operator \texttt{eq} which expands to the CIC term on the right hand side
of the statement. That CIC term can be written using only built-in concrete
syntax, can contain no ambiguity source; still, it can refer to operator
arguments bound on the left hand side and can contain implicit terms (denoted
with \texttt{\_}) which will be expanded to fresh metavariables. The latter
feature is used in the example above for the first argument of Leibniz's
polymorhpic equality.

\subsubsection{Disambiguation algorithm}

A \emph{disambiguation algorithm} takes as input a content level term and return
a fully determined CIC term. The key observation on which a disambiguation
algorithm is based is that given a content level term with more than one sources
of ambiguity, not all possible combination of interpretation lead to a typable
CIC term. In the term of Ex.~\ref{ex:disambiguation} for instance the
interpretation of \texttt{ln} as a function from \IR to \IR and the
interpretation of \texttt{1} as the Peano number $1$ can't coexists. The notion
of ``can't coexists'' in the disambiguation of \MATITA{} is defined on top of
the \emph{refiner} for CIC terms described in~\cite{csc-phd}.

Briefly, a refiner is a function whose input is an \emph{incomplete CIC term}
$t_1$ --- i.e. a term where metavariables occur (Sect.~\ref{sec:metavariables}
--- and whose output is either

\begin{enumerate}
 
 \item an incomplete CIC term $t_2$ where $t_2$ is a well-typed term obtained
  assigning a type to each metavariable in $t_1$ (in case of dependent types,
  instantiation of some of the metavariable occurring in $t_1$ may occur as
  well);

 \item $\epsilon$, meaning that no well-typed term could be obtained via
  assignment of type to metavariable in $t_1$ and their instantiation;

 \item $\bot$, meaning that the refiner is unable to decide whether of the two
  cases above apply (refinement is semi-decidable).

\end{enumerate}

On top of a CIC refiner \MATITA{} implement an efficient disambiguation
algorithm, which is outlined below. It takes as input a content level term $c$
and proceeds as follows:

\begin{enumerate}

 \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(c)\}$, where
  $\mathit{Dom}(c)$ is the set of ambiguity sources of $c$. Each $D_i$ is a set
  of CIC terms and can be built as described above.

 \item An \emph{interpretation} $\Phi$ for $c$ is a map associating an
  incomplete CIC term to each ambiguity source of $c$. Given $c$ and one of its
  interpretations an incomplete CIC term is fully determined replacing each
  ambiguity source of $c$ with its mapping in the interpretation and injecting
  the remaining structure of the content level in the CIC level (e.g. replacing
  the application of the content level with the application of the CIC level).
  This operation is informally called ``interpreting $c$ with $\Phi$''.
  
  Create an initial interpretation $\Phi_0 = \{\phi_i | \phi_i = \_,
  i\in\mathit{Dom}(c)\}$, which associates a fresh metavariable to each source
  of ambiguity of $c$. During this step, implicit terms are expanded to fresh
  metavariables as well.

 \item Refine the current incomplete CIC term (i.e.  the term obtained
  interpreting $t$ with $\Phi_i$).

  If the refinement succeeds or is undetermined the next interpretation
  $\Phi_{i+1}$ will be created \emph{making a choice}, that is replacing in the
  current interpretation one of the metavariable appearing in $\Phi_i$ with one
  of the possible choice from the corresponding disambiguation domain. The
  metavariable to be replaced is chosen following a preorder visit of the
  ambiguous term. Then, step 3 is attempted again with the new interpretation.
    
  If the refinement fails the current set of choices cannot lead to a well-typed
  term and backtracking of the current interpretation is attempted.
    
 \item Once an unambiguous correct interpretation is found (i.e. $\Phi_i$ does
  no longer contain any placeholder), backtracking is attempted anyway to find
  the other correct interpretations.

 \item Let $n$ be the number of interpretations who survived step 4. If $n=0$
  signal a type error. If $n=1$ we have found exactly one (incomplete) CIC term
  corresponding to the content level term $c$, returns it as output of the
  disambiguation phase. If $n>1$ we have found many different (incomplete) CIC
  terms which can correspond to the content level term, let the user choose one
  of the $n$ interpretations and returns the corresponding term.

\end{enumerate}

The efficiency of this algorithm resides in the fact that as soon as an
incomplete CIC term is not typable, no further instantiation of the
metavariables of the corresponding interpretation is attemped.
% For example, during the disambiguation of the user input
% \texttt{\TEXMACRO{forall} x. x*0 = 0}, an interpretation $\Phi_i$ is
% encountered which associates $?$ to the instance of \texttt{0} on the right,
% the real number $0$ to the instance of \texttt{0} on the left, and the
% multiplication over natural numbers (\texttt{mult} for short) to \texttt{*}.
% The refiner will fail, since \texttt{mult} require a natural argument, and no
% further instantiation of the placeholder will be tried.

Details of the disambiguation algorithm along with an analysis of its complexity
can be found in~\cite{disambiguation}, where a formulation without backtracking
(corresponding to the actual \MATITA{} implementation) is also presented.

\subsubsection{Disambiguation stages}

\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}

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.

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

\begin{table}
\caption{\label{tab:il1f2} Instantiation of level 1 patterns from level 2.\strut}
\hrule
\[
\begin{array}{rcll}
  \ITO{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\ITO{(P_1)}{E},\dots,\ITO{(P_n)}{E} ] \\
  \ITO{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
  \ITO{\BREAK}{E} & = & \BREAK \\
  \ITO{(P)}{E} & = & \ITO{P}{E} \\
  \ITO{(P_1\cdots P_n)}{E} & = & B_H^{00}[\ITO{P_1}{E}\cdots\ITO{P_n}{E}] \\
  \ITO{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
  \ITO{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
  \ITO{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
  \ITO{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\
  \ITO{\mathtt{opt}~P}{E} & = & \ITO{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. \\
  \ITO{\mathtt{list}k~P~l?}{E} & = & \ITO{P}{{E}_1}~{l?}\cdots {l?}~\ITO{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. \\
  \ITO{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} Can't read the AST and need parentheses? Here you go!.\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}

\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}
    {\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:il2f1} Instantiation of level 2 patterns from level 1.
 \strut}
\hrule
\[
\begin{array}{rcll}

\IOT{C[t_1,\dots,t_n]}{\mathcal{E}} & =
& C[\IOT{t_1}{\mathcal{E}},\dots,\IOT{t_n}{\mathcal{E}}] \\

\IOT{\mathtt{term}~x}{\mathcal{E}} & = & t & \mathcal{E}(x) = \mathtt{Term}~t \\

\IOT{\mathtt{number}~x}{\mathcal{E}} & =
& n & \mathcal{E}(x) = \mathtt{Number}~n \\

\IOT{\mathtt{ident}~x}{\mathcal{E}} & =
& y & \mathcal{E}(x) = \mathtt{String}~y \\

\IOT{\mathtt{fresh}~x}{\mathcal{E}} & = & y & \mathcal{E}(x) = \mathtt{String}~y \\

\IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & =
& \IOT{P_1}{\UPDATE{\mathcal{E}}{x_i|->v_i}}
& \mathcal{E}(x_i)=\mathtt{Some}~v_i \\
& & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\

\IOT{\mathtt{default}~P_1~P_2}{\mathcal{E}} & =
& \IOT{P_2}{\UPDATE{\mathcal{E}}{x_i|->\bot}}
& \mathcal{E}(x_i)=\mathtt{None} \\
& & & \NAMES(P_1)\setminus\NAMES(P_2)=\{x_1,\dots,x_n\} \\

\IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
& =
& \IOT{P_1}{\mathcal{E}'}
& \mathcal{E}(\NAMES(P_2)\setminus\{x\}) = \{[],\dots,[]\} \\
& & \multicolumn{2}{l}{\mathcal{E}'=\UPDATE{\mathcal{E}}{\NAMES(P_2)\setminus\{x\}|->\bot}}
\\

\IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
& =
& \IOT{P_2}{\mathcal{E}'}
& \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\
& & & \NAMES(P_2)\setminus\{x\}=\{y_1,\dots,y_m\} \\
& & \multicolumn{2}{l}{\mathcal{E}'(y) =
 \left\{
 \begin{array}{@{}ll}
 \IOT{\mathtt{fold}~\mathtt{right}~P_1~\mathtt{rec}~x~P_e}{\mathcal{E}''}
	        & y=x \\
 v_{i1}		& y=y_i \\
 \mathcal{E}(y) & \mbox{otherwise} \\
 \end{array}
 \right.} \\
& & \multicolumn{2}{l}{\mathcal{E}''(y) =
 \left\{
 \begin{array}{@{}ll}
 [v_{i2};\dots;v_{in}] & y=y_i \\
 \mathcal{E}(y)        & \mbox{otherwise} \\
 \end{array}
 \right.} \\

\IOT{\mathtt{fold}~\mathtt{left}~P_1~\mathtt{rec}~x~P_2}{\mathcal{E}}
& =
& \mathit{eval\_fold}(x,P_2,\mathcal{E}')
& \\
& & \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->
\IOT{P_1}{\UPDATE{\mathcal{E}}{\NAMES(P_2)|->\bot}}}} \\

\mathit{eval\_fold}(x,P,\mathcal{E})
& =
& \mathcal{E}(x)
& \mathcal{E}(\NAMES(P)\setminus\{x\})=\{[],\dots,[]\} \\

\mathit{eval\_fold}(x,P,\mathcal{E})
& =
& \mathit{eval\_fold}(x,P,\mathcal{E}')
& \mathcal{E}(y_i) = [v_{i1},\dots,v_{in}] \\
& & & \NAMES(P)\setminus{x}=\{y_1,\dots,y_m\} \\
&
& \multicolumn{2}{l}{\mathcal{E}' = \UPDATE{\mathcal{E}}{x|->\IOT{P}{\mathcal{E}''}; ~ y_i |-> [v_{i2};\dots;v_{in_i}]}}
\\
&
& \multicolumn{2}{l}{\mathcal{E}''(y) =
\left\{
\begin{array}{ll}
 v_1		& y\in \NAMES(P)\setminus\{x\} \\
 \mathcal{E}(x) & y=x \\
 \bot		& \mathit{otherwise} \\
\end{array}
\right.
}
\\

\end{array} \\
\]
\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 FoldRec]
    {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
    {t \in \mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
  \\
  \mbox{where}~\mathcal{E}''(y) = \left\{
    \renewcommand{\arraystretch}{1}
    \begin{array}{ll}
      \mathcal{E}(y)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{right} \\
      \mathcal{E}'(y)@[\mathcal{E}(y)] & y \in \NAMES(P_2) \setminus \{x\} \wedge d = \mathtt{left} \\
      \mathcal{E}'(y) & \mbox{otherwise}
    \end{array}  
  \right.
  \\
  \inference[\sc FoldBase]
    {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}

\begin{table}
 \caption{\label{tab:synl3} Abstract syntax of level 3 terms and patterns.}
 \hrule
 \[
 \begin{array}{@{}ll@{}}
  \begin{array}[t]{rcll}
   T & : := &   & \mbox{(\bf terms)} \\
     &      & u & \mbox{(uri)} \\
     &  |   & \lambda x.T & \mbox{($\lambda$-abstraction)} \\
     &  |   & (T_1 \dots T_n) & \mbox{(application)} \\
     &  |   & \dots \\[2ex]
  \end{array} &
  \begin{array}[t]{rcll}
   P & : := &   & \mbox{(\bf patterns)} \\
     &      & u & \mbox{(uri)} \\
     &  |   & V & \mbox{(variable)} \\
     &  |   & (P_1 \dots P_n) & \mbox{(application)} \\[2ex]
   V & : := &   & \mbox{(\bf variables)} \\
     &      & \TVAR{x} & \mbox{(term variable)} \\
     &  |   & \IMPVAR & \mbox{(implicit variable)} \\
  \end{array} \\
 \end{array}
 \]
 \hrule
\end{table}

\begin{table}
\caption{\label{tab:wfl3} Well-formedness rules for level 3 patterns.\strut}
\hrule
\[
\renewcommand{\arraystretch}{3.5}
\begin{array}{@{}c@{}}
 \inference[\sc Uri] {} {u :: \emptyset} \quad
 \inference[\sc ImpVar] {} {\TVAR{x} :: \emptyset} \quad
 \inference[\sc TermVar] {} {\TVAR{x} :: x:\mathtt{Term}} \\
 \inference[\sc Appl]
  {P_i :: D_i
   \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset}
  {P_1\cdots P_n :: D_1\oplus\cdots\oplus D_n} \\
\end{array}
\]
\hrule
\end{table}

\begin{table}
 \caption{\label{tab:synargp} Abstract syntax of applicative symbol patterns.}
 \hrule
 \[
 \begin{array}{rcll}
  P & : := &           & \mbox{(\bf patterns)} \\
    &      & s ~ \{ \mathit{arg} \} & \mbox{(symbol pattern)} \\[2ex]
  \mathit{arg} & : := & & \mbox{(\bf argument)} \\
    &      & \TVAR{x} & \mbox{(term variable)} \\
    &  |   & \eta.\mathit{arg} & \mbox{($\eta$-abstraction)} \\
 \end{array}
 \]
 \hrule
\end{table}

\begin{table}
\caption{\label{tab:wfargp} Well-formedness rules for applicative symbol
patterns.\strut}
\hrule
\[
\renewcommand{\arraystretch}{3.5}
\begin{array}{@{}c@{}}
 \inference[\sc Pattern]
  {\mathit{arg}_i :: D_i
   \quad \forall i,j,i\neq j=>\DOMAIN(D_i)\cap\DOMAIN(D_j)=\emptyset}
  {s~\mathit{arg}_1\cdots\mathit{arg}_n :: D_1\oplus\cdots\oplus D_n} \\
 \inference[\sc TermVar]
  {}
  {\TVAR{x} :: x : \mathtt{Term}}
 \quad
 \inference[\sc EtaAbs]
  {\mathit{arg} :: D}
  {\eta.\mathit{arg} :: D}
 \\
\end{array}
\]
\hrule
\end{table}

\begin{table}
\caption{\label{tab:l3match} Pattern matching of level 3 terms.\strut}
\hrule
\[
\renewcommand{\arraystretch}{3.5}
\begin{array}{@{}c@{}}
 \inference[\sc Uri] {} {u\in u ~> []} \quad
 \inference[\sc Appl] {t_i\in P_i ~> \mathcal{E}_i}
  {(t_1\dots t_n)\in(P_1\dots P_n) ~>
   \mathcal{E}_1\oplus\cdots\oplus\mathcal{E}_n} \\
 \inference[\sc TermVar] {} {t\in \TVAR{x} ~> [x |-> \mathtt{Term}~t]} \quad
 \inference[\sc ImpVar] {} {t\in \IMPVAR ~> []} \\
\end{array}
\]
\hrule
\end{table}

\begin{table}
\caption{\label{tab:iapf3} Instantiation of applicative symbol patterns (from
level 3).\strut}
\hrule
\[
\begin{array}{rcll}
 \IAP{s~a_1\cdots a_n}{\mathcal{E}} & = &
  (s~\IAPP{a_1}{\mathcal{E}}{0}\cdots\IAPP{a_n}{\mathcal{E}}{0}) & \\
 \IAPP{\TVAR{x}}{\mathcal{E}}{0} & = & t & \mathcal{E}(x)=\mathtt{Term}~t \\
 \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & = & \lambda y.\IAPP{t}{\mathcal{E}}{i}
  & \mathcal{E}(x)=\mathtt{Term}~\lambda y.t \\
 \IAPP{\TVAR{x}}{\mathcal{E}}{i+1} & =
  & \lambda y_1.\cdots.\lambda y_{i+1}.t~y_1\cdots y_{i+1}
  & \mathcal{E}(x)=\mathtt{Term}~t\wedge\forall y,t\neq\lambda y.t \\
 \IAPP{\eta.a}{\mathcal{E}}{i} & = & \IAPP{a}{\mathcal{E}}{i+1} \\
\end{array}
\]
\hrule
\end{table}

\section{Type checking}

\subsection{Level 1 $<->$ Level 2}

\newcommand{\GUARDED}{\mathit{guarded}}
\newcommand{\TRUE}{\mathit{true}}
\newcommand{\FALSE}{\mathit{false}}

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

\begin{table}
\caption{\label{tab:guarded} Guarded condition of level 2
pattern. Note that the recursive case of the \texttt{fold} magic is
not explicitly required to be guarded. The point is that it must
contain at least two distinct names, and this guarantees that whatever
is matched by the recursive pattern, the terms matched by those two
names will be smaller than the whole matched term.\strut} \hrule
\[
\begin{array}{rcll}
  \GUARDED(C(M(P))) & = & \GUARDED(P) \\
  \GUARDED(C(t_1,\dots,t_n)) & = & \TRUE \\
  \GUARDED(\mathtt{term}~x) & = & \FALSE \\
  \GUARDED(\mathtt{number}~x) & = & \FALSE \\
  \GUARDED(\mathtt{ident}~x) & = & \FALSE \\
  \GUARDED(\mathtt{fresh}~x) & = & \FALSE \\
  \GUARDED(\mathtt{anonymous}) & = & \TRUE \\
  \GUARDED(\mathtt{default}~P_1~P_2) & = & \GUARDED(P_1) \wedge \GUARDED(P_2) \\
  \GUARDED(\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3) & = & \GUARDED(P_2) \wedge \GUARDED(P_3) \\
  \GUARDED(\mathtt{fail}) & = & \TRUE \\
  \GUARDED(\mathtt{fold}~d~P_1~\mathtt{rec}~x~P_2) & = & \GUARDED(P_1)
\end{array}
\]
\hrule
\end{table}

%% 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 $P_1$ is a well-formed \emph{level 1 pattern} in some context $D$ and
  $P_2$ is a well-formed \emph{level 2 pattern} in the very same context $D$,
  that is $P_1 :: D$ and $P_2 :: D$;
  \item the pattern $P_2$ is guarded, that is $\GUARDED(P_2)=\TRUE$;
  \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?

\subsection{Level 2 $<->$ Level 3}

We say that an \emph{interpretation}
\[
 P_2 <=> P_3
\]
is well-formed if:
\begin{itemize}
 \item $P_2$ is a well-formed \emph{applicative symbol pattern} in some context
  $D$ and $P_3$ is a well-formed \emph{level 3 pattern} in the very same
  context $D$, that is $P_2 :: D$ and $P_3 :: D$.
\end{itemize}

\section{Semantic selection}

