---  Core Syntax ---

layout "where";

-- A program is a list of declarations:
Module.   Program   ::= [CDecl] ;
separator CDecl ";" ;

-- An expression is either \x -> e or i e1 ... en

EIdent.   CExp2   ::= Ident ;                 -- without arguments
EApp.     CExp1   ::= Ident  [CExp2] ;        -- with arguments
EAbs.     CExp    ::= "\\" Ident "->" CExp ;
_.        CExp2   ::= "("CExp")" ;             -- nontrivial arguments
separator nonempty CExp2 "" ;

-- A type expression is either "Set" or "(x : A) -> B" or a term: 

TFun.   TExp     ::= "(" VarDecl ")" "->" TExp ;
TSet.   TExp     ::= "Set" ;
TEl.    TExp     ::= CExp ;
VDecl.   VarDecl ::= Ident ":" TExp  ;

-- A declaration is either a typing declaration or a definition.
-- A typing declaration is of the form "i : e":


Var.  CDecl    ::= VarDecl ; 

-- An explicit definition is of the form "i = e"

Def.  CDecl    ::= Ident ":" TExp "=" CExp ;

-- An implicit definition is of the form

--  fun f (x1:t1) ... (xn:tn) : te =
--              c1 y1 ... ym -> e1 |
--                  ...
--              ck z1 ... zm -> ek

DecImpl.    CDecl        ::= "fun" ImplTyping "=" [Branch] ;
Implt.      ImplTyping  ::= Ident Telescope ":" TExp ;
Telcon.   Telescope     ::= [VarDecl];
[].      [VarDecl]     ::= ;
(:).     [VarDecl]     ::= "(" VarDecl ")" [VarDecl];
BranchCon. Branch       ::= ApplVars "->" CExp ;
AppPattern.  ApplVars   ::= [Ident] ;    -- an application to variables
separator nonempty Ident "" ;
separator Branch "|" ;


-- A data type definition is of the form

--  data D (x1:t1) ... (xn:tn) :tm =
--                c1 : e1| 
--                   ... 
--                cn : en
DecData.   CDecl     ::= "data" ImplTyping "where" [ConstrDecl] ;
Const.    ConstrDecl::= Ident ":" CExp;
separator ConstrDecl "|" ;
comment "--" ;
comment "{-" "-}" ;