i (empty) → 0.1

raw patch · 19 files changed

+5220/−0 lines, 19 filesdep +basedep +constraintsdep +hedgehogbuild-type:Customsetup-changed

Dependencies added: base, constraints, hedgehog, i, kind-integer, kind-rational, tasty, tasty-hedgehog, tasty-hunit

Files

• CHANGELOG.md +3/−0
• LICENSE +219/−0
• README.md +4/−0
• Setup.hs +116/−0
• hs/I.hs +95/−0
• hs/I/Int8.hs +112/−0
• hs/I/Integer.hs +352/−0
• hs/I/Internal.hs +770/−0
• hs/I/Natural.hs +200/−0
• hs/I/Rational.hs +688/−0
• hs/I/Word8.hs +98/−0
• i.cabal +130/−0
• test/I/Test/Int8.hs +194/−0
• test/I/Test/Integer.hs +565/−0
• test/I/Test/Main.hs +32/−0
• test/I/Test/Natural.hs +281/−0
• test/I/Test/Rational.hs +1036/−0
• test/I/Test/Support.hs +164/−0
• test/I/Test/Word8.hs +161/−0

@@ -0,0 +1,3 @@+# Version 0.1++* Initial version.

@@ -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.

@@ -0,0 +1,4 @@+# i++Haskell interval types.+

@@ -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++

@@ -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 ()+

@@ -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))+

@@ -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+

@@ -0,0 +1,770 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}++#include <MachDeps.h>+#include <HsBaseConfig.h>++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)+

@@ -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)+

@@ -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+

@@ -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))+

@@ -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,+

@@ -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++

@@ -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))++  ]+

@@ -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+  ]+

@@ -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+

@@ -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))++  ]+

@@ -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+

@@ -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