pub struct TreeTerm<L: Language> {
pub node: L,
pub backward_rule: Option<Symbol>,
pub forward_rule: Option<Symbol>,
pub child_proofs: Vec<TreeExplanation<L>>,
/* private fields */
}
Expand description
An explanation for a term and its equivalent children.
Each child is a proof transforming the initial child into the final child term.
The initial term is given by taking each first sub-term
in each child_proofs
recursively.
The final term is given by all of the final terms in each child_proofs
.
If forward_rule
is provided, then this TreeTerm’s initial term
can be derived from the previous
TreeTerm by applying the rule.
Similarly, if backward_rule
is provided,
then the previous TreeTerm’s final term is given by applying the rule to this TreeTerm’s initial term.
TreeTerms are flattened by first flattening child_proofs
, then wrapping
the flattened proof with this TreeTerm’s node.
Fields§
§node: L
A node representing this TreeTerm’s operator. The children of the node should be ignored.
backward_rule: Option<Symbol>
A rule rewriting this TreeTerm’s initial term back to the last TreeTerm’s final term.
forward_rule: Option<Symbol>
A rule rewriting the last TreeTerm’s final term to this TreeTerm’s initial term.
child_proofs: Vec<TreeExplanation<L>>
A list of child proofs, each transforming the initial term to the final term for that child.
Implementations§
source§impl<L: Language> TreeTerm<L>
impl<L: Language> TreeTerm<L>
sourcepub fn new(node: L, child_proofs: Vec<TreeExplanation<L>>) -> TreeTerm<L>
pub fn new(node: L, child_proofs: Vec<TreeExplanation<L>>) -> TreeTerm<L>
Construct a new TreeTerm given its node and child_proofs.
sourcepub fn get_initial_flat_term(&self) -> FlatTerm<L>
pub fn get_initial_flat_term(&self) -> FlatTerm<L>
Get a FlatTerm representing the first term in this proof.
sourcepub fn get_last_flat_term(&self) -> FlatTerm<L>
pub fn get_last_flat_term(&self) -> FlatTerm<L>
Get a FlatTerm representing the final term in this proof.
sourcepub fn flatten_explanation(&self) -> FlatExplanation<L>
pub fn flatten_explanation(&self) -> FlatExplanation<L>
Construct the FlatExplanation
for this TreeTerm.