From 5eef3d27fb252f7a181c3d78ef4a57fa99b3b5a7 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 19 Nov 2024 13:54:45 -0800 Subject: [PATCH] feat: have `#print` show precise fields of structures (#6096) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR improves the `#print` command for structures to show all fields and which parents the fields were inherited from, hiding internal details such as which parents are represented as subobjects. This information is still present in the constructor if needed. The pretty printer for private constants is also improved, and it now handles private names from the current module like any other name; private names from other modules are made hygienic. Example output for `#print Monad`: ``` class Monad.{u, v} (m : Type u → Type v) : Type (max (u + 1) v) number of parameters: 1 parents: Monad.toApplicative : Applicative m Monad.toBind : Bind m fields: Functor.map : {α β : Type u} → (α → β) → m α → m β Functor.mapConst : {α β : Type u} → α → m β → m α Pure.pure : {α : Type u} → α → m α Seq.seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β SeqLeft.seqLeft : {α β : Type u} → m α → (Unit → m β) → m α SeqRight.seqRight : {α β : Type u} → m α → (Unit → m β) → m β Bind.bind : {α β : Type u} → m α → (α → m β) → m β constructor: Monad.mk.{u, v} {m : Type u → Type v} [toApplicative : Applicative m] [toBind : Bind m] : Monad m resolution order: Monad, Applicative, Bind, Functor, Pure, Seq, SeqLeft, SeqRight ``` Suggested by Floris van Doorn [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.23print.20command.20for.20structures/near/482503637). --- src/Lean/Elab/Print.lean | 98 ++++++++---- .../PrettyPrinter/Delaborator/Builtins.lean | 37 +++-- tests/lean/diamond1.lean.expected.out | 18 ++- tests/lean/diamond8.lean.expected.out | 19 ++- tests/lean/printStructure.lean | 144 ++++++++++++------ tests/lean/run/2291.lean | 14 +- tests/lean/run/4465.lean | 2 +- tests/lean/run/print_cmd.lean | 111 ++++++++++++-- tests/lean/structAutoBound.lean.expected.out | 20 +-- 9 files changed, 330 insertions(+), 133 deletions(-) diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index a895c7dc04..ab2d244e3b 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -22,7 +22,7 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData := m := m ++ ", " ++ toMessageData u return m ++ "}" -private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do +private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do let m : MessageData := match (← getReducibilityStatus id) with | ReducibilityStatus.irreducible => "@[irreducible] " @@ -38,11 +38,13 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type let (m, id) := match privateToUserName? id with | some id => (m ++ "private ", id) | none => (m, id) - let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type - pure m + if sig then + return m!"{m}{kind} {id}{levelParamsToMessageData levelParams} : {type}" + else + return m!"{m}{kind}" -private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData := - mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) +private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) (sig : Bool := true) : CommandElabM MessageData := + mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) (sig := sig) private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do let m ← mkHeader kind id levelParams type safety @@ -65,32 +67,63 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat) m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type logInfo m +/-- +Computes the origin of a field. Returns its projection function 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 + 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 + open Meta in private def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr) - (ctor : Name) (fields : Array Name) (isUnsafe : Bool) (isClass : Bool) : CommandElabM Unit := do - let kind := if isClass then "class" else "structure" - let mut m ← mkHeader' kind id levelParams type isUnsafe - m := m ++ Format.line ++ "number of parameters: " ++ toString numParams - m := m ++ Format.line ++ "constructor:" - let cinfo ← getConstInfo ctor - m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type - m := m ++ Format.line ++ "fields:" ++ (← doFields) - logInfo m -where - doFields := liftTermElabM do - forallTelescope (← getConstInfo id).type fun params _ => - withLocalDeclD `self (mkAppN (Expr.const id (levelParams.map .param)) params) fun self => do - let params := params.push self - let mut m : MessageData := "" + (isUnsafe : Bool) : CommandElabM Unit := do + let env ← getEnv + let kind := if isClass env id then "class" else "structure" + let header ← mkHeader' kind id levelParams type isUnsafe (sig := false) + liftTermElabM <| forallTelescope (← getConstInfo id).type fun params _ => + let s := Expr.const id (levelParams.map .param) + withLocalDeclD `self (mkAppN s params) fun self => do + let mut m : MessageData := header + -- Signature + m := m ++ " " ++ .ofFormatWithInfosM do + let (stx, infos) ← PrettyPrinter.delabCore s (delab := PrettyPrinter.Delaborator.delabConstWithSignature) + pure ⟨← PrettyPrinter.ppTerm ⟨stx⟩, infos⟩ + m := m ++ Format.line ++ m!"number of parameters: {numParams}" + -- Parents + let parents := getStructureParentInfo env id + unless parents.isEmpty do + m := m ++ Format.line ++ "parents:" + for parent in parents do + let ptype ← inferType (mkApp (mkAppN (.const parent.projFn (levelParams.map .param)) params) self) + m := m ++ indentD m!"{.ofConstName parent.projFn (fullNames := true)} : {ptype}" + -- Fields + let fields := getStructureFieldsFlattened env id (includeSubobjectFields := false) + if fields.isEmpty then + m := m ++ Format.line ++ "fields: (none)" + else + m := m ++ Format.line ++ "fields:" for field in fields do - match getProjFnForField? (← getEnv) id field with - | some proj => - let field : Format := if isPrivateName proj then "private " ++ toString field else toString field - let cinfo ← getConstInfo proj - let ftype ← instantiateForall cinfo.type params - m := m ++ Format.line ++ field ++ " : " ++ ftype - | none => panic! "missing structure field info" - addMessageContext m + let some source := findField? env id field | panic! "missing structure field info" + let proj ← getFieldOrigin source field + let modifier := if isPrivateName proj then "private " else "" + let ftype ← inferType (← mkProjection self field) + m := m ++ indentD (m!"{modifier}{.ofConstName proj (fullNames := true)} : {ftype}") + -- Constructor + let cinfo := getStructureCtor (← getEnv) id + let ctorModifier := if isPrivateName cinfo.name then "private " else "" + m := m ++ Format.line ++ "constructor:" ++ indentD (ctorModifier ++ .signature cinfo.name) + -- Resolution order + let resOrder ← getStructureResolutionOrder id + if resOrder.size > 1 then + m := m ++ Format.line ++ "resolution order:" + ++ indentD (MessageData.joinSep (resOrder.map (.ofConstName · (fullNames := true))).toList ", ") + logInfo m private def printIdCore (id : Name) : CommandElabM Unit := do let env ← getEnv @@ -103,11 +136,10 @@ private def printIdCore (id : Name) : CommandElabM Unit := do | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } => - match getStructureInfo? env id with - | some { fieldNames, .. } => - let [ctor] := ctors | panic! "structures have only one constructor" - printStructure id us numParams t ctor fieldNames u (isClass env id) - | none => printInduct id us numParams t ctors u + if isStructure env id then + printStructure id us numParams t u + else + printInduct id us numParams t ctors u | none => throwUnknownId id private def printId (id : Syntax) : CommandElabM Unit := do diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 8d106035e4..22a6bf99f0 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -91,21 +91,32 @@ Rather, it is called through the `app` delaborator. -/ def delabConst : Delab := do let Expr.const c₀ ls ← getExpr | unreachable! - let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀ - - let mut c ← unresolveNameGlobal c₀ (fullNames := ← getPPOption getPPFullNames) - let stx ← if ls.isEmpty || !(← getPPOption getPPUniverses) then - if (← getLCtx).usesUserName c then - -- `c` is also a local declaration - if c == c₀ && !(← read).inPattern then - -- `c` is the fully qualified named. So, we append the `_root_` prefix - c := `_root_ ++ c + let mut c₀ := c₀ + let mut c := c₀ + if let some n := privateToUserName? c₀ then + unless (← getPPOption getPPPrivateNames) do + if c₀ == mkPrivateName (← getEnv) n then + -- The name is defined in this module, so use `n` as the name and unresolve like any other name. + c₀ := n + c ← unresolveNameGlobal n (fullNames := ← getPPOption getPPFullNames) else - c := c₀ - pure <| mkIdent c + -- The name is not defined in this module, so make inaccessible. Unresolving does not make sense to do. + c ← withFreshMacroScope <| MonadQuotation.addMacroScope n else - let mvars ← getPPOption getPPMVarsLevels - `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*}) + c ← unresolveNameGlobal c (fullNames := ← getPPOption getPPFullNames) + let stx ← + if ls.isEmpty || !(← getPPOption getPPUniverses) then + if (← getLCtx).usesUserName c then + -- `c` is also a local declaration + if c == c₀ && !(← read).inPattern then + -- `c` is the fully qualified named. So, we append the `_root_` prefix + c := `_root_ ++ c + else + c := c₀ + pure <| mkIdent c + else + let mvars ← getPPOption getPPMVarsLevels + `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*}) let stx ← maybeAddBlockImplicit stx if (← getPPOption getPPTagAppFns) then diff --git a/tests/lean/diamond1.lean.expected.out b/tests/lean/diamond1.lean.expected.out index 49118dbdb3..a7c8f62c67 100644 --- a/tests/lean/diamond1.lean.expected.out +++ b/tests/lean/diamond1.lean.expected.out @@ -2,14 +2,20 @@ diamond1.lean:11:40-11:45: error: parent field type mismatch, field 'a' from par α → α : Type but is expected to have type α : Type -structure Foo : Type → Type +structure Foo (α : Type) : Type number of parameters: 1 -constructor: -Foo.mk : {α : Type} → Bar (α → α) → (Bool → α) → Nat → Foo α +parents: + Foo.toBar : Bar (α → α) + Foo.toBaz : Baz α fields: -toBar : Bar (α → α) -c : Bool → α -d : Nat + Bar.a : α → α + Bar.b : Nat → α → α + Baz.c : Bool → α + Baz.d : Nat +constructor: + Foo.mk {α : Type} (toBar : Bar (α → α)) (c : Bool → α) (d : Nat) : Foo α +resolution order: + Foo, Bar, Baz def f : Nat → Foo Nat := fun x => { a := fun y => x + y, b := fun x1 x2 => x1 + x2, c := fun x_1 => x, d := x } diamond1.lean:27:47-27:52: warning: field 'a' from 'Baz' has already been declared diff --git a/tests/lean/diamond8.lean.expected.out b/tests/lean/diamond8.lean.expected.out index 6dbbcd8b7b..07f82208a1 100644 --- a/tests/lean/diamond8.lean.expected.out +++ b/tests/lean/diamond8.lean.expected.out @@ -1,7 +1,16 @@ -class Semiring.{u} : Type u → Type u +class Semiring.{u} (R : Type u) : Type u number of parameters: 1 -constructor: -Semiring.mk : {R : Type u} → [toAddCommMonoid : AddCommMonoid R] → [toMonoid : Monoid R] → Semiring R +parents: + Semiring.toAddCommMonoid : AddCommMonoid R + Semiring.toMonoidWithZero : MonoidWithZero R + Semiring.toOne : One R fields: -toAddCommMonoid : AddCommMonoid R -toMonoid : Monoid R + Add.add : R → R → R + Zero.zero : R + Mul.mul : R → R → R + One.one : R + Monoid.mul_one : ∀ (m : R), m * 1 = m +constructor: + Semiring.mk.{u} {R : Type u} [toAddCommMonoid : AddCommMonoid R] [toMonoid : Monoid R] : Semiring R +resolution order: + Semiring, AddCommMonoid, MonoidWithZero, Add, Monoid, Zero, Mul, One diff --git a/tests/lean/printStructure.lean b/tests/lean/printStructure.lean index 7c3685f6f6..b867ef066d 100644 --- a/tests/lean/printStructure.lean +++ b/tests/lean/printStructure.lean @@ -1,94 +1,152 @@ /-! - Test #print command for structures and classes +# Test `#print` command for structures and classes -/ -/- Structure -/ +/-! Structure -/ /-- -info: structure Prod.{u, v} : Type u → Type v → Type (max u v) +info: structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v) number of parameters: 2 -constructor: -Prod.mk : {α : Type u} → {β : Type v} → α → β → α × β fields: -fst : α -snd : β + Prod.fst : α + Prod.snd : β +constructor: + Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β -/ #guard_msgs in #print Prod -/- Class -/ +/-! Class -/ /-- -info: class Inhabited.{u} : Sort u → Sort (max 1 u) +info: class Inhabited.{u} (α : Sort u) : Sort (max 1 u) number of parameters: 1 -constructor: -Inhabited.mk : {α : Sort u} → α → Inhabited α fields: -default : α + Inhabited.default : α +constructor: + Inhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α -/ #guard_msgs in #print Inhabited -/- Structure with private field -/ +/-! Structure with private field, imported -/ /-- -info: structure Thunk.{u} : Type u → Type u +info: structure Thunk.{u} (α : Type u) : Type u number of parameters: 1 -constructor: -Thunk.mk : {α : Type u} → (Unit → α) → Thunk α fields: -private fn : Unit → α + private Thunk.fn✝ : Unit → α +constructor: + Thunk.mk.{u} {α : Type u} (fn : Unit → α) : Thunk α -/ #guard_msgs in #print Thunk -/- Extended class -/ +/-! Structure with private field, current module -/ +structure PrivField where + private x : Nat + /-- -info: class Alternative.{u, v} : (Type u → Type v) → Type (max (u + 1) v) -number of parameters: 1 -constructor: -Alternative.mk : {f : Type u → Type v} → - [toApplicative : Applicative f] → ({α : Type u} → f α) → ({α : Type u} → f α → (Unit → f α) → f α) → Alternative f +info: structure PrivField : Type +number of parameters: 0 fields: -toApplicative : Applicative f -failure : {α : Type u} → f α -orElse : {α : Type u} → f α → (Unit → f α) → f α + private PrivField.x : Nat +constructor: + PrivField.mk (x : Nat) : PrivField +-/ +#guard_msgs in +#print PrivField + +/-! Private constructor, imported -/ +/-- +info: class TypeName.{u} (α : Type u) : Type +number of parameters: 1 +fields: + private TypeName.data✝ : (TypeNameData✝ α).type +constructor: + private TypeName.mk'✝.{u} {α : Type u} (data : (TypeNameData✝ α).type) : TypeName α +-/ +#guard_msgs in +#print TypeName + +/-! Private constructor, current module -/ +structure PrivCtor where private mk :: + x : Nat +/-- +info: structure PrivCtor : Type +number of parameters: 0 +fields: + PrivCtor.x : Nat +constructor: + private PrivCtor.mk (x : Nat) : PrivCtor +-/ +#guard_msgs in +#print PrivCtor + +/-! Extended class -/ +/-- +info: class Alternative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v) +number of parameters: 1 +parents: + Alternative.toApplicative : Applicative f +fields: + Functor.map : {α β : Type u} → (α → β) → f α → f β + Functor.mapConst : {α β : Type u} → α → f β → f α + 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 β + Alternative.failure : {α : Type u} → f α + Alternative.orElse : {α : Type u} → f α → (Unit → f α) → f α +constructor: + Alternative.mk.{u, v} {f : Type u → Type v} [toApplicative : Applicative f] (failure : {α : Type u} → f α) + (orElse : {α : Type u} → f α → (Unit → f α) → f α) : Alternative f +resolution order: + Alternative, Applicative, Functor, Pure, Seq, SeqLeft, SeqRight -/ #guard_msgs in #print Alternative -/- Multiply extended class -/ +/-! Multiply extended class -/ /-- -info: class Applicative.{u, v} : (Type u → Type v) → Type (max (u + 1) v) +info: class Applicative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v) number of parameters: 1 -constructor: -Applicative.mk : {f : Type u → Type v} → - [toFunctor : Functor f] → - [toPure : Pure f] → [toSeq : Seq f] → [toSeqLeft : SeqLeft f] → [toSeqRight : SeqRight f] → Applicative f +parents: + Applicative.toFunctor : Functor f + Applicative.toPure : Pure f + Applicative.toSeq : Seq f + Applicative.toSeqLeft : SeqLeft f + Applicative.toSeqRight : SeqRight f fields: -toFunctor : Functor f -toPure : Pure f -toSeq : Seq f -toSeqLeft : SeqLeft f -toSeqRight : SeqRight f + Functor.map : {α β : Type u} → (α → β) → f α → f β + Functor.mapConst : {α β : Type u} → α → f β → f α + 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 β +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 +resolution order: + Applicative, Functor, Pure, Seq, SeqLeft, SeqRight -/ #guard_msgs in #print Applicative -/- Structure with unused parameter -/ +/-! Structure with unused parameter -/ structure Weird (α β : Type _) where a : α /-- -info: structure Weird.{u_1, u_2} : Type u_1 → Type u_2 → Type u_1 +info: structure Weird.{u_1, u_2} (α : Type u_1) (β : Type u_2) : Type u_1 number of parameters: 2 -constructor: -Weird.mk : {α : Type u_1} → {β : Type u_2} → α → Weird α β fields: -a : α + Weird.a : α +constructor: + Weird.mk.{u_1, u_2} {α : Type u_1} {β : Type u_2} (a : α) : Weird α β -/ #guard_msgs in #print Weird -/- Structure-like inductive -/ +/-! Structure-like inductive -/ inductive Fake (α : Type _) where | mk : (x : α) → Fake α diff --git a/tests/lean/run/2291.lean b/tests/lean/run/2291.lean index d3520cb313..e5330ac1d7 100644 --- a/tests/lean/run/2291.lean +++ b/tests/lean/run/2291.lean @@ -21,13 +21,13 @@ let _x_29 := Lean.Expr.const _x_28 _x_25; let _x_30 := _x_29.app _x_23; let _x_31 := []; let _x_32 := 0 :: _x_31; -let _x_33 := Lean.List.toExprAux _x_27 _x_30 _x_32; +let _x_33 := Lean.List.toExprAux✝ _x_27 _x_30 _x_32; Lean.MessageData.ofExpr _x_33 [compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1 fun nilFn consFn x => List.casesOn fun head tail => let _x_1 := Lean.mkNatLit head; - let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail; + let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail; Lean.mkAppB consFn _x_1 _x_2 >> _eval let _x_14 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat"; @@ -41,13 +41,13 @@ let _x_21 := `List.cons; let _x_22 := Lean.Expr.const._override _x_21 _x_18; let _x_23 := Lean.Expr.app._override _x_22 _x_16; let _x_24 := List.cons _neutral 0 _x_15; -let _x_25 := Lean.List.toExprAux._at._eval._spec_1 _x_20 _x_23 _x_24; +let _x_25 := Lean.List.toExprAux._at._eval._spec_1✝ _x_20 _x_23 _x_24; Lean.MessageData.ofExpr _x_25 [compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1 fun nilFn consFn x => List.casesOn fun head tail => let _x_1 := Lean.mkNatLit head; - let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail; + let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail; Lean.mkAppB consFn _x_1 _x_2 >> _eval let _x_1 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat"; @@ -61,13 +61,13 @@ let _x_8 := `List.cons; let _x_9 := Lean.Expr.const._override _x_8 _x_5; let _x_10 := Lean.Expr.app._override _x_9 _x_3; let _x_11 := List.cons _neutral 0 _x_2; -let _x_12 := Lean.List.toExprAux._at._eval._spec_1 _x_7 _x_10 _x_11; +let _x_12 := Lean.List.toExprAux._at._eval._spec_1✝ _x_7 _x_10 _x_11; Lean.MessageData.ofExpr _x_12 [compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1 fun nilFn consFn x => List.casesOn fun head tail => let _x_1 := Lean.mkNatLit head; - let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail; + let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail; Lean.mkAppB consFn _x_1 _x_2 >> _eval._closed_1 "Nat" @@ -102,7 +102,7 @@ let _x_1 := List.nil _neutral; List.cons _neutral 0 _x_1 >> _eval let _x_1 := - Lean.List.toExprAux._at._eval._spec_1 _eval._closed_9 _eval._closed_13 + Lean.List.toExprAux._at._eval._spec_1✝ _eval._closed_9 _eval._closed_13 _eval._closed_14; Lean.MessageData.ofExpr _x_1 --- diff --git a/tests/lean/run/4465.lean b/tests/lean/run/4465.lean index 94591e5dad..081b599642 100644 --- a/tests/lean/run/4465.lean +++ b/tests/lean/run/4465.lean @@ -3,7 +3,7 @@ #reduce Char.ofNat (nat_lit 0) /-- -info: { val := { toBitVec := { toFin := ⟨0, isValidChar_UInt32 (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ } }, +info: { val := { toBitVec := { toFin := ⟨0, isValidChar_UInt32✝ (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ } }, valid := Or.inl (Nat.le_of_ble_eq_true rfl) } -/ #guard_msgs in diff --git a/tests/lean/run/print_cmd.lean b/tests/lean/run/print_cmd.lean index d59f9c2c43..65a21b21fa 100644 --- a/tests/lean/run/print_cmd.lean +++ b/tests/lean/run/print_cmd.lean @@ -2,18 +2,99 @@ private def foo (x : Nat) : Nat := x + 1 -#print "hello" -#print id -#print propext -#print default -#print ReaderT.read -#print Prod -#print Prod.mk -#print Nat -#print Nat.succ -#print Nat.rec -#print Nat.casesOn -#print foo -#print Quot.mk -#print Quot.ind -#print Quot.mk +/-- info: hello -/ +#guard_msgs in #print "hello" +/-- +info: def id.{u} : {α : Sort u} → α → α := +fun {α} a => a +-/ +#guard_msgs in #print id +/-- info: axiom propext : ∀ {a b : Prop}, (a ↔ b) → a = b -/ +#guard_msgs in #print propext +/-- +info: def Inhabited.default.{u} : {α : Sort u} → [self : Inhabited α] → α := +fun α [self : Inhabited α] => self.1 +-/ +#guard_msgs in #print default +/-- +info: protected def ReaderT.read.{u, v} : {ρ : Type u} → {m : Type u → Type v} → [inst : Monad m] → ReaderT ρ m ρ := +fun {ρ} {m} [Monad m] => pure +-/ +#guard_msgs in #print ReaderT.read +/-- +info: structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v) +number of parameters: 2 +fields: + Prod.fst : α + Prod.snd : β +constructor: + Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β +-/ +#guard_msgs in #print Prod +/-- info: constructor Prod.mk.{u, v} : {α : Type u} → {β : Type v} → α → β → α × β -/ +#guard_msgs in #print Prod.mk +/-- +info: inductive Nat : Type +number of parameters: 0 +constructors: +Nat.zero : Nat +Nat.succ : Nat → Nat +-/ +#guard_msgs in #print Nat +/-- info: constructor Nat.succ : Nat → Nat -/ +#guard_msgs in #print Nat.succ +/-- +info: recursor Nat.rec.{u} : {motive : Nat → Sort u} → + motive Nat.zero → ((n : Nat) → motive n → motive n.succ) → (t : Nat) → motive t +-/ +#guard_msgs in #print Nat.rec +/-- +info: @[reducible] def Nat.casesOn.{u} : {motive : Nat → Sort u} → + (t : Nat) → motive Nat.zero → ((n : Nat) → motive n.succ) → motive t := +fun {motive} t zero succ => Nat.rec zero (fun n n_ih => succ n) t +-/ +#guard_msgs in #print Nat.casesOn +/-- +info: private def foo : Nat → Nat := +fun x => x + 1 +-/ +#guard_msgs in #print foo +/-- info: Quotient primitive Quot.mk.{u} : {α : Sort u} → (r : α → α → Prop) → α → Quot r -/ +#guard_msgs in #print Quot.mk +/-- +info: Quotient primitive Quot.ind.{u} : ∀ {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop}, + (∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q +-/ +#guard_msgs in #print Quot.ind +/-- info: Quotient primitive Quot.mk.{u} : {α : Sort u} → (r : α → α → Prop) → α → Quot r -/ +#guard_msgs in #print Quot.mk + +/-! +Structure with diamond inheritance +-/ +structure A where + a : Nat +structure B extends A where + b : Nat +structure C extends A where + c : Nat +structure D extends B, C where + d : Nat + +/-- +info: structure D : Type +number of parameters: 0 +parents: + D.toB : B + D.toC : C +fields: + A.a : Nat + B.b : Nat + C.c : Nat + D.d : Nat +constructor: + D.mk (toB : B) (c d : Nat) : D +resolution order: + D, B, C, A +-/ +#guard_msgs in #print D diff --git a/tests/lean/structAutoBound.lean.expected.out b/tests/lean/structAutoBound.lean.expected.out index 85f9426ef2..6c66d7380c 100644 --- a/tests/lean/structAutoBound.lean.expected.out +++ b/tests/lean/structAutoBound.lean.expected.out @@ -1,16 +1,16 @@ -structure Foo.{v, u_1} : {α : Sort u_1} → (α → Type v) → Sort (max u_1 (v + 1)) +structure Foo.{v, u_1} {α : Sort u_1} (β : α → Type v) : Sort (max u_1 (v + 1)) number of parameters: 2 -constructor: -Foo.mk : {α : Sort u_1} → {β : α → Type v} → (a : α) → β a → Foo β fields: -a : α -b : β self.a + Foo.a : α + Foo.b : β self.a +constructor: + Foo.mk.{v, u_1} {α : Sort u_1} {β : α → Type v} (a : α) (b : β a) : Foo β structAutoBound.lean:9:15-9:16: error: a universe level named 'u' has already been declared -structure Boo.{u, v} : Type u → Type v → Type (max u v) +structure Boo.{u, v} (α : Type u) (β : Type v) : Type (max u v) number of parameters: 2 -constructor: -Boo.mk : {α : Type u} → {β : Type v} → α → β → Boo α β fields: -a : α -b : β + Boo.a : α + Boo.b : β +constructor: + Boo.mk.{u, v} {α : Type u} {β : Type v} (a : α) (b : β) : Boo α β structAutoBound.lean:18:10-18:44: error: unused universe parameter 'w'