
  0 | module Geom.Matrix
  1 | 
  2 | ||| A 2x2 matrix of floating point numbers
  3 | public export
  4 | record Matrix where
  5 |   constructor M
  6 |   x11 : Double
  7 |   x12 : Double
  8 |   x21 : Double
  9 |   x22 : Double
 10 | 
 11 | ||| Matrix addition
 12 | export
 13 | (+) : Matrix -> Matrix -> Matrix
 14 | M a1 b1 c1 d1 + M a2 b2 c2 d2 = M (a1 + a2) (b1 + b2) (c1 + c2) (d1 + d2)
 15 | 
 16 | ||| Matrix multiplication
 17 | export
 18 | (*) : Matrix -> Matrix -> Matrix
 19 | M x11 x12 x21 x22 * M y11 y12 y21 y22 =
 20 |   M (x11 * y11 + x12 * y21)
 21 |     (x11 * y21 + x12 * y22)
 22 |     (x21 * y11 + x22 * y21)
 23 |     (x21 * y21 + x22 * y22)
 24 | 
 25 | ||| Tries to compute the inverse of a matrix
 26 | |||
 27 | ||| This fails if the determinant of the matrix equals zero.
 28 | export
 29 | inverse : Matrix -> Maybe Matrix
 30 | inverse (M a b c d) =
 31 |   let det := a * d - b * c
 32 |    in if abs det < 1.0e-12 then Nothing
 33 |       else Just $ M (d / det) (negate b / det) (negate c / det) (a / det)
 34 |