Lax58.CertifiedDerivationElab
Certified encoding derivation (elaboration infrastructure)
concepts/Lax58/CertifiedDerivationElab.lean · lax-58
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Elaboration infrastructure
This module implements ; it is tooling, not a mathematical definition of advice-freedom. The mathematical vocabulary is in and . The small agreement record and its field operations are in .
The command inspects the actual constructors and generates an encoder, its complete , and its checked witness together. Field resolution is closed: Nat, Fin, proof-erased subtypes, finite families, direct recursive children, and earlier successful constructor derivations only. Unsupported fields fail, and a failed command rolls back its declarations.
The private registry records successful command outputs; it never consumes arbitrary agreement values or instances. The generator establishes correspondence with the source declaration, while Lean's kernel checks the expanded equations and proofs. Importing this tooling does not make arbitrary encoders certified.
Lax currently classifies every non-root concept-package module as a concept. The infrastructure label makes this packaging constraint explicit; it does not hide the implementation or introduce a new archive module category.
Lean source view on GitHub
| 1 | import Lean |
| 2 | import Lax58.CertifiedDerivation |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Certified encoding derivation (elaboration infrastructure) |
| 7 | type: elaboration infrastructure |
| 8 | --- |
| 9 | |
| 10 | This module implements `derive_certified_encoding`; it is tooling, not a |
| 11 | mathematical definition of advice-freedom. The mathematical vocabulary is in |
| 12 | `StructuralPresentation` and `StructuralCombinators`. The small agreement |
| 13 | record and its field operations are in `CertifiedDerivation`. |
| 14 | |
| 15 | The command inspects the actual constructors and generates an encoder, its |
| 16 | complete `.Laws`, and its checked `.certified` witness together. Field |
| 17 | resolution is closed: Nat, Fin, proof-erased subtypes, finite families, direct |
| 18 | recursive children, and earlier successful constructor derivations only. |
| 19 | Unsupported fields fail, and a failed command rolls back its declarations. |
| 20 | |
| 21 | The private registry records successful command outputs; it never consumes |
| 22 | arbitrary agreement values or `FieldEncoding` instances. The generator |
| 23 | establishes correspondence with the source declaration, while Lean's kernel |
| 24 | checks the expanded equations and proofs. Importing this tooling does not |
| 25 | make arbitrary encoders certified. |
| 26 | |
| 27 | Lax currently classifies every non-root concept-package module as a concept. |
| 28 | The infrastructure label makes this packaging constraint explicit; it does |
| 29 | not hide the implementation or introduce a new archive module category. |
| 30 | -/ |
| 31 | |
| 32 | namespace Lax58.CertifiedDerivationElab |
| 33 | |
| 34 | open Lax58.StructuralPresentation Lax58.StructuralCombinators |
| 35 | open Lax58.CertifiedDerivation |
| 36 | |
| 37 | open Lean Meta Elab Term Command |
| 38 | open Lean.Parser.Term |
| 39 | |
| 40 | private initialize certifiedEncoders : SimplePersistentEnvExtension Name (Array Name) ← |
| 41 | registerSimplePersistentEnvExtension { |
| 42 | addEntryFn := Array.push |
| 43 | addImportedFn := fun entries => entries.foldl (· ++ ·) #[] } |
| 44 | |
| 45 | /-- Resolve only fixed primitives or a witness generated by this module's |
| 46 | command. In particular, neither `FieldEncoding` nor user instances are read. -/ |
| 47 | private partial def certifiedField (type : Expr) : TermElabM Expr := do |
| 48 | let type ← whnf type |
| 49 | if type.isConstOf ``Nat then |
| 50 | return mkConst ``CertifiedFieldEncoding.nat |
| 51 | if type.isAppOfArity ``Fin 1 then |
| 52 | return ← mkAppM ``CertifiedFieldEncoding.fin #[type.appArg!] |
| 53 | if type.isAppOfArity ``Subtype 2 then |
| 54 | let args := type.getAppArgs |
| 55 | let base ← certifiedField args[0]! |
| 56 | return ← mkAppM ``CertifiedFieldEncoding.subtype #[base, args[1]!] |
| 57 | if let .forallE name domain body bi := type then |
| 58 | let domain ← whnf domain |
| 59 | if domain.isAppOfArity ``Fin 1 then |
| 60 | return ← withLocalDecl name bi domain fun i => do |
| 61 | let item ← certifiedField (body.instantiate1 i) |
| 62 | mkAppM ``CertifiedFieldEncoding.family #[← mkLambdaFVars #[i] item] |
| 63 | for name in certifiedEncoders.getState (← getEnv) do |
| 64 | let saved ← saveState |
| 65 | let candidate ← mkConstWithFreshMVarLevels name |
| 66 | let (args, _, result) ← forallMetaTelescopeReducing (← inferType candidate) |
| 67 | if result.isAppOfArity ``CertifiedFieldEncoding 3 && |
| 68 | (← isDefEq result.getAppArgs[0]! type) then |
| 69 | let candidate ← instantiateMVars (mkAppN candidate args) |
| 70 | if !candidate.hasExprMVar then |
| 71 | return candidate |
| 72 | saved.restore |
| 73 | throwError "unsupported certified field type {type}; expected Nat, Fin, a proof-erased subtype, a finite family, or an earlier constructor-certified datatype" |
| 74 | |
| 75 | /-- Read-only access to the closed field resolver for other elaborators. |
| 76 | This does not register encoders or consume caller-supplied agreement values. -/ |
| 77 | def resolveCertifiedField (type : Expr) : TermElabM Expr := |
| 78 | certifiedField type |
| 79 | |
| 80 | private def recursiveType (indName : Name) (type : Expr) : TermElabM Bool := do |
| 81 | return (← whnf type).getAppFn.constName? == some indName |
| 82 | |
| 83 | private def explicitBinders : Expr → Expr |
| 84 | | .lam name type body _ => .lam name type (explicitBinders body) .default |
| 85 | | body => body |
| 86 | |
| 87 | private def certifiedAlternative (indInfo : InductiveVal) (levels : List Level) |
| 88 | (params : Array Expr) |
| 89 | (recursiveCall : TSyntax `term) (constructorName : Name) : |
| 90 | TermElabM (TSyntax ``matchAlt) := do |
| 91 | let constructor ← getConstInfoCtor constructorName |
| 92 | let ctorType ← inferType (mkAppN (mkConst constructorName levels) params) |
| 93 | forallTelescopeReducing ctorType fun arguments result => do |
| 94 | let mut lctx ← getLCtx |
| 95 | for argument in arguments do |
| 96 | let decl ← argument.fvarId!.getDecl |
| 97 | lctx := lctx.setUserName argument.fvarId! (← mkFreshUserName decl.userName) |
| 98 | withLCtx lctx (← getLocalInstances) do |
| 99 | let mut patterns : Array (TSyntax `term) := #[] |
| 100 | for _ in params do patterns := patterns.push (← `(_)) |
| 101 | let mut fields : Array (Ident × Expr × BinderInfo) := #[] |
| 102 | for argument in arguments do |
| 103 | let decl ← argument.fvarId!.getDecl |
| 104 | let name := mkIdent decl.userName |
| 105 | patterns := patterns.push name |
| 106 | fields := fields.push (name, decl.type, decl.binderInfo) |
| 107 | -- An actually empty field eliminates its whole constructor. This handles |
| 108 | -- function-free first-order languages without accepting a user IsEmpty. |
| 109 | for (name, type, _) in fields do |
| 110 | let type ← whnf type |
| 111 | if let .const emptyName _ := type.getAppFn then |
| 112 | if let .inductInfo emptyInfo ← getConstInfo emptyName then |
| 113 | if emptyInfo.ctors.isEmpty then |
| 114 | return ← `(matchAltExpr| |
| 115 | | @$(mkIdent constructor.name):ident $patterns:term* => nomatch $name:ident) |
| 116 | let mut encoded : TSyntax `term ← `([]) |
| 117 | for (name, type, bi) in fields.reverse do |
| 118 | if ← isProp type then continue |
| 119 | -- Implicit fields must still pass validation. Only intrinsic indices |
| 120 | -- (Nat/Fin in the present supported syntax) are erased. |
| 121 | if !bi.isExplicit then |
| 122 | let normalized ← whnf type |
| 123 | unless normalized.isConstOf ``Nat || normalized.isAppOfArity ``Fin 1 do |
| 124 | throwError "{constructorName}: unsupported implicit field {name}: {type}" |
| 125 | let some decl := lctx.findFromUserName? name.getId |
| 126 | | throwError "missing constructor field {name}" |
| 127 | unless result.containsFVar decl.fvarId || |
| 128 | fields.any (fun (_, ty, _) => ty.containsFVar decl.fvarId) do |
| 129 | throwError "{constructorName}: implicit field {name} is not an intrinsic index" |
| 130 | continue |
| 131 | if ← recursiveType indInfo.name type then |
| 132 | encoded ← `(($recursiveCall) $name:ident :: $encoded) |
| 133 | else |
| 134 | let type ← whnf type |
| 135 | if let .forallE _ domain body _ := type then |
| 136 | if (← whnf domain).isAppOfArity ``Fin 1 && |
| 137 | (← recursiveType indInfo.name body) then |
| 138 | encoded ← `(List.ofFn (fun i => ($recursiveCall) ($name:ident i)) ++ $encoded) |
| 139 | continue |
| 140 | let witness ← try certifiedField type catch ex => |
| 141 | throwError "{constructorName}, field {name}: {ex.toMessageData}" |
| 142 | -- Embed the checked expression itself, abstracting constructor locals |
| 143 | -- before leaving their telescope. Pretty-printer round trips would |
| 144 | -- let downstream delaborators change the selected witness. |
| 145 | let witnessFunction ← exprToSyntax (explicitBinders (← mkLambdaFVars arguments witness)) |
| 146 | let fieldNames : Array (TSyntax `term) := fields.map fun (id, _, _) => ⟨id.raw⟩ |
| 147 | encoded ← `((CertifiedFieldEncoding.toRaw |
| 148 | ($witnessFunction $fieldNames*) $name:ident) :: $encoded) |
| 149 | let tag := constructor.name.eraseMacroScopes.getString! |
| 150 | `(matchAltExpr| | @$(mkIdent constructor.name):ident $patterns:term* => |
| 151 | Raw.constructor $(quote tag) $encoded) |
| 152 | |
| 153 | private def alternativesFor (type : Expr) (recursiveCall : TSyntax `term) : |
| 154 | TermElabM (Array (TSyntax ``matchAlt)) := do |
| 155 | let type ← whnf type |
| 156 | let some name := type.getAppFn.constName? |
| 157 | | throwError "certified derivation expects an inductive datatype, got {type}" |
| 158 | let info ← getConstInfoInduct name |
| 159 | unless info.all.length == 1 do |
| 160 | throwError "certified derivation does not support mutual inductives: {name}" |
| 161 | let params := type.getAppArgs.extract 0 info.numParams |
| 162 | return (← info.ctors.mapM |
| 163 | (certifiedAlternative info type.getAppFn.constLevels! params recursiveCall)).toArray |
| 164 | |
| 165 | elab "certifiedFun% " "using " recursiveCall:term : term <= expectedType => do |
| 166 | let .forallE _ domain _ _ ← whnf expectedType |
| 167 | | throwError "expected an encoder function type" |
| 168 | let alts ← alternativesFor domain recursiveCall |
| 169 | elabTerm (← `(fun $alts:matchAlt*)) (some expectedType) |
| 170 | |
| 171 | elab "certifiedMatch% " value:term " using " recursiveCall:term : term => do |
| 172 | let expr ← elabTerm value none |
| 173 | let alts ← alternativesFor (← inferType expr) recursiveCall |
| 174 | elabTerm (← `(match $value:term with $alts:matchAlt*)) (some (mkConst ``Raw)) |
| 175 | |
| 176 | /-- Generate the encoder, `.Laws`, and `.certified`. Ordinary binders are |
| 177 | fixed parameters; binders following `indexed` are intrinsic indices that |
| 178 | recursive constructors may change. All generated names belong to the encoder. |
| 179 | -/ |
| 180 | syntax (name := deriveCertifiedEncoding) |
| 181 | (docComment)? "derive_certified_encoding " ident bracketedBinder* " indexed " bracketedBinder* |
| 182 | " : " term : command |
| 183 | |
| 184 | elab_rules : command |
| 185 | | `($[$doc:docComment]? derive_certified_encoding $name:ident $params:bracketedBinder* |
| 186 | indexed $indices:bracketedBinder* : $type:term) => do |
| 187 | let mut paramNames : Array (TSyntax `term) := #[] |
| 188 | for param in params do |
| 189 | unless param.raw.getKind == ``Lean.Parser.Term.explicitBinder do |
| 190 | throwError "fixed parameters must use explicit typed binders" |
| 191 | for id in param.raw[1].getArgs do |
| 192 | unless id.isIdent do throwError "expected named fixed parameter" |
| 193 | paramNames := paramNames.push ⟨id⟩ |
| 194 | let call ← `($name $paramNames*) |
| 195 | let lawsName := mkIdent (name.getId ++ `Laws) |
| 196 | let witnessName := mkIdent (name.getId ++ `certified) |
| 197 | let funIndices : TSyntaxArray ``funBinder := indices.map fun stx => ⟨stx.raw⟩ |
| 198 | let mut indexNames : Array (TSyntax `term) := #[] |
| 199 | for binder in indices do |
| 200 | for id in binder.raw[1].getArgs do |
| 201 | unless id.isIdent do throwError "expected named index" |
| 202 | indexNames := indexNames.push ⟨id⟩ |
| 203 | let savedEnv ← getEnv |
| 204 | try |
| 205 | elabCommand (← `($[$doc:docComment]? def $name $params* : ∀ $indices*, $type → Raw := |
| 206 | fun $funIndices* => certifiedFun% using $call)) |
| 207 | if (← get).messages.hasErrors then throwAbortCommand |
| 208 | elabCommand (← `(def $lawsName $params* $indices* : Prop := |
| 209 | ∀ value : $type, $call value = certifiedMatch% value using $call)) |
| 210 | if (← get).messages.hasErrors then throwAbortCommand |
| 211 | elabCommand (← `(def $witnessName $params* $indices* : |
| 212 | CertifiedFieldEncoding $type $call (@$lawsName $paramNames* $indexNames*) := |
| 213 | CertifiedFieldEncoding.ofLaws $call (by |
| 214 | intro value |
| 215 | cases value <;> rfl))) |
| 216 | if (← get).messages.hasErrors then throwAbortCommand |
| 217 | let fullName ← resolveGlobalConstNoOverload witnessName |
| 218 | modifyEnv fun env => certifiedEncoders.addEntry env fullName |
| 219 | catch ex => |
| 220 | setEnv savedEnv |
| 221 | throw ex |
| 222 | |
| 223 | end Lax58.CertifiedDerivationElab |
| 224 |
Builds on
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