-\documentclass[a4paper]{article}
+\documentclass[a4paper,draft]{article}
+\usepackage{manfnt}
+\usepackage{a4wide}
\usepackage{pifont}
\usepackage{semantic}
+\usepackage{stmaryrd,latexsym}
-\newcommand{\MATITA}{\ding{46}\textsf{Matita}}
+\newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}
+\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
\title{Extensible notation for \MATITA}
\author{Luca Padovani \qquad Stefano Zacchiroli \\
\newcommand{\BREAK}{\mathtt{break}}
\newcommand{\TVAR}[1]{#1:\mathtt{term}}
+\newcommand{\IMPVAR}{\TVAR{\_}}
\newcommand{\NVAR}[1]{#1:\mathtt{number}}
\newcommand{\IVAR}[1]{#1:\mathtt{name}}
+\newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
+\newcommand{\ITO}[2]{|[#1|]_{\mathcal#2}^1}
+\newcommand{\IOT}[2]{|[#1|]_{#2}^2}
+\newcommand{\IAP}[2]{|[#1|]_{#2}^a}
+\newcommand{\IAPP}[3]{|[#1|]_{#2,#3}^a}
+\newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
+\newcommand{\NAMES}{\mathit{names}}
+\newcommand{\DOMAIN}{\mathit{domain}}
+\newcommand{\UPDATE}[2]{#1[#2]}
+
+\mathlig{~>}{\leadsto}
+\mathlig{|->}{\mapsto}
\begin{document}
\maketitle
-\section{Environment}
-
-\[
-\begin{array}{rcll}
- V & ::= & & \mbox{(\bf values)} \\
- & & \verb+Term+~T & \mbox{(term)} \\
- & | & \verb+String+~s & \mbox{(string)} \\
- & | & \verb+Number+~n & \mbox{(number)} \\
- & | & \verb+None+ & \mbox{(optional value)} \\
- & | & \verb+Some+~V & \mbox{(optional value)} \\
- & | & [ V^{*} ] & \mbox{(list value)} \\[2ex]
-\end{array}
-\]
-
-An environment is a map $\mathcal E : \mathit{Name} -> V$.
-
-\section{Level 1: concrete syntax patterns}
-
-\[
-\begin{array}{rcll}
- P & ::= & & \mbox{(patterns)} \\
- & & S^{+} \\[2ex]
- S & ::= & & \mbox{(\bf simple patterns)} \\
- & & L_\kappa[S_1,\dots,S_n] & \mbox{(layout)} \\
- & | & B_\kappa^{ab}[P] & \mbox{(box)} \\
- & | & \BREAK & \mbox{(breakpoint)} \\
- & | & (P) & \mbox{(fenced)} \\
- & | & M & \mbox{(magic)} \\
- & | & V & \mbox{(variable)} \\
- & | & l & \mbox{(literal)} \\[2ex]
- V & ::= & & \mbox{(\bf variables)} \\
- & & \TVAR{x} & \mbox{(term variable)} \\
- & | & \NVAR{x} & \mbox{(number variable)} \\
- & | & \IVAR{x} & \mbox{(name variable)} \\[2ex]
- M & ::= & & \mbox{(\bf magic patterns)} \\
- & & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
- & | & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
- & | & \verb+opt+~S & \mbox{(option)} \\[2ex]
-\end{array}
-\]
-
-% IOT = Instantiate Two to One
-\newcommand{\IOT}[2]{|[#1|]_{\mathcal{#2}}}
-\newcommand{\NAMES}{\mathit{names}}
-
-\[
-\begin{array}{rcll}
- \IOT{S_1\cdots S_n}{E} & = & \IOT{S_1}{E}\cdots\IOT{S_n}{E} \\
- \IOT{L_\kappa[S_1,\dots,S_n]}{E} & = & L_\kappa[\IOT{S_1}{E},\dots,\IOT{S_n}{E} ] \\
- \IOT{B_\kappa^{ab}[P]}{E} & = & B_\kappa^{ab}[\IOT{P}{E}] \\
- \IOT{\BREAK}{E} & = & \BREAK \\
- \IOT{(P)}{E} & = & (\IOT{P}{E}) \\
- \IOT{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
- \IOT{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
- \IOT{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
- \IOT{\mathtt{opt}~S}{E} & = & \varepsilon & \forall x \in \NAMES(S), \mathcal{E}(x) = \mathtt{None} \\
- \IOT{\mathtt{opt}~S}{E} & = & \varepsilon & \forall x \in \NAMES(S), \mathcal{E}(x) = \mathtt{None} \\
-
-%% & | & (P) & \mbox{(fenced)} \\
-%% & | & M & \mbox{(magic)} \\
-%% & | & V & \mbox{(variable)} \\
-%% & | & l & \mbox{(literal)} \\[2ex]
-%% V & ::= & & \mbox{(\bf variables)} \\
-%% & & \TVAR{x} & \mbox{(term variable)} \\
-%% & | & \NVAR{x} & \mbox{(number variable)} \\
-%% & | & \IVAR{x} & \mbox{(name variable)} \\[2ex]
-%% M & ::= & & \mbox{(\bf magic patterns)} \\
-%% & & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
-%% & | & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
-%% & | & \verb+opt+~S & \mbox{(option)} \\[2ex]
-\end{array}
-\]
+ \input{body}
- \section{Level 2: abstract syntax}
+\end{document}
-\end{document}
\ No newline at end of file