doc minicoq (grammaires)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@48 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 103 insertions, 0 deletions

diff --git a/doc/Makefile b/doc/Makefile
index b8bad1995..65ce899ca 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -1,6 +1,8 @@
 
 # Makefile for doc/
 
+all: minicoq.dvi
+
 coq.dvi: coq.tex
 	latex coq && latex coq
 
@@ -9,5 +11,8 @@ clean::
 
 .SUFFIXES: .tex .dvi .ps
 
+.tex.dvi:
+	latex $< && latex $<
+
 .dvi.ps:
 	dvips $< -o
diff --git a/doc/minicoq.tex b/doc/minicoq.tex
new file mode 100644
index 000000000..a34b03a49
--- /dev/null
+++ b/doc/minicoq.tex
@@ -0,0 +1,98 @@
+\documentclass{article}
+
+\usepackage{fullpage}
+\input{./macros.tex}
+\newcommand{\minicoq}{\textsf{minicoq}}
+\newcommand{\nonterm}[1]{\textit{#1}}
+\newcommand{\terminal}[1]{\textsf{#1}}
+\newcommand{\listzero}{\textit{LIST$_0$}}
+\newcommand{\listun}{\textit{LIST$_1$}}
+\newcommand{\sep}{\textit{SEP}}
+
+\title{Minicoq: a type-checker for the pure \\ 
+       Calculus of Inductive Constructions}
+
+
+\begin{document}
+
+\maketitle
+
+\section{Introduction}
+
+\minicoq\ is a minimal toplevel for the \Coq\ kernel.
+
+
+\section{Grammar of terms}
+
+The grammar of \minicoq's terms is given in Figure~\ref{fig:terms}. 
+
+\begin{figure}[htbp]
+  \hrulefill
+  \begin{center}
+    \begin{tabular}{lrl}
+      term & ::= & identifier \\
+           & $|$ & \terminal{Rel} integer \\
+           & $|$ & \terminal{Set} \\
+           & $|$ & \terminal{Prop} \\
+           & $|$ & \terminal{Type} \\
+           & $|$ & \terminal{Const} identifier \\
+           & $|$ & \terminal{Ind} identifier integer \\
+           & $|$ & \terminal{Construct} identifier integer integer \\
+           & $|$ & \terminal{[} name \terminal{:} term
+                   \terminal{]} term \\
+           & $|$ & \terminal{(} name \terminal{:} term
+                   \terminal{)} term \\
+           & $|$ & term \verb!->! term \\
+           & $|$ & \terminal{(} \listun\ term \terminal{)} \\
+           & $|$ & \terminal{(} term \terminal{::} term \terminal{)} \\
+           & $|$ & \verb!<! term \verb!>! \terminal{Case}
+                   term \terminal{of} \listzero\ term \terminal{end} 
+      \\[1em]
+      name & ::= & \verb!_! \\
+           & $|$ & identifier 
+   \end{tabular}
+  \end{center}
+  \hrulefill
+  \caption{Grammar of terms}
+  \label{fig:terms}
+\end{figure}
+
+\section{Commands}
+The grammar of \minicoq's commands are given in
+Figure~\ref{fig:commands}. All commands end with a dot.
+
+\begin{figure}[htbp]
+  \hrulefill
+  \begin{center}
+    \begin{tabular}{lrl}
+      command & ::= & \terminal{Definition} identifier \terminal{:=} term. \\
+              & $|$ & \terminal{Definition} identifier \terminal{:} term
+                      \terminal{:=} term. \\
+              & $|$ & \terminal{Parameter} identifier \terminal{:} term. \\
+              & $|$ & \terminal{Variable} identifier \terminal{:} term. \\
+              & $|$ & \terminal{Inductive} \terminal{[} \listzero\ param 
+                      \terminal{]} \listun\ inductive \sep\ 
+                      \terminal{with}. \\
+              & $|$ & \terminal{Check} term. 
+      \\[1em]
+      param   & ::= & identifier 
+      \\[1em]
+      inductive & ::= & identifier \terminal{:} term \terminal{:=}
+                        \listzero\ constructor \sep\ \terminal{$|$}
+      \\[1em]
+      constructor & ::= & identifier \terminal{:} term
+    \end{tabular}
+  \end{center}
+  \hrulefill
+  \caption{Commands}
+  \label{fig:commands}
+\end{figure}
+
+
+\end{document}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: