Struct Frame

pub struct Frame {
    pub stype: StatementType,
    pub valid: GlobalRange,
    pub label_atom: Atom,
    pub const_pool: Box<[u8]>,
    pub hypotheses: Box<[Hyp]>,
    pub target: VerifyExpr,
    pub stub_expr: Box<[u8]>,
    pub var_list: Box<[Atom]>,
    pub mandatory_count: usize,
    pub mandatory_dv: Box<[(VarIndex, VarIndex)]>,
    pub optional_dv: Box<[Bitset]>,
}

Frames represent the logical content of the database, and are the main work product of the scope check pass.

Every $a and $p statement in the database is associated with a “frame” and an “extended frame” as defined in the Metamath spec. The frame consists of the math string of the statement, the strings of all hypotheses, and any disjoint variable hypotheses which are required to hold when using the statement in a later proof; the extended frame additionally contains types and disjointness conditions for variables that may be used in the proof, but are not mentioned in the hypotheses and thus need not be respected by users.

In the spec, the extended frame includes all $f statements which are in scope. We do not actually track optional $f statements directly in the frame; instead, when you encounter a use of a $f statement in a proof, you need to look it up and check the valid range to see if it can be used in the current proof. $f statements are tracked using the same Frame data type, although they do not strictly speaking have associated frames.

Since the primary user of frames currently is the verifier, the format is heavily tuned for what the verifier requires. From the verifier’s perspective, the main use of a frame is to match the top several entries in a proof stack and perform substitutions; the frame may be considered a kind of program, and optimizations are taken for the execution of steps.

Support for non-verifier users of frame data is expected to be quite weak at the present time.

Variable names are replaced with small integers so that the substitution being built can be maintained as an array.

Fields

stype: StatementType

Type of this statement, will be StatementType::Axiom, StatementType::Floating, or StatementType::Provable.

valid: GlobalRange

Valid range of this statement.

Use this to ensure that $f pseudo-frames are used only where they are in scope, and that $a $p frames are not used before they are defined.

label_atom: Atom

Atom representation of this statement’s label (valid only if incremental).

const_pool: Box<[u8]>

Backing array for all literal fragments in the hypotheses and target expression.

hypotheses: Box<[Hyp]>

Ordered list of hypotheses required by this frame.

The last entry corresponds to the top of the stack at application time. If you process hypotheses in the order of this list, then you will never need to subsitute a variable before it has been set; this is a consequence of Metamath rules requiring $f to be in scope for an $e to be valid.

target: VerifyExpr

Expression which is subsituted and pushed on the stack after validating hypotheses.

stub_expr: Box<[u8]>

Compressed representation of the variable name, used only for $f pseudo-frames.

var_list: Box<[Atom]>

Mapping from variable indices to the variable names.

mandatory_count: usize

Length of the prefix of var_list representing mandatory variables; the number of slots in the subsitution for this frame.

mandatory_dv: Box<[(VarIndex, VarIndex)]>

List of pairs of variables in simple mandatory disjoint variable constraints for this frame.

optional_dv: Box<[Bitset]>

Two-dimensional bit array of pairs of variables which can be treated as disjoint in proofs of this frame.

Implementations

impl Frame

pub const fn as_ref<'a>(&'a self, db: &'a Database) -> FrameRef<'a>

Augment a frame with a database reference, to produce a FrameRef.

pub fn mandatory_vars(&self) -> &[Atom]

The list of mandatory variables in the frame.

pub fn mandatory_hyps(&self) -> &[Hyp]

The list of mandatory hypotheses in the frame. Every Hyp in this list will be Hyp::Floating.

impl Frame

pub fn floating(&self) -> impl Iterator<Item = StatementAddress> + '_

Iterates over the floating hypotheses for this frame.

Trait Implementations

impl Clone for Frame

fn clone(&self) -> Frame

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Frame

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

Formats the value using the given formatter.

impl Default for Frame

fn default() -> Frame

Returns the “default value” for a type.