From: Luca Padovani 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