X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fdoc%2Fmain.tex;h=36d35026c309c511212cb85e59404038e3c549a5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f47350553d8cdf5025e53b3c24dec8f637a7e4dc;hpb=4a6b34934452db18cf3c1fa6e87c71c9f02d256b;p=helm.git diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex index f47350553..36d35026c 100644 --- a/helm/ocaml/cic_notation/doc/main.tex +++ b/helm/ocaml/cic_notation/doc/main.tex @@ -1,9 +1,12 @@ -\documentclass[a4paper]{article} +\documentclass[a4paper,draft]{article} +\usepackage{manfnt} \usepackage{a4wide} \usepackage{pifont} \usepackage{semantic} -\usepackage{stmaryrd} +\usepackage{stmaryrd,latexsym} + +\newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}} \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}} @@ -15,275 +18,26 @@ \newcommand{\BREAK}{\mathtt{break}} \newcommand{\TVAR}[1]{#1:\mathtt{term}} +\newcommand{\IMPVAR}{\TVAR{\_}} \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{\ITO}[2]{|[#1|]_{\mathcal#2}^1} +\newcommand{\IOT}[2]{|[#1|]_{#2}^2} +\newcommand{\IAP}[2]{|[#1|]_{#2}^a} +\newcommand{\IAPP}[3]{|[#1|]_{#2,#3}^a} \newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}} \newcommand{\NAMES}{\mathit{names}} \newcommand{\DOMAIN}{\mathit{domain}} +\newcommand{\UPDATE}[2]{#1[#2]} + +\mathlig{~>}{\leadsto} +\mathlig{|->}{\mapsto} \begin{document} \maketitle -\section{Environment} - -\[ -\begin{array}{rcll} - V & ::= & & \mbox{(\bf values)} \\ - & & \verb+Term+~T & \mbox{(term)} \\ - & | & \verb+String+~s & \mbox{(string)} \\ - & | & \verb+Number+~n & \mbox{(number)} \\ - & | & \verb+None+ & \mbox{(optional value)} \\ - & | & \verb+Some+~V & \mbox{(optional value)} \\ - & | & [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} - -\begin{table} -\caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut} -\hrule -\[ -\begin{array}{rcll} - P & ::= & & \mbox{(\bf patterns)} \\ - & & S^{+} \\[2ex] - S & ::= & & \mbox{(\bf simple patterns)} \\ - & & 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)} \\ - & | & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\ - & | & M & \mbox{(magic)} \\ - & | & V & \mbox{(variable)} \\ - & | & 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+~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{\cdot}{{}} : P -> \mathit{Env} -> T -\] - -\begin{table} -\caption{\label{tab:il1} Instantiation of level 1 patterns.\strut} -\hrule -\[ -\begin{array}{rcll} - \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_1\cdots P_n)}{E} & = & B_H^{00}[\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}~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)} \\ -%% & | & V & \mbox{(variable)} \\ -%% & | & l & \mbox{(literal)} \\[2ex] -%% 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] -\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 :: \emptyset} - \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} - -\newcommand{\ATTRS}[1]{\langle#1\rangle} -\newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}} - -\begin{table} -\caption{\label{tab:addparens} Where are parentheses added? Look here.\strut} -\hrule -\[ -\begin{array}{rcll} - \ADDPARENS{l}{n} & = & l \\ - \ADDPARENS{\BREAK}{n} & = & \BREAK \\ - \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \ADDPARENS{T}{m} & n < m \\ - \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} & n > m \\ - \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=L,\mathit{pos}=R}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\ - \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=R,\mathit{pos}=L}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\ - \ADDPARENS{\ATTRS{\cdots}T}{n} & = & \ADDPARENS{T}{n} \\ - \ADDPARENS{L_\kappa[T_1,\dots,\underline{T_k},\dots,T_m]}{n} & = & L_\kappa[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_k}{\bot},\dots,\ADDPARENS{T_m}{n}] \\ - \ADDPARENS{B_\kappa^{ab}[T_1,\dots,T_m]}{n} & = & B_\kappa^{ab}[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_m}{n}] -\end{array} -\] -\hrule -\end{table} - -\begin{table} -\caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut} -\hrule -\[ -\begin{array}{rcll} - \ANNPOS{l}{p,q} & = & l \\ - \ANNPOS{\BREAK}{p,q} & = & \BREAK \\ - \ANNPOS{x}{1,0} & = & \ATTRS{\mathit{pos}=L}{x} \\ - \ANNPOS{x}{0,1} & = & \ATTRS{\mathit{pos}=R}{x} \\ - \ANNPOS{x}{p,q} & = & \ATTRS{\mathit{pos}=I}{x} \\ - \ANNPOS{B_\kappa^{ab}[P]}{p,q} & = & B_\kappa^{ab}[\ANNPOS{P}{p,q}] \\ - \ANNPOS{B_\kappa^{ab}[\{\BREAK\} P_1\cdots P_n\{\BREAK\}]}{p,q} & = & B_\kappa^{ab}[\begin{array}[t]{@{}l} - \{\BREAK\} \ANNPOS{P_1}{p,0} \\ - \ANNPOS{P_2}{0,0}\cdots\ANNPOS{P_{n-1}}{0,0} \\ - \ANNPOS{P_n}{0,q}\{\BREAK\}] - \end{array} - -%% & & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\ -%% & | & \BREAK & \mbox{(breakpoint)} \\ -%% & | & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\ -%% 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+~P~l? & \mbox{(possibly empty list)} \\ -%% & | & \verb+list1+~P~l? & \mbox{(non-empty list)} \\ -%% & | & \verb+opt+~P & \mbox{(option)} \\[2ex] -\end{array} -\] -\hrule -\end{table} + \input{body} -\section{Level 2: abstract syntax} +\end{document} -\end{document} \ No newline at end of file