Documentation

Aesop.Index.RulePattern

@[reducible, inline]

A map from rule names to rule pattern substitutions. When run on a goal, the rule pattern index returns such a map.

Equations

Insert an array of rule pattern substitutions into a rule pattern substitution map.

Equations
  • One or more equations did not get rendered due to their size.

Build a rule pattern substitution map from an array of substitutions.

Equations

Convert a rule pattern substitution map to a flat array of substitutions.

Equations
  • One or more equations did not get rendered due to their size.

An entry of the rule pattern index.

  • name : RuleName

    The name of the rule to which the pattern belongs.

  • pattern : RulePattern

    The rule's pattern. We assume that there is at most one pattern per rule.

Instances For

A rule pattern index. Maps expressions e to rule patterns that likely unify with e.

Instances For
Equations
  • One or more equations did not get rendered due to their size.

Add a rule pattern to the index.

Equations

Merge two rule pattern indices. Patterns that appear in both indices appear twice in the result.

Equations

Get rule pattern substitutions for the patterns that match e.

Equations
  • One or more equations did not get rendered due to their size.

Get all substitutions of the rule patterns that match a subexpression of e. Subexpressions containing bound variables are not considered. The returned array may contain duplicates.

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

Get all substitutions of the rule patterns that match a subexpression of e. Subexpressions containing bound variables are not considered. The returned array may contain duplicates.

Equations

Get all substitutions of the rule patterns that match a subexpression of the given local declaration. Subexpressions containing bound variables are not considered.

Equations
  • One or more equations did not get rendered due to their size.

Get all substitutions of the rule patterns that match a subexpression of the given local declaration. Subexpressions containing bound variables are not considered.

Equations

Get all substitutions of the rule patterns that match a subexpression of a hypothesis or the target. Subexpressions containing bound variables are not considered.

Equations
  • One or more equations did not get rendered due to their size.