Modernize Bison parsers.
* src/ltlparse/ltlparse.yy, src/tgbaparse/tgbaparse.yy, src/evtgbaparse/evtgbaparse.yy, src/eltlparse/eltlparse.yy: Use token types for %destructor and %printer. Remove the yylex hack, since %name-prefix is now honored by Bison. Also remove the useless <token> type. Suggested by Akim Demaille.
This commit is contained in:
parent
d71ceb3b04
commit
bbd526ac81
5 changed files with 37 additions and 49 deletions
10
ChangeLog
10
ChangeLog
|
|
@ -1,3 +1,13 @@
|
||||||
|
2010-04-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
|
Modernize Bison parsers.
|
||||||
|
|
||||||
|
* src/ltlparse/ltlparse.yy, src/tgbaparse/tgbaparse.yy,
|
||||||
|
src/evtgbaparse/evtgbaparse.yy, src/eltlparse/eltlparse.yy: Use
|
||||||
|
token types for %destructor and %printer. Remove the yylex hack,
|
||||||
|
since %name-prefix is now honored by Bison. Also remove the
|
||||||
|
useless <token> type. Suggested by Akim Demaille.
|
||||||
|
|
||||||
2010-03-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
2010-03-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
Fix column in LTL error messages, it was off by one.
|
Fix column in LTL error messages, it was off by one.
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
/* Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
|
/* Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
|
||||||
** de l'Epita (LRDE).
|
** Développement de l'Epita (LRDE).
|
||||||
**
|
**
|
||||||
** This file is part of Spot, a model checking library.
|
** This file is part of Spot, a model checking library.
|
||||||
**
|
**
|
||||||
|
|
@ -230,10 +230,10 @@ using namespace spot::ltl;
|
||||||
%type <pval> nfa_arg
|
%type <pval> nfa_arg
|
||||||
%type <bval> nfa_arg_list
|
%type <bval> nfa_arg_list
|
||||||
|
|
||||||
%destructor { delete $$; } "atomic proposition"
|
%destructor { delete $$; } <sval>
|
||||||
%destructor { $$->destroy(); } subformula
|
%destructor { $$->destroy(); } <fval>
|
||||||
|
|
||||||
%printer { debug_stream() << *$$; } "atomic proposition"
|
%printer { debug_stream() << *$$; } <sval>
|
||||||
|
|
||||||
%%
|
%%
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
/* Copyright (C) 2009 Laboratoire de Recherche et Développement
|
/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
||||||
** de l'Epita (LRDE).
|
** de l'Epita (LRDE).
|
||||||
/* Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de
|
** Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||||
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||||
** Université Pierre et Marie Curie.
|
** Université Pierre et Marie Curie.
|
||||||
**
|
**
|
||||||
|
|
@ -50,11 +50,6 @@
|
||||||
We mut ensure that YYSTYPE is declared (by the above %union)
|
We mut ensure that YYSTYPE is declared (by the above %union)
|
||||||
before parsedecl.hh uses it. */
|
before parsedecl.hh uses it. */
|
||||||
#include "parsedecl.hh"
|
#include "parsedecl.hh"
|
||||||
|
|
||||||
/* Ugly hack so that Bison use tgbayylex, not yylex.
|
|
||||||
(%name-prefix doesn't work for the lalr1.cc skeleton
|
|
||||||
at the time of writing.) */
|
|
||||||
#define yylex evtgbayylex
|
|
||||||
}
|
}
|
||||||
|
|
||||||
%token <str> STRING UNTERMINATED_STRING
|
%token <str> STRING UNTERMINATED_STRING
|
||||||
|
|
@ -64,11 +59,9 @@
|
||||||
%token ACC_DEF
|
%token ACC_DEF
|
||||||
%token INIT_DEF
|
%token INIT_DEF
|
||||||
|
|
||||||
%destructor { delete $$; } STRING UNTERMINATED_STRING IDENT
|
%destructor { delete $$; } <str>
|
||||||
strident string acc_list
|
|
||||||
|
|
||||||
%printer { debug_stream() << *$$; } STRING UNTERMINATED_STRING IDENT
|
%printer { debug_stream() << *$$; } <str>
|
||||||
strident string
|
|
||||||
|
|
||||||
%%
|
%%
|
||||||
evtgba: lines
|
evtgba: lines
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,8 @@
|
||||||
/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
||||||
** de l'Epita (LRDE).
|
** de l'Epita (LRDE).
|
||||||
/* Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
/* Copyright (C) 2010 Laboratoire de Recherche et Développement de
|
||||||
|
** l'Epita (LRDE).
|
||||||
|
** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||||
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||||
** Université Pierre et Marie Curie.
|
** Université Pierre et Marie Curie.
|
||||||
**
|
**
|
||||||
|
|
@ -40,7 +42,6 @@
|
||||||
%parse-param {spot::ltl::formula* &result}
|
%parse-param {spot::ltl::formula* &result}
|
||||||
%union
|
%union
|
||||||
{
|
{
|
||||||
int token;
|
|
||||||
std::string* str;
|
std::string* str;
|
||||||
spot::ltl::formula* ltl;
|
spot::ltl::formula* ltl;
|
||||||
}
|
}
|
||||||
|
|
@ -52,11 +53,6 @@
|
||||||
#include "parsedecl.hh"
|
#include "parsedecl.hh"
|
||||||
using namespace spot::ltl;
|
using namespace spot::ltl;
|
||||||
|
|
||||||
/* Ugly hack so that Bison uses ltlyylex, not yylex.
|
|
||||||
(%name-prefix doesn't work for the lalr1.cc skeleton
|
|
||||||
at the time of writing.) */
|
|
||||||
#define yylex ltlyylex
|
|
||||||
|
|
||||||
#define missing_right_op(res, op, str) \
|
#define missing_right_op(res, op, str) \
|
||||||
do \
|
do \
|
||||||
{ \
|
{ \
|
||||||
|
|
@ -79,13 +75,13 @@ using namespace spot::ltl;
|
||||||
|
|
||||||
/* All tokens. */
|
/* All tokens. */
|
||||||
|
|
||||||
%token <token> PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis"
|
%token PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis"
|
||||||
%token <token> OP_OR "or operator" OP_XOR "xor operator" OP_AND "and operator"
|
%token OP_OR "or operator" OP_XOR "xor operator" OP_AND "and operator"
|
||||||
%token <token> OP_IMPLIES "implication operator" OP_EQUIV "equivalent operator"
|
%token OP_IMPLIES "implication operator" OP_EQUIV "equivalent operator"
|
||||||
%token <token> OP_U "until operator" OP_R "release operator"
|
%token OP_U "until operator" OP_R "release operator"
|
||||||
%token <token> OP_F "sometimes operator" OP_G "always operator"
|
%token OP_F "sometimes operator" OP_G "always operator"
|
||||||
%token <token> OP_X "next operator"
|
%token OP_X "next operator" OP_NOT "not operator"
|
||||||
%token <str> ATOMIC_PROP "atomic proposition" OP_NOT "not operator"
|
%token <str> ATOMIC_PROP "atomic proposition"
|
||||||
%token CONST_TRUE "constant true" CONST_FALSE "constant false"
|
%token CONST_TRUE "constant true" CONST_FALSE "constant false"
|
||||||
%token END_OF_INPUT "end of formula"
|
%token END_OF_INPUT "end of formula"
|
||||||
%token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix"
|
%token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix"
|
||||||
|
|
@ -110,14 +106,10 @@ using namespace spot::ltl;
|
||||||
|
|
||||||
%type <ltl> subformula
|
%type <ltl> subformula
|
||||||
|
|
||||||
/* At the time of writing (2004-01-05) there is a bug in CVS Bison: if
|
%destructor { delete $$; } <str>
|
||||||
you give a token (such a ATOMIC_PROP) a name (such as "atomic
|
%destructor { $$->destroy(); } <ltl>
|
||||||
proposition"), then the %destructor should refer to that name.
|
|
||||||
References to ATOMIC_PROP are silently ignored. */
|
|
||||||
%destructor { delete $$; } "atomic proposition"
|
|
||||||
%destructor { $$->destroy(); } subformula
|
|
||||||
|
|
||||||
%printer { debug_stream() << *$$; } "atomic proposition"
|
%printer { debug_stream() << *$$; } <str>
|
||||||
|
|
||||||
%%
|
%%
|
||||||
result: subformula END_OF_INPUT
|
result: subformula END_OF_INPUT
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
/* Copyright (C) 2009 Laboratoire de Recherche et Développement
|
/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
||||||
** de l'Epita (LRDE).
|
** de l'Epita (LRDE).
|
||||||
/* Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||||
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||||
** Université Pierre et Marie Curie.
|
** Université Pierre et Marie Curie.
|
||||||
**
|
**
|
||||||
|
|
@ -68,11 +68,6 @@ typedef std::map<std::string, bdd> formula_cache;
|
||||||
#include "parsedecl.hh"
|
#include "parsedecl.hh"
|
||||||
using namespace spot::ltl;
|
using namespace spot::ltl;
|
||||||
|
|
||||||
/* Ugly hack so that Bison use tgbayylex, not yylex.
|
|
||||||
(%name-prefix doesn't work for the lalr1.cc skeleton
|
|
||||||
at the time of writing.) */
|
|
||||||
#define yylex tgbayylex
|
|
||||||
|
|
||||||
typedef std::pair<bool, spot::ltl::formula*> pair;
|
typedef std::pair<bool, spot::ltl::formula*> pair;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -83,17 +78,15 @@ typedef std::pair<bool, spot::ltl::formula*> pair;
|
||||||
%type <list> acc_list
|
%type <list> acc_list
|
||||||
%token ACC_DEF
|
%token ACC_DEF
|
||||||
|
|
||||||
%destructor { delete $$; } STRING UNTERMINATED_STRING IDENT
|
%destructor { delete $$; } <str>
|
||||||
strident string condition
|
|
||||||
%destructor {
|
%destructor {
|
||||||
for (std::list<spot::ltl::formula*>::iterator i = $$->begin();
|
for (std::list<spot::ltl::formula*>::iterator i = $$->begin();
|
||||||
i != $$->end(); ++i)
|
i != $$->end(); ++i)
|
||||||
(*i)->destroy();
|
(*i)->destroy();
|
||||||
delete $$;
|
delete $$;
|
||||||
} acc_list
|
} <list>
|
||||||
|
|
||||||
%printer { debug_stream() << *$$; } STRING UNTERMINATED_STRING IDENT
|
%printer { debug_stream() << *$$; } <str>
|
||||||
strident string condition
|
|
||||||
|
|
||||||
%%
|
%%
|
||||||
tgba: acceptance_decl lines
|
tgba: acceptance_decl lines
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue