diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,3 @@ +# Version 0.1 + +* Initial version. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,219 @@ +Copyright 2020, Renzo Carbonara. + +Except where otherwise explicitly mentioned, all of contents of the +Haskell "i" project are licensed under the Apache License, +Version 2.0 (the "License"); you may not use this file except in +compliance with the License. You may obtain a copy of the License at the +end of this file or at http://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. + + +------------------------------------------------------------------------------- + + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,4 @@ +# i + +Haskell interval types. + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} + +module Main (main) where + +import Control.Monad +import Data.List (stripPrefix) +import Distribution.Compat.Time (getModTime) +import Distribution.PackageDescription (PackageDescription) +import Distribution.Simple (defaultMainWithHooks, simpleUserHooks, UserHooks(..)) +import Distribution.Simple.BuildPaths (autogenComponentModulesDir, getSourceFiles) +import Distribution.Simple.LocalBuildInfo (LocalBuildInfo, withLibLBI) +import Distribution.Simple.Utils (debug) +import Distribution.Verbosity (normal) +import System.Directory (createDirectoryIfMissing, doesFileExist) + +main :: IO () +main = defaultMainWithHooks $ simpleUserHooks + { buildHook = \pd lbi uh bf -> do + generate pd lbi + buildHook simpleUserHooks pd lbi uh bf + , haddockHook = \pd lbi uh bf -> do + generate pd lbi + haddockHook simpleUserHooks pd lbi uh bf + , replHook = \pd lbi uh bf args -> do + generate pd lbi + replHook simpleUserHooks pd lbi uh bf args + } + where + generate :: PackageDescription -> LocalBuildInfo -> IO () + generate pd lbi = do + withLibLBI pd lbi $ \lib clbi -> do + lMods <- getSourceFiles normal ["hs"] ["I.Word8", "I.Int8"] + Just mWord8Path <- pure $ lookup "I.Word8" lMods + Just mInt8Path <- pure $ lookup "I.Int8" lMods + + let lAutogenDir = autogenComponentModulesDir lbi clbi + lIAutogenDir = lAutogenDir <> "/I/Autogen" + createDirectoryIfMissing True lIAutogenDir + + mWord8Source <- readFile mWord8Path + mWord8ModTime <- getModTime mWord8Path + forM_ likeWord8 $ \like -> do + let likePath = lIAutogenDir <> "/" <> like <> ".hs" + gen <- doesFileExist likePath >>= \case + False -> pure True + True -> do likeModTime <- getModTime likePath + pure (likeModTime < mWord8ModTime) + when gen $ do + writeFile likePath + $ replace "Word8" like + $ replace "module I.Word8" "module I.Autogen.Word8" + $ mWord8Source + debug normal ("Generated " <> likePath) + + mInt8Source <- readFile mInt8Path + mInt8ModTime <- getModTime mInt8Path + forM_ likeInt8 $ \like -> do + let likePath = lIAutogenDir <> "/" <> like <> ".hs" + gen <- doesFileExist likePath >>= \case + False -> pure True + True -> do likeModTime <- getModTime likePath + pure (likeModTime < mInt8ModTime) + when gen $ do + writeFile likePath + $ replace "Int8" like + $ replace "module I.Int8" "module I.Autogen.Int8" + $ mInt8Source + debug normal ("Generated " <> likePath) + + +likeWord8 :: [String] +likeWord8 = + [ "Word" + , "Word16" + , "Word32" + , "Word64" + , "CUChar" + , "CUShort" + , "CUInt" + , "CULong" + , "CSize" + , "CULLong" + , "CUIntPtr" + , "CUIntMax" + ] + +likeInt8 :: [String] +likeInt8 = + [ "Int" + , "Int16" + , "Int32" + , "Int64" + , "CChar" + , "CSChar" + , "CShort" + , "CInt" + , "CLong" + , "CPtrdiff" + , "CWchar" + , "CLLong" + , "CIntPtr" + , "CIntMax" + ] + +replace + :: String -- ^ Old substring. + -> String -- ^ New substring. + -> String -- ^ Old string. + -> String -- ^ New string. +replace o n [] = [] +replace o n x@(x0:xs) + | Just y <- stripPrefix o x = n <> replace o n y + | otherwise = x0 : replace o n xs + + diff --git a/hs/I.hs b/hs/I.hs new file mode 100644 --- /dev/null +++ b/hs/I.hs @@ -0,0 +1,95 @@ +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | "I" am a Haskell module designed to be imported as follows: +-- +-- @ +-- import "I" ('I') +-- import "I" qualified +-- @ +-- +-- 'I' exist so that you don't have to manually check that a value is within +-- an interval. For example: +-- +-- [@'I' 'Prelude.Int' ('KindInteger.N' 5) ('KindInteger.P' 5)@] +-- An 'Prelude.Int' known to be in the interval /[-5, +5]/. +-- +-- [@'I' 'Numeric.Natural.Natural' 100 ''Prelude.Nothing'@] +-- A 'Numeric.Natural.Natural' known to be in the interval /[100, +infinity)/. +-- +-- [@'I' 'Prelude.Rational' (''Prelude.Just' '( ''Prelude.False', 0 'KindRational./' 1)) (''Prelude.Just' '( ''Prelude.True', 1 'KindRational./' 2))@] +-- A 'Prelude.Rational' known to be in the interval /(0, +0.5]/. +module I + ( -- * Interval + I + , T + , MinT + , MaxT + , L + , MinL + , R + , MaxR + , Interval(..) + , unwrap + , wrap + , unsafe + , Clamp(..) + , Up(..) + , down + , Discrete(..) + , Succ(..) + , Pred(..) + , One(..) + , Zero(..) + , Negate(..) + , Plus(..) + , Mult(..) + , Minus(..) + , Div(..) + -- * Known + , Known(..) + , known + , With(..) + , min + , max + , single + -- * Testing + , Shove(..) + -- * Danger + , unsafest + ) where + +import I.Internal +import I.Int8 () +import I.Word8 () +import I.Natural () +import I.Integer () +import I.Rational () + +import I.Autogen.CChar () +import I.Autogen.CInt () +import I.Autogen.CIntMax () +import I.Autogen.CIntPtr () +import I.Autogen.CLLong () +import I.Autogen.CLong () +import I.Autogen.CPtrdiff () +import I.Autogen.CSChar () +import I.Autogen.CShort () +import I.Autogen.CSize () +import I.Autogen.CUChar () +import I.Autogen.CUInt () +import I.Autogen.CUIntMax () +import I.Autogen.CUIntPtr () +import I.Autogen.CULLong () +import I.Autogen.CULong () +import I.Autogen.CUShort () +import I.Autogen.CWchar () +import I.Autogen.Int () +import I.Autogen.Int16 () +import I.Autogen.Int32 () +import I.Autogen.Int64 () +import I.Autogen.Word () +import I.Autogen.Word16 () +import I.Autogen.Word32 () +import I.Autogen.Word64 () + diff --git a/hs/I/Int8.hs b/hs/I/Int8.hs new file mode 100644 --- /dev/null +++ b/hs/I/Int8.hs @@ -0,0 +1,112 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_HADDOCK not-home #-} + +module I.Int8 () where + +import Control.Monad +import Data.Constraint +import Data.Int +import Data.Maybe +import Data.Proxy +import Data.Type.Ord +import Foreign.C.Types +import KindInteger (type (/=), type (==)) +import KindInteger qualified as K +import Prelude hiding (min, max, div) +import Prelude qualified as P + +import I.Internal + +-------------------------------------------------------------------------------- + +-- | This is so that GHC doesn't complain about the unused modules, +-- which we import here so that `genmodules.sh` doesn't have to add it +-- to the generated modules. +_ignore :: (CSize, Int) +_ignore = (0, 0) + +-------------------------------------------------------------------------------- + +type instance MinL Int8 = MinT Int8 +type instance MaxR Int8 = MaxT Int8 + +instance forall (l :: K.Integer) (r :: K.Integer). + ( IntervalCtx Int8 l r + ) => Interval Int8 l r where + type IntervalCtx Int8 l r = + ( K.KnownInteger l + , K.KnownInteger r + , MinT Int8 <= l + , l <= r + , r <= MaxT Int8 ) + type MinI Int8 l r = l + type MaxI Int8 l r = r + inhabitant = min + from = \x -> unsafest x <$ guard (l <= x && x <= r) + where l = fromInteger (K.integerVal (Proxy @l)) :: Int8 + r = fromInteger (K.integerVal (Proxy @r)) :: Int8 + negate' (unwrap -> x) = do + guard (x /= minBound) + from (P.negate x) + (unwrap -> a) `plus'` (unwrap -> b) + | b > 0 && a > maxBound - b = Nothing + | b < 0 && a < minBound - b = Nothing + | otherwise = from (a + b) + (unwrap -> a) `mult'` (unwrap -> b) = do + guard $ case a <= 0 of + True | b <= 0 -> a == 0 || b >= (maxBound `quot` a) + | otherwise -> a >= (minBound `quot` b) + False | b <= 0 -> b >= (minBound `quot` a) + | otherwise -> a <= (maxBound `quot` b) + from (a * b) + (unwrap -> a) `minus'` (unwrap -> b) + | b > 0 && a < minBound + b = Nothing + | b < 0 && a > maxBound + b = Nothing + | otherwise = from (a - b) + (unwrap -> a) `div'` (unwrap -> b) = do + guard (b /= 0 && (b /= -1 || a /= minBound)) + let (q, m) = divMod a b + guard (m == 0) + from q + +instance (Interval Int8 l r) => Clamp Int8 l r + +instance (Interval Int8 ld rd, Interval Int8 lu ru, lu <= ld, rd <= ru) + => Up Int8 ld rd lu ru + +instance forall l r t. + ( Interval Int8 l r, KnownCtx Int8 l r t + ) => Known Int8 l r t where + type KnownCtx Int8 l r t = (K.KnownInteger t, l <= t, t <= r) + known' = unsafe . fromInteger . K.integerVal + +instance forall l r. (Interval Int8 l r) => With Int8 l r where + with x g = case K.someIntegerVal (toInteger (unwrap x)) of + K.SomeInteger (pt :: Proxy t) -> + fromMaybe (error "I.with: impossible") $ do + Dict <- leInteger @l @t + Dict <- leInteger @t @r + pure (g pt) + +instance (Interval Int8 l r, l /= r) => Discrete Int8 l r where + pred' i = unsafe (unwrap i - 1) <$ guard (min < i) + succ' i = unsafe (unwrap i + 1) <$ guard (i < max) + +instance (Zero Int8 l r, l == K.Negate r) => Negate Int8 l r where + negate = unsafe . P.negate . unwrap + +instance (Interval Int8 l r, l <= K.P 0, K.P 0 <= r) => Zero Int8 l r where + zero = unsafe 0 + +instance (Interval Int8 l r, l <= K.P 1, K.P 1 <= r) => One Int8 l r where + one = unsafe 1 + +instance forall l r. (Interval Int8 l r) => Shove Int8 l r where + shove = \x -> fromMaybe (error "shove(Int8): impossible") $ + from $ fromInteger (mod (toInteger x) (r - l + 1) + l) + where l = toInteger (unwrap (min @Int8 @l @r)) + r = toInteger (unwrap (max @Int8 @l @r)) + diff --git a/hs/I/Integer.hs b/hs/I/Integer.hs new file mode 100644 --- /dev/null +++ b/hs/I/Integer.hs @@ -0,0 +1,352 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_HADDOCK not-home #-} + +module I.Integer () where + +import Control.Monad +import Data.Constraint +import Data.Maybe +import Data.Proxy +import Data.Type.Ord +import KindInteger qualified as K +import KindInteger (type (/=)) +import Prelude hiding (min, max, div, succ, pred) +import Prelude qualified as P + +import I.Internal + +-------------------------------------------------------------------------------- + +type instance MinL P.Integer = 'Nothing +type instance MaxR P.Integer = 'Nothing + +instance forall l r. + ( IntervalCtx P.Integer ('Just l) ('Just r) + ) => Interval P.Integer ('Just l) ('Just r) where + type IntervalCtx P.Integer ('Just l) ('Just r) = + (K.KnownInteger l, K.KnownInteger r, l <= r) + type MinI P.Integer ('Just l) ('Just r) = l + type MaxI P.Integer ('Just l) ('Just r) = r + inhabitant = min + from = \x -> unsafest x <$ guard (l <= x && x <= r) + where l = K.integerVal (Proxy @l) + r = K.integerVal (Proxy @r) + negate' = from . P.negate . unwrap + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + let (q, m) = divMod (unwrap a) (unwrap b) + guard (m == 0) + from q + +instance forall l. + ( IntervalCtx P.Integer ('Just l) 'Nothing + ) => Interval P.Integer ('Just l) 'Nothing where + type IntervalCtx P.Integer ('Just l) 'Nothing = K.KnownInteger l + type MinI P.Integer ('Just l) 'Nothing = l + inhabitant = min + from = \x -> unsafest x <$ guard (l <= x) + where l = K.integerVal (Proxy @l) + negate' = from . P.negate . unwrap + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + let (q, m) = divMod (unwrap a) (unwrap b) + guard (m == 0) + from q + +instance forall r. + ( IntervalCtx P.Integer 'Nothing ('Just r) + ) => Interval P.Integer 'Nothing ('Just r) where + type IntervalCtx P.Integer 'Nothing ('Just r) = K.KnownInteger r + type MaxI P.Integer 'Nothing ('Just r) = r + inhabitant = max + from = \x -> unsafest x <$ guard (x <= r) + where r = K.integerVal (Proxy @r) + negate' = from . P.negate . unwrap + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + let (q, m) = divMod (unwrap a) (unwrap b) + guard (m == 0) + from q + +instance Interval P.Integer 'Nothing 'Nothing where + inhabitant = zero + from = pure . wrap + negate' = pure . wrap . P.negate . unwrap + a `plus'` b = pure (a `plus` b) + a `mult'` b = pure (a `mult` b) + a `minus'` b = pure (a `minus` b) + a `div'` b = do guard (unwrap b /= 0) + let (q, m) = divMod (unwrap a) (unwrap b) + guard (m == 0) + from q + +-------------------------------------------------------------------------------- + +instance + ( Interval Integer ('Just l) ('Just r) + ) => Clamp Integer ('Just l) ('Just r) + +instance + ( Interval Integer ('Just l) 'Nothing + ) => Clamp Integer ('Just l) 'Nothing where + clamp = \case + x | x <= unwrap min_ -> min_ + | otherwise -> UnsafeI x + where min_ = min + +instance + ( Interval Integer 'Nothing ('Just r) + ) => Clamp Integer 'Nothing ('Just r) where + clamp = \case + x | x >= unwrap max_ -> max_ + | otherwise -> UnsafeI x + where max_ = max + +instance + ( Interval Integer 'Nothing 'Nothing + ) => Clamp Integer 'Nothing 'Nothing where + clamp = UnsafeI + +-------------------------------------------------------------------------------- + +instance + ( lu <= ld + , rd <= ru + , Interval Integer ('Just ld) ('Just rd) + , Interval Integer ('Just lu) ('Just ru) + ) => Up Integer ('Just ld) ('Just rd) ('Just lu) ('Just ru) + +instance + ( lu <= ld + , Interval Integer ('Just ld) yrd + , Interval Integer ('Just lu) 'Nothing + ) => Up Integer ('Just ld) yrd ('Just lu) 'Nothing + +instance + ( rd <= ru + , Interval Integer yld ('Just rd) + , Interval Integer 'Nothing ('Just ru) + ) => Up Integer yld ('Just rd) 'Nothing ('Just ru) + +instance + ( Interval Integer yld yrd + , Interval Integer 'Nothing 'Nothing ) + => Up Integer yld yrd 'Nothing 'Nothing + +-------------------------------------------------------------------------------- + +instance forall l r t. + ( Interval P.Integer ('Just l) ('Just r) + , KnownCtx P.Integer ('Just l) ('Just r) t + ) => Known P.Integer ('Just l) ('Just r) t where + type KnownCtx P.Integer ('Just l) ('Just r) t = + (K.KnownInteger t, l <= t, t <= r) + known' = UnsafeI . K.integerVal + +instance forall t l. + ( Interval P.Integer ('Just l) 'Nothing + , KnownCtx P.Integer ('Just l) 'Nothing t + ) => Known P.Integer ('Just l) 'Nothing t where + type KnownCtx P.Integer ('Just l) 'Nothing t = (K.KnownInteger t, l <= t) + known' = UnsafeI . K.integerVal + +instance forall t r. + ( Interval P.Integer 'Nothing ('Just r) + , KnownCtx P.Integer 'Nothing ('Just r) t + ) => Known P.Integer 'Nothing ('Just r) t where + type KnownCtx P.Integer 'Nothing ('Just r) t = (K.KnownInteger t, t <= r) + known' = UnsafeI . K.integerVal + +instance forall t. + ( KnownCtx P.Integer 'Nothing 'Nothing t + ) => Known P.Integer 'Nothing 'Nothing t where + type KnownCtx P.Integer 'Nothing 'Nothing t = K.KnownInteger t + known' = UnsafeI . K.integerVal + +-------------------------------------------------------------------------------- + +instance forall l r. + ( Interval P.Integer ('Just l) ('Just r) + ) => With P.Integer ('Just l) ('Just r) where + with x g = case K.someIntegerVal (unwrap x) of + K.SomeInteger (pt :: Proxy t) -> + fromMaybe (error "I.with(Integer): impossible") $ do + Dict <- leInteger @l @t + Dict <- leInteger @t @r + pure (g pt) + +instance forall l. + ( Interval P.Integer ('Just l) 'Nothing + ) => With P.Integer ('Just l) 'Nothing where + with x g = case K.someIntegerVal (unwrap x) of + K.SomeInteger (pt :: Proxy t) -> + fromMaybe (error "I.with(Integer): impossible") $ do + Dict <- leInteger @l @t + pure (g pt) + +instance forall r. + ( Interval P.Integer 'Nothing ('Just r) + ) => With P.Integer 'Nothing ('Just r) where + with x g = case K.someIntegerVal (unwrap x) of + K.SomeInteger (pt :: Proxy t) -> + fromMaybe (error "I.with(Integer): impossible") $ do + Dict <- leInteger @t @r + pure (g pt) + +instance With P.Integer 'Nothing 'Nothing where + with x g = case K.someIntegerVal (unwrap x) of + K.SomeInteger (pt :: Proxy t) -> g pt + +-------------------------------------------------------------------------------- + +instance + ( Interval P.Integer ('Just l) ('Just r), l /= r + ) => Discrete P.Integer ('Just l) ('Just r) where + pred' i = UnsafeI (unwrap i - 1) <$ guard (min < i) + succ' i = UnsafeI (unwrap i + 1) <$ guard (i < max) + +instance + ( Interval P.Integer ('Just l) 'Nothing + ) => Discrete P.Integer ('Just l) 'Nothing where + pred' i = UnsafeI (unwrap i - 1) <$ guard (min < i) + succ' = pure . succ + +instance + ( Interval P.Integer 'Nothing ('Just r) + ) => Discrete P.Integer 'Nothing ('Just r) where + pred' = pure . pred + succ' i = UnsafeI (unwrap i + 1) <$ guard (i < max) + +instance Discrete P.Integer 'Nothing 'Nothing where + pred' = pure . pred + succ' = pure . succ + +-------------------------------------------------------------------------------- + +instance + ( Discrete P.Integer 'Nothing r + ) => Pred P.Integer 'Nothing r where + pred i = UnsafeI (unwrap i - 1) + +-------------------------------------------------------------------------------- + +instance + ( Discrete P.Integer l 'Nothing + ) => Succ P.Integer l 'Nothing where + succ i = UnsafeI (unwrap i + 1) + +-------------------------------------------------------------------------------- + +instance + ( Interval P.Integer ('Just l) 'Nothing, K.P 0 <= l + ) => Plus P.Integer ('Just l) 'Nothing where + a `plus` b = UnsafeI (unwrap a + unwrap b) + +instance + ( Interval P.Integer 'Nothing ('Just r), r <= K.P 0 + ) => Plus P.Integer 'Nothing ('Just r) where + a `plus` b = UnsafeI (unwrap a + unwrap b) + +instance Plus P.Integer 'Nothing 'Nothing where + a `plus` b = UnsafeI (unwrap a + unwrap b) + +-------------------------------------------------------------------------------- + +instance + ( Interval P.Integer ('Just l) 'Nothing, K.P 0 <= l + ) => Mult P.Integer ('Just l) 'Nothing where + a `mult` b = UnsafeI (unwrap a * unwrap b) + +instance Mult P.Integer 'Nothing 'Nothing where + a `mult` b = UnsafeI (unwrap a * unwrap b) + +-------------------------------------------------------------------------------- + +instance Minus P.Integer 'Nothing 'Nothing where + a `minus` b = UnsafeI (unwrap a - unwrap b) + +-------------------------------------------------------------------------------- + +instance + ( Interval P.Integer ('Just l) ('Just r), l <= K.P 0, K.P 0 <= r + ) => Zero P.Integer ('Just l) ('Just r) where + zero = UnsafeI 0 + +instance + ( Interval P.Integer ('Just l) 'Nothing, l <= K.P 0 + ) => Zero P.Integer ('Just l) 'Nothing where + zero = UnsafeI 0 + +instance + ( Interval P.Integer 'Nothing ('Just r), K.P 0 <= r + ) => Zero P.Integer 'Nothing ('Just r) where + zero = UnsafeI 0 + +instance Zero P.Integer 'Nothing 'Nothing where + zero = UnsafeI 0 + +-------------------------------------------------------------------------------- + +instance + ( Interval P.Integer ('Just l) ('Just r), l <= K.P 1, K.P 1 <= r + ) => One P.Integer ('Just l) ('Just r) where + one = UnsafeI 1 + +instance + ( Interval P.Integer ('Just l) 'Nothing, l <= K.P 1 + ) => One P.Integer ('Just l) 'Nothing where + one = UnsafeI 1 + +instance + ( Interval P.Integer 'Nothing ('Just r), K.P 1 <= r + ) => One P.Integer 'Nothing ('Just r) where + one = UnsafeI 1 + +instance One P.Integer 'Nothing 'Nothing where + one = UnsafeI 1 + +-------------------------------------------------------------------------------- + +instance + ( Zero P.Integer ('Just l) ('Just r), l K.== K.Negate r + ) => Negate P.Integer ('Just l) ('Just r) where + negate = UnsafeI . P.negate . unwrap + +instance Negate P.Integer 'Nothing 'Nothing where + negate = UnsafeI . P.negate . unwrap + +-------------------------------------------------------------------------------- + +instance + ( Interval Integer ('Just l) ('Just r) + ) => Shove Integer ('Just l) ('Just r) where + shove = \x -> unsafe $ mod x (r - l + 1) + l + where l = unwrap (min @Integer @('Just l) @('Just r)) + r = unwrap (max @Integer @('Just l) @('Just r)) + +instance + ( Interval Integer ('Just l) 'Nothing + ) => Shove Integer ('Just l) 'Nothing where + shove = \x -> unsafe $ if x < l then l + (l - x) else x + where l = unwrap (min @Integer @('Just l) @'Nothing) + +instance + ( Interval Integer 'Nothing ('Just r) + ) => Shove Integer 'Nothing ('Just r) where + shove = \x -> unsafe $ if x > r then r - (x - r) else x + where r = unwrap (max @Integer @'Nothing @('Just r)) + +instance + ( Interval Integer 'Nothing 'Nothing + ) => Shove Integer 'Nothing 'Nothing where + shove = wrap + diff --git a/hs/I/Internal.hs b/hs/I/Internal.hs new file mode 100644 --- /dev/null +++ b/hs/I/Internal.hs @@ -0,0 +1,770 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +#include +#include + +module I.Internal where + +import Data.Coerce +import Data.Constraint +import Data.Kind +import Data.Int +import Data.Maybe +import Data.Proxy +import Data.Word +import Data.Type.Equality +import Foreign.C.Types +import GHC.TypeLits qualified as L +import GHC.Stack +import KindInteger qualified as KI +import KindRational qualified as KR +import Prelude hiding (min, max, div, pred, succ, recip, negate) +import Unsafe.Coerce (unsafeCoerce) + +-------------------------------------------------------------------------------- + +leNatural + :: forall a b + . (L.KnownNat a, L.KnownNat b) + => Maybe (Dict (a L.<= b)) +leNatural = case L.cmpNat (Proxy @a) (Proxy @b) of + L.LTI -> Just $ unsafeCoerce (Dict @()) + L.EQI -> Just $ unsafeCoerce (Dict @()) + L.GTI -> Nothing + +leInteger + :: forall (a :: KI.Integer) (b :: KI.Integer) + . (KI.KnownInteger a, KI.KnownInteger b) + => Maybe (Dict (a L.<= b)) +leInteger = case KI.cmpInteger (Proxy @a) (Proxy @b) of + L.LTI -> Just $ unsafeCoerce (Dict @()) + L.EQI -> Just $ unsafeCoerce (Dict @()) + L.GTI -> Nothing + +-------------------------------------------------------------------------------- + +type role I nominal nominal nominal +-- | A value of type @x@ known to be within the __i__nterval determined +-- by the left end @l@ and right end @r@. +newtype I (x :: Type) (l :: L x) (r :: R x) = UnsafeI x + -- ^ For @'UnsafeI' x@ to be safe, @'Known' x l r t@ needs to be satisfied, + -- with @t@ being the type-level representation of the value of type @x@. + deriving newtype (Eq, Ord, Show) + +-- | The kind of the __t__ype-level representation of @x@ in @'I' x l r@, +-- as it appears in @'Known' x l r t@. +type family T (x :: Type) :: k + +-- | Type-level verison of @__'minBound'__ :: x@. If @x@ is unbounded on the +-- left end, then it's ok to leave @'MinT' x@ undefined. +-- If defined, it should match what 'MinL' means. +type family MinT (x :: Type) :: T x + +-- | Type-level verison of @__'maxBound'__ :: x@. If @x@ is unbounded on the +-- right end, then it's ok to leave @'MaxT' x@ undefined. +-- If defined, it should match what 'MaxR' means. +type family MaxT (x :: Type) :: T x + +-- | The kind of @__l__@ in @'I' x l r@. +type family L (x :: Type) :: k + +-- | __Min__imum __l__eft bound for @x@. All the values of type @x@ are at +-- least as @'MinL' x@ says, as required by 'wrap'. +type family MinL (x :: Type) :: L x + +-- | The kind of @__r__@ in @'I' x l r@. +type family R (x :: Type) :: k + +-- | __Max__imum __r__ight bound for @x@. All the values of type @x@ are at +-- most as @'MaxR' x@ says, as required by 'wrap'. +type family MaxR (x :: Type) :: R x + + +-- | For @'I' x l r@ to be a valid interval type, @'Interval' x l r@ needs +-- to be satisfied. All 'Interval's are non-empty. +-- +-- __NB__: When defining 'Interval' instances, instead of mentioning any +-- necessary constraints in the instance context, mention them them in +-- 'IntervalCtx'. By doing so, when an instance of @'Interval' x l r@ is +-- satisfied, @'IntervalCtx' x l r@ is satisfied as well. If you don't do +-- this, 'with' won't behave as you would expect. +class IntervalCtx x l r => Interval (x :: Type) (l :: L x) (r :: R x) where + -- | Constraints to be satisfied for @'I' x l r@ to be a valid non-empty + -- interval type. + type IntervalCtx x l r :: Constraint + type IntervalCtx x l r = () + + -- | Minimum value of type @x@ contained in the interval @'I' x l r@, if any. + -- If @'I' x l r@ is unbounded on the left end, then it's ok to leave + -- @'MinI' x l r@ undefined. If defined, it should mean the same as @l@. + type MinI x l r :: T x + type MinI x l r = L.TypeError + ('L.Text "MinI not defined in instance ‘" 'L.:<>: + 'L.ShowType (Interval x l r) 'L.:<>: 'L.Text "’") + + -- | Maximum value of type @x@ contained in the interval @'I' x l r@, if any. + -- If @'I' x l r@ is unbounded on the right end, then it's ok to leave + -- @'MaxI' x l r@ undefined. If defined, it should mean the same as @r@. + type MaxI x l r :: T x + type MaxI x l r = L.TypeError + ('L.Text "MaxI not defined in instance ‘" 'L.:<>: + 'L.ShowType (Interval x l r) 'L.:<>: 'L.Text "’") + + -- | Proof that there is at least one element in the @'I' x l r@ interval. + -- + -- No guarantees are made about the value of 'inhabitant' other than the + -- fact that it is known to inhabit the interval. The only exception to this + -- are intervals that contain a single inhabitant, in which case + -- 'inhabitant' will produce it. See 'single'. + inhabitant :: I x l r + + -- | Wrap the @x@ value in the interval @'I' x l r@, if it fits. + -- + -- * Consider using 'wrap' if the interval includes all values of type @x@. + -- + -- * Consider using 'known' if you have type-level knowledge + -- about the value of @x@. + -- + -- * Consider using 'unsafe' if you know that the @x@ is within the interval. + -- + -- [Identity law] + -- + -- @ + -- forall (x :: 'Type'). + -- /such that/ 'isJust' ('from' x). + -- 'fmap' 'unwrap' ('from' x) == 'Just' x + -- @ + from :: x -> Maybe (I x l r) + + -- | @'plus'' a b@ adds @a@ and @b@. + -- + -- 'Nothing' if the result would be out of the interval. See 'plus', too. + plus' :: I x l r -> I x l r -> Maybe (I x l r) + plus' _ _ = Nothing + + -- | @'mult'' a b@ multiplies @a@ times @b@. + -- + -- 'Nothing' if the result would be out of the interval. See 'mult', too. + mult' :: I x l r -> I x l r -> Maybe (I x l r) + mult' _ _ = Nothing + + -- | @'minus'' a b@ substracts @b@ from @a@. + -- + -- 'Nothing' if the result would be out of the interval. See 'minus', too. + minus' :: I x l r -> I x l r -> Maybe (I x l r) + minus' a b = plus' a =<< negate' b + {-# INLINE minus' #-} + + -- | @'negate'' a@ is the additive inverse of @a@. + -- + -- 'Nothing' if the result would be out of the interval. See 'negate', too. + negate' :: I x l r -> Maybe (I x l r) + negate' _ = Nothing + + -- | @'recip'' a@ is the multiplicative inverse of @a@. + -- + -- 'Nothing' if the result would be out of the interval. + recip' :: I x l r -> Maybe (I x l r) + recip' _ = Nothing + + -- | @'div'' a b@ divides @a@ by @b@. + -- + -- 'Nothing' if the result would be out of the interval. See 'div' too. + div' :: I x l r -> I x l r -> Maybe (I x l r) + div' a b = mult' a =<< recip' b + {-# INLINE div' #-} + +-- | 'unsafe' allows you to wrap an @x@ in an @'I' x l r@, failing +-- with 'error' if the @x@ is outside the interval. +-- +-- __WARNING__: This function calls 'from', which means that you can't use +-- it to implement 'from'. You will have to use 'unsafest' in that case. +-- Your code will loop indefinitely otherwise. +unsafe :: forall x l r. (HasCallStack, Interval x l r) => x -> I x l r +unsafe = fromMaybe (error "I.unsafe: input outside interval") . from +{-# INLINE unsafe #-} + +-- | 'unsafest' allows you to wrap an @x@ in an @'I' x l r@ without +-- checking whether the @x@ is within the interval ends. +-- +-- __WARNING__: This function is fast because it doesn't do any work, but also +-- it is very dangerous because it ignores all the safety supposedly given by +-- the @'I' x l r@ type. Don't use this unless you have proved by other means +-- that the @x@ is within the @'I' x l r@ interval. +-- Please use 'from' instead, or even 'unsafe'. +unsafest :: forall x l r. x -> I x l r +unsafest = coerce +{-# INLINE unsafest #-} + +-- | 'Interval's that support clamping. +class (Interval x l r) => Clamp (x :: Type) (l :: L x) (r :: R x) where + -- | Wrap @x@ in @'I' x l r@, making sure that @x@ is within the interval + -- ends by clamping it to @'MinI' x l r@ if less than @l@, or to + -- @'MaxI' x l r@ if more than @r@, if necessary. + clamp :: x -> I x l r + default clamp + :: ( Known x l r (MinI x l r) + , Known x l r (MaxI x l r) + , Ord x ) + => x + -> I x l r + clamp = \case + x | x <= unwrap min_ -> min_ + | x >= unwrap max_ -> max_ + | otherwise -> unsafe x + where min_ = min -- for both type-inferrence and memoizing purposes + max_ = max + +-- | Downcast @'I' x lu ru@ into @'I' x ld rd@ if wrapped @x@ value fits +-- in @'I' x ld rd@. +down :: forall x lu ru ld rd + . (Interval x ld rd) + => I x lu ru + -> Maybe (I x ld rd) +down = from . unwrap +{-# INLINE down #-} + +-- | 'Interval's that can be upcasted to a larger 'Interval' type. +class + ( Interval x ld rd + , Interval x lu ru + ) => Up (x :: Type) (ld :: L x) (rd :: R x) (lu :: L x) (ru :: R x) + where + -- | Proof that @'I' x ld rd@ can be upcasted into @'I' x lu ru@. + -- + -- [Identity law] + -- + -- @ + -- forall (a :: 'I' x ld rd). + -- ('Up' x ld rd lu ru) => + -- 'unwrap' a == 'unwrap' ('up' a :: 'I' x lu ru) + -- @ + up :: I x ld rd -> I x lu ru + -- For safety reasons, the default implementation is @'unsafe' . 'unwrap'@, + -- which means upcasting is not free, as it involves a runtime check and a + -- posibility of 'error'. Consider giving an implementation using 'unsafest'. + default up :: HasCallStack => I x ld rd -> I x lu ru + up = unsafe . unwrap + {-# INLINE up #-} + +-- | Identity. This instance is /INCOHERENT/, but that's OK because all +-- implementations of 'up' should give the same result, and this instance +-- is as fast as possible. So, it doesn't matter whether this instance +-- or another one is picked. +instance {-# INCOHERENT #-} (Interval x l r) => Up x l r l r where + up = unsafest . unwrap + {-# INLINE up #-} + +-- | 'Interval's that contain /discrete/ elements. +class (Interval x l r) => Discrete (x :: Type) (l :: L x) (r :: R x) where + -- | __Pred__ecessor. That is, the previous /discrete/ value in the interval. + -- + -- 'Nothing' if the result would be out of the interval. See 'pred' too. + pred' :: I x l r -> Maybe (I x l r) + -- | __Succ__essor. That is, the next /discrete/ value in the interval. + -- + -- 'Nothing' if the result would be out of the interval. See 'succ' too. + succ' :: I x l r -> Maybe (I x l r) + +-- | 'Interval's known to be inhabited by the number /zero/. +class (Interval x l r) => Zero (x :: Type) (l :: L x) (r :: R x) where + -- | Zero. + zero :: I x l r + +-- | 'Interval's known to be inhabited by the number /one/. +class (Interval x l r) => One (x :: Type) (l :: L x) (r :: R x) where + -- | One. + one :: I x l r + +-- | 'Interval's where /addition/ is known to be a closed operation. +class (Interval x l r) => Plus (x :: Type) (l :: L x) (r :: R x) where + -- | @'plus' a b@ adds @a@ and @b@. + -- + -- [Correspondence with 'plus''] + -- + -- @ + -- forall (a :: 'I' x l r) (b :: 'I' x l r). + -- ('Plus' x l r) => + -- 'plus'' a b == 'Just' ('plus' a b) + -- @ + plus :: I x l r -> I x l r -> I x l r + +-- | 'Interval's where /multiplication/ is known to be a closed operation. +class (Interval x l r) => Mult (x :: Type) (l :: L x) (r :: R x) where + -- | @'mult' a b@ multiplies @a@ times @b@. + -- + -- [Correspondence with 'mult''] + -- + -- @ + -- forall (a :: 'I' x l r) (b :: 'I' x l r). + -- ('Mult' x l r) => + -- 'mult'' a b == 'Just' ('mult' a b) + -- @ + mult :: I x l r -> I x l r -> I x l r + +-- | 'Interval's where /subtraction/ is known to be a closed operation. +class (Zero x l r) => Minus (x :: Type) (l :: L x) (r :: R x) where + -- | @'minus' a b@ substracts @b@ from @a@ + -- + -- [Correspondence with 'minus''] + -- + -- @ + -- forall (a :: 'I' x l r) (b :: 'I' x l r). + -- ('Minus' x l r) => + -- 'minus'' a b == 'Just' ('minus' a b) + -- @ + minus :: I x l r -> I x l r -> I x l r + +-- | 'Interval's where /negation/ is known to be a closed operation. +class (Zero x l r) => Negate (x :: Type) (l :: L x) (r :: R x) where + -- | Additive inverse, if it fits in the interval. + -- + -- [Identity law] + -- + -- @ + -- forall (a :: 'I' x l r). + -- ('Negate' x l r) => + -- a == 'negate' ('negate' a) + -- @ + -- + -- [Correspondence with 'negate''] + -- + -- @ + -- forall (a :: 'I' x l r) (b :: 'I' x l r). + -- ('Minus' x l r) => + -- 'negate'' a b == 'Just' ('negate' a b) + -- @ + negate :: I x l r -> I x l r + +-- | 'Discrete' 'Interval's where obtaining the /predecessor/ is knonwn +-- to be a closed operation. +class (Discrete x l r) => Pred (x :: Type) (l :: L x) (r :: R x) where + -- | @'pred' a@ is the previous discrete value in the interval, + -- the /predecessor/. + -- + -- [Correspondence with 'pred''] + -- + -- @ + -- forall (a :: 'I' x l r). + -- ('Pred' x l r) => + -- 'pred'' a == 'Just' ('pred' a) + -- @ + pred :: I x l r -> I x l r + +-- | 'Discrete' 'Interval's where obtaining the /successor/ is knonwn +-- to be a closed operation. +class (Discrete x l r) => Succ (x :: Type) (l :: L x) (r :: R x) where + -- | @'succ' a@ is the next discrete value in the interval, the /successor/. + -- + -- [Correspondence with 'succ''] + -- + -- @ + -- forall (a :: 'I' x l r). + -- ('Succ' x l r) => + -- 'succ'' a == 'Just' ('succ' a) + -- @ + succ :: I x l r -> I x l r + +-- | 'Interval's where /division/ is known to be a closed operation. +class (Interval x l r) => Div (x :: Type) (l :: L x) (r :: R x) where + -- | @'div' a b@ divides @a@ by @b@. + -- + -- [Correspondence with 'div''] + -- + -- @ + -- forall (a :: 'I' x l r) (b :: 'I' x l r). + -- ('Div' x l r) => + -- 'div'' a b == 'Just' ('div' a b) + -- @ + div :: I x l r -> I x l r -> I x l r + + +-- | If an 'Interval' contains a /single/ 'inhabitant', obtain it. +single + :: forall x l r + . ( MinI x l r ~ MaxI x l r + , Known x l r (MinI x l r) ) + => I x l r +single = inhabitant +{-# INLINE single #-} + +-- | Proof that @t@ is __known__ to be within @l@ and @r@ in @'I' x l r@. +-- +-- __NB__: When defining 'Known' instances, instead of mentioning any +-- necessary constraints in the instance context, mention them them in +-- 'KnownCtx'. By doing so, when an instance of @'Known' x l r@ is +-- satisfied, @'KnownCtx' x l r@ is satisfied as well. If you don't do +-- this, 'with' won't behave as you would expect. +class + ( Interval x l r, KnownCtx x l r t + ) => Known (x :: Type) (l :: L x) (r :: R x) (t :: T x) where + -- | Constraints to be satisfied by @t@ if it is known to be within + -- the @'I' x l r@ interval. + type KnownCtx x l r t :: Constraint + type KnownCtx x l r t = () + -- | Obtain a term-level representation of @t@ as @'I' x l r@. + -- + -- Also consider using 'known', an alternative version of this function + -- designed to be used with @-XTypeApplications@. + known' :: Proxy t -> I x l r + +-- | Alternative version of 'known'', designed to be used with +-- @-XTypeApplications@. It works only when @x@ can be inferred by other means. +-- +-- @ +-- > :type 'known' +-- /'known' :: forall __{__x :: 'Type'__}__ (__t__ :: 'T' x) (__l__ :: 'L' x) (__r__ :: 'R' x). 'Known' x l r t => 'I' x l r/ +-- +-- > :type 'known' \@55 :: 'Known' 'Word8' l r 55 => 'I' 'Word8' l r +-- /'known' \@55 :: 'Known' 'Word8' l r 55 => 'I' 'Word8' l r/ +-- +-- > :type 'known' \@55 \@33 :: 'Known' 'Word8' 33 r 55 => 'I' 'Word8' 33 r +-- /'known' \@55 \@33 :: 'Known' 'Word8' 33 r 55 => 'I' 'Word8' 33 r/ +-- +-- > :type 'known' \@55 \@33 \@77 :: 'I' 'Word8' 33 77 +-- /'known' \@55 \@33 \@77 :: 'I' 'Word8' 33 77 :: 'I' 'Word8' 33 77/ +-- +-- > 'known' \@55 \@33 \@77 :: 'I' 'Word8' 33 77 +-- /55/ +-- @ +known :: forall {x} t l r. Known x l r t => I x l r +known = known' (Proxy @t) +{-# INLINE known #-} + +-- | Proof that @'I' x l r@ contains a value of type @x@ whose +-- type-level representation @t :: 'T' x@ satisfies a @'Known' x l r t@. + +-- TODO: The 'with' method belongs in the 'Interval' class, but I can't +-- get it to type-check, so it's here in this separate 'With' class. +class (Interval x l r) => With (x :: Type) (l :: L x) (r :: R x) where + -- | Bring to scope the type-level representation of @x@ as @t :: 'T' x@, + -- together with the constraints that prove that @t@ is 'Known' to be in the + -- interval @'I' x l r@. + -- + -- [Identity law] + -- + -- @ + -- x == 'with' x 'known'' + -- @ + with :: I x l r -> (forall (t :: T x). Known x l r t => Proxy t -> b) -> b + +-- | Wrap the given @x@ in the interval @'I' x ('MinL' x) ('MaxR' x)@. +-- +-- This function always succeeds because the interval known to fit all the +-- values of type @x@. +-- +-- [Identity law] +-- +-- @ +-- 'wrap' . 'unwrap' == 'id' +-- 'unwrap' . 'wrap' == 'id' +-- @ +-- +-- If the interval is not as big as @x@: +-- +-- * Consider using 'from'. +-- +-- * Consider using 'known' if you have type-level knowledge +-- about the value of @x@. +-- +-- * Consider using 'unsafe' if you know that the @x@ is within +-- the interval. +wrap :: Interval x (MinL x) (MaxR x) => x -> I x (MinL x) (MaxR x) +wrap = coerce +{-# INLINE wrap #-} + +-- | Obtain the @x@ that is wrapped in the @'I' x l r@. +-- +-- [Identity law] +-- +-- @ +-- 'wrap' . 'unwrap' == 'id' +-- 'unwrap' . 'wrap' == 'id' +-- @ +unwrap :: forall x l r. I x l r -> x +unwrap = coerce +{-# INLINE unwrap #-} + +-------------------------------------------------------------------------------- + +-- | Minimum value in the interval, if @'MinI' x@ is defined. +min :: forall x l r. Known x l r (MinI x l r) => I x l r +min = known @(MinI x l r) + +-- | Maximum value in the interval, if @'MaxI' x@ is defined. +max :: forall x l r. Known x l r (MaxI x l r) => I x l r +max = known @(MaxI x l r) + +instance + ( Known x l r (MinI x l r) + , Known x l r (MaxI x l r) + ) => Bounded (I x l r) where + minBound = min + maxBound = max + +-------------------------------------------------------------------------------- + +-- | Shove an @x@ into an interval @'I' x l r@, somehow. +-- +-- Note: This class is for testing purposes only. For example, if you want to +-- generate random values of type @'I' x l r@ for testing purposes, all you +-- have to do is generate random values of type @x@ and then 'shove' them into +-- @'I' x l r@. +-- +-- Note: We don't like this too much. If there was a good way to export +-- generators for Hedgehog or QuickCheck without depending on these libraries, +-- we'd probably export that instead. +class Interval x l r => Shove (x :: Type) (l :: L x) (r :: R x) where + -- | No guarantees are made about the @x@ value that ends up in @'I' x l r@. + -- In particular, you can't expect @'id' == 'unwrap' . 'shove'@, not even + -- for @x@ values for which @'from' == 'Just'@. All 'shove' guarantees is + -- a more or less uniform distribution. + shove :: x -> I x l r + +-------------------------------------------------------------------------------- + + +{- +TODO: I have no idea why, but if I move the T, L or R type instance +definitions to the I.Naturals module, it does not compile. +It leads to errors like the following all over the module. + + hs/I/Naturals.hs:108:41: error: + • Expected kind ‘Natural’, but ‘r’ has kind ‘R Word8’ + • In the second argument of ‘(<=)’, namely ‘r’ + In the type ‘(l <= 1, 1 <= r)’ + In the type instance declaration for ‘OneCtx’ + | + 108 | type OneCtx Word8 l r = (l <= 1, 1 <= r) + + +On the contrary, it doesn't seem necessary to define define MinT and MaxT +instances here. However, it's convenient, so we do it. +It's easier to only deal with the CPP stuff here, too. +-} + +type instance T Word8 = L.Natural +type instance L Word8 = L.Natural +type instance R Word8 = L.Natural +type instance MinT Word8 = 0 +type instance MaxT Word8 = 255 + +type instance T Word16 = L.Natural +type instance L Word16 = L.Natural +type instance R Word16 = L.Natural +type instance MinT Word16 = 0 +type instance MaxT Word16 = 65535 + +type instance T Word32 = L.Natural +type instance L Word32 = L.Natural +type instance R Word32 = L.Natural +type instance MinT Word32 = 0 +type instance MaxT Word32 = 4294967295 + +type instance T Word64 = L.Natural +type instance L Word64 = L.Natural +type instance R Word64 = L.Natural +type instance MinT Word64 = 0 +type instance MaxT Word64 = 18446744073709551615 + +type instance T Word = L.Natural +type instance L Word = L.Natural +type instance R Word = L.Natural +type instance MinT Word = 0 +type instance MaxT Word = (2 L.^ WORD_SIZE_IN_BITS) L.- 1 + +type instance T Int8 = KI.Integer +type instance L Int8 = KI.Integer +type instance R Int8 = KI.Integer +type instance MinT Int8 = KI.N 128 +type instance MaxT Int8 = KI.P 127 + +type instance T Int16 = KI.Integer +type instance L Int16 = KI.Integer +type instance R Int16 = KI.Integer +type instance MinT Int16 = KI.N 32768 +type instance MaxT Int16 = KI.P 32767 + +type instance T Int32 = KI.Integer +type instance L Int32 = KI.Integer +type instance R Int32 = KI.Integer +type instance MinT Int32 = KI.N 2147483648 +type instance MaxT Int32 = KI.P 2147483647 + +type instance T Int64 = KI.Integer +type instance L Int64 = KI.Integer +type instance R Int64 = KI.Integer +type instance MinT Int64 = KI.N 9223372036854775808 +type instance MaxT Int64 = KI.P 9223372036854775807 + +type instance T Int = KI.Integer +type instance L Int = KI.Integer +type instance R Int = KI.Integer +type instance MinT Int = KI.N (L.Div (2 L.^ WORD_SIZE_IN_BITS) 2) +type instance MaxT Int = KI.P (L.Div (2 L.^ WORD_SIZE_IN_BITS) 2 L.- 1) + +type instance T CChar = T HTYPE_CHAR +type instance L CChar = L HTYPE_CHAR +type instance R CChar = R HTYPE_CHAR +type instance MinT CChar = MinT HTYPE_CHAR +type instance MaxT CChar = MaxT HTYPE_CHAR + +type instance T CSize = T HTYPE_SIZE_T +type instance L CSize = L HTYPE_SIZE_T +type instance R CSize = R HTYPE_SIZE_T +type instance MinT CSize = MinT HTYPE_SIZE_T +type instance MaxT CSize = MaxT HTYPE_SIZE_T + +type instance T CClock = T HTYPE_CLOCK_T +type instance L CClock = L HTYPE_CLOCK_T +type instance R CClock = R HTYPE_CLOCK_T +type instance MinT CClock = MinT HTYPE_CLOCK_T +type instance MaxT CClock = MaxT HTYPE_CLOCK_T + +type instance T CInt = T HTYPE_INT +type instance L CInt = L HTYPE_INT +type instance R CInt = R HTYPE_INT +type instance MinT CInt = MinT HTYPE_INT +type instance MaxT CInt = MaxT HTYPE_INT + +type instance T CIntMax = T HTYPE_INTMAX_T +type instance L CIntMax = L HTYPE_INTMAX_T +type instance R CIntMax = R HTYPE_INTMAX_T +type instance MinT CIntMax = MinT HTYPE_INTMAX_T +type instance MaxT CIntMax = MaxT HTYPE_INTMAX_T + +type instance T CIntPtr = T HTYPE_INTPTR_T +type instance L CIntPtr = L HTYPE_INTPTR_T +type instance R CIntPtr = R HTYPE_INTPTR_T +type instance MinT CIntPtr = MinT HTYPE_INTPTR_T +type instance MaxT CIntPtr = MaxT HTYPE_INTPTR_T + +type instance T CLLong = T HTYPE_LONG_LONG +type instance L CLLong = L HTYPE_LONG_LONG +type instance R CLLong = R HTYPE_LONG_LONG +type instance MinT CLLong = MinT HTYPE_LONG_LONG +type instance MaxT CLLong = MaxT HTYPE_LONG_LONG + +type instance T CLong = T HTYPE_LONG +type instance L CLong = L HTYPE_LONG +type instance R CLong = R HTYPE_LONG +type instance MinT CLong = MinT HTYPE_LONG +type instance MaxT CLong = MaxT HTYPE_LONG + +type instance T CPtrdiff = T HTYPE_PTRDIFF_T +type instance L CPtrdiff = L HTYPE_PTRDIFF_T +type instance R CPtrdiff = R HTYPE_PTRDIFF_T +type instance MinT CPtrdiff = MinT HTYPE_PTRDIFF_T +type instance MaxT CPtrdiff = MaxT HTYPE_PTRDIFF_T + +type instance T CSChar = T HTYPE_SIGNED_CHAR +type instance L CSChar = L HTYPE_SIGNED_CHAR +type instance R CSChar = R HTYPE_SIGNED_CHAR +type instance MinT CSChar = MinT HTYPE_SIGNED_CHAR +type instance MaxT CSChar = MaxT HTYPE_SIGNED_CHAR + +type instance T CSUSeconds = T HTYPE_SUSECONDS_T +type instance L CSUSeconds = L HTYPE_SUSECONDS_T +type instance R CSUSeconds = R HTYPE_SUSECONDS_T +type instance MinT CSUSeconds = MinT HTYPE_SUSECONDS_T +type instance MaxT CSUSeconds = MaxT HTYPE_SUSECONDS_T + +type instance T CShort = T HTYPE_SHORT +type instance L CShort = L HTYPE_SHORT +type instance R CShort = R HTYPE_SHORT +type instance MinT CShort = MinT HTYPE_SHORT +type instance MaxT CShort = MaxT HTYPE_SHORT + +type instance T CTime = T HTYPE_TIME_T +type instance L CTime = L HTYPE_TIME_T +type instance R CTime = R HTYPE_TIME_T +type instance MinT CTime = MinT HTYPE_TIME_T +type instance MaxT CTime = MaxT HTYPE_TIME_T + +type instance T CUChar = T HTYPE_UNSIGNED_CHAR +type instance L CUChar = L HTYPE_UNSIGNED_CHAR +type instance R CUChar = R HTYPE_UNSIGNED_CHAR +type instance MinT CUChar = MinT HTYPE_UNSIGNED_CHAR +type instance MaxT CUChar = MaxT HTYPE_UNSIGNED_CHAR + +type instance T CUInt = T HTYPE_UNSIGNED_INT +type instance L CUInt = L HTYPE_UNSIGNED_INT +type instance R CUInt = R HTYPE_UNSIGNED_INT +type instance MinT CUInt = MinT HTYPE_UNSIGNED_INT +type instance MaxT CUInt = MaxT HTYPE_UNSIGNED_INT + +type instance T CUIntMax = T HTYPE_UINTMAX_T +type instance L CUIntMax = L HTYPE_UINTMAX_T +type instance R CUIntMax = R HTYPE_UINTMAX_T +type instance MinT CUIntMax = MinT HTYPE_UINTMAX_T +type instance MaxT CUIntMax = MaxT HTYPE_UINTMAX_T + +type instance T CUIntPtr = T HTYPE_UINTPTR_T +type instance L CUIntPtr = L HTYPE_UINTPTR_T +type instance R CUIntPtr = R HTYPE_UINTPTR_T +type instance MinT CUIntPtr = MinT HTYPE_UINTPTR_T +type instance MaxT CUIntPtr = MaxT HTYPE_UINTPTR_T + +type instance T CULLong = T HTYPE_UNSIGNED_LONG_LONG +type instance L CULLong = L HTYPE_UNSIGNED_LONG_LONG +type instance R CULLong = R HTYPE_UNSIGNED_LONG_LONG +type instance MinT CULLong = MinT HTYPE_UNSIGNED_LONG_LONG +type instance MaxT CULLong = MaxT HTYPE_UNSIGNED_LONG_LONG + +type instance T CULong = T HTYPE_UNSIGNED_LONG +type instance L CULong = L HTYPE_UNSIGNED_LONG +type instance R CULong = R HTYPE_UNSIGNED_LONG +type instance MinT CULong = MinT HTYPE_UNSIGNED_LONG +type instance MaxT CULong = MaxT HTYPE_UNSIGNED_LONG + +type instance T CUSeconds = T HTYPE_USECONDS_T +type instance L CUSeconds = L HTYPE_USECONDS_T +type instance R CUSeconds = R HTYPE_USECONDS_T +type instance MinT CUSeconds = MinT HTYPE_USECONDS_T +type instance MaxT CUSeconds = MaxT HTYPE_USECONDS_T + +type instance T CUShort = T HTYPE_UNSIGNED_SHORT +type instance L CUShort = L HTYPE_UNSIGNED_SHORT +type instance R CUShort = R HTYPE_UNSIGNED_SHORT +type instance MinT CUShort = MinT HTYPE_UNSIGNED_SHORT +type instance MaxT CUShort = MaxT HTYPE_UNSIGNED_SHORT + +type instance T CWchar = T HTYPE_WCHAR_T +type instance L CWchar = L HTYPE_WCHAR_T +type instance R CWchar = R HTYPE_WCHAR_T +type instance MinT CWchar = MinT HTYPE_WCHAR_T +type instance MaxT CWchar = MaxT HTYPE_WCHAR_T + +type instance T L.Natural = L.Natural +type instance L L.Natural = L.Natural +-- | ''Nothing' means /unbounded/. +type instance R L.Natural = Maybe L.Natural +type instance MinT L.Natural = 0 + +type instance T Integer = KI.Integer +-- | * ''Nothing' means /unbounded/. +-- +-- * @''Just' t@ means up to @t@, /inclusive/. +type instance L Integer = Maybe KI.Integer +-- | * ''Nothing' means /unbounded/. +-- +-- * @''Just' t@ means /up to @t@, inclusive/. +type instance R Integer = Maybe KI.Integer + +type instance T Rational = KR.Rational +-- | * ''Nothing' means /unbounded/. +-- +-- * @''Just (''True', t)@ means /up to @t@, inclusive/. +-- +-- * @''Just (''False', t)@ means /up to @t@, exclusive/. +type instance L Rational = Maybe (Bool, KR.Rational) +-- | * ''Nothing' means /unbounded/. +-- +-- * @''Just (''True', t)@ means /up to @t@, inclusive/. +-- +-- * @''Just (''False', t)@ means /up to @t@, exclusive/. +type instance R Rational = Maybe (Bool, KR.Rational) + diff --git a/hs/I/Natural.hs b/hs/I/Natural.hs new file mode 100644 --- /dev/null +++ b/hs/I/Natural.hs @@ -0,0 +1,200 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_HADDOCK not-home #-} + +module I.Natural () where + +import Control.Monad +import Data.Bits +import Data.Constraint +import Data.Maybe +import Data.Proxy +import Data.Type.Ord +import Numeric.Natural (Natural) +import GHC.TypeNats qualified as N +import KindInteger (type (/=)) +import Prelude hiding (min, max, div, succ) + +import I.Internal + +-------------------------------------------------------------------------------- + +type instance MinL Natural = MinT Natural +type instance MaxR Natural = 'Nothing + +-------------------------------------------------------------------------------- + +instance forall l r. + ( IntervalCtx Natural l ('Just r) + ) => Interval Natural l ('Just r) where + type IntervalCtx Natural l ('Just r) = + ( N.KnownNat l + , N.KnownNat r + , MinT Natural <= l + , l <= r ) + type MinI Natural l ('Just r) = l + type MaxI Natural l ('Just r) = r + inhabitant = min + from = \x -> unsafest x <$ guard (l <= x && x <= r) + where l = N.natVal (Proxy @l) + r = N.natVal (Proxy @r) + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from =<< toIntegralSized (toInteger (unwrap a) - + toInteger (unwrap b)) + a `div'` b = do guard (unwrap b /= 0) + (q, 0) <- pure $ divMod (unwrap a) (unwrap b) + from q + +instance forall l. + ( IntervalCtx Natural l 'Nothing + ) => Interval Natural l 'Nothing where + type IntervalCtx Natural l 'Nothing = (N.KnownNat l, MinT Natural <= l) + type MinI Natural l 'Nothing = l + inhabitant = min + from = \x -> unsafest x <$ guard (l <= x) + where l = N.natVal (Proxy @l) + a `plus'` b = pure (a `plus` b) + a `mult'` b = pure (a `mult` b) + a `minus'` b = from =<< toIntegralSized (toInteger (unwrap a) - + toInteger (unwrap b)) + a `div'` b = do guard (unwrap b /= 0) + (q, 0) <- pure $ divMod (unwrap a) (unwrap b) + from q + +-------------------------------------------------------------------------------- + +instance + ( Interval Natural l ('Just r) + ) => Clamp Natural l ('Just r) + +instance + ( Interval Natural l 'Nothing + ) => Clamp Natural l 'Nothing where + clamp = \case + x | x <= unwrap min_ -> min_ + | otherwise -> unsafe x + where min_ = min + +-------------------------------------------------------------------------------- + +instance + ( lu <= ld, rd <= ru + , Interval Natural ld ('Just rd) + , Interval Natural lu ('Just ru) ) + => Up Natural ld ('Just rd) lu ('Just ru) + +instance + ( lu <= ld + , Interval Natural ld yrd + , Interval Natural lu 'Nothing + ) => Up Natural ld yrd lu 'Nothing + +-------------------------------------------------------------------------------- + +instance forall l r t. + ( Interval Natural l ('Just r) + , KnownCtx Natural l ('Just r) t + ) => Known Natural l ('Just r) t where + type KnownCtx Natural l ('Just r) t = (N.KnownNat t, l <= t, t <= r) + known' = unsafe . N.natVal + +instance forall t l. + ( Interval Natural l 'Nothing + , KnownCtx Natural l 'Nothing t + ) => Known Natural l 'Nothing t where + type KnownCtx Natural l 'Nothing t = (N.KnownNat t, l <= t) + known' = unsafe . N.natVal + +-------------------------------------------------------------------------------- + +instance forall l r. + ( Interval Natural l ('Just r) + ) => With Natural l ('Just r) where + with x g = case N.someNatVal (unwrap x) of + N.SomeNat (pt :: Proxy t) -> + fromMaybe (error "I.with(Natural): impossible") $ do + Dict <- leNatural @l @t + Dict <- leNatural @t @r + pure (g pt) + +instance forall l. + ( Interval Natural l 'Nothing + ) => With Natural l 'Nothing where + with x g = case N.someNatVal (unwrap x) of + N.SomeNat (pt :: Proxy t) -> + fromMaybe (error "I.with(Natural): impossible") $ do + Dict <- leNatural @l @t + pure (g pt) + +-------------------------------------------------------------------------------- + +instance + ( Interval Natural l ('Just r), l /= r + ) => Discrete Natural l ('Just r) where + pred' i = unsafe (unwrap i - 1) <$ guard (min < i) + succ' i = unsafe (unwrap i + 1) <$ guard (i < max) + +instance + ( Interval Natural l 'Nothing + ) => Discrete Natural l 'Nothing where + pred' i = unsafe (unwrap i - 1) <$ guard (min < i) + succ' = pure . succ + +-------------------------------------------------------------------------------- + +instance + ( Interval Natural l 'Nothing + ) => Plus Natural l 'Nothing where + plus a b = unsafe (unwrap a + unwrap b) + +-------------------------------------------------------------------------------- + +instance + ( Interval Natural l 'Nothing + ) => Mult Natural l 'Nothing where + mult a b = unsafe (unwrap a * unwrap b) + +-------------------------------------------------------------------------------- + +instance + ( Discrete Natural l 'Nothing + ) => Succ Natural l 'Nothing where + succ i = unsafe (unwrap i + 1) + +-------------------------------------------------------------------------------- + +instance + ( Interval Natural 0 r + ) => Zero Natural 0 r where + zero = unsafe 0 + +-------------------------------------------------------------------------------- + +instance + ( Interval Natural l 'Nothing, l <= 1 + ) => One Natural l 'Nothing where + one = unsafe 1 + +instance + ( Interval Natural l ('Just r), l <= 1, 1 <= r + ) => One Natural l ('Just r) where + one = unsafe 1 + +-------------------------------------------------------------------------------- + +instance + ( Interval Natural l ('Just r) + ) => Shove Natural l ('Just r) where + shove = \x -> unsafe $ mod x (r - l + 1) + l + where l = unwrap (min @Natural @l @('Just r)) + r = unwrap (max @Natural @l @('Just r)) + +instance + ( Interval Natural l 'Nothing + ) => Shove Natural l 'Nothing where + shove = \x -> unsafe $ if x < l then l + (l - x) else x + where l = unwrap (min @Natural @l @'Nothing) + diff --git a/hs/I/Rational.hs b/hs/I/Rational.hs new file mode 100644 --- /dev/null +++ b/hs/I/Rational.hs @@ -0,0 +1,688 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_HADDOCK not-home #-} + +module I.Rational () where + +import Control.Monad +import Data.Constraint +import Data.Maybe +import Data.Proxy +import Data.Type.Ord +import GHC.TypeLits qualified as L +import GHC.Real +import KindRational (type (/)) +import KindRational qualified as KR +import Prelude hiding (min, max, div, succ, pred) +import Prelude qualified as P +import Unsafe.Coerce (unsafeCoerce) + +import I.Internal + +-------------------------------------------------------------------------------- + +type instance MinL P.Rational = 'Nothing +type instance MaxR P.Rational = 'Nothing + +instance forall l r. + ( IntervalCtx P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + ) => Interval P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where + type IntervalCtx P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) = + (KR.KnownRational l, KR.KnownRational r, l <= r) + type MinI P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) = l + type MaxI P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) = r + inhabitant = min + from = \x -> unsafest x <$ guard (l <= x && x <= r) + where l = KR.rationalVal (Proxy @l) + r = KR.rationalVal (Proxy @r) + negate' = from . P.negate . unwrap + recip' x = case unwrap x of n :% d -> from (d :% n) + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + from (unwrap a / unwrap b) + +instance forall l r. + ( IntervalCtx P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) + ) => Interval P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where + type IntervalCtx P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) = + (KR.KnownRational l, KR.KnownRational r, l < r) + type MinI P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) = l + inhabitant = min + from = \x -> unsafest x <$ guard (l <= x && x < r) + where l = KR.rationalVal (Proxy @l) + r = KR.rationalVal (Proxy @r) + negate' = from . P.negate . unwrap + recip' x = case unwrap x of n :% d -> from (d :% n) + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + from (unwrap a / unwrap b) + +instance forall l. + ( IntervalCtx P.Rational ('Just '( 'True, l)) 'Nothing + ) => Interval P.Rational ('Just '( 'True, l)) 'Nothing where + type IntervalCtx P.Rational ('Just '( 'True, l)) 'Nothing = KR.KnownRational l + type MinI P.Rational ('Just '( 'True, l)) 'Nothing = l + inhabitant = min + from = \x -> unsafest x <$ guard (l <= x) + where l = KR.rationalVal (Proxy @l) + negate' = from . P.negate . unwrap + recip' x = case unwrap x of n :% d -> from (d :% n) + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + from (unwrap a / unwrap b) + + +instance forall l r. + ( IntervalCtx P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) + ) => Interval P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where + type IntervalCtx P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) = + (KR.KnownRational l, KR.KnownRational r, l < r) + type MaxI P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) = r + inhabitant = max + from = \x -> unsafest x <$ guard (l < x && x <= r) + where l = KR.rationalVal (Proxy @l) + r = KR.rationalVal (Proxy @r) + negate' = from . P.negate . unwrap + recip' x = case unwrap x of n :% d -> from (d :% n) + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + from (unwrap a / unwrap b) + +instance forall r. + ( IntervalCtx P.Rational 'Nothing ('Just '( 'True, r)) + ) => Interval P.Rational 'Nothing ('Just '( 'True, r)) where + type IntervalCtx P.Rational 'Nothing ('Just '( 'True, r)) = KR.KnownRational r + type MaxI P.Rational 'Nothing ('Just '( 'True, r)) = r + inhabitant = max + from = \x -> unsafest x <$ guard (x <= r) + where r = KR.rationalVal (Proxy @r) + negate' = from . P.negate . unwrap + recip' x = case unwrap x of n :% d -> from (d :% n) + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + from (unwrap a / unwrap b) + +instance forall l r. + ( IntervalCtx P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) + ) => Interval P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where + type IntervalCtx P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) = + (KR.KnownRational l, KR.KnownRational r, l < r) + inhabitant = -- halfway between l and r + let l' = KR.rationalVal (Proxy @l) + r' = KR.rationalVal (Proxy @r) + in unsafe (l' + (r' - l') / 2) + from = \x -> unsafest x <$ guard (l < x && x < r) + where l = KR.rationalVal (Proxy @l) + r = KR.rationalVal (Proxy @r) + negate' = from . P.negate . unwrap + recip' x = case unwrap x of n :% d -> from (d :% n) + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + from (unwrap a / unwrap b) + +instance forall r. + ( IntervalCtx P.Rational 'Nothing ('Just '( 'False, r)) + ) => Interval P.Rational 'Nothing ('Just '( 'False, r)) where + type IntervalCtx P.Rational 'Nothing ('Just '( 'False, r)) = + KR.KnownRational r + inhabitant = unsafe (KR.rationalVal (Proxy @r) - 1) + from = \x -> unsafest x <$ guard (x < r) + where r = KR.rationalVal (Proxy @r) + negate' = from . P.negate . unwrap + recip' x = case unwrap x of n :% d -> from (d :% n) + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + from (unwrap a / unwrap b) + +instance forall l. + ( IntervalCtx P.Rational ('Just '( 'False, l)) 'Nothing + ) => Interval P.Rational ('Just '( 'False, l)) 'Nothing where + type IntervalCtx P.Rational ('Just '( 'False, l)) 'Nothing = + KR.KnownRational l + inhabitant = unsafe (KR.rationalVal (Proxy @l) + 1) + from = \x -> unsafest x <$ guard (l < x) + where l = KR.rationalVal (Proxy @l) + negate' = from . P.negate . unwrap + recip' x = case unwrap x of n :% d -> from (d :% n) + a `plus'` b = from (unwrap a + unwrap b) + a `mult'` b = from (unwrap a * unwrap b) + a `minus'` b = from (unwrap a - unwrap b) + a `div'` b = do guard (unwrap b /= 0) + from (unwrap a / unwrap b) + +instance Interval P.Rational 'Nothing 'Nothing where + inhabitant = zero + from = pure . wrap + negate' = pure . wrap . P.negate . unwrap + recip' x = case unwrap x of n :% d -> from (d :% n) + a `plus'` b = pure (a `plus` b) + a `mult'` b = pure (a `mult` b) + a `minus'` b = pure (a `minus` b) + a `div'` b = do guard (unwrap b /= 0) + pure (wrap (unwrap a / unwrap b)) + +-------------------------------------------------------------------------------- + +instance (Interval Rational ('Just '( 'True, l)) ('Just '( 'True, r))) + => Clamp Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + +instance (Interval Rational ('Just '( 'True, l)) 'Nothing) + => Clamp Rational ('Just '( 'True, l)) 'Nothing where + clamp = \case + x | x <= unwrap min_ -> min_ + | otherwise -> unsafe x + where min_ = min + +instance (Interval Rational 'Nothing ('Just '( 'True, r))) + => Clamp Rational 'Nothing ('Just '( 'True, r)) where + clamp = \case + x | x >= unwrap max_ -> max_ + | otherwise -> unsafe x + where max_ = max + +instance (Interval Rational 'Nothing 'Nothing) + => Clamp Rational 'Nothing 'Nothing where + clamp = unsafe + +-------------------------------------------------------------------------------- + +-- OO +instance + ( Interval Rational ('Just '( 'False, ld)) ('Just '( 'False, rd)) + , Interval Rational ('Just '( 'False, lu)) ('Just '( 'False, ru)) + , lu <= ld + , rd <= ru ) + => Up Rational ('Just '( 'False, ld)) ('Just '( 'False, rd)) + ('Just '( 'False, lu)) ('Just '( 'False, ru)) + +-- OC +instance + ( Interval Rational ('Just '( 'False, ld)) ('Just '( ird , rd)) + , Interval Rational ('Just '( 'False, lu)) ('Just '( 'True, ru)) + , lu <= ld + , rd <= ru ) + => Up Rational ('Just '( 'False, ld)) ('Just '( ird , rd)) + ('Just '( 'False, lu)) ('Just '( 'True, ru)) + +-- OU +instance + ( Interval Rational ('Just '( 'False, ld)) yrd + , Interval Rational ('Just '( 'False, lu)) 'Nothing + , lu <= ld ) + => Up Rational ('Just '( 'False, ld)) yrd + ('Just '( 'False, lu)) 'Nothing + +-- CO +instance + ( Interval Rational ('Just '( ild , ld)) ('Just '( 'False, rd)) + , Interval Rational ('Just '( 'True, lu)) ('Just '( 'False, ru)) + , lu <= ld + , rd <= ru ) + => Up Rational ('Just '( ild , ld)) ('Just '( 'False, rd)) + ('Just '( 'True, lu)) ('Just '( 'False, ru)) + +-- CC +instance + ( Interval Rational ('Just '( ild , ld)) ('Just '( ird , rd)) + , Interval Rational ('Just '( 'True, lu)) ('Just '( 'True, ru)) + , lu <= ld + , rd <= ru ) + => Up Rational ('Just '( ild , ld)) ('Just '( ird , rd)) + ('Just '( 'True, lu)) ('Just '( 'True, ru)) + +-- CU +instance + ( Interval Rational ('Just '( ild , ld)) yrd + , Interval Rational ('Just '( 'True, lu)) 'Nothing + , lu <= ld ) + => Up Rational ('Just '( ild , ld)) yrd + ('Just '( 'True, lu)) 'Nothing + +-- UO +instance + ( Interval Rational yld ('Just '( 'False, rd)) + , Interval Rational 'Nothing ('Just '( 'False, ru)) + , ru <= rd ) + => Up Rational yld ('Just '( 'False, rd)) + 'Nothing ('Just '( 'False, ru)) + +-- UC +instance + ( Interval Rational yld ('Just '( ird , rd)) + , Interval Rational 'Nothing ('Just '( 'True, ru)) + , ru <= rd ) + => Up Rational yld ('Just '( ird , rd)) + 'Nothing ('Just '( 'True, ru)) + +-- UU +instance + ( Interval Rational yld yrd + , Interval Rational 'Nothing 'Nothing ) + => Up Rational yld yrd + 'Nothing 'Nothing + +-------------------------------------------------------------------------------- + + +instance forall t l r. + ( Interval P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + , KnownCtx P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) t + ) => Known P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) t where + type KnownCtx P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) t = + (KR.KnownRational t, l <= t, t <= r) + known' = unsafe . KR.rationalVal + +instance forall t l r. + ( Interval P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) + , KnownCtx P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) t + ) => Known P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) t where + type KnownCtx P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) t = + (KR.KnownRational t, l <= t, t < r) + known' = unsafe . KR.rationalVal + +instance forall t l. + ( Interval P.Rational ('Just '( 'True, l)) 'Nothing + , KnownCtx P.Rational ('Just '( 'True, l)) 'Nothing t + ) => Known P.Rational ('Just '( 'True, l)) 'Nothing t where + type KnownCtx P.Rational ('Just '( 'True, l)) 'Nothing t = + (KR.KnownRational t, l <= t) + known' = unsafe . KR.rationalVal + +instance forall t l r. + ( Interval P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) + , KnownCtx P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) t + ) => Known P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) t where + type KnownCtx P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) t = + (KR.KnownRational t, l < t, t <= r) + known' = unsafe . KR.rationalVal + +instance forall t l. + ( Interval P.Rational ('Just '( 'False, l)) 'Nothing + , KnownCtx P.Rational ('Just '( 'False, l)) 'Nothing t + ) => Known P.Rational ('Just '( 'False, l)) 'Nothing t where + type KnownCtx P.Rational ('Just '( 'False, l)) 'Nothing t = + (KR.KnownRational t, l < t) + known' = unsafe . KR.rationalVal + +instance forall t r. + ( Interval P.Rational 'Nothing ('Just '( 'True, r)) + , KnownCtx P.Rational 'Nothing ('Just '( 'True, r)) t + ) => Known P.Rational 'Nothing ('Just '( 'True, r)) t where + type KnownCtx P.Rational 'Nothing ('Just '( 'True, r)) t = + (KR.KnownRational t, t <= r) + known' = unsafe . KR.rationalVal + +instance forall t r. + ( Interval P.Rational 'Nothing ('Just '( 'False, r)) + , KnownCtx P.Rational 'Nothing ('Just '( 'False, r)) t + ) => Known P.Rational 'Nothing ('Just '( 'False, r)) t where + type KnownCtx P.Rational 'Nothing ('Just '( 'False, r)) t = + (KR.KnownRational t, t < r) + known' = unsafe . KR.rationalVal + +instance forall t l r. + ( Interval P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) + , KnownCtx P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) t + ) => Known P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) t where + type KnownCtx P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) t = + (KR.KnownRational t, l < t, t < r) + known' = unsafe . KR.rationalVal + +instance forall t. + ( KnownCtx P.Rational 'Nothing 'Nothing t + ) => Known P.Rational 'Nothing 'Nothing t where + type KnownCtx P.Rational 'Nothing 'Nothing t = KR.KnownRational t + known' = unsafe . KR.rationalVal + +-------------------------------------------------------------------------------- + +instance forall l r. + ( Interval P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + ) => With P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where + with x g = case KR.someRationalVal (unwrap x) of + KR.SomeRational (pt :: Proxy t) -> + fromMaybe (error "I.with(Rational): impossible") $ do + Dict <- le @l @t + Dict <- le @t @r + pure (g pt) + +instance forall l r. + ( Interval P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) + ) => With P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where + with x g = case KR.someRationalVal (unwrap x) of + KR.SomeRational (pt :: Proxy t) -> + fromMaybe (error "I.with(Rational): impossible") $ do + Dict <- le @l @t + Dict <- lt @t @r + pure (g pt) + +instance forall l. + ( Interval P.Rational ('Just '( 'True, l)) 'Nothing + ) => With P.Rational ('Just '( 'True, l)) 'Nothing where + with x g = case KR.someRationalVal (unwrap x) of + KR.SomeRational (pt :: Proxy t) -> + fromMaybe (error "I.with(Rational): impossible") $ do + Dict <- le @l @t + pure (g pt) + +instance forall l. + ( Interval P.Rational ('Just '( 'False, l)) 'Nothing + ) => With P.Rational ('Just '( 'False, l)) 'Nothing where + with x g = case KR.someRationalVal (unwrap x) of + KR.SomeRational (pt :: Proxy t) -> + fromMaybe (error "I.with(Rational): impossible") $ do + Dict <- lt @l @t + pure (g pt) + +instance forall l r. + ( Interval P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) + ) => With P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where + with x g = case KR.someRationalVal (unwrap x) of + KR.SomeRational (pt :: Proxy t) -> + fromMaybe (error "I.with(Rational): impossible") $ do + Dict <- lt @l @t + Dict <- le @t @r + pure (g pt) + +instance forall r. + ( Interval P.Rational 'Nothing ('Just '( 'True, r)) + ) => With P.Rational 'Nothing ('Just '( 'True, r)) where + with x g = case KR.someRationalVal (unwrap x) of + KR.SomeRational (pt :: Proxy t) -> + fromMaybe (error "I.with(Rational): impossible") $ do + Dict <- le @t @r + pure (g pt) + +instance forall l r. + ( Interval P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) + ) => With P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where + with x g = case KR.someRationalVal (unwrap x) of + KR.SomeRational (pt :: Proxy t) -> + fromMaybe (error "I.with(Rational): impossible") $ do + Dict <- lt @l @t + Dict <- lt @t @r + pure (g pt) + +instance forall r. + ( Interval P.Rational 'Nothing ('Just '( 'False, r)) + ) => With P.Rational 'Nothing ('Just '( 'False, r)) where + with x g = case KR.someRationalVal (unwrap x) of + KR.SomeRational (pt :: Proxy t) -> + fromMaybe (error "I.with(Rational): impossible") $ do + Dict <- lt @t @r + pure (g pt) + +instance With P.Rational 'Nothing 'Nothing where + with x g = case KR.someRationalVal (unwrap x) of + KR.SomeRational (pt :: Proxy t) -> g pt + +-------------------------------------------------------------------------------- + +instance + ( Interval P.Rational ('Just '(il, l)) 'Nothing, 0/1 <= l + ) => Plus P.Rational ('Just '(il, l)) 'Nothing where + a `plus` b = unsafe (unwrap a + unwrap b) + +instance + ( Interval P.Rational 'Nothing ('Just '(ir, r)), r <= 0/1 + ) => Plus P.Rational 'Nothing ('Just '(ir, r)) where + a `plus` b = unsafe (unwrap a + unwrap b) + +instance Plus P.Rational 'Nothing 'Nothing where + a `plus` b = unsafe (unwrap a + unwrap b) + +-------------------------------------------------------------------------------- + +instance + ( Interval P.Rational ('Just '(il, l)) 'Nothing, 1/1 <= l + ) => Mult P.Rational ('Just '(il, l)) 'Nothing where + a `mult` b = unsafe (unwrap a * unwrap b) + +instance + ( Interval P.Rational ('Just '(il, l)) ('Just '(ir, r)), 0/1 <= l, r <= 1/1 + ) => Mult P.Rational ('Just '(il, l)) ('Just '(ir, r)) where + a `mult` b = unsafe (unwrap a * unwrap b) + +instance Mult P.Rational 'Nothing 'Nothing where + a `mult` b = unsafe (unwrap a * unwrap b) + +-------------------------------------------------------------------------------- + +instance + ( 0/1 < l, r <= 1/1 + , Interval P.Rational ('Just '(il, l)) ('Just '(ir, r)) + ) => Div P.Rational ('Just '(il, l)) ('Just '(ir, r)) where + a `div` b = unsafe (unwrap a / unwrap b) + +-------------------------------------------------------------------------------- + +instance Minus P.Rational 'Nothing 'Nothing where + a `minus` b = unsafe (unwrap a - unwrap b) + +-------------------------------------------------------------------------------- + +instance + ( l <= 0/1, 0/1 <= r + , Interval P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + ) => Zero P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where + zero = unsafe 0 + +instance + ( l <= 0/1, 0/1 < r + , Interval P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) + ) => Zero P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where + zero = unsafe 0 + +instance + ( l < 0/1, 0/1 <= r + , Interval P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) + ) => Zero P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where + zero = unsafe 0 + +instance + ( Interval P.Rational ('Just '( 'True, l)) 'Nothing, l <= 0/1 + ) => Zero P.Rational ('Just '( 'True, l)) 'Nothing where + zero = unsafe 0 + +instance + ( Interval P.Rational ('Just '( 'False, l)) 'Nothing, l < 0/1 + ) => Zero P.Rational ('Just '( 'False, l)) 'Nothing where + zero = unsafe 0 + +instance + ( Interval P.Rational 'Nothing ('Just '( 'True, r)), 0/1 <= r + ) => Zero P.Rational 'Nothing ('Just '( 'True, r)) where + zero = unsafe 0 + +instance + ( Interval P.Rational 'Nothing ('Just '( 'False, r)), 0/1 < r + ) => Zero P.Rational 'Nothing ('Just '( 'False, r)) where + zero = unsafe 0 + +instance + ( l < 0/1, 0/1 < r + , Interval P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) + ) => Zero P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where + zero = unsafe 0 + +instance Zero P.Rational 'Nothing 'Nothing where + zero = unsafe 0 + +-------------------------------------------------------------------------------- + +instance + ( l <= 1/1, 1/1 <= r + , Interval P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + ) => One P.Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where + one = unsafe 1 + +instance + ( l <= 1/1, 1/1 < r + , Interval P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) + ) => One P.Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where + one = unsafe 1 + +instance + ( l < 1/1, 1/1 <= r + , Interval P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) + ) => One P.Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where + one = unsafe 1 + +instance + ( Interval P.Rational ('Just '( 'True, l)) 'Nothing, l <= 1/1 + ) => One P.Rational ('Just '( 'True, l)) 'Nothing where + one = unsafe 1 + +instance + ( Interval P.Rational ('Just '( 'False, l)) 'Nothing, l < 1/1 + ) => One P.Rational ('Just '( 'False, l)) 'Nothing where + one = unsafe 1 + +instance + ( Interval P.Rational 'Nothing ('Just '( 'True, r)), 1/1 <= r + ) => One P.Rational 'Nothing ('Just '( 'True, r)) where + one = unsafe 1 + +instance + ( Interval P.Rational 'Nothing ('Just '( 'False, r)), 1/1 < r + ) => One P.Rational 'Nothing ('Just '( 'False, r)) where + one = unsafe 1 + +instance + ( l < 1/1, 1/1 < r + , Interval P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) + ) => One P.Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where + one = unsafe 1 + +instance One P.Rational 'Nothing 'Nothing where + one = unsafe 1 + +-------------------------------------------------------------------------------- + +instance + ( l KR.== KR.Negate r + , Zero P.Rational ('Just '(i, l)) ('Just '(i, r)) + ) => Negate P.Rational ('Just '(i, l)) ('Just '(i, r)) where + negate = unsafe . P.negate . unwrap + +instance Negate P.Rational 'Nothing 'Nothing where + negate = unsafe . P.negate . unwrap + +-------------------------------------------------------------------------------- + +instance + ( Interval Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + ) => Shove Rational ('Just '( 'True, l)) ('Just '( 'True, r)) where + shove | d == 0 = \_ -> min + | otherwise = \x -> + let t = P.min (abs (numerator x)) (abs (denominator x)) + % P.max (abs (numerator x)) (abs (denominator x)) + in unsafe $ if x < 0 then r - d * t else l + d * t + where + l = KR.rationalVal (Proxy @l) + r = KR.rationalVal (Proxy @r) + d = r - l + +instance + ( Interval Rational ('Just '( 'True, l)) ('Just '( 'False, r)) + ) => Shove Rational ('Just '( 'True, l)) ('Just '( 'False, r)) where + shove = \x -> let t = P.min (abs (numerator x)) (abs (denominator x)) + % P.max (abs (numerator x)) (abs (denominator x)) + in unsafe $ if x < 0 then r1 - d1 * t else l0 + d1 * t + where + l0 = KR.rationalVal (Proxy @l) + r0 = KR.rationalVal (Proxy @r) + d0 = r0 - l0 + p0 = d0 / 1000 + r1 = r0 - p0 + d1 = r1 - l0 + +instance Interval Rational ('Just '( 'True, l)) 'Nothing + => Shove Rational ('Just '( 'True, l)) 'Nothing where + shove = \x -> unsafe (if l <= x then x else l + (l - x)) + where l = KR.rationalVal (Proxy @l) + +instance + ( Interval Rational ('Just '( 'False, l)) ('Just '( 'True, r)) + ) => Shove Rational ('Just '( 'False, l)) ('Just '( 'True, r)) where + shove = \x -> let t = P.min (abs (numerator x)) (abs (denominator x)) + % P.max (abs (numerator x)) (abs (denominator x)) + in unsafe $ if x < 0 then r0 - d1 * t else l1 + d1 * t + where + l0 = KR.rationalVal (Proxy @l) + r0 = KR.rationalVal (Proxy @r) + d0 = r0 - l0 + p0 = d0 / 1000 + l1 = l0 + p0 + d1 = r0 - l1 + +instance + ( Interval Rational ('Just '( 'False, l)) ('Just '( 'False, r)) + ) => Shove Rational ('Just '( 'False, l)) ('Just '( 'False, r)) where + shove = \x -> let t = P.min (abs (numerator x)) (abs (denominator x)) + % P.max (abs (numerator x)) (abs (denominator x)) + in unsafe $ if x <= 0 then r1 - d1 * t else l1 + d1 * t + where + l0 = KR.rationalVal (Proxy @l) + r0 = KR.rationalVal (Proxy @r) + d0 = r0 - l0 + p0 = d0 / 1000 + l1 = l0 + p0 + r1 = r0 - p0 + d1 = r1 - l1 + +instance + ( Interval Rational ('Just '( 'False, l)) 'Nothing + ) => Shove Rational ('Just '( 'False, l)) 'Nothing where + shove = \x -> unsafe $ if x <= l then l + (l - x) + 1 else x + where l = KR.rationalVal (Proxy @l) + +instance + ( Interval Rational 'Nothing ('Just '( 'True, r)) + ) => Shove Rational 'Nothing ('Just '( 'True, r)) where + shove = \x -> unsafe $ if r < x then r - (x - r) else x + where r = KR.rationalVal (Proxy @r) + +instance + ( Interval Rational 'Nothing ('Just '( 'False, r)) + ) => Shove Rational 'Nothing ('Just '( 'False, r)) where + shove = \x -> unsafe $ if r <= x then r - (x - r) - 1 else x + where r = KR.rationalVal (Proxy @r) + +instance Shove Rational 'Nothing 'Nothing where + shove = unsafe + +-------------------------------------------------------------------------------- + +lt :: forall (a :: KR.Rational) (b :: KR.Rational) + . (KR.KnownRational a, KR.KnownRational b) + => Maybe (Dict (a < b)) +lt = case KR.cmpRational (Proxy @a) (Proxy @b) of + L.LTI -> Just $ unsafeCoerce (Dict @()) + L.EQI -> Nothing + L.GTI -> Nothing + +le :: forall (a :: KR.Rational) (b :: KR.Rational) + . (KR.KnownRational a, KR.KnownRational b) + => Maybe (Dict (a <= b)) +le = case KR.cmpRational (Proxy @a) (Proxy @b) of + L.LTI -> Just $ unsafeCoerce (Dict @()) + L.EQI -> Just $ unsafeCoerce (Dict @()) + L.GTI -> Nothing + diff --git a/hs/I/Word8.hs b/hs/I/Word8.hs new file mode 100644 --- /dev/null +++ b/hs/I/Word8.hs @@ -0,0 +1,98 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_HADDOCK not-home #-} + +module I.Word8 () where + +import Control.Monad +import Data.Constraint +import Data.Maybe +import Data.Proxy +import Data.Word +import Data.Type.Ord +import Foreign.C.Types +import GHC.TypeLits qualified as L +import KindInteger (type (/=)) +import Prelude hiding (min, max, div) + +import I.Internal + +-------------------------------------------------------------------------------- + +-- | This is so that GHC doesn't complain about the unused modules, +-- which we import here so that `genmodules.sh` doesn't have to add it +-- to the generated modules. +_ignore :: (CSize, Word) +_ignore = (0, 0) + +-------------------------------------------------------------------------------- + + +type instance MinL Word8 = MinT Word8 +type instance MaxR Word8 = MaxT Word8 + +instance forall l r. + ( IntervalCtx Word8 l r + ) => Interval Word8 l r where + type IntervalCtx Word8 l r = + ( L.KnownNat l + , L.KnownNat r + , MinT Word8 <= l + , l <= r + , r <= MaxT Word8 ) + type MinI Word8 l r = l + type MaxI Word8 l r = r + inhabitant = min + from = \x -> unsafest x <$ guard (l <= x && x <= r) + where l = fromInteger (L.natVal (Proxy @l)) :: Word8 + r = fromInteger (L.natVal (Proxy @r)) :: Word8 + (unwrap -> a) `plus'` (unwrap -> b) = do + guard (b <= maxBound - a) + from (a + b) + (unwrap -> a) `mult'` (unwrap -> b) = do + guard (b == 0 || a <= maxBound `quot` b) + from (a * b) + (unwrap -> a) `minus'` (unwrap -> b) = do + guard (b <= a) + from (a - b) + (unwrap -> a) `div'` (unwrap -> b) = do + guard (b /= 0) + let (q, m) = divMod a b + guard (m == 0) + from q + +instance (Interval Word8 l r) => Clamp Word8 l r + +instance (Interval Word8 ld rd, Interval Word8 lu ru, lu <= ld, rd <= ru) + => Up Word8 ld rd lu ru + +instance forall l r t. + ( Interval Word8 l r, KnownCtx Word8 l r t + ) => Known Word8 l r t where + type KnownCtx Word8 l r t = (L.KnownNat t, l <= t, t <= r) + known' = unsafe . fromInteger . L.natVal + +instance forall l r. (Interval Word8 l r) => With Word8 l r where + with x g = fromMaybe (error "I.with: impossible") $ do + L.SomeNat (pt :: Proxy t) <- L.someNatVal (toInteger (unwrap x)) + Dict <- leNatural @l @t + Dict <- leNatural @t @r + pure (g pt) + +instance (Interval Word8 l r, l /= r) => Discrete Word8 l r where + pred' i = unsafe (unwrap i - 1) <$ guard (min < i) + succ' i = unsafe (unwrap i + 1) <$ guard (i < max) + +instance (Interval Word8 0 r) => Zero Word8 0 r where + zero = unsafe 0 + +instance (Interval Word8 l r, l <= 1, 1 <= r) => One Word8 l r where + one = unsafe 1 + +instance forall l r. (Interval Word8 l r) => Shove Word8 l r where + shove = \x -> unsafe $ fromInteger (mod (toInteger x) (r - l + 1) + l) + where l = toInteger (unwrap (min @Word8 @l @r)) + r = toInteger (unwrap (max @Word8 @l @r)) + diff --git a/i.cabal b/i.cabal new file mode 100644 --- /dev/null +++ b/i.cabal @@ -0,0 +1,130 @@ +cabal-version: 2.4 +name: i +version: 0.1 +license: Apache-2.0 +license-file: LICENSE +extra-source-files: README.md CHANGELOG.md +author: Renzo Carbonara +maintainer: renλren.zone +copyright: Copyright (c) Renzo Carbonara 2023 +category: Numbers +build-type: Custom +synopsis: Haskell interval types. Bounds checking. +description: Haskell interval types. Bounds checking. +homepage: https://github.com/k0001/hs-i +bug-reports: https://github.com/k0001/hs-i/issues +tested-with: GHC ==9.4.3 + +common basic + default-language: GHC2021 + ghc-options: -O2 -Wall + build-depends: base ==4.* + default-extensions: + DataKinds + DefaultSignatures + DerivingStrategies + GeneralizedNewtypeDeriving + LambdaCase + MultiWayIf + RoleAnnotations + TypeFamilies + ViewPatterns + +custom-setup + setup-depends: + base ==4.*, + directory, + Cabal ==3.*, + +library + import: basic + hs-source-dirs: hs + build-depends: + constraints, + kind-integer, + kind-rational, + exposed-modules: I + other-modules: + I.Int8 + I.Integer + I.Internal + I.Natural + I.Rational + I.Word8 + I.Autogen.CChar + I.Autogen.CInt + I.Autogen.CIntMax + I.Autogen.CIntPtr + I.Autogen.CLLong + I.Autogen.CLong + I.Autogen.CPtrdiff + I.Autogen.CSChar + I.Autogen.CShort + I.Autogen.CSize + I.Autogen.CUChar + I.Autogen.CUInt + I.Autogen.CUIntMax + I.Autogen.CUIntPtr + I.Autogen.CULLong + I.Autogen.CULong + I.Autogen.CUShort + I.Autogen.CWchar + I.Autogen.Int + I.Autogen.Int16 + I.Autogen.Int32 + I.Autogen.Int64 + I.Autogen.Word + I.Autogen.Word16 + I.Autogen.Word32 + I.Autogen.Word64 + autogen-modules: + I.Autogen.CChar + I.Autogen.CInt + I.Autogen.CIntMax + I.Autogen.CIntPtr + I.Autogen.CLLong + I.Autogen.CLong + I.Autogen.CPtrdiff + I.Autogen.CSChar + I.Autogen.CShort + I.Autogen.CSize + I.Autogen.CUChar + I.Autogen.CUInt + I.Autogen.CUIntMax + I.Autogen.CUIntPtr + I.Autogen.CULLong + I.Autogen.CULong + I.Autogen.CUShort + I.Autogen.CWchar + I.Autogen.Int + I.Autogen.Int16 + I.Autogen.Int32 + I.Autogen.Int64 + I.Autogen.Word + I.Autogen.Word16 + I.Autogen.Word32 + I.Autogen.Word64 + +test-suite test + import: basic + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: I/Test/Main.hs + ghc-options: -threaded -with-rtsopts=-N -main-is I.Test.Main.main + other-modules: + I.Test.Int8 + I.Test.Integer + I.Test.Natural + I.Test.Rational + I.Test.Support + I.Test.Word8 + build-depends: + i, + constraints, + hedgehog, + kind-integer, + kind-rational, + tasty, + tasty-hedgehog, + tasty-hunit, + diff --git a/test/I/Test/Int8.hs b/test/I/Test/Int8.hs new file mode 100644 --- /dev/null +++ b/test/I/Test/Int8.hs @@ -0,0 +1,194 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} + +module I.Test.Int8 (tt) where + +import Control.Monad +import Data.Bits +import Data.Constraint +import Data.Int +import Data.Proxy +import Data.Type.Ord +import Hedgehog (failure, forAll, property, assert, (===), (/==)) +import Hedgehog.Gen qualified as Gen +import KindInteger (N, P) +import KindInteger qualified as KI +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@=?)) +import Test.Tasty.Hedgehog (testProperty) + +import I (I) +import I qualified + +import I.Test.Support + +-------------------------------------------------------------------------------- + +-- checking some constants used below +_tt :: Dict (I.MinL Int8 ~ N 128, I.MaxR Int8 ~ P 127) +_tt = Dict + +tt :: TestTree +tt = testGroup "Int8" + [ testProperty "wrap" $ property $ do + x <- forAll genInt8 + x === I.unwrap (I.wrap x) + + , tt' @(N 128) @(P 127) -- full range + + , tt' @(N 1) @(N 1) + , tt' @(N 1) @(P 0) + , tt' @(P 0) @(P 0) + , tt' @(P 0) @(P 1) + , tt' @(P 1) @(P 1) + + , tt' @(N 128) @(N 128) -- left end + , tt' @(P 127) @(P 127) -- right end + + , tt' @(N 128) @(N 100) -- partial on the left, some negatives + , tt' @(N 128) @(N 1) -- partial on the left, all negatives + , tt' @(N 128) @(N 0) -- partial on the left, all negatives and zero + , tt' @(N 128) @(P 50) -- partial on the left, negative and positive + + , tt' @(P 100) @(P 127) -- partial on the right, some positives + , tt' @(P 1) @(P 127) -- partial on the right, all positives + , tt' @(P 0) @(P 127) -- partial on the right, all positives and zero + , tt' @(N 50) @(P 127) -- partial on the right, negative and positive + + , tt' @(N 100) @(N 1) -- partial on the center, negatives + , tt' @(N 100) @(N 0) -- partial on the center, negatives and zero + , tt' @(P 1) @(P 100) -- partial on the center, positives + , tt' @(N 0) @(P 100) -- partial on the center, positives and zero + , tt' @(N 100) @(P 100) -- partial on the center, negative and positive + + ] + +tt' + :: forall (l :: I.L Int8) (r :: I.R Int8) + . I.Interval Int8 l r + => TestTree +tt' = testGroup ("Interval [" <> show l <> ", " <> show r <> "]") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genInt8 + case I.from @Int8 @l @r x of + Nothing -> assert (x < l' || x > r') + Just y -> do assert (x >= l' && x <= r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genInt8 + let y = I.shove @Int8 @l @r x + I.from (I.unwrap y) === Just y + if x < l' || x > r' + then I.from @Int8 @l @r x === Nothing + else I.from @Int8 @l @r x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIInt8 @l @r + b <- forAll $ genIInt8 @l @r + let x = toInteger (I.unwrap a) + toInteger (I.unwrap b) + case I.plus' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIInt8 @l @r + b <- forAll $ genIInt8 @l @r + let x = toInteger (I.unwrap a) * toInteger (I.unwrap b) + case I.mult' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIInt8 @l @r + b <- forAll $ genIInt8 @l @r + let x = toInteger (I.unwrap a) - toInteger (I.unwrap b) + case I.minus' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , if (l' == 0 && r' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIInt8 @l @r + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) (genIInt8 @l @r) + let (q, m) = toInteger (I.unwrap a) `divMod` toInteger (I.unwrap b) + case I.div' a b of + Nothing -> assert (q < l'' || q > r'' || m /= 0) + Just y -> do q === toInteger (I.unwrap y) + m === 0 + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genInt8 + case I.clamp @Int8 @l @r x of + y | x < l' -> I.unwrap y === l' + | x > r' -> I.unwrap y === r' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIInt8 @l @r + x === I.with x I.known' + + , case KI.cmpInteger (Proxy @l) (Proxy @r) of + LTI -> + [ testProperty "pred'" $ property $ do + x <- forAll $ genIInt8 @l @r + case I.pred' x of + Nothing -> x === l + Just y -> do x /== l + I.unwrap y === I.unwrap x - 1 + , testProperty "succ'" $ property $ do + x <- forAll $ genIInt8 @l @r + case I.succ' x of + Nothing -> x === r + Just y -> do x /== r + I.unwrap y === I.unwrap x + 1 + ] + _ -> mzero + + , case (leInteger @l @(P 0), leInteger @(P 0) @r) of + (Just Dict, Just Dict) -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Int8 @l @r) + _ -> mzero + + , case (leInteger @l @(P 1), leInteger @(P 1) @r) of + (Just Dict, Just Dict) -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Int8 @l @r) + _ -> mzero + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genIInt8 @l @r + I.negate' x === + (I.from =<< toIntegralSized (negate (toInteger (I.unwrap x)))) + + , withDict (negateInteger @r) $ + case (leInteger @l @(P 0), leInteger @(P 0) @r) of + (Just Dict, Just Dict) -> + case KI.cmpInteger (Proxy @l) (Proxy @(KI.Negate r)) of + EQI -> pure $ testProperty "negate" $ property $ do + x <- forAll $ genIInt8 @l @r + Just (I.negate x) === I.negate' x + _ -> mzero + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIInt8 @l @r + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Int8 (I.MinL Int8) (I.MaxR Int8)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIInt8 @l @r + x === I.up x + I.unwrap x === I.unwrap (I.up x :: I Int8 (I.MinL Int8) (I.MaxR Int8)) + ] + where + l = I.min :: I Int8 l r + l' = I.unwrap l :: Int8 + l'' = toInteger l' :: Integer + r = I.max :: I Int8 l r + r' = I.unwrap r :: Int8 + r'' = toInteger r' :: Integer + + diff --git a/test/I/Test/Integer.hs b/test/I/Test/Integer.hs new file mode 100644 --- /dev/null +++ b/test/I/Test/Integer.hs @@ -0,0 +1,565 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} + +module I.Test.Integer (tt) where + +import Control.Monad +import Data.Constraint +import Data.Proxy +import Data.Type.Ord +import Hedgehog (failure, forAll, property, assert, (===), (/==)) +import Hedgehog.Gen qualified as Gen +import KindInteger (N, P) +import KindInteger qualified as KI +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@=?)) +import Test.Tasty.Hedgehog (testProperty) + +import I (I) +import I qualified + +import I.Test.Support + +-------------------------------------------------------------------------------- + +tt :: TestTree +tt = testGroup "Integer" + [ testProperty "wrap" $ property $ do + x <- forAll genInteger + x === I.unwrap (I.wrap x) + + , tt'lr @(N 100) @(N 100) + , tt'lr @(N 100) @(N 10) + , tt'lr @(N 100) @(N 1) + , tt'lr @(N 100) @(N 0) + , tt'lr @(N 1) @(N 1) + , tt'lr @(N 1) @(P 0) + , tt'lr @(P 0) @(P 0) + , tt'lr @(P 0) @(P 1) + , tt'lr @(P 1) @(P 1) + , tt'lr @(P 0) @(P 100) + , tt'lr @(P 1) @(P 100) + , tt'lr @(P 10) @(P 100) + , tt'lr @(P 100) @(P 100) + + , tt'lu @(N 100) + , tt'lu @(N 1) + , tt'lu @(P 0) + , tt'lu @(P 1) + , tt'lu @(P 100) + + , tt'ur @(N 100) + , tt'ur @(N 1) + , tt'ur @(P 0) + , tt'ur @(P 1) + , tt'ur @(P 100) + + , tt'uu + ] + +tt'lr + :: forall (l :: KI.Integer) (r :: KI.Integer) + . I.Interval Integer ('Just l) ('Just r) + => TestTree +tt'lr = testGroup ("Interval [" <> show l <> ", " <> show r <> "]") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genInteger + case I.from @Integer @('Just l) @('Just r) x of + Nothing -> assert (x < l' || x > r') + Just y -> do assert (x >= l' && x <= r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genInteger + let y = I.shove @Integer @('Just l) @('Just r) x + I.from (I.unwrap y) === Just y + if x < l' || x > r' + then I.from @Integer @('Just l) @('Just r) x === Nothing + else I.from @Integer @('Just l) @('Just r) x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIInteger @('Just l) @('Just r) + b <- forAll $ genIInteger @('Just l) @('Just r) + let x = toInteger (I.unwrap a) + toInteger (I.unwrap b) + case I.plus' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIInteger @('Just l) @('Just r) + b <- forAll $ genIInteger @('Just l) @('Just r) + let x = toInteger (I.unwrap a) * toInteger (I.unwrap b) + case I.mult' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIInteger @('Just l) @('Just r) + b <- forAll $ genIInteger @('Just l) @('Just r) + let x = toInteger (I.unwrap a) - toInteger (I.unwrap b) + case I.minus' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , if (l' == 0 && r' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIInteger @('Just l) @('Just r) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) + (genIInteger @('Just l) @('Just r)) + let (q, m) = toInteger (I.unwrap a) `divMod` toInteger (I.unwrap b) + case I.div' a b of + Nothing -> assert (q < l'' || q > r'' || m /= 0) + Just y -> do q === toInteger (I.unwrap y) + m === 0 + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genInteger + case I.clamp @Integer @('Just l) @('Just r) x of + y | x < l' -> I.unwrap y === l' + | x > r' -> I.unwrap y === r' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIInteger @('Just l) @('Just r) + x === I.with x I.known' + + + , case KI.cmpInteger (Proxy @l) (Proxy @r) of + LTI -> + [ testProperty "pred'" $ property $ do + x <- forAll $ genIInteger @('Just l) @('Just r) + case I.pred' x of + Nothing -> x === l + Just y -> do x /== l + I.unwrap y === I.unwrap x - 1 + + , testProperty "succ'" $ property $ do + x <- forAll $ genIInteger @('Just l) @('Just r) + case I.succ' x of + Nothing -> x === r + Just y -> do x /== r + I.unwrap y === I.unwrap x + 1 + ] + _ -> mzero + + , case (leInteger @l @(P 0), leInteger @(P 0) @r) of + (Just Dict, Just Dict) -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Integer @('Just l) @('Just r)) + _ -> mzero + + + , case (leInteger @l @(P 1), leInteger @(P 1) @r) of + (Just Dict, Just Dict) -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Integer @('Just l) @('Just r)) + _ -> mzero + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genIInteger @('Just l) @('Just r) + case I.negate' x of + Just y -> Just x === I.negate' y + Nothing -> Nothing === I.from @Integer @('Just l) @('Just r) + (negate (toInteger (I.unwrap x))) + + , withDict (negateInteger @r) $ + case (leInteger @l @(P 0), leInteger @(P 0) @r) of + (Just Dict, Just Dict) -> + case KI.cmpInteger (Proxy @l) (Proxy @(KI.Negate r)) of + EQI -> pure $ testProperty "negate" $ property $ do + x <- forAll $ genIInteger @('Just l) @('Just r) + Just (I.negate x) === I.negate' x + _ -> mzero + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIInteger @('Just l) @('Just r) + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Integer (I.MinL Integer) (I.MaxR Integer)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIInteger @('Just l) @('Just r) + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Integer (I.MinL Integer) (I.MaxR Integer)) + + ] + where + l = I.min :: I Integer ('Just l) ('Just r) + l' = I.unwrap l :: Integer + l'' = toInteger l' :: Integer + r = I.max :: I Integer ('Just l) ('Just r) + r' = I.unwrap r :: Integer + r'' = toInteger r' :: Integer + + +tt'lu + :: forall (l :: KI.Integer) + . I.Interval Integer ('Just l) 'Nothing + => TestTree +tt'lu = testGroup ("Interval [" <> show l <> ", infinity)") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genInteger + case I.from @Integer @('Just l) @'Nothing x of + Nothing -> assert (x < l') + Just y -> do assert (x >= l') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genInteger + let y = I.shove @Integer @('Just l) @'Nothing x + I.from (I.unwrap y) === Just y + if x < l' + then I.from @Integer @('Just l) @'Nothing x === Nothing + else I.from @Integer @('Just l) @'Nothing x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIInteger @('Just l) @'Nothing + b <- forAll $ genIInteger @('Just l) @'Nothing + let x = toInteger (I.unwrap a) + toInteger (I.unwrap b) + case I.plus' a b of + Nothing -> assert (x < l'') + Just y -> toInteger (I.unwrap y) === x + + , case leInteger @(P 0) @l of + Nothing -> mzero + Just Dict -> pure $ testProperty "plus" $ property $ do + a <- forAll $ genIInteger @('Just l) @'Nothing + b <- forAll $ genIInteger @('Just l) @'Nothing + Just (I.plus a b) === I.plus' a b + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIInteger @('Just l) @'Nothing + b <- forAll $ genIInteger @('Just l) @'Nothing + let x = toInteger (I.unwrap a) * toInteger (I.unwrap b) + case I.mult' a b of + Nothing -> assert (x < l'') + Just y -> toInteger (I.unwrap y) === x + + , case leInteger @(P 0) @l of + Nothing -> mzero + Just Dict -> pure $ testProperty "mult" $ property $ do + a <- forAll $ genIInteger @('Just l) @'Nothing + b <- forAll $ genIInteger @('Just l) @'Nothing + Just (I.mult a b) === I.mult' a b + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIInteger @('Just l) @'Nothing + b <- forAll $ genIInteger @('Just l) @'Nothing + let x = toInteger (I.unwrap a) - toInteger (I.unwrap b) + case I.minus' a b of + Nothing -> assert (x < l'') + Just y -> toInteger (I.unwrap y) === x + + , if (l' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIInteger @('Just l) @'Nothing + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) + (genIInteger @('Just l) @'Nothing) + let (q, m) = toInteger (I.unwrap a) `divMod` toInteger (I.unwrap b) + case I.div' a b of + Nothing -> assert (q < l'' || m /= 0) + Just y -> do q === toInteger (I.unwrap y) + m === 0 + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genInteger + case I.clamp @Integer @('Just l) @'Nothing x of + y | x < l' -> I.unwrap y === l' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIInteger @('Just l) @'Nothing + x === I.with x I.known' + + , pure $ testProperty "pred'" $ property $ do + x <- forAll $ genIInteger @('Just l) @'Nothing + case I.pred' x of + Nothing -> x === l + Just y -> do x /== l + I.unwrap y === I.unwrap x - 1 + + , pure $ testProperty "succ'" $ property $ do + x <- forAll $ genIInteger @('Just l) @'Nothing + case I.succ' x of + Nothing -> failure + Just y -> do I.unwrap y === I.unwrap x + 1 + + , pure $ testProperty "succ" $ property $ do + x <- forAll $ genIInteger @('Just l) @'Nothing + Just (I.succ x) === I.succ' x + + , case leInteger @l @(P 0) of + Just Dict -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Integer @('Just l) @'Nothing) + _ -> mzero + + , case leInteger @l @(P 1) of + Just Dict -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Integer @('Just l) @'Nothing) + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIInteger @('Just l) @'Nothing + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Integer (I.MinL Integer) (I.MaxR Integer)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIInteger @('Just l) @'Nothing + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Integer (I.MinL Integer) (I.MaxR Integer)) + + ] + where + l = I.min :: I Integer ('Just l) 'Nothing + l' = I.unwrap l :: Integer + l'' = toInteger l' :: Integer + +tt'ur + :: forall (r :: KI.Integer) + . I.Interval Integer 'Nothing ('Just r) + => TestTree +tt'ur = testGroup ("Interval (-infinity, " <> show r <> "]") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genInteger + case I.from @Integer @'Nothing @('Just r) x of + Nothing -> assert (x > r') + Just y -> do assert (x <= r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genInteger + let y = I.shove @Integer @'Nothing @('Just r) x + I.from (I.unwrap y) === Just y + if x > r' + then I.from @Integer @'Nothing @('Just r) x === Nothing + else I.from @Integer @'Nothing @('Just r) x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIInteger @'Nothing @('Just r) + b <- forAll $ genIInteger @'Nothing @('Just r) + let x = toInteger (I.unwrap a) + toInteger (I.unwrap b) + case I.plus' a b of + Nothing -> assert (x > r'') + Just y -> toInteger (I.unwrap y) === x + + , case leInteger @r @(P 0) of + Nothing -> mzero + Just Dict -> pure $ testProperty "plus" $ property $ do + a <- forAll $ genIInteger @'Nothing @('Just r) + b <- forAll $ genIInteger @'Nothing @('Just r) + Just (I.plus a b) === I.plus' a b + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIInteger @'Nothing @('Just r) + b <- forAll $ genIInteger @'Nothing @('Just r) + let x = toInteger (I.unwrap a) * toInteger (I.unwrap b) + case I.mult' a b of + Nothing -> assert (x > r'') + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIInteger @'Nothing @('Just r) + b <- forAll $ genIInteger @'Nothing @('Just r) + let x = toInteger (I.unwrap a) - toInteger (I.unwrap b) + case I.minus' a b of + Nothing -> assert (x > r'') + Just y -> toInteger (I.unwrap y) === x + + , if (r' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIInteger @'Nothing @('Just r) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) + (genIInteger @'Nothing @('Just r)) + let (q, m) = toInteger (I.unwrap a) `divMod` toInteger (I.unwrap b) + case I.div' a b of + Nothing -> assert (q > r'' || m /= 0) + Just y -> do q === toInteger (I.unwrap y) + m === 0 + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genInteger + case I.clamp @Integer @'Nothing @('Just r) x of + y | x > r' -> I.unwrap y === r' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIInteger @'Nothing @('Just r) + x === I.with x I.known' + + , pure $ testProperty "pred'" $ property $ do + x <- forAll $ genIInteger @'Nothing @('Just r) + case I.pred' x of + Nothing -> failure + Just y -> I.unwrap y === I.unwrap x - 1 + + , pure $ testProperty "succ'" $ property $ do + x <- forAll $ genIInteger @'Nothing @('Just r) + case I.succ' x of + Nothing -> x === r + Just y -> do I.unwrap y === I.unwrap x + 1 + + , pure $ testProperty "pred" $ property $ do + x <- forAll $ genIInteger @'Nothing @('Just r) + Just (I.pred x) === I.pred' x + + , case leInteger @(P 0) @r of + Just Dict -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Integer @'Nothing @('Just r)) + _ -> mzero + + , case leInteger @(P 1) @r of + Just Dict -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Integer @'Nothing @('Just r)) + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIInteger @'Nothing @('Just r) + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Integer (I.MinL Integer) (I.MaxR Integer)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIInteger @'Nothing @('Just r) + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Integer (I.MinL Integer) (I.MaxR Integer)) + + ] + where + r = I.max :: I Integer 'Nothing ('Just r) + r' = I.unwrap r :: Integer + r'' = toInteger r' :: Integer + +tt'uu :: TestTree +tt'uu = testGroup "Interval (-infinity, +infinity)" + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genInteger + case I.from @Integer @'Nothing @'Nothing x of + Nothing -> failure + Just y -> I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genInteger + let y = I.shove @Integer @'Nothing @'Nothing x + I.from (I.unwrap y) === Just y + I.from @Integer @'Nothing @'Nothing x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIInteger @'Nothing @'Nothing + b <- forAll $ genIInteger @'Nothing @'Nothing + let x = toInteger (I.unwrap a) + toInteger (I.unwrap b) + case I.plus' a b of + Nothing -> failure + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "plus" $ property $ do + a <- forAll $ genIInteger @'Nothing @'Nothing + b <- forAll $ genIInteger @'Nothing @'Nothing + Just (I.plus a b) === I.plus' a b + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIInteger @'Nothing @'Nothing + b <- forAll $ genIInteger @'Nothing @'Nothing + let x = toInteger (I.unwrap a) * toInteger (I.unwrap b) + case I.mult' a b of + Nothing -> failure + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "mult" $ property $ do + a <- forAll $ genIInteger @'Nothing @'Nothing + b <- forAll $ genIInteger @'Nothing @'Nothing + Just (I.mult a b) === I.mult' a b + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIInteger @'Nothing @'Nothing + b <- forAll $ genIInteger @'Nothing @'Nothing + let x = toInteger (I.unwrap a) - toInteger (I.unwrap b) + case I.minus' a b of + Nothing -> failure + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "minus" $ property $ do + a <- forAll $ genIInteger @'Nothing @'Nothing + b <- forAll $ genIInteger @'Nothing @'Nothing + Just (I.minus a b) === I.minus' a b + + , pure $ testProperty "div'" $ property $ do + a <- forAll $ genIInteger @'Nothing @'Nothing + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) + (genIInteger @'Nothing @'Nothing) + let (q, m) = toInteger (I.unwrap a) `divMod` toInteger (I.unwrap b) + case I.div' a b of + Nothing -> assert (m /= 0) + Just y -> do q === toInteger (I.unwrap y) + m === 0 + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genInteger + x === I.unwrap (I.clamp @Integer @'Nothing @'Nothing x) + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIInteger @'Nothing @'Nothing + x === I.with x I.known' + + , pure $ testProperty "pred'" $ property $ do + x <- forAll $ genIInteger @'Nothing @'Nothing + case I.pred' x of + Nothing -> failure + Just y -> I.unwrap y === I.unwrap x - 1 + + , pure $ testProperty "succ'" $ property $ do + x <- forAll $ genIInteger @'Nothing @'Nothing + case I.succ' x of + Nothing -> failure + Just y -> I.unwrap y === I.unwrap x + 1 + + , pure $ testProperty "pred" $ property $ do + x <- forAll $ genIInteger @'Nothing @'Nothing + Just (I.pred x) === I.pred' x + + , pure $ testProperty "succ" $ property $ do + x <- forAll $ genIInteger @'Nothing @'Nothing + Just (I.succ x) === I.succ' x + + , pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Integer @'Nothing @'Nothing) + + , pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Integer @'Nothing @'Nothing) + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genIInteger @'Nothing @'Nothing + fmap I.unwrap (I.negate' x) === Just (negate (I.unwrap x)) + + , pure $ testProperty "negate" $ property $ do + x <- forAll $ genIInteger @'Nothing @'Nothing + Just (I.negate x) === I.negate' x + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIInteger @'Nothing @'Nothing + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Integer (I.MinL Integer) (I.MaxR Integer)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIInteger @'Nothing @'Nothing + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Integer (I.MinL Integer) (I.MaxR Integer)) + + ] + diff --git a/test/I/Test/Main.hs b/test/I/Test/Main.hs new file mode 100644 --- /dev/null +++ b/test/I/Test/Main.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} + +module I.Test.Main (main) where + +import Test.Tasty (TestTree, testGroup) +import Test.Tasty qualified as Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit(..)) +import Test.Tasty.Runners qualified as Tasty + +import I.Test.Int8 qualified +import I.Test.Integer qualified +import I.Test.Natural qualified +import I.Test.Rational qualified +import I.Test.Word8 qualified + +-------------------------------------------------------------------------------- + +main :: IO () +main = Tasty.defaultMainWithIngredients + [ Tasty.consoleTestReporter, Tasty.listingTests ] + $ Tasty.localOption (HedgehogTestLimit (Just 2000)) + $ tt + +tt :: TestTree +tt = testGroup "I" + [ I.Test.Word8.tt + , I.Test.Int8.tt + , I.Test.Natural.tt + , I.Test.Integer.tt + , I.Test.Rational.tt + ] + diff --git a/test/I/Test/Natural.hs b/test/I/Test/Natural.hs new file mode 100644 --- /dev/null +++ b/test/I/Test/Natural.hs @@ -0,0 +1,281 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} + +module I.Test.Natural (tt) where + +import Control.Monad +import Data.Constraint +import Data.Proxy +import Data.Type.Ord +import GHC.TypeLits qualified as L +import Hedgehog (failure, forAll, property, assert, (===), (/==)) +import Hedgehog.Gen qualified as Gen +import Numeric.Natural +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@=?)) +import Test.Tasty.Hedgehog (testProperty) + +import I (I) +import I qualified + +import I.Test.Support + +-------------------------------------------------------------------------------- + +tt :: TestTree +tt = testGroup "Natural" + [ testProperty "wrap" $ property $ do + x <- forAll genNatural + x === I.unwrap (I.wrap x) + + , tt'lr @0 @0 + , tt'lr @0 @1 + , tt'lr @0 @100 + , tt'l @0 + + , tt'lr @1 @1 + , tt'lr @1 @100 + , tt'l @1 + + , tt'lr @10 @10 + , tt'lr @10 @100 + , tt'l @10 + ] + +tt'lr + :: forall (l :: I.L Natural) (r :: Natural) + . I.Interval Natural l ('Just r) + => TestTree +tt'lr = testGroup ("Interval [" <> show l <> ", " <> show r <> "]") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genNatural + case I.from @Natural @l @('Just r) x of + Nothing -> assert (x < l' || x > r') + Just y -> do assert (x >= l' && x <= r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genNatural + let y = I.shove @Natural @l @('Just r) x + I.from (I.unwrap y) === Just y + if x < l' || x > r' + then I.from @Natural @l @('Just r) x === Nothing + else I.from @Natural @l @('Just r) x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genINatural @l @('Just r) + b <- forAll $ genINatural @l @('Just r) + let x = toInteger (I.unwrap a) + toInteger (I.unwrap b) + case I.plus' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genINatural @l @('Just r) + b <- forAll $ genINatural @l @('Just r) + let x = toInteger (I.unwrap a) * toInteger (I.unwrap b) + case I.mult' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genINatural @l @('Just r) + b <- forAll $ genINatural @l @('Just r) + let x = toInteger (I.unwrap a) - toInteger (I.unwrap b) + case I.minus' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , if (l' == 0 && r' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genINatural @l @('Just r) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) + (genINatural @l @('Just r)) + let (q, m) = toInteger (I.unwrap a) `divMod` toInteger (I.unwrap b) + case I.div' a b of + Nothing -> assert (q < l'' || q > r'' || m /= 0) + Just y -> do q === toInteger (I.unwrap y) + m === 0 + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genNatural + case I.clamp @Natural @l @('Just r) x of + y | x < l' -> I.unwrap y === l' + | x > r' -> I.unwrap y === r' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genINatural @l @('Just r) + x === I.with x I.known' + + + , case L.cmpNat (Proxy @l) (Proxy @r) of + LTI -> + [ testProperty "pred'" $ property $ do + x <- forAll $ genINatural @l @('Just r) + case I.pred' x of + Nothing -> x === l + Just y -> do x /== l + I.unwrap y === I.unwrap x - 1 + , testProperty "succ'" $ property $ do + x <- forAll $ genINatural @l @('Just r) + case I.succ' x of + Nothing -> x === r + Just y -> do x /== r + I.unwrap y === I.unwrap x + 1 + ] + _ -> mzero + + , case L.cmpNat (Proxy @l) (Proxy @0) of + EQI -> pure $ testCase "zero" $ + 0 @=? I.unwrap (I.zero @Natural @l @('Just r)) + _ -> mzero + + , case (leNatural @l @1, leNatural @1 @r) of + (Just Dict, Just Dict) -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Natural @l @('Just r)) + _ -> mzero + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genINatural @l @('Just r) + Nothing === I.negate' x + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genINatural @l @('Just r) + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Natural (I.MinL Natural) (I.MaxR Natural)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genINatural @l @('Just r) + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Natural (I.MinL Natural) (I.MaxR Natural)) + + ] + where + l = I.min :: I Natural l ('Just r) + l' = I.unwrap l :: Natural + l'' = toInteger l' :: Integer + r = I.max :: I Natural l ('Just r) + r' = I.unwrap r :: Natural + r'' = toInteger r' :: Integer + + +tt'l + :: forall (l :: I.L Natural) + . I.Interval Natural l 'Nothing + => TestTree +tt'l = testGroup ("Interval [" <> show l <> ", infinity)") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genNatural + case I.from @Natural @l @'Nothing x of + Nothing -> assert (x < l') + Just y -> do assert (x >= l') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genNatural + let y = I.shove @Natural @l @'Nothing x + I.from (I.unwrap y) === Just y + if x < l' + then I.from @Natural @l @'Nothing x === Nothing + else I.from @Natural @l @'Nothing x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genINatural @l @'Nothing + b <- forAll $ genINatural @l @'Nothing + let x = toInteger (I.unwrap a) + toInteger (I.unwrap b) + case I.plus' a b of + Nothing -> assert (x < l'') + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genINatural @l @'Nothing + b <- forAll $ genINatural @l @'Nothing + let x = toInteger (I.unwrap a) * toInteger (I.unwrap b) + case I.mult' a b of + Nothing -> assert (x < l'') + Just y -> toInteger (I.unwrap y) === x + + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genINatural @l @'Nothing + b <- forAll $ genINatural @l @'Nothing + let x = toInteger (I.unwrap a) - toInteger (I.unwrap b) + case I.minus' a b of + Nothing -> assert (x < l'') + Just y -> toInteger (I.unwrap y) === x + + , if (l' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genINatural @l @'Nothing + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) + (genINatural @l @'Nothing) + let (q, m) = toInteger (I.unwrap a) `divMod` toInteger (I.unwrap b) + case I.div' a b of + Nothing -> assert (q < l'' || m /= 0) + Just y -> do q === toInteger (I.unwrap y) + m === 0 + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genNatural + case I.clamp @Natural @l @'Nothing x of + y | x < l' -> I.unwrap y === l' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genINatural @l @'Nothing + x === I.with x I.known' + + , pure $ testProperty "pred'" $ property $ do + x <- forAll $ genINatural @l @'Nothing + case I.pred' x of + Nothing -> x === l + Just y -> do x /== l + I.unwrap y === I.unwrap x - 1 + + , pure $ testProperty "succ'" $ property $ do + x <- forAll $ genINatural @l @'Nothing + case I.succ' x of + Nothing -> failure + Just y -> I.unwrap y === I.unwrap x + 1 + + , pure $ testProperty "succ" $ property $ do + x <- forAll $ genINatural @l @'Nothing + Just (I.succ x) === I.succ' x + + , case L.cmpNat (Proxy @l) (Proxy @0) of + EQI -> pure $ testCase "zero" $ + 0 @=? I.unwrap (I.zero @Natural @l @'Nothing) + _ -> mzero + + , case leNatural @l @1 of + Just Dict -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Natural @l @'Nothing) + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genINatural @l @'Nothing + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Natural (I.MinL Natural) (I.MaxR Natural)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genINatural @l @'Nothing + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Natural (I.MinL Natural) (I.MaxR Natural)) + + ] + where + l = I.min :: I Natural l 'Nothing + l' = I.unwrap l :: Natural + l'' = toInteger l' :: Integer + diff --git a/test/I/Test/Rational.hs b/test/I/Test/Rational.hs new file mode 100644 --- /dev/null +++ b/test/I/Test/Rational.hs @@ -0,0 +1,1036 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE OverloadedStrings #-} + +{-# OPTIONS_GHC -Wno-unused-top-binds -Wno-unused-imports #-} + +module I.Test.Rational (tt) where + +import Control.Monad +import Data.Constraint +import Data.Proxy +import Data.Type.Ord +import Hedgehog (failure, forAll, property, assert, (===), (/==)) +import Hedgehog.Gen qualified as Gen +import KindInteger (N) +import KindRational (type (/)) +import KindRational qualified as KR +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@=?)) +import Test.Tasty.Hedgehog (testProperty) + +import I (I) +import I qualified + +import I.Test.Support + +-------------------------------------------------------------------------------- + +tt :: TestTree +tt = testGroup "Rational" + [ testProperty "wrap" $ property $ do + x <- forAll genRational + x === I.unwrap (I.wrap x) + + , tt'cc @(N 100/1) @(N 100/1) + , tt'cc @(N 100/1) @(N 10/1) + , tt'cc @(N 100/1) @(N 1/1) + , tt'cc @(N 100/1) @(N 0/1) + , tt'cc @(N 1/1) @(N 1/1) + , tt'cc @(N 1/1) @(0/1) + , tt'cc @(0/1) @(0/1) + , tt'cc @(0/1) @(1/1) + , tt'cc @(1/1) @(1/1) + , tt'cc @(0/1) @(100/1) + , tt'cc @(1/1) @(100/1) + , tt'cc @(10/1) @(100/1) + , tt'cc @(100/1) @(100/1) + + , tt'co @(N 100/1) @(N 10/1) + , tt'co @(N 100/1) @(N 1/1) + , tt'co @(N 100/1) @(N 0/1) + , tt'co @(N 1/1) @(0/1) + , tt'co @(0/1) @(1/1) + , tt'co @(0/1) @(100/1) + , tt'co @(1/1) @(100/1) + , tt'co @(10/1) @(100/1) + + , tt'cu @(N 100/1) + , tt'cu @(N 1/1) + , tt'cu @(0/1) + , tt'cu @(1/1) + , tt'cu @(100/1) + + , tt'oc @(N 100/1) @(N 10/1) + , tt'oc @(N 100/1) @(N 1/1) + , tt'oc @(N 100/1) @(N 0/1) + , tt'oc @(N 1/1) @(0/1) + , tt'oc @(0/1) @(1/1) + , tt'oc @(0/1) @(100/1) + , tt'oc @(1/1) @(100/1) + , tt'oc @(10/1) @(100/1) + + , tt'oo @(N 100/1) @(N 10/1) + , tt'oo @(N 100/1) @(N 1/1) + , tt'oo @(N 100/1) @(N 0/1) + , tt'oo @(N 1/1) @(0/1) + , tt'oo @(0/1) @(1/1) + , tt'oo @(0/1) @(100/1) + , tt'oo @(1/1) @(100/1) + , tt'oo @(10/1) @(100/1) + + , tt'ou @(N 100/1) + , tt'ou @(N 1/1) + , tt'ou @(0/1) + , tt'ou @(1/1) + , tt'ou @(100/1) + + , tt'uc @(N 100/1) + , tt'uc @(N 1/1) + , tt'uc @(0/1) + , tt'uc @(1/1) + , tt'uc @(100/1) + + , tt'uo @(N 100/1) + , tt'uo @(N 1/1) + , tt'uo @(0/1) + , tt'uo @(1/1) + , tt'uo @(100/1) + + , tt'uu + ] + +tt'cc + :: forall (l :: KR.Rational) (r :: KR.Rational) + . I.Interval Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + => TestTree +tt'cc = testGroup ("Interval [" <> show l <> ", " <> show r <> "]") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genRational + case I.from @Rational @('Just '( 'True, l)) @('Just '( 'True, r)) x of + Nothing -> assert (x < l' || x > r') + Just y -> do assert (x >= l' && x <= r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genRational + let y = I.shove @Rational @('Just '( 'True, l)) @('Just '( 'True, r)) x + I.from (I.unwrap y) === Just y + if x < l' || x > r' + then I.from @Rational @('Just '( 'True, l)) @('Just '( 'True, r)) x === Nothing + else I.from @Rational @('Just '( 'True, l)) @('Just '( 'True, r)) x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + b <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + let x = I.unwrap a + I.unwrap b + case I.plus' a b of + Nothing -> assert (x < l' || x > r') + Just y -> I.unwrap y === x + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + b <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + let x = I.unwrap a * I.unwrap b + case I.mult' a b of + Nothing -> assert (x < l' || x > r') + Just y -> I.unwrap y === x + + , case (leRational @(0/1) @l, leRational @r @(1/1)) of + (Just Dict, Just Dict) -> + pure $ testProperty "mult" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + b <- forAll $ genIRational + Just (I.mult a b) === I.mult' a b + _ -> mzero + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + b <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + let x = I.unwrap a - I.unwrap b + case I.minus' a b of + Nothing -> assert (x < l' || x > r') + Just y -> I.unwrap y === x + + , if (l' == 0 && r' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === I.from (I.unwrap a / I.unwrap b) + + , case (ltRational @(0/1) @l, leRational @r @(1/1)) of + (Just Dict, Just Dict) -> pure $ testProperty "div" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) + (genIRational @('Just '( 'True, l)) + @('Just '( 'True, r))) + I.div' a b === Just (I.div a b) + _ -> mzero + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genRational + case I.clamp @Rational @('Just '( 'True, l)) @('Just '( 'True, r)) x of + y | x < l' -> I.unwrap y === l' + | x > r' -> I.unwrap y === r' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + x === I.with x I.known' + + , case (leRational @l @(0/1), leRational @(0/1) @r) of + (Just Dict, Just Dict) -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Rational @('Just '( 'True, l)) + @('Just '( 'True, r))) + _ -> mzero + + , case (leRational @l @(1/1), leRational @(1/1) @r) of + (Just Dict, Just Dict) -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Rational @('Just '( 'True, l)) + @('Just '( 'True, r))) + _ -> mzero + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + case I.negate' x of + Just y -> Just x === I.negate' y + Nothing -> Nothing === I.from @Rational + @('Just '( 'True, l)) + @('Just '( 'True, r)) + (negate (I.unwrap x)) + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'True, r)) + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + ] + where + l = I.min :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + l' = I.unwrap l :: Rational + r = I.max :: I Rational ('Just '( 'True, l)) ('Just '( 'True, r)) + r' = I.unwrap r :: Rational + +tt'co + :: forall (l :: KR.Rational) (r :: KR.Rational) + . I.Interval Rational ('Just '( 'True, l)) ('Just '( 'False, r)) + => TestTree +tt'co = testGroup ("Interval [" <> show l <> ", " <> show r' <> ")") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genRational + case I.from @Rational @('Just '( 'True, l)) @('Just '( 'False, r)) x of + Nothing -> assert (x < l' || x >= r') + Just y -> do assert (x >= l' && x < r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genRational + let y = I.shove @Rational @('Just '( 'True, l)) @('Just '( 'False, r)) x + I.from (I.unwrap y) === Just y + if x < l' || x >= r' + then I.from @Rational @('Just '( 'True, l)) @('Just '( 'False, r)) x === Nothing + else I.from @Rational @('Just '( 'True, l)) @('Just '( 'False, r)) x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + b <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + let x = I.unwrap a + I.unwrap b + case I.plus' a b of + Nothing -> assert (x < l' || x >= r') + Just y -> I.unwrap y === x + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + b <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + let x = I.unwrap a * I.unwrap b + case I.mult' a b of + Nothing -> assert (x < l' || x >= r') + Just y -> I.unwrap y === x + + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + b <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + let x = I.unwrap a - I.unwrap b + case I.minus' a b of + Nothing -> assert (x < l' || x >= r') + Just y -> I.unwrap y === x + + , if (l' == 0 && r' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === I.from (I.unwrap a / I.unwrap b) + + , case (ltRational @(0/1) @l, leRational @r @(1/1)) of + (Just Dict, Just Dict) -> pure $ testProperty "div" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === Just (I.div a b) + _ -> mzero + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + x === I.with x I.known' + + , case (leRational @l @(0/1), ltRational @(0/1) @r) of + (Just Dict, Just Dict) -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Rational @('Just '( 'True, l)) + @('Just '( 'False, r))) + _ -> mzero + + + , case (leRational @l @(1/1), ltRational @(1/1) @r) of + (Just Dict, Just Dict) -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Rational @('Just '( 'True, l)) + @('Just '( 'False, r))) + _ -> mzero + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + case I.negate' x of + Just y -> Just x === I.negate' y + Nothing -> Nothing === I.from @Rational + @('Just '( 'True, l)) + @('Just '( 'False, r)) + (negate (I.unwrap x)) + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @('Just '( 'False, r)) + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + ] + where + l = I.min :: I Rational ('Just '( 'True, l)) ('Just '( 'False, r)) + l' = I.unwrap l :: Rational + r' = KR.rationalVal (Proxy @r) :: Rational + +tt'cu + :: forall (l :: KR.Rational) + . I.Interval Rational ('Just '( 'True, l)) 'Nothing + => TestTree +tt'cu = testGroup ("Interval [" <> show l <> ", infinity)") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genRational + case I.from @Rational @('Just '( 'True, l)) @'Nothing x of + Nothing -> assert (x < l') + Just y -> do assert (x >= l') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genRational + let y = I.shove @Rational @('Just '( 'True, l)) @'Nothing x + I.from (I.unwrap y) === Just y + if x < l' + then I.from @Rational @('Just '( 'True, l)) @'Nothing x === Nothing + else I.from @Rational @('Just '( 'True, l)) @'Nothing x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + let x = I.unwrap a + I.unwrap b + case I.plus' a b of + Nothing -> assert (x < l') + Just y -> I.unwrap y === x + + , case leRational @(0/1) @l of + Nothing -> mzero + Just Dict -> pure $ testProperty "plus" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + Just (I.plus a b) === I.plus' a b + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + let x = I.unwrap a * I.unwrap b + case I.mult' a b of + Nothing -> assert (x < l') + Just y -> I.unwrap y === x + + , case leRational @(1/1) @l of + Nothing -> mzero + Just Dict -> pure $ testProperty "mult" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + Just (I.mult a b) === I.mult' a b + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + let x = I.unwrap a - I.unwrap b + case I.minus' a b of + Nothing -> assert (x < l') + Just y -> I.unwrap y === x + + , if (l' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === I.from (I.unwrap a / I.unwrap b) + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genRational + case I.clamp @Rational @('Just '( 'True, l)) @'Nothing x of + y | x < l' -> I.unwrap y === l' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + x === I.with x I.known' + + , case leRational @l @(0/1) of + Just Dict -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Rational @('Just '( 'True, l)) @'Nothing) + _ -> mzero + + , case leRational @l @(1/1) of + Just Dict -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Rational @('Just '( 'True, l)) @'Nothing) + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIRational @('Just '( 'True, l)) @'Nothing + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Rational (I.MinL Rational) (I.MaxR Rational)) + ] + where + l = I.min :: I Rational ('Just '( 'True, l)) 'Nothing + l' = I.unwrap l :: Rational + +tt'oc + :: forall (l :: KR.Rational) (r :: KR.Rational) + . I.Interval Rational ('Just '( 'False, l)) ('Just '( 'True, r)) + => TestTree +tt'oc = testGroup ("Interval (" <> show l' <> ", " <> show r <> "]") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genRational + case I.from @Rational @('Just '( 'False, l)) @('Just '( 'True, r)) x of + Nothing -> assert (x <= l' || x > r') + Just y -> do assert (x > l' && x <= r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genRational + let y = I.shove @Rational @('Just '( 'False, l)) @('Just '( 'True, r)) x + I.from (I.unwrap y) === Just y + if x <= l' || x > r' + then I.from @Rational @('Just '( 'False, l)) @('Just '( 'True, r)) x === Nothing + else I.from @Rational @('Just '( 'False, l)) @('Just '( 'True, r)) x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + b <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + let x = I.unwrap a + I.unwrap b + case I.plus' a b of + Nothing -> assert (x <= l' || x > r') + Just y -> I.unwrap y === x + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + b <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + let x = I.unwrap a * I.unwrap b + case I.mult' a b of + Nothing -> assert (x <= l' || x > r') + Just y -> I.unwrap y === x + + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + b <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + let x = I.unwrap a - I.unwrap b + case I.minus' a b of + Nothing -> assert (x <= l' || x > r') + Just y -> I.unwrap y === x + + , if (r' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === I.from (I.unwrap a / I.unwrap b) + + , case (ltRational @(0/1) @l, leRational @r @(1/1)) of + (Just Dict, Just Dict) -> pure $ testProperty "div" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === Just (I.div a b) + _ -> mzero + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + x === I.with x I.known' + + , case (ltRational @l @(0/1), leRational @(0/1) @r) of + (Just Dict, Just Dict) -> + pure $ testCase "zero" $ + 0 @=? I.unwrap (I.zero @Rational @('Just '( 'False, l)) + @('Just '( 'True, r))) + _ -> mzero + + , case (ltRational @l @(1/1), leRational @(1/1) @r) of + (Just Dict, Just Dict) -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Rational @('Just '( 'False, l)) + @('Just '( 'True, r))) + _ -> mzero + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + case I.negate' x of + Just y -> Just x === I.negate' y + Nothing -> Nothing === I.from @Rational + @('Just '( 'False, l)) + @('Just '( 'True, r)) + (negate (I.unwrap x)) + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'True, r)) + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + ] + where + l' = KR.rationalVal (Proxy @l) :: Rational + r = I.max :: I Rational ('Just '( 'False, l)) ('Just '( 'True, r)) + r' = I.unwrap r :: Rational + +tt'oo + :: forall (l :: KR.Rational) (r :: KR.Rational) + . I.Interval Rational ('Just '( 'False, l)) ('Just '( 'False, r)) + => TestTree +tt'oo = testGroup ("Interval (" <> show l' <> ", " <> show r' <> ")") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genRational + case I.from @Rational @('Just '( 'False, l)) @('Just '( 'False, r)) x of + Nothing -> assert (x <= l' || x >= r') + Just y -> do assert (x > l' && x < r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genRational + let y = I.shove @Rational @('Just '( 'False, l)) @('Just '( 'False, r)) x + I.from (I.unwrap y) === Just y + if x <= l' || x >= r' + then I.from @Rational @('Just '( 'False, l)) @('Just '( 'False, r)) x === Nothing + else I.from @Rational @('Just '( 'False, l)) @('Just '( 'False, r)) x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + b <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + let x = I.unwrap a + I.unwrap b + case I.plus' a b of + Nothing -> assert (x <= l' || x >= r') + Just y -> I.unwrap y === x + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + b <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + let x = I.unwrap a * I.unwrap b + case I.mult' a b of + Nothing -> assert (x <= l' || x >= r') + Just y -> I.unwrap y === x + + , case (leRational @(0/1) @l, leRational @r @(1/1)) of + (Just Dict, Just Dict) -> + pure $ testProperty "mult" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + b <- forAll $ genIRational + Just (I.mult a b) === I.mult' a b + _ -> mzero + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + b <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + let x = I.unwrap a - I.unwrap b + case I.minus' a b of + Nothing -> assert (x <= l' || x >= r') + Just y -> I.unwrap y === x + + , pure $ testProperty "div'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === I.from (I.unwrap a / I.unwrap b) + + , case (ltRational @(0/1) @l, leRational @r @(1/1)) of + (Just Dict, Just Dict) -> pure $ testProperty "div" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) + (genIRational @('Just '( 'False, l)) + @('Just '( 'False, r))) + I.div' a b === Just (I.div a b) + _ -> mzero + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + x === I.with x I.known' + + , case (ltRational @l @(0/1), ltRational @(0/1) @r) of + (Just Dict, Just Dict) -> pure $ testCase "one" $ do + 0 @=? I.unwrap (I.zero @Rational @('Just '( 'False, l)) + @('Just '( 'False, r))) + _ -> mzero + + , case (ltRational @l @(1/1), ltRational @(1/1) @r) of + (Just Dict, Just Dict) -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Rational @('Just '( 'False, l)) + @('Just '( 'False, r))) + _ -> mzero + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + case I.negate' x of + Just y -> Just x === I.negate' y + Nothing -> Nothing === I.from @Rational + @('Just '( 'False, l)) + @('Just '( 'False, r)) + (negate (I.unwrap x)) + + , withDict (negateRational @r) $ + case (ltRational @l @(0/1), ltRational @(0/1) @r) of + (Just Dict, Just Dict) -> + case KR.cmpRational (Proxy @l) (Proxy @(KR.Negate r)) of + EQI -> pure $ testProperty "negate" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) + @('Just '( 'False, r)) + Just (I.negate x) === I.negate' x + _ -> mzero + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @('Just '( 'False, r)) + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + ] + where + l' = KR.rationalVal (Proxy @l) :: Rational + r' = KR.rationalVal (Proxy @r) :: Rational + +tt'ou + :: forall (l :: KR.Rational) + . I.Interval Rational ('Just '( 'False, l)) 'Nothing + => TestTree +tt'ou = testGroup ("Interval (" <> show l' <> ", infinity)") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genRational + case I.from @Rational @('Just '( 'False, l)) @'Nothing x of + Nothing -> assert (x <= l') + Just y -> do assert (x > l') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genRational + let y = I.shove @Rational @('Just '( 'False, l)) @'Nothing x + I.from (I.unwrap y) === Just y + if x <= l' + then I.from @Rational @('Just '( 'False, l)) @'Nothing x === Nothing + else I.from @Rational @('Just '( 'False, l)) @'Nothing x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + let x = I.unwrap a + I.unwrap b + case I.plus' a b of + Nothing -> assert (x <= l') + Just y -> I.unwrap y === x + + , case leRational @(0/1) @l of + Nothing -> mzero + Just Dict -> pure $ testProperty "plus" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + Just (I.plus a b) === I.plus' a b + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + let x = I.unwrap a * I.unwrap b + case I.mult' a b of + Nothing -> assert (x <= l') + Just y -> I.unwrap y === x + + , case leRational @(1/1) @l of + Nothing -> mzero + Just Dict -> pure $ testProperty "mult" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + Just (I.mult a b) === I.mult' a b + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + b <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + let x = I.unwrap a - I.unwrap b + case I.minus' a b of + Nothing -> assert (x <= l') + Just y -> I.unwrap y === x + + , if (l' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === I.from (I.unwrap a / I.unwrap b) + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + x === I.with x I.known' + + , case ltRational @l @(0/1) of + Just Dict -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Rational @('Just '( 'False, l)) @'Nothing) + _ -> mzero + + , case ltRational @l @(1/1) of + Just Dict -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Rational @('Just '( 'False, l)) @'Nothing) + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIRational @('Just '( 'False, l)) @'Nothing + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + ] + where + l' = KR.rationalVal (Proxy @l) :: Rational + +tt'uc + :: forall (r :: KR.Rational) + . I.Interval Rational 'Nothing ('Just '( 'True, r)) + => TestTree +tt'uc = testGroup ("Interval (-infinity, " <> show r <> "]") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genRational + case I.from @Rational @'Nothing @('Just '( 'True, r)) x of + Nothing -> assert (x > r') + Just y -> do assert (x <= r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genRational + let y = I.shove @Rational @'Nothing @('Just '( 'True, r)) x + I.from (I.unwrap y) === Just y + if x > r' + then I.from @Rational @'Nothing @('Just '( 'True, r)) x === Nothing + else I.from @Rational @'Nothing @('Just '( 'True, r)) x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + b <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + let x = I.unwrap a + I.unwrap b + case I.plus' a b of + Nothing -> assert (x > r') + Just y -> I.unwrap y === x + + , case leRational @r @(0/1) of + Nothing -> mzero + Just Dict -> pure $ testProperty "plus" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + b <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + Just (I.plus a b) === I.plus' a b + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + b <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + let x = I.unwrap a * I.unwrap b + case I.mult' a b of + Nothing -> assert (x > r') + Just y -> I.unwrap y === x + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + b <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + let x = I.unwrap a - I.unwrap b + case I.minus' a b of + Nothing -> assert (x > r') + Just y -> I.unwrap y === x + + , if (r' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === I.from (I.unwrap a / I.unwrap b) + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genRational + case I.clamp @Rational @'Nothing @('Just '( 'True, r)) x of + y | x > r' -> I.unwrap y === r' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + x === I.with x I.known' + + , case leRational @(0/1) @r of + Just Dict -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Rational @'Nothing @('Just '( 'True, r))) + _ -> mzero + + , case leRational @(1/1) @r of + Just Dict -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Rational @'Nothing @('Just '( 'True, r))) + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIRational @'Nothing @('Just '( 'True, r)) + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Rational (I.MinL Rational) (I.MaxR Rational)) + ] + where + r = I.max :: I Rational 'Nothing ('Just '( 'True, r)) + r' = I.unwrap r :: Rational + +tt'uo + :: forall (r :: KR.Rational) + . I.Interval Rational 'Nothing ('Just '( 'False, r)) + => TestTree +tt'uo = testGroup ("Interval (-infinity, " <> show r' <> ")") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genRational + case I.from @Rational @'Nothing @('Just '( 'False, r)) x of + Nothing -> assert (x >= r') + Just y -> do assert (x < r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genRational + let y = I.shove @Rational @'Nothing @('Just '( 'False, r)) x + I.from (I.unwrap y) === Just y + if x >= r' + then I.from @Rational @'Nothing @('Just '( 'False, r)) x === Nothing + else I.from @Rational @'Nothing @('Just '( 'False, r)) x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + b <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + let x = I.unwrap a + I.unwrap b + case I.plus' a b of + Nothing -> assert (x >= r') + Just y -> I.unwrap y === x + + , case leRational @r @(0/1) of + Nothing -> mzero + Just Dict -> pure $ testProperty "plus" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + b <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + Just (I.plus a b) === I.plus' a b + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + b <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + let x = I.unwrap a * I.unwrap b + case I.mult' a b of + Nothing -> assert (x >= r') + Just y -> I.unwrap y === x + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + b <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + let x = I.unwrap a - I.unwrap b + case I.minus' a b of + Nothing -> assert (x >= r') + Just y -> I.unwrap y === x + + , pure $ testProperty "div'" $ property $ do + a <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === I.from (I.unwrap a / I.unwrap b) + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + x === I.with x I.known' + + , case ltRational @(0/1) @r of + Just Dict -> pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Rational @'Nothing @('Just '( 'False, r))) + _ -> mzero + + , case ltRational @(1/1) @r of + Just Dict -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Rational @'Nothing @('Just '( 'False, r))) + _ -> mzero + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIRational @'Nothing @('Just '( 'False, r)) + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + ] + where + r' = KR.rationalVal (Proxy @r) :: Rational + +tt'uu :: TestTree +tt'uu = testGroup "Interval (-infinity, +infinity)" + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genRational + case I.from @Rational @'Nothing @'Nothing x of + Nothing -> failure + Just y -> I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genRational + let y = I.shove @Rational @'Nothing @'Nothing x + I.from (I.unwrap y) === Just y + I.from @Rational @'Nothing @'Nothing x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIRational @'Nothing @'Nothing + b <- forAll $ genIRational @'Nothing @'Nothing + let x = I.unwrap a + I.unwrap b + case I.plus' a b of + Nothing -> failure + Just y -> I.unwrap y === x + + , pure $ testProperty "plus" $ property $ do + a <- forAll $ genIRational @'Nothing @'Nothing + b <- forAll $ genIRational @'Nothing @'Nothing + Just (I.plus a b) === I.plus' a b + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIRational @'Nothing @'Nothing + b <- forAll $ genIRational @'Nothing @'Nothing + let x = I.unwrap a * I.unwrap b + case I.mult' a b of + Nothing -> failure + Just y -> I.unwrap y === x + + , pure $ testProperty "mult" $ property $ do + a <- forAll $ genIRational @'Nothing @'Nothing + b <- forAll $ genIRational @'Nothing @'Nothing + Just (I.mult a b) === I.mult' a b + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIRational @'Nothing @'Nothing + b <- forAll $ genIRational @'Nothing @'Nothing + let x = I.unwrap a - I.unwrap b + case I.minus' a b of + Nothing -> failure + Just y -> I.unwrap y === x + + , pure $ testProperty "minus" $ property $ do + a <- forAll $ genIRational @'Nothing @'Nothing + b <- forAll $ genIRational @'Nothing @'Nothing + Just (I.minus a b) === I.minus' a b + + , pure $ testProperty "div'" $ property $ do + a <- forAll $ genIRational @'Nothing @'Nothing + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) genIRational + I.div' a b === I.from (I.unwrap a / I.unwrap b) + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genRational + x === I.unwrap (I.clamp @Rational @'Nothing @'Nothing x) + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIRational @'Nothing @'Nothing + x === I.with x I.known' + + , pure $ testCase "zero" $ do + 0 @=? I.unwrap (I.zero @Rational @'Nothing @'Nothing) + + , pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Rational @'Nothing @'Nothing) + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genIRational @'Nothing @'Nothing + fmap I.unwrap (I.negate' x) === Just (negate (I.unwrap x)) + + , pure $ testProperty "negate" $ property $ do + x <- forAll $ genIRational @'Nothing @'Nothing + Just (I.negate x) === I.negate' x + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIRational @'Nothing @'Nothing + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIRational @'Nothing @'Nothing + x === I.up x + I.unwrap x === + I.unwrap (I.up x :: I Rational (I.MinL Rational) (I.MaxR Rational)) + + ] + diff --git a/test/I/Test/Support.hs b/test/I/Test/Support.hs new file mode 100644 --- /dev/null +++ b/test/I/Test/Support.hs @@ -0,0 +1,164 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +module I.Test.Support + ( genWord8 + , genInt8 + , genNatural + , genInteger + , genRational + + , genIWord8 + , genIInt8 + , genINatural + , genIInteger + , genIRational + + , leNatural + , leInteger + , leRational + , ltRational + + , negateInteger + , negateRational + ) where + +import Data.Constraint +import Data.Int +import Data.Proxy +import Data.Type.Ord +import Data.Word +import GHC.Real ((%)) +import GHC.TypeLits qualified as L +import Hedgehog (MonadGen) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +import KindInteger qualified as KI +import KindRational qualified as KR +import Numeric.Natural +import Unsafe.Coerce (unsafeCoerce) + +import I (I) +import I qualified + +-------------------------------------------------------------------------------- + +genWord8 :: MonadGen m => m Word8 +genWord8 = Gen.integral $ Range.constant minBound maxBound + +genInt8 :: MonadGen m => m Int8 +genInt8 = Gen.integral $ Range.constant minBound maxBound + +genNatural :: MonadGen m => m Natural +genNatural = Gen.integral $ Range.linear 0 (10 ^ (10 :: Int)) + +genInteger :: MonadGen m => m Integer +genInteger = Gen.integral $ Range.linearFrom 0 (negate (10 ^ (10 :: Int))) + (10 ^ (10 :: Int)) + +genRational :: MonadGen m => m Rational +genRational = do + n <- genInteger + d <- Gen.integral $ Range.linear 1 (10 ^ (10 :: Int)) + pure (n % d) + +-------------------------------------------------------------------------------- + +genIWord8 :: forall l r m. (MonadGen m, I.Shove Word8 l r) => m (I Word8 l r) +genIWord8 = I.shove <$> genWord8 + + +genIInt8 :: forall l r m. (MonadGen m, I.Shove Int8 l r) => m (I Int8 l r) +genIInt8 = I.shove <$> genInt8 + +genINatural + :: forall l r m. (MonadGen m, I.Shove Natural l r) => m (I Natural l r) +genINatural = I.shove <$> genNatural + +genIInteger + :: forall l r m. (MonadGen m, I.Shove Integer l r) => m (I Integer l r) +genIInteger = I.shove <$> genInteger + +genIRational + :: forall l r m. (MonadGen m, I.Shove Rational l r) => m (I Rational l r) +genIRational = I.shove <$> genRational + +-------------------------------------------------------------------------------- + +leNatural + :: forall a b + . (L.KnownNat a, L.KnownNat b) + => Maybe (Dict (a L.<= b)) +leNatural = case L.cmpNat (Proxy @a) (Proxy @b) of + L.LTI -> Just $ unsafeCoerce (Dict @()) + L.EQI -> Just $ unsafeCoerce (Dict @()) + L.GTI -> Nothing + +leInteger + :: forall (a :: KI.Integer) (b :: KI.Integer) + . (KI.KnownInteger a, KI.KnownInteger b) + => Maybe (Dict (a <= b)) +leInteger = case KI.cmpInteger (Proxy @a) (Proxy @b) of + L.LTI -> Just $ unsafeCoerce (Dict @()) + L.EQI -> Just $ unsafeCoerce (Dict @()) + L.GTI -> Nothing + +leRational + :: forall (a :: KR.Rational) (b :: KR.Rational) + . (KR.KnownRational a, KR.KnownRational b) + => Maybe (Dict (a <= b)) +leRational = case KR.cmpRational (Proxy @a) (Proxy @b) of + L.LTI -> Just $ unsafeCoerce (Dict @()) + L.EQI -> Just $ unsafeCoerce (Dict @()) + L.GTI -> Nothing + +ltRational + :: forall (a :: KR.Rational) (b :: KR.Rational) + . (KR.KnownRational a, KR.KnownRational b) + => Maybe (Dict (a < b)) +ltRational = case KR.cmpRational (Proxy @a) (Proxy @b) of + L.LTI -> Just $ unsafeCoerce (Dict @()) + L.EQI -> Nothing + L.GTI -> Nothing + +-------------------------------------------------------------------------------- +-- TODO: Move this stuff to KindInteger (ideas from Data.Constraint.Nat) + +newtype IntegerMagic n = + IntegerMagic (KI.KnownInteger n => Dict (KI.KnownInteger n)) + +-- WARNING: Causes SIGSEGV on GHCi 9.4.3. See GHC issue #19667. The workaround +-- is to run tests with `cabal test` instead. +integerMagic1 + :: forall a b + . (Integer -> Integer) -- ^ a -> b + -> (KI.KnownInteger a :- KI.KnownInteger b) +integerMagic1 f = Sub $ unsafeCoerce (IntegerMagic Dict) + $ f (KI.integerVal (Proxy @a)) + +negateInteger + :: forall (a :: KI.Integer) + . (KI.KnownInteger a) :- (KI.KnownInteger (KI.Negate a)) +negateInteger = integerMagic1 negate + + +-------------------------------------------------------------------------------- +-- TODO: Move this stuff to KindRational (ideas from Data.Constraint.Nat) + +newtype RationalMagic n = + RationalMagic (KR.KnownRational n => Dict (KR.KnownRational n)) + +-- WARNING: Causes SIGSEGV on GHCi 9.4.3. See GHC issue #19667. The workaround +-- is to run tests with `cabal test` instead. +rationalMagic1 + :: forall a b + . (Rational -> Rational) -- ^ a -> b + -> (KR.KnownRational a :- KR.KnownRational b) +rationalMagic1 f = Sub $ unsafeCoerce (RationalMagic Dict) + $ f (KR.rationalVal (Proxy @a)) + +negateRational + :: forall (a :: KR.Rational) + . (KR.KnownRational a) :- (KR.KnownRational (KR.Negate a)) +negateRational = rationalMagic1 negate + diff --git a/test/I/Test/Word8.hs b/test/I/Test/Word8.hs new file mode 100644 --- /dev/null +++ b/test/I/Test/Word8.hs @@ -0,0 +1,161 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} + +module I.Test.Word8 (tt) where + +import Control.Monad +import Data.Constraint +import Data.Proxy +import Data.Word +import Data.Type.Ord +import GHC.TypeLits qualified as L +import Hedgehog (failure, forAll, property, assert, (===), (/==)) +import qualified Hedgehog.Gen as Gen +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@=?)) +import Test.Tasty.Hedgehog (testProperty) + +import I (I) +import I qualified + +import I.Test.Support + +-------------------------------------------------------------------------------- + +-- checking some constants used below +_tt :: Dict (I.MinL Word8 ~ 0, I.MaxR Word8 ~ 255) +_tt = Dict + +tt :: TestTree +tt = testGroup "Word8" + [ testProperty "wrap" $ property $ do + x <- forAll genWord8 + x === I.unwrap (I.wrap x) + + , tt' @0 @0 + , tt' @0 @1 + , tt' @1 @1 + , tt' @100 @100 + , tt' @255 @255 + , tt' @0 @255 + , tt' @0 @100 + , tt' @100 @200 + , tt' @200 @255 + ] + +tt' + :: forall (l :: I.L Word8) (r :: I.R Word8) + . I.Interval Word8 l r + => TestTree +tt' = testGroup ("Interval [" <> show l <> ", " <> show r <> "]") + $ concat + [ pure $ testProperty "from" $ property $ do + x <- forAll genWord8 + case I.from @Word8 @l @r x of + Nothing -> assert (x < l' || x > r') + Just y -> do assert (x >= l' && x <= r') + I.unwrap y === x + + , pure $ testProperty "shove" $ property $ do + x <- forAll genWord8 + let y = I.shove @Word8 @l @r x + I.from (I.unwrap y) === Just y + if x < l' || x > r' + then I.from @Word8 @l @r x === Nothing + else I.from @Word8 @l @r x /== Nothing + + , pure $ testProperty "plus'" $ property $ do + a <- forAll $ genIWord8 @l @r + b <- forAll $ genIWord8 @l @r + let x = toInteger (I.unwrap a) + toInteger (I.unwrap b) + case I.plus' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "mult'" $ property $ do + a <- forAll $ genIWord8 @l @r + b <- forAll $ genIWord8 @l @r + let x = toInteger (I.unwrap a) * toInteger (I.unwrap b) + case I.mult' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , pure $ testProperty "minus'" $ property $ do + a <- forAll $ genIWord8 @l @r + b <- forAll $ genIWord8 @l @r + let x = toInteger (I.unwrap a) - toInteger (I.unwrap b) + case I.minus' a b of + Nothing -> assert (x < l'' || x > r'') + Just y -> toInteger (I.unwrap y) === x + + , if (l' == 0 && r' == 0) then mzero else + pure $ testProperty "div'" $ property $ do + a <- forAll $ genIWord8 @l @r + b <- forAll $ Gen.filter (\x -> I.unwrap x /= 0) (genIWord8 @l @r) + let (q, m) = toInteger (I.unwrap a) `divMod` toInteger (I.unwrap b) + case I.div' a b of + Nothing -> assert (q < l'' || q > r'' || m /= 0) + Just y -> do q === toInteger (I.unwrap y) + m === 0 + + , pure $ testProperty "clamp'" $ property $ do + x <- forAll $ genWord8 + case I.clamp @Word8 @l @r x of + y | x < l' -> I.unwrap y === l' + | x > r' -> I.unwrap y === r' + | otherwise -> Just y === I.from x + + , pure $ testProperty "with" $ property $ do + x <- forAll $ genIWord8 @l @r + x === I.with x I.known' + + , case L.cmpNat (Proxy @l) (Proxy @r) of + LTI -> + [ testProperty "pred'" $ property $ do + x <- forAll $ genIWord8 @l @r + case I.pred' x of + Nothing -> x === l + Just y -> do x /== l + I.unwrap y === I.unwrap x - 1 + , testProperty "succ'" $ property $ do + x <- forAll $ genIWord8 @l @r + case I.succ' x of + Nothing -> x === r + Just y -> do x /== r + I.unwrap y === I.unwrap x + 1 + ] + _ -> mzero + + , case L.cmpNat (Proxy @l) (Proxy @0) of + EQI -> pure $ testCase "zero" $ + 0 @=? I.unwrap (I.zero @Word8 @l @r) + _ -> mzero + + , case (leNatural @l @1, leNatural @1 @r) of + (Just Dict, Just Dict) -> pure $ testCase "one" $ do + 1 @=? I.unwrap (I.one @Word8 @l @r) + _ -> mzero + + , pure $ testProperty "negate'" $ property $ do + x <- forAll $ genIWord8 @l @r + Nothing === I.negate' x + + , pure $ testProperty "down" $ property $ do + x <- forAll $ genIWord8 @l @r + Just x === I.down x + case I.down x of + Nothing -> failure + Just y -> I.unwrap x + === I.unwrap (y :: I Word8 (I.MinL Word8) (I.MaxR Word8)) + + , pure $ testProperty "up" $ property $ do + x <- forAll $ genIWord8 @l @r + x === I.up x + I.unwrap x === I.unwrap (I.up x :: I Word8 (I.MinL Word8) (I.MaxR Word8)) + ] + where + l = I.min :: I Word8 l r + l' = I.unwrap l :: Word8 + l'' = toInteger l' :: Integer + r = I.max :: I Word8 l r + r' = I.unwrap r :: Word8 + r'' = toInteger r' :: Integer