unfold_pattern_matching.h

Go to the documentation of this file.

// Author(s): Ruud Koolen, Thomas Neele
// 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_DATA_UNFOLD_PATTERN_MATCHING_H
#define MCRL2_DATA_UNFOLD_PATTERN_MATCHING_H
 
#include "mcrl2/data/join.h"
#include "mcrl2/data/replace.h"
#include "mcrl2/data/representative_generator.h"
#include "mcrl2/data/substitutions/map_substitution.h"
#include "mcrl2/data/substitutions/variable_substitution.h"
 
namespace mcrl2::data
{
 
namespace detail
{
struct rule
{
  std::map<data_expression, data_expression> match_criteria;
  data_expression rhs;
  data_expression condition;
  variable_list variables;
 
  rule(const std::map<data_expression, data_expression>& mc,
       const data_expression& r,
       const data_expression& c,
       const variable_list& v)
  : match_criteria(mc)
  , rhs(r)
  , condition(c)
  , variables(v)
  {
    assert(condition.sort() == sort_bool::bool_());
  }
 
};
 
inline
std::ostream& operator<<(std::ostream& out, const rule& r)
{
  return out << core::detail::print_list(r.variables) << ". " << r.condition << " -> " << core::detail::print_map(r.match_criteria) << " = " << r.rhs;
}
 
 
inline
function_symbol get_top_fs(const data_expression& expr)
{
  if (is_function_symbol(expr))
  {
    return atermpp::down_cast<function_symbol>(expr);
  }
  if (is_application(expr))
  {
    const application& expr_appl = atermpp::down_cast<application>(expr);
    if (is_function_symbol(expr_appl.head()))
    {
      return atermpp::down_cast<function_symbol>(expr_appl.head());
    }
  }
  return function_symbol();
}
 
inline
data_expression construct_condition_rhs(const std::vector<rule>& rules, const data_expression& representative)
{
  // data_expression_vector negated_conditions;
  // for (const rule& r: rules)
  // {
  //   negated_conditions.push_back(sort_bool::not_(r.condition));
  // }
  // data_expression else_clause = join_and(negated_conditions.begin(), negated_conditions.end());
  // TODO: Check whether else_clause is equivalent to false. Can we use the enumerator for this?
 
  if (rules.size() == 0)
  {
    return representative;
  }
 
  data_expression result;
  for (const rule& r: rules)
  {
    std::map<variable, data_expression> substitution_map;
    for (const auto& [var_expr, pattern]: r.match_criteria)
    {
      assert(is_variable(pattern));
      substitution_map[atermpp::down_cast<variable>(pattern)] = var_expr;
    }
    map_substitution<std::map<variable, data_expression> > substitution(substitution_map);
 
    data_expression condition = replace_variables_capture_avoiding(r.condition, substitution);
    data_expression rhs = replace_variables_capture_avoiding(r.rhs, substitution);
 
    if (result == data_expression())
    {
      result = rhs;
    }
    else
    {
      result = lazy::if_(condition, rhs, result);
    }
  }
 
  return result;
}
 
template <typename StructInfo>
data_expression construct_rhs(
  StructInfo& ssf,
  representative_generator& gen,
  const std::vector<rule>& rules,
  const sort_expression& sort
)
{
  if (rules.empty())
  {
    return construct_condition_rhs(rules, gen(sort));
  }
 
  /*
   * For each matching rule LHS, check whether pattern matching needs to happen on that LHS.
   *
   * We prefer to match on an expression such that *all* rules perform matching on that expression.
   * For example, for a ruleset representing the following rewrite rules:
   *
   *   optionally_remove_first_element(false, l) = l
   *   optionally_remove_first_element(true, []) = []
   *   optionally_remove_first_element(true, x |> l) = l
   *
   * We prefer to pattern match on the first parameter, not the second. Pattern matching on the
   * second parameter will (recursively) happen only on the true-branch, not the false-branch.
   * Pattern matching on the second parameter is still possible if there is no other option, but
   * it requires splitting the first rewrite rule into different cases for different
   * constructors -- suboptimal.
   */
  data_expression matching_target;
  enum class MatchType
  {
    NONE, INCOMPLETE, PARTIAL, FULL
  };
  MatchType matching_type = MatchType::NONE;
  // iterate over matches, this is the same for all rules, so just use rules[0]
  // More formally, we have rules[i].match_criteria->first is equivalent for all i.
  for (const auto& [var_expr, _]: rules[0].match_criteria)
  {
    bool variable_seen = false;
    std::set<function_symbol> constructors_seen;
    for (const rule& r: rules)
    {
      const data_expression& pattern = r.match_criteria.at(var_expr);
      if (is_variable(pattern))
      {
        variable_seen = true;
      }
      else
      {
        // either function symbol or application of function symbol
        function_symbol fs = get_top_fs(pattern);
        // this also means fs != function_symbol()
        assert(ssf.is_constructor(fs));
        constructors_seen.insert(fs);
      }
    }
 
    MatchType new_matching_type;
    if (constructors_seen.empty())
    {
      // No pattern matching is possible on this variable.
      new_matching_type = MatchType::NONE;
    }
    else if (variable_seen)
    {
      // There are both rules that match on this variable and rules that do not.
      // That's better than an incomplete matching but worse than a full matching.
      new_matching_type = MatchType::PARTIAL;
    }
    else if (constructors_seen.size() != ssf.get_constructors(var_expr.sort()).size())
    {
      // There are constructors for which there are no rules.
      // Thus, we have an incomplete function definition, that needs to be completed artificially.
      // A partial matching would be a better choice.
      new_matching_type = MatchType::INCOMPLETE;
    }
    else
    {
      // There is a matching rule for each constructor, and no rule with a plain variable.
      // This variable is a perfect pattern matching candidate.
      new_matching_type = MatchType::FULL;
    }
 
    if (new_matching_type > matching_type)
    {
      matching_target = var_expr;
      matching_type = new_matching_type;
    }
    if (matching_type == MatchType::FULL)
    {
      break;
    }
  }
 
  if (matching_type == MatchType::NONE)
  {
    // No constructor-based matching needs to happen.
    // All that needs to happen is incorporating the rule conditions.
    return construct_condition_rhs(rules, gen(sort));
  }
 
  /*
   * For each constructor, find the set of rules that apply to it, rewritten to match the constructor.
   */
  // auto type below depends on the type of ssf
  const auto& match_constructors = ssf.get_constructors(matching_target.sort());
  std::map<function_symbol, std::vector<rule> > constructor_rules;
  for (const rule& r: rules)
  {
    const data_expression& pattern = r.match_criteria.at(matching_target);
    if (is_function_symbol(pattern) || is_application(pattern))
    {
      /*
       * For a rule with a constructor pattern, strip the constructor and
       * introduce patterns for the constructor parameters.
       */
      function_symbol constructor = get_top_fs(pattern);
      assert(constructor != function_symbol());
      assert(utilities::detail::contains(match_constructors, constructor));
 
      data_expression_vector parameters;
      if (is_application(pattern))
      {
        const application& pattern_appl = atermpp::down_cast<application>(pattern);
        parameters.insert(parameters.end(), pattern_appl.begin(), pattern_appl.end());
      }
 
      rule rule = r;
      rule.match_criteria.erase(matching_target);
      // To prevent creating expressions of the shape head(l) |> tail(l), we perform a substitution here
      // This is only safe if there are no binders in the right-hand side
      std::set<data_expression> subexpr = find_data_expressions(rule.rhs);
      if (!parameters.empty() && std::none_of(subexpr.begin(), subexpr.end(), [](const data_expression& e) { return is_abstraction(e); }))
      {
        auto sigma = [&](const data_expression& x) { return x == pattern ? matching_target : x; };
        rule.rhs = replace_data_expressions(rule.rhs, sigma, true);
        rule.condition = replace_data_expressions(rule.condition, sigma, true);
      }
      for (std::size_t j = 0; j < parameters.size(); j++)
      {
        function_symbol projection_function = ssf.get_projection_funcs(constructor)[j];
        data_expression lhs_expression = application(projection_function, matching_target);
        rule.match_criteria[lhs_expression] = parameters[j];
      }
      constructor_rules[constructor].push_back(rule);
    }
    else
    {
      /*
       * For a rule with a variable pattern that nonetheless needs to pattern match
       * against the possible constructors for that variable, copy the rule for each
       * possible constructor. Substitute the original un-matched term for the pattern
       * variable that disappears.
       */
      assert(is_variable(pattern));
      variable_substitution sigma(atermpp::down_cast<variable>(pattern), matching_target);
      data_expression condition = replace_variables_capture_avoiding(r.condition, sigma);
      data_expression rhs = replace_variables_capture_avoiding(r.rhs, sigma);
 
      for (const function_symbol& f: match_constructors)
      {
        rule rule(r.match_criteria, rhs, condition, r.variables);
        rule.match_criteria.erase(matching_target);
 
        set_identifier_generator generator;
        for (const variable& v: r.variables)
        {
          generator.add_identifier(v.name());
        }
 
        if (is_function_sort(f.sort()))
        {
          function_sort sort(f.sort());
          std::size_t index = 0;
          for (const sort_expression& s: sort.domain())
          {
            variable variable(generator("v"), s);
            function_symbol projection_function = ssf.get_projection_funcs(f)[index];
            data_expression lhs_expression = application(projection_function, matching_target);
            rule.match_criteria[lhs_expression] = variable;
            index++;
          }
        }
 
        constructor_rules[f].push_back(rule);
      }
    }
  }
 
  /*
   * Construct an rhs of the form if(is_cons1, rhs_cons1, if(is_cons2, rhs_cons2, ...)) or equivalent
   * The exact form depends on the implementation in ssf
   */
  data_expression_vector rhs;
  for (const auto& f: match_constructors)
  {
    rhs.push_back(construct_rhs(ssf, gen, constructor_rules[f], sort));
  }
  return ssf.create_cases(matching_target, rhs);
}
 
} // namespace detail
 
template <typename StructInfo>
bool is_pattern_matching_rule(StructInfo& ssf, const data_equation& rewrite_rule)
{
  // For this rewrite rule to be usable in pattern matching, its lhs must only contain
  // constructor functions and variables that occur at most once.
 
  std::set<data_expression> subexpressions = find_data_expressions(rewrite_rule.lhs());
  subexpressions.erase(rewrite_rule.lhs());
  if (is_application(rewrite_rule.lhs()))
  {
    subexpressions.erase(application(rewrite_rule.lhs()).head());
  }
 
  bool all_pattern = std::all_of(subexpressions.begin(), subexpressions.end(), [&ssf](const data_expression& expr) {
    return
      is_variable(expr) ||
      (is_function_symbol(expr) && ssf.is_constructor(atermpp::down_cast<function_symbol>(expr))) ||
      (is_application(expr) && is_function_symbol(atermpp::down_cast<application>(expr).head()) &&
                          ssf.is_constructor(function_symbol(atermpp::down_cast<application>(expr).head())));
  });
  if (!all_pattern)
  {
    return false;
  }
  if (std::all_of(subexpressions.begin(), subexpressions.end(), [](const data_expression& x){ return is_variable(x); }))
  {
    // Each argument is a variable, this is just an ordinarily defined function
    return false;
  }
 
  // Check whether each variable occurs at most once
  std::set<variable> variable_set;
  std::multiset<variable> variable_multiset;
  find_all_variables(rewrite_rule.lhs(), std::inserter(variable_set, variable_set.end()));
  find_all_variables(rewrite_rule.lhs(), std::inserter(variable_multiset, variable_multiset.end()));
  return variable_set.size() == variable_multiset.size();
}
 
template <typename StructInfo>
data_equation unfold_pattern_matching(
  const function_symbol& mapping,
  const data_equation_vector& rewrite_rules,
  StructInfo& ssf,
  representative_generator& gen,
  set_identifier_generator& id_gen
)
{
  sort_expression codomain = mapping.sort().target_sort();
  variable_vector temp_par;
  if (is_function_sort(mapping.sort()))
  {
    const function_sort& sort = atermpp::down_cast<function_sort>(mapping.sort());
    for (sort_expression s: sort.domain())
    {
      temp_par.push_back(variable(id_gen("x"), s));
    }
  }
  variable_list new_parameters(temp_par.begin(), temp_par.end());
 
  // Create a rule for each data_equation
  std::vector<detail::rule> rules;
  for (const data_equation& eq: rewrite_rules)
  {
    assert(is_pattern_matching_rule(ssf, eq));
 
    std::map<data_expression, data_expression> match_criteria;
    if (is_application(eq.lhs()))
    {
      const application& lhs_appl = atermpp::down_cast<application>(eq.lhs());
 
      assert(lhs_appl.head() == mapping);
      assert(new_parameters.size() == lhs_appl.size());
 
      // Simultaneously iterate the parameters defined by the mapping and this
      // left-hand side to determine how matching occurs
      auto mappar_it = new_parameters.begin();
      auto lhspar_it = lhs_appl.begin();
      while(mappar_it != new_parameters.end())
      {
        match_criteria[*mappar_it] = *lhspar_it;
        ++mappar_it, ++lhspar_it;
      }
 
      assert(lhspar_it == lhs_appl.end());
    }
 
    detail::rule rule(match_criteria, eq.rhs(), eq.condition(), eq.variables());
    rules.push_back(rule);
  }
#ifdef MCRL2_ENABLE_MACHINENUMBERS
  assert(rules.size() != 0 || sort_pos::is_most_significant_digit_function_symbol(mapping));
#else 
  assert(rules.size() != 0);
#endif
 
  data_expression new_lhs(application(mapping, new_parameters));
  data_expression new_rhs(construct_rhs(ssf, gen, rules, codomain));
  return data_equation(new_parameters, new_lhs, new_rhs);
}
 
} // namespace mcrl2::data
 
#endif