{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-}
module Main where
import NumHask.Pair
import NumHask.Prelude
import NumHask.Range
import NumHask.Rect
import NumHask.Space
import NumHask.Laws
import Test.DocTest
import Test.Tasty (defaultMain, testGroup)
main :: IO ()
main = do
doctest
[ "src/NumHask/Pair.hs"
, "src/NumHask/Range.hs"
]
defaultMain $
testGroup
"numhask-range"
[ testGroup "project" $
testLawOf2 ([] :: [(Range Double, Double)]) <$>
projectSpaceFuzzyLaws 10.0
, testGroup "Additive" $
testLawOf ([] :: [Range Double]) <$> additiveSpaceFuzzyLaws 10.0
, testGroup "Multiplicative" $
testLawOf ([] :: [Range Double]) <$> multiplicativeSpaceFuzzyLaws 10.0
, testGroup "MultiplicativeGroup" $
testLawOf ([] :: [Range Double]) <$>
multiplicativeGroupSpaceFuzzyLaws 10.0
, testGroup "Pair" $
testLawOf ([] :: [Pair Double]) <$> fieldFuzzyLaws 10.0
, testGroup "rect project" $
testLawOf2 ([] :: [(Rect Double, Pair Double)]) <$>
projectSpaceFuzzyLaws (Pair 10.0 10.0)
, testGroup "Additive" $
testLawOf ([] :: [Rect Double]) <$>
additiveSpaceFuzzyLaws (Pair 10.0 10.0)
, testGroup "Multiplicative" $
testLawOf ([] :: [Rect Double]) <$>
multiplicativeSpaceFuzzyLaws (Pair 10.0 10.0)
, testGroup "MultiplicativeGroup" $
testLawOf ([] :: [Rect Double]) <$>
multiplicativeGroupSpaceFuzzyLaws (Pair 10.0 10.0)
]
projectSpaceFuzzyLaws ::
( Epsilon (Element s)
, Signed (Element s)
, Ord (Element s)
, Normed s (Element s)
, Space s
)
=> Element s
-> [Law2 s (Element s)]
projectSpaceFuzzyLaws x =
[ ( "project o n (lower o) ≈ lower n"
, Binary20
(\o n ->
singular o ||
singular n ||
x < abs (normL1 o) ||
x < abs (normL1 n) || project o n (lower o) ≈ lower n))
, ( "project o n (upper o) ≈ upper n"
, Binary20
(\o n ->
singular o ||
singular n ||
x < abs (normL1 o) ||
x < abs (normL1 n) || project o n (upper o) ≈ upper n))
, ( "project a a x ≈ x"
, Binary11 (\o s -> singular o || x < abs (normL1 o) || project o o s ≈ s))
]
additiveSpaceFuzzyLaws ::
( Signed (Element s)
, Ord (Element s)
, Normed s (Element s)
, Signed s
, Epsilon s
)
=> Element s
-> [Law s]
additiveSpaceFuzzyLaws n =
[ ( "left unital: zero + a ≈ a"
, Unary (\a -> n < abs (normL1 a) || zero + a ≈ a))
, ( "right unital: a + zero ≈ a"
, Unary (\a -> n < abs (normL1 a) || zero + a ≈ a))
, ( "associative: (a + b) + c ≈ a + (b +c)"
, Ternary (\a b c -> n < abs (normL1 a) || (a + b) + c ≈ a + (b + c)))
, ( "commutative a + b ≈ b + a"
, Binary (\a b -> n < abs (normL1 a) || a + b ≈ b + a))
, ("idempotent a + a ≈ a", Unary (\a -> n < abs (normL1 a) || a + a ≈ a))
, ( "idempotent negate a + negate a ≈ abs a"
, Unary (\a -> n < abs (normL1 a) || a + negate a ≈ abs a))
]
multiplicativeSpaceFuzzyLaws ::
( Signed (Element s)
, Ord (Element s)
, Normed s (Element s)
, Signed s
, Epsilon s
, Multiplicative s
)
=> Element s
-> [Law s]
multiplicativeSpaceFuzzyLaws n =
[ ("left unital: one * a ≈ a", Unary (\a -> n < abs (normL1 a) || one * a ≈ a))
, ("right unital: a * one ≈ a", Unary (\a -> n < abs (normL1 a) || one * a ≈ a))
, ( "associative: (a * b) * c ≈ a * (b *c)"
, Ternary
(\a b c ->
n < abs (normL1 a) ||
n < abs (normL1 b) || n < abs (normL1 c) || (a * b) * c ≈ a * (b * c)))
, ( "commutative a * b ≈ b * a"
, Binary (\a b -> n < abs (normL1 a) || a * b ≈ b * a))
]
multiplicativeGroupSpaceFuzzyLaws ::
( Signed (Element s)
, Ord (Element s)
, Normed s (Element s)
, Signed s
, Space s
, Epsilon s
, MultiplicativeGroup s
)
=> Element s
-> [Law s]
multiplicativeGroupSpaceFuzzyLaws n =
[ ( "divide: a / a ≈ one"
, Unary (\a -> singular a || n < abs (normL1 a) || (a / a) ≈ one))
, ( "recip divide: recip a ≈ one / a"
, Unary (\a -> singular a || n < abs (normL1 a) || recip a ≈ one / a))
, ( "recip left: recip a * a ≈ one"
, Unary (\a -> singular a || n < abs (normL1 a) || recip a * a ≈ one))
, ( "recip right: a * recip a ≈ one"
, Unary (\a -> singular a || n < abs (normL1 a) || a * recip a ≈ one))
]
fieldFuzzyLaws ::
( Signed a
, Ord a
, Normed (r a) a
, Signed (r a)
, MultiplicativeGroup (r a)
, Epsilon (r a)
)
=> a
-> [Law (r a)]
fieldFuzzyLaws n =
[ ( "left unital: zero + a ≈ a"
, Unary (\a -> n < abs (normL1 a) || zero + a ≈ a))
, ( "right unital: a + zero ≈ a"
, Unary (\a -> n < abs (normL1 a) || zero + a ≈ a))
, ( "associative: (a + b) + c ≈ a + (b +c)"
, Ternary (\a b c -> n < abs (normL1 a) || (a + b) + c ≈ a + (b + c)))
, ( "commutative a + b ≈ b + a"
, Binary (\a b -> n < abs (normL1 a) || a + b ≈ b + a))
, ( "minus: a - a ≈ zero"
, Unary (\a -> nearZero a || n < abs (normL1 a) || (a - a) ≈ zero))
, ( "negate minus: negate a ≈ zero - a"
, Unary (\a -> nearZero a || n < abs (normL1 a) || negate a ≈ zero - a))
, ( "negate left: negate a * a ≈ zero"
, Unary (\a -> nearZero a || n < abs (normL1 a) || negate a + a ≈ zero))
, ( "negate right: a * negate a ≈ zero"
, Unary (\a -> nearZero a || n < abs (normL1 a) || a + negate a ≈ zero))
, ("left unital: one * a ≈ a", Unary (\a -> n < abs (normL1 a) || one * a ≈ a))
, ("right unital: a * one ≈ a", Unary (\a -> n < abs (normL1 a) || one * a ≈ a))
, ( "associative: (a * b) * c ≈ a * (b *c)"
, Ternary
(\a b c ->
n < abs (normL1 a) ||
n < abs (normL1 b) || n < abs (normL1 c) || (a * b) * c ≈ a * (b * c)))
, ( "commutative a * b ≈ b * a"
, Binary (\a b -> n < abs (normL1 a) || a * b ≈ b * a))
, ( "divide: a / a ≈ one"
, Unary (\a -> nearZero a || n < abs (normL1 a) || (a / a) ≈ one))
, ( "recip divide: recip a ≈ one / a"
, Unary (\a -> nearZero a || n < abs (normL1 a) || recip a ≈ one / a))
, ( "recip left: recip a * a ≈ one"
, Unary (\a -> nearZero a || n < abs (normL1 a) || recip a * a ≈ one))
, ( "recip right: a * recip a ≈ one"
, Unary (\a -> nearZero a || n < abs (normL1 a) || a * recip a ≈ one))
, ( "left annihilation: a * zero ≈ zero"
, Unary (\a -> n < abs (normL1 a) || a * zero ≈ zero))
, ( "right annihilation: zero * a ≈ zero"
, Unary (\a -> n < abs (normL1 a) || zero * a ≈ zero))
, ( "left distributivity: a * (b + c) ≈ a * b + a * c"
, Ternary
(\a b c ->
n < abs (normL1 a) ||
n < abs (normL1 b) || n < abs (normL1 c) || a * (b + c) ≈ a * b + a * c))
, ( "right distributivity: (a + b) * c ≈ a * c + b * c"
, Ternary
(\a b c ->
n < abs (normL1 a) ||
n < abs (normL1 b) || n < abs (normL1 c) || (a + b) * c ≈ a * c + b * c))
]
semiringFuzzyLaws ::
( Ord a
, Semiring a
, Epsilon a
)
=> [Law a]
semiringFuzzyLaws = additiveLaws <> distributionFuzzyLaws
distributionFuzzyLaws :: (Epsilon a, Eq a, Distribution a) => [Law a]
distributionFuzzyLaws =
[ ( "left annihilation: a * zero == zero"
, Unary (\a -> a `times` zero == zero))
, ( "right annihilation: zero * a == zero"
, Unary (\a -> zero `times` a == zero))
, ( "left distributivity: a * (b + c) ≈ a * b + a * c"
, Ternary (\a b c -> a `times` (b + c) ≈ a `times` b + a `times` c))
, ( "right distributivity: (a + b) * c ≈ a * c + b * c"
, Ternary (\a b c -> (a + b) `times` c ≈ a `times` c + b `times` c))
]