A VECTOR CLASS WITH OPERATORS

namespace IntSight.XSight.Geometry;
public

    // Vectors are immutable structures
    Vector = const record
    public
        x, y, z: Double; readonly;

        constructor(x, y, z: Double);
        begin
            Self.x := x;
            Self.y := y;
            Self.z := z;
        end;

    public
        property Length: Double => (x.Sqr + y.Sqr + z.Sqr).Sqrt;
            ensures Result >= 0;

        method Mirror(axis: Vector): Vector => Self - 2 * Self * axis;
            requires Self.Length = 1, axis.Length = 1;
            ensures Result.Length = 1;

        method Normalize: Vector =>
            using L := Length do
                if L = 0 then Self else Self / L;
            ensures Self.Length > 0 -> Result.Length = 1;

    public
        static method Combine(f1: Double; v1: Vector; f2: Double; v2: Vector) =>
            new Vector(
                f1 * v1.x + f2 * v2.x,
                f1 * v1.y + f2 * v2.y,
                f1 * v1.z + f2 * v2.z);

    public
        <commutative, associative>
        method+(v1, v2: Vector) =>
            new Vector(v1.x + v2.x, v1.y + v2.y, v1.z + v2.z);

        method-(v1, v2: Vector) =>
            new Vector(v1.x - v2.x, v1.y - v2.y, v1.z - v2.z);

        method-(v: Vector) =>
            new Vector(-v.x, -v.y, -v.z);

        <commutative>
        method*(v1, v2: Vector): Double =>
            v1.x * v2.x + v1.y * v2.y + v1.z * v2.z;

        <associative>
        method^(v1, v2: Vector) =>
            new Vector(
                v1.y * v2.z - v1.z * v2.y,
                v1.z * v2.x - v1.x * v2.z,
                v1.x * v2.y - v1.y * v2.x);

        <commutative>
        method*(v: Vector; f: Double) =>
            new Vector(f * v.x, f * v.y, f * v.z);

        method/(v: Vector; f: Double) =>
            new Vector(v.x / f, v.y / f, v.z / f);
            requires f <> 0;

        operator Explicit(v: Vector): Double => v.Length;
    end;

end.