Enum mm0b_parser::UnifyCmd

pub enum UnifyCmd {
    Term {
        tid: TermId,
        save: bool,
    },
    Ref(u32),
    Dummy(SortId),
    Hyp,
}

Unify commands appear in the header data for a def or axiom/theorem. They are executed by the ProofCmd::Thm command in order to perform substitutions. The state of the unify stack machine is:

• MS: Stack<StackEl>: The main stack, called S in the ProofCmd documentation. Since a unification is called as a subroutine during a proof command, the main stack is available, but most operations don’t use it.
• S: Stack<Expr>: The unify stack, which contains expressions from the target context that are being destructured.
• H: Vec<Expr>: The unify heap, also known as the substitution. This is initialized with the expressions that the target context would like to substitute for the variable names in the theorem being applied, but it can be extended in order to support substitutions with sharing as well as dummy variables.

Variants

Term

UTerm t: S, (t e1 ... en) --> S, en, ..., e1
USave: H; S, e --> H, e; S, e
UTermSave t = USave; UTerm t:
  H; S, (t e1 ... en) --> H, (t e1 ... en); S, en, ..., e1

Pop an element from the stack, ensure that the head is t, then push the n arguments to the term (in reverse order, so that they are dealt with in the correct order in the command stream). UTermSave does the same thing but saves the term to the unify heap before the destructuring.

Fields of Term

tid: TermId

The term that should be at the head

save: bool

True if we want to recall this substitution for later

Ref(u32)

URef i: H; S, Hi --> H; S

Get the i-th element from the unify heap (the substitution), and match it against the head of the unify stack.

Tuple Fields of Ref

0: u32

Dummy(SortId)

UDummy s: H; S, x --> H, x; S   (where x:s)

Pop a variable from the unify stack (ensure that it is a name of the appropriate sort) and push it to the heap (ensure that it is distinct from everything else in the substitution).

Tuple Fields of Dummy

0: SortId

Hyp

UHyp (UThm mode):  MS, |- e; S --> MS; S, e
UHyp (UThmEnd mode):  HS, e; S --> HS; S, e

UHyp is a command that is used in theorem declarations to indicate that we are about to read a hypothesis. There are two contexts where we read this, when we are first declaring the theorem and check the statement (UThmEnd mode), and later when we are applying the theorem and have to apply a substitution (UThm mode). When we are applying the theorem, we have |- e on the main stack, and we pop that and load the expression onto the unify stack. When we are checking a theorem, we have been pushing hypotheses onto the hypothesis stack, so we pop it from there instead.

Implementations

impl UnifyCmd

pub fn write_to(self, w: &mut impl Write) -> Result<()>

Serialize a UnifyCmd to the given writer. Uses the UNIFY_* commands in mmb::export::cmd.

Trait Implementations

impl Clone for UnifyCmd

fn clone(&self) -> UnifyCmd

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for UnifyCmd

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

Formats the value using the given formatter.

impl TryFrom<(u8, u32)> for UnifyCmd

type Error = ParseError

The type returned in the event of a conversion error.

fn try_from((cmd, data): (u8, u32)) -> Result<Self, Self::Error>

Performs the conversion.

impl Copy for UnifyCmd