+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 be defined in OCaml or directly using
+\TODO{notazione per i numeri}.
+
+\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 \FILE{matita/library/logic/equality.ma} from the \MATITA{} standard
+library we read:
+
+\begin{grafite}
+interpretation "leibnitz's equality"
+ 'eq x y =
+ (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
+\end{grafite}
+
+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}
+
+\NOTE{assumo che si sia gia' parlato di refine}
+
+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 inherited from the
+refiner described in Sect.~\ref{sec:metavariables}: as long as
+$\mathit{refine}(c)\neq\epsilon$, the combination of interpretation which led to
+$c$
+can coexists.
+
+The \emph{naive disambiguation algorithm} takes as input a content level term
+$t$ and proceeds as follows:
+
+\begin{enumerate}
+
+ \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(t)\}$, where
+ $\mathit{Dom}(t)$ is the set of ambiguity sources of $t$. Each $D_i$ is a set
+ of CIC terms and can be built as described above.
+
+ \item Let $\Phi = \{\phi_i | {i\in\mathit{Dom}(t)},\phi_i\in D_i\}$ be an
+ interpretation for $t$. Given $t$ and an interpretation $\Phi$, a CIC term is
+ fully determined. Iterate over all possible interpretations of $t$ and refine
+ the corresponding CIC terms, keep only interpretations which lead to CIC terms
+ $c$ s.t. $\mathit{refine}(c)\neq\epsilon$ (i.e. interpretations that determine
+ typable terms).
+
+ \item Let $n$ be the number of interpretations who survived step 2. If $n=0$
+ signal a type error. If $n=1$ we have found exactly one CIC term corresponding
+ to $t$, returns it as output of the disambiguation phase. If $n>1$ we have
+ found many different 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 above algorithm is highly inefficient since the number of possible
+interpretations $\Phi$ grows exponentially with the number of ambiguity sources.
+The actual algorithm used in \MATITA{} is far more efficient being, in the
+average case, linear in the number of ambiguity sources.
+
+The efficient algorithm --- thoroughly described along with an analysis of its
+complexity in~\cite{disambiguation} --- exploit the refiner and the metavariable
+extension (Sect.~\ref{sec:metavariables}) of the calculus used in \MATITA.
+
+\TODO{FINQUI}
+
+The efficient algorithm can be applied if the logic can be extended with
+metavariables and a refiner can be implemented. This is the case for CIC and
+several other logics.
+\emph{Metavariables}~\cite{munoz} are typed, non linear placeholders that can
+occur in terms; $?_i$ usually denotes the $i$-th metavariable, while $?$ denotes
+a freshly created metavariable. A \emph{refiner}~\cite{McBride} is a
+function whose input is a term with placeholders and whose output is either a
+new term obtained instantiating some placeholder or $\epsilon$, meaning that no
+well typed instantiation could be found for the placeholders occurring in
+the term (type error).
+
+The efficient algorithm starts with an interpretation $\Phi_0 = \{\phi_i |
+\phi_i = ?, i\in\mathit{Dom}(t)\}$,
+which associates a fresh metavariable to each
+source of ambiguity. Then it iterates refining the current CIC term (i.e. the
+term obtained interpreting $t$ with $\Phi_i$). If the refinement succeeds the
+next interpretation $\Phi_{i+1}$ will be created \emph{making a choice}, that is
+replacing a placeholder with one of the possible choice from the corresponding
+disambiguation domain. The placeholder to be replaced is chosen following a
+preorder visit of the ambiguous term. If the refinement fails the current set of
+choices cannot lead to a well-typed term and backtracking is attempted.
+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.
+
+The intuition which explain why this algorithm is more efficient is that as soon
+as a term containing placeholders is not typable, no further instantiation of
+its placeholders could lead to a typable term. For example, during the
+disambiguation of 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.
+
+If, at the end of the disambiguation, more than one possible interpretations are
+possible, the user will be asked to choose the intended one (see
+Fig.~\ref{fig:disambiguation}).
+
+\begin{figure}[htb]
+% \centerline{\includegraphics[width=0.9\textwidth]{disambiguation-1}}
+ \caption{\label{fig:disambiguation} Disambiguation: interpretation choice}
+\end{figure}
+
+Details of the disambiguation algorithm of \WHELP{} can
+be found in~\cite{disambiguation}, where an equivalent algorithm
+that avoids backtracking is also presented.
+
+
+\subsection{notazione}
+\label{sec:notation}
+\ASSIGNEDTO{zack}
+
+\subsection{mathml}
+\ASSIGNEDTO{zack}
+
+\subsection{selezione semantica, cut paste, hyperlink}
+\ASSIGNEDTO{zack}
+
+\subsection{pattern}
+\ASSIGNEDTO{gares}\\
+Patterns are the textual counterpart of the MathML widget graphical
+selection.
+
+Matita benefits of a graphical interface and a powerful MathML rendering
+widget that allows the user to select pieces of the sequent he is working
+on. While this is an extremely intuitive way for the user to
+restrict the application of tactics, for example, to some subterms of the
+conclusion or some hypothesis, the way this action is recorded to the text
+script is not obvious.\\
+In \MATITA{} this issue is addressed by patterns.
+
+\subsubsection{Pattern syntax}
+A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
+$\NT{wanted}$.
+The former mocks-up a sequent, discharging unwanted subterms with $?$ and
+selecting the interesting parts with the placeholder $\%$.
+The latter is a term that lives in the context of the placeholders.
+
+The concrete syntax is reported in table \ref{tab:pathsyn}
+\NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
+\begin{table}
+ \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
+\hrule
+\[
+\begin{array}{@{}rcll@{}}
+ \NT{pattern} &
+ ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
+ \NT{sequent\_path} &
+ ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
+ [~\verb+\vdash+~\NT{multipath}~] & \\
+ \NT{wanted} & ::= & \NT{term} & \\
+ \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\subsubsection{How patterns work}
+Patterns mimic the user's selection in two steps. The first one
+selects roots (subterms) of the sequent, using the
+$\NT{sequent\_path}$, while the second
+one searches the $\NT{wanted}$ term starting from these roots. Both are
+optional steps, and by convention the empty pattern selects the whole
+conclusion.
+
+\begin{description}
+\item[Phase 1]
+ concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
+ part of the syntax. $\NT{ident}$ is an hypothesis name and
+ selects the assumption where the following optional $\NT{multipath}$
+ will operate. \verb+\vdash+ can be considered the name for the goal.
+ If the whole pattern is omitted, the whole goal will be selected.
+ If one or more hypotheses names are given the selection is restricted to
+ these assumptions. If a $\NT{multipath}$ is omitted the whole
+ assumption is selected. Remember that the user can be mostly
+ unaware of this syntax, since the system is able to write down a
+ $\NT{sequent\_path}$ starting from a visual selection.
+ \NOTE{Questo ancora non va in matita}
+
+ A $\NT{multipath}$ is a CiC term in which a special constant $\%$
+ is allowed.
+ The roots of discharged subterms are marked with $?$, while $\%$
+ is used to select roots. The default $\NT{multipath}$, the one that
+ selects the whole term, is simply $\%$.
+ Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
+ that respectively select the first argument of an application or
+ the source of an arrow and the head of the application that is
+ found in the arrow target.
+
+ The first phase selects not only terms (roots of subterms) but also
+ their context that will be eventually used in the second phase.
+
+\item[Phase 2]
+ plays a role only if the $[~\verb+in match+~\NT{wanted}~]$
+ part is specified. From the first phase we have some terms, that we
+ will see as subterm roots, and their context. For each of these
+ contexts the $\NT{wanted}$ term is disambiguated in it and the
+ corresponding root is searched for a subterm $\alpha$-equivalent to
+ $\NT{wanted}$. The result of this search is the selection the
+ pattern represents.
+
+\end{description}
+
+\noindent
+Since the first step is equipotent to the composition of the two
+steps, the system uses it to represent each visual selection.
+The second step is only meant for the
+experienced user that writes patterns by hand, since it really
+helps in writing concise patterns as we will see in the
+following examples.
+
+\subsubsection{Examples}
+To explain how the first step works let's give an example. Consider
+you want to prove the uniqueness of the identity element $0$ for natural
+sum, and that you can relay on the previously demonstrated left
+injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
+Typing
+\begin{grafite}
+theorem valid_name: \forall n,m. m + n = n \to m = O.
+ intros (n m H).
+\end{grafite}
+\noindent
+leads you to the following sequent
+\sequent{
+n:nat\\
+m:nat\\
+H: m + n = n}{
+m=O
+}
+\noindent
+where you want to change the right part of the equivalence of the $H$
+hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
+\begin{grafite}
+ change in H:(? ? ? %) with (O + n).
+\end{grafite}
+\noindent
+This pattern, that is a simple instance of the $\NT{sequent\_path}$
+grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
+and discharges the head of the application and the first two arguments with a
+$?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
+but the user can simply select with the mouse the right part of the equivalence
+and left to the system the burden of writing down in the script file the
+corresponding pattern with $?$ and $\%$ in the right place (that is not
+trivial, expecially where implicit arguments are hidden by the notation, like
+the type $nat$ in this example).
+
+Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$
+works too and can be done, by the experienced user, writing directly
+a simpler pattern that uses the second phase.
+\begin{grafite}
+ change in match n in H with (O + n).
+\end{grafite}
+\noindent
+In this case the $\NT{sequent\_path}$ selects the whole $H$, while
+the second phase searches the wanted $n$ inside it by
+$\alpha$-equivalence. The resulting
+equivalence will be $m+(O+n)=O+n$ since the second phase found two
+occurrences of $n$ in $H$ and the tactic changed both.
+
+Just for completeness the second pattern is equivalent to the
+following one, that is less readable but uses only the first phase.
+\begin{grafite}
+ change in H:(? ? (? ? %) %) with (O + n).
+\end{grafite}
+\noindent
+
+\subsubsection{Tactics supporting patterns}
+In \MATITA{} all the tactics that can be restricted to subterm of the working
+sequent accept the pattern syntax. In particular these tactics are: simplify,
+change, fold, unfold, generalize, replace and rewrite.
+
+\NOTE{attualmente rewrite e fold non supportano phase 2. per
+supportarlo bisogna far loro trasformare il pattern phase1+phase2
+in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
+con una pattern\_of(select(pattern))}
+
+\subsubsection{Comparison with Coq}
+Coq has a two diffrent ways of restricting the application of tactis to
+subterms of the sequent, both relaying on the same special syntax to identify
+a term occurrence.
+
+The first way is to use this special syntax to specify directly to the
+tactic the occurrnces of a wanted term that should be affected, while
+the second is to prepare the sequent with another tactic called
+pattern and the apply the real tactic. Note that the choice is not
+left to the user, since some tactics needs the sequent to be prepared
+with pattern and do not accept directly this special syntax.
+
+The base idea is that to identify a subterm of the sequent we can
+write it and say that we want, for example, the third and the fifth
+occurce of it (counting from left to right). In our previous example,
+to change only the left part of the equivalence, the correct command
+is
+\begin{grafite}
+ change n at 2 in H with (O + n)
+\end{grafite}
+\noindent
+meaning that in the hypothesis $H$ the $n$ we want to change is the
+second we encounter proceeding from left toright.
+
+The tactic pattern computes a
+$\beta$-expansion of a part of the sequent with respect to some
+occurrences of the given term. In the previous example the following
+command
+\begin{grafite}
+ pattern n at 2 in H
+\end{grafite}
+\noindent
+would have resulted in this sequent
+\begin{grafite}
+ n : nat
+ m : nat
+ H : (fun n0 : nat => m + n = n0) n
+ ============================
+ m = 0
+\end{grafite}
+\noindent
+where $H$ is $\beta$-expanded over the second $n$
+occurrence. This is a trick to make the unification algorithm ignore
+the head of the application (since the unification is essentially
+first-order) but normally operate on the arguments.
+This works for some tactics, like rewrite and replace,
+but for example not for change and other tactics that do not relay on
+unification.
+
+The idea behind this way of identifying subterms in not really far
+from the idea behind patterns, but really fails in extending to
+complex notation, since it relays on a mono-dimensional sequent representation.
+Real math notation places arguments upside-down (like in indexed sums or
+integrations) or even puts them inside a bidimensional matrix.
+In these cases using the mouse to select the wanted term is probably the
+only way to tell the system exactly what you want to do.
+
+One of the goals of \MATITA{} is to use modern publishing techiques, and
+adopting a method for restricting tactics application domain that discourages
+using heavy math notation, would definitively be a bad choice.
+
+\subsection{tatticali}
+\ASSIGNEDTO{gares}
+
+\subsection{named variable e disambiguazione lazy}
+\ASSIGNEDTO{csc}
+
+\subsection{metavariabili}
+\label{sec:metavariables}
+\ASSIGNEDTO{csc}
+
+\begin{verbatim}
+
+\end{verbatim}
+
+\section{Drawbacks, missing, \dots}
+
+\subsection{moduli}
+\ASSIGNEDTO{}
+
+\subsection{ltac}
+\ASSIGNEDTO{}
+
+\subsection{estrazione}
+\ASSIGNEDTO{}
+
+\subsection{localizzazione errori}
+\ASSIGNEDTO{}
+
+\acknowledgements