Alfa.cf

-- layout rules

layout "of", "let", "where", "sig", "struct", "mutual" ;
layout stop "in" ;
layout toplevel ;

-- top level

Module.  Module ::= "{" [Decl] "}" ;

separator  Decl ";" ;
separator  Def ";" ;

-- declarations/definitions

DDef.    Decl ::= [DefAttr] Def ;
DImp.    Decl ::= Import ;

Value.   Def  ::= AIdent [VarDecl] "::" Exp "=" Exp ;
Binding. Def  ::= AIdent "=" Exp ;
Package. Def  ::= "package" AIdent [Typing] "where" PackageBody ;
Open.    Def  ::= "open" Exp "use" [OpenArg] ;
Data.    Def  ::= "data" AIdent [Typing] "=" [Constructor] ;
Type.    Def  ::= "type" AIdent [Typing] "=" Exp ;
Axiom.   Def  ::= "postulate" AIdent [Typing] "::" Exp ;
Mutual.  Def  ::= "mutual" "{" [Def] "}" ;
Commt.   Def  ::= Comment ;

-- expressions

EVar.    Exp4 ::= AIdent ;
ECon.    Exp4 ::= AIdent "@_" ;
ESet.    Exp4 ::= "Set" ;
EType.   Exp4 ::= "Type" ;
EMeta.   Exp4 ::= "?" ;
EStar.   Exp4 ::= "#" Integer ;
EMetaU.  Exp4 ::= "_" ;
EString. Exp4 ::= String ;
EChar.   Exp4 ::= Char ;
EInt.    Exp4 ::= Integer ;
EDouble. Exp4 ::= Double ;
EProj.   Exp3 ::= Exp3 "." AIdent ;
EApp.    Exp1 ::= Exp1 Exp2 ;
EInfix.  Exp  ::= Exp1 Infix Exp1 ;
ESig.    Exp1 ::= "sig" "{" [FieldDecl] "}" ;
EStr.    Exp1 ::= "struct" "{" [Binding] "}" ;
ESum.    Exp  ::= "data" [Constructor] ;
EPi.     Exp  ::= VarDecl Arrow Exp ;
EFun.    Exp  ::= Exp1 Arrow Exp ;
EAbs.    Exp  ::= "\\" VarDecl Arrow Exp ;
EAbsUnt. Exp  ::= "\\" [AIdent] Arrow Exp ;
ELet.    Exp  ::= "let" "{" [Decl] "}" "in" Exp ;
EOpen.   Exp  ::= "open" Exp "use" [OpenArg] "in" Exp ; ---- "in" does not parse
ECase.   Exp  ::= "case" Exp "of" "{" [Branch] "}" ;
EIData.  Exp  ::= "idata" [VarDecl] [IndConstructor] ;  --- [Typing]

ECommL.  Exp  ::= Comment Exp1 ;
ECommR.  Exp  ::= Exp1 Comment ;

internal EConst. Exp4 ::= AIdent ;
internal EMetaN. Exp4 ::= "?" Integer ;

coercions Exp 4 ;

-- shown/hidden arguments

AShow.  Arrow ::= "->" ;
AHide.  Arrow ::= "|->" ;

-- typings/hypotheses

TDecl. Typing  ::= VarDecl ;
TExp.  Typing  ::= Exp2 ;

terminator Typing "" ;  

VDecl. VarDecl ::= "(" [Bound] "::" Exp ")" ;

BVar.  Bound ::= AIdent ;
BHide. Bound ::= "|" AIdent ;

separator nonempty Bound "," ;

terminator VarDecl "" ;

FDecl. FieldDecl ::= AIdent "::" Exp ;

separator FieldDecl ";" ;

-- case branches

BranchCon . Branch ::= "(" AIdent [AIdent] ")" "->" Exp ; --- no deeper patterns?
BranchInf . Branch ::= "(" AIdent Infix AIdent ")" "->" Exp ;
BranchVar . Branch ::= AIdent "->" Exp ;

separator Branch   ";" ;

-- constructions in data definitions

Cnstr . Constructor ::= AIdent [Typing] ;
separator  Constructor "|" ;

ICnstr . IndConstructor ::= AIdent [Typing] "::" "_" [Exp2] ;
separator  IndConstructor "|" ;
terminator Exp2 "" ;

-- bindings in structures

Bind . Binding ::= AIdent "=" Exp ;
separator Binding  ";" ;


PackageDef .  PackageBody ::= "{" [Decl] "}" ;
PackageInst . PackageBody ::= Exp ;

OArg .  OpenArg ::= [DefAttr] AIdent ;
OArgT . OpenArg ::= [DefAttr] AIdent "::" Exp ;
OArgD . OpenArg ::= [DefAttr] AIdent "=" Exp ;
OArgTD. OpenArg ::= [DefAttr] AIdent "::" Exp "=" Exp ;

Private  . DefAttr ::= "private" ;
Public   . DefAttr ::= "public" ;
Abstract . DefAttr ::= "abstract" ;
Concrete . DefAttr ::= "concrete" ;

Import  .  Import  ::= "import" String ";" ;

separator  DefAttr     "" ;
separator  AIdent      "" ;
separator  OpenArg     "," ; 

-- two kinds of comments; preserve enclosed ones

comment "--" ;

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

token Comment ('{' '-' ((char - '-') | '-' (char - '}'))* ('-')+ '}') ;

--- identifiers, including infix in parentheses

token Infix ([".:-^*+=<>&%$!#%|/\\"]+) ;

I. AIdent ::= "(" Infix ")" ;
F. AIdent ::= PIdent ;

-- ordinary identifiers now have position

position token PIdent (letter (letter|digit|'_'|'\'')*) ;