toki/numidr
1
0
Fork 0
Code Issues Pull requests Activity

Make WithEpsilon named implementations generic

Browse source
This commit is contained in:
Kiana Sheibani 2024-05-06 04:36:43 -04:00
parent f6809697e8
commit d8c22d7ed6
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
2 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Data/NumIdr/Interfaces.idr
View file

@ -31,16 +31,16 @@ export
FieldCmp Double where
abslt = (<) `on` abs
-- Alternative implementations of `Eq` and `FieldCmp` that compare floating
-- point numbers approximately, useful when working with transforms
-- Alternative implementations of `Eq` and `FieldCmp` that compare approximately,
-- useful when working with flating point numbers
namespace Eq
export
WithEpsilon : Double -> Eq Double
WithEpsilon : (Neg a, Abs a, Ord a) => a -> Eq a
WithEpsilon ep = MkEq (\x,y => abs (x - y) < ep) (\x,y => abs (x - y) >= ep)
namespace FieldCmp
export
WithEpsilon : Double -> FieldCmp Double
WithEpsilon : (Neg a, Fractional a, Abs a, Ord a) => a -> FieldCmp a
WithEpsilon ep = MkFieldCmp @{WithEpsilon ep} ((<) `on` abs)
--------------------------------------------------------------------------------

11
src/Data/NumIdr/Transform/Translation.idr
View file

@ -25,12 +25,13 @@ isTranslation : Eq a => Num a => HMatrix' n a -> Bool
isTranslation {n} mat with (viewShape mat)
_ | Shape [S n,S n] = isHMatrix mat && getMatrix mat == identity
||| Construct a translation given a vector.
export
translate : Num a => Vector n a -> Translation n a
translate v = unsafeMkTrans (translationH v)
||| Try to construct a translation from a homogeneous matrix.
export
fromHMatrix : Eq a => Num a => HMatrix' n a -> Maybe (Translation n a)
fromHMatrix mat = if isTranslation mat then Just (unsafeMkTrans mat) else Nothing
||| Construct a translation given a vector.
export
translate : Num a => Vector n a -> Translation n a
translate v = unsafeMkTrans (translationH v)