/-!
# Tests of the structure elaborator
-/

-- We want to see the exact constructors in tests.
set_option pp.structureInstances false
set_option pp.proofs true


/-!
Diamond, look at the constructors and flat constructors
-/
namespace Test1

structure S1 (α : Type) where
  x : α
  y : Nat

structure S2 (α : Type) extends S1 α where
  z : Nat

structure S3 (α : Type) extends S1 α where
  w : Nat

structure S4 (α : Type) extends S2 α, S3 α where
  x' : α

/-- info: Test1.S1.mk {α : Type} (x : α) (y : Nat) : S1 α -/
#guard_msgs in #check S1.mk
/-- info: Test1.S2.mk {α : Type} (toS1 : S1 α) (z : Nat) : S2 α -/
#guard_msgs in #check S2.mk
/-- info: Test1.S3.mk {α : Type} (toS1 : S1 α) (w : Nat) : S3 α -/
#guard_msgs in #check S3.mk
/-- info: Test1.S4.mk {α : Type} (toS2 : S2 α) (w : Nat) (x' : α) : S4 α -/
#guard_msgs in #check S4.mk
/--
info: def Test1.S1.mk._flat_ctor : {α : Type} → α → Nat → S1 α :=
fun α x y => S1.mk x y
-/
#guard_msgs in #print S1.mk._flat_ctor
/--
info: def Test1.S2.mk._flat_ctor : {α : Type} → α → Nat → Nat → S2 α :=
fun α x y z => S2.mk (S1.mk x y) z
-/
#guard_msgs in #print S2.mk._flat_ctor
/--
info: def Test1.S3.mk._flat_ctor : {α : Type} → α → Nat → Nat → S3 α :=
fun α x y w => S3.mk (S1.mk x y) w
-/
#guard_msgs in #print S3.mk._flat_ctor
/--
info: def Test1.S4.mk._flat_ctor : {α : Type} → α → Nat → Nat → Nat → α → S4 α :=
fun α x y z w x' => S4.mk (S2.mk (S1.mk x y) z) w x'
-/
#guard_msgs in #print S4.mk._flat_ctor
/-- info: Test1.S4.mk._flat_ctor {α : Type} (x : α) (y z w : Nat) (x' : α) : S4 α -/
#guard_msgs in #check S4.mk._flat_ctor

end Test1

/-!
Verify existence of default value definitions
-/
namespace TestD1

structure D1 where
  x := 1
structure D2 extends D1 where
structure D3 extends D1 where
  x := 3
structure D4 extends D2, D3

/--
info: def TestD1.D1.x._default : Nat :=
id 1
-/
#guard_msgs in #print D1.x._default
/-- error: Unknown constant `D2.x._default` -/
#guard_msgs in #print D2.x._default
/--
info: def TestD1.D2.x._inherited_default : Nat :=
id 1
-/
#guard_msgs in #print D2.x._inherited_default
/--
info: def TestD1.D3.x._default : Nat :=
id 3
-/
#guard_msgs in #print D3.x._default
/-- error: Unknown constant `D4.x._default` -/
#guard_msgs in #print D4.x._default
/--
info: def TestD1.D4.x._inherited_default : Nat :=
id 3
-/
#guard_msgs in #print D4.x._inherited_default

end TestD1

/-!
Verify default value definitions can support parameters
-/
namespace TestD2

structure D1 (α : Type) [Inhabited α] where
  x : α := default
structure D2 (α : Type) [Inhabited α] extends D1 α where
structure D3 extends D1 Nat where

/--
info: def TestD2.D1.x._default : {α : Type} → {inst : Inhabited α} → α :=
fun {α} {inst} => id default
-/
#guard_msgs in #print D1.x._default
/-- error: Unknown constant `D2.x._default` -/
#guard_msgs in #print D2.x._default
/--
info: def TestD2.D2.x._inherited_default : {α : Type} → {inst : Inhabited α} → α :=
fun {α} {inst} => id default
-/
#guard_msgs in #print D2.x._inherited_default
/-- error: Unknown constant `D3.x._default` -/
#guard_msgs in #print D3.x._default
/--
info: def TestD2.D3.x._inherited_default : Nat :=
id default
-/
#guard_msgs in #print D3.x._inherited_default

end TestD2

/-!
Make sure class parents can be used in successive parents
-/
namespace Test2_1

local infixl:70 (priority := high) " * " => Mul.mul

class AssociativeMul (α : Type _) [Mul α] : Prop where
  mul_assoc (x y z : α) : x * y * z = x * (y * z)

class Semigroup (α : Type _) extends Mul α, AssociativeMul α where

/--
info: Test2_1.Semigroup.mk.{u_1} {α : Type u_1} [toMul : Mul α] [toAssociativeMul : AssociativeMul α] : Semigroup α
-/
#guard_msgs in #check Semigroup.mk
/--
info: def Test2_1.Semigroup.mk._flat_ctor.{u_1} : {α : Type u_1} →
  (mul : α → α → α) → (∀ (x y z : α), @Eq α (mul (mul x y) z) (mul x (mul y z))) → Semigroup α :=
fun α mul mul_assoc => @Semigroup.mk α (@Mul.mk α mul) (@AssociativeMul.mk α (@Mul.mk α mul) mul_assoc)
-/
#guard_msgs in set_option pp.explicit true in #print Semigroup.mk._flat_ctor
/--
info: Test2_1.Semigroup.mk._flat_ctor.{u_1} {α : Type u_1} (mul : α → α → α)
  (mul_assoc : ∀ (x y z : α), @Eq α (mul (mul x y) z) (mul x (mul y z))) : Semigroup α
-/
#guard_msgs in set_option pp.explicit true in #check Semigroup.mk._flat_ctor

end Test2_1

/-!
Make sure instances can come from parents with overlapping fields
-/
namespace Test2_2

structure Add2 (α : Type _) where
  add : α → α → α

class Add3 (α : Type _) extends Add2 α, Add α where
  h (x : α) : x + x = x

/--
info: Test2_2.Add3.mk._flat_ctor.{u_1} {α : Type u_1} (add : α → α → α)
  (h : ∀ (x : α), @Eq α (@HAdd.hAdd α α α (@instHAdd α (@Add.mk α add)) x x) x) : Add3 α
-/
#guard_msgs in set_option pp.explicit true in #check Add3.mk._flat_ctor

end Test2_2

/-!
Example that used to be in a comment at `getFieldDefaultValue?`.
The issue was that the default value function was in terms of subobject fields,
so there could be a cyclic dependency.
With a field-centric view in #7302, this is no longer an issue to consider.
-/
namespace Test3

structure A where
  a : Nat

structure B where
  a : Nat
  b : Nat
  c : Nat

structure C extends B where
  d : Nat
  c := b + d

structure D extends A, C

/--
info: def Test3.D.c._inherited_default : Nat → Nat → Nat :=
fun b d => @id Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) b d)
-/
#guard_msgs in set_option pp.explicit true in #print D.c._inherited_default

end Test3

/-!
Make sure we can fill in `toMagma` at the use of `mul`.
It used to be (before #7302) that `mul` would see that the type of `a`, `b`, and `c` were `toMagma.α`,
which would cause unification to fill in the `M` argument.
However, now the types of these variables are just `α`, with no connection to `toMagma`.
We use the heuristic that parent structures should effectively be singleton types while elaborating fields,
and so the `?M : Magma` metavariable should be assigned with `toMagma`.
-/

namespace Test4

structure Magma where
  α   : Type u
  mul : α → α → α

instance : CoeSort Magma (Type u) where
  coe s := s.α

abbrev mul {M : Magma} (a b : M) : M :=
  M.mul a b

local infixl:70 (priority := high) " * " => mul

structure Semigroup extends Magma where
  mul_assoc (a b c : α) : a * b * c = a * (b * c)

/--
info: Test4.Semigroup.mk.{u_1} (toMagma : Magma)
  (mul_assoc :
    ∀ (a b c : toMagma.α), @Eq toMagma.α (@mul toMagma (@mul toMagma a b) c) (@mul toMagma a (@mul toMagma b c))) :
  Semigroup
-/
#guard_msgs in set_option pp.explicit true in #check Semigroup.mk

/--
info: def Test4.Semigroup.mk._flat_ctor.{u_1} : (α : Type u_1) →
  (mul : α → α → α) →
    (∀ (a b c : α),
        @Eq α (@Test4.mul (Magma.mk α mul) (@Test4.mul (Magma.mk α mul) a b) c)
          (@Test4.mul (Magma.mk α mul) a (@Test4.mul (Magma.mk α mul) b c))) →
      Semigroup :=
fun α mul mul_assoc => Semigroup.mk (Magma.mk α mul) mul_assoc
-/
#guard_msgs in set_option pp.explicit true in #print Semigroup.mk._flat_ctor

end Test4

/-!
Default value involving parent instance
-/
namespace Test5

structure C (α : Type) extends Mul α where
  (x y : α)
  z := x * y

/--
info: def Test5.C.z._default : {α : Type} → (α → α → α) → α → α → α :=
fun {α} mul x y => @id α (@HMul.hMul α α α (@instHMul α (@Mul.mk α mul)) x y)
-/
#guard_msgs in set_option pp.explicit true in #print C.z._default

end Test5

/-!
Test from a docstring in Elab/StructInst, to check computed defaults.
-/
namespace Test6

structure A where
  x : Nat := 1

structure B extends A where
  y : Nat := x + 1
  x := y + 1

structure C extends B where
  z : Nat := 2*y
  x := z + 3

/--
info: def Test6.A.x._default : Nat :=
id 1
-/
#guard_msgs in #print A.x._default
/--
info: def Test6.B.y._default : Nat → Nat :=
fun x => id (x + 1)
-/
#guard_msgs in #print B.y._default
/--
info: def Test6.B.x._default : Nat → Nat :=
fun y => id (y + 1)
-/
#guard_msgs in #print B.x._default
/--
info: def Test6.C.x._default : Nat → Nat :=
fun z => id (z + 3)
-/
#guard_msgs in #print C.x._default
/--
info: def Test6.C.y._inherited_default : Nat → Nat :=
fun x => id (x + 1)
-/
#guard_msgs in #print C.y._inherited_default
/--
info: def Test6.C.z._default : Nat → Nat :=
fun y => id (2 * y)
-/
#guard_msgs in #print C.z._default

end Test6

/-!
Dependent types to an inherited field
-/
namespace Test7

structure A1 where
  n : Nat
structure A2 extends A1 where
  h : n > 0

/--
info: def Test7.A2.mk._flat_ctor : (n : Nat) → n > 0 → A2 :=
fun n h => A2.mk (A1.mk n) h
-/
#guard_msgs in #print A2.mk._flat_ctor

end Test7

/-!
Binders and default values
-/
namespace Test8

structure S where
  n (x : Nat) : Nat := x
  m (x : Nat) : Nat := by intros; assumption

/-- info: S.mk (fun x => x) fun x => x : S -/
#guard_msgs in #check { : S }

end Test8

/-!
The default value declaration has the parameters even if they're not used.
-/
namespace Test9
structure Baz (α : Type u) where
  n : Nat := 0
/-- info: Test9.Baz.n._default.{u} {α : Type u} : Nat -/
#guard_msgs in #check Baz.n._default
end Test9

/-!
Diamond inheritance, override autoParam with an autoParam
-/
namespace TestO1

structure S1 where
  x : Nat := by exact 0
structure S2 extends S1 where
structure S3 extends S1 where
  x := by exact 1
structure S4 extends S2, S3


/-- info: TestO1.S1.mk (x : Nat := by exact 0) : S1 -/
#guard_msgs in #check S1.mk
/-- info: TestO1.S2.mk (toS1 : S1) : S2 -/
#guard_msgs in #check S2.mk
/-- info: TestO1.S3.mk (toS1 : S1) : S3 -/
#guard_msgs in #check S3.mk
/-- info: TestO1.S4.mk (toS2 : S2) : S4 -/
#guard_msgs in #check S4.mk
/-- info: TestO1.S1.mk._flat_ctor (x : Nat := by exact 0) : S1 -/
#guard_msgs in #check S1.mk._flat_ctor
/-- info: TestO1.S2.mk._flat_ctor (x : Nat := by exact 0) : S2 -/
#guard_msgs in #check S2.mk._flat_ctor
/-- info: TestO1.S3.mk._flat_ctor (x : Nat := by exact 1) : S3 -/
#guard_msgs in #check S3.mk._flat_ctor
/-- info: TestO1.S4.mk._flat_ctor (x : Nat := by exact 1) : S4 -/
#guard_msgs in #check S4.mk._flat_ctor

/-- info: S1.mk 0 : S1 -/
#guard_msgs in #check { : S1 }
/-- info: S2.mk (S1.mk 0) : S2 -/
#guard_msgs in #check { : S2 }
/-- info: S3.mk (S1.mk 1) : S3 -/
#guard_msgs in #check { : S3 }
/-- info: S4.mk (S2.mk (S1.mk 1)) : S4 -/
#guard_msgs in #check { : S4 }

end TestO1

/-!
Diamond inheritance, override autoParam with an optParam
-/
namespace TestO2

structure S1 where
  x : Nat := by exact 0
structure S2 extends S1 where
structure S3 extends S1 where
  x := 1
structure S4 extends S2, S3


/-- info: TestO2.S1.mk (x : Nat := by exact 0) : S1 -/
#guard_msgs in #check S1.mk
/-- info: TestO2.S2.mk (toS1 : S1) : S2 -/
#guard_msgs in #check S2.mk
/-- info: TestO2.S3.mk (toS1 : S1) : S3 -/
#guard_msgs in #check S3.mk
/-- info: TestO2.S4.mk (toS2 : S2) : S4 -/
#guard_msgs in #check S4.mk
/-- info: TestO2.S1.mk._flat_ctor (x : Nat := by exact 0) : S1 -/
#guard_msgs in #check S1.mk._flat_ctor
/-- info: TestO2.S2.mk._flat_ctor (x : Nat := by exact 0) : S2 -/
#guard_msgs in #check S2.mk._flat_ctor
/-- info: TestO2.S3.mk._flat_ctor (x : Nat) : S3 -/
#guard_msgs in #check S3.mk._flat_ctor
/-- info: TestO2.S3.x._default : Nat -/
#guard_msgs in #check S3.x._default
/-- info: TestO2.S4.mk._flat_ctor (x : Nat) : S4 -/
#guard_msgs in #check S4.mk._flat_ctor
/-- info: TestO2.S4.x._inherited_default : Nat -/
#guard_msgs in #check S4.x._inherited_default

/-- info: S1.mk 0 : S1 -/
#guard_msgs in #check { : S1 }
/-- info: S2.mk (S1.mk 0) : S2 -/
#guard_msgs in #check { : S2 }
/-- info: S3.mk (S1.mk 1) : S3 -/
#guard_msgs in #check { : S3 }
/-- info: S4.mk (S2.mk (S1.mk 1)) : S4 -/
#guard_msgs in #check { : S4 }

end TestO2

namespace TestOptParam

/-!
All fields are in scope when elaborating default values.
-/
structure Loop where
  x : Nat := y
  y : Nat := x
  deriving Repr

/-- info: { x := 1, y := 1 } -/
#guard_msgs in #eval { x := 1 : Loop }
/-- info: { x := 2, y := 2 } -/
#guard_msgs in #eval { y := 2 : Loop }
/-- info: { x := 1, y := 2 } -/
#guard_msgs in #eval { x := 1, y := 2 : Loop }

/-!
Testing a loop that goes through the parent structure.
-/
structure Base where
  x : Nat
  y : Nat := x
  deriving Repr
structure Loop2 extends Base where
  x := y
  deriving Repr
/-- info: { toBase := { x := 1, y := 1 } } -/
#guard_msgs in #eval { x := 1 : Loop2 }
/-- info: { toBase := { x := 2, y := 2 } } -/
#guard_msgs in #eval { y := 2 : Loop2 }

/-!
Restating the type of an inherited field is OK
-/
structure RestateType extends Base where
  x : Nat := 1
  deriving Repr
/-- info: { toBase := { x := 1, y := 1 } } -/
#guard_msgs in #eval { : RestateType }

/-!
Restating the type of an inherited field is a valid
way to change the binder names.
-/
structure A (m : Type → Type) where
  map (f : α → β) : m α → m β
structure A' extends A List where
  map {α β} (g : α → β) (xs : List α) : List β := List.map g xs

/-- info: A'.mk (A.mk fun {α β} g xs => List.map g xs) : A' -/
#guard_msgs in #check { : A'}

/-!
Default values cannot refer to the field.
-/
/-- error: Unknown identifier `x` -/
#guard_msgs in
structure InapplicableDefault1 where
  x : Nat := x + 1

/-!
Default values can refer to later fields.
-/
structure ApplicableDefault2 where
  x : Nat := y + 1
  y : Fin 2

/-!
Default values cannot refer to later fields if they depend on the field.
-/
/-- error: Unknown identifier `y` -/
#guard_msgs in
structure InpplicableDefault3 where
  x : Nat := y + 1
  y : Fin x

/-!
Default values cannot refer to the field, even for inherited fields.
-/
structure Base2 where
  x : Nat
/-- error: Unknown identifier `x` -/
#guard_msgs in
structure InapplicableDefault2 extends Base2 where
  x := x

end TestOptParam

/-!
Some failures from unsupported autoparams
-/
namespace TestFail1

/-- error: Failed to infer type of field `x` -/
#guard_msgs in
structure F1 where
  x := by exact 0

structure F2 where
  x (n : Nat) : Nat
/--
error: Invalid field: Uexpected type for field `x` when setting auto-param tactic for inherited field
-/
#guard_msgs in
structure F3 extends F2 where
  x : Nat → Nat := by exact 0

/--
error: Invalid field: Unexpected binders for field `x` when setting auto-param tactic for inherited field
-/
#guard_msgs in
structure F4 extends F2 where
  x (n : Nat) := by exact 0

/-- error: A default value for field `x` has already been set for this structure -/
#guard_msgs in
structure F5 extends F2 where
  x := by exact 0
  x := by exact 0

/-- error: A default value for field `x` has already been set for this structure -/
#guard_msgs in
structure F6 extends F2 where
  x := id
  x := by exact 0

/-- error: A default value for field `x` has already been set for this structure -/
#guard_msgs in
structure F7 extends F2 where
  x := by exact 0
  x := id

end TestFail1