A rule describes a partially pattern-matched rewrite rule. More...

#include <unfold_pattern_matching.h>

Public Member Functions
	rule (const std::map< data_expression, data_expression > &mc, const data_expression &r, const data_expression &c, const variable_list &v)

Public Attributes
std::map< data_expression, data_expression >	match_criteria

data_expression	rhs

data_expression	condition

variable_list	variables

Detailed Description

A rule describes a partially pattern-matched rewrite rule.

match_criteria is a set of data_expression pairs (A, B) where A is a data_expression over variables in the left hand side of a function definition, and B is a pattern consisting of constructor applications over free variables.

The rule match_criteria = { (A, B), (C, D) }, condition = E, rhs = R describes the following rewrite proposition:

"if the data expression A pattern-matches to pattern B, and the data expression C pattern-matches to pattern D, and the condition E is true after substituting the proper pattern-matching variables, then the right hand side R applies (again with substitution of pattern-matched variables."

Pattern matching can then be performed by deconstructing the patterns in the right hand sides of match_criteria, and rewriting rules accordingly. As an example, the following rewrite rule:

is_even(n) -> sign_of_list_sum(n |> l) = sign_of_list_sum(l)

Can be represented as the following rule:

match_criteria = { v1 -> n |> l }, condition = is_even(n), rhs = sign_of_list_sum(l)

Which, after one step of pattern matching, gets simplified to the following rule:

match_criteria = { head(v1) -> n, tail(v1) -> l }, condition = is_even(n), rhs = sign_of_list_sum(l)

Definition at line 54 of file unfold_pattern_matching.h.

Constructor & Destructor Documentation

◆ rule()

mcrl2::data::detail::rule::rule	(	const std::map< data_expression, data_expression > &	mc,
		const data_expression &	r,
		const data_expression &	c,
		const variable_list &	v
	)

inline

Definition at line 61 of file unfold_pattern_matching.h.

Member Data Documentation

◆ condition

data_expression mcrl2::data::detail::rule::condition

Definition at line 58 of file unfold_pattern_matching.h.

◆ match_criteria

std::map<data_expression, data_expression> mcrl2::data::detail::rule::match_criteria

Definition at line 56 of file unfold_pattern_matching.h.

◆ rhs

data_expression mcrl2::data::detail::rule::rhs

Definition at line 57 of file unfold_pattern_matching.h.

◆ variables

variable_list mcrl2::data::detail::rule::variables

Definition at line 59 of file unfold_pattern_matching.h.

The documentation for this struct was generated from the following file:

data/include/mcrl2/data/unfold_pattern_matching.h

Public Member Functions

Public Attributes