{-# language Trustworthy #-} module NatOptics.Positive.Math ( minus, plus, ) where import Data.Maybe ( Maybe (..) ) import Data.Ord ( Ord, (<) ) import Optics.Core ( preview, review ) import Prelude ( Num, abs, (+), (-) ) import NatOptics.Positive.Unsafe ( Positive (..) ) import qualified NatOptics.Positive as Positive import NatOptics.Signed ( Signed ) import qualified NatOptics.Signed as Signed plus :: Num n => Positive n -> Positive n -> Positive n plus :: forall n. Num n => Positive n -> Positive n -> Positive n plus (PositiveUnsafe n a) (PositiveUnsafe n b) = n -> Positive n forall number. number -> Positive number PositiveUnsafe (n a n -> n -> n forall a. Num a => a -> a -> a + n b) minus :: (Num n, Ord n) => Positive n -> Positive n -> Signed n minus :: forall n. (Num n, Ord n) => Positive n -> Positive n -> Signed n minus Positive n a Positive n b = let a' :: n a' = Optic' A_Prism NoIx n (Positive n) -> Positive n -> n forall k (is :: IxList) t b. Is k A_Review => Optic' k is t b -> b -> t review Optic' A_Prism NoIx n (Positive n) forall n. (Num n, Ord n) => Prism' n (Positive n) Positive.refine Positive n a b' :: n b' = Optic' A_Prism NoIx n (Positive n) -> Positive n -> n forall k (is :: IxList) t b. Is k A_Review => Optic' k is t b -> b -> t review Optic' A_Prism NoIx n (Positive n) forall n. (Num n, Ord n) => Prism' n (Positive n) Positive.refine Positive n b diff :: n diff = n a' n -> n -> n forall a. Num a => a -> a -> a - n b' in case Optic' A_Prism NoIx n (Positive n) -> n -> Maybe (Positive n) forall k (is :: IxList) s a. Is k An_AffineFold => Optic' k is s a -> s -> Maybe a preview Optic' A_Prism NoIx n (Positive n) forall n. (Num n, Ord n) => Prism' n (Positive n) Positive.refine (n -> n forall a. Num a => a -> a abs n diff) of Maybe (Positive n) Nothing -> Signed n forall n. Signed n Signed.Zero Just Positive n diff' -> if n diff n -> n -> Bool forall a. Ord a => a -> a -> Bool < n 0 then Positive n -> Signed n forall n. Positive n -> Signed n Signed.Minus Positive n diff' else Positive n -> Signed n forall n. Positive n -> Signed n Signed.Plus Positive n diff'