/* Precedences */

%nonassoc IN
%nonassoc prec_forall prec_exists
%right ARROW LRARROW
%right OR
%right AND 
%nonassoc prec_ite
%left prec_relation EQUAL NOTEQ LT LE GT GE
%left PLUS MINUS
%left TIMES SLASH PERCENT AT
%nonassoc HAT
%nonassoc uminus
%nonassoc NOT
%right prec_named
%left LEFTSQ


file:
| list1_decl EOF 
| EOF 

list1_decl:
| decl 
| decl list1_decl 


decl:
| TYPE ident
| TYPE type_var ident
| TYPE LEFTPAR list1_type_var_sep_comma RIGHTPAR ident
| LOGIC ac_modifier list1_ident_sep_comma COLON logic_type
| FUNCTION ident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR COLON 
  primitive_type EQUAL lexpr
| PREDICATE ident EQUAL lexpr
| PREDICATE ident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR EQUAL lexpr
| AXIOM ident COLON lexpr
| GOAL ident COLON lexpr


ac_modifier:
  /* epsilon */ 
| AC    

primitive_type:
| INT 
| BOOL 
| REAL 
| UNIT 
| BITV LEFTSQ INTEGER RIGHTSQ
| ident 
| type_var 
| primitive_type ident
| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR ident
| primitive_type FARRAY 

logic_type:
| list0_primitive_type_sep_comma ARROW PROP
| PROP
| list0_primitive_type_sep_comma ARROW primitive_type
| primitive_type

list1_primitive_type_sep_comma:
| primitive_type
| primitive_type COMMA list1_primitive_type_sep_comma

list0_primitive_type_sep_comma:
| /* epsilon */                  
| list1_primitive_type_sep_comma 

list0_logic_binder_sep_comma:
| /* epsilon */                
| list1_logic_binder_sep_comma 

list1_logic_binder_sep_comma:
| logic_binder                                    
| logic_binder COMMA list1_logic_binder_sep_comma 

logic_binder:
| ident COLON primitive_type       

lexpr:
/* constants */
| INTEGER
| NUM
| TRUE
| FALSE
| VOID 

/* binary operators */
| lexpr PLUS lexpr
| lexpr MINUS lexpr
| lexpr TIMES lexpr
| lexpr SLASH lexpr
| lexpr PERCENT lexpr
| lexpr AND lexpr 
| lexpr OR lexpr 
| lexpr LRARROW lexpr 
| lexpr ARROW lexpr 
| lexpr relation lexpr %prec prec_relation

/* unary operators */
| NOT lexpr 
| MINUS lexpr %prec uminus

/* bit vectors */
| LEFTSQ BAR INTEGER BAR RIGHTSQ
| lexpr HAT LEFTBR INTEGER COMMA INTEGER RIGHTBR
| lexpr AT lexpr

/* arrays */
| lexpr LEFTSQ lexpr RIGHTSQ
| lexpr LEFTSQ array_assignements RIGHTSQ

/* predicate or function calls */
| ident
| ident LEFTPAR list0_lexpr_sep_comma RIGHTPAR 
| IF lexpr THEN lexpr ELSE lexpr %prec prec_ite
| FORALL list1_ident_sep_comma COLON primitive_type triggers 
  DOT lexpr %prec prec_forall
| EXISTS ident COLON primitive_type DOT lexpr %prec prec_exists
| ident_or_string COLON lexpr %prec prec_named
| LET ident EQUAL lexpr IN lexpr
| LEFTPAR lexpr RIGHTPAR

array_assignements:
| array_assignement
| array_assignement COMMA array_assignements

array_assignement:
|  lexpr LEFTARROW lexpr

triggers:
| /* epsilon */ 
| LEFTSQ list1_trigger_sep_bar RIGHTSQ

list1_trigger_sep_bar:
| trigger
| trigger BAR list1_trigger_sep_bar

trigger:
  list1_lexpr_sep_comma

list0_lexpr_sep_comma:
| /*empty */                        
| lexpr                             
| lexpr COMMA list1_lexpr_sep_comma 

list1_lexpr_sep_comma:
| lexpr                             
| lexpr COMMA list1_lexpr_sep_comma 

relation:
| LT 
| LE 
| GT 
| GE 
| EQUAL 
| NOTEQ 

type_var:
| QUOTE ident 

list1_type_var_sep_comma:
| type_var                                
| type_var COMMA list1_type_var_sep_comma 

ident:
| IDENT

list1_ident_sep_comma:
| ident                             
| ident COMMA list1_ident_sep_comma 

ident_or_string:
| IDENT  
| STRING