* src/ltlparse/ltlparse.yy (error_list, parse_environment, result):
CVS Bison now supports %parse-param for the C++ skeleton; pass these variables as arguments to the Parser::Parser constructor instead of using globals. (parse): Adjust Parser::Parser call.
This commit is contained in:
parent
8e988470b1
commit
a92327d30b
2 changed files with 54 additions and 63 deletions
42
ChangeLog
42
ChangeLog
|
|
@ -1,3 +1,11 @@
|
|||
2003-05-15 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||
|
||||
* src/ltlparse/ltlparse.yy (error_list, parse_environment, result):
|
||||
CVS Bison now supports %parse-param for the C++ skeleton; pass these
|
||||
variables as arguments to the Parser::Parser constructor instead of
|
||||
using globals.
|
||||
(parse): Adjust Parser::Parser call.
|
||||
|
||||
2003-05-12 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||
|
||||
* src/ltlvisit/tostring.cc: Reindent and strip out superfluous
|
||||
|
|
@ -17,9 +25,9 @@
|
|||
|
||||
* src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ...
|
||||
(noinst_LTLIBRARIES): ... this.
|
||||
* src/ltlenv/Makefile.am, src/ltlast/Makefile.am,
|
||||
* src/ltlenv/Makefile.am, src/ltlast/Makefile.am,
|
||||
src/ltlparse/Makefile.am: Likewise.
|
||||
* src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES,
|
||||
* src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES,
|
||||
libspot_la_LIBADD): New variable. Build a libspot.la library
|
||||
from all the sub-libraries.
|
||||
|
||||
|
|
@ -32,7 +40,7 @@
|
|||
2003-04-29 Alexandre DURET-LUTZ <aduret@src.lip6.fr>
|
||||
|
||||
* configure.ac: Call AC_PROG_LIBTOOL.
|
||||
* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
|
||||
* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
|
||||
src/ltlparse/Makefile.am, src/ltltest/Makefile.am,
|
||||
src/ltlvisit/Makefile.am: Adust to build libtool libraries.
|
||||
|
||||
|
|
@ -42,12 +50,12 @@
|
|||
* src/ltltest/tostring.test: Simplify with set -e. Move the
|
||||
description of the test ...
|
||||
* src/ltltest/tostring.cc: ... here, where it is actually coded.
|
||||
* src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test,
|
||||
src/ltltest/nenoform.test, src/ltltest/tunenoform.test:
|
||||
* src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test,
|
||||
src/ltltest/nenoform.test, src/ltltest/tunenoform.test:
|
||||
Simplify with set -e.
|
||||
|
||||
* configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make
|
||||
sure we always use paths relative to src/ in src/'s
|
||||
sure we always use paths relative to src/ in src/'s
|
||||
subdirectories.
|
||||
|
||||
2003-04-28 Alexandre DURET-LUTZ <aduret@src.lip6.fr>
|
||||
|
|
@ -75,7 +83,7 @@
|
|||
src/ltlparse/public.hh, src/ltlvisit/clone.hh,
|
||||
src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh,
|
||||
src/ltlvisit/equals.hh, src/ltlvisit/lunabbrev.hh,
|
||||
src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add
|
||||
src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add
|
||||
Doxygen comments.
|
||||
* src/visitor.hh: Do not use const_sel. This clarifies
|
||||
the code and helps Doxygen.
|
||||
|
|
@ -83,9 +91,9 @@
|
|||
* configure.ac: Output doc/Doxyfile and doc/Makefile.
|
||||
* doc/Makefile.am, doc/Doxyfile.in: New files.
|
||||
* Makefile.am (SUBDIRS): Add doc.
|
||||
|
||||
|
||||
* src/ltlparse/ltlscan.ll: Recognize && and ||.
|
||||
* src/ltltest/parse.test, src/ltltest/parseerr.test,
|
||||
* src/ltltest/parse.test, src/ltltest/parseerr.test,
|
||||
src/ltltest/equals.test: Use these operators..
|
||||
|
||||
2003-04-17 Alexandre DURET-LUTZ <aduret@src.lip6.fr>
|
||||
|
|
@ -100,10 +108,10 @@
|
|||
* src/ltlast/atomic_prop.cc (atomic_prop, env): Likewise.
|
||||
* src/ltlenv/defaultenv.cc (require): Pass *this as the
|
||||
environment argument to atomic_prop.
|
||||
* src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy
|
||||
* src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy
|
||||
the environment.
|
||||
* src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise.
|
||||
|
||||
|
||||
* configure.ac: Output src/ltlenv/Makefile.
|
||||
* src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc,
|
||||
src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files.
|
||||
|
|
@ -125,7 +133,7 @@
|
|||
* src/ltltest/nenoform.test, src/ltltest/tunenoform.test: New files.
|
||||
* src/ltltest/Makefile.am (check_PROGRAMS): Add nenoform and
|
||||
tunenoform.
|
||||
(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES,
|
||||
(nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES,
|
||||
tunenoform_CPPFLAGS): New variables.
|
||||
(TESTS): Add nenoform.test and tunenoform.test.
|
||||
|
||||
|
|
@ -145,7 +153,7 @@
|
|||
New virtual function.
|
||||
* src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::recurse):
|
||||
Likewise.
|
||||
(unabbreviate_logic_visitor::visit): Use it instead of calling
|
||||
(unabbreviate_logic_visitor::visit): Use it instead of calling
|
||||
unabbreviate_logic directly.
|
||||
|
||||
* src/ltlvisit/lunabbrev.hh: Add missing include guard.
|
||||
|
|
@ -169,7 +177,7 @@
|
|||
* src/ltlast/formula.hh (formulae): Rename as ...
|
||||
(formula): ... this.
|
||||
Adjust all uses.
|
||||
|
||||
|
||||
* src/ltlparse/public.hh (format_parse_errors): New function.
|
||||
* src/ltlparse/fmterror.cc: New file.
|
||||
* src/ltlparse/Makefile.am (libltlparse_a_SOURCES): Add fmterror.cc.
|
||||
|
|
@ -185,7 +193,7 @@
|
|||
(TESTS): Add equals.test.
|
||||
|
||||
* src/ltlast/multop.cc (multop::multop): Use multop::add.
|
||||
(multop::add): If the formulae we add is itself a multop for the
|
||||
(multop::add): If the formulae we add is itself a multop for the
|
||||
same operator, merge its children with ours.
|
||||
* src/ltltest/parseerr.test: Add two tests for multop merging.
|
||||
|
||||
|
|
@ -216,6 +224,6 @@
|
|||
src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
|
||||
src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
|
||||
src/ltlvisit/rewrite.cc, src/ltlvisit/rewrite.hh,
|
||||
src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
|
||||
src/ltltest/parse.test, src/ltltest/parseerr.test,
|
||||
src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
|
||||
src/ltltest/parse.test, src/ltltest/parseerr.test,
|
||||
src/misc/Makefile.am, src/misc/const_sel.hh: New files.
|
||||
|
|
|
|||
|
|
@ -7,6 +7,9 @@ extern spot::ltl::formula* result;
|
|||
|
||||
%}
|
||||
|
||||
%parse-param {spot::ltl::parse_error_list &error_list}
|
||||
%parse-param {spot::ltl::environment &parse_environment}
|
||||
%parse-param {spot::ltl::formula* &result}
|
||||
%debug
|
||||
%error-verbose
|
||||
%union
|
||||
|
|
@ -22,18 +25,6 @@ extern spot::ltl::formula* result;
|
|||
before parsedecl.hh uses it. */
|
||||
#include "parsedecl.hh"
|
||||
using namespace spot::ltl;
|
||||
|
||||
// At the time of writing C++ support in Bison is quite
|
||||
// new and there is still no way to pass error_list to
|
||||
// the parser. We use a global variable instead.
|
||||
namespace spot
|
||||
{
|
||||
namespace ltl
|
||||
{
|
||||
extern parse_error_list* error_list;
|
||||
extern environment* parse_environment;
|
||||
}
|
||||
}
|
||||
%}
|
||||
|
||||
/* Logical operators. */
|
||||
|
|
@ -55,7 +46,7 @@ namespace spot
|
|||
%token <str> ATOMIC_PROP
|
||||
|
||||
/* Constants */
|
||||
%token CONST_TRUE
|
||||
%token CONST_TRUE
|
||||
%token CONST_FALSE
|
||||
%token END_OF_INPUT
|
||||
|
||||
|
|
@ -63,24 +54,23 @@ namespace spot
|
|||
|
||||
%%
|
||||
result: ltl_formula END_OF_INPUT
|
||||
{ result = $$ = $1;
|
||||
{ result = $$ = $1;
|
||||
YYACCEPT;
|
||||
}
|
||||
| many_errors END_OF_INPUT
|
||||
{ error_list->push_back(parse_error(@1,
|
||||
"couldn't parse anything sensible"));
|
||||
{ error_list.push_back(parse_error(@1,
|
||||
"couldn't parse anything sensible"));
|
||||
result = $$ = 0;
|
||||
YYABORT;
|
||||
}
|
||||
| END_OF_INPUT
|
||||
{ error_list->push_back(parse_error(@1,
|
||||
"empty input"));
|
||||
{ error_list.push_back(parse_error(@1, "empty input"));
|
||||
result = $$ = 0;
|
||||
YYABORT;
|
||||
}
|
||||
|
||||
many_errors_diagnosed : many_errors
|
||||
{ error_list->push_back(parse_error(@1,
|
||||
many_errors_diagnosed : many_errors
|
||||
{ error_list.push_back(parse_error(@1,
|
||||
"unexpected input ignored")); }
|
||||
|
||||
ltl_formula: subformula
|
||||
|
|
@ -94,21 +84,21 @@ many_errors: error
|
|||
| many_errors error
|
||||
|
||||
subformula: ATOMIC_PROP
|
||||
{
|
||||
$$ = parse_environment->require(*$1);
|
||||
{
|
||||
$$ = parse_environment.require(*$1);
|
||||
if (! $$)
|
||||
{
|
||||
std::string s = "unknown atomic proposition `";
|
||||
s += *$1;
|
||||
s += "' in environment `";
|
||||
s += parse_environment->name();
|
||||
s += parse_environment.name();
|
||||
s += "'";
|
||||
error_list->push_back(parse_error(@1, s));
|
||||
delete $1;
|
||||
error_list.push_back(parse_error(@1, s));
|
||||
delete $1;
|
||||
YYERROR;
|
||||
}
|
||||
else
|
||||
delete $1;
|
||||
delete $1;
|
||||
}
|
||||
| CONST_TRUE
|
||||
{ $$ = new constant(constant::True); }
|
||||
|
|
@ -117,13 +107,13 @@ subformula: ATOMIC_PROP
|
|||
| PAR_OPEN subformula PAR_CLOSE
|
||||
{ $$ = $2; }
|
||||
| PAR_OPEN error PAR_CLOSE
|
||||
{ error_list->push_back(parse_error(@$,
|
||||
"treating this parenthetical block as false"));
|
||||
{ error_list.push_back(parse_error(@$,
|
||||
"treating this parenthetical block as false"));
|
||||
$$ = new constant(constant::False);
|
||||
}
|
||||
| PAR_OPEN subformula many_errors PAR_CLOSE
|
||||
{ error_list->push_back(parse_error(@3,
|
||||
"unexpected input ignored"));
|
||||
{ error_list.push_back(parse_error(@3,
|
||||
"unexpected input ignored"));
|
||||
$$ = $2;
|
||||
}
|
||||
| OP_NOT subformula
|
||||
|
|
@ -149,11 +139,11 @@ subformula: ATOMIC_PROP
|
|||
| OP_X subformula
|
||||
{ $$ = new unop(unop::X, $2); }
|
||||
// | subformula many_errors
|
||||
// { error_list->push_back(parse_error(@2,
|
||||
// "ignoring these unexpected trailing tokens"));
|
||||
// { error_list->push_back(parse_error(@2,
|
||||
// "ignoring these unexpected trailing tokens"));
|
||||
// $$ = $1;
|
||||
// }
|
||||
|
||||
|
||||
;
|
||||
|
||||
%%
|
||||
|
|
@ -161,37 +151,30 @@ subformula: ATOMIC_PROP
|
|||
void
|
||||
yy::Parser::print_()
|
||||
{
|
||||
if (looka_ == ATOMIC_PROP)
|
||||
if (looka_ == ATOMIC_PROP)
|
||||
YYCDEBUG << " '" << *value.str << "'";
|
||||
}
|
||||
|
||||
void
|
||||
yy::Parser::error_()
|
||||
{
|
||||
error_list->push_back(parse_error(location, message));
|
||||
error_list.push_back(parse_error(location, message));
|
||||
}
|
||||
|
||||
formula* result = 0;
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace ltl
|
||||
{
|
||||
parse_error_list* error_list;
|
||||
environment* parse_environment;
|
||||
|
||||
formula*
|
||||
parse(const std::string& ltl_string,
|
||||
parse(const std::string& ltl_string,
|
||||
parse_error_list& error_list,
|
||||
environment& env,
|
||||
bool debug)
|
||||
{
|
||||
result = 0;
|
||||
ltl::error_list = &error_list;
|
||||
parse_environment = &env;
|
||||
formula* result = 0;
|
||||
flex_set_buffer(ltl_string.c_str());
|
||||
yy::Parser parser(debug, yy::Location());
|
||||
parser.parse();
|
||||
yy::Parser parser(debug, yy::Location(), error_list, env, result);
|
||||
parser.parse();
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue