The Whelp search engine is the Web service that provides an interface to
the \texttt{whelp} \component.
+ According to our vision, the library is developed collaboratively so that
+ changing or removing a notion can invalidate other notions in the library.
+ Moreover, changing or removing a notion requires a corresponding change
+ in the metadata database. The \texttt{library} \component{} is responsible
+ of preserving the coherence of the library and the database. For instance,
+ when a notion is removed, all the notions that depend on it and their
+ metadata are removed from the library. This aspect will be better detailed
+ in Sect.~\ref{decompilazione}.
+
\subsection{Partially specified terms}
\emph{Partially specified terms} are CIC terms where subterms can be omitted.
Omitted subterms can bear no information at all or they may be associated to
\emph{Tactics} are the procedures that the user can apply to progress in the
proof. A tactic proves a conjecture possibly creating new (and hopefully
simpler) conjectures. The implementation of tactics is given in the
-\texttt{tactics} \component. It is heavily based on the refinement and unification
-procedures of the \texttt{cic\_unification} \component. \TODO{citare paramodulation
-da qualche part o toglierla dal grafo}
+\texttt{tactics} \component. It is heavily based on the refinement and
+unification procedures of the \texttt{cic\_unification} \component.
+
+The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the
+commands of the \MATITA{} proof assistant. Most of the commands are tactics.
+Other commands are used to give definitions and axioms or to state theorems
+and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}.
+It implements the semantics of each command in the grafite AST as a function
+from status to status. It implements also an undo function to go back to
+previous statuses. \TODO{parlare di disambiguazione lazy \& co?}
As fully specified terms, partially specified terms are not well suited
for user consumption since their syntax is not extendible and it is not
This association is made easier when the term is represented as a tree since
it is possible to label each node with an unique identifier and associate
the typing information using a map on the identifiers.
-The \texttt{cic\_acic} \component annotates partially specified terms.
+The \texttt{cic\_acic} \component{} unshares and annotates terms. It is used
+by the \texttt{library} \component{} since fully specified terms are stored
+in the library in their annotated form.
We do not provide yet a reverse translation from content level proofs to
-partially specified terms. But in \texttt{disambiguation} we do provide
+partially specified terms. But in \texttt{cic\_disambiguation} we do provide
the reverse translation for expressions. The mapping from
content level expressions to partially specified terms is not unique due to
the ambiguity of the content level. As a consequence the translation
is guided by an \emph{interpretation}, that is a function that chooses for
every ambiguous expression one partially specified term. The
-\texttt{disambiguation} \component{} contains the implementation of the
+\texttt{cic\_disambiguation} \component{} implements the
disambiguation algorithm we presented in~\cite{disambiguation} that is
responsible of building in an efficicent way the set of all ``correct''
interpretations. An interpretation is correct if the partially specified term
level terms with pointers to the content level terms and to the partially
specified terms they correspond to. Highlight of formulae in the widget is
constrained to selection of meaningful expressions, i.e. expressions that
-correspond to a lower\footnote{\TODO{non abbiamo parlato di ``ordine''}} level term. Once the rendering of a lower level term is
+correspond to a lower level term, that is a content term or a partially or
+fully specified term.
+Once the rendering of a lower level term is
selected it is possible for the application to retrieve the pointer to the
lower level term. An example of applications of semantic selection is
\emph{semantic cut\&paste}: the user can select an expression and paste it
grammars. Thus we require the mapping from presentation level terms
(concrete syntax) to content level terms (abstract syntax) to be unique.
This means that the user must fix once and for all the associativity and
-precedence level of every operator he is using. In prctice this limitation
+precedence level of every operator he is using. In practice this limitation
does not seem too strong. The reason is that the target of the
translation is an ambiguous language and the user is free to associate
to every content level term several different interpretations (as a
partially specified term).
+Both the direct and reverse translation from presentation to content level
+terms are parameterized over the user provided mathematical notation.
+The \texttt{lexicon} \component{} is responsible of managing the lexicon,
+that is the set of active notations. It defines an abstract syntax tree
+of commands to declare and activate new notations and it implements the
+semantics of these commands. It also implements undoing of the semantic
+actions. Among the commands there are hints to the
+disambiguation algorithm that are used to control and speed up disambiguation.
+These mechanisms will be further discussed in Sect.~\ref{disambiguazione}.
+
+Finally, the \texttt{grafite\_parser} \component{} implements a parser for
+the concrete syntax of the commands of \MATITA. The parser process a stream
+of characters and returns a stream of abstract syntax trees (the ones
+defined by the \texttt{grafite} component and whose semantics is given
+by \texttt{grafite\_engine}). When the parser meets a command that changes
+the lexicon, it invokes the \texttt{lexicon} \component{} to immediately
+process the command. When the parser needs to parse a term at the presentation
+level, it invokes the already described parser for terms contained in
+\texttt{content\_pres}.
+
The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
-against the \texttt{cic\_disambiguation} and \texttt{content\_pres} \components{}
+against the \texttt{grafite\_parser} \components{}
since they provide an interface to the user. In both cases the formulae
written by the user are parsed using the \texttt{content\_pres} \component{} and
then disambiguated using the \texttt{cic\_disambiguation} \component.
+However, only \MATITA{} is linked against the \texttt{grafite\_engine} and
+\texttt{tactics} components since \WHELP{} can only execute those ASTs that
+correspond to queries (implemented in the \texttt{whelp} component).
The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
providing a rendering service for the documents in the distributed library.
it returns the result document to be rendered by the user's
browser.\footnote{\TODO{manca la passata verso HTML}}
-\hrule
-
-At the bottom of the DAG we have a few \components{} (\texttt{extlib},
-\texttt{xml} and the \texttt{registry}) that provide a core of
-useful functions used everywhere else. In particular, the \texttt{xml} \component{}
-to easily represent, parse and pretty-print XML files is a central component
-since in HELM every piece of information is stored in \ldots. [FINIRE]
-The other basic \components{} provide often needed operations over generic
-data structures (\texttt{extlib}) and central storage for configuration options
-(the \texttt{registry}).
-
-\texttt{urimanager}
-
-\texttt{getter}
-\texttt{cic}
+The \components{} not yet described (\texttt{extlib}, \texttt{xml},
+\texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are
+minor \components{} that provide a core of useful functions and basic
+services missing from the standard library of the programming language.
+In particular, the \texttt{xml} \component{} is used
+to easily represent, parse and pretty-print XML files.
\section{Partially specified terms}
--- il mondo delle tattiche e dintorni ---
projects / helm.git / commitdiff