-\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}}}
\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
projects / helm.git / blobdiff