From: Luca Padovani <luca.padovani@unito.it>
Date: Sat, 1 Oct 2005 06:36:25 +0000 (+0000)
Subject: * added pattern matching of level 2 terms
X-Git-Tag: V_0_7_2_3~269
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e74df6c2543bdb6938d51f1852f7485716005dc;p=helm.git

* added pattern matching of level 2 terms
---

diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex
index f27cebdd6..2e7c27853 100644
--- a/helm/ocaml/cic_notation/doc/main.tex
+++ b/helm/ocaml/cic_notation/doc/main.tex
@@ -4,7 +4,7 @@
 \usepackage{a4wide}
 \usepackage{pifont}
 \usepackage{semantic}
-\usepackage{stmaryrd}
+\usepackage{stmaryrd,latexsym}
 
 \newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}
 
@@ -26,6 +26,9 @@
 \newcommand{\NAMES}{\mathit{names}}
 \newcommand{\DOMAIN}{\mathit{domain}}
 
+\mathlig{~>}{\leadsto}
+\mathlig{|->}{\mapsto}
+
 \begin{document}
   \maketitle
 
@@ -345,4 +348,90 @@ used in different contexts.
 \]
 \end{table}
 
+\begin{table}
+\caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+  \inference[\sc Constr]
+    {t_i \in P_i ~> \mathcal E_i & i\ne j => \DOMAIN(\mathcal E_i)\cap\DOMAIN(\mathcal E_j)=\emptyset}
+    {C[t_1,\dots,t_n] \in C[P_1,\dots,P_n] ~> \mathcal E_1 \oplus \cdots \oplus \mathcal E_n}
+  \\
+  \inference[\sc TermVar]
+    {}
+    {t \in [\mathtt{term}]~x ~> [x |-> \mathtt{Term}~t]}
+  \quad
+  \inference[\sc NumVar]
+    {}
+    {n \in \mathtt{number}~x ~> [x |-> \mathtt{Number}~n]}
+  \\
+  \inference[\sc IdentVar]
+    {}
+    {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
+  \quad
+  \inference[\sc Success]
+    {}
+    {t \in \mathtt{anonymous} ~> \emptyset}
+  \\
+  \inference[\sc DefaultT]
+    {t \in P_1 ~> \mathcal E}
+    {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
+    \quad
+    \mathcal E'(x) = \left\{
+    \renewcommand{\arraystretch}{1}
+    \begin{array}{ll}
+      \mathtt{Some}~\mathcal{E}(x) & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
+      \mathcal{E}(x) & \mbox{otherwise}
+    \end{array}
+    \right.
+  \\
+  \inference[\sc DefaultF]
+    {t \not\in P_1 & t \in P_2 ~> \mathcal E}
+    {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
+    \quad
+    \mathcal E'(x) = \left\{
+    \renewcommand{\arraystretch}{1}
+    \begin{array}{ll}
+      \mathtt{None} & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
+      \mathcal{E}(x) & \mbox{otherwise}
+    \end{array}
+    \right.
+  \\
+  \inference[\sc IfT]
+    {t \in P_1 ~> \mathcal E' & t \in P_2 ~> \mathcal E}
+    {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
+  \quad
+  \inference[\sc IfF]
+    {t \not\in P_1 & t \in P_3 ~> \mathcal E}
+    {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
+  \\
+  \inference[\sc FoldR]
+    {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
+    {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
+  \quad
+  \mathcal E''(y) = \left\{
+    \renewcommand{\arraystretch}{1}
+    \begin{array}{ll}
+      \mathcal{E}(y)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \\
+      \mathcal{E}'(y) & \mbox{otherwise}
+    \end{array}  
+  \right.
+  \\
+  \inference[\sc FoldB]
+    {t \not\in P_2 & t \in P_1 ~> \mathcal E}
+    {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
+  \quad
+  \mathcal E'(y) = \left\{
+    \renewcommand{\arraystretch}{1}
+    \begin{array}{ll}
+      [] & y \in \NAMES(P_2) \setminus \{x\} \\
+      \mathcal{E}(y) & \mbox{otherwise}
+    \end{array}  
+  \right.
+\end{array}
+\]
+\hrule
+\end{table}
+
 \end{document}
\ No newline at end of file