\newcommand{\components}{components}
\newcommand{\AUTO}{\textsc{Auto}}
+\newcommand{\BOXML}{BoxML}
\newcommand{\COQ}{Coq}
\newcommand{\COQIDE}{CoqIde}
\newcommand{\ELIM}{\textsc{Elim}}
\newcommand{\GDOME}{Gdome}
+\newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
\newcommand{\IN}{\ensuremath{\dN}}
\newcommand{\LIBXSLT}{LibXSLT}
\newcommand{\LOCATE}{\textsc{Locate}}
\newcommand{\MATCH}{\textsc{Match}}
+\newcommand{\MATHML}{MathML}
\newcommand{\MATITA}{Matita}
\newcommand{\MATITAC}{\texttt{matitac}}
\newcommand{\MATITADEP}{\texttt{matitadep}}
\newcommand{\URI}[1]{\texttt{#1}}
\newcommand{\OP}[1]{``\texttt{#1}''}
-%{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
\newenvironment{grafite}{\VerbatimEnvironment
\begin{SaveVerbatim}{boxtmp}}%
{\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
{}
\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
\newcommand{\FILE}[1]{\texttt{#1}}
-% \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}}
-\newcommand{\NOTE}[1]{\ednote{#1}{foo}}
+\newcommand{\NOTE}[1]{\ednote{#1}{}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
\newcounter{pass}
%search engine, described in~\cite{whelp};
\item developing languages and tools for a high-quality notational
rendering of mathematical information\footnote{We have been
-active in the MathML Working group since 1999.};
+active in the \MATHML{} Working group since 1999.};
%and developed inside
-%\HELM{} a MathML-compliant widget for the GTK graphical environment
+%\HELM{} a \MATHML-compliant widget for the GTK graphical environment
%which can be integrated in any application.
\end{itemize}
partially specified terms, used by the disambiguating parser;
\item complex transformation algorithms for proof rendering in natural
language \cite{remathematization};
-\item an innovative, MathML-compliant rendering widget for the GTK
+\item an innovative, \MATHML-compliant rendering widget for the GTK
graphical environment\cite{padovani}, supporting
high-quality bidimensional
rendering, and semantic selection, i.e. the possibility to select semantically
\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
split in two main windows: on the left a textual widget is used to edit the
-script, on the right the list of open goal is shown using a MathML rendering
+script, on the right the list of open goal is shown using a \MATHML{} rendering
widget. A distinguished part of the script (shaded in the screenshot) represent
the commands already executed and can't be edited without undoing them. The
remaining part can be freely edited and commands from that part can be executed
%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
%organized in components which work on data in this format. For instance the
%rendering engine, which transform $\lambda$-terms encoded as XML document to
-%MathML Presentation documents, can be used apart from \MATITA{} to print ...
+%\MATHML{} Presentation documents, can be used apart from \MATITA{} to print ...
%FINIRE
A final section is devoted to some innovative aspects
formulae. The firsts are translated to a content level representation of
proof steps that can easily be rendered in natural language. The representation
adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now
-isomorphic to it. Terms that represent formulae are translated to MathML
-Content formulae. MathML Content~\cite{mathml} is a W3C standard
+isomorphic to it. Terms that represent formulae are translated to \MATHML{}
+Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard
for the representation of content level formulae in an XML extensible format.
The translation to content level is implemented in the
single day, but they stick to a set of symbols that is more or less fixed.
The fact that the presentation language is finite allows the definition of
-standard languages. In particular, for formulae we have adopt MathML
+standard languages. In particular, for formulae we have adopt \MATHML{}
Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To
visually
represent proofs it is enough to embed formulae in plain text enriched with
formatting boxes. Since the language of formatting boxes is very simple,
many equivalent specifications exist and we have adopted our own, called
-BoxML.
+\BOXML.
The \texttt{content\_pres} \component{} contains the implementation of the
translation from content level terms to presentation level terms. The
rendering of presentation level terms is left to the application that uses
the \component. However, in the \texttt{hgdome} \component{} we provide a few
-utility functions to build a \GDOME~\cite{gdome2} MathML+BoxML tree from our
+utility functions to build a \GDOME~\cite{gdome2} \MATHML+\BOXML{} tree from our
presentation
-level terms. \GDOME{} MathML+BoxML trees can be rendered by the GtkMathView
+level terms. \GDOME{} \MATHML+\BOXML{} trees can be rendered by the
+\GTKMATHVIEW{}
widget developed by Luca Padovani \cite{padovani}. The widget is
particularly interesting since it allows to implement \emph{semantic
selection}.
\subsection{Patterns}
+\subsubsection{Direct manipulation of terms}
+
+While terms are input as \TeX-like formulae in \MATITA, they're converted to a
+mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
+\GTKMATHVIEW. This mixed choice~\cite{latexmathml} enables both high-quality
+bidimensional rendering of terms (including the use of fancy layout schemata
+like radicals and matrices~\cite{mathml}) and the use of a concise and
+widespread textual syntax.
+
\begin{figure}[t]
\begin{center}
\includegraphics[width=0.40\textwidth]{matita-screenshot-selection}
\hspace{0.05\textwidth}
\raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{matita-screenshot-href}}
\caption{Semantic selection and hyperlinks}
- \label{fig:semselection}
+ \label{fig:directmanip}
\end{center}
\end{figure}
-serve una intro che almeno cita il widget (per i patterns) e che fa
-il resoconto delle cose che abbiamo e che non descriviamo,
-sottolineando che abbiamo qualcosa da dire sui pattern e sui
-tattichini.\\
-
-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.
+Keeping pointers from the presentations level terms down to the partially
+specified ones \MATITA{} enable direct manipulation of rendered (sub)terms in
+the form of hyperlinks and semantic selection. \emph{Hyperlinks} have anchors on
+the occurrences of constant and inductive type constructors and point to the
+corresponding definitions in the library. Anchors are available notwithstanding
+the use of user-defined mathematical notation: as can be seen on the right of
+Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols encoding
+complex notations retain all the hyperlinks of constants or constructors used in
+the notation.
+
+\emph{Semantic selection} enable the selection of mixed \MATHML+\BOXML{} markup,
+constraining the selection to markup representing meaningful CIC (sub)terms. In
+the example on the left of Fig.~\ref{fig:directmanip} is thus possible to select
+the subterm $\mathrm{prime}~n$, whereas it would not be possible to select
+$\forall~n:nat$ since the former denotes an application while the latter denotes
+an incomplete $\Pi$-binder. Once a (sub)term has been selected that way actions
+can be done on it like reductions or tactic applications.
+
+In our experience working with direct manipulation of terms is really effective
+and faster than retyping them. Nonetheless we need a way to encode term
+selections in scripts so that they can be batch compiled by \MATITAC. In
+\MATITA{} \emph{patterns} implement that encoding, being patterns the textual
+representations of \GTKMATHVIEW semantic selections.\NOTE{Zack:c'\`e scritto da
+qualche parte che l'utente non li deve necessariamente scrivere a mano, ma che
+pu\`o incollarli? Va scritto.}
\subsubsection{Pattern syntax}
A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
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}
+ \caption{\label{tab:pathsyn} Patterns concrete syntax.\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}
+% \]
\[
\begin{array}{@{}rcll@{}}
\NT{pattern} &
- ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
+ ::= & [~\verb+in+~\NT{sequent\_path}~]~[~\verb+match+~\NT{wanted}~] & \\
\NT{sequent\_path} &
::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
[~\verb+\vdash+~\NT{multipath}~] & \\
- \NT{wanted} & ::= & \NT{term} & \\
\NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
+ \NT{wanted} & ::= & \NT{term} & \\
\end{array}
\]
\hrule
\end{table}
-\subsubsection{How patterns work}
+\subsubsection{Pattern concepts}
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
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}~]$
+ plays a role only if the $[~\verb+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
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).
+ change in H match n with (O + n).
\end{grafite}
\noindent
In this case the $\NT{sequent\_path}$ selects the whole $H$, while
projects / helm.git / commitdiff