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: LA 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
sourceimpl<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.
Trait Implementations
Auto Trait Implementations
impl<L> RefUnwindSafe for TreeTerm<L> where
L: RefUnwindSafe,
impl<L> !Send for TreeTerm<L>
impl<L> !Sync for TreeTerm<L>
impl<L> Unpin for TreeTerm<L> where
L: Unpin,
impl<L> UnwindSafe for TreeTerm<L> where
L: UnwindSafe + RefUnwindSafe,
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcepub fn borrow_mut(&mut self) -> &mut T
pub fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
sourceimpl<T> ToOwned for T where
T: Clone,
impl<T> ToOwned for T where
T: Clone,
type Owned = T
type Owned = T
The resulting type after obtaining ownership.
sourcepub fn to_owned(&self) -> T
pub fn to_owned(&self) -> T
Creates owned data from borrowed data, usually by cloning. Read more
sourcepub fn clone_into(&self, target: &mut T)
pub fn clone_into(&self, target: &mut T)
toowned_clone_into)Uses borrowed data to replace owned data, usually by cloning. Read more