34 lines
866 B
CFEngine3
34 lines
866 B
CFEngine3
entrypoints [Def], Exp ;
|
||
|
||
token Id ((letter|digit|["[]_"])+) ;
|
||
|
||
comment "--" ;
|
||
comment "{-" "-}" ;
|
||
|
||
BE. BD ::= Id;
|
||
BI. BD ::= "{" Id "}";
|
||
separator nonempty BD "" ;
|
||
|
||
ExpPiE. Exp ::= "Π" "(" Id ":" Exp ")" Exp;
|
||
ExpPiI. Exp ::= "Π" "{" Id ":" Exp "}" Exp;
|
||
ExpSig. Exp ::= "Σ" "(" Id ":" Exp ")" Exp;
|
||
ExpLet. Exp ::= "let" Id ":" Exp ":=" Exp "in" Exp;
|
||
ExpLam. Exp ::= "λ" [BD] "." Exp;
|
||
ExpApp. Exp1 ::= Exp1 Exp2;
|
||
ExpVar. Exp2 ::= Id;
|
||
ExpT0. Exp2 ::= "⊥";
|
||
ExpT1. Exp2 ::= "⊤";
|
||
ExpT1tr. Exp2 ::= "⋆";
|
||
ExpTNat. Exp2 ::= "ℕ";
|
||
ExpTZero. Exp2 ::= "0";
|
||
ExpTSuc. Exp2 ::= "S";
|
||
ExpTBool. Exp2 ::= "𝔹";
|
||
ExpTTrue. Exp2 ::= "T";
|
||
ExpTFalse. Exp2 ::= "F";
|
||
ExpTPair. Exp2 ::= "⟨" Exp "," Exp "⟩";
|
||
ExpTFst. Exp2 ::= "pr₁";
|
||
ExpTSnd. Exp2 ::= "pr₂";
|
||
|
||
VarDef. Def ::= "def" Id ":" Exp ":=" Exp;
|
||
|
||
separator Def ";" ; |