From 18829d4879446f929af6d4be9e5b13b2ca00ddd8 Mon Sep 17 00:00:00 2001 From: Luca Padovani Date: Sun, 2 Oct 2005 07:54:42 +0000 Subject: [PATCH] * added well-formedness rules for level 2 patterns --- helm/ocaml/cic_notation/doc/main.tex | 93 ++++++++++++++++++++++------ 1 file changed, 74 insertions(+), 19 deletions(-) diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex index 2e7c27853..2b6f10b55 100644 --- 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} -- 2.39.2