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/merge_data_specifications.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_MERGE_DATA_SPECIFICATIONS_H
      13             : #define MCRL2_DATA_MERGE_DATA_SPECIFICATIONS_H
      14             : 
      15             : #include "mcrl2/data/typecheck.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace data {
      20             : 
      21             : /// \brief Merges two data specifications.  Throws an exception if conflicts are detected.
      22             : /// \details If the data specifications have equal aliases, types, constructors or functions these are merged.
      23             : /// \param[in] dataspec1 The first data specification to be merged.
      24             : /// \param[out] dataspec2 The second data specification to be merged.
      25             : /// \return The merged data specification.
      26             : inline
      27           9 : data_specification merge_data_specifications(const data_specification& dataspec1, const data_specification& dataspec2)
      28             : {
      29           9 :   data_specification result = dataspec1;
      30             :  
      31             :   // Merge the sorts.
      32          10 :   for(const basic_sort& s: dataspec2.user_defined_sorts())
      33             :   {
      34           1 :     if (std::find(dataspec1.user_defined_sorts().begin(),dataspec1.user_defined_sorts().end(),s)==dataspec1.user_defined_sorts().end())
      35             :     {
      36           0 :       result.add_sort(s);
      37             :     }
      38             :   }
      39             : 
      40             :   // Merge the aliases.
      41          15 :   for(const alias& a: dataspec2.user_defined_aliases())
      42             :   {
      43           6 :     if (std::find(dataspec1.user_defined_aliases().begin(),dataspec1.user_defined_aliases().end(),a)==dataspec1.user_defined_aliases().end())
      44             :     {
      45           0 :       result.add_alias(a);
      46             :     }
      47             :   }
      48             : 
      49             :   // Merge the constructors.
      50          10 :   for(const function_symbol& f: dataspec2.user_defined_constructors())
      51             :   {
      52           1 :     if (std::find(dataspec1.user_defined_constructors().begin(),dataspec1.user_defined_constructors().end(),f)==
      53           2 :                                 dataspec1.user_defined_constructors().end())
      54             :     {
      55           0 :       result.add_constructor(f);
      56             :     }
      57             :   }
      58             : 
      59             :   // Merge the mappings.
      60          13 :   for(const function_symbol& f: dataspec2.user_defined_mappings())
      61             :   {
      62           4 :     if (std::find(dataspec1.user_defined_mappings().begin(),dataspec1.user_defined_mappings().end(),f)==dataspec1.user_defined_mappings().end())
      63             :     {
      64           0 :       result.add_mapping(f);
      65             :     }
      66             :   }
      67             : 
      68             :   // Merge the data equations.
      69          13 :   for(const data_equation& e: dataspec2.user_defined_equations())
      70             :   {
      71           4 :     if (std::find(dataspec1.user_defined_equations().begin(),dataspec1.user_defined_equations().end(),e)==dataspec1.user_defined_equations().end())
      72             :     {
      73           0 :       result.add_equation(e);
      74             :     }
      75             :   }
      76             : 
      77           9 :   data_type_checker type_checker(result);
      78             :   try
      79             :   {
      80             :     // Type check the resulting specification.
      81             :     // Throw an exception when there is an issue.
      82           9 :     type_checker();
      83             :   }
      84           0 :   catch (mcrl2::runtime_error& e)
      85             :   {
      86           0 :     throw mcrl2::runtime_error(std::string("Merging of two data specifications fails.\n") + e.what());
      87           0 :   }
      88             : 
      89          18 :   return result;
      90           9 : }
      91             : 
      92             : } // namespace data
      93             : 
      94             : } // namespace mcrl2
      95             : 
      96             : #endif // MCRL2_DATA_MERGE_DATA_SPECIFICATIONS_H