# Definitional laws for Vec2.
#
# Base F32 arithmetic is opaque to Bend's definitional equality. Therefore the
# exact laws below preserve F32.add/sub/mul/dot normal forms rather than making
# false claims that those primitives normalize to mathematical real arithmetic.
# They still lock down constructors, projections, component placement, and the
# concrete expansion of the usual vector identities.
import Base
import ./lib.bend as V

law make_ctor:
  { V.Vec2.make(1.0, 2.0) == V.Vec2{1.0, 2.0} : V.Vec2 }

law zero_ctor:
  { V.Vec2.zero() == V.Vec2{0.0, 0.0} : V.Vec2 }

law unit_x_ctor:
  { V.Vec2.unit_x() == V.Vec2{1.0, 0.0} : V.Vec2 }

law unit_y_ctor:
  { V.Vec2.unit_y() == V.Vec2{0.0, 1.0} : V.Vec2 }

law x_projection:
  { V.Vec2.x(V.Vec2.make(3.0, 4.0)) == 3.0 : F32 }

law y_projection:
  { V.Vec2.y(V.Vec2.make(3.0, 4.0)) == 4.0 : F32 }

# add zero, stated at the exact F32 normal form available to Base.
law add_zero:
  {
    V.Vec2.add(V.Vec2.make(3.0, 4.0), V.Vec2.zero())
      == V.Vec2{F32.add(3.0, 0.0), F32.add(4.0, 0.0)}
    : V.Vec2
  }

# scale one, stated at the exact F32 normal form available to Base.
law scale_one:
  {
    V.Vec2.scale(V.Vec2.make(3.0, 4.0), 1.0)
      == V.Vec2{F32.mul(3.0, 1.0), F32.mul(4.0, 1.0)}
    : V.Vec2
  }

law sub_self:
  {
    V.Vec2.sub(V.Vec2.make(3.0, 4.0), V.Vec2.make(3.0, 4.0))
      == V.Vec2{F32.sub(3.0, 3.0), F32.sub(4.0, 4.0)}
    : V.Vec2
  }

law dot:
  {
    V.Vec2.dot(V.Vec2.make(3.0, 4.0), V.Vec2.make(2.0, 5.0))
      == F32.add(F32.mul(3.0, 2.0), F32.mul(4.0, 5.0))
    : F32
  }

law length_sq:
  {
    V.Vec2.length_sq(V.Vec2.make(3.0, 4.0))
      == F32.add(F32.mul(3.0, 3.0), F32.mul(4.0, 4.0))
    : F32
  }

law lerp:
  {
    V.Vec2.lerp(V.Vec2.make(0.0, 2.0), V.Vec2.make(10.0, 6.0), 0.25)
      == V.Vec2.add(
        V.Vec2.make(0.0, 2.0),
        V.Vec2.scale(
          V.Vec2.sub(V.Vec2.make(10.0, 6.0), V.Vec2.make(0.0, 2.0)),
          0.25))
    : V.Vec2
  }

law unit_x_dot_unit_y:
  {
    V.Vec2.dot(V.Vec2.unit_x(), V.Vec2.unit_y())
      == F32.add(F32.mul(1.0, 0.0), F32.mul(0.0, 1.0))
    : F32
  }