content: {-# LANGUAGE QuasiQuotes, TemplateHaskell #-}
  
  module RawSyntax where
  import Language.LBNF
  
  bnfc [lbnf|
  
  comment "--" ;
  comment "{-" "-}" ;
  
  ETag.    Exp6 ::= "'" AIdent;
  EFin.    Exp6 ::= OpenBrack [AIdent] "]";
  ECas.    Exp6 ::= "case" Open [Defin] "}" ;
  EHole.   Exp6 ::= Hole ;
  EVar.    Exp6 ::= AIdent ;
  ESet.    Exp6 ::= Sort ;
  EProj.   Exp4 ::= Exp4 "." AIdent ;
  EApp.    Exp3 ::= Exp3 Exp4 ;
  EPi.     Exp2  ::= Exp3 Arrow Exp2 ;
  ESigma.  Exp2  ::= Open [Exp] "}" ;
  EAbs.    Exp2  ::= "\\" [Bind] Arrow Exp2 ;
  EThis.   Exp6  ::= "this" ;
  EAnn.    Exp1 ::= Exp2 ":" Exp1 ;
  EPair.   Exp  ::= [Defin] ;
  
  coercions Exp 6 ;
  
  separator Exp ";";
  
  
  Def.   Defin ::= AIdent "=" Exp ;
  separator nonempty Defin ",";
  separator AIdent ",";
  
  token Arrow  ('-' '>') ;
  
  NoBind. Bind   ::= AIdent ; 
  Bind.   Bind   ::= "(" AIdent ":" Exp ")" ;
  AIdent. AIdent ::= Identifier ;
  terminator Bind "" ;
  
  token Natural digit+;
  
  position token Open ('{');
  position token OpenBrack ('[');
  position token Identifier ('!'|letter|digit|'-'|'_')((letter|digit|'-'|'_'|'\'')*) ;
  position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ;
  
  position token Sort ('#' | '*' (digit*));
  
  |]
  