Generates general bindings for primitive substitution.
A general binding for a quantified variable of type $\alpha_1\to\cdots\to\alpha_n\to o$ fixes a logical head symbol $Q$ while leaving the sub-formula positions as fresh free variables (holes):
$$ \lambda y_1^{\alpha_1}\cdots y_n^{\alpha_n}.\; Q\bigl(H_1\;\overline{y},\;\ldots,\;H_m\;\overline{y}\bigr) $$
Generation is split into two independent phases so that an incrementally growing type universe can be accommodated without replaying earlier work:
Base heads — propositional connectives ($\top$, $\bot$, $\lnot$, $\land$, $\lor$, $\supset$, $\equiv$) and, at depth $\geq 2$, propositional compositions. Stable across the proof.
Polymorphic heads — $=_\tau$, $\forall_\beta$, $\exists_\beta$ for each type in the universe. At depth $\geq 2$, additionally includes compositions of polymorphic heads with propositional connectives ($\lnot(=_\tau)$, $(\forall_\beta)\land H$, etc.). Depth-dependent, requiring per-depth coverage tracking.
Head specifications are lightweight {matrix_fn, hole_types} tuples;
the expensive term construction happens only in build_binding/2.
Summary
Types
A head specification pairs a matrix builder with the types of its holes.
Functions
Returns the base (propositional) head specifications for bindings over the
given arg_types at the given depth. Independent of the type universe.
Constructs a binding term from argument types and a head specification.
Returns {binding, h_terms} where h_terms are the fresh $H$ hole
variables minted for this binding — callers need them to record
provenance so a later unifier can be traced back to this rule.
Returns polymorphic head specifications over the given set of types at the
given depth. Equality heads come first; quantifier heads come last so they
are tried much later in proof search.
Returns unit-set head specifications: for each constant c of type $\tau$,
produces $\lambda\overline{y}.\;(H\;\overline{y}) =_\tau c$ with a single
hole $H : \overline{\alpha} \to \tau$.
Types
@type head_spec() :: {([ShotDs.Data.Term.term_id()] -> ShotDs.Data.Term.term_id()), [ShotDs.Data.Type.t()]}
A head specification pairs a matrix builder with the types of its holes.
The builder receives the applied hole terms ($H_i\;\overline{y}$, each of the appropriate result type) and returns the matrix term ID.
Functions
@spec base_heads([ShotDs.Data.Type.t()], pos_integer()) :: [head_spec()]
Returns the base (propositional) head specifications for bindings over the
given arg_types at the given depth. Independent of the type universe.
@spec build_binding([ShotDs.Data.Type.t()], head_spec()) :: {ShotDs.Data.Term.term_id(), [ShotDs.Data.Term.term_id()]}
Constructs a binding term from argument types and a head specification.
Returns {binding, h_terms} where h_terms are the fresh $H$ hole
variables minted for this binding — callers need them to record
provenance so a later unifier can be traced back to this rule.
The $H$ holes are minted outside the scratchpad because they must survive as global term ids for provenance lookup. The scratchpad's job is limited to GCing the temporary $y$ binder terms once the abstraction has folded them into de Bruijn indices.
@spec polymorphic_heads( [ShotDs.Data.Type.t()], pos_integer(), Enumerable.t(ShotDs.Data.Type.t()) ) :: [ head_spec() ]
Returns polymorphic head specifications over the given set of types at the
given depth. Equality heads come first; quantifier heads come last so they
are tried much later in proof search.
@spec unit_set_heads( [ShotDs.Data.Type.t()], Enumerable.t(ShotDs.Data.Declaration.const_t()) ) :: [ head_spec() ]
Returns unit-set head specifications: for each constant c of type $\tau$,
produces $\lambda\overline{y}.\;(H\;\overline{y}) =_\tau c$ with a single
hole $H : \overline{\alpha} \to \tau$.