\documentclass[a4paper]{article}

\usepackage{pifont}
\usepackage{semantic}

\newcommand{\MATITA}{\ding{46}\textsf{Matita}}


\title{Extensible notation for \MATITA}
\author{Luca Padovani \qquad Stefano Zacchiroli \\
\small Department of Computer Science, University of Bologna \\
\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
\small \{\texttt{lpadovan}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}

\newcommand{\BREAK}{\mathtt{break}}
\newcommand{\TVAR}[1]{#1:\mathtt{term}}
\newcommand{\NVAR}[1]{#1:\mathtt{number}}
\newcommand{\IVAR}[1]{#1:\mathtt{name}}

\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}
\]

  \section{Level 2: abstract syntax}

\end{document}