Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax58.StructuralDerivation

Unrestricted structural folds (elaboration infrastructure)

concepts/Lax58/StructuralDerivation.lean · lax-58

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Elaboration infrastructure

    The `structural% value using recursiveCall` term derives the structural fold of an inductive value from its declaration. Constructor names and explicit constructor-field order are read from the declaration; direct recursive fields and finite families of recursive fields are folded recursively. Implicit indices and witnesses are erased. Only genuinely primitive explicit fields require an explicit FieldEncodingFieldEncoding.

    FieldEncodingFieldEncoding and the folds in this module are low-level elaboration infrastructure, not structurality certificates. Reduction equations using unrestricted field instances do not establish the provenance of those fields. Lax58.CertifiedDerivationElabLax58.CertifiedDerivationElab supplies the separate closed derivation path and does not consult this module's instances.

    Lean source view on GitHub

    1import Lean.Elab.Match
    2import Lax58.StructuralCombinators
    3
    4/-!
    5---
    6title: Unrestricted structural folds (elaboration infrastructure)
    7type: elaboration infrastructure
    8---
    9
    10The `structural% value using recursiveCall` term derives the structural fold
    11of an inductive value from its declaration. Constructor names and explicit
    12constructor-field order are read from the declaration; direct recursive fields
    13and finite families of recursive fields are folded recursively. Implicit
    14indices and witnesses are erased. Only genuinely primitive explicit fields
    15require an explicit `FieldEncoding`.
    16
    17`FieldEncoding` and the folds in this module are low-level elaboration
    18infrastructure, not structurality certificates. Reduction equations using
    19unrestricted field instances do not establish the provenance of those fields.
    20`Lax58.CertifiedDerivationElab` supplies the separate closed derivation path and
    21does not consult this module's instances.
    22-/
    23
    24namespace Lax58.StructuralDerivation
    25
    26open Lax58.StructuralPresentation
    27open Lax58.StructuralCombinators
    28
    29universe u
    30
    31/-- Low-level encoding of a non-recursive constructor field. Possessing an
    32instance alone confers no complexity-theoretic status. -/
    33class FieldEncoding (α : Type u) where
    34 toRaw : α → Raw
    35
    36/-- Apply the selected primitive-field encoding. -/
    37def fieldRaw {α : Type u} [P : FieldEncoding α] (x : α) : Raw :=
    38 P.toRaw x
    39
    40instance : FieldEncoding Nat where
    41 toRaw := Raw.nat
    42
    43instance {n : Nat} : FieldEncoding (Fin n) where
    44 toRaw i := Raw.nat i.val
    45
    46/-- Finite function fields are represented by their values in intrinsic
    47index order. This determines represented content but makes no claim about the
    48cost of evaluating the Lean function. -/
    49instance {n : Nat} {α : Type u} [P : FieldEncoding α] :
    50 FieldEncoding (Fin n → α) where
    51 toRaw f := Raw.fields (List.ofFn fun i => P.toRaw (f i))
    52
    53open Lean Meta Elab Term
    54open Lean.Parser.Term
    55
    56private def isDirectRecursiveField (inductiveName : Name) (type : Expr) : Bool :=
    57 type.getAppFn.constName? == some inductiveName
    58
    59private def isFiniteRecursiveFamily (inductiveName : Name) (type : Expr) : Bool :=
    60 match type with
    61 | .forallE _ domain body _ =>
    62 domain.getAppFn.constName? == some ``Fin &&
    63 body.getAppFn.constName? == some inductiveName
    64 | _ => false
    65
    66private def structuralAlternative (indInfo : InductiveVal)
    67 (recursiveCall : TSyntax `term) (constructorName : Name) :
    68 TermElabM (TSyntax ``matchAlt) := do
    69 let constructor ← getConstInfoCtor constructorName
    70 forallTelescopeReducing constructor.type fun arguments _ => do
    71 let mut patternArguments := #[]
    72 for _ in *...indInfo.numParams do
    73 patternArguments := patternArguments.push (← `(_))
    74 let mut fields : Array (Ident × Expr) := #[]
    75 for i in *...constructor.numFields do
    76 let argument := arguments[indInfo.numParams + i]!
    77 let declaration ← argument.fvarId!.getDecl
    78 if declaration.binderInfo.isExplicit then
    79 let fieldName := mkIdent (← mkFreshUserName `field)
    80 fields := fields.push (fieldName, declaration.type)
    81 patternArguments := patternArguments.push fieldName
    82 else
    83 -- Intrinsic indices and dependent witnesses are implicit constructor
    84 -- arguments. They remain available to dependent pattern matching, but
    85 -- do not duplicate data already fixed by the indexed value and its
    86 -- explicit fields. A downstream `Presentation.Lawful` proof remains
    87 -- responsible for showing that this erasure loses no value.
    88 patternArguments := patternArguments.push (← `(_))
    89 let mut encodedFields : TSyntax `term ← `([])
    90 for (fieldName, fieldType) in fields.reverse do
    91 encodedFields ←
    92 if isDirectRecursiveField indInfo.name fieldType then
    93 `(($recursiveCall:term) $fieldName:ident :: $encodedFields:term)
    94 else if isFiniteRecursiveFamily indInfo.name fieldType then
    95 `(List.ofFn (fun i => ($recursiveCall:term) ($fieldName:ident i)) ++
    96 $encodedFields:term)
    97 else
    98 `(Lax58.StructuralDerivation.fieldRaw $fieldName:ident ::
    99 $encodedFields:term)
    100 let tag := constructor.name.eraseMacroScopes.getString!
    101 let rightHandSide ←
    102 `(Lax58.StructuralCombinators.Raw.constructor $(quote tag)
    103 $encodedFields:term)
    104 `(matchAltExpr|
    105 | @$(mkIdent constructor.name):ident $patternArguments:term* =>
    106 $rightHandSide:term)
    107
    108/-- Derive one complete constructor-structural match. The caller supplies the
    109recursive function application so ordinary Lean termination checking remains
    110authoritative. -/
    111elab "structural% " value:term " using " recursiveCall:term : term => do
    112 let valueExpression ← elabTerm value none
    113 let valueType ← whnf (← inferType valueExpression)
    114 let some inductiveName := valueType.getAppFn.constName?
    115 | throwError "structural% expects an inductive value, got {valueType}"
    116 let indInfo ← getConstInfoInduct inductiveName
    117 let alternatives := (← indInfo.ctors.mapM
    118 (structuralAlternative indInfo recursiveCall)).toArray
    119 let generated ← `(match $value:term with $alternatives:matchAlt*)
    120 elabTerm generated (some (mkConst ``Raw))
    121
    122/-- Derive a complete constructor-structural function from its expected
    123single-argument function type. Unlike an inner `match`, the generated
    124constructor clauses remain visible to Lean's equation compiler, which is
    125needed for nested recursive fields such as `Fin n → Tree`.
    126
    127Example:
    128```
    129def treeRaw : Tree → Raw :=
    130 structuralFun% using treeRaw
    131```
    132-/
    133elab "structuralFun% " "using " recursiveCall:term : term <= expectedType => do
    134 let expectedType ← instantiateMVars expectedType
    135 let functionType ← whnf expectedType
    136 let .forallE _ valueType _resultType _ := functionType
    137 | throwError
    138 "structuralFun% expects a single-argument function type, got {expectedType}"
    139 let valueType ← whnf valueType
    140 let some inductiveName := valueType.getAppFn.constName?
    141 | throwError
    142 "structuralFun% expects an inductive argument type, got {valueType}"
    143 let indInfo ← getConstInfoInduct inductiveName
    144 let alternatives := (← indInfo.ctors.mapM
    145 (structuralAlternative indInfo recursiveCall)).toArray
    146 let generated ← `(fun $alternatives:matchAlt*)
    147 elabTerm generated (some expectedType)
    148
    149end Lax58.StructuralDerivation
    150

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…