is_well_typed.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_LPS_IS_WELL_TYPED_H
#define MCRL2_LPS_IS_WELL_TYPED_H
 
#include "mcrl2/data/detail/sequence_algorithm.h"
#include "mcrl2/lps/detail/action_utility.h"
#include "mcrl2/lps/stochastic_specification.h"
#include <boost/iterator/transform_iterator.hpp>
 
namespace mcrl2 {
 
namespace lps {
 
namespace detail
{
 
struct lps_well_typed_checker
{
  // The result of the last well typedness check.
  bool result;
 
  // Error message are written to the output stream error.
  mutable std::ostringstream error;
 
  lps_well_typed_checker()
    : result(false)
  {}
 
  bool check_time(const data::data_expression& t, const std::string& type) const
  {
    if (!data::sort_real::is_real(t.sort()))
    {
      error << "is_well_typed(" << type << ") failed: time " << t << " doesn't have sort real." << std::endl;
      return false;
    }
    return true;
  }
 
  bool check_condition(const data::data_expression& t, const std::string& type) const
  {
    if (!data::sort_bool::is_bool(t.sort()))
    {
      error << "is_well_typed(" << type << ") failed: condition " << t << " doesn't have sort bool." << std::endl;
      return false;
    }
    return true;
  }
 
  bool check_assignments(const data::assignment_list& l, const std::string& type) const
  {
    if (!is_well_typed_container(l))
    {
      error << "is_well_typed(" << type << ") failed: the assignments " << l << " are not well typed." << std::endl;
      return false;
    }
    auto lhs = [](const data::assignment& a) { return a.lhs(); };
    if (data::detail::sequence_contains_duplicates(
          boost::make_transform_iterator(l.begin(), lhs),
          boost::make_transform_iterator(l.end()  , lhs)
        )
       )
    {
      error << "is_well_typed(" << type << ") failed: data assignments " << l << " don't have unique left hand sides." << std::endl;
      return false;
    }
    return true;
  }
 
  template <typename Container>
  bool is_well_typed_container(const Container& c) const
  {
    for (auto i = c.begin(); i != c.end(); ++i)
    {
      if (!is_well_typed(*i))
      {
        return false;
      }
    }
    return true;
  }
 
  bool is_well_typed(const data::sort_expression& d) const
  {
    (void)d; // Suppress an unused variable warning.
    return true;
  }
 
  bool is_well_typed(const data::variable& d) const
  {
    (void)d; // Suppress an unused variable warning.
    return true;
  }
 
  bool is_well_typed(const data::data_expression& d) const
  {
    (void)d; // Suppress an unused variable warning.
    return true;
  }
 
  bool is_well_typed(const data::assignment& a) const
  {
    if (a.lhs().sort() != a.rhs().sort())
    {
      std::clog << "is_well_typed(data_assignment) failed: the left and right hand sides "
                << a.lhs() << " and " << a.rhs() << " have different sorts." << std::endl;
      return false;
    }
    return true;
  }
 
  bool is_well_typed(const process::action_label& d) const
  {
    (void)d; // Suppress an unused variable warning.
    return true;
  }
 
  bool is_well_typed(const process::action& a) const
  {
    (void)a; // Suppress an unused variable warning.
    return true;
  }
 
  bool is_well_typed(const deadlock& d) const
  {
    if (d.has_time())
    {
      check_time(d.time(), "deadlock");
    }
    return true;
  }
 
  bool is_well_typed(const multi_action& a) const
  {
    if (a.has_time())
    {
      check_time(a.time(), "multi_action");
    }
    return true;
  }
 
  bool is_well_typed(const action_summand& s) const
  {
    if (!data::detail::unique_names(s.summation_variables()))
    {
      error << "is_well_typed(action_summand) failed: summation variables " << core::detail::print_list(s.summation_variables()) << " don't have unique names." << std::endl;
      return false;
    }
    if (!check_condition(s.condition(), "action_summand"))
    {
      return false;
    }
    if (!is_well_typed(s.multi_action()))
    {
      return false;
    }
    if (!check_assignments(s.assignments(), "action_summand"))
    {
      return false;
    }
    return true;
  }
 
  bool is_well_typed(const deadlock_summand& s) const
  {
    if (!check_condition(s.condition(), "deadlock_summand"))
    {
      return false;
    }
    if (!is_well_typed(s.deadlock()))
    {
      return false;
    }
    return true;
  }
 
  template <typename ActionSummand>
  bool is_well_typed(const linear_process_base<ActionSummand>& p) const
  {
    // check 2)
    if (!data::detail::unique_names(p.process_parameters()))
    {
      error << "is_well_typed(linear_process) failed: process parameters " << core::detail::print_list(p.process_parameters()) << " don't have unique names." << std::endl;
      return false;
    }
 
    // check 4)
    std::set<core::identifier_string> names;
    for (auto i = p.process_parameters().begin(); i != p.process_parameters().end(); ++i)
    {
      names.insert(i->name());
    }
    for (auto i = p.action_summands().begin(); i != p.action_summands().end(); ++i)
    {
      if (!data::detail::check_variable_names(i->summation_variables(), names))
      {
        error << "is_well_typed(linear_process) failed: some of the names of the summation variables " << core::detail::print_list(i->summation_variables()) << " also appear as process parameters." << std::endl;
        return false;
      }
    }
 
    // check 5)
    for (auto i = p.action_summands().begin(); i != p.action_summands().end(); ++i)
    {
      if (!data::detail::check_assignment_variables(i->assignments(), p.process_parameters()))
      {
        error << "is_well_typed(linear_process) failed: some left hand sides of the assignments " << core::detail::print_list(i->assignments()) << " do not appear as process parameters." << std::endl;
        return false;
      }
    }
 
    // check 6)
    if (!is_well_typed_container(p.action_summands()))
    {
      return false;
    }
    if (!is_well_typed_container(p.deadlock_summands()))
    {
      return false;
    }
    return true;
  }
 
  template <typename LinearProcess, typename InitialProcessExpression>
  bool is_well_typed(const specification_base<LinearProcess, InitialProcessExpression>& spec,
                     const std::set<data::variable>& free_variables) const
  {
    std::set<data::sort_expression> declared_sorts = data::detail::make_set(spec.data().sorts());
    std::set<process::action_label> declared_labels = data::detail::make_set(spec.action_labels());
    auto const& action_summands = spec.process().action_summands();
 
    // check 1)
    for (auto i = action_summands.begin(); i != action_summands.end(); ++i)
    {
      if (!(data::detail::check_variable_sorts(i->summation_variables(), declared_sorts)))
      {
        error << "is_well_typed(specification) failed: some of the sorts of the summation variables " << core::detail::print_list(i->summation_variables()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl;
        return false;
      }
    }
 
    // check 2)
    if (!(data::detail::check_variable_sorts(spec.process().process_parameters(), declared_sorts)))
    {
      error << "is_well_typed(specification) failed: some of the sorts of the process parameters " << core::detail::print_list(spec.process().process_parameters()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl;
      return false;
    }
 
    // check 3)
    if (!(data::detail::check_variable_sorts(spec.global_variables(), declared_sorts)))
    {
      error << "is_well_typed(specification) failed: some of the sorts of the free variables " << core::detail::print_list(spec.global_variables()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl;
      return false;
    }
 
    // check 4)
    if (!(detail::check_action_label_sorts(spec.action_labels(), declared_sorts)))
    {
      error << "is_well_typed(specification) failed: some of the sorts occurring in the action labels " << core::detail::print_list(spec.action_labels()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl;
      return false;
    }
 
    // check 5)
    for (const action_summand& s: action_summands)
    {
      if (!(detail::check_action_labels(s.multi_action().actions(), declared_labels)))
      {
        error << "is_well_typed(specification) failed: some of the labels occurring in the actions " << core::detail::print_list(s.multi_action().actions()) << " are not declared in the action specification " << core::detail::print_list(spec.action_labels()) << std::endl;
        return false;
      }
    }
    if (!is_well_typed(spec.process()))
    {
      return false;
    }
    if (!spec.data().is_well_typed())
    {
      return false;
    }
    if (!free_variables.empty())
    {
      error << "is_well_typed(specification) failed: some of the free variables were not declared\n";
      error << "declared global variables: " << core::detail::print_list(spec.global_variables()) << std::endl;
      error << "occurring free variables: " << core::detail::print_list(free_variables) << std::endl;
      return false;
    }
 
    // check 3)
    if (!data::detail::unique_names(spec.global_variables()))
    {
      error << "is_well_typed(specification) failed: global variables " << core::detail::print_list(spec.global_variables()) << " don't have unique names." << std::endl;
      return false;
    }
 
    return true;
  }
 
  bool is_well_typed(const specification& spec) const
  {
    std::set<data::variable> free_variables = lps::find_free_variables(spec);
    return is_well_typed(spec, free_variables);
  }
 
  bool is_well_typed(const stochastic_specification& spec) const
  {
    std::set<data::variable> free_variables = lps::find_free_variables(spec);
    return is_well_typed(spec, free_variables);
  }
 
  template <typename Term>
  bool operator()(const Term& t) const
  {
    return is_well_typed(t);
  }
};
 
template <typename T>
bool is_well_typed(const T& x)
{
  lps::detail::lps_well_typed_checker checker;
  return checker(x);
}
 
template <typename T>
bool check_well_typedness(const T& x)
{
  lps::detail::lps_well_typed_checker checker;
  bool result = checker(x);
  if (!result)
  {
    mCRL2log(log::error) << checker.error.str();
  }
  return result;
}
 
} // namespace detail
 
} // namespace lps
 
} // namespace mcrl2
 
#endif // MCRL2_LPS_IS_WELL_TYPED_H