* added concrete syntax for level 2

diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex
index f47350553d8cdf5025e53b3c24dec8f637a7e4dc..f27cebdd6ce0e5274407471dda8784ee152f9285 100644 (file)
--- a/helm/ocaml/cic_notation/doc/main.tex
+++ b/helm/ocaml/cic_notation/doc/main.tex
@@ -1,10 +1,13 @@
 \documentclass[a4paper]{article}
 
+\usepackage{manfnt}
 \usepackage{a4wide}
 \usepackage{pifont}
 \usepackage{semantic}
 \usepackage{stmaryrd}
 
+\newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}
+
 \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
 
 \title{Extensible notation for \MATITA}
@@ -132,9 +135,10 @@ used in different contexts.
 \hrule
 \[
 \begin{array}{rcll}
-  \IOT{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\IOT{P_1}{E},\dots,\IOT{P_n}{E} ] \\
+  \IOT{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\IOT{(P_1)}{E},\dots,\IOT{(P_n)}{E} ] \\
   \IOT{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\
   \IOT{\BREAK}{E} & = & \BREAK \\
+  \IOT{(P)}{E} & = & \IOT{P}{E} \\
   \IOT{(P_1\cdots P_n)}{E} & = & B_H^{00}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\
   \IOT{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
   \IOT{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
@@ -286,4 +290,59 @@ used in different contexts.
 
 \section{Level 2: abstract syntax}
 
+\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
+
+\begin{table}
+\[
+\begin{array}{@{}rcll@{}}
+  \NT{term} & ::= & & \mbox{(\bf terms)} \\
+    &     & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
+    &  |  & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
+    &  |  & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
+    &  |  & \NT{term}~\NT{term} & \mbox{(application)} \\
+    &  |  & x & \mbox{(identifier)} \\
+    &  |  & \mathrm{URI} & \mbox{(URI)} \\
+    &  |  & n & \mbox{(number)} \\
+    &  |  & \verb+?+ & \mbox{(implicit)} \\
+    &  |  & \verb+%+ & \mbox{(placeholder)} \\
+    &  |  & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
+    &  |  & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
+    &  |  & [\verb+[+~\NT{term}~\verb+]+]~\verb+match+~\NT{term}~\verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \mbox{(pattern match)} \\
+    &  |  & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
+    &  |  & \verb+(+~\NT{term}~\verb+)+ \\
+    &  |  & \BLOB & \mbox{(blob)} \\
+  \NT{defs}  & ::= & & \mbox{(\bf mutual definitions)} \\
+    &     & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
+  \NT{fun} & ::= & & \mbox{(\bf function)} \\
+    &     & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
+  \NT{binder} & ::= & & \mbox{(\bf binders)} \\
+    &     & \verb+\Pi+ \mid \verb+\exists+ \mid \verb+\forall+ \mid \verb+\lambda+ \\
+  \NT{arg} & ::= & & \mbox{(\bf single argument)} \\
+    &     & \verb+_+ \mid x \mid \BLOB \\
+  \NT{ptname} & ::= & & \mbox{(\bf possibly typed name)} \\
+    &     & \NT{arg} \\
+    &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
+  \NT{ptnames} & ::= & & \mbox{(\bf bound variables)} \\
+    &     & \NT{arg} \\
+    &  |  & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
+  \NT{kind} & ::= & & \mbox{(\bf induction kind)} \\
+    &     & \verb+rec+ \mid \verb+corec+ \\
+  \NT{rule} & ::= & & \mbox{(\bf rules)} \\
+    &     & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]
+
+  \NT{meta} & ::= & & \mbox{(\bf meta)} \\
+    &     & \BLOB \\
+    &  |  & [\verb+term+]~x \\
+    &  |  & \verb+number+~x \\
+    &  |  & \verb+ident+~x \\
+    &  |  & \verb+fresh+~x \\
+    &  |  & \verb+anonymous+ \\
+    &  |  & \verb+fold+~[\verb+left+\mid\verb+right+]~\NT{meta}~\verb+rec+~x~\NT{meta} \\
+    &  |  & \verb+default+~\NT{meta}~\NT{meta} \\
+    &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
+    &  |  & \verb+fail+ 
+\end{array}
+\]
+\end{table}
+
 \end{document}
\ No newline at end of file