Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/data/detail/variable_context.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_VARIABLE_CONTEXT_H
      13             : #define MCRL2_DATA_DETAIL_VARIABLE_CONTEXT_H
      14             : 
      15             : #include "mcrl2/data/variable.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace data {
      20             : 
      21             : class data_type_checker;
      22             : 
      23             : namespace detail {
      24             : 
      25             : // Throws an exception if the names of the variables are not unique
      26             : inline
      27        3265 : void check_duplicate_variable_names(const data::variable_list& x, const std::string& msg)
      28             : {
      29        3265 :   std::set<core::identifier_string> names;
      30        9128 :   for (const data::variable& v: x)
      31             :   {
      32        5863 :     auto p = names.insert(v.name());
      33        5863 :     if (!p.second)
      34             :     {
      35           0 :       throw mcrl2::runtime_error("Duplicate " + msg + " " + std::string(v.name()) + " encountered");
      36             :     }
      37             :   }
      38        3265 : }
      39             : 
      40             : class variable_context
      41             : {
      42             :   private:
      43             :     std::map<core::identifier_string, sort_expression> m_variables;
      44             : 
      45             :   protected:
      46             :     void typecheck_variable(const data_type_checker& typechecker, const variable& v) const;
      47             : 
      48             :   public:
      49        4857 :     variable_context()
      50        4857 :     { }
      51             : 
      52             :     explicit variable_context(const std::map<core::identifier_string, sort_expression>& variables)
      53             :       : m_variables(variables)
      54             :     { }
      55             : 
      56      121088 :     const std::map<core::identifier_string, sort_expression>& context() const
      57             :     {
      58      121088 :       return m_variables;
      59             :     }
      60             : 
      61             :     // Adds the elements of variables to variable_map without checking.
      62             :     template <typename VariableContainer>
      63        1335 :     void add_context_variables(const VariableContainer& variables)
      64             :     {
      65        9301 :       for (const data::variable& v: variables)
      66             :       {
      67        6631 :           m_variables[v.name()] = v.sort();
      68             :       }
      69        1335 :     }
      70             : 
      71             : 
      72             :     // Adds the elements of variables to variable_map
      73             :     // Throws an exception if a typecheck error is encountered
      74             :     template <typename VariableContainer>
      75        8016 :     void add_context_variables(const VariableContainer& variables, const data_type_checker& typechecker)
      76             :     {
      77             :       // first remove the existing entries
      78       24019 :       for (const data::variable& v: variables)
      79             :       {
      80        9990 :         m_variables.erase(v.name());
      81             :       }
      82             : 
      83       24019 :       for (const data::variable& v: variables)
      84             :       {
      85        9990 :         typecheck_variable(typechecker, v);
      86        9990 :         auto i = m_variables.find(v.name());
      87        9990 :         if (i == m_variables.end())
      88             :         {
      89        9990 :           m_variables[v.name()] = v.sort();
      90             :         }
      91             :         else
      92             :         {
      93           0 :           throw mcrl2::runtime_error("attempt to overload global variable " + core::pp(v.name()));
      94             :         }
      95             :       }
      96        8016 :     }
      97             : 
      98        1622 :     void clear()
      99             :     {
     100        1622 :       m_variables.clear();
     101        1622 :     }
     102             : };
     103             : 
     104             : } // namespace detail
     105             : 
     106             : } // namespace data
     107             : 
     108             : } // namespace mcrl2
     109             : 
     110             : #endif // MCRL2_DATA_DETAIL_VARIABLE_CONTEXT_H