package guru.hol.parsers.isabelle;
import java_cup.runtime.*;
import guru.hol.ast.*;
import java.util.*;
 
parser code {:
    public void syntax_error(Symbol current) {
        IsabelleParserHelper.getReporter().error("Syntax error", current.left, current.right);
    }
 
    public void unrecovered_syntax_error(Symbol current) {
        IsabelleParserHelper.getReporter().fatalError("Couldn't repair from parsing errors");
    }
:};
 
/* Preliminaries to set up and use the JFlex scanner.  */
init with {: :};
scan with {: return getScanner().next_token(); :};
 
/* Terminals (tokens returned by the scanner). */
terminal           PLUS, TIMES, MINUS, DIV, EQUALS, NEQUALS, AND, OR, ASSIGN;
terminal	       FINITE, CARD, INTERSECTION, UNION, SUBSETEQ, SETMINUS, EMPTYSET;
terminal           GT, LEQ, LT, GEQ, ALL, EX, NOT, EQUIV, IMPLIES, HASTYPE, QUOTES;
terminal           LAMBDA, DOT, LPAREN, RPAREN, BOOL, INT, OBJ, LET, IN, NAT;
terminal           IF, THEN, ELSE;
terminal           LPARR, RPARR;
terminal           TRUE, FALSE;
terminal           EMPTYLIST;
terminal           SET, MULTISET, LIST, FUNCTIONARROW, BACKTICK;
terminal           TYPEANNOT;    // useless if not for precedence
terminal           LCURLYBRACKET, RCURLYBRACKET, LSQUAREBRACKET, RSQUAREBRACKET, COMMA;
terminal           THEORY, BEGIN, END, IMPORTS, DATATYPE, TYPES, RECORD;
terminal           DEFINITION, WHERE, FUN, PRIMREC;
terminal Integer   NUMBER;
terminal String    ID;
 
 
/* Non-terminals */
non terminal TheoryTrees.Theory			        theory;
non terminal TheoryTrees.TheoryTree           	theory_stmt;
non terminal List			                	theory_stmts;
non terminal FormulaTrees.FormulaTree           imports_list;
non terminal FormulaTrees.FormulaTree           imports_thy;
non terminal TheoryTrees.TheoryTree             definition;
non terminal FormulaTrees.Var		            definition_sign;
//non terminal FormulaTrees.FormulaTree           definition_body;
non terminal List                               fun_args;
non terminal TheoryTrees.TheoryTree             fun_def;
non terminal FormulaTrees.Var		            fun_sign;
non terminal List                               fun_eqns;
non terminal FormulaTrees.FormulaTree           fun_eqn;
non terminal TheoryTrees.TheoryTree             types_synonym_def;
non terminal List                               type_synonym_defs;
non terminal TheoryTrees.TypeSynonym            type_synonym_def;
non terminal TheoryTrees.TheoryTree             adt_type_def;
non terminal List                               type_alternatives;
non terminal TheoryTrees.TypeAlternative        type_alternative;
non terminal TypeTrees.TypeTree                 parametric_type;
non terminal List                               type_params;
non terminal List                               cons_arguments;
non terminal TheoryTrees.TheoryTree             record_def;
non terminal FormulaTrees.FormulaTree           field_def;
non terminal List                               field_defs;
non terminal FormulaTrees.FormulaTree           field_update;
non terminal List                               field_updates;
non terminal FormulaTrees.FormulaTree           listnode_update;
non terminal List                               listnode_updates;
non terminal FormulaTrees.FormulaTree           bound_form;
non terminal List                               bound_form_list_comma;
non terminal FormulaTrees.FormulaTree           formula;
non terminal FormulaTrees.FormulaTree           factor;
non terminal FormulaTrees.FormulaTree           set_comp;
non terminal FormulaTrees.FormulaTree           factor_list;
non terminal List                               factor_list_comma;
non terminal FormulaTrees.BoundVar              bound_variable;
non terminal List                               bound_variable_list;
non terminal List                               bound_variable_list_comma;
non terminal TypeTrees.TypeTree                 type;
non terminal TypeTrees.TypeTree                 encapsulated_type;
non terminal TypeTrees.TypeTree                 easy_type;
non terminal                                    empty;
 
/* Precedences */
precedence nonassoc 	EQUIV;
precedence right        IMPLIES;
precedence left         OR;
precedence left         AND;
precedence left         EQUALS;
precedence left         NEQUALS;
 
precedence nonassoc     SUBSETEQ;
precedence left         SETMINUS;
precedence left         UNION;
precedence left         INTERSECTION;
 
precedence nonassoc     GT, LEQ, LT, GEQ;
precedence left         PLUS, MINUS;
precedence left         TIMES, DIV;
precedence left         NOT;
 
precedence nonassoc     HASTYPE;
 
precedence right        FUNCTIONARROW;
precedence left         TYPEANNOT;
/* The grammar */
start with theory;
 
theory           ::= THEORY ID:name imports_list BEGIN theory_stmts:defs END
		             {: RESULT = ASTFactory.makeIsabelleTheory(name, defs); :}
                  |  bound_form : f                 // keep this line to allow formulas to be parsed directly
                     {: RESULT = ASTFactory.makeSingleFormulaTheory(f); :}
                  ;
 
/* ------- Parsing Outer Theory ----------------------------------------------- */
 
imports_list     ::= IMPORTS imports_thy | empty;
imports_thy      ::= imports_thy ID | ID;
 
theory_stmts     ::= theory_stmt:st
                     {: List list = new LinkedList(); list. add(st); RESULT = list; :}
                  |  theory_stmts:sts theory_stmt:st
                     {: sts.add(st); RESULT = sts; :}
                  ;
 
theory_stmt      ::= definition:df
                     {: RESULT = df; :}
                  |  fun_def:pr
                     {: RESULT = pr; :} 
                  |  adt_type_def:adt
                     {: RESULT = adt; :}
                  |  types_synonym_def:td
                     {: RESULT = td; :}
                  |  record_def:rd
                     {: RESULT = rd; :}
                  ;
 
definition       ::= DEFINITION fun_sign:sgn WHERE fun_eqn:fe
                     {: RESULT = ASTFactory.makeNonrecFunDefinition(sgn, sgn.getType(), fe); :}   
                  ;
 
fun_args         ::= empty
                     {: RESULT = new LinkedList(); :}
//                  |  fun_args:fns factor:f
//                     {: fns.add(f); RESULT = fns; :}
                  |  fun_args:fns bound_variable:bv
                     {: fns.add(bv); RESULT = fns; :}
                  ;             
 
fun_def          ::= FUN fun_sign:sgn WHERE fun_eqns:fes
                     {: RESULT = ASTFactory.makeFunDefinition(sgn, sgn.getType(), fes); :}
                  ;
 
fun_sign         ::= ID:id HASTYPE encapsulated_type:t
                     {: FormulaTrees.Var v = ASTFactory.makeVar(id, idleft, idright); v.setType(t); RESULT = v; :}
                  ;
 
fun_eqns         ::= fun_eqn:fe
                     {: List list = new LinkedList(); list.add(fe); RESULT = list; :}
                  |  fun_eqns:fes OR fun_eqn:fe
                     {: fes.add(fe); RESULT = fes; :}
                  ;  
 
fun_eqn          ::= QUOTES ID:fun fun_args:fs EQUALS bound_form:f QUOTES
                     {: if( fs.size() != 0) RESULT = ASTFactory.makeLambdaAbstractions(fs,f,funleft,funright); else RESULT = f; :}                  
                  |  QUOTES ID:fun fun_args:fs EQUIV bound_form:f QUOTES
                     {: if( fs.size() != 0) RESULT = ASTFactory.makeLambdaAbstractions(fs,f,funleft,funright); else RESULT = f; :}
                  ;   
 
adt_type_def     ::= DATATYPE ID:id EQUALS type_alternatives:tals
                     {: RESULT = ASTFactory.makeAdtTypeDefinition( new LinkedList(), id, tals); :}
                  |   DATATYPE type_params:tps ID:id EQUALS type_alternatives:tals
                     {: RESULT = ASTFactory.makeAdtTypeDefinition( tps, id, tals); :}
                  ;
 
type_alternatives::= type_alternative:ta
                     {: List list = new LinkedList(); list. add(ta); RESULT = list; :}
                  |  type_alternatives:tas OR type_alternative:ta
                     {: tas.add(ta); RESULT = tas; :}
                  ;
 
type_alternative ::= ID:id cons_arguments:ca
                     {: RESULT = ASTFactory.makeTypeAlternative(id,ca); :}
                  ;
 
cons_arguments   ::= empty
                  {: RESULT = new LinkedList(); :}
                  |  cons_arguments:cas encapsulated_type:et
                     {: cas.add(et); RESULT = cas; :} 
                  ;
 
types_synonym_def::= TYPES:typ type_synonym_defs:t
                  {: RESULT = ASTFactory.makeTypeSynonymDefinition( t, typleft, typright); :}
                  ;
 
type_synonym_defs::= type_synonym_def:t
                     {: List list = new LinkedList(); list.add(t); RESULT = list; :}
                  |  type_synonym_defs:ts type_synonym_def:t
                     {: ts.add(t); RESULT = ts; :}
                  ;
 
type_synonym_def ::= ID:id EQUALS encapsulated_type:et
                     {: RESULT = ASTFactory.makeTypeSynonym(id, et); :}
                  ;                     
 
record_def       ::= RECORD ID:id EQUALS field_defs:fds
                     {: RESULT = ASTFactory.makeRecordDefinition(id,fds,idleft,idright); :}
                  ;
 
field_defs       ::= field_def:f
                     {: List list = new LinkedList(); list.add(f); RESULT = list; :}
                  |  field_defs:fs field_def:f
                     {: fs.add(f); RESULT = fs; :}
                  ;
 
field_def        ::= ID:id HASTYPE encapsulated_type:t
                     {: FormulaTrees.Var v = ASTFactory.makeVar(id, idleft, idright); v.setType(t); RESULT = v; :}
                  ;
 
/* ------------ Parsing Formulas (and Types) -------------------------- */
 
 
bound_variable   ::= ID:id
                     {: RESULT = ASTFactory.makeBoundVar(id, idleft, idright); :}
                  |  ID:id HASTYPE type:t
                     {: FormulaTrees.BoundVar v = ASTFactory.makeBoundVar(id, idleft, idright); v.setType(t); RESULT = v; :}
                  |  LPAREN bound_variable_list_comma:blc RPAREN
                     {: RESULT = ASTFactory.makeBoundVarTuple(blc,blcleft,blcright); :}
                  |  LPAREN ID:id error RPAREN
                  ;
 
bound_variable_list_comma ::= bound_variable:v
                     {: List list = new LinkedList(); list.add(v); RESULT = list; :}
                  |  bound_variable_list_comma:blc COMMA bound_variable:v
                     {: blc.add(v); RESULT = blc; :}
                  ;
 
bound_variable_list  ::= bound_variable:v
                     {: List list = new LinkedList(); list.add(v); RESULT = list; :}
                  |  bound_variable_list:bvs bound_variable:v
                     {: bvs.add(v); RESULT = bvs; :}
                  ;
 
bound_form       ::= LAMBDA:p bound_variable_list:bvs DOT bound_form:f
                     {: RESULT = ASTFactory.makeLambdaAbstractions(bvs,f,pleft,pright); :}
                  |  ALL:p bound_variable_list:bvs DOT bound_form:f
                     {: RESULT = ASTFactory.makeUniversals(bvs,f,pleft,pright); :}
                  |  EX:p bound_variable_list:bvs DOT bound_form:f
                     {: RESULT = ASTFactory.makeExistentials(bvs,f,pleft,pright); :}
                  |  formula:f
                     {: RESULT = f; :}
                  |  LPAREN bound_form:f HASTYPE type:t RPAREN
                     {: FormulaTrees.FormulaTree r = f; r.setType(t); RESULT = r; :}
                  |  LET:p bound_variable:bv EQUALS bound_form:f1 IN bound_form:f2
                     {: RESULT = ASTFactory.makeLet(bv, f1, f2, pleft, pright); :}
                  |  IF bound_form:cond THEN bound_form:st1 ELSE bound_form:st2
                     {: RESULT = ASTFactory.makeConditional( cond, st1, st2); :}
                  ;
 
bound_form_list_comma  ::= bound_form:f
	                 {: List list = new LinkedList(); list.add(f); RESULT = list; :}
                  |  bound_form_list_comma:fs COMMA bound_form:f
                    {: fs.add(f); RESULT = fs; :}
                  ;                  
 
formula          ::= formula:f1 IMPLIES:p formula:f2 
                     {: RESULT = ASTFactory.makeImplies(f1, f2, pleft, pright); :}
                  |  formula:f1 OR:p formula:f2 
                     {: RESULT = ASTFactory.makeOr(f1, f2, pleft, pright); :}
                  |  formula:f1 AND:p formula:f2 
                     {: RESULT = ASTFactory.makeAnd(f1, f2, pleft, pright); :}
                  |  formula:f1 SUBSETEQ:p formula:f2 
                     {: RESULT = ASTFactory.makeSubseteq(f1, f2, pleft, pright); :}
                  |  formula:f1 UNION:p formula:f2 
                     {: RESULT = ASTFactory.makeUnion(f1, f2, pleft, pright); :}
                  |  formula:f1 INTERSECTION:p formula:f2 
                     {: RESULT = ASTFactory.makeIntersection(f1, f2, pleft, pright); :}
                  |  formula:f1 SETMINUS:p formula:f2 
                     {: RESULT = ASTFactory.makeSetminus(f1, f2, pleft, pright); :}
                  |  formula:f1 EQUALS:p formula:f2 
                     {: RESULT = ASTFactory.makeEquals(f1, f2, pleft, pright); :}
                  |  formula:f1 NEQUALS:p formula:f2
                     {: RESULT = ASTFactory.makeNEquals(f1, f2, pleft, pright); :}
                  |  formula:f1 LT:p formula:f2 
                     {: RESULT = ASTFactory.makeLessThan(f1, f2, pleft, pright); :}
                  |  formula:f1 LEQ:p formula:f2 
                     {: RESULT = ASTFactory.makeLessEquals(f1, f2, pleft, pright); :}
                  |  formula:f1 GT:p formula:f2 
                     {: RESULT = ASTFactory.makeGreaterThan(f1, f2, pleft, pright); :}
                  |  formula:f1 GEQ:p formula:f2 
                     {: RESULT = ASTFactory.makeGreaterEquals(f1, f2, pleft, pright); :}
                  |  formula:f1 PLUS:p formula:f2 
                     {: RESULT = ASTFactory.makePlus(f1, f2, pleft, pright); :}
                  |  formula:f1 MINUS:p formula:f2 
                     {: RESULT = ASTFactory.makeMinus(f1, f2, pleft, pright); :}
                  |  formula:f1 TIMES:p formula:f2 
                     {: RESULT = ASTFactory.makeTimes(f1, f2, pleft, pright); :}
                  |  formula:f1 DIV:p formula:f2
                     {: RESULT = ASTFactory.makeDiv(f1, f2, pleft, pright); :}
                  |  NOT:p formula:f
                     {: RESULT = ASTFactory.makeNot(f, pleft, pright); :} %prec NOT 
                  |  factor_list:f
                     {: RESULT = f; :}
                  ;
 
factor           ::= ID:id
                     {: RESULT = ASTFactory.makeVar(id, idleft, idright); :}
                  |  CARD:p
	                 {: RESULT = ASTFactory.makeCardConst(pleft, pright); :}
                  |  FINITE:p
	                 {: RESULT = ASTFactory.makeFiniteConst(pleft, pright); :}
                  |  EMPTYSET:p
                     {: RESULT = ASTFactory.makeEmptySetConst(pleft, pright); :}
                  |  EMPTYLIST:p
                     {: RESULT = ASTFactory.makeListNilConst(pleft, pright); :}
                  |  set_comp:sc
                     {: RESULT = sc; :} 
                  |  NUMBER:n
                     {: RESULT = ASTFactory.makeIntConst(n.intValue(), nleft, nright); :}
                  |  TRUE:t
                     {: RESULT = ASTFactory.makeBoolConst(true, tleft, tright); :}
                  |  FALSE:t
                     {: RESULT = ASTFactory.makeBoolConst(false, tleft, tright); :}                     
                  |  LPAREN bound_form_list_comma:fs RPAREN                    
                     {: if( fs.size() == 1) RESULT = (FormulaTrees.FormulaTree) fs.get(0); 
                        else RESULT = ASTFactory.makeTuple(fs, fsleft, fsright); :} 
                  |  LPAREN error RPAREN
                  ;
 
factor_list      ::= factor:f
                     {: RESULT = f; :}
	              |  factor_list:fl factor:f
                     {: RESULT = ASTFactory.makeApply(fl, f); :}
	              |  factor_list:fl LPAREN factor ASSIGN factor_list RPAREN               // function update
                     {: RESULT = fl; :} // FIX
                  |  factor_list:fl LPARR field_updates:fus RPARR                         // record update
                     {: RESULT = ASTFactory.makeRecordUpdate( fl, fus); :}
                  |  factor_list:fl LSQUAREBRACKET listnode_updates:lus RSQUAREBRACKET         // list update
                     {: RESULT = ASTFactory.makeListUpdate( fl, lus); :}
	              ;                  
 
factor_list_comma::= factor:f
                     {: List list = new LinkedList(); list.add(f); RESULT = list; :}
		          |  factor_list_comma:fs COMMA factor:f
                     {: fs.add(fs); RESULT = fs; :}
		          ;
 
set_comp         ::= LCURLYBRACKET bound_variable:v DOT bound_form:f RCURLYBRACKET // set of v such that f
                     {: RESULT = ASTFactory.makeLambdaAbstraction(v, f); :}
		          // |  LCURLYBRACKET factor_list_comma:elems RCURLYBRACKET    // finite set containing elems
		          // {: RESULT = ASTFactory.makeSetConst(elems); :}  
		          // {: RESULT = elems; :} // FIX
                  ;
 
field_updates    ::= field_update:fu
                     {: List list = new LinkedList(); list.add(fu); RESULT = list; :}
                  |  field_updates:fus COMMA field_update:fu
                     {: fus.add(fu); RESULT = fus; :}
                  ;
 
field_update     ::= ID:id ASSIGN bound_form:f
                     {: RESULT = ASTFactory.makeFieldUpdate(id, f, idleft, idright); :}
                  ;
 
listnode_updates ::= listnode_update:lu
                     {: List list = new LinkedList(); list.add(lu); RESULT = list; :}
                  |  listnode_updates:lus COMMA listnode_update:lu
                     {: lus.add(lu); RESULT = lus; :}
                  ;                  
 
listnode_update  ::= factor:pos ASSIGN bound_form:f
                     {: RESULT = ASTFactory.makeListNodeUpdate(pos, f, posleft, posright); :}
                  ;
 
encapsulated_type::= QUOTES type:t QUOTES
                     {: RESULT = t; :}
                  |  easy_type:t
                     {: RESULT = t; :}
                  ;
 
type             ::= easy_type:t
                     {: RESULT = t; :}
                  |  BACKTICK ID:id
                     {: RESULT = ASTFactory.makeVarType(id, idleft, idright); :}
                  |  type:t1 TIMES:p type:t2
                     {: RESULT = ASTFactory.makePairType(t1, t2, pleft, pright); :}
                  |  type:t1 FUNCTIONARROW:p type:t2
                     {: RESULT = ASTFactory.makeFunctionType(t1, t2, pleft, pright); :}
                  |  parametric_type:pt
                     {: RESULT = pt; :}
//                  |  QUOTES type:t QUOTES
//                     {: RESULT = t; :}
                  |  LPAREN error RPAREN                     
                  ;
 
easy_type        ::= ID:id
                     {: RESULT = ASTFactory.makeNamedType(id, idleft, idright); :}
                  |  OBJ:p
                     {: RESULT = ASTFactory.makeObjType(pleft, pright); :}
                  |  BOOL:p
                     {: RESULT = ASTFactory.makeBoolType(pleft, pright); :}
                  |  INT:p
                     {: RESULT = ASTFactory.makeIntType(pleft, pright); :}
                  |  NAT:p
                     {: RESULT = ASTFactory.makeIntType(pleft, pright); :}                     
                  ;
 
parametric_type  ::= LPAREN type_params:tps RPAREN ID:id     // type with more than one parameters
                     {: RESULT = ASTFactory.makeParametricType(tps,id,idleft,idright); :}
                  |  LPAREN type_params:tps RPAREN SET:s
                     {: RESULT = ASTFactory.makeSetType((TypeTrees.TypeTree)tps.get(0), sleft, sright); :}                  
                  |  LPAREN type_params:tps RPAREN LIST:l
                     {: RESULT = ASTFactory.makeListType((TypeTrees.TypeTree)tps.get(0), lleft, lright); :}                     
                  |  type:t ID:id 
                     {: List list = new LinkedList(); list.add(t); RESULT = ASTFactory.makeParametricType(list,id,idleft,idright); :} %prec TYPEANNOT
                  |  type:t SET:p
                     {: RESULT = ASTFactory.makeSetType(t, pleft, pright); :} %prec TYPEANNOT
                  |  type:t LIST:p
                     {: RESULT = ASTFactory.makeListType(t, pleft, pright); :} %prec TYPEANNOT
                  |  type:t MULTISET:p
                     {: RESULT = ASTFactory.makeMultisetType(t, pleft, pright); :} %prec TYPEANNOT
                  ;
 
type_params      ::= type:t
                     {: List list = new LinkedList(); list.add(t); RESULT = list; :} %prec TYPEANNOT
                  |  type_params:tps COMMA type:t 
                     {: tps.add(t); RESULT = tps; :} %prec TYPEANNOT
                  ;
 
empty            ::= /* nothing */;