//---------------------------------------------------- // The following code was generated by jh-javacup-1.2 20210807 // Sun Oct 27 17:47:59 CET 2024 //---------------------------------------------------- package de.uni_freiburg.informatik.ultimate.crocotta.parser; import java.io.IOException; import java.io.InputStream; import java.io.Reader; import com.github.jhoenicke.javacup.runtime.Symbol; import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider; import de.uni_freiburg.informatik.ultimate.crocotta.ast.Concatenation; import de.uni_freiburg.informatik.ultimate.crocotta.ast.Event; import de.uni_freiburg.informatik.ultimate.crocotta.ast.FinInfExpression; import de.uni_freiburg.informatik.ultimate.crocotta.ast.FixpointQuery; import de.uni_freiburg.informatik.ultimate.crocotta.ast.InclusionQuery; import de.uni_freiburg.informatik.ultimate.crocotta.ast.Intersection; import de.uni_freiburg.informatik.ultimate.crocotta.ast.LanguageExpression; import de.uni_freiburg.informatik.ultimate.crocotta.ast.Numeral; import de.uni_freiburg.informatik.ultimate.crocotta.ast.Query; import de.uni_freiburg.informatik.ultimate.crocotta.ast.Union; /** jh-javacup-1.2 20210807 generated parser. * @version Sun Oct 27 17:47:59 CET 2024 */ public class CrocParser extends com.github.jhoenicke.javacup.runtime.LRParser { /** Default constructor. */ public CrocParser() {super();} /** Constructor which sets the default scanner. */ public CrocParser(com.github.jhoenicke.javacup.runtime.Scanner s) {super(s);} /** Constructor which sets the default scanner. */ public CrocParser(com.github.jhoenicke.javacup.runtime.Scanner s, com.github.jhoenicke.javacup.runtime.SymbolFactory sf) {super(s,sf);} /** The static parse table */ static com.github.jhoenicke.javacup.runtime.ParseTable CUP$parse_table = new com.github.jhoenicke.javacup.runtime.ParseTable(new String[] { "\042\000\002\004\002\005\005\005\005\002\001" + "\002\001\002\003\002\003\002\003\002\003\003" + "\003\001\001\001\001\001\003\007\000\006\001" + "\006\002\047\051\047\061\u0123\047\067\047\047" + "\115\u0107\353\317\047\263\077\047\047\055\051" + "\047\075\227\047\173\137\053\075\103\047\047" + "\047\047\047\047\047\071\067\047\047\u0145\000" + "\000\000\000\040\004\004\002\000\000\000\000" + "\030\000\000\032\012\000\014\042\000\000\014" + "\000\000\000\000\000\000\026\016\020\022\024" + "\034\000\000\010\006\047\001\001\036\034\021" + "\034\023\034\025\034\027\002\017\000\003\022" + "\071\034\031\034\033\021\067\001\007\031\103" + "\034\035\034\037\033\021\033\023\033\025\033" + "\027\005\007\044\115\043\113\033\031\033\033" + "\032\105\024\073\016\065\033\035\033\037\030" + "\021\030\023\030\025\030\027\010\051\047\001" + "\047\001\030\031\030\033\047\001\047\001\047" + "\001\030\035\030\037\027\021\027\023\027\025" + "\027\027\047\001\047\001\047\001\027\031\027" + "\033\047\001\047\001\047\001\027\035\027\037" + "\025\021\025\023\025\025\025\027\047\001\047" + "\001\047\001\025\031\025\033\047\001\047\001" + "\047\001\025\035\025\037\015\021\015\023\015" + "\025\015\027\047\001\047\001\047\001\015\031" + "\015\033\047\001\047\001\047\001\015\035\015" + "\037\013\021\013\023\013\025\013\027\047\001" + "\047\001\047\001\013\031\013\033\047\001\047" + "\001\047\001\013\035\013\037\012\021\012\023" + "\012\025\012\027\047\001\047\001\047\001\012" + "\031\012\033\047\001\047\001\047\001\012\035" + "\012\037\011\021\011\023\011\025\011\027\047" + "\001\047\001\047\001\011\031\011\033\047\001" + "\047\001\047\001\011\035\011\037\003\021\003" + "\023\003\025\003\027\047\001\047\001\047\001" + "\003\031\003\033\047\001\047\001\047\001\003" + "\035\003\037\047\001\065\000\055\001\056\002" + "\007\020\044\026\053\050\045\023\042\020\043" + "\026\020\040\026\001\037\001\034\020\001\001" + "\015\005\020\037\026\020\036\026\020\031\026" + "\020\030\026\020\027\026\020\025\026\020\021" + "\022\004\005\006" }); /** Return parse table */ protected com.github.jhoenicke.javacup.runtime.ParseTable parse_table() { return CUP$parse_table; } /** Instance of action encapsulation class. */ protected Action$ action_obj; /** Action encapsulation object initializer. */ protected void init_actions() { action_obj = new Action$(this); } /** Invoke a user supplied parse action. */ public com.github.jhoenicke.javacup.runtime.Symbol do_action( int act_num, java.util.ArrayList stack) throws java.lang.Exception { /* call code in generated class */ return action_obj.CUP$do_action(act_num, stack); } /** Scan to get the next Symbol. */ public com.github.jhoenicke.javacup.runtime.Symbol scan() throws java.lang.Exception { return getScanner().next_token(); } private IUltimateServiceProvider mServices; private String mFilename; private ILogger mLogger; public CrocParser(final IUltimateServiceProvider services, final ILogger logger, final Reader reader, final String filename) throws IOException { this(new CrocLexer(reader)); mServices = services; mLogger = logger; mFilename = filename; } public CrocParser(final IUltimateServiceProvider services, final ILogger logger, final InputStream stream, final String filename) throws IOException { this(new CrocLexer(stream)); mServices = services; mLogger = logger; mFilename = filename; } @Override public void report_error(final String s, final Object sym) { String location; if (sym instanceof CrocSymbolFactory.LineColumnSymbol) { final CrocSymbolFactory.LineColumnSymbol bsym = (CrocSymbolFactory.LineColumnSymbol) sym; location = bsym.getLocation(); } else if ((sym instanceof Symbol) && ((Symbol) sym).sym == CrocSymbols.EOF) { location = "EOF"; } else { location = "UNKNOWN"; } final String filename = mFilename == null ? "" : (mFilename + ":"); mLogger.error(filename + location + ": " + s); } public void report_error(final String s) { report_error(s, cur_token); } @Override public void syntax_error(final Symbol sym) { report_error("Syntax Error", sym); } /** Cup generated class to encapsulate user supplied action code.*/ static class Action$ { private final CrocParser parser; /** Constructor */ Action$(CrocParser parser) { this.parser = parser; } /** Method with the actual generated action code. */ @SuppressWarnings({ "unused", "unchecked" }) public final com.github.jhoenicke.javacup.runtime.Symbol CUP$do_action( int CUP$act_num, java.util.ArrayList CUP$stack) throws java.lang.Exception { /* Stack size for peeking into the stack */ int CUP$size = CUP$stack.size(); /* select the action based on the action number */ switch (CUP$act_num) { // $START ::= goal EOF case 0: { Object RESULT; com.github.jhoenicke.javacup.runtime.Symbol CUP$rhs$ = CUP$stack.get(CUP$size - 2); Query[] CUP$rhs = (Query[]) CUP$rhs$.value; RESULT = CUP$rhs; /* ACCEPT */ parser.done_parsing(); return parser.getSymbolFactory().newSymbol("$START", 0, CUP$rhs$, CUP$stack.get(CUP$size - 1), RESULT); } // goal ::= CONSTRAINTS constraint* case 1: { Query[] RESULT; com.github.jhoenicke.javacup.runtime.Symbol s$ = CUP$stack.get(CUP$size - 1); java.util.ArrayList CUP$list$s = (java.util.ArrayList) s$.value; Query[] s = CUP$list$s.toArray(new Query[CUP$list$s.size()]); RESULT = s; return parser.getSymbolFactory().newSymbol("goal", 4, CUP$stack.get(CUP$size - 2), s$, RESULT); } // constraint ::= LBRAK fininfpair EQUALS langExpr RBRAK case 2: { Query RESULT; com.github.jhoenicke.javacup.runtime.Symbol e$ = CUP$stack.get(CUP$size - 2); LanguageExpression e = (LanguageExpression) e$.value; com.github.jhoenicke.javacup.runtime.Symbol fip$ = CUP$stack.get(CUP$size - 4); FinInfExpression fip = (FinInfExpression) fip$.value; RESULT = new FixpointQuery(fip, e); return parser.getSymbolFactory().newSymbol("constraint", 5, CUP$stack.get(CUP$size - 5), CUP$stack.get(CUP$size - 1), RESULT); } // constraint ::= LBRAK langExpr INCLUSION langExpr RBRAK case 3: { Query RESULT; com.github.jhoenicke.javacup.runtime.Symbol e2$ = CUP$stack.get(CUP$size - 2); LanguageExpression e2 = (LanguageExpression) e2$.value; com.github.jhoenicke.javacup.runtime.Symbol e1$ = CUP$stack.get(CUP$size - 4); LanguageExpression e1 = (LanguageExpression) e1$.value; RESULT = new InclusionQuery(e1, e2); return parser.getSymbolFactory().newSymbol("constraint", 5, CUP$stack.get(CUP$size - 5), CUP$stack.get(CUP$size - 1), RESULT); } // langExpr ::= specConstant case 4: { LanguageExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol s$ = CUP$stack.get(CUP$size - 1); LanguageExpression s = (LanguageExpression) s$.value; RESULT = s; return parser.getSymbolFactory().newSymbol("langExpr", 2, s$, s$, RESULT); } // langExpr ::= fininfpair case 5: { LanguageExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol fip$ = CUP$stack.get(CUP$size - 1); FinInfExpression fip = (FinInfExpression) fip$.value; RESULT = fip; return parser.getSymbolFactory().newSymbol("langExpr", 2, fip$, fip$, RESULT); } // langExpr ::= CONCAT langExpr langExpr case 6: { LanguageExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol e2$ = CUP$stack.get(CUP$size - 1); LanguageExpression e2 = (LanguageExpression) e2$.value; com.github.jhoenicke.javacup.runtime.Symbol e1$ = CUP$stack.get(CUP$size - 2); LanguageExpression e1 = (LanguageExpression) e1$.value; RESULT = new Concatenation(new LanguageExpression[]{e1, e2}); return parser.getSymbolFactory().newSymbol("langExpr", 2, CUP$stack.get(CUP$size - 3), e2$, RESULT); } // langExpr ::= UNION langExpr langExpr case 7: { LanguageExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol e2$ = CUP$stack.get(CUP$size - 1); LanguageExpression e2 = (LanguageExpression) e2$.value; com.github.jhoenicke.javacup.runtime.Symbol e1$ = CUP$stack.get(CUP$size - 2); LanguageExpression e1 = (LanguageExpression) e1$.value; RESULT = new Union(new LanguageExpression[]{e1, e2}); return parser.getSymbolFactory().newSymbol("langExpr", 2, CUP$stack.get(CUP$size - 3), e2$, RESULT); } // langExpr ::= ISECT langExpr langExpr case 8: { LanguageExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol e2$ = CUP$stack.get(CUP$size - 1); LanguageExpression e2 = (LanguageExpression) e2$.value; com.github.jhoenicke.javacup.runtime.Symbol e1$ = CUP$stack.get(CUP$size - 2); LanguageExpression e1 = (LanguageExpression) e1$.value; RESULT = new Intersection(new LanguageExpression[]{e1, e2}); return parser.getSymbolFactory().newSymbol("langExpr", 2, CUP$stack.get(CUP$size - 3), e2$, RESULT); } // langExpr ::= LPAR langExpr RPAR case 9: { LanguageExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol e$ = CUP$stack.get(CUP$size - 2); LanguageExpression e = (LanguageExpression) e$.value; RESULT = e; return parser.getSymbolFactory().newSymbol("langExpr", 2, CUP$stack.get(CUP$size - 3), CUP$stack.get(CUP$size - 1), RESULT); } // fininfpair ::= PAIR ID ID case 10: { FinInfExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol v$ = CUP$stack.get(CUP$size - 1); String v = (String) v$.value; com.github.jhoenicke.javacup.runtime.Symbol u$ = CUP$stack.get(CUP$size - 2); String u = (String) u$.value; RESULT = new FinInfExpression(u, v); return parser.getSymbolFactory().newSymbol("fininfpair", 3, CUP$stack.get(CUP$size - 3), v$, RESULT); } // specConstant ::= NUMERAL case 11: { LanguageExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol n$ = CUP$stack.get(CUP$size - 1); int n = (int) n$.value; RESULT = new Numeral(n); return parser.getSymbolFactory().newSymbol("specConstant", 1, n$, n$, RESULT); } // specConstant ::= ID case 12: { LanguageExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol n$ = CUP$stack.get(CUP$size - 1); String n = (String) n$.value; RESULT = new Event(n); return parser.getSymbolFactory().newSymbol("specConstant", 1, n$, n$, RESULT); } // specConstant ::= QUOTE ID QUOTE case 13: { LanguageExpression RESULT; com.github.jhoenicke.javacup.runtime.Symbol n$ = CUP$stack.get(CUP$size - 2); String n = (String) n$.value; RESULT = new Event(n); return parser.getSymbolFactory().newSymbol("specConstant", 1, CUP$stack.get(CUP$size - 3), CUP$stack.get(CUP$size - 1), RESULT); } // constraint* ::= case 14: { com.github.jhoenicke.javacup.runtime.Symbol CUP$sym = CUP$stack.get(CUP$size - 1); return parser.getSymbolFactory().newSymbol("constraint*", 7, CUP$sym, CUP$sym, new java.util.ArrayList()); } // constraint+ ::= constraint case 15: { com.github.jhoenicke.javacup.runtime.Symbol CUP$0 = CUP$stack.get(CUP$size - 1); java.util.ArrayList RESULT = new java.util.ArrayList(); RESULT.add((Query) CUP$0.value); return parser.getSymbolFactory().newSymbol("constraint+", 6, CUP$0, CUP$0, RESULT); } // constraint+ ::= constraint+ constraint case 16: { com.github.jhoenicke.javacup.runtime.Symbol CUP$1 = CUP$stack.get(CUP$size - 1); com.github.jhoenicke.javacup.runtime.Symbol CUP$0 = CUP$stack.get(CUP$size - 2); java.util.ArrayList RESULT = (java.util.ArrayList) CUP$0.value; RESULT.add((Query) CUP$1.value); return parser.getSymbolFactory().newSymbol("constraint+", 6, CUP$0, CUP$1, RESULT); } /* . . . . . .*/ default: throw new InternalError( "Invalid action number found in internal parse table"); } } } }