pub struct FlatTerm<L: Language> {
pub node: L,
pub backward_rule: Option<Symbol>,
pub forward_rule: Option<Symbol>,
pub children: FlatExplanation<L>,
}
Expand description
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 FlatTerm
s,
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§
source§impl<L: Language> FlatTerm<L>
impl<L: Language> FlatTerm<L>
sourcepub fn remove_rewrites(&self) -> FlatTerm<L>
pub fn remove_rewrites(&self) -> FlatTerm<L>
Remove the rewrite annotation from this flatterm, if any.
source§impl<L: Language + Display + FromOp> FlatTerm<L>
impl<L: Language + Display + FromOp> FlatTerm<L>
sourcepub fn get_string(&self) -> String
pub fn get_string(&self) -> String
Convert this FlatTerm to an S-expression.
See get_flat_string
for the format of these expressions.
sourcepub fn get_recexpr(&self) -> RecExpr<L>
pub fn get_recexpr(&self) -> RecExpr<L>
Convert this FlatTerm to a RecExpr.
source§impl<L: Language> FlatTerm<L>
impl<L: Language> FlatTerm<L>
sourcepub fn new(node: L, children: FlatExplanation<L>) -> FlatTerm<L>
pub fn new(node: L, children: FlatExplanation<L>) -> FlatTerm<L>
Construct a new FlatTerm given a node and its children.
sourcepub fn rewrite(&self, lhs: &PatternAst<L>, rhs: &PatternAst<L>) -> FlatTerm<L>
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.
sourcepub fn has_rewrite_forward(&self) -> bool
pub fn has_rewrite_forward(&self) -> bool
Checks if this term or any child has a forward_rule
.
sourcepub fn has_rewrite_backward(&self) -> bool
pub fn has_rewrite_backward(&self) -> bool
Checks if this term or any child has a backward_rule
.
Trait Implementations§
source§impl<L: Language> PartialEq<FlatTerm<L>> for FlatTerm<L>
impl<L: Language> PartialEq<FlatTerm<L>> for FlatTerm<L>
impl<L: Eq + Language> Eq for FlatTerm<L>
impl<L: Language> StructuralEq for FlatTerm<L>
Auto Trait Implementations§
impl<L> RefUnwindSafe for FlatTerm<L>where
L: RefUnwindSafe,
impl<L> Send for FlatTerm<L>where
L: Send,
impl<L> Sync for FlatTerm<L>where
L: Sync,
impl<L> Unpin for FlatTerm<L>where
L: Unpin,
impl<L> UnwindSafe for FlatTerm<L>where
L: UnwindSafe,
Blanket Implementations§
source§impl<Q, K> Equivalent<K> for Qwhere
Q: Eq + ?Sized,
K: Borrow<Q> + ?Sized,
impl<Q, K> Equivalent<K> for Qwhere
Q: Eq + ?Sized,
K: Borrow<Q> + ?Sized,
source§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
key
and return true
if they are equal.