ProLin/Exp.cf at master · GU-CLASP/ProLin · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
entrypoints Modul ;

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

Mod. Modul ::= [Decl];

DeclRule.   Decl ::= AIdent ":" Exp ;
DeclCtx.    Decl ::= AIdent "::" Exp ;
separator   Decl ";" ;

Equality. Exp1 ::= Exp2 "==" Exp2 ;
Fun.      Exp1 ::= Exp2 "->" Exp1 ;
LFun.     Exp1 ::= Exp2 "-o" Exp1 ;
NFun.     Exp1 ::= Exp2 "?->" Exp1 ;
LFunR.    Exp1 ::= Exp2 "-*" Exp1 ;
Pi.       Exp1 ::= "(" PseudoTDecl ")" "->" Exp1 ;
LinPi.    Exp1 ::= "(" PseudoTDecl ")" "-o" Exp1 ;
LinPiR.   Exp1 ::= "(" PseudoTDecl ")" "-*" Exp1 ;
PiU.  Exp1 ::= "(" PseudoTDecl ")" "!->" Exp1 ;
App.      Exp2 ::= Exp2 Exp3 ;
Var.      Exp3 ::= AIdent ;
StrLit.   Exp3 ::= String ;
U.        Exp3 ::= "Type" ;
Rec.      Exp3 ::= "[" [Decl] "]";
coercions Exp 3 ;


-- Nonempty telescopes with Exp:s, this is hack to avoid ambiguities
-- in the grammar when parsing Pi
PseudoTDecl.  PseudoTDecl ::=  Exp ":" Exp ;

position token AIdent ((letter|'_'|'`')(letter|digit|'\''|'_')*) ;
terminator AIdent "" ;