From be119f5116a22bf93284c5c15bab62b5accde447 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 21 Oct 2022 17:59:22 -0400 Subject: [PATCH] Add approximate floating point comparison --- src/Data/NumIdr/Interfaces.idr | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/src/Data/NumIdr/Interfaces.idr b/src/Data/NumIdr/Interfaces.idr index 506f146..1f133eb 100644 --- a/src/Data/NumIdr/Interfaces.idr +++ b/src/Data/NumIdr/Interfaces.idr @@ -28,10 +28,22 @@ interface (Eq a, Neg a, Fractional a) => FieldCmp a where export -(Ord a, Abs a, Neg a, Fractional a) => FieldCmp a where - abslt x y = abs x < abs y +FieldCmp Double where + abslt = (<) `on` abs +-- Alternative implementations of `Eq` and `FieldCmp` that compare floating +-- point numbers approximately, useful when working with transforms +namespace Eq + export + WithEpsilon : Double -> Eq Double + WithEpsilon ep = MkEq (\x,y => x - y < ep) (\x,y => x - y >= ep) + +namespace FieldCmp + export + WithEpsilon : Double -> FieldCmp Double + WithEpsilon ep = MkFieldCmp @{WithEpsilon ep} ((<) `on` abs) + -------------------------------------------------------------------------------- -- Multiplication -------------------------------------------------------------------------------- @@ -82,8 +94,8 @@ interface MultMonoid a => MultGroup a where constructor MkMultGroup ||| Calculate the inverse of the matrix or transformation. ||| WARNING: This function will not check if an inverse exists for the given - ||| input, and will happily return results containing NaN values. To avoid - ||| this, use `tryInverse` instead. + ||| input, and will happily divide by zero or return results containing NaN. + ||| To avoid this, use `tryInverse` instead. inverse : a -> a