From: Claudio Sacerdoti Coen Date: Wed, 18 Jan 2006 16:06:50 +0000 (+0000) Subject: Aggiornato alla nuova gerarchia di moduli. X-Git-Tag: make_still_working~7813 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=768514ae739c7b9a8c5a89a3684496912d1ced05;p=helm.git Aggiornato alla nuova gerarchia di moduli. --- diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 7c8e2fa45..94e21bb19 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -401,6 +401,15 @@ content level terms; presentation level terms. 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 @@ -432,9 +441,16 @@ prove. \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 @@ -496,16 +512,18 @@ two different positions we need to associate different typing informations. 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 @@ -547,7 +565,9 @@ Semantic selection is a technique that consists in enriching the presentation 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 @@ -563,17 +583,40 @@ parsing tool we have adopted (CamlP4) is not able to parse ambiguous 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. @@ -583,22 +626,13 @@ it to the presentation level passing through the content level. Finally 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 ---