\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 \\
\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
& | & \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)} \\
%% & | & \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}
projects / helm.git / commitdiff