Struct TagValNode 

pub struct TagValNode<Tag, Left, Right>(pub Left, pub Right, pub PhantomData<Tag>);

One of the dependent family of combinators

Balanced binary tree node for tag-value choices.

Tuple Fields

0: Left

1: Right

2: PhantomData<Tag>

Trait Implementations

impl<Tag, Left, Right> DepCombinator for TagValNode<Tag, Left, Right>

where Left: DepCombinator<Key = Tag>, Right: DepCombinator<Key = Tag>,

open spec fn apply(&self, key: Self::Key) -> Self::Body

{ Choice(self.0.apply(key), self.1.apply(key)) }

open spec fn recover(&self, value: Self::Val) -> Self::Key

{
    match value {
        Sum::Inl(vl) => self.0.recover(vl),
        Sum::Inr(vr) => self.1.recover(vr),
    }
}

open spec fn recover_inv(&self) -> bool

{ self.0.recover_inv() && self.1.recover_inv() }

proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val)

type Key = Tag

The type of keys parsed by the head combinator/to be recovered during serialization.

type Val = Sum<<Left as DepCombinator>::Val, <Right as DepCombinator>::Val>

The type of values consumed/produced by the body combinator.

type Body = Choice<<Left as DepCombinator>::Body, <Right as DepCombinator>::Body>

The type of the body combinator produced by apply.