eee2909c9d
This PR makes the `deriving Inhabited` handler for `structure`s be able to inherit `Inhabited` instances from structure parents, using the same mechanism as for class parents. This fixes a regression introduced by #9815, which lost the ability to apply `Inhabited` instances for parents represented as subobject fields. With this PR, now it works for all parents in the hierarchy. Implementation detail: adds `struct_inst_default%` for synthesizing a structure default value using `Inhabited` instances for parents and fields. Closes #13372
156 lines
3.6 KiB
Text
156 lines
3.6 KiB
Text
module
|
||
/-!
|
||
# `deriving Inhabited` uses structure field defaults
|
||
|
||
https://github.com/leanprover/lean4/issues/9463
|
||
-/
|
||
|
||
/-!
|
||
This used to use `false` in the `default` instance.
|
||
-/
|
||
structure Config where
|
||
iota := true
|
||
deriving Inhabited
|
||
|
||
/-- info: true -/
|
||
#guard_msgs in #eval (default : Config).iota
|
||
|
||
/-- info: instInhabitedConfig : Inhabited Config -/
|
||
#guard_msgs in #check instInhabitedConfig
|
||
|
||
/-!
|
||
We don't require that every field have a default value.
|
||
-/
|
||
structure Config' where
|
||
iota := true
|
||
n : Nat
|
||
deriving Inhabited
|
||
|
||
/-- info: true -/
|
||
#guard_msgs in #eval (default : Config').iota
|
||
/-- info: 0 -/
|
||
#guard_msgs in #eval (default : Config').n
|
||
|
||
/-- info: instInhabitedConfig' : Inhabited Config' -/
|
||
#guard_msgs in #check instInhabitedConfig'
|
||
|
||
/-!
|
||
It still includes an `[Inhabited _]` parameter when needed.
|
||
-/
|
||
structure Config'' (α : Type) where
|
||
iota := true
|
||
n : α
|
||
deriving Inhabited
|
||
|
||
/-- info: true -/
|
||
#guard_msgs in #eval (default : Config'' Nat).iota
|
||
/-- info: 0 -/
|
||
#guard_msgs in #eval (default : Config'' Nat).n
|
||
|
||
/-- info: instInhabitedConfig'' {a✝ : Type} [Inhabited a✝] : Inhabited (Config'' a✝) -/
|
||
#guard_msgs in #check instInhabitedConfig''
|
||
|
||
/-!
|
||
In this example we can see that it adds an inhabited parameter.
|
||
-/
|
||
structure Config''' (α : Type) where
|
||
n : α → α
|
||
deriving Inhabited
|
||
|
||
/-- info: instInhabitedConfig''' {a✝ : Type} [Inhabited a✝] : Inhabited (Config''' a✝) -/
|
||
#guard_msgs in #check instInhabitedConfig'''
|
||
|
||
/-!
|
||
Providing a default value inhibits adding an inhabited parameter.
|
||
-/
|
||
structure Config'''' (α : Type) where
|
||
n : α → α := id
|
||
deriving Inhabited
|
||
|
||
/-- info: instInhabitedConfig'''' {a✝ : Type} : Inhabited (Config'''' a✝) -/
|
||
#guard_msgs in #check instInhabitedConfig''''
|
||
|
||
/-!
|
||
Mixed needs for `Inhabited` parameters.
|
||
-/
|
||
structure S (α β : Type) where
|
||
f : α → α := id
|
||
g : β
|
||
deriving Inhabited
|
||
|
||
/-- info: instInhabitedS {a✝ a✝¹ : Type} [Inhabited a✝¹] : Inhabited (S a✝ a✝¹) -/
|
||
#guard_msgs in #check instInhabitedS
|
||
|
||
/-!
|
||
When there are structure field default value cycles, those defaults can be ignored.
|
||
-/
|
||
structure A (α : Type) where
|
||
(x y : α)
|
||
deriving Inhabited
|
||
structure B extends A Nat where
|
||
n : Nat := 2
|
||
x := y + 1
|
||
y := x + 1
|
||
deriving Inhabited
|
||
|
||
/-- info: 2 -/
|
||
#guard_msgs in #eval (default : B).n
|
||
/-- info: 0 -/
|
||
#guard_msgs in #eval (default : B).x
|
||
/-- info: 0 -/
|
||
#guard_msgs in #eval (default : B).y
|
||
|
||
/-!
|
||
Regression test: take `meta` into account.
|
||
-/
|
||
public meta section
|
||
|
||
inductive AliasInfo where
|
||
| plain (n : Nat)
|
||
deriving Inhabited, Repr
|
||
|
||
/-- info: AliasInfo.plain 0 -/
|
||
#guard_msgs in #eval repr (default : AliasInfo)
|
||
end
|
||
|
||
/-!
|
||
Regression test: take namespace into account.
|
||
-/
|
||
structure MyNS.MyStruct where
|
||
x : Nat
|
||
deriving Inhabited
|
||
/-- info: MyNS.instInhabitedMyStruct.default : MyNS.MyStruct -/
|
||
#guard_msgs in #check MyNS.instInhabitedMyStruct.default
|
||
/-- info: MyNS.instInhabitedMyStruct : Inhabited MyNS.MyStruct -/
|
||
#guard_msgs in #check MyNS.instInhabitedMyStruct
|
||
|
||
/-!
|
||
Fix for https://github.com/leanprover/lean4/issues/13372
|
||
Should inherit parent structures' Inhabited instances.
|
||
-/
|
||
|
||
structure Foo where
|
||
n : Nat
|
||
m : Nat
|
||
h : n ≤ m
|
||
|
||
instance : Inhabited Foo where
|
||
default := ⟨5, 5, Nat.le.refl⟩
|
||
|
||
-- Was: "failed to generate Inhabited instance for Bar"
|
||
structure Bar extends Foo where
|
||
extra : Bool := true
|
||
a : Nat
|
||
deriving Inhabited
|
||
|
||
/-- info: 5 -/
|
||
#guard_msgs in #eval (default : Bar).n
|
||
/-- info: true -/
|
||
#guard_msgs in #eval (default : Bar).extra
|
||
/-- info: 0 -/
|
||
#guard_msgs in #eval (default : Bar).a
|
||
|
||
/-- info: Bar.mk default true default : Bar -/
|
||
#guard_msgs in
|
||
set_option pp.structureInstances false in
|
||
#check (struct_inst_default% : Bar)
|