Syntax.cf

comment "--" ;

layout toplevel ;

token VarIdent (lower (letter | digit | '_' | '\'')*) ;
token MetaVarIdent (upper (letter | digit | '_' | '\'')*) ;

-- A Program is a list of Commands
AProgram. Program ::= [Command] ;

-- Commands for checking and computing
CommandCompute. Command ::= "compute" Term ;
terminator Command ";" ;

-- Terms in the lambda calculus
Lam.     Term  ::= "λ" Pattern ":" Type "." ScopedTerm ;
Let.     Term  ::= "let" Pattern "=" Term "in" ScopedTerm ;
App.     Term1 ::= Term1 Term2 ; -- x y z  =  (x y) z  ≠  x (y z)
Var.     Term2 ::= VarIdent ;
MetaVar. Term2 ::= MetaVarIdent "[" [Term] "]";
_.       Term  ::= Term1 ;
_.       Term1 ::= Term2 ;
_.       Term2 ::= "(" Term ")" ;

separator Term "," ;

AScopedTerm. ScopedTerm ::= Term ;
APattern. Pattern ::= VarIdent ;

ABinder. Binder ::= VarIdent ":" Type ;
separator Binder "," ;

AMetaSubst. MetaSubst ::= MetaVarIdent "[" [Binder] "]" "↦" ScopedTerm ;
AUnificationConstraint. UnificationConstraint ::= "∀" [Binder] "." ScopedTerm "=" ScopedTerm ;

separator VarIdent "," ;

-- Types
Fun.    Type ::= Type1 "->" Type ;
Base.   Type1 ::= VarIdent ;
coercions Type 1;