X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fdoc%2Fmain.tex;h=36d35026c309c511212cb85e59404038e3c549a5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=16b29bf8a30796a42f96de356ff036292e803a99;hpb=2d9b039d9b2f1f20fae18e577306ead3b5d2090d;p=helm.git

diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex
index 16b29bf8a..36d35026c 100644
--- a/helm/ocaml/cic_notation/doc/main.tex
+++ b/helm/ocaml/cic_notation/doc/main.tex
@@ -1,10 +1,14 @@
-\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 \\
@@ -14,85 +18,26 @@
 
 \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