Permalink
Fetching contributors…
Cannot retrieve contributors at this time
150 lines (103 sloc) 3.7 KB
-- 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|'_'|'\'')*) ;