mcrl2/data/unfold_pattern_matching.h

Include file:

#include "mcrl2/data/unfold_pattern_matching.h"

Classes

• mcrl2::data::detail::rule

Functions

bool mcrl2::data::is_pattern_matching_rule(StructInfo &ssf, const data_equation &rewrite_rule)

Check whether the given rewrite rule can be classified as a pattern matching rule.

That is, its arguments are constructed only out of unique variable occurrences and constructor function symbols and constructor function applications.

data_equation mcrl2::data::unfold_pattern_matching(const function_symbol &mapping, const data_equation_vector &rewrite_rules, StructInfo &ssf, representative_generator &gen, set_identifier_generator &id_gen)

This converts a collection of rewrite rules for a give function symbol into a one-rule specification of the function, using recogniser and projection functions to implement pattern matching.

For example, the collection of rewrite rules below:sign_of_list_sum([]) = false; is_even(n) -> sign_of_list_sum(n |> l) = sign_of_list_sum(l); !is_even(n) -> sign_of_list_sum(n |> l) = !sign_of_list_sum(l);gets translated into the following function specification:sign_of_list_sum(l) = if(is_emptylist(l), false, if(is_even(head(l)), sign_of_list_sum(tail(l)), !sign_of_list_sum(tail(l))))Two complications can arise. The rewrite rule set may contain rules that do not pattern-match on the function parameters, such as 'not(not(b)) = b`; rules like these are discarded. More problematically, the set of rewrite rules may not be complete, or may not easily be proven complete; in the example above, if the rewriter cannot rewrite 'is_even(n) || !is_even(n)’ to ‘true’, the translation cannot tell that the rewrite rule set is complete. In cases where a (non-constructor )function invocation can genuinely not be rewritten any further, the MCRL2 semantics are unspecified (TODO check this); the translation resolves this situation by returning an arbitrary value in this case. Thus, in practice, the function definion above might well be translated into the following:sign_of_list_sum(l) = if(is_emptylist(l), false, if(is_even(head(l)), sign_of_list_sum(tail(l)), if(!is_even(head(l)), !sign_of_list_sum(tail(l)), false)))Where ‘false’ is a representative of sort_bool.

Functions

static data_expression mcrl2::data::detail::construct_condition_rhs(const std::vector<rule> &rules, const data_expression &representative)

For a list of rules with equal left hand sides of match_criteria and only variables in the right hand sides of match_criteria, construct a right hand side based on the conditions and right hand sides of the rules.

data_expression mcrl2::data::detail::construct_rhs(StructInfo &ssf, representative_generator &gen, const std::vector<rule> &rules, const sort_expression &sort)

For a list of rules with equal left hand sides of match_criteria, construct a right hand side.

function_symbol mcrl2::data::detail::get_top_fs(const data_expression &expr)

Get the top level function symbol f if expr is of the shape f or f(t1,…,tn)

Parameters:

• expr The expression from which to extract the top function symbol

Returns: The top function symbol, or function_symbol() if it has none

std::ostream &mcrl2::data::detail::operator<<(std::ostream &out, const rule &r)