eval: adjust to recent parser changes
* spot/parsetl/fmterror.cc, spot/tl/parse.hh: Add an option to display shifted diagnostics. * spot/twaalgos/word.cc: Use the new parser interface and the above option.
This commit is contained in:
parent
1c82444376
commit
8360c4e856
3 changed files with 48 additions and 21 deletions
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2010, 2012, 2013, 2015 Laboratoire de Recherche et
|
// Copyright (C) 2010, 2012, 2013, 2015, 2016 Laboratoire de Recherche et
|
||||||
// Développement de l'Epita (LRDE).
|
// Développement de l'Epita (LRDE).
|
||||||
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
|
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
|
||||||
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||||
|
|
@ -66,10 +66,11 @@ namespace spot
|
||||||
|
|
||||||
namespace
|
namespace
|
||||||
{
|
{
|
||||||
bool
|
static bool
|
||||||
format_parse_errors_aux(std::ostream& os,
|
format_parse_errors_aux(std::ostream& os,
|
||||||
const std::string& ltl_string,
|
const std::string& ltl_string,
|
||||||
const parse_error_list& error_list)
|
const parse_error_list& error_list,
|
||||||
|
unsigned shift)
|
||||||
{
|
{
|
||||||
bool printed = false;
|
bool printed = false;
|
||||||
for (auto it: error_list)
|
for (auto it: error_list)
|
||||||
|
|
@ -78,12 +79,12 @@ namespace spot
|
||||||
const location& l = it.first;
|
const location& l = it.first;
|
||||||
|
|
||||||
unsigned n = 1;
|
unsigned n = 1;
|
||||||
for (; n < 4 + l.begin.column; ++n)
|
for (; n < 4 + l.begin.column + shift; ++n)
|
||||||
os << ' ';
|
os << ' ';
|
||||||
// Write at least one '^', even if begin==end.
|
// Write at least one '^', even if begin==end.
|
||||||
os << '^';
|
os << '^';
|
||||||
++n;
|
++n;
|
||||||
for (; n < 4 + l.end.column; ++n)
|
for (; n < 4 + l.end.column + shift; ++n)
|
||||||
os << '^';
|
os << '^';
|
||||||
os << '\n' << it.second << "\n\n";
|
os << '\n' << it.second << "\n\n";
|
||||||
printed = true;
|
printed = true;
|
||||||
|
|
@ -93,17 +94,27 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
bool
|
bool
|
||||||
parsed_formula::format_errors(std::ostream& os)
|
parsed_formula::format_errors(std::ostream& os,
|
||||||
|
const std::string& real_input,
|
||||||
|
unsigned shift)
|
||||||
{
|
{
|
||||||
if (utf8::is_valid(input.begin(), input.end()))
|
if (utf8::is_valid(input.begin(), input.end()))
|
||||||
{
|
{
|
||||||
parse_error_list fixed = errors;
|
parse_error_list fixed = errors;
|
||||||
fix_utf8_locations(input, fixed);
|
fix_utf8_locations(input, fixed);
|
||||||
return format_parse_errors_aux(os, input, fixed);
|
return format_parse_errors_aux(os, real_input, fixed, shift);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
return format_parse_errors_aux(os, input, errors);
|
return format_parse_errors_aux(os, real_input, errors, shift);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
bool
|
||||||
|
parsed_formula::format_errors(std::ostream& os)
|
||||||
|
{
|
||||||
|
return format_errors(os, input, 0);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -74,6 +74,28 @@ namespace spot
|
||||||
/// \param os Where diagnostics should be output.
|
/// \param os Where diagnostics should be output.
|
||||||
/// \return \c true iff any diagnostic was output.
|
/// \return \c true iff any diagnostic was output.
|
||||||
bool format_errors(std::ostream& os);
|
bool format_errors(std::ostream& os);
|
||||||
|
|
||||||
|
/// \brief Format shifted diagnostics.
|
||||||
|
///
|
||||||
|
/// If the user input was something like "formula = a U b;" but you
|
||||||
|
/// only passed "a U b" to the parser, it might be convenient to
|
||||||
|
/// display the diagnostic in the context of "formula = a U b;".
|
||||||
|
///
|
||||||
|
/// So pass the real input as \a input, and specify the number
|
||||||
|
/// of character to skip before the actual text passed to the
|
||||||
|
/// parser starts.
|
||||||
|
///
|
||||||
|
/// This procedure assumes that the text passed to the parser
|
||||||
|
/// appears as-is in the input string. If you had to un-escape it
|
||||||
|
/// in any way, the error locations will be wrong.
|
||||||
|
///
|
||||||
|
/// \param os Where diagnostics should be output.
|
||||||
|
/// \param input the real input string
|
||||||
|
/// \param shift how many characters to add to the error locations
|
||||||
|
/// \return \c true iff any diagnostic was output.
|
||||||
|
bool format_errors(std::ostream& os,
|
||||||
|
const std::string& input,
|
||||||
|
unsigned shift);
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -117,15 +117,10 @@ namespace spot
|
||||||
namespace
|
namespace
|
||||||
{
|
{
|
||||||
static void word_parse_error(const std::string& word,
|
static void word_parse_error(const std::string& word,
|
||||||
size_t i, parse_error_list pel)
|
size_t i, parsed_formula pf)
|
||||||
{
|
{
|
||||||
for (auto& err: pel)
|
|
||||||
{
|
|
||||||
err.first.begin.column += i;
|
|
||||||
err.first.end.column += i;
|
|
||||||
}
|
|
||||||
std::ostringstream os;
|
std::ostringstream os;
|
||||||
format_parse_errors(os, word, pel);
|
pf.format_errors(os, word, i);
|
||||||
throw parse_error(os.str());
|
throw parse_error(os.str());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -166,7 +161,6 @@ namespace spot
|
||||||
twa_word_ptr parse_word(const std::string& word, const bdd_dict_ptr& dict)
|
twa_word_ptr parse_word(const std::string& word, const bdd_dict_ptr& dict)
|
||||||
{
|
{
|
||||||
atomic_prop_set aps;
|
atomic_prop_set aps;
|
||||||
parse_error_list pel;
|
|
||||||
tl_simplifier tls(dict);
|
tl_simplifier tls(dict);
|
||||||
twa_word_ptr tw = make_twa_word(dict);
|
twa_word_ptr tw = make_twa_word(dict);
|
||||||
size_t i = 0;
|
size_t i = 0;
|
||||||
|
|
@ -176,11 +170,11 @@ namespace spot
|
||||||
[&](typename twa_word::seq_t& seq)
|
[&](typename twa_word::seq_t& seq)
|
||||||
{
|
{
|
||||||
auto sub = word.substr(i, ind - i);
|
auto sub = word.substr(i, ind - i);
|
||||||
formula f = spot::parse_infix_boolean(sub, pel);
|
auto pf = spot::parse_infix_boolean(sub);
|
||||||
if (!pel.empty())
|
if (!pf.errors.empty())
|
||||||
word_parse_error(word, i, pel);
|
word_parse_error(word, i, pf);
|
||||||
atomic_prop_collect(f, &aps);
|
atomic_prop_collect(pf.f, &aps);
|
||||||
seq.push_back(tls.as_bdd(f));
|
seq.push_back(tls.as_bdd(pf.f));
|
||||||
if (word[ind] == '}')
|
if (word[ind] == '}')
|
||||||
return true;
|
return true;
|
||||||
// Skip blanks after semi-colon
|
// Skip blanks after semi-colon
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue