Data.NumIdr.Homogeneous

Definitions

HMatrix : Nat -> Nat -> Type -> Type

  A homogeneous matrix type.
  
  Homogeneous matrices are matrices that encode an affine transformation, as
  opposed to the more restriced linear transformations of normal matrices.
  Their multiplication is identical to regular matrix multiplication, but the
  extra dimension in each axis allows the homogeneous matrix to store a
  translation vector that is applied during multiplication.
  
  ```hmatrix mat tr *. v == mat *. v + tr```

Totality: total
Visibility: public export

HMatrix' : Nat -> Type -> Type

  A synonym for a square homogeneous matrix.

Totality: total
Visibility: public export

HVector : Nat -> Type -> Type

  An homogeneous vector type.
  
  Homogeneous vectors are vectors intended to be multiplied with homogeneous
  matrices (see `HMatrix`). They have an extra dimension compared to regular
  vectors.

Totality: total
Visibility: public export

vectorToH : Num a => Vector n a -> HVector n a

  Convert a vector to a homogeneous vector.

Totality: total
Visibility: export

vectorToHLinear : Num a => Vector n a -> HVector n a

  Convert a vector to a homogeneous vector that ignores the translation
  component of homogeneous matrices.

Totality: total
Visibility: export

hvector : Num a => Vect n a -> HVector n a

  Construct a homogeneous vector given its coordinates.

Totality: total
Visibility: export

hvectorLinear : Num a => Vect n a -> HVector n a

  Construct a homogeneous vector that ignores translations given its
  coordinates.

Totality: total
Visibility: export

fromHomogeneous : HVector n a -> Vector n a

  Extract a normal vector from a homogeneous vector.

Totality: total
Visibility: export

hmatrix : Num a => Matrix m n a -> Vector m a -> HMatrix m n a

  Construct a homogeneous matrix given a matrix and a translation vector.

Totality: total
Visibility: export

matrixToH : Num a => Matrix m n a -> HMatrix m n a

  Convert a regular matrix to a homogeneous matrix.

Totality: total
Visibility: export

isHMatrix : Eq a => Num a => Matrix m n a -> Bool

  Determine if a matrix fits the pattern of a homogeneous matrix.

Totality: total
Visibility: export

getMatrix : HMatrix m n a -> Matrix m n a

  Get the regular matrix component of a homogeneous matrix.

Totality: total
Visibility: export

getTranslationVector : HMatrix m n a -> Vector m a

  Get the translation vector from a homogeneous matrix.

Totality: total
Visibility: export

scalingH : {default B rep : Rep} -> RepConstraint rep a => Num a => a -> HMatrix' n a

  Construct a homogeneous matrix that scales a vector by the input.

Totality: total
Visibility: export

translationH : Num a => Vector n a -> HMatrix' n a

  Construct a homogeneous matrix that translates by the given vector.

Totality: total
Visibility: export

rotate2DH : {default B rep : Rep} -> RepConstraint rep Double => Double -> HMatrix' 2 Double

  Construct a 2D homogeneous matrix that rotates by the given angle (in radians).

Totality: total
Visibility: export

rotate3DXH : {default B rep : Rep} -> RepConstraint rep Double => Double -> HMatrix' 3 Double

  Construct a 3D homogeneous matrix that rotates around the x-axis.

Totality: total
Visibility: export

rotate3DYH : {default B rep : Rep} -> RepConstraint rep Double => Double -> HMatrix' 3 Double

  Construct a 3D homogeneous matrix that rotates around the y-axis.

Totality: total
Visibility: export

rotate3DZH : {default B rep : Rep} -> RepConstraint rep Double => Double -> HMatrix' 3 Double

  Construct a 3D homogeneous matrix that rotates around the z-axis.

Totality: total
Visibility: export

reflectH : Neg a => Fin n -> HMatrix' n a

Totality: total
Visibility: export

reflectXH : Neg a => HMatrix' (1 + n) a

Totality: total
Visibility: export

reflectYH : Neg a => HMatrix' (2 + n) a

Totality: total
Visibility: export

reflectZH : Neg a => HMatrix' (3 + n) a

Totality: total
Visibility: export