Inspecting proof-carrying capabilities and backend plans

Capability inspection reads the instances used by execution. It reports which universal operations exist, the candidate selected by each capability, and the planner decisions behind that selection. The selected candidate comes from the capability; diagnostic assessments rerun the shared selector on that capability's candidate estimates and policy.

def FloatLib.Floats.ExecFloat.Inspection.conversions (valueType : Lean.Expr) : Lean.MetaM (List InfoEntry)

Inspect the explicit conversion capabilities installed for one user-facing value type.

Source decoding, destination quantization, and a default context are inspected independently. A source-only family can supply operands to casts or mixed arithmetic; a destination without a default context requires an explicit context.

def FloatLib.Floats.ExecFloat.Inspection.withConversions (profile : FormatProfile) (valueType : Lean.Expr) : Lean.MetaM FormatProfile

Attach synthesized conversion capabilities to a family-authored format profile.

def FloatLib.Floats.ExecFloat.Inspection.execFamily? (valueType : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Recover the configured family encoded by an ExecFloat value type.

The check recognizes a Subtype predicate of the form fun _ => ExecFloatTag family. It recovers the tag without checking that the underlying carrier is the code type of family.

def FloatLib.Floats.ExecFloat.Inspection.execFamilyApplication? (familyName : Lean.Name) (arity : ℕ) (valueType : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Array Lean.Expr))

Recover an ExecFloat family only when it is an application of the expected declaration and arity. The returned argument array is safe to index below arity.

def FloatLib.Floats.ExecFloat.Inspection.hasCapability (className : Lean.Name) (family : Lean.Expr) : Lean.MetaM Bool

Synthesize the actual encoded-format, policy, and arithmetic capability dictionaries.

The result is proof-backed availability, not a declaration-name or storage-width heuristic.

def FloatLib.Floats.ExecFloat.Inspection.coreOperations (family : Lean.Expr) : Lean.MetaM CoreOperationCoverage

Inspect all six universal operation capabilities for one exact configured family.

def FloatLib.Floats.ExecFloat.Inspection.reduceProjection (fieldName : Lean.Name) (object : Lean.Expr) : Lean.MetaM Lean.Expr

Reduce one projection from a closed expression.

Format-specific #float_info elaborators use this helper to inspect embedded descriptors without duplicating projection construction or transparency policy.

def FloatLib.Floats.ExecFloat.Inspection.readFlagProjection (description : String) (fieldName trueConstructor falseConstructor : Lean.Name) (object : Lean.Expr) : Lean.MetaM Bool

Read a closed two-constructor projection as a Boolean report field.

The caller supplies the constructors that mean true and false; inspection compares declaration identities directly and never relies on printed names or constructor order.

def FloatLib.Floats.ExecFloat.Inspection.readNat (description : String) (value : Lean.Expr) : Lean.MetaM ℕ

Read a closed natural-number expression after reduction.

Family-specific #float_info elaborators use this helper for static widths, radix bases, and scale parameters. Keeping the reduction and diagnostic policy here prevents each representation family from maintaining a slightly different copy.

def FloatLib.Floats.ExecFloat.Inspection.readNatProjection (description : String) (fieldName : Lean.Name) (object : Lean.Expr) : Lean.MetaM ℕ

Read a natural-number-valued projection from a closed expression.

The description identifies the embedded descriptor or plan in diagnostics, while the projection name identifies the exact field that failed to reduce.

def FloatLib.Floats.ExecFloat.Inspection.readString (description : String) (value : Lean.Expr) : Lean.MetaM String

Evaluate one closed string expression.

def FloatLib.Floats.ExecFloat.Inspection.selectedBackends (family : Lean.Expr) : Lean.MetaM (List InfoEntry)

Inspect selected backends and all alternatives for every synthesized universal capability.

Families append these entries to their own representation- and semantics-specific execution profile. This keeps selection reporting uniform without imposing a common numerical model.