From 608a5899dc5e9eba260ffd71bc59dd0701482766 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 24 Mar 2025 02:25:27 -0700 Subject: [PATCH] feat: have `#print` show structure field defaults (#7652) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR gives `#print` for structures the ability to show the default values and auto-param tactics for fields. Example: ``` #print Applicative ``` shows ``` class Applicative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v) [...] fields: Functor.map : {α β : Type u} → (α → β) → f α → f β := fun {α β} x y => pure x <*> y Functor.mapConst : {α β : Type u} → α → f β → f α := fun {α β} => Functor.map ∘ Function.const β Pure.pure : {α : Type u} → α → f α Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α := fun {α β} a b => Function.const β <$> a <*> b () SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β := fun {α β} a b => Function.const α id <$> a <*> b () [...] ``` --- src/Lean/Elab/Print.lean | 66 +++++++++++++++++++++++++++++----- tests/lean/printStructure.lean | 24 ++++++++----- 2 files changed, 74 insertions(+), 16 deletions(-) diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index 9a5516ca65..06c22150b1 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -68,20 +68,20 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat) logInfo m /-- -Computes the origin of a field. Returns its projection function at the origin. +Computes the origin of a field. Returns its `StructureFieldInfo` at the origin. Multiple parents could be the origin of a field, but we say the first parent that provides it is the one that determines the origin. -/ -private partial def getFieldOrigin (structName field : Name) : MetaM Name := do +private partial def getFieldOrigin (structName field : Name) : MetaM StructureFieldInfo := do let env ← getEnv for parent in getStructureParentInfo env structName do if (findField? env parent.structName field).isSome then return ← getFieldOrigin parent.structName field let some fi := getFieldInfo? env structName field | throwError "no such field {field} in {structName}" - return fi.projFn + return fi open Meta in -private def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr) +private partial def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr) (isUnsafe : Bool) : CommandElabM Unit := do let env ← getEnv let kind := if isClass env id then "class" else "structure" @@ -103,17 +103,47 @@ private def printStructure (id : Name) (levelParams : List Name) (numParams : Na let ptype ← inferType (mkApp (mkAppN (.const parent.projFn (levelParams.map .param)) params) self) m := m ++ indentD m!"{.ofConstName parent.projFn (fullNames := true)} : {ptype}" -- Fields + -- Collect params in a map for default value processing + let paramMap : NameMap Expr ← params.foldlM (init := {}) fun paramMap param => do + pure <| paramMap.insert (← param.fvarId!.getUserName) param + -- Collect autoParam tactics, which are all on the flat constructor: + let flatCtorName := mkFlatCtorOfStructName id + let autoParams : NameMap Syntax ← forallTelescope (← getConstInfo flatCtorName).type fun args _ => + args[numParams:].foldlM (init := {}) fun set arg => do + let decl ← arg.fvarId!.getDecl + if let some (.const tacticDecl _) := decl.type.getAutoParamTactic? then + let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl + pure <| set.insert decl.userName tacticSyntax + else + pure set let fields := getStructureFieldsFlattened env id (includeSubobjectFields := false) if fields.isEmpty then m := m ++ Format.line ++ "fields: (none)" else m := m ++ Format.line ++ "fields:" + -- Map of fields to projections of `self` + let fieldMap : NameMap Expr ← fields.foldlM (init := {}) fun fieldMap field => do + pure <| fieldMap.insert field (← mkProjection self field) for field in fields do let some source := findField? env id field | panic! "missing structure field info" - let proj ← getFieldOrigin source field + let fi ← getFieldOrigin source field + let proj := fi.projFn let modifier := if isPrivateName proj then "private " else "" - let ftype ← inferType (← mkProjection self field) - m := m ++ indentD (m!"{modifier}{.ofConstName proj (fullNames := true)} : {ftype}") + let ftype ← inferType (fieldMap.find! field) + let value ← + if let some stx := autoParams.find? field then + let stx : TSyntax ``Parser.Tactic.tacticSeq := ⟨stx⟩ + pure m!" := by{indentD stx}" + else if let some defFn := getEffectiveDefaultFnForField? env id field then + let cinfo ← getConstInfo defFn + let defValue ← instantiateValueLevelParams cinfo (levelParams.map .param) + if let some val ← processDefaultValue paramMap fieldMap defValue then + pure m!" :={indentExpr val}" + else + pure m!" := " + else + pure m!"" + m := m ++ indentD (m!"{modifier}{.ofConstName proj (fullNames := true)} : {MessageData.nest 2 ftype}{value}") -- Constructor let cinfo := getStructureCtor (← getEnv) id let ctorModifier := if isPrivateName cinfo.name then "private " else "" @@ -123,7 +153,27 @@ private def printStructure (id : Name) (levelParams : List Name) (numParams : Na if resOrder.size > 1 then m := m ++ Format.line ++ "field notation resolution order:" ++ indentD (MessageData.joinSep (resOrder.map (.ofConstName · (fullNames := true))).toList ", ") - logInfo m + -- Omit proofs; the delaborator enables `pp.proofs` for non-constant proofs, but we don't want this for default values + withOptions (fun opts => opts.set pp.proofs.name false) do + logInfo m +where + processDefaultValue (paramMap : NameMap Expr) (fieldValues : NameMap Expr) : Expr → MetaM (Option Expr) + | .lam n d b c => do + if c.isExplicit then + let some val := fieldValues.find? n | return none + if ← isDefEq (← inferType val) d then + processDefaultValue paramMap fieldValues (b.instantiate1 val) + else + return none + else + let some param := paramMap.find? n | return none + if ← isDefEq (← inferType param) d then + processDefaultValue paramMap fieldValues (b.instantiate1 param) + else + return none + | e => + let_expr id _ a := e | return some e + return some a private def printIdCore (id : Name) : CommandElabM Unit := do let env ← getEnv diff --git a/tests/lean/printStructure.lean b/tests/lean/printStructure.lean index 778e9b8581..082e50e1d3 100644 --- a/tests/lean/printStructure.lean +++ b/tests/lean/printStructure.lean @@ -87,12 +87,16 @@ number of parameters: 1 parents: Alternative.toApplicative : Applicative f fields: - Functor.map : {α β : Type u} → (α → β) → f α → f β - Functor.mapConst : {α β : Type u} → α → f β → f α + Functor.map : {α β : Type u} → (α → β) → f α → f β := + fun {α β} x y => pure x <*> y + Functor.mapConst : {α β : Type u} → α → f β → f α := + fun {α β} => Functor.map ∘ Function.const β Pure.pure : {α : Type u} → α → f α Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β - SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α - SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β + SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α := + fun {α β} a b => Function.const β <$> a <*> b () + SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β := + fun {α β} a b => Function.const α id <$> a <*> b () Alternative.failure : {α : Type u} → f α Alternative.orElse : {α : Type u} → f α → (Unit → f α) → f α constructor: @@ -115,12 +119,16 @@ parents: Applicative.toSeqLeft : SeqLeft f Applicative.toSeqRight : SeqRight f fields: - Functor.map : {α β : Type u} → (α → β) → f α → f β - Functor.mapConst : {α β : Type u} → α → f β → f α + Functor.map : {α β : Type u} → (α → β) → f α → f β := + fun {α β} x y => pure x <*> y + Functor.mapConst : {α β : Type u} → α → f β → f α := + fun {α β} => Functor.map ∘ Function.const β Pure.pure : {α : Type u} → α → f α Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β - SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α - SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β + SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α := + fun {α β} a b => Function.const β <$> a <*> b () + SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β := + fun {α β} a b => Function.const α id <$> a <*> b () constructor: Applicative.mk.{u, v} {f : Type u → Type v} [toFunctor : Functor f] [toPure : Pure f] [toSeq : Seq f] [toSeqLeft : SeqLeft f] [toSeqRight : SeqRight f] : Applicative f