{-# LANGUAGE QuasiQuotes #-}

module RawSyntax where

import Language.LBNF

compile [$cf|


comment "--" ;
comment "{-" "-}" ;

EHole.   Exp6 ::= Hole ;
EVar.    Exp6 ::= AIdent ;
ESet.    Exp6 ::= Sort ;
EParam.  Exp4 ::= Exp4 "!";
EUp.     Exp4 ::= Exp4 "^";
ELeft.   Exp4 ::= Exp4 "<";
EDestr.  Exp4 ::= Exp4 "%" Natural ;
EProj.   Exp4 ::= Exp4 "#" AIdent ;
EExtr.   Exp4 ::= Exp4 "/" AIdent ;
EApp.    Exp3 ::= Exp3 Exp4 ;
EPi.     Exp2  ::= Exp3 Arrow Exp2 ;
ESigma.  Exp2  ::= Exp3 ";" Exp2 ;
EAbs.    Exp2  ::= "\\" [Bind] Arrow Exp2 ;
EAnn.    Exp1 ::= Exp2 ":" Exp1 ;
EPair.   Exp  ::= Decl "," Exp ;

coercions Exp 6 ;

Decl. Decl ::= AIdent "=" Exp1 ;
PDecl. Decl ::= "param" AIdent "=" Exp1 "::" Exp2;
terminator AIdent "" ;
terminator Decl ";" ;

token Arrow  '-' '>' ;

NoBind. Bind   ::= AIdent ; 
Bind.   Bind   ::= "(" AIdent ":" Exp ")" ;
AIdent. AIdent ::= Identifier ;
terminator Bind "" ;

token Natural digit+;

position token Identifier ('!'|'['|']'|letter|digit|'-'|'_'|'\'')(('*'|'['|']'|letter|digit|'-'|'_'|'\'')*) ;

position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ;

position token Sort '*' (digit*) ('@' digit+)?;

|]