* snapshot

diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex
index f79286f6d519aa5e6ed695ed82634da0515ef501..f47350553d8cdf5025e53b3c24dec8f637a7e4dc 100644 (file)
--- a/helm/ocaml/cic_notation/doc/main.tex
+++ b/helm/ocaml/cic_notation/doc/main.tex
@@ -3,6 +3,7 @@
 \usepackage{a4wide}
 \usepackage{pifont}
 \usepackage{semantic}
+\usepackage{stmaryrd}
 
 \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
 
@@ -18,6 +19,7 @@
 \newcommand{\IVAR}[1]{#1:\mathtt{name}}
 \newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
 \newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^1}
+\newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
 \newcommand{\NAMES}{\mathit{names}}
 \newcommand{\DOMAIN}{\mathit{domain}}
 
@@ -133,7 +135,7 @@ used in different contexts.
   \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{\FENCED{P_1\cdots P_n}}{E} & = & \FENCED{\IOT{P_1}{E}\cdots\IOT{P_n}{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 \\
   \IOT{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
@@ -197,7 +199,7 @@ used in different contexts.
   \qquad
   \inference[\sc literal]
     {}
-    {l}
+    {l :: \emptyset}
   \qquad
   \inference[\sc tvar]
     {}
@@ -227,6 +229,61 @@ used in different contexts.
 \hrule
 \end{table}
 
-  \section{Level 2: abstract syntax}
+\newcommand{\ATTRS}[1]{\langle#1\rangle}
+\newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}}
+
+\begin{table}
+\caption{\label{tab:addparens} Where are parentheses added? Look here.\strut}
+\hrule
+\[
+\begin{array}{rcll}
+  \ADDPARENS{l}{n} & = & l \\
+  \ADDPARENS{\BREAK}{n} & = & \BREAK \\
+  \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \ADDPARENS{T}{m} & n < m \\
+  \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} & n > m \\
+  \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=L,\mathit{pos}=R}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
+  \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=R,\mathit{pos}=L}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
+  \ADDPARENS{\ATTRS{\cdots}T}{n} & = & \ADDPARENS{T}{n} \\
+  \ADDPARENS{L_\kappa[T_1,\dots,\underline{T_k},\dots,T_m]}{n} & = & L_\kappa[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_k}{\bot},\dots,\ADDPARENS{T_m}{n}] \\
+  \ADDPARENS{B_\kappa^{ab}[T_1,\dots,T_m]}{n} & = & B_\kappa^{ab}[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_m}{n}]
+\end{array}
+\]
+\hrule
+\end{table}
+
+\begin{table}
+\caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut}
+\hrule
+\[
+\begin{array}{rcll}
+  \ANNPOS{l}{p,q} & = & l \\
+  \ANNPOS{\BREAK}{p,q} & = & \BREAK \\
+  \ANNPOS{x}{1,0} & = & \ATTRS{\mathit{pos}=L}{x} \\
+  \ANNPOS{x}{0,1} & = & \ATTRS{\mathit{pos}=R}{x} \\
+  \ANNPOS{x}{p,q} & = & \ATTRS{\mathit{pos}=I}{x} \\
+  \ANNPOS{B_\kappa^{ab}[P]}{p,q} & = & B_\kappa^{ab}[\ANNPOS{P}{p,q}] \\
+  \ANNPOS{B_\kappa^{ab}[\{\BREAK\} P_1\cdots P_n\{\BREAK\}]}{p,q} & = & B_\kappa^{ab}[\begin{array}[t]{@{}l}
+      \{\BREAK\} \ANNPOS{P_1}{p,0} \\
+      \ANNPOS{P_2}{0,0}\cdots\ANNPOS{P_{n-1}}{0,0} \\
+      \ANNPOS{P_n}{0,q}\{\BREAK\}]
+  \end{array}
+
+%%     &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
+%%     &  |  & \BREAK & \mbox{(breakpoint)} \\
+%%     &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
+%%   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+~P~l? & \mbox{(possibly empty list)} \\
+%%     &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
+%%     &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
+\end{array}
+\]
+\hrule
+\end{table}
+
+\section{Level 2: abstract syntax}
 
 \end{document}
\ No newline at end of file