Data.NumIdr.Transform.Transform

Definitions

TransType : Type

  A transform type encodes the properties of a transform. There are 8 transform
  types, and together with the coersion relation `(:<)` they form a semilattice.

Totality: total
Visibility: export

TTrivial : TransType

Totality: total
Visibility: public export

TTranslation : TransType

Totality: total
Visibility: public export

TRotation : TransType

Totality: total
Visibility: public export

TRigid : TransType

Totality: total
Visibility: public export

TOrthonormal : TransType

Totality: total
Visibility: public export

TLinear : TransType

Totality: total
Visibility: public export

TIsometry : TransType

Totality: total
Visibility: public export

TAffine : TransType

Totality: total
Visibility: public export

(:<) : TransType -> TransType -> Bool

  Coersion relation for transform types.
  `a :< b` is `True` if and only if any transform of type `a` can be cast into
  a transform of type `b`.

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 7

transMult : TransType -> TransType -> TransType

  Return the type of transform resulting from multiplying transforms of
  the two input types.

Totality: total
Visibility: public export

linearizeType : TransType -> TransType

  Return the linearized transform type, i.e. the transform type resulting
  from removing the translation component of the original transform.

Totality: total
Visibility: public export

delinearizeType : TransType -> TransType

  Return the delinearized transform type, i.e. the transform type resulting
  from adding a translation to the original transform.

Totality: total
Visibility: public export

data Transform : TransType -> Nat -> Type -> Type

  A transform is a wrapper for a homogeneous matrix subject to certain
  restrictions, such as a rotation, an isometry, or a rigid transform.
  The restriction on the transform is encoded by the transform's *type*.
  
  Transforms have special behavior over matrices when it comes to multiplication.
  When a transform is applied to a vector, only the linear part of the transform
  is applied, as if `linearize` were called on the transform before the operation.
  
  In order for non-linear transformations to be used, the transform should be
  applied to the special wrapper type `Point`. This separates the concepts of
  point and vector, which is often useful when working with affine maps.

Totality: total
Visibility: export
Constructor: 

MkTrans : (ty : TransType) -> HMatrix' n a -> Transform ty n a

Hints:

So (t1 :< t2) => Cast a b => Cast (Transform t1 n a) (Transform t2 n b)

Num a => Mult (Transform ty n a) (Point n a) (Point n a)

Num a => Mult (Transform ty n a) (Vector n a) (Vector n a)

Num a => Mult (Transform t1 n a) (Transform t2 n a) (Transform (transMult t1 t2) n a)

FieldCmp a => MultGroup (Transform ty n a)

Num a => MultMonoid (Transform ty n a)

unsafeMkTrans : HMatrix' n a -> Transform ty n a

Totality: total
Visibility: export

getHMatrix : Transform ty n a -> HMatrix' n a

  Unwrap the inner homogeneous matrix from a transform.

Totality: total
Visibility: export

getMatrix : Transform ty n a -> Matrix' n a

  Unwrap the inner matrix from a transform, ignoring the translation component
  if one exists.

Totality: total
Visibility: export

convertRep : (rep : Rep) -> RepConstraint rep a => Transform ty n a -> Transform ty n a

Totality: total
Visibility: export

linearize : Num a => Transform ty n a -> Transform (linearizeType ty) n a

  Linearize a transform by removing its translation component.
  If the transform is already linear, then this function does nothing.

Totality: total
Visibility: export

setTranslation : Num a => Vector n a -> Transform ty n a -> Transform (delinearizeType ty) n a

  Set the translation component of a transform.
  
  `setTranslation v tr == translate v *. linearize tr`
  
  If `tr` is linear:
  `setTranslation v tr == translate v *. tr`

Totality: total
Visibility: export

applyInv : FieldCmp a => Transform ty n a -> Vector n a -> Vector n a

Totality: total
Visibility: export

applyInv : FieldCmp a => Transform ty n a -> Point n a -> Point n a

Totality: total
Visibility: export