* first version of the specification

diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex
new file mode 100644 (file)
index 0000000..16b29bf
--- /dev/null
+++ b/helm/ocaml/cic_notation/doc/main.tex
@@ -0,0 +1,98 @@
+\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}
\ No newline at end of file