From: Luca Padovani Date: Wed, 28 Sep 2005 16:28:30 +0000 (+0000) Subject: * first version of the specification X-Git-Tag: V_0_7_2_3~284 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d9b039d9b2f1f20fae18e577306ead3b5d2090d;p=helm.git * first version of the specification --- diff --git a/helm/ocaml/cic_notation/doc/main.tex b/helm/ocaml/cic_notation/doc/main.tex new file mode 100644 index 000000000..16b29bf8a --- /dev/null +++ b/helm/ocaml/cic_notation/doc/main.tex @@ -0,0 +1,98 @@ +\documentclass[a4paper]{article} + +\usepackage{pifont} +\usepackage{semantic} + +\newcommand{\MATITA}{\ding{46}\textsf{Matita}} + + +\title{Extensible notation for \MATITA} +\author{Luca Padovani \qquad Stefano Zacchiroli \\ +\small Department of Computer Science, University of Bologna \\ +\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\ +\small \{\texttt{lpadovan}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}} + +\newcommand{\BREAK}{\mathtt{break}} +\newcommand{\TVAR}[1]{#1:\mathtt{term}} +\newcommand{\NVAR}[1]{#1:\mathtt{number}} +\newcommand{\IVAR}[1]{#1:\mathtt{name}} + +\begin{document} + \maketitle + +\section{Environment} + +\[ +\begin{array}{rcll} + V & ::= & & \mbox{(\bf values)} \\ + & & \verb+Term+~T & \mbox{(term)} \\ + & | & \verb+String+~s & \mbox{(string)} \\ + & | & \verb+Number+~n & \mbox{(number)} \\ + & | & \verb+None+ & \mbox{(optional value)} \\ + & | & \verb+Some+~V & \mbox{(optional value)} \\ + & | & [ V^{*} ] & \mbox{(list value)} \\[2ex] +\end{array} +\] + +An environment is a map $\mathcal E : \mathit{Name} -> V$. + +\section{Level 1: concrete syntax patterns} + +\[ +\begin{array}{rcll} + P & ::= & & \mbox{(patterns)} \\ + & & S^{+} \\[2ex] + S & ::= & & \mbox{(\bf simple patterns)} \\ + & & L_\kappa[S_1,\dots,S_n] & \mbox{(layout)} \\ + & | & B_\kappa^{ab}[P] & \mbox{(box)} \\ + & | & \BREAK & \mbox{(breakpoint)} \\ + & | & (P) & \mbox{(fenced)} \\ + & | & M & \mbox{(magic)} \\ + & | & V & \mbox{(variable)} \\ + & | & l & \mbox{(literal)} \\[2ex] + 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] +\end{array} +\] + +% IOT = Instantiate Two to One +\newcommand{\IOT}[2]{|[#1|]_{\mathcal{#2}}} +\newcommand{\NAMES}{\mathit{names}} + +\[ +\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{\BREAK}{E} & = & \BREAK \\ + \IOT{(P)}{E} & = & (\IOT{P}{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} \\ + +%% & | & (P) & \mbox{(fenced)} \\ +%% & | & M & \mbox{(magic)} \\ +%% & | & V & \mbox{(variable)} \\ +%% & | & l & \mbox{(literal)} \\[2ex] +%% 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] +\end{array} +\] + + \section{Level 2: abstract syntax} + +\end{document} \ No newline at end of file