The Language Cubicaltt
BNF Converter


% File generated by the BNF Converter.


This document was automatically generated by the //BNF-Converter//.

==The lexical structure of Cubicaltt==

AIdent literals are recognized by the regular expression
`````'_' | (lower | upper) (lower | upper | digit | ''' | '_')* | ('!') (digit)*`````

CIdent literals are recognized by the regular expression
`````('/') ('\')`````

HoleIdent literals are recognized by the regular expression
`````'?'`````

===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:
  | ``Glue`` | ``Id`` | ``PathP`` | ``U``
  | ``comp`` | ``data`` | ``fill`` | ``glue``
  | ``hComp`` | ``hdata`` | ``idC`` | ``idJ``
  | ``import`` | ``in`` | ``let`` | ``module``
  | ``mutual`` | ``opaque`` | ``split`` | ``transparent``
  | ``transparent_all`` | ``transport`` | ``undefined`` | ``unglue``
  | ``where`` | ``with``  |  |

The symbols used in Cubicaltt  the following:
  | ( | ) | * | ,
  | - | -> | .1 | .2
  | 0 | 1 | : | ;
  | < | = | > | @
  | [ | \ | \/ | ]
  | split@ | { | | | }

===Comments===

Single-line comments begin with --.
Multiple-line comments are  enclosed with {- and -}.

==The syntactic structure of Cubicaltt ==
Non-terminals are enclosed between < and >.
The symbols **->** (production), **|** (union)
and **eps** (empty rule) belong to the BNF notation.
All other symbols are terminals.

  | //Branch// | -> | //AIdent// //[AIdent]// ``->`` //ExpWhere//
  |  |  **|**  | //AIdent// //[AIdent]// ``@`` //[AIdent]// ``->`` //ExpWhere//
  | //Decl// | -> | ``data`` //AIdent// //[Tele]// ``=`` //[Label]//
  |  |  **|**  | //AIdent// //[Tele]// ``:`` //Exp// ``=`` //ExpWhere//
  |  |  **|**  | ``hdata`` //AIdent// //[Tele]// ``=`` //[Label]//
  |  |  **|**  | ``mutual`` ``{`` //[Decl]// ``}``
  |  |  **|**  | ``opaque`` //AIdent//
  |  |  **|**  | //AIdent// //[Tele]// ``:`` //Exp// ``=`` ``split`` ``{`` //[Branch]// ``}``
  |  |  **|**  | ``transparent`` //AIdent//
  |  |  **|**  | ``transparent_all``
  |  |  **|**  | //AIdent// //[Tele]// ``:`` //Exp// ``=`` ``undefined``
  | //Dir// | -> | ``0``
  |  |  **|**  | ``1``
  | //Exp// | -> | ``\`` //[PTele]// ``->`` //Exp//
  |  |  **|**  | ``let`` ``{`` //[Decl]// ``}`` ``in`` //Exp//
  |  |  **|**  | ``<`` //[AIdent]// ``>`` //Exp//
  |  |  **|**  | ``split@`` //Exp// ``with`` ``{`` //[Branch]// ``}``
  |  |  **|**  | //Exp1//
  | //ExpWhere// | -> | //Exp//
  |  |  **|**  | //Exp// ``where`` ``{`` //[Decl]// ``}``
  | //Face// | -> | ``(`` //AIdent// ``=`` //Dir// ``)``
  | //Formula// | -> | //Formula// ``\/`` //Formula1//
  |  |  **|**  | //Formula1//
  | //Imp// | -> | ``import`` //AIdent//
  | //Label// | -> | //AIdent// //[Tele]//
  |  |  **|**  | //AIdent// //[Tele]// ``<`` //[AIdent]// ``>`` //System//
  | //Module// | -> | ``module`` //AIdent// ``where`` ``{`` //[Imp]// //[Decl]// ``}``
  | //PTele// | -> | ``(`` //Exp// ``:`` //Exp// ``)``
  | //Side// | -> | //[Face]// ``->`` //Exp//
  | //System// | -> | ``[`` //[Side]// ``]``
  | //Tele// | -> | ``(`` //AIdent// //[AIdent]// ``:`` //Exp// ``)``
  | //[AIdent]// | -> | **eps**
  |  |  **|**  | //AIdent// //[AIdent]//
  | //[Branch]// | -> | **eps**
  |  |  **|**  | //Branch//
  |  |  **|**  | //Branch// ``;`` //[Branch]//
  | //[Decl]// | -> | **eps**
  |  |  **|**  | //Decl//
  |  |  **|**  | //Decl// ``;`` //[Decl]//
  | //[Exp]// | -> | //Exp//
  |  |  **|**  | //Exp// ``,`` //[Exp]//
  | //[Face]// | -> | **eps**
  |  |  **|**  | //Face// //[Face]//
  | //[Imp]// | -> | **eps**
  |  |  **|**  | //Imp//
  |  |  **|**  | //Imp// ``;`` //[Imp]//
  | //[Label]// | -> | **eps**
  |  |  **|**  | //Label//
  |  |  **|**  | //Label// ``|`` //[Label]//
  | //[PTele]// | -> | //PTele//
  |  |  **|**  | //PTele// //[PTele]//
  | //[Side]// | -> | **eps**
  |  |  **|**  | //Side//
  |  |  **|**  | //Side// ``,`` //[Side]//
  | //[Tele]// | -> | **eps**
  |  |  **|**  | //Tele// //[Tele]//
  | //Exp1// | -> | //Exp2// ``->`` //Exp1//
  |  |  **|**  | //[PTele]// ``->`` //Exp1//
  |  |  **|**  | //[PTele]// ``*`` //Exp1//
  |  |  **|**  | //Exp2//
  | //Exp2// | -> | //Exp2// //Exp3//
  |  |  **|**  | //Exp2// ``@`` //Formula//
  |  |  **|**  | //Exp3//
  | //Exp3// | -> | ``comp`` //Exp4// //Exp4// //System//
  |  |  **|**  | ``fill`` //Exp4// //Exp4// //System//
  |  |  **|**  | ``Glue`` //Exp4// //System//
  |  |  **|**  | ``glue`` //Exp4// //System//
  |  |  **|**  | ``hComp`` //Exp4// //Exp4// //System//
  |  |  **|**  | ``Id`` //Exp4// //Exp4// //Exp3//
  |  |  **|**  | ``idJ`` //Exp4// //Exp4// //Exp4// //Exp4// //Exp4// //Exp4//
  |  |  **|**  | ``idC`` //Exp4// //System//
  |  |  **|**  | ``PathP`` //Exp4// //Exp4// //Exp4//
  |  |  **|**  | ``transport`` //Exp4// //Exp4//
  |  |  **|**  | ``unglue`` //Exp4// //System//
  |  |  **|**  | //Exp4//
  | //Exp4// | -> | //Exp4// ``.1``
  |  |  **|**  | //Exp4// ``.2``
  |  |  **|**  | //Exp5//
  | //Exp5// | -> | //HoleIdent//
  |  |  **|**  | //AIdent// ``{`` //Exp// ``}``
  |  |  **|**  | ``(`` //Exp// ``,`` //[Exp]// ``)``
  |  |  **|**  | ``U``
  |  |  **|**  | //AIdent//
  |  |  **|**  | ``(`` //Exp// ``)``
  | //Formula1// | -> | //Formula1// //CIdent// //Formula2//
  |  |  **|**  | //Formula2//
  | //Formula2// | -> | //AIdent//
  |  |  **|**  | //Dir//
  |  |  **|**  | ``-`` //Formula2//
  |  |  **|**  | ``(`` //Formula// ``)``