ShotTx.Prover.Branch (ShotTx v0.0.1)

Copy Markdown View Source

Pure functional core representing a single branch in the proof tree. Applies rules and returns the resulting state and any intended side-effects (Outbox pattern) for the stateful Worker to execute.

History format

Each history entry is a triple {source | nil, rule, [produced_id]}:

  • source — term id of the formula that was processed. Reinserted gamma /
             prim_subst rules carry the originating formula's id through the
         queue, so every entry is tagged with a real parent.
  • rule — the classified rule tuple from Rules.
  • produced — term ids of the formulas that this rule spawned onto the
             branch. For beta / `instantiate`, the produced list mirrors the
         sibling branches.

History is recorded inside apply_rule/6 after the rule runs, so the produced list is exact and {:closed, branch} carries a branch whose history includes the closing step.

Equality handling

Every formula added to the branch is run through ingest_formula/3. This preserves the existing decomposition of equality via the :equality_expansion rule (Leibniz / extensional / o-type iff) and additionally:

  • If the formula is an equation s = t, it is recorded in branch.equations and every existing literal is paramodulated against the new equation, with the variants pushed onto the queue.
  • When a new literal lands on the branch via the :atomic rule, it is paramodulated against all currently known equations.

The :instantiate rule additionally performs dual instantiation: the source literal is treated as an atom on the branch in addition to the lazily-instantiated variants being branched on.

Summary

Types

effect()
history_entry()
step_result()
t()

Functions

new(id, formulas, params, opts \\ [])

Constructs a new root branch or an explicitly defined child branch.

splice_suggested_instantiate(branch, recipe, term, source, params)

Splices a synthetic {:suggested_instantiate, recipe, term} rule onto the branch's priority queue. Called by Worker when it consumes a suggestion from the :suggestions ETS table — the rule enters the ordinary popping loop and fires via the dedicated apply_rule/6 clause, which adds app(recipe, term) to the branch without spawning a child.

step(branch, params, gamma_limit, prim_limit)

Pops the next formula/rule from the queue and applies it. Returns a tuple instructing the Worker on how to proceed. History is recorded inside apply_rule/6.

wake_up(branch, cost_fn)

Wakes up a sleeping branch by reinserting its sleeping gamma rules into the queue.

Types

effect()

@type effect() ::
  :no_effects
  | {:notify_ca, MapSet.t()}
  | {:record_provenance,
     [{ShotDs.Data.Term.term_id(), ShotTx.Prover.Provenance.t()}]}

history_entry()

@type history_entry() ::
  {ShotDs.Data.Term.term_id() | nil, ShotTx.Prover.Rules.rule_t(),
   [ShotDs.Data.Term.term_id()]}

step_result()

@type step_result() ::
  {:continue,
   %ShotTx.Prover.Branch{
     defs: term(),
     equations: term(),
     frontier: term(),
     frontier_version: term(),
     ground_terms: term(),
     history: term(),
     id: term(),
     last_clash: term(),
     literals: term(),
     pending_closure: term(),
     processed_rules: term(),
     queue: term(),
     sleeping_gamma_rules: term(),
     term_ids: term(),
     type_universe: term()
   }, effect()}
  | {:split,
     my_branch :: %ShotTx.Prover.Branch{
       defs: term(),
       equations: term(),
       frontier: term(),
       frontier_version: term(),
       ground_terms: term(),
       history: term(),
       id: term(),
       last_clash: term(),
       literals: term(),
       pending_closure: term(),
       processed_rules: term(),
       queue: term(),
       sleeping_gamma_rules: term(),
       term_ids: term(),
       type_universe: term()
     },
     sibling :: %ShotTx.Prover.Branch{
       defs: term(),
       equations: term(),
       frontier: term(),
       frontier_version: term(),
       ground_terms: term(),
       history: term(),
       id: term(),
       last_clash: term(),
       literals: term(),
       pending_closure: term(),
       processed_rules: term(),
       queue: term(),
       sleeping_gamma_rules: term(),
       term_ids: term(),
       type_universe: term()
     }}
  | {:instantiate,
     branches :: [
       %ShotTx.Prover.Branch{
         defs: term(),
         equations: term(),
         frontier: term(),
         frontier_version: term(),
         ground_terms: term(),
         history: term(),
         id: term(),
         last_clash: term(),
         literals: term(),
         pending_closure: term(),
         processed_rules: term(),
         queue: term(),
         sleeping_gamma_rules: term(),
         term_ids: term(),
         type_universe: term()
       }
     ]}
  | {:idle,
     %ShotTx.Prover.Branch{
       defs: term(),
       equations: term(),
       frontier: term(),
       frontier_version: term(),
       ground_terms: term(),
       history: term(),
       id: term(),
       last_clash: term(),
       literals: term(),
       pending_closure: term(),
       processed_rules: term(),
       queue: term(),
       sleeping_gamma_rules: term(),
       term_ids: term(),
       type_universe: term()
     }}
  | {:saturated, {defs :: map(), literals :: MapSet.t()}}
  | {:closed,
     %ShotTx.Prover.Branch{
       defs: term(),
       equations: term(),
       frontier: term(),
       frontier_version: term(),
       ground_terms: term(),
       history: term(),
       id: term(),
       last_clash: term(),
       literals: term(),
       pending_closure: term(),
       processed_rules: term(),
       queue: term(),
       sleeping_gamma_rules: term(),
       term_ids: term(),
       type_universe: term()
     }}

t()

@type t() :: %ShotTx.Prover.Branch{
  defs: term(),
  equations: term(),
  frontier: term(),
  frontier_version: term(),
  ground_terms: term(),
  history: term(),
  id: term(),
  last_clash: term(),
  literals: term(),
  pending_closure: term(),
  processed_rules: term(),
  queue: term(),
  sleeping_gamma_rules: term(),
  term_ids: term(),
  type_universe: term()
}

Functions

new(id, formulas, params, opts \\ [])

@spec new(
  String.t(),
  [ShotDs.Data.Term.term_id()],
  ShotTx.Data.Parameters.t(),
  keyword()
) ::
  %ShotTx.Prover.Branch{
    defs: term(),
    equations: term(),
    frontier: term(),
    frontier_version: term(),
    ground_terms: term(),
    history: term(),
    id: term(),
    last_clash: term(),
    literals: term(),
    pending_closure: term(),
    processed_rules: term(),
    queue: term(),
    sleeping_gamma_rules: term(),
    term_ids: term(),
    type_universe: term()
  }

Constructs a new root branch or an explicitly defined child branch.

splice_suggested_instantiate(branch, recipe, term, source, params)

@spec splice_suggested_instantiate(
  t(),
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Term.term_id(),
  ShotDs.Data.Term.term_id() | nil,
  ShotTx.Data.Parameters.t()
) :: t()

Splices a synthetic {:suggested_instantiate, recipe, term} rule onto the branch's priority queue. Called by Worker when it consumes a suggestion from the :suggestions ETS table — the rule enters the ordinary popping loop and fires via the dedicated apply_rule/6 clause, which adds app(recipe, term) to the branch without spawning a child.

step(branch, params, gamma_limit, prim_limit)

@spec step(
  %ShotTx.Prover.Branch{
    defs: term(),
    equations: term(),
    frontier: term(),
    frontier_version: term(),
    ground_terms: term(),
    history: term(),
    id: term(),
    last_clash: term(),
    literals: term(),
    pending_closure: term(),
    processed_rules: term(),
    queue: term(),
    sleeping_gamma_rules: term(),
    term_ids: term(),
    type_universe: term()
  },
  ShotTx.Data.Parameters.t(),
  non_neg_integer(),
  non_neg_integer()
) :: step_result()

Pops the next formula/rule from the queue and applies it. Returns a tuple instructing the Worker on how to proceed. History is recorded inside apply_rule/6.

wake_up(branch, cost_fn)

@spec wake_up(
  %ShotTx.Prover.Branch{
    defs: term(),
    equations: term(),
    frontier: term(),
    frontier_version: term(),
    ground_terms: term(),
    history: term(),
    id: term(),
    last_clash: term(),
    literals: term(),
    pending_closure: term(),
    processed_rules: term(),
    queue: term(),
    sleeping_gamma_rules: term(),
    term_ids: term(),
    type_universe: term()
  },
  (ShotTx.Prover.Rules.rule_t() -> non_neg_integer())
) :: %ShotTx.Prover.Branch{
  defs: term(),
  equations: term(),
  frontier: term(),
  frontier_version: term(),
  ground_terms: term(),
  history: term(),
  id: term(),
  last_clash: term(),
  literals: term(),
  pending_closure: term(),
  processed_rules: term(),
  queue: term(),
  sleeping_gamma_rules: term(),
  term_ids: term(),
  type_universe: term()
}

Wakes up a sleeping branch by reinserting its sleeping gamma rules into the queue.