helm/ocaml/cic_notation/doc/main.tex

   1 \documentclass[a4paper]{article}
   2
   3 \usepackage{pifont}
   4 \usepackage{semantic}
   5
   6 \newcommand{\MATITA}{\ding{46}\textsf{Matita}}
   7
   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
  20 \begin{document}
  21   \maketitle
  22
  23 \section{Environment}
  24
  25 \[
  26 \begin{array}{rcll}
  27   V & ::= & & \mbox{(\bf values)} \\
  28     &     & \verb+Term+~T & \mbox{(term)} \\
  29     &  |  & \verb+String+~s & \mbox{(string)} \\
  30     &  |  & \verb+Number+~n & \mbox{(number)} \\
  31     &  |  & \verb+None+ & \mbox{(optional value)} \\
  32     &  |  & \verb+Some+~V & \mbox{(optional value)} \\
  33     &  |  & [ V^{*} ] & \mbox{(list value)} \\[2ex]
  34 \end{array}
  35 \]
  36
  37 An environment is a map $\mathcal E : \mathit{Name} -> V$.
  38
  39 \section{Level 1: concrete syntax patterns}
  40
  41 \[
  42 \begin{array}{rcll}
  43   P & ::= & & \mbox{(patterns)} \\
  44     &     & S^{+} \\[2ex]
  45   S & ::= & & \mbox{(\bf simple patterns)} \\
  46     &     & L_\kappa[S_1,\dots,S_n] & \mbox{(layout)} \\
  47     &  |  & B_\kappa^{ab}[P] & \mbox{(box)} \\
  48     &  |  & \BREAK & \mbox{(breakpoint)} \\
  49     &  |  & (P) & \mbox{(fenced)} \\
  50     &  |  & M & \mbox{(magic)} \\
  51     &  |  & V & \mbox{(variable)} \\
  52     &  |  & l & \mbox{(literal)} \\[2ex]
  53   V & ::= & & \mbox{(\bf variables)} \\
  54     &     & \TVAR{x} & \mbox{(term variable)} \\
  55     &  |  & \NVAR{x} & \mbox{(number variable)} \\
  56     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
  57   M & ::= & & \mbox{(\bf magic patterns)} \\
  58     &     & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
  59     &  |  & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
  60     &  |  & \verb+opt+~S & \mbox{(option)} \\[2ex]
  61 \end{array}
  62 \]
  63
  64 % IOT = Instantiate Two to One
  65 \newcommand{\IOT}[2]{|[#1|]_{\mathcal{#2}}}
  66 \newcommand{\NAMES}{\mathit{names}}
  67
  68 \[
  69 \begin{array}{rcll}
  70   \IOT{S_1\cdots S_n}{E} & = & \IOT{S_1}{E}\cdots\IOT{S_n}{E} \\
  71   \IOT{L_\kappa[S_1,\dots,S_n]}{E} & = & L_\kappa[\IOT{S_1}{E},\dots,\IOT{S_n}{E} ] \\
  72   \IOT{B_\kappa^{ab}[P]}{E} & = & B_\kappa^{ab}[\IOT{P}{E}] \\
  73   \IOT{\BREAK}{E} & = & \BREAK \\
  74   \IOT{(P)}{E} & = & (\IOT{P}{E}) \\
  75   \IOT{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
  76   \IOT{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
  77   \IOT{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
  78   \IOT{\mathtt{opt}~S}{E} & = & \varepsilon & \forall x \in \NAMES(S), \mathcal{E}(x) = \mathtt{None} \\
  79   \IOT{\mathtt{opt}~S}{E} & = & \varepsilon & \forall x \in \NAMES(S), \mathcal{E}(x) = \mathtt{None} \\
  80
  81 %%     &  |  & (P) & \mbox{(fenced)} \\
  82 %%     &  |  & M & \mbox{(magic)} \\
  83 %%     &  |  & V & \mbox{(variable)} \\
  84 %%     &  |  & l & \mbox{(literal)} \\[2ex]
  85 %%   V & ::= & & \mbox{(\bf variables)} \\
  86 %%     &     & \TVAR{x} & \mbox{(term variable)} \\
  87 %%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
  88 %%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
  89 %%   M & ::= & & \mbox{(\bf magic patterns)} \\
  90 %%     &     & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
  91 %%     &  |  & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
  92 %%     &  |  & \verb+opt+~S & \mbox{(option)} \\[2ex]
  93 \end{array}
  94 \]
  95
  96   \section{Level 2: abstract syntax}
  97
  98 \end{document}