PROGRAM. PROGRAM ::= [SENT] ;
ASentPred. SENT6 ::= PredId [TERMS] ")";
TrueSent. SENT6 ::= "true" ;
FalseSent. SENT6 ::= "false" ;
IdentSent. SENT6 ::= Idents ;
ASentEq. SENT6 ::= TERM "=" TERM ;
NegSent. SENT5 ::= "not" SENT5 ;
IfSent. SENT4 ::= "if" SENT3 "then" SENT3 "else" SENT3 ;
AndSent. SENT3 ::= SENT3 "and" SENT4 ;
OrSent. SENT3 ::= SENT3 "or" SENT4 ;
ImpSent. SENT2 ::= SENT2 "implies" SENT3 ;
LetSent. SENT4 ::= "let" [DEF] "in" SENT2 ;
DefSent. DEF ::= Idents "=" SENT ;
ForallSent. SENT ::= "forall" [TERM] "." SENT ;
ExistsSent. SENT ::= "exists" [TERM] "." SENT ;
FunctTerm. TERM ::= FunctId [TERMS] ")" ;
ConstVarTerm. TERM1 ::= Idents ;
Terms. TERMS ::= [TERM] ;
--separator Idents "," ;
separator TERMS ")(" ;
separator DEF "," ;
terminator SENT ";" ;
coercions SENT 6 ;
coercions TERM 1 ;
separator TERM "," ;
token Idents ((letter)+ (digit)* | (digit)+) ;
-- Note: parents must start right after pred and funct names.
token PredId (upper (letter)* '(' );
token FunctId (lower (letter)* '(');
comment "--" ;