From c0552123266c4e726ed8eb34f3a58a24bdcc5fe7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 1 Aug 2006 16:35:06 +0000 Subject: [PATCH] * src/evtgbatest/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, src/evtgbaparse/parsedecl.hh, src/evtgbaparse/public.hh, src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh, src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy, src/tgbaparse/tgbascan.ll: Adjust for Bison 2.3. Use %name-prefix instead of the "#define yy ... " kludge. --- ChangeLog | 11 +++++++++ src/evtgbaparse/evtgbaparse.yy | 6 +++-- src/evtgbaparse/evtgbascan.ll | 11 +++++---- src/evtgbaparse/parsedecl.hh | 16 ++----------- src/evtgbaparse/public.hh | 4 ++-- src/ltlparse/fmterror.cc | 2 +- src/ltlparse/ltlparse.yy | 5 ++-- src/ltlparse/ltlscan.ll | 42 ++++++++++++++++++---------------- src/ltlparse/parsedecl.hh | 2 +- src/ltlparse/public.hh | 4 ++-- src/tgbaparse/parsedecl.hh | 13 ++++++----- src/tgbaparse/public.hh | 7 ++++-- src/tgbaparse/tgbaparse.yy | 23 +++++++++++-------- src/tgbaparse/tgbascan.ll | 10 ++++---- 14 files changed, 86 insertions(+), 70 deletions(-) diff --git a/ChangeLog b/ChangeLog index 40b4dfa0d..71e8b5b56 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2006-08-01 Alexandre Duret-Lutz + + * src/evtgbatest/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, + src/evtgbaparse/parsedecl.hh, src/evtgbaparse/public.hh, + src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy, + src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh, + src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh, + src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy, + src/tgbaparse/tgbascan.ll: Adjust for Bison 2.3. Use %name-prefix + instead of the "#define yy ... " kludge. + 2006-07-24 Alexandre Duret-Lutz * src/ltlvisit/contain.hh, src/ltlvisit/contain.cc: Adjust to only diff --git a/src/evtgbaparse/evtgbaparse.yy b/src/evtgbaparse/evtgbaparse.yy index 889e1a705..d0be3cc40 100644 --- a/src/evtgbaparse/evtgbaparse.yy +++ b/src/evtgbaparse/evtgbaparse.yy @@ -25,6 +25,7 @@ #include "evtgba/symbol.hh" %} +%name-prefix="evtgbayy" %parse-param {spot::evtgba_parse_error_list &error_list} %parse-param {spot::evtgba_explicit* &result} %debug @@ -120,7 +121,8 @@ init_decl: %% void -yy::parser::error(const location_type& location, const std::string& message) +evtgbayy::parser::error(const location_type& location, + const std::string& message) { error_list.push_back(spot::evtgba_parse_error(location, message)); } @@ -135,7 +137,7 @@ namespace spot if (evtgbayyopen(name)) { error_list.push_back - (evtgba_parse_error(yy::location(), + (evtgba_parse_error(evtgbayy::location(), std::string("Cannot open file ") + name)); return 0; } diff --git a/src/evtgbaparse/evtgbascan.ll b/src/evtgbaparse/evtgbascan.ll index 2302569f2..5151de8e4 100644 --- a/src/evtgbaparse/evtgbascan.ll +++ b/src/evtgbaparse/evtgbascan.ll @@ -33,6 +33,7 @@ #define YY_NEVER_INTERACTIVE 1 +typedef evtgbayy::parser::token token; %} eol \n|\r|\n\r|\r\n @@ -43,12 +44,12 @@ eol \n|\r|\n\r|\r\n yylloc->step (); %} -acc[ \t]*= return ACC_DEF; -init[ \t]*= return INIT_DEF; +acc[ \t]*= return token::ACC_DEF; +init[ \t]*= return token::INIT_DEF; [a-zA-Z][a-zA-Z0-9_]* { yylval->str = new std::string(yytext); - return IDENT; + return token::IDENT; } /* discard whitespace */ @@ -66,13 +67,13 @@ init[ \t]*= return INIT_DEF; { \" { BEGIN(INITIAL); - return STRING; + return token::STRING; } \\["\\] yylval->str->append(1, yytext[1]); [^"\\]+ yylval->str->append(yytext, yyleng); <> { BEGIN(INITIAL); - return UNTERMINATED_STRING; + return token::UNTERMINATED_STRING; } } diff --git a/src/evtgbaparse/parsedecl.hh b/src/evtgbaparse/parsedecl.hh index a41c585f7..447fe1744 100644 --- a/src/evtgbaparse/parsedecl.hh +++ b/src/evtgbaparse/parsedecl.hh @@ -27,7 +27,8 @@ #include "location.hh" # define YY_DECL \ - int evtgbayylex (yystype *yylval, yy::location *yylloc) + int evtgbayylex (evtgbayy::parser::semantic_type *yylval, \ + evtgbayy::location *yylloc) YY_DECL; namespace spot @@ -37,17 +38,4 @@ namespace spot } -// Gross kludge to compile yy::Parser in another namespace (tgbayy::) -// but still use yy::Location. The reason is that Bison's C++ -// skeleton does not support anything close to %name-prefix at the -// moment. All parser are named yy::Parser which makes it somewhat -// difficult to define multiple parsers. -namespace evtgbayy -{ - using namespace yy; -} -#define yy evtgbayy - - - #endif // SPOT_EVTGBAPARSE_PARSEDECL_HH diff --git a/src/evtgbaparse/public.hh b/src/evtgbaparse/public.hh index 5f8824058..2fab20175 100644 --- a/src/evtgbaparse/public.hh +++ b/src/evtgbaparse/public.hh @@ -23,7 +23,7 @@ # define SPOT_EVTGBAPARSE_PUBLIC_HH # include "evtgba/explicit.hh" -# include "ltlparse/location.hh" +# include "location.hh" # include # include # include @@ -32,7 +32,7 @@ namespace spot { /// \brief A parse diagnostic with its location. - typedef std::pair evtgba_parse_error; + typedef std::pair evtgba_parse_error; /// \brief A list of parser diagnostics, as filled by parse. typedef std::list evtgba_parse_error_list; diff --git a/src/ltlparse/fmterror.cc b/src/ltlparse/fmterror.cc index 7e2765d92..62020b4cb 100644 --- a/src/ltlparse/fmterror.cc +++ b/src/ltlparse/fmterror.cc @@ -37,7 +37,7 @@ namespace spot for (it = error_list.begin(); it != error_list.end(); ++it) { os << ">>> " << ltl_string << std::endl; - yy::location& l = it->first; + ltlyy::location& l = it->first; unsigned n = 0; for (; n < 4 + l.begin.column; ++n) diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index a25bfc78e..6e8efce8f 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -27,6 +27,7 @@ %} +%name-prefix="ltlyy" %parse-param {spot::ltl::parse_error_list &error_list} %parse-param {spot::ltl::environment &parse_environment} %parse-param {spot::ltl::formula* &result} @@ -262,7 +263,7 @@ subformula: ATOMIC_PROP %% void -yy::parser::error(const location_type& location, const std::string& message) +ltlyy::parser::error(const location_type& location, const std::string& message) { error_list.push_back(parse_error(location, message)); } @@ -279,7 +280,7 @@ namespace spot { formula* result = 0; flex_set_buffer(ltl_string.c_str()); - yy::parser parser(error_list, env, result); + ltlyy::parser parser(error_list, env, result); parser.set_debug_level(debug); parser.parse(); return result; diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 97fb10a61..ed6d0a4c1 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -42,6 +42,8 @@ static const char* to_parse = 0; static size_t to_parse_size = 0; +typedef ltlyy::parser::token token; + void flex_set_buffer(const char* buf) { @@ -59,36 +61,36 @@ flex_set_buffer(const char* buf) yylloc->step(); %} -"(" BEGIN(0); return PAR_OPEN; -")" BEGIN(not_prop); return PAR_CLOSE; +"(" BEGIN(0); return token::PAR_OPEN; +")" BEGIN(not_prop); return token::PAR_CLOSE; /* Must go before the other operators, because the F of FALSE should not be mistaken with a unary F. */ -"1"|[tT][rR][uU][eE] BEGIN(0); return CONST_TRUE; -"0"|[fF][aA][lL][sS][eE] BEGIN(0); return CONST_FALSE; +"1"|[tT][rR][uU][eE] BEGIN(0); return token::CONST_TRUE; +"0"|[fF][aA][lL][sS][eE] BEGIN(0); return token::CONST_FALSE; -"!" BEGIN(0); return OP_NOT; +"!" BEGIN(0); return token::OP_NOT; /* & and | come from Spin. && and || from LTL2BA. /\, \/, and xor are from LBTT. */ -"||"|"|"|"+"|"\\/" BEGIN(0); return OP_OR; -"&&"|"&"|"."|"*"|"/\\" BEGIN(0); return OP_AND; -"^"|"xor" BEGIN(0); return OP_XOR; -"=>"|"->" BEGIN(0); return OP_IMPLIES; -"<=>"|"<->" BEGIN(0); return OP_EQUIV; +"||"|"|"|"+"|"\\/" BEGIN(0); return token::OP_OR; +"&&"|"&"|"."|"*"|"/\\" BEGIN(0); return token::OP_AND; +"^"|"xor" BEGIN(0); return token::OP_XOR; +"=>"|"->" BEGIN(0); return token::OP_IMPLIES; +"<=>"|"<->" BEGIN(0); return token::OP_EQUIV; /* <>, [], and () are used in Spin. */ -"F"|"<>" BEGIN(0); return OP_F; -"G"|"[]" BEGIN(0); return OP_G; -"U" BEGIN(0); return OP_U; -"R"|"V" BEGIN(0); return OP_R; -"X"|"()" BEGIN(0); return OP_X; +"F"|"<>" BEGIN(0); return token::OP_F; +"G"|"[]" BEGIN(0); return token::OP_G; +"U" BEGIN(0); return token::OP_U; +"R"|"V" BEGIN(0); return token::OP_R; +"X"|"()" BEGIN(0); return token::OP_X; -"=0" return OP_POST_NEG; -"=1" return OP_POST_POS; +"=0" return token::OP_POST_NEG; +"=1" return token::OP_POST_POS; [ \t\n]+ /* discard whitespace */ yylloc->step (); @@ -118,7 +120,7 @@ flex_set_buffer(const char* buf) [a-zA-EH-QSTWYZ_][a-zA-EH-WYZ0-9_][a-zA-Z0-9_]* { yylval->str = new std::string(yytext, yyleng); BEGIN(not_prop); - return ATOMIC_PROP; + return token::ATOMIC_PROP; } /* Atomic propositions can also be enclosed in double quotes. */ @@ -126,12 +128,12 @@ flex_set_buffer(const char* buf) yylval->str = new std::string(yytext + 1, yyleng - 2); BEGIN(not_prop); - return ATOMIC_PROP; + return token::ATOMIC_PROP; } . return *yytext; -<> return END_OF_INPUT; +<> return token::END_OF_INPUT; %{ /* Dummy use of yyunput to shut up a gcc warning. */ diff --git a/src/ltlparse/parsedecl.hh b/src/ltlparse/parsedecl.hh index f6c1217cc..7d802296a 100644 --- a/src/ltlparse/parsedecl.hh +++ b/src/ltlparse/parsedecl.hh @@ -26,7 +26,7 @@ #include "location.hh" # define YY_DECL \ - int ltlyylex (yystype *yylval, yy::location *yylloc) + int ltlyylex (ltlyy::parser::semantic_type *yylval, ltlyy::location *yylloc) YY_DECL; void flex_set_buffer(const char *buf); diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index a4297452c..b952b8117 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -23,7 +23,7 @@ # define SPOT_LTLPARSE_PUBLIC_HH # include "ltlast/formula.hh" -# include "location.hh" +# include "ltlparse/location.hh" # include "ltlenv/defaultenv.hh" # include # include @@ -38,7 +38,7 @@ namespace spot /// @{ /// \brief A parse diagnostic with its location. - typedef std::pair parse_error; + typedef std::pair parse_error; /// \brief A list of parser diagnostics, as filled by parse. typedef std::list parse_error_list; diff --git a/src/tgbaparse/parsedecl.hh b/src/tgbaparse/parsedecl.hh index 27a9fc2ac..dc51f75ed 100644 --- a/src/tgbaparse/parsedecl.hh +++ b/src/tgbaparse/parsedecl.hh @@ -27,7 +27,8 @@ #include "location.hh" # define YY_DECL \ - int tgbayylex (yystype *yylval, yy::location *yylloc) + int tgbayylex (tgbayy::parser::semantic_type *yylval, \ + tgbayy::location *yylloc) YY_DECL; namespace spot @@ -42,11 +43,11 @@ namespace spot // skeleton does not support anything close to %name-prefix at the // moment. All parser are named yy::Parser which makes it somewhat // difficult to define multiple parsers. -namespace tgbayy -{ - using namespace yy; -} -#define yy tgbayy +// namespace tgbayy +// { +// using namespace yy; +// } +// #define yy tgbayy diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index 869d85b9c..2ccb56e5e 100644 --- a/src/tgbaparse/public.hh +++ b/src/tgbaparse/public.hh @@ -23,7 +23,10 @@ # define SPOT_TGBAPARSE_PUBLIC_HH # include "tgba/tgbaexplicit.hh" -# include "ltlparse/location.hh" + /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */ +# undef BISON_LOCATION_HH +# undef BISON_POSITION_HH +# include "tgbaparse/location.hh" # include "ltlenv/defaultenv.hh" # include # include @@ -36,7 +39,7 @@ namespace spot /// @{ /// \brief A parse diagnostic with its location. - typedef std::pair tgba_parse_error; + typedef std::pair tgba_parse_error; /// \brief A list of parser diagnostics, as filled by parse. typedef std::list tgba_parse_error_list; diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index e5b11b18b..d11841145 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -22,8 +22,15 @@ %{ #include #include "public.hh" + +/* Cache parsed formulae. Labels on arcs are frequently identical and + it would be a waste of time to parse them to formula* over and + over, and to register all their atomic_propositions in the + bdd_dict. Keep the bdd result around so we can reuse it. */ +typedef std::map formula_cache; %} +%name-prefix="tgbayy" %parse-param {spot::tgba_parse_error_list& error_list} %parse-param {spot::ltl::environment& parse_environment} %parse-param {spot::ltl::environment& parse_envacc} @@ -42,11 +49,14 @@ %{ #include "ltlast/constant.hh" #include "ltlvisit/destroy.hh" + /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */ +#undef BISON_POSITION_HH +#undef BISON_LOCATION_HH #include "ltlparse/public.hh" #include /* tgbaparse.hh and parsedecl.hh include each other recursively. - We mut ensure that YYSTYPE is declared (by the above %union) + We must ensure that YYSTYPE is declared (by the above %union) before parsedecl.hh uses it. */ #include "parsedecl.hh" using namespace spot::ltl; @@ -57,12 +67,6 @@ using namespace spot::ltl; #define yylex tgbayylex typedef std::pair pair; - -/* Cache parsed formulae. Labels on arcs are frequently identical and - it would be a waste of time to parse them to formula* over and - over, and to register all their atomic_propositions in the - bdd_dict. Keep the bdd result around so we can reuse it. */ -typedef std::map formula_cache; %} %token STRING UNTERMINATED_STRING @@ -215,7 +219,8 @@ acc_decl: %% void -yy::parser::error(const location_type& location, const std::string& message) +tgbayy::parser::error(const location_type& location, + const std::string& message) { error_list.push_back(spot::tgba_parse_error(location, message)); } @@ -233,7 +238,7 @@ namespace spot if (tgbayyopen(name)) { error_list.push_back - (tgba_parse_error(yy::location(), + (tgba_parse_error(tgbayy::location(), std::string("Cannot open file ") + name)); return 0; } diff --git a/src/tgbaparse/tgbascan.ll b/src/tgbaparse/tgbascan.ll index fac2a9466..0f46e7eff 100644 --- a/src/tgbaparse/tgbascan.ll +++ b/src/tgbaparse/tgbascan.ll @@ -33,6 +33,8 @@ #define YY_NEVER_INTERACTIVE 1 +typedef tgbayy::parser::token token; + %} eol \n|\r|\n\r|\r\n @@ -43,11 +45,11 @@ eol \n|\r|\n\r|\r\n yylloc->step (); %} -acc[ \t]*= return ACC_DEF; +acc[ \t]*= return token::ACC_DEF; [a-zA-Z][a-zA-Z0-9_]* { yylval->str = new std::string(yytext, yyleng); - return IDENT; + return token::IDENT; } /* discard whitespace */ @@ -65,13 +67,13 @@ acc[ \t]*= return ACC_DEF; { \" { BEGIN(INITIAL); - return STRING; + return token::STRING; } \\["\\] yylval->str->append(1, yytext[1]); [^"\\]+ yylval->str->append(yytext, yyleng); <> { BEGIN(INITIAL); - return UNTERMINATED_STRING; + return token::UNTERMINATED_STRING; } }