parse.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 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),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <spot/tl/formula.hh>
#include <spot/misc/location.hh>
#include <spot/tl/defaultenv.hh>
#include <string>
#include <list>
#include <utility>
#include <iosfwd>
 
namespace spot
{
 
#ifndef SWIG
  typedef std::pair<location, std::string> one_parse_error;
  typedef std::list<one_parse_error> parse_error_list;
#else
  // Turn parse_error_list into an opaque type for Swig.
  struct parse_error_list {};
#endif
 
  struct SPOT_API parsed_formula final
  {
    formula f = nullptr;
 
    std::string input;
 
    parse_error_list errors;
 
    parsed_formula(const std::string& str = "")
      : input(str)
    {
    }
 
    bool format_errors(std::ostream& os);
 
    bool format_errors(std::ostream& os,
                       const std::string& input,
                       unsigned shift);
  };
 
 
  SPOT_API
  parsed_formula parse_infix_psl(const std::string& ltl_string,
                                 environment& env =
                                 default_environment::instance(),
                                 bool debug = false,
                                 bool lenient = false);
 
  SPOT_API
  parsed_formula parse_infix_boolean(const std::string& ltl_string,
                                     environment& env =
                                     default_environment::instance(),
                                     bool debug = false,
                                     bool lenient = false);
 
  SPOT_API
  parsed_formula parse_prefix_ltl(const std::string& ltl_string,
                                  environment& env =
                                  default_environment::instance(),
                                  bool debug = false);
 
  SPOT_API formula
  parse_formula(const std::string& ltl_string,
                environment& env = default_environment::instance());
 
  SPOT_API
  parsed_formula parse_infix_sere(const std::string& sere_string,
                                  environment& env =
                                  default_environment::instance(),
                                  bool debug = false,
                                  bool lenient = false);
 
  SPOT_API
  void
  fix_utf8_locations(const std::string& input_string,
                     parse_error_list& error_list);
 
}