Struct FlatTerm 

pub struct FlatTerm<L: Language> {
    pub node: L,
    pub backward_rule: Option<Symbol>,
    pub forward_rule: Option<Symbol>,
    pub children: FlatExplanation<L>,
}

A single term in an flattened explanation. After the first term in a FlatExplanation, each term will be annotated with exactly one backward_rule or one forward_rule. This can appear in children FlatTerms, indicating that the child is being rewritten.

When forward_rule is provided, the previous FlatTerm can be rewritten to this FlatTerm by applying the rule. When backward_rule is provided, the previous FlatTerm is given by applying the rule to this FlatTerm. Rules are either the string of the name of the rule or the reason provided to union_instantiations.

Fields

node: L

The node representing this FlatTerm’s operator. The children of the node should be ignored.

backward_rule: Option<Symbol>

A rule rewriting this FlatTerm back to the last FlatTerm.

forward_rule: Option<Symbol>

A rule rewriting the last FlatTerm to this FlatTerm.

children: FlatExplanation<L>

The children of this FlatTerm.

Implementations

impl<L: Language> FlatTerm<L>

pub fn remove_rewrites(&self) -> FlatTerm<L>

Remove the rewrite annotation from this flatterm, if any.

impl<L: Language + Display + FromOp> FlatTerm<L>

pub fn get_string(&self) -> String

Convert this FlatTerm to an S-expression. See get_flat_string for the format of these expressions.

pub fn get_recexpr(&self) -> RecExpr<L>

Convert this FlatTerm to a RecExpr.

impl<L: Language> FlatTerm<L>

pub fn new(node: L, children: FlatExplanation<L>) -> FlatTerm<L>

Construct a new FlatTerm given a node and its children.

pub fn rewrite(&self, lhs: &PatternAst<L>, rhs: &PatternAst<L>) -> FlatTerm<L>

Rewrite the FlatTerm by matching the lhs and substituting the rhs. The lhs must be guaranteed to match.

pub fn has_rewrite_forward(&self) -> bool

Checks if this term or any child has a forward_rule.

pub fn has_rewrite_backward(&self) -> bool

Checks if this term or any child has a backward_rule.

Trait Implementations

impl<L: Clone + Language> Clone for FlatTerm<L>

fn clone(&self) -> FlatTerm<L>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<L: Debug + Language> Debug for FlatTerm<L>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<L: Language + Display + FromOp> Display for FlatTerm<L>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<L: Language> PartialEq for FlatTerm<L>

fn eq(&self, other: &FlatTerm<L>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<L: Eq + Language> Eq for FlatTerm<L>