%% File generated by the BNF Converter. \batchmode \documentclass[a4paper,11pt]{article} \usepackage[T1]{fontenc} \usepackage[utf8x]{inputenc} \setlength{\parindent}{0mm} \setlength{\parskip}{1mm} \title{The Language Cubicaltt} \author{BNF-converter} \begin{document} \maketitle \newcommand{\emptyP}{\mbox{$\epsilon$}} \newcommand{\terminal}[1]{\mbox{{\texttt {#1}}}} \newcommand{\nonterminal}[1]{\mbox{$\langle \mbox{{\sl #1 }} \! \rangle$}} \newcommand{\arrow}{\mbox{::=}} \newcommand{\delimit}{\mbox{$|$}} \newcommand{\reserved}[1]{\mbox{{\texttt {#1}}}} \newcommand{\literal}[1]{\mbox{{\texttt {#1}}}} \newcommand{\symb}[1]{\mbox{{\texttt {#1}}}} This document was automatically generated by the {\em BNF-Converter}. \section*{The lexical structure of Cubicaltt} AIdent literals are recognized by the regular expression \(\mbox{`\_'} \mid ({\nonterminal{lower}} \mid {\nonterminal{upper}}) ({\nonterminal{lower}} \mid {\nonterminal{upper}} \mid {\nonterminal{digit}} \mid \mbox{`''} \mid \mbox{`\_'})* \mid (\mbox{`!'}) ({\nonterminal{digit}})*\) CIdent literals are recognized by the regular expression \((\mbox{`/'}) (\mbox{`$\backslash$'})\) HoleIdent literals are recognized by the regular expression \(\mbox{`?'}\) \subsection*{Reserved words and symbols} The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions. The reserved words used in Cubicaltt are the following: \\ \begin{tabular}{lll} {\reserved{Glue}} & {\reserved{Id}} & {\reserved{PathP}} \\ {\reserved{U}} & {\reserved{comp}} & {\reserved{data}} \\ {\reserved{fill}} & {\reserved{glue}} & {\reserved{hComp}} \\ {\reserved{hdata}} & {\reserved{idC}} & {\reserved{idJ}} \\ {\reserved{import}} & {\reserved{in}} & {\reserved{let}} \\ {\reserved{module}} & {\reserved{mutual}} & {\reserved{opaque}} \\ {\reserved{split}} & {\reserved{transparent}} & {\reserved{transparent\_all}} \\ {\reserved{transport}} & {\reserved{undefined}} & {\reserved{unglue}} \\ {\reserved{where}} & {\reserved{with}} & \\ \end{tabular} \\ The symbols used in Cubicaltt are the following: \\ \begin{tabular}{lll} {\symb{(}} & {\symb{)}} & {\symb{*}} \\ {\symb{,}} & {\symb{{$-$}}} & {\symb{{$-$}{$>$}}} \\ {\symb{.1}} & {\symb{.2}} & {\symb{0}} \\ {\symb{1}} & {\symb{:}} & {\symb{;}} \\ {\symb{{$<$}}} & {\symb{{$=$}}} & {\symb{{$>$}}} \\ {\symb{@}} & {\symb{[}} & {\symb{$\backslash$}} \\ {\symb{$\backslash$/}} & {\symb{]}} & {\symb{split@}} \\ {\symb{\{}} & {\symb{{$|$}}} & {\symb{\}}} \\ \end{tabular} \\ \subsection*{Comments} Single-line comments begin with {\symb{{$-$}{$-$}}}. Multiple-line comments are enclosed with {\symb{\{{$-$}}} and {\symb{{$-$}\}}}. \section*{The syntactic structure of Cubicaltt} Non-terminals are enclosed between $\langle$ and $\rangle$. The symbols {\arrow} (production), {\delimit} (union) and {\emptyP} (empty rule) belong to the BNF notation. All other symbols are terminals.\\ \begin{tabular}{lll} {\nonterminal{Branch}} & {\arrow} &{\nonterminal{AIdent}} {\nonterminal{ListAIdent}} {\terminal{{$-$}{$>$}}} {\nonterminal{ExpWhere}} \\ & {\delimit} &{\nonterminal{AIdent}} {\nonterminal{ListAIdent}} {\terminal{@}} {\nonterminal{ListAIdent}} {\terminal{{$-$}{$>$}}} {\nonterminal{ExpWhere}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Decl}} & {\arrow} &{\terminal{data}} {\nonterminal{AIdent}} {\nonterminal{ListTele}} {\terminal{{$=$}}} {\nonterminal{ListLabel}} \\ & {\delimit} &{\nonterminal{AIdent}} {\nonterminal{ListTele}} {\terminal{:}} {\nonterminal{Exp}} {\terminal{{$=$}}} {\nonterminal{ExpWhere}} \\ & {\delimit} &{\terminal{hdata}} {\nonterminal{AIdent}} {\nonterminal{ListTele}} {\terminal{{$=$}}} {\nonterminal{ListLabel}} \\ & {\delimit} &{\terminal{mutual}} {\terminal{\{}} {\nonterminal{ListDecl}} {\terminal{\}}} \\ & {\delimit} &{\terminal{opaque}} {\nonterminal{AIdent}} \\ & {\delimit} &{\nonterminal{AIdent}} {\nonterminal{ListTele}} {\terminal{:}} {\nonterminal{Exp}} {\terminal{{$=$}}} {\terminal{split}} {\terminal{\{}} {\nonterminal{ListBranch}} {\terminal{\}}} \\ & {\delimit} &{\terminal{transparent}} {\nonterminal{AIdent}} \\ & {\delimit} &{\terminal{transparent\_all}} \\ & {\delimit} &{\nonterminal{AIdent}} {\nonterminal{ListTele}} {\terminal{:}} {\nonterminal{Exp}} {\terminal{{$=$}}} {\terminal{undefined}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Dir}} & {\arrow} &{\terminal{0}} \\ & {\delimit} &{\terminal{1}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Exp}} & {\arrow} &{\terminal{$\backslash$}} {\nonterminal{ListPTele}} {\terminal{{$-$}{$>$}}} {\nonterminal{Exp}} \\ & {\delimit} &{\terminal{let}} {\terminal{\{}} {\nonterminal{ListDecl}} {\terminal{\}}} {\terminal{in}} {\nonterminal{Exp}} \\ & {\delimit} &{\terminal{{$<$}}} {\nonterminal{ListAIdent}} {\terminal{{$>$}}} {\nonterminal{Exp}} \\ & {\delimit} &{\terminal{split@}} {\nonterminal{Exp}} {\terminal{with}} {\terminal{\{}} {\nonterminal{ListBranch}} {\terminal{\}}} \\ & {\delimit} &{\nonterminal{Exp1}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ExpWhere}} & {\arrow} &{\nonterminal{Exp}} \\ & {\delimit} &{\nonterminal{Exp}} {\terminal{where}} {\terminal{\{}} {\nonterminal{ListDecl}} {\terminal{\}}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Face}} & {\arrow} &{\terminal{(}} {\nonterminal{AIdent}} {\terminal{{$=$}}} {\nonterminal{Dir}} {\terminal{)}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Formula}} & {\arrow} &{\nonterminal{Formula}} {\terminal{$\backslash$/}} {\nonterminal{Formula1}} \\ & {\delimit} &{\nonterminal{Formula1}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Imp}} & {\arrow} &{\terminal{import}} {\nonterminal{AIdent}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Label}} & {\arrow} &{\nonterminal{AIdent}} {\nonterminal{ListTele}} \\ & {\delimit} &{\nonterminal{AIdent}} {\nonterminal{ListTele}} {\terminal{{$<$}}} {\nonterminal{ListAIdent}} {\terminal{{$>$}}} {\nonterminal{System}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Module}} & {\arrow} &{\terminal{module}} {\nonterminal{AIdent}} {\terminal{where}} {\terminal{\{}} {\nonterminal{ListImp}} {\nonterminal{ListDecl}} {\terminal{\}}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{PTele}} & {\arrow} &{\terminal{(}} {\nonterminal{Exp}} {\terminal{:}} {\nonterminal{Exp}} {\terminal{)}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Side}} & {\arrow} &{\nonterminal{ListFace}} {\terminal{{$-$}{$>$}}} {\nonterminal{Exp}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{System}} & {\arrow} &{\terminal{[}} {\nonterminal{ListSide}} {\terminal{]}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Tele}} & {\arrow} &{\terminal{(}} {\nonterminal{AIdent}} {\nonterminal{ListAIdent}} {\terminal{:}} {\nonterminal{Exp}} {\terminal{)}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListAIdent}} & {\arrow} &{\emptyP} \\ & {\delimit} &{\nonterminal{AIdent}} {\nonterminal{ListAIdent}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListBranch}} & {\arrow} &{\emptyP} \\ & {\delimit} &{\nonterminal{Branch}} \\ & {\delimit} &{\nonterminal{Branch}} {\terminal{;}} {\nonterminal{ListBranch}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListDecl}} & {\arrow} &{\emptyP} \\ & {\delimit} &{\nonterminal{Decl}} \\ & {\delimit} &{\nonterminal{Decl}} {\terminal{;}} {\nonterminal{ListDecl}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListExp}} & {\arrow} &{\nonterminal{Exp}} \\ & {\delimit} &{\nonterminal{Exp}} {\terminal{,}} {\nonterminal{ListExp}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListFace}} & {\arrow} &{\emptyP} \\ & {\delimit} &{\nonterminal{Face}} {\nonterminal{ListFace}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListImp}} & {\arrow} &{\emptyP} \\ & {\delimit} &{\nonterminal{Imp}} \\ & {\delimit} &{\nonterminal{Imp}} {\terminal{;}} {\nonterminal{ListImp}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListLabel}} & {\arrow} &{\emptyP} \\ & {\delimit} &{\nonterminal{Label}} \\ & {\delimit} &{\nonterminal{Label}} {\terminal{{$|$}}} {\nonterminal{ListLabel}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListPTele}} & {\arrow} &{\nonterminal{PTele}} \\ & {\delimit} &{\nonterminal{PTele}} {\nonterminal{ListPTele}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListSide}} & {\arrow} &{\emptyP} \\ & {\delimit} &{\nonterminal{Side}} \\ & {\delimit} &{\nonterminal{Side}} {\terminal{,}} {\nonterminal{ListSide}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{ListTele}} & {\arrow} &{\emptyP} \\ & {\delimit} &{\nonterminal{Tele}} {\nonterminal{ListTele}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Exp1}} & {\arrow} &{\nonterminal{Exp2}} {\terminal{{$-$}{$>$}}} {\nonterminal{Exp1}} \\ & {\delimit} &{\nonterminal{ListPTele}} {\terminal{{$-$}{$>$}}} {\nonterminal{Exp1}} \\ & {\delimit} &{\nonterminal{ListPTele}} {\terminal{*}} {\nonterminal{Exp1}} \\ & {\delimit} &{\nonterminal{Exp2}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Exp2}} & {\arrow} &{\nonterminal{Exp2}} {\nonterminal{Exp3}} \\ & {\delimit} &{\nonterminal{Exp2}} {\terminal{@}} {\nonterminal{Formula}} \\ & {\delimit} &{\nonterminal{Exp3}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Exp3}} & {\arrow} &{\terminal{comp}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} {\nonterminal{System}} \\ & {\delimit} &{\terminal{fill}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} {\nonterminal{System}} \\ & {\delimit} &{\terminal{Glue}} {\nonterminal{Exp4}} {\nonterminal{System}} \\ & {\delimit} &{\terminal{glue}} {\nonterminal{Exp4}} {\nonterminal{System}} \\ & {\delimit} &{\terminal{hComp}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} {\nonterminal{System}} \\ & {\delimit} &{\terminal{Id}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} {\nonterminal{Exp3}} \\ & {\delimit} &{\terminal{idJ}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} \\ & {\delimit} &{\terminal{idC}} {\nonterminal{Exp4}} {\nonterminal{System}} \\ & {\delimit} &{\terminal{PathP}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} \\ & {\delimit} &{\terminal{transport}} {\nonterminal{Exp4}} {\nonterminal{Exp4}} \\ & {\delimit} &{\terminal{unglue}} {\nonterminal{Exp4}} {\nonterminal{System}} \\ & {\delimit} &{\nonterminal{Exp4}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Exp4}} & {\arrow} &{\nonterminal{Exp4}} {\terminal{.1}} \\ & {\delimit} &{\nonterminal{Exp4}} {\terminal{.2}} \\ & {\delimit} &{\nonterminal{Exp5}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Exp5}} & {\arrow} &{\nonterminal{HoleIdent}} \\ & {\delimit} &{\nonterminal{AIdent}} {\terminal{\{}} {\nonterminal{Exp}} {\terminal{\}}} \\ & {\delimit} &{\terminal{(}} {\nonterminal{Exp}} {\terminal{,}} {\nonterminal{ListExp}} {\terminal{)}} \\ & {\delimit} &{\terminal{U}} \\ & {\delimit} &{\nonterminal{AIdent}} \\ & {\delimit} &{\terminal{(}} {\nonterminal{Exp}} {\terminal{)}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Formula1}} & {\arrow} &{\nonterminal{Formula1}} {\nonterminal{CIdent}} {\nonterminal{Formula2}} \\ & {\delimit} &{\nonterminal{Formula2}} \\ \end{tabular} \\ \begin{tabular}{lll} {\nonterminal{Formula2}} & {\arrow} &{\nonterminal{AIdent}} \\ & {\delimit} &{\nonterminal{Dir}} \\ & {\delimit} &{\terminal{{$-$}}} {\nonterminal{Formula2}} \\ & {\delimit} &{\terminal{(}} {\nonterminal{Formula}} {\terminal{)}} \\ \end{tabular} \\ \end{document}