* added well-formedness rules for level 2 patterns

diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex
index 2e7c2785373e3dce3e7a529596407d603d8df30c..2b6f10b55465df74a07598c9120a7843f962bdf3 100644 (file)
--- a/helm/ocaml/cic_notation/doc/main.tex
+++ b/helm/ocaml/cic_notation/doc/main.tex
@@ -298,43 +298,43 @@ used in different contexts.
 \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)} \\
+  \NT{term} & ::= & & \mbox{\bf terms} \\
+    &     & x & \mbox{(identifier)} \\
     &  |  & n & \mbox{(number)} \\
+    &  |  & \mathrm{URI} & \mbox{(URI)} \\
     &  |  & \verb+?+ & \mbox{(implicit)} \\
     &  |  & \verb+%+ & \mbox{(placeholder)} \\
     &  |  & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
+    &  |  & \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)} \\
     &  |  & \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)} \\
+    &  |  & \BLOB(\NT{meta},\dots,\NT{meta}) & \mbox{(meta blob)} \\
+  \NT{defs}  & ::= & & \mbox{\bf mutual definitions} \\
     &     & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
-  \NT{fun} & ::= & & \mbox{(\bf function)} \\
+  \NT{fun} & ::= & & \mbox{\bf functions} \\
     &     & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
-  \NT{binder} & ::= & & \mbox{(\bf binders)} \\
+  \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} & ::= & & \mbox{\bf single argument} \\
+    &     & \verb+_+ \mid x \mid \BLOB(\NT{meta},\dots,\NT{meta}) \\
+  \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
     &     & \NT{arg} \\
     &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
-  \NT{ptnames} & ::= & & \mbox{(\bf bound variables)} \\
+  \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
     &     & \NT{arg} \\
     &  |  & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
-  \NT{kind} & ::= & & \mbox{(\bf induction kind)} \\
+  \NT{kind} & ::= & & \mbox{\bf induction kind} \\
     &     & \verb+rec+ \mid \verb+corec+ \\
-  \NT{rule} & ::= & & \mbox{(\bf rules)} \\
+  \NT{rule} & ::= & & \mbox{\bf rules} \\
     &     & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]
 
-  \NT{meta} & ::= & & \mbox{(\bf meta)} \\
-    &     & \BLOB \\
+  \NT{meta} & ::= & & \mbox{\bf meta} \\
+    &     & \BLOB(\NT{term},\dots,\NT{term}) & (term blob) \\
     &  |  & [\verb+term+]~x \\
     &  |  & \verb+number+~x \\
     &  |  & \verb+ident+~x \\
@@ -348,6 +348,57 @@ used in different contexts.
 \]
 \end{table}
 
+\begin{table}
+\caption{\label{tab:wfl2} Well-formedness rules for level 2 patterns.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+  \inference[\sc Constr]
+    {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
+    {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\
+  \inference[\sc TermVar]
+    {}
+    {[\mathtt{term}]~x :: x : \mathtt{Term}}
+  \quad
+  \inference[\sc NumVar]
+    {}
+    {\mathtt{number}~x :: x : \mathtt{Number}}
+  \\
+  \inference[\sc IdentVar]
+    {}
+    {\mathtt{ident}~x :: x : \mathtt{String}}
+  \quad
+  \inference[\sc FreshVar]
+    {}
+    {\mathtt{fresh}~x :: x : \mathtt{String}}
+  \\
+  \inference[\sc Success]
+    {}
+    {\mathtt{anonymous} :: \emptyset}
+  \\
+  \inference[\sc Fold]
+    {P_1 :: D_1 & P_2 :: D_2 \oplus (x : \mathtt{Term}) & \DOMAIN(D_2)\ne\emptyset & \DOMAIN(D_1)\cap\DOMAIN(D_2)=\emptyset}
+    {\mathtt{fold}~P_1~\mathtt{rec}~x~P_2 :: D_1 \oplus D_2~\mathtt{List}}
+  \\
+  \inference[\sc Default]
+    {P_1 :: D \oplus D_1 & P_2 :: D & \DOMAIN(D_1) \ne \emptyset & \DOMAIN(D) \cap \DOMAIN(D_1) = \emptyset}
+    {\mathtt{default}~P_1~P_2 :: D \oplus D_1~\mathtt{Option}}
+  \\
+  \inference[\sc If]
+    {P_1 :: \emptyset & P_2 :: D & P_3 :: D }
+    {\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 :: D}
+  \qquad
+  \inference[\sc Fail]
+    {}
+    {\mathtt{fail} : \emptyset}
+%%     &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
+%%     &  |  & \verb+fail+ 
+\end{array}
+\]
+\hrule
+\end{table}
+
 \begin{table}
 \caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
 \hrule
@@ -370,6 +421,10 @@ used in different contexts.
     {}
     {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
   \quad
+  \inference[\sc FreshVar]
+    {}
+    {x \in \mathtt{fresh}~x ~> [x |-> \mathtt{String}~x]}
+  \\
   \inference[\sc Success]
     {}
     {t \in \mathtt{anonymous} ~> \emptyset}