LAWS.bend source

LAWS.bend on the hub · documented module

# 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 Baseimport ./lib.bend as Vlaw 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  }