helm/ocaml/cic_notation/doc/main.tex

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