helm/ocaml/cic_notation/doc/main.tex

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