2417ec667b
Some checks are pending
Lean Action CI / build (push) Waiting to run
Replaces ~900 lines of per-constructor reflect/reify boilerplate with
a generic Lean.Elab.Command macro that introspects each inductive's
ConstructorVal data via getConstInfoInduct + forallTelescopeReducing
and emits the per-arm code automatically.
Macro infrastructure (~750 lines under Macro namespace):
· classifyFieldType — type-shape dispatch (String / Nat / ULevel /
DimVar / DimExpr / FaceFormula / CType ℓ / CTerm / List X / Σ_ℓ
CType ℓ / Prod variants). Project-specific dispatch table; new
field types extend this once.
· collectFields — walks ctorVal.type via forallTelescopeReducing.
· mkReflectArm / mkReifyArmDoSeq — per-constructor arm builders.
· mkReflectFunBody / mkReifyFunBody — match-body assemblers.
· mkInductiveDefs — emits the partial-def pair.
· 4 specialized list helpers for the heterogeneous Σ-list shapes
(auto-discovered during the constructor-walking pass).
· derive_reflect_reify command + elabDeriveReflectReify elaborator.
Application (line 970):
derive_reflect_reify DimVar, DimExpr, FaceFormula, CType, CTerm,
CTypeArg, CtorSpec, CTypeSchema
Preserved as-is: file docstring, imports, Contract abbrev,
mathematical reifyULevel (special-cased), Contract registry +
register/lookupByName/allRegistered, the 4 round-trip theorems.
Engineering notes (full version in commit body / source comments):
· Hygiene: mkIdent for forward-reference function names, mkCIdent
only for closed-world Lean.* references.
· doMatch arm RHS must be doSeq, not term.
· Inner `match ← X with` requires enclosing do block.
· Level coherence on reify: tracks fvars of ULevel fields, matches
against subsequent CType fields' index expressions, emits
`if h : ℓ_rec = ℓ then h ▸ A else return none` accordingly.
Verification:
· Reflect.lean: 1544 → 1118 lines (-426).
· lake build (48 jobs) PASS.
· lake build CubicalTransport (43 jobs) PASS.
· lake exe cubical-test: 49/49 + 46/46 = 95/95 PASS.
· Round-trip smoke test (temp file, deleted post-verify): 26/26
inputs round-tripped successfully across DimVar, DimExpr,
FaceFormula, CType, CTerm — including leaf/single-arg/multi-arg/
implicit-ULevel/string-and-dim-var-payload cases.
· 4 sorries unchanged (the round-trip theorems on lines
1048/1059/1076/1116).
· Zero new sorry, zero noncomputable, zero Classical.propDecidable,
zero unsafe, zero Unhygienic.run.
Future inductive additions to Syntax.lean (e.g., next phase's
ModalityKind unification) get reflect/reify for free — just add the
type to the derive_reflect_reify list, no per-constructor cascade.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
42 lines
1.5 KiB
Text
42 lines
1.5 KiB
Text
import Lean
|
|
import CubicalTransport.Syntax
|
|
namespace CubicalTransport.Test.Reify
|
|
|
|
partial def reifyStrLit (e : Lean.Expr) : Lean.MetaM (Option String) := do
|
|
let e ← Lean.Meta.whnf e
|
|
match e with
|
|
| .lit (.strVal s) => return some s
|
|
| _ => return none
|
|
|
|
open Lean Elab Command Term Lean.Parser.Term
|
|
|
|
elab "myDeriveDimVar15" : command => do
|
|
let lExpr := mkCIdent ``Lean.Expr
|
|
let lMetaM := mkCIdent ``Lean.MetaM
|
|
let lOption := mkCIdent ``Option
|
|
let lDimVar := mkCIdent ``DimVar
|
|
let lWhnf := mkCIdent ``Lean.Meta.whnf
|
|
let lDimVarMk := mkCIdent ``DimVar.mk
|
|
let lReifyStrLit := mkCIdent `CubicalTransport.Test.Reify.reifyStrLit
|
|
let arm1Body : TSyntax ``Lean.Parser.Term.doSeq ←
|
|
`(doSeq| if h : args.size = 1 then
|
|
match ← ($lReifyStrLit (args[0]'(by omega))) with
|
|
| none => return none
|
|
| some name_ => return some (@$lDimVarMk name_)
|
|
else
|
|
return none)
|
|
let pat1 ← `(($(quote ``DimVar.mk), args))
|
|
let pat2 ← `(_)
|
|
let body2 ← `(doSeq| return none)
|
|
let pats : Array Term := #[pat1, pat2]
|
|
let bodies : Array (TSyntax ``Lean.Parser.Term.doSeq) := #[arm1Body, body2]
|
|
-- Splice (pat, body) pairs:
|
|
let cmd ← `(partial def reifyDimVar' : $lExpr → $lMetaM ($lOption $lDimVar) := fun e => do
|
|
let e ← ($lWhnf e)
|
|
match (e).getAppFnArgs with
|
|
$[| $pats => $bodies]*)
|
|
elabCommand cmd
|
|
|
|
myDeriveDimVar15
|
|
|
|
end CubicalTransport.Test.Reify
|