0 | module Data.NumIdr.Transform.Point
  1 |
  2 | import Data.Vect
  3 | import Data.NumIdr.PrimArray
  4 | import Data.NumIdr.Array
  5 | import Data.NumIdr.Vector
  6 | import Data.NumIdr.Matrix
  7 | import Data.NumIdr.Interfaces
  8 |
  9 | %default total
 10 |
 11 |
 12 | ||| A point is a wrapper around the basic vector type, intended to be used with
 13 | ||| `Transform`. These contain the exact same information as a vector, but
 14 | ||| behave differently when transforms are applied to them.
 15 | export
 16 | record Point n a where
 17 |   constructor MkPoint
 18 |   vec : Vector n a
 19 |
 20 | %name Point p,q,r
 21 |
 22 |
 23 | --------------------------------------------------------------------------------
 24 | -- Point constructors
 25 | --------------------------------------------------------------------------------
 26 |
 27 |
 28 | ||| Construct a point from a vector.
 29 | export
 30 | fromVector : Vector n a -> Point n a
 31 | fromVector = MkPoint
 32 |
 33 | ||| Convert a point to a vector.
 34 | export
 35 | toVector : Point n a -> Vector n a
 36 | toVector = vec
 37 |
 38 | ||| Construct a point given its coordinates.
 39 | export
 40 | point : Vect n a -> Point n a
 41 | point = fromVector . vector
 42 |
 43 |
 44 | ||| The origin point.
 45 | export
 46 | origin : Num a => {n : Nat} -> Point n a
 47 | origin = fromVector $ zeros [n]
 48 |
 49 |
 50 | --------------------------------------------------------------------------------
 51 | -- Point indexing
 52 | --------------------------------------------------------------------------------
 53 |
 54 |
 55 | infixl 10 !!
 56 | infixl 10 !?
 57 |
 58 | ||| Index the point at the given coordinate.
 59 | export
 60 | index : Fin n -> Point n a -> a
 61 | index i (MkPoint v) = index i v
 62 |
 63 | ||| Index the point at the given coordinate.
 64 | |||
 65 | ||| This is the operator form of `index`.
 66 | export
 67 | (!!) : Point n a -> Fin n -> a
 68 | (!!) = flip index
 69 |
 70 | ||| Index the point at the given coordinate, returning `Nothing` if the index
 71 | ||| is out of bounds.
 72 | export
 73 | indexNB : Nat -> Point n a -> Maybe a
 74 | indexNB n (MkPoint v) = indexNB n v
 75 |
 76 | ||| Index the point at the given coordinate, returning `Nothing` if the index
 77 | ||| is out of bounds.
 78 | |||
 79 | ||| This is the operator form of `indexNB`.
 80 | export
 81 | (!?) : Point n a -> Nat -> Maybe a
 82 | (!?) = flip indexNB
 83 |
 84 |
 85 | ||| Return a `Vect` of the coordinates in the point.
 86 | export
 87 | toVect : Point n a -> Vect n a
 88 | toVect = toVect . vec
 89 |
 90 |
 91 | -- Named projections
 92 |
 93 | ||| Return the x-coordinate (the first value) of the vector.
 94 | export
 95 | (.x) : Point (1 + n) a -> a
 96 | (.x) = index FZ
 97 |
 98 | ||| Return the y-coordinate (the second value) of the vector.
 99 | export
100 | (.y) : Point (2 + n) a -> a
101 | (.y) = index (FS FZ)
102 |
103 | ||| Return the z-coordinate (the third value) of the vector.
104 | export
105 | (.z) : Point (3 + n) a -> a
106 | (.z) = index (FS (FS FZ))
107 |
108 |
109 | --------------------------------------------------------------------------------
110 | -- Arithmetic operations
111 | --------------------------------------------------------------------------------
112 |
113 | infixr 8 +.
114 | infixl 8 .+
115 | infixl 8 -.
116 |
117 | -- Affine space operations
118 | -- These would have been named simply (+) and (-), but that caused
119 | -- too many issues with interface resolution.
120 |
121 | ||| Add a vector to a point.
122 | export
123 | (+.) : Num a => Vector n a -> Point n a -> Point n a
124 | a +. MkPoint b = MkPoint (zipWith (+) a b)
125 |
126 | ||| Add a point to a vector.
127 | export
128 | (.+) : Num a => Point n a -> Vector n a -> Point n a
129 | MkPoint a .+ b = MkPoint (zipWith (+) a b)
130 |
131 |
132 | ||| Subtract two points to get the vector between them.
133 | export
134 | (-.) : Neg a => Point n a -> Point n a -> Vector n a
135 | MkPoint a -. MkPoint b = zipWith (-) a b
136 |
137 |
138 | --------------------------------------------------------------------------------
139 | -- Interface implementations
140 | --------------------------------------------------------------------------------
141 |
142 |
143 | export
144 | Zippable (Point n) where
145 |   zipWith f (MkPoint v1) (MkPoint v2) = MkPoint (zipWith f v1 v2)
146 |   zipWith3 f (MkPoint v1) (MkPoint v2) (MkPoint v3) = MkPoint (zipWith3 f v1 v2 v3)
147 |   unzipWith f (MkPoint v) = bimap MkPoint MkPoint (unzipWith f v)
148 |   unzipWith3 f (MkPoint v) = bimap MkPoint (bimap MkPoint MkPoint) (unzipWith3 f v)
149 |
150 | export
151 | Functor (Point n) where
152 |   map f (MkPoint v) = MkPoint (map f v)
153 |
154 | export
155 | {n : _} -> Applicative (Point n) where
156 |   pure = MkPoint . pure
157 |   MkPoint f <*> MkPoint v = MkPoint (f <*> v)
158 |
159 | {n : _} -> Monad (Point n) where
160 |   join (MkPoint v) = MkPoint $ join $ map unwrap v
161 |     where
162 |       unwrap : Point n a -> Vector n a
163 |       unwrap (MkPoint x) = x
164 |
165 | export
166 | Foldable (Point n) where
167 |   foldl f z (MkPoint v) = foldl f z v
168 |   foldr f z (MkPoint v) = foldr f z v
169 |   null (MkPoint v) = null v
170 |   toList (MkPoint v) = toList v
171 |
172 | export
173 | Traversable (Point n) where
174 |   traverse f (MkPoint v) = map MkPoint (traverse f v)
175 |
176 | export
177 | Show a => Show (Point n a) where
178 |   showPrec d (MkPoint v) = showCon d "point" $ showArg $ toVect v
179 |
180 | export
181 | Cast a b => Cast (Point n a) (Point n b) where
182 |   cast (MkPoint v) = MkPoint (cast v)
183 |
184 | export
185 | Num a => Mult (Matrix m n a) (Point n a) (Point m a) where
186 |   mat *. MkPoint v = MkPoint (mat *. v)
187 |