This is an old revision of the document!

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 */;