have either adopted or cloned Proof General as their main user interface.
The authoring interface of \MATITA{} is a clone of the Proof General interface.
+TODO
\begin{itemize}
- \item scelta del sistema fondazional.
\item sistema indipendente (da \COQ)
\item compatibilit\`a con sistemi legacy
\end{itemize}
providing a mapping from logical names (URIs) to the physical location
of a notion (an URL). The \texttt{urimanager} \component{} provides the URI
data type and several utility functions over URIs. The
- \texttt{cic\_proof\_checking} \component{} calls the \GETTER
+ \texttt{cic\_proof\_checking} \component{} calls the \GETTER{}
\component{} every time it needs to retrieve the definition of a mathematical
notion referenced by a term that is being type-checked.
\subsubsection{Disambiguation aliases}
\label{sec:disambaliases}
-Let us start with the definition of the ``strictly greater then'' notion over
-(Peano) natural numbers.
-\begin{grafite}
-include "nat/nat.ma".
-..
-definition gt: nat \to nat \to Prop \def
- \lambda n, m. m < n.
-\end{grafite}
-
-The \texttt{include} statement adds the requirement that the part of the library
-defining the notion of natural numbers should be defined before
-processing what follows. Note indeed that the algorithm presented
-in~\cite{disambiguation} does not describe where interpretations for ambiguous
-expressions come from, since it is application-specific. As a first
-approximation, we will assume that in \MATITA{} they come from the library (i.e.
-all interpretations available in the library are used) and the \texttt{include}
-statements are used to ensure the availability of required library slices (see
-Sect.~\ref{sec:libmanagement}).
-
-While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
-terms: its type and its body. Being available in the required library only one
-interpretation both for the unbound identifier \texttt{nat} and for the
-\OP{<} operator, and being the resulting partially specified term refinable,
-both type and body are easily disambiguated.
-
-Now suppose we have defined integers as signed natural numbers, and that we want
-to prove a theorem about an order relationship already defined on them (which of
-course overload the \OP{<} operator):
+Consider the following command to state a theorem over integer numbers.
\begin{grafite}
-include "Z/z.ma".
-..
theorem Zlt_compat:
\forall x, y, z. x < y \to y < z \to x < z.
\end{grafite}
-Since integers are defined on top of natural numbers, the part of the library
-concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
-type. Thus, according to the disambiguation algorithm, two different partially
-specified terms could be associated to it. At first, this might not be seen as a
-problem, since the user is asked and can choose interactively which of the two
-she had in mind. However in the long run it has the drawbacks of inhibiting
-batch compilation of the library (a technique used in \MATITA{} for behind the
-scene compilation when needed, e.g. when an \texttt{include} is issued) and
-yields to poor user interaction (imagine how tedious would be to be asked for a
-choice each time you re-evaluate \texttt{Zlt\_compat}!).
-
-For this reason we added to \MATITA{} the concept of \emph{disambiguation
-aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
-expressions to partially specified terms, which are part of the runtime status
-of \MATITA. They can be provided by users with the \texttt{alias} statement, but
-are usually automatically added when evaluating \texttt{include} statements
-(\emph{implicit aliases}). Aliases implicitly inferred during disambiguation
-are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
-which require interactive choice are saved in batch compilable format. Thus,
-after evaluating the above theorem the script will be changed to the following
-snippet (assuming that the interpretation of \OP{<} over integers has been
-chosen):
+The symbol ``\texttt{<}'' is likely to be overloaded in the library
+(at least over natural numbers).
+Thus, according to the disambiguation algorithm, two different
+refinable partially specified terms could be associated to it.
+\MATITA{} asks the user what interpretation he meant. However, to avoid
+posing the same question in case of a future re-execution (e.g. undo/redo),
+the choice must be recorded. Scripts need to be re-executed after invalidation.
+Therefore the choice record must be permanently stored somewhere. The most
+natural place is in the script itself.
+
+In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}.
+They are mappings, stored in the library, from ambiguity sources
+(identifiers, symbols and literal numbers at the content level) to partially
+specified terms. In case of overloaded sources there exists multiple aliases
+with the same source. It is possible to record \emph{disambiguation
+preferences} to select one of the aliases of an overloaded source.
+
+Preferences can be explicitely given in the script (using the
+misleading \texttt{alias} commands), but
+are also implicitly added when a new concept is introduced (\emph{implicit
+preferences}) or after a sucessfull disambiguation that did not require
+user interaction. Explicit preferences are added automatically by \MATITA{} to
+record the disambiguation choices of the user. For instance, after the
+disambiguation of the command above, the script is altered as follows:
\begin{grafite}
alias symbol "lt" = "integer 'less than'".
\forall x, y, z. x < y \to y < z \to x < z.
\end{grafite}
-But how are disambiguation aliases used? Since they come from the parts of the
-library explicitly included we may be tempted of using them as the only
-available interpretations. This would speed up the disambiguation, but may fail.
-Consider for example:
+The ``alias'' command in the example sets the preferred alias for the
+``\texttt{lt}'' symbol.
+
+Implicit preferences for new concepts are set since a concept just defined is
+likely to be the preferred one in the rest of the script. Implicit preferences
+learned from disambiguation of previous commands grant the coherence of
+the disambiguation in the rest of the script and speed up disambiguation
+reducing the search space.
+
+Disambiguation preferences are included in the lexicon status
+(see Sect.~\ref{???}) that is part of the authoring interface status.
+Unlike aliases, they are not part of the library.
+
+When starting a new authoring session the set of disambiguation preferences
+is empty. Until it contains a preference for each overloaded symbol to be
+used in the script, the user can be faced with questions from the disambiguator.
+To reduce the likelyhood of user interactions, we introduced
+the \texttt{include} command. With \texttt{include} it is possible to import
+at once in the current session the set of preferences that was in effect
+at the end of the execution of a given script.
+
+Preferences can be changed. For instance, at the start of the development
+of integer numbers the preference for the symbol ``\texttt{<}'' is likely
+to be the one over natural numbers; sooner or later it will be set to the one
+over integer numbers.
+
+Nothing forbids the set of preferences to become incoherent. For this reason
+the disambiguator cannot always respect the user preferences.
+For example consider:
\begin{grafite}
-theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
+theorem Zlt_mono: \forall x, y, k. x < y \to x < y + k.
\end{grafite}
+No refinable partially specified term corresponds to the preferences:
+\OP{+} over natural numbers, \OP{<} over integer numbers.
+When the disambiguator fails, disambiguation is tried again with a less
+strict set of preferences. Thus disambiguation is organized in
+multiple \emph{passes}. In the first pass, called \emph{mono-preferences},
+we consider only the aliases corresponding to the current preferences.
+In the second pass, called \emph{multi-preferences},
+we consider every alias corresponding to a current or past preference.
+For instance, in the example above disambiguation succeeds in the
+multi-preference pass
+TODO: CAMBIATO SOLO FINO A QUI
+
+
and suppose that the \OP{+} operator is defined only on natural numbers. If
the alias for \OP{<} points to the integer version of the operator, no
refinable partially specified term matching the term could be found.
\end{center}
\end{figure}
+TODO: referenziarli e spostarli nella parte sulla libreria?
\begin{figure}[!ht]
\begin{center}
\includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-browsing}
projects / helm.git / commitdiff