F.2 Syntactical Grammar

F.2 Syntactical Grammar

// parsing of a declaration or prover command
main:
  declaration SEMICOLON
| "tcc" SEMICOLON 
| "prove" IDENT SEMICOLON
| "flip" LABEL SEMICOLON
| "goal" LABEL SEMICOLON
| "skolemize" SEMICOLON
| "flatten" SEMICOLON
| "split" ( LABEL )? SEMICOLON
| "decompose" SEMICOLON
| "simplify" ( LABEL )? SEMICOLON
| "scatter" SEMICOLON
| "auto" ( LABEL ( ","  LABEL )* )? SEMICOLON
| "autostar" SEMICOLON
| "counterexample" SEMICOLON
| "assume" valueExp SEMICOLON
| "case" valueExp ( ","  valueExp )* SEMICOLON
| "lemma" IDENT ( "," IDENT )* SEMICOLON
| "instantiate" valueExp ( ","  valueExp  )* 
    "in" LABEL SEMICOLON
| "typeaxiom" valueExp ( ","  valueExp  )* 
    "in" IDENT SEMICOLON
| "expand" IDENT ( "," IDENT )* 
    ( "in" LABEL ( "," LABEL )* )? SEMICOLON
| "induction" ( IDENT ( "in" LABEL )? )? SEMICOLON
| "open" SEMICOLON
| "next" SEMICOLON
| "prev" SEMICOLON
| "goto" LABEL SEMICOLON
| "undo" ( LABEL )? SEMICOLON
| "redo" ( LABEL )? SEMICOLON
| "environment" SEMICOLON
| "proof" ( IDENT )? SEMICOLON
| "state" ( LABEL ( IDENT )? )? SEMICOLON
| "type" IDENT SEMICOLON
| "value" IDENT SEMICOLON
| "formula" IDENT SEMICOLON
| "quit" SEMICOLON
| "read" STRING SEMICOLON
| "option" IDENT ( "=" STRING )? SEMICOLON
| "newcontext" ( STRING )? SEMICOLON
| SEMICOLON
| EOF
;

declaration:
  IDENT ":"
  ( "TYPE" ( "=" typeExp )?
  | typeExp ( "=" valueExp )?
  | "FORMULA" valueExp 
  | "AXIOM" valueExp 
  )
;

typeExp:
  typeExpBase "->" typeExp
| "(" typeExp ( ","  typeExp )+  )" "->" typeExp
| "ARRAY" typeExpBase "OF" typeExp
| typeExpBase
;
  
typeExpBase:
  IDENT
| "BOOLEAN" 
| "INT"  
| "NAT"  
| "REAL" 
| "[" typeExp ( ","  typeExp )+  "]" 
| "[" typeExp "]"
| "[#" IDENT ":" typeExp ( "," IDENT ":" typeExp )* "#]"
| "SUBTYPE" "(" valueExp ")"
| "[" valueExp ".." valueExp "]"
| "(" typeExp ")"
;

valueExp:
  "LAMBDA" paramList ":" valueExp
| "ARRAY" paramList ":" valueExp
| "FORALL" paramList ":" valueExp
| "EXISTS" paramList ":" valueExp
| valueExp90
;

vdeclaration:
  IDENT ( ":" typeExp )? "=" valueExp 
;
  	    
valueExp90:
  "LET" vdeclaration ( "," vdeclaration )* "IN" valueExp90
| valueExp70
;

valueExp70:
  valueExp60 "=>" valueExp70
| valueExp60 ( "<=>" valueExp70 | "XOR" valueExp70 )*
;

valueExp60:
  valueExp50 ( "OR" valueExp60 )*
;

valueExp50:
  valueExp45 ( "AND" valueExp50 )*
;

valueExp45:
  "NOT" valueExp45
| valueExp43
;

valueExp43:
  valueExp40 ( "=" valueExp43 | "/=" valueExp43 )?
;

valueExp40:
  valueExp30 
  ( "<" valueExp40 | "<=" valueExp40 | 
    ">" valueExp40 | ">=" valueExp40 )?
;

valueExp30:
  valueExp10 ( "+" valueExp30 | "-" valueExp30 )*
;

valueExp10:
  valueExp9 ( "*" valueExp9 | "/" valueExp9 )*
;

valueExp9:
  valueExp8 ( "^" valueExp8 )*
;

valueExp8:
  "+" valueExp6
| "-" valueExp6
| valueExp6
;

valueExp6:
  valueExp5
  ( "WITH" ( "." ( NUMBER | IDENT ) | "[" valueExp "]" )+ 
  ":=" valueExp )*

valueExp5:
  valueExp3
  ( 
    "." ( NUMBER | IDENT )
  | "[" valueExp "]"
  )*
;

valueExp3:
  valueExp0 ( "(" valueExp ( "," valueExp  )* ")" )*
;

valueExp0:
  IDENT
| UNDERSCORE
| NUMBER
| "TRUE"
| "FALSE"
| "(" valueExp ( ","  valueExp )* ")"
| "(#" IDENT ":=" valueExp ( "," IDENT ":=" valueExp )* "#)"
| "IF" valueExp "THEN" valueExp 
  ( "ELSIF" valueExp "THEN" valueExp )* 
  "ELSE" valueExp "ENDIF"
;

paramList:
  "(" param ( "," param )* ")" 
;

param: 
  IDENT ( "," IDENT )* ":" typeExp
;

F.2 Syntactical Grammar