From: Luca Padovani Date: Thu, 29 Sep 2005 07:07:13 +0000 (+0000) Subject: + well-formedness of level 1 patterns X-Git-Tag: V_0_7_2_3~283 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3d42df327558a73b38ace7bda97c9aef24adda14;p=helm.git + well-formedness of level 1 patterns + concrete syntax of level 1 patterns + level 1 terms --- diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex index 16b29bf8a..f79286f6d 100644 --- a/helm/ocaml/cic_notation/doc/main.tex +++ b/helm/ocaml/cic_notation/doc/main.tex @@ -1,10 +1,10 @@ \documentclass[a4paper]{article} +\usepackage{a4wide} \usepackage{pifont} \usepackage{semantic} -\newcommand{\MATITA}{\ding{46}\textsf{Matita}} - +\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}} \title{Extensible notation for \MATITA} \author{Luca Padovani \qquad Stefano Zacchiroli \\ @@ -16,6 +16,10 @@ \newcommand{\TVAR}[1]{#1:\mathtt{term}} \newcommand{\NVAR}[1]{#1:\mathtt{number}} \newcommand{\IVAR}[1]{#1:\mathtt{name}} +\newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}} +\newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^1} +\newcommand{\NAMES}{\mathit{names}} +\newcommand{\DOMAIN}{\mathit{domain}} \begin{document} \maketitle @@ -30,53 +34,127 @@ & | & \verb+Number+~n & \mbox{(number)} \\ & | & \verb+None+ & \mbox{(optional value)} \\ & | & \verb+Some+~V & \mbox{(optional value)} \\ - & | & [ V^{*} ] & \mbox{(list value)} \\[2ex] + & | & [V_1,\dots,V_n] & \mbox{(list value)} \\[2ex] \end{array} \] An environment is a map $\mathcal E : \mathit{Name} -> V$. -\section{Level 1: concrete syntax patterns} +\section{Level 1: concrete syntax} +\begin{table} +\caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut} +\hrule \[ \begin{array}{rcll} - P & ::= & & \mbox{(patterns)} \\ + P & ::= & & \mbox{(\bf patterns)} \\ & & S^{+} \\[2ex] S & ::= & & \mbox{(\bf simple patterns)} \\ - & & L_\kappa[S_1,\dots,S_n] & \mbox{(layout)} \\ - & | & B_\kappa^{ab}[P] & \mbox{(box)} \\ + & & l \\ + & | & S~\verb+\sub+~S\\ + & | & S~\verb+\sup+~S\\ + & | & S~\verb+\below+~S\\ + & | & S~\verb+\atop+~S\\ + & | & S~\verb+\over+~S\\ + & | & S~\verb+\atop+~S\\ + & | & \verb+\frac+~S~S \\ + & | & \verb+\sqrt+~S \\ + & | & \verb+\root+~S~\verb+\of+~S \\ + & | & \verb+(+~P~\verb+)+ \\ + & | & \verb+hbox (+~P~\verb+)+ \\ + & | & \verb+vbox (+~P~\verb+)+ \\ + & | & \verb+hvbox (+~P~\verb+)+ \\ + & | & \verb+hovbox (+~P~\verb+)+ \\ + & | & \verb+break+ \\ + & | & \verb+list0+~S~[\verb+sep+~l] \\ + & | & \verb+list1+~S~[\verb+sep+~l] \\ + & | & \verb+opt+~S \\ + & | & [\verb+term+]~x \\ + & | & \verb+number+~x \\ + & | & \verb+ident+~x \\ +\end{array} +\] +\hrule +\end{table} + +Rationale: while the layout schemata can occur in the concrete syntax +used by user, the box schemata and the magic patterns can only occur +when defining the notation. This is why the layout schemata are +``escaped'' with a backslash, so that they cannot be confused with +plain identifiers, wherease the others are not. Alternatively, they +could be defined as keywords, but this would prevent their names to be +used in different contexts. + +\begin{table} +\caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut} +\hrule +\[ +\begin{array}{@{}ll@{}} +\begin{array}[t]{rcll} + T & ::= & & \mbox{(\bf terms)} \\ + & & L_\kappa[T_1,\dots,T_n] & \mbox{(layout)} \\ + & | & B_\kappa^{ab}[T_1\cdots T_n] & \mbox{(box)} \\ + & | & \BREAK & \mbox{(breakpoint)} \\ + & | & \FENCED{T_1\cdots T_n} & \mbox{(fenced)} \\ + & | & l & \mbox{(literal)} \\[2ex] + P & ::= & & \mbox{(\bf patterns)} \\ + & & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\ + & | & B_\kappa^{ab}[P_1\cdots P_n] & \mbox{(box)} \\ & | & \BREAK & \mbox{(breakpoint)} \\ - & | & (P) & \mbox{(fenced)} \\ + & | & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\ & | & M & \mbox{(magic)} \\ & | & V & \mbox{(variable)} \\ - & | & l & \mbox{(literal)} \\[2ex] + & | & l & \mbox{(literal)} \\ +\end{array} & +\begin{array}[t]{rcll} V & ::= & & \mbox{(\bf variables)} \\ & & \TVAR{x} & \mbox{(term variable)} \\ & | & \NVAR{x} & \mbox{(number variable)} \\ & | & \IVAR{x} & \mbox{(name variable)} \\[2ex] M & ::= & & \mbox{(\bf magic patterns)} \\ - & & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\ - & | & \verb+list1+~S~l? & \mbox{(non-empty list)} \\ - & | & \verb+opt+~S & \mbox{(option)} \\[2ex] + & & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\ + & | & \verb+list1+~P~l? & \mbox{(non-empty list)} \\ + & | & \verb+opt+~P & \mbox{(option)} \\[2ex] +\end{array} \end{array} \] +\hrule +\end{table} -% IOT = Instantiate Two to One -\newcommand{\IOT}[2]{|[#1|]_{\mathcal{#2}}} -\newcommand{\NAMES}{\mathit{names}} +\[ +\IOT{\cdot}{{}} : P -> \mathit{Env} -> T +\] +\begin{table} +\caption{\label{tab:il1} Instantiation of level 1 patterns.\strut} +\hrule \[ \begin{array}{rcll} - \IOT{S_1\cdots S_n}{E} & = & \IOT{S_1}{E}\cdots\IOT{S_n}{E} \\ - \IOT{L_\kappa[S_1,\dots,S_n]}{E} & = & L_\kappa[\IOT{S_1}{E},\dots,\IOT{S_n}{E} ] \\ - \IOT{B_\kappa^{ab}[P]}{E} & = & B_\kappa^{ab}[\IOT{P}{E}] \\ + \IOT{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\IOT{P_1}{E},\dots,\IOT{P_n}{E} ] \\ + \IOT{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\ \IOT{\BREAK}{E} & = & \BREAK \\ - \IOT{(P)}{E} & = & (\IOT{P}{E}) \\ + \IOT{\FENCED{P_1\cdots P_n}}{E} & = & \FENCED{\IOT{P_1}{E}\cdots\IOT{P_n}{E}} \\ \IOT{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\ \IOT{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\ \IOT{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\ - \IOT{\mathtt{opt}~S}{E} & = & \varepsilon & \forall x \in \NAMES(S), \mathcal{E}(x) = \mathtt{None} \\ - \IOT{\mathtt{opt}~S}{E} & = & \varepsilon & \forall x \in \NAMES(S), \mathcal{E}(x) = \mathtt{None} \\ + \IOT{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\ + \IOT{\mathtt{opt}~P}{E} & = & \IOT{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\ + & & & \mathcal{E}'(x)=\left\{ + \begin{array}{@{}ll} + v, & \mathcal{E}(x) = \mathtt{Some}~v \\ + \mathcal{E}(x), & \mbox{otherwise} + \end{array} + \right. \\ + \IOT{\mathtt{list}k~P~l?}{E} & = & \IOT{P}{{E}_1}~{l?}\cdots {l?}~\IOT{P}{{E}_n} & + \mathcal{E}(\NAMES(P)) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\ + & & & n\ge k \\ + & & & \mathcal{E}_i(x) = \left\{ + \begin{array}{@{}ll} + v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\ + \mathcal{E}(x), & \mbox{otherwise} + \end{array} + \right. \\ + \IOT{l}{E} & = & l \\ %% & | & (P) & \mbox{(fenced)} \\ %% & | & M & \mbox{(magic)} \\ @@ -92,6 +170,62 @@ An environment is a map $\mathcal E : \mathit{Name} -> V$. %% & | & \verb+opt+~S & \mbox{(option)} \\[2ex] \end{array} \] +\hrule +\end{table} + +\begin{table} +\caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut} +\hrule +\[ +\renewcommand{\arraystretch}{3.5} +\begin{array}[t]{@{}c@{}} + \inference[\sc layout] + {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset} + {L_\kappa[P_1,\dots,P_n] :: D_1\oplus\cdots\oplus D_n} + \\ + \inference[\sc box] + {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset} + {B_\kappa^{ab}[P_1\cdots P_n] :: D_1\oplus\cdots\oplus D_n} + \\ + \inference[\sc fenced] + {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset} + {\FENCED{P_1\cdots P_n} :: D_1\oplus\cdots\oplus D_n} + \\ + \inference[\sc breakpoint] + {} + {\BREAK :: \emptyset} + \qquad + \inference[\sc literal] + {} + {l} + \qquad + \inference[\sc tvar] + {} + {\TVAR{x} :: \TVAR{x}} + \\ + \inference[\sc nvar] + {} + {\NVAR{x} :: \NVAR{x}} + \qquad + \inference[\sc ivar] + {} + {\IVAR{x} :: \IVAR{x}} + \\ + \inference[\sc list0] + {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}} + {\mathtt{list0}~P~l? :: D'} + \\ + \inference[\sc list1] + {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}} + {\mathtt{list1}~P~l? :: D'} + \\ + \inference[\sc opt] + {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}} + {\mathtt{opt}~P :: D'} +\end{array} +\] +\hrule +\end{table} \section{Level 2: abstract syntax}