entrypoints Decl1;

layout "where";

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

token Var letter (letter | digit | '_' | '\'')* ;

Def.	Decl  ::= Var [Bind] ":" Expr RHS ;
Inst.	Decl  ::= "module" Var [Bind] "=" Id [Expr2] [Modifier] ;
open.   Decl  ::= "open" Id [ Modifier ] ;
Open.	Decl  ::= "open" Id Access [ Modifier ] ;
_.	Decl  ::= Decl1 ;
Module. Decl1 ::= "module" Var [Bind] "where" "{" [Decl] "}" ;

define open x mods = Open x Private mods ;

NoRHS.	RHS   ::= ;
RHS.	RHS   ::= "=" Expr Where ;

NoWhere.   Where ::= ;
AnyWhere.  Where ::= "where" "{" [Decl] "}" ;
SomeWhere. Where ::= "module" Var [Bind] "where" "{" [Decl] "}" ;

Renaming. Modifier ::= "renaming" "(" [Renaming] ")" ;
Using.	  Modifier ::= "using" "(" [ImportName] ")" ;
Hiding.	  Modifier ::= "hiding" "(" [ImportName] ")" ;

To.	   Renaming   ::= ImportName "to" Var;
ImportDef. ImportName ::= Var ;
ImportMod. ImportName ::= "module" Var ;

Public.	 Access ::= "public" ;
Private. Access ::= "private" ;

Pi.	Expr  ::= "(" Var ":" Expr ")" "->" Expr ;
fun.	Expr  ::= Expr1 "->" Expr ;
Lam.	Expr  ::= "\\" Var "->" Expr ;
App.	Expr1 ::= Expr1 Expr2 ;
Name.	Expr2 ::= Id ;
Set.	Expr2 ::= "Set" ;

Id.	Id    ::= [Var];

Bind.	Bind  ::= "(" Var ":" Expr ")" ;

define fun a b = Pi (Var "_") a b ;

coercions Expr 2;

separator Decl ";";
separator nonempty Var ".";
separator Expr2 "";
separator Bind "";
separator Modifier "";
separator Renaming ";";
separator ImportName ";";