helm/ocaml/cic_notation/doc/main.tex

   1 \documentclass[a4paper]{article}
   2
   3 \usepackage{a4wide}
   4 \usepackage{pifont}
   5 \usepackage{semantic}
   6
   7 \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
   8
   9 \title{Extensible notation for \MATITA}
  10 \author{Luca Padovani \qquad Stefano Zacchiroli \\
  11 \small Department of Computer Science, University of Bologna \\
  12 \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
  13 \small \{\texttt{lpadovan}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
  14
  15 \newcommand{\BREAK}{\mathtt{break}}
  16 \newcommand{\TVAR}[1]{#1:\mathtt{term}}
  17 \newcommand{\NVAR}[1]{#1:\mathtt{number}}
  18 \newcommand{\IVAR}[1]{#1:\mathtt{name}}
  19 \newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
  20 \newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^1}
  21 \newcommand{\NAMES}{\mathit{names}}
  22 \newcommand{\DOMAIN}{\mathit{domain}}
  23
  24 \begin{document}
  25   \maketitle
  26
  27 \section{Environment}
  28
  29 \[
  30 \begin{array}{rcll}
  31   V & ::= & & \mbox{(\bf values)} \\
  32     &     & \verb+Term+~T & \mbox{(term)} \\
  33     &  |  & \verb+String+~s & \mbox{(string)} \\
  34     &  |  & \verb+Number+~n & \mbox{(number)} \\
  35     &  |  & \verb+None+ & \mbox{(optional value)} \\
  36     &  |  & \verb+Some+~V & \mbox{(optional value)} \\
  37     &  |  & [V_1,\dots,V_n] & \mbox{(list value)} \\[2ex]
  38 \end{array}
  39 \]
  40
  41 An environment is a map $\mathcal E : \mathit{Name} -> V$.
  42
  43 \section{Level 1: concrete syntax}
  44
  45 \begin{table}
  46 \caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut}
  47 \hrule
  48 \[
  49 \begin{array}{rcll}
  50   P & ::= & & \mbox{(\bf patterns)} \\
  51     &     & S^{+} \\[2ex]
  52   S & ::= & & \mbox{(\bf simple patterns)} \\
  53     &     & l \\
  54     &  |  & S~\verb+\sub+~S\\
  55     &  |  & S~\verb+\sup+~S\\
  56     &  |  & S~\verb+\below+~S\\
  57     &  |  & S~\verb+\atop+~S\\
  58     &  |  & S~\verb+\over+~S\\
  59     &  |  & S~\verb+\atop+~S\\
  60     &  |  & \verb+\frac+~S~S \\
  61     &  |  & \verb+\sqrt+~S \\
  62     &  |  & \verb+\root+~S~\verb+\of+~S \\
  63     &  |  & \verb+(+~P~\verb+)+ \\
  64     &  |  & \verb+hbox (+~P~\verb+)+ \\
  65     &  |  & \verb+vbox (+~P~\verb+)+ \\
  66     &  |  & \verb+hvbox (+~P~\verb+)+ \\
  67     &  |  & \verb+hovbox (+~P~\verb+)+ \\
  68     &  |  & \verb+break+ \\
  69     &  |  & \verb+list0+~S~[\verb+sep+~l] \\
  70     &  |  & \verb+list1+~S~[\verb+sep+~l] \\
  71     &  |  & \verb+opt+~S \\
  72     &  |  & [\verb+term+]~x \\
  73     &  |  & \verb+number+~x \\
  74     &  |  & \verb+ident+~x \\
  75 \end{array}
  76 \]
  77 \hrule
  78 \end{table}
  79
  80 Rationale: while the layout schemata can occur in the concrete syntax
  81 used by user, the box schemata and the magic patterns can only occur
  82 when defining the notation. This is why the layout schemata are
  83 ``escaped'' with a backslash, so that they cannot be confused with
  84 plain identifiers, wherease the others are not. Alternatively, they
  85 could be defined as keywords, but this would prevent their names to be
  86 used in different contexts.
  87
  88 \begin{table}
  89 \caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut}
  90 \hrule
  91 \[
  92 \begin{array}{@{}ll@{}}
  93 \begin{array}[t]{rcll}
  94   T & ::= & & \mbox{(\bf terms)} \\
  95     &     & L_\kappa[T_1,\dots,T_n] & \mbox{(layout)} \\
  96     &  |  & B_\kappa^{ab}[T_1\cdots T_n] & \mbox{(box)} \\
  97     &  |  & \BREAK & \mbox{(breakpoint)} \\
  98     &  |  & \FENCED{T_1\cdots T_n} & \mbox{(fenced)} \\
  99     &  |  & l & \mbox{(literal)} \\[2ex]
 100   P & ::= & & \mbox{(\bf patterns)} \\
 101     &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
 102     &  |  & B_\kappa^{ab}[P_1\cdots P_n] & \mbox{(box)} \\
 103     &  |  & \BREAK & \mbox{(breakpoint)} \\
 104     &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
 105     &  |  & M & \mbox{(magic)} \\
 106     &  |  & V & \mbox{(variable)} \\
 107     &  |  & l & \mbox{(literal)} \\
 108 \end{array} &
 109 \begin{array}[t]{rcll}
 110   V & ::= & & \mbox{(\bf variables)} \\
 111     &     & \TVAR{x} & \mbox{(term variable)} \\
 112     &  |  & \NVAR{x} & \mbox{(number variable)} \\
 113     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
 114   M & ::= & & \mbox{(\bf magic patterns)} \\
 115     &     & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
 116     &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
 117     &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
 118 \end{array}
 119 \end{array}
 120 \]
 121 \hrule
 122 \end{table}
 123
 124 \[
 125 \IOT{\cdot}{{}} : P -> \mathit{Env} -> T
 126 \]
 127
 128 \begin{table}
 129 \caption{\label{tab:il1} Instantiation of level 1 patterns.\strut}
 130 \hrule
 131 \[
 132 \begin{array}{rcll}
 133   \IOT{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\IOT{P_1}{E},\dots,\IOT{P_n}{E} ] \\
 134   \IOT{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\
 135   \IOT{\BREAK}{E} & = & \BREAK \\
 136   \IOT{\FENCED{P_1\cdots P_n}}{E} & = & \FENCED{\IOT{P_1}{E}\cdots\IOT{P_n}{E}} \\
 137   \IOT{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
 138   \IOT{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
 139   \IOT{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
 140   \IOT{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\
 141   \IOT{\mathtt{opt}~P}{E} & = & \IOT{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
 142   & & & \mathcal{E}'(x)=\left\{
 143   \begin{array}{@{}ll}
 144     v, & \mathcal{E}(x) = \mathtt{Some}~v \\
 145     \mathcal{E}(x), & \mbox{otherwise}
 146   \end{array}
 147   \right. \\
 148   \IOT{\mathtt{list}k~P~l?}{E} & = & \IOT{P}{{E}_1}~{l?}\cdots {l?}~\IOT{P}{{E}_n} &
 149     \mathcal{E}(\NAMES(P)) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\
 150     & & & n\ge k \\
 151   & & & \mathcal{E}_i(x) = \left\{
 152   \begin{array}{@{}ll}
 153     v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\
 154     \mathcal{E}(x), & \mbox{otherwise}
 155   \end{array}
 156   \right. \\
 157   \IOT{l}{E} & = & l \\
 158
 159 %%     &  |  & (P) & \mbox{(fenced)} \\
 160 %%     &  |  & M & \mbox{(magic)} \\
 161 %%     &  |  & V & \mbox{(variable)} \\
 162 %%     &  |  & l & \mbox{(literal)} \\[2ex]
 163 %%   V & ::= & & \mbox{(\bf variables)} \\
 164 %%     &     & \TVAR{x} & \mbox{(term variable)} \\
 165 %%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
 166 %%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
 167 %%   M & ::= & & \mbox{(\bf magic patterns)} \\
 168 %%     &     & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
 169 %%     &  |  & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
 170 %%     &  |  & \verb+opt+~S & \mbox{(option)} \\[2ex]
 171 \end{array}
 172 \]
 173 \hrule
 174 \end{table}
 175
 176 \begin{table}
 177 \caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut}
 178 \hrule
 179 \[
 180 \renewcommand{\arraystretch}{3.5}
 181 \begin{array}[t]{@{}c@{}}
 182   \inference[\sc layout]
 183     {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
 184     {L_\kappa[P_1,\dots,P_n] :: D_1\oplus\cdots\oplus D_n}
 185   \\
 186   \inference[\sc box]
 187     {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
 188     {B_\kappa^{ab}[P_1\cdots P_n] :: D_1\oplus\cdots\oplus D_n}
 189   \\
 190   \inference[\sc fenced]
 191     {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
 192     {\FENCED{P_1\cdots P_n} :: D_1\oplus\cdots\oplus D_n}
 193   \\
 194   \inference[\sc breakpoint]
 195     {}
 196     {\BREAK :: \emptyset}
 197   \qquad
 198   \inference[\sc literal]
 199     {}
 200     {l}
 201   \qquad
 202   \inference[\sc tvar]
 203     {}
 204     {\TVAR{x} :: \TVAR{x}}
 205   \\
 206   \inference[\sc nvar]
 207     {}
 208     {\NVAR{x} :: \NVAR{x}}
 209   \qquad
 210   \inference[\sc ivar]
 211     {}
 212     {\IVAR{x} :: \IVAR{x}}
 213   \\
 214   \inference[\sc list0]
 215     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
 216     {\mathtt{list0}~P~l? :: D'}
 217   \\
 218   \inference[\sc list1]
 219     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
 220     {\mathtt{list1}~P~l? :: D'}
 221   \\
 222   \inference[\sc opt]
 223     {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}}
 224     {\mathtt{opt}~P :: D'}
 225 \end{array}
 226 \]
 227 \hrule
 228 \end{table}
 229
 230   \section{Level 2: abstract syntax}
 231
 232 \end{document}