ShotTx.Prover.Provenance (ShotTx v0.0.1)

Copy Markdown View Source

Per-fresh-variable annotation recording which quantifier minted the variable and on which branch. Consumed by ContradictionAgent and SuggestionAgent to turn unifier evidence back into instantiation hints.

Written at exactly two sites in ShotTx.Prover.Branch:

  • the γ fresh-var mint, and
  • every hole H produced by a general binding in the prim-subst enumerator.

Reads are performed by the agents. Workers never read this table.

Summary

Types

origin()
t()

Functions

fetch(table, fresh_var_id)

Fetches the provenance for fresh_var_id, or nil if unknown.

record(table, fresh_var_id, provenance)

Inserts provenance for fresh_var_id. Uses :ets.insert_new/2 so a redundant write (which would only happen under a bug — fresh vars are minted once) silently returns false rather than clobbering an earlier entry that another consumer may already have observed.

Types

origin()

@type origin() :: :gamma | :prim_subst

t()

@type t() :: %ShotTx.Prover.Provenance{
  birth_branch: String.t(),
  gamma_iteration: non_neg_integer(),
  origin: origin(),
  recipe: ShotDs.Data.Term.term_id(),
  source: ShotDs.Data.Term.term_id()
}

Functions

fetch(table, fresh_var_id)

@spec fetch(:ets.tab(), ShotDs.Data.Term.term_id()) :: t() | nil

Fetches the provenance for fresh_var_id, or nil if unknown.

record(table, fresh_var_id, provenance)

@spec record(:ets.tab(), ShotDs.Data.Term.term_id(), t()) :: boolean()

Inserts provenance for fresh_var_id. Uses :ets.insert_new/2 so a redundant write (which would only happen under a bug — fresh vars are minted once) silently returns false rather than clobbering an earlier entry that another consumer may already have observed.