packages feed

natural-arithmetic 0.1.4.0 → 0.2.3.0

raw patch · 11 files changed

Files

CHANGELOG.md view
@@ -1,5 +1,44 @@ # Revision history for natural-arithmetic +## 0.2.3.0 -- 2025-06-12++* Add Fin.greatest#+* Add Plus.commutative#+* Add substitution functions for unlifted less-than-or-equal-to+* Add Nat.substitute#+* Add Eq.symmetric#+* Add nativeFrom32#+* Add incrementL#+* Add testLessThanEqual#+* Add nativeTo32#+* Add Fin.ascendFromToM_#+* Add Fin.weaken#++## 0.2.2.0 -- 2025-04-07++* Add Fin.weakenL#+* Add Fin.weakenR#+* Add Fin.demote32#+* Add Fin.constant#+* Add Fin.equals#+* Add more nat constants (N8192# and N16384#)+* Add EitherFin#++## 0.2.1.0 -- 2024-02-02++* Add `fromInt` and `fromInt#` to `Arithmetic.Fin`.+* Update package metadata.++## 0.2.0.0 -- 2024-01-09++* Change the types of `with#` and `construct#` (both in `Arithmetic.Fin`)+  to use an unboxed "less than" instead of a boxed one. This is a breaking+  change.+* Add patterns for the natural numbers 5, 6, 7.+* Add a lot of primitives for working with unboxed natural and inequalities.+  GHC is unable to eliminate the boxed `Fin` type in a suprisingly large+  number of cases, and `Fin#` helps a lot with this.+ ## 0.1.4.0 -- 2023-05-31  * Add unboxed Nat type
− Setup.hs 
@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain
natural-arithmetic.cabal view
@@ -1,7 +1,7 @@-cabal-version: 2.2-name: natural-arithmetic-version: 0.1.4.0-synopsis: Arithmetic of natural numbers+cabal-version:   2.2+name:            natural-arithmetic+version:         0.2.3.0+synopsis:        Arithmetic of natural numbers description:   A search for terms like `arithmetic` and `natural` on hackage reveals   no shortage of libraries for handling the arithmetic of natural@@ -18,7 +18,7 @@   application code, not in library code. This is because libraries   should not require the presence of typechecker plugins. Technically,   they can (you could document it), but many developers will not-  use libraries that have unusual install procedures like this. +  use libraries that have unusual install procedures like this.   .   This library, in places, requires users to use the 'TypeApplications`   language extension. This is done when a number is only need at@@ -28,7 +28,7 @@   in `Arithmetic.Lt` and `Arithmetic.Lte`. This is done in the interest   of making it easy for user to assemble proofs. Recall that proof   assembly is done by hand rather than by an SMT solver, so removing-  some tediousness from this is helpful to users. +  some tediousness from this is helpful to users.   .   This library provides left and variants variants of several functions.   For example, `Arithmetic.Lte` provides both `substituteL` and@@ -54,27 +54,41 @@   * Decrement: Decrease an upper bound along with the bounded value   .   * Substitute: Replace a number with an equal number-homepage: https://github.com/andrewthad/natural-arithmetic-bug-reports: https://github.com/andrewthad/natural-arithmetic/issues-license: BSD-3-Clause-license-file: LICENSE-author: Andrew Martin-maintainer: andrew.thaddeus@gmail.com-copyright: 2019 Andrew Martin-category: Math-extra-source-files: CHANGELOG.md +homepage:        https://github.com/byteverse/natural-arithmetic+bug-reports:     https://github.com/byteverse/natural-arithmetic/issues+license:         BSD-3-Clause+license-file:    LICENSE+author:          Andrew Martin+maintainer:      amartin@layer3com.com+copyright:       2019 Andrew Martin+category:        Math+extra-doc-files: CHANGELOG.md+tested-with:     GHC ==9.4.8 || ==9.6.3 || ==9.8.1++common build-settings+  default-language: Haskell2010+  ghc-options:      -Wall -Wunused-packages+ library+  import:          build-settings   exposed-modules:-    Arithmetic.Fin     Arithmetic.Equal+    Arithmetic.Fin     Arithmetic.Lt     Arithmetic.Lte     Arithmetic.Nat+    Arithmetic.Plus     Arithmetic.Types     Arithmetic.Unsafe-    Arithmetic.Plus-  build-depends: base>=4.14 && <5-  hs-source-dirs: src-  default-language: Haskell2010-  ghc-options: -Wall -O2++  build-depends:+    , base      >=4.14  && <5+    , unlifted  >=0.2.1++  hs-source-dirs:  src+  ghc-options:     -O2++source-repository head+  type:     git+  location: git://github.com/byteverse/natural-arithmetic.git
src/Arithmetic/Equal.hs view
@@ -1,25 +1,52 @@-{-# language DataKinds #-}-{-# language ExplicitForAll #-}-{-# language KindSignatures #-}-{-# language TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}  module Arithmetic.Equal   ( symmetric+  , symmetric#   , plusR   , plusL+  , plusR#+  , plusL#+  , lift+  , unlift   ) where -import Arithmetic.Unsafe (type (:=:)(Eq))+import Arithmetic.Unsafe (type (:=:) (Eq), type (:=:#) (Eq#)) import GHC.TypeNats (type (+))  symmetric :: (m :=: n) -> (n :=: m)-{-# inline symmetric #-}+{-# INLINE symmetric #-} symmetric Eq = Eq +symmetric# :: (m :=:# n) -> (n :=:# m)+{-# INLINE symmetric# #-}+symmetric# _ = Eq# (# #)+ plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n)-{-# inline plusL #-}+{-# INLINE plusL #-} plusL Eq = Eq  plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c)-{-# inline plusR #-}+{-# INLINE plusR #-} plusR Eq = Eq++plusL# :: forall c m n. (m :=:# n) -> (c + m :=:# c + n)+{-# INLINE plusL# #-}+plusL# _ = Eq# (# #)++plusR# :: forall c m n. (m :=:# n) -> (m + c :=:# n + c)+{-# INLINE plusR# #-}+plusR# _ = Eq# (# #)++lift :: (m :=:# n) -> (m :=: n)+{-# INLINE lift #-}+lift _ = Eq++unlift :: (m :=: n) -> (m :=:# n)+{-# INLINE unlift #-}+unlift _ = Eq# (# #)
src/Arithmetic/Fin.hs view
@@ -1,21 +1,32 @@-{-# language BangPatterns #-}-{-# language DataKinds #-}-{-# language ExplicitNamespaces #-}-{-# language GADTs #-}-{-# language KindSignatures #-}-{-# language MagicHash #-}-{-# language RankNTypes #-}-{-# language ScopedTypeVariables #-}-{-# language TypeApplications #-}-{-# language TypeOperators #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}+ module Arithmetic.Fin   ( -- * Modification     incrementL+  , incrementL#   , incrementR+  , incrementR#   , weaken+  , weaken#   , weakenL+  , weakenL#   , weakenR+  , weakenR#+  , succ+  , succ#+     -- * Traverse+     -- | These use the terms @ascend@ and @descend@ rather than the     -- more popular @l@ (left) and @r@ (right) that pervade the Haskell     -- ecosystem. The general rule is that ascending functions pair@@ -29,7 +40,9 @@   , ascendM#   , ascendM_   , ascendM_#+  , ascendFromToM_#   , descend+  , descend#   , descend'   , descendM   , descendM_@@ -37,160 +50,252 @@   , descending   , ascendingSlice   , descendingSlice+     -- * Absurdities   , absurd+     -- * Demote   , demote+  , demote#+  , demote32#+     -- * Deconstruct   , with   , with#+     -- * Construct   , construct#+  , nativeTo32#+  , nativeFrom32#+  , remInt#+  , remWord#+  , fromInt+  , fromInt#+  , constant#+  , greatest#++    -- * Compare+  , equals#++    -- * Substitute Bound+  , substitute#+     -- * Lift and Unlift   , lift   , unlift   ) where -import Prelude hiding (last)+import Prelude hiding (last, succ) -import Arithmetic.Nat ((<?))-import Arithmetic.Types (Fin(..),Fin#,Difference(..),Nat,Nat#,type (<), type (<=), type (:=:))-import GHC.Exts (Int(I#))-import GHC.TypeNats (type (+))+import Arithmetic.Nat ((<?),(<?#))+import Arithmetic.Types (Difference (..), Fin (..), Nat, Nat#, pattern MaybeFinJust#, pattern MaybeFinNothing#, type (:=:), type (<), type (<#), type (<=), (:=:#))+import Arithmetic.Types (type (<=#))+import Arithmetic.Unsafe (Fin# (Fin#), MaybeFin#, Nat# (Nat#), Fin32#(Fin32#))+import Data.Maybe.Void (pattern JustVoid#)+import GHC.Exts (Int (I#), Int32#, Int#, Word#, (+#), (==#))+import GHC.TypeNats (CmpNat, type (+)) +import qualified Arithmetic.Equal as Eq import qualified Arithmetic.Lt as Lt import qualified Arithmetic.Lte as Lte-import qualified Arithmetic.Equal as Eq import qualified Arithmetic.Nat as Nat import qualified Arithmetic.Plus as Plus import qualified Arithmetic.Unsafe as Unsafe+import qualified GHC.Exts as Exts+import qualified GHC.TypeNats as GHC --- | Raise the index by @m@ and weaken the bound by @m@, adding--- @m@ to the right-hand side of @n@.+{- | Raise the index by @m@ and weaken the bound by @m@, adding+@m@ to the right-hand side of @n@.+-} incrementR :: forall n m. Nat m -> Fin n -> Fin (n + m)-{-# inline incrementR #-}+{-# INLINE incrementR #-} incrementR m (Fin i pf) = Fin (Nat.plus i m) (Lt.incrementR @m pf) --- | Raise the index by @m@ and weaken the bound by @m@, adding--- @m@ to the left-hand side of @n@.+incrementR# :: forall n m. Nat# m -> Fin# n -> Fin# (n + m)+{-# INLINE incrementR# #-}+incrementR# (Nat# n) (Fin# i) = Fin# (n +# i)++{- | Raise the index by @m@ and weaken the bound by @m@, adding+@m@ to the left-hand side of @n@.+-} incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n)-{-# inline incrementL #-}+{-# INLINE incrementL #-} incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf) --- | Weaken the bound by @m@, adding it to the left-hand side of--- the existing bound. This does not change the index.+incrementL# :: forall n m. Nat# m -> Fin# n -> Fin# (m + n)+{-# INLINE incrementL# #-}+incrementL# (Nat# n) (Fin# i) = Fin# (n +# i)++{- | Weaken the bound by @m@, adding it to the left-hand side of+the existing bound. This does not change the index.+-} weakenL :: forall n m. Fin n -> Fin (m + n)-{-# inline weakenL #-}-weakenL (Fin i pf) = Fin i-  ( Lt.substituteR-    (Plus.commutative @n @m)-    (Lt.plus pf (Lte.zero @m))-  )+{-# INLINE weakenL #-}+weakenL (Fin i pf) =+  Fin+    i+    ( Lt.substituteR+        (Plus.commutative @n @m)+        (Lt.plus pf (Lte.zero @m))+    ) --- | Weaken the bound by @m@, adding it to the right-hand side of--- the existing bound. This does not change the index.+{- | Unboxed variant of 'weakenL'.+-}+weakenL# :: forall n m. Fin# n -> Fin# (m + n)+{-# INLINE weakenL# #-}+weakenL# (Fin# i) = Fin# i++{- | Weaken the bound by @m@, adding it to the right-hand side of+the existing bound. This does not change the index.+-} weakenR :: forall n m. Fin n -> Fin (n + m)-{-# inline weakenR #-}+{-# INLINE weakenR #-} weakenR (Fin i pf) = Fin i (Lt.plus pf Lte.zero) --- | Weaken the bound, replacing it by another number greater than--- or equal to itself. This does not change the index.+{- | Unboxed variant of 'weakenR'.+-}+weakenR# :: forall n m. Fin# n -> Fin# (n + m)+{-# INLINE weakenR# #-}+weakenR# (Fin# i) = Fin# i++{- | Weaken the bound, replacing it by another number greater than+or equal to itself. This does not change the index.+-} weaken :: forall n m. (n <= m) -> Fin n -> Fin m-{-# inline weaken #-}+{-# INLINE weaken #-} weaken lt (Fin i pf) = Fin i (Lt.transitiveNonstrictR pf lt) +weaken# :: forall n m. (n <=# m) -> Fin# n -> Fin# m+{-# INLINE weaken# #-}+weaken# _ (Fin# x) = Fin# x+ -- | A finite set of no values is impossible. absurd :: Fin 0 -> void-{-# inline absurd #-}+{-# INLINE absurd #-} absurd (Fin _ pf) = Lt.absurd pf --- | Fold over the numbers bounded by @n@ in descending--- order. This is lazy in the accumulator. For convenince,--- this differs from @foldr@ in the order of the parameters.------ > descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))-descend :: forall a n.-     Nat n -- ^ Upper bound-  -> a -- ^ Initial accumulator-  -> (Fin n -> a -> a) -- ^ Update accumulator-  -> a-{-# inline descend #-}+{- | Fold over the numbers bounded by @n@ in descending+order. This is lazy in the accumulator. For convenince,+this differs from @foldr@ in the order of the parameters.++> descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))+-}+descend ::+  forall a n.+  -- | Upper bound+  Nat n ->+  -- | Initial accumulator+  a ->+  -- | Update accumulator+  (Fin n -> a -> a) ->+  a+{-# INLINE descend #-} descend !n b0 f = go Nat.zero-  where+ where   go :: Nat m -> a   go !m = case m <? n of     Nothing -> b0     Just lt -> f (Fin m lt) (go (Nat.succ m)) --- | Fold over the numbers bounded by @n@ in descending--- order. This is strict in the accumulator. For convenince,--- this differs from @foldr'@ in the order of the parameters.------ > descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))-descend' :: forall a n.-     Nat n -- ^ Upper bound-  -> a -- ^ Initial accumulator-  -> (Fin n -> a -> a) -- ^ Update accumulator-  -> a-{-# inline descend' #-}+descend# ::+  forall a n.+  -- | Upper bound+  Nat# n ->+  -- | Initial accumulator+  a ->+  -- | Update accumulator+  (Fin# n -> a -> a) ->+  a+{-# INLINE descend# #-}+descend# !n b0 f = descend (Nat.lift n) b0 (\ix a -> f (unlift ix) a)++{- | Fold over the numbers bounded by @n@ in descending+order. This is strict in the accumulator. For convenince,+this differs from @foldr'@ in the order of the parameters.++> descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))+-}+descend' ::+  forall a n.+  -- | Upper bound+  Nat n ->+  -- | Initial accumulator+  a ->+  -- | Update accumulator+  (Fin n -> a -> a) ->+  a+{-# INLINE descend' #-} descend' !n !b0 f = go n Lte.reflexive b0-  where-    go :: Nat p -> p <= n -> a -> a-    go !m pLteEn !b = case Nat.monus m Nat.one of-      Nothing -> b-      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->-        let !cLtEn = descendLemma cPlusOneEqP pLteEn-        in go mpred (Lte.fromStrict cLtEn) (f (Fin mpred cLtEn) b)+ where+  go :: Nat p -> p <= n -> a -> a+  go !m pLteEn !b = case Nat.monus m Nat.one of+    Nothing -> b+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->+      let !cLtEn = descendLemma cPlusOneEqP pLteEn+       in go mpred (Lte.fromStrict cLtEn) (f (Fin mpred cLtEn) b) --- | Fold over the numbers bounded by @n@ in ascending order. This--- is lazy in the accumulator.------ > ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))-ascend :: forall a n.-     Nat n-  -> a-  -> (Fin n -> a -> a)-  -> a-{-# inline ascend #-}+{- | Fold over the numbers bounded by @n@ in ascending order. This+is lazy in the accumulator.++> ascend 4 z f = f 3 (f 2 (f 1 (f 0 z)))+-}+ascend ::+  forall a n.+  Nat n ->+  a ->+  (Fin n -> a -> a) ->+  a+{-# INLINE ascend #-} ascend !n !b0 f = go n Lte.reflexive-  where-    go :: Nat p -> (p <= n) -> a-    go !m pLteEn = case Nat.monus m Nat.one of-      Nothing -> b0-      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->-        let !cLtEn = descendLemma cPlusOneEqP pLteEn-        in f (Fin mpred cLtEn) (go mpred (Lte.fromStrict cLtEn))+ where+  go :: Nat p -> (p <= n) -> a+  go !m pLteEn = case Nat.monus m Nat.one of+    Nothing -> b0+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->+      let !cLtEn = descendLemma cPlusOneEqP pLteEn+       in f (Fin mpred cLtEn) (go mpred (Lte.fromStrict cLtEn)) --- | Strict fold over the numbers bounded by @n@ in ascending--- order. For convenince, this differs from @foldl'@ in the--- order of the parameters.------ > ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))-ascend' :: forall a n.-     Nat n -- ^ Upper bound-  -> a -- ^ Initial accumulator-  -> (Fin n -> a -> a) -- ^ Update accumulator-  -> a-{-# inline ascend' #-}+{- | Strict fold over the numbers bounded by @n@ in ascending+order. For convenince, this differs from @foldl'@ in the+order of the parameters.++> ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))+-}+ascend' ::+  forall a n.+  -- | Upper bound+  Nat n ->+  -- | Initial accumulator+  a ->+  -- | Update accumulator+  (Fin n -> a -> a) ->+  a+{-# INLINE ascend' #-} ascend' !n !b0 f = go Nat.zero b0-  where+ where   go :: Nat m -> a -> a   go !m !b = case m <? n of     Nothing -> b     Just lt -> go (Nat.succ m) (f (Fin m lt) b) --- | Generalization of @ascend'@ that lets the caller pick the starting index:------ > ascend' === ascendFrom' 0-ascendFrom' :: forall a m n.-     Nat m -- ^ Index to start at-  -> Nat n -- ^ Number of steps to take-  -> a -- ^ Initial accumulator-  -> (Fin (m + n) -> a -> a) -- ^ Update accumulator-  -> a-{-# inline ascendFrom' #-}+{- | Generalization of @ascend'@ that lets the caller pick the starting index:++> ascend' === ascendFrom' 0+-}+ascendFrom' ::+  forall a m n.+  -- | Index to start at+  Nat m ->+  -- | Number of steps to take+  Nat n ->+  -- | Initial accumulator+  a ->+  -- | Update accumulator+  (Fin (m + n) -> a -> a) ->+  a+{-# INLINE ascendFrom' #-} ascendFrom' !m0 !n !b0 f = go m0 b0-  where+ where   end = Nat.plus m0 n   go :: Nat k -> a -> a   go !m !b = case m <? end of@@ -198,223 +303,385 @@     Just lt -> go (Nat.succ m) (f (Fin m lt) b)  -- | Variant of @ascendFrom'@ with unboxed arguments.-ascendFrom'# :: forall a m n.-     Nat# m -- ^ Index to start at-  -> Nat# n -- ^ Number of steps to take-  -> a -- ^ Initial accumulator-  -> (Fin# (m + n) -> a -> a) -- ^ Update accumulator-  -> a-{-# inline ascendFrom'# #-}+ascendFrom'# ::+  forall a m n.+  -- | Index to start at+  Nat# m ->+  -- | Number of steps to take+  Nat# n ->+  -- | Initial accumulator+  a ->+  -- | Update accumulator+  (Fin# (m + n) -> a -> a) ->+  a+{-# INLINE ascendFrom'# #-} ascendFrom'# !m0 !n !b0 f = ascendFrom' (Nat.lift m0) (Nat.lift n) b0 (\ix -> f (unlift ix)) --- | Strict monadic left fold over the numbers bounded by @n@--- in ascending order. Roughly:------ > ascendM 4 z0 f =--- >   f 0 z0 >>= \z1 ->--- >   f 1 z1 >>= \z2 ->--- >   f 2 z2 >>= \z3 ->--- >   f 3 z3-ascendM :: forall m a n. Monad m-  => Nat n -- ^ Upper bound-  -> a -- ^ Initial accumulator-  -> (Fin n -> a -> m a) -- ^ Update accumulator-  -> m a-{-# inline ascendM #-}+{- | Strict monadic left fold over the numbers bounded by @n@+in ascending order. Roughly:++> ascendM 4 z0 f =+>   f 0 z0 >>= \z1 ->+>   f 1 z1 >>= \z2 ->+>   f 2 z2 >>= \z3 ->+>   f 3 z3+-}+ascendM ::+  forall m a n.+  (Monad m) =>+  -- | Upper bound+  Nat n ->+  -- | Initial accumulator+  a ->+  -- | Update accumulator+  (Fin n -> a -> m a) ->+  m a+{-# INLINE ascendM #-} ascendM !n !b0 f = go Nat.zero b0-  where+ where   go :: Nat p -> a -> m a   go !m !b = case m <? n of     Nothing -> pure b     Just lt -> go (Nat.succ m) =<< f (Fin m lt) b --- | Variant of @ascendM@ that takes an unboxed Nat and provides--- an unboxed Fin to the callback.-ascendM# :: forall m a n. Monad m-  => Nat# n -- ^ Upper bound-  -> a -- ^ Initial accumulator-  -> (Fin# n -> a -> m a) -- ^ Update accumulator-  -> m a-{-# inline ascendM# #-}+{- | Variant of @ascendM@ that takes an unboxed Nat and provides+an unboxed Fin to the callback.+-}+ascendM# ::+  forall m a n.+  (Monad m) =>+  -- | Upper bound+  Nat# n ->+  -- | Initial accumulator+  a ->+  -- | Update accumulator+  (Fin# n -> a -> m a) ->+  m a+{-# INLINE ascendM# #-} ascendM# n !a0 f = ascendM (Nat.lift n) a0 (\ix a -> f (unlift ix) a) --- | Monadic traversal of the numbers bounded by @n@--- in ascending order.------ > ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3-ascendM_ :: forall m a n. Applicative m-  => Nat n -- ^ Upper bound-  -> (Fin n -> m a) -- ^ Effectful interpretion-  -> m ()-{-# inline ascendM_ #-}+{- | Monadic traversal of the numbers bounded by @n@+in ascending order.++> ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3+-}+ascendM_ ::+  forall m a n.+  (Applicative m) =>+  -- | Upper bound+  Nat n ->+  -- | Effectful interpretion+  (Fin n -> m a) ->+  m ()+{-# INLINE ascendM_ #-} ascendM_ !n f = go Nat.zero-  where+ where   go :: Nat p -> m ()   go !m = case m <? n of     Nothing -> pure ()     Just lt -> f (Fin m lt) *> go (Nat.succ m) --- | Variant of @ascendM_@ that takes an unboxed Nat and provides--- an unboxed Fin to the callback.-ascendM_# :: forall m a n. Monad m-  => Nat# n -- ^ Upper bound-  -> (Fin# n -> m a) -- ^ Update accumulator-  -> m ()-{-# inline ascendM_# #-}+ascendFromToM_# ::+  forall m a i n.+  (Monad m) =>+  -- | Index to start at (inclusive)+  Nat# i ->+  -- | Upper bound (exclusive)+  Nat# n ->+  -- | Update accumulator+  (Fin# n -> m a) ->+  m ()+ascendFromToM_# m0 end f = go m0+  where+  go :: forall k. Nat# k -> m ()+  go m = case m <?# end of+    JustVoid# lt -> f (construct# lt m) *> go (Nat.succ# m)+    _ -> pure ()++{- | Variant of @ascendM_@ that takes an unboxed Nat and provides+an unboxed Fin to the callback.+-}+ascendM_# ::+  forall m a n.+  (Monad m) =>+  -- | Upper bound+  Nat# n ->+  -- | Update accumulator+  (Fin# n -> m a) ->+  m ()+{-# INLINE ascendM_# #-} ascendM_# n f = ascendM_ (Nat.lift n) (\ix -> f (unlift ix))  descendLemma :: forall a b c. a + 1 :=: b -> b <= c -> a < c-{-# inline descendLemma #-}-descendLemma !aPlusOneEqB !bLteC = id-  $ Lt.transitiveNonstrictR-      (Lt.substituteR (Plus.commutative @1 @a)-      (Lt.plus Lt.zero Lte.reflexive))-  $ Lte.substituteL (Eq.symmetric aPlusOneEqB) bLteC+{-# INLINE descendLemma #-}+descendLemma !aPlusOneEqB !bLteC =+  id+    $ Lt.transitiveNonstrictR+      ( Lt.substituteR+          (Plus.commutative @1 @a)+          (Lt.plus Lt.zero Lte.reflexive)+      )+    $ Lte.substituteL (Eq.symmetric aPlusOneEqB) bLteC --- | Strict monadic left fold over the numbers bounded by @n@--- in descending order. Roughly:------ > descendM 4 z f =--- >   f 3 z0 >>= \z1 ->--- >   f 2 z1 >>= \z2 ->--- >   f 1 z2 >>= \z3 ->--- >   f 0 z3-descendM :: forall m a n. Monad m-  => Nat n-  -> a-  -> (Fin n -> a -> m a)-  -> m a-{-# inline descendM #-}+{- | Strict monadic left fold over the numbers bounded by @n@+in descending order. Roughly:++> descendM 4 z f =+>   f 3 z0 >>= \z1 ->+>   f 2 z1 >>= \z2 ->+>   f 1 z2 >>= \z3 ->+>   f 0 z3+-}+descendM ::+  forall m a n.+  (Monad m) =>+  Nat n ->+  a ->+  (Fin n -> a -> m a) ->+  m a+{-# INLINE descendM #-} descendM !n !b0 f = go n Lte.reflexive b0-  where-    go :: Nat p -> p <= n -> a -> m a-    go !m pLteEn !b = case Nat.monus m Nat.one of-      Nothing -> pure b-      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->-        let !cLtEn = descendLemma cPlusOneEqP pLteEn-        in go mpred (Lte.fromStrict cLtEn) =<< f (Fin mpred cLtEn) b+ where+  go :: Nat p -> p <= n -> a -> m a+  go !m pLteEn !b = case Nat.monus m Nat.one of+    Nothing -> pure b+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->+      let !cLtEn = descendLemma cPlusOneEqP pLteEn+       in go mpred (Lte.fromStrict cLtEn) =<< f (Fin mpred cLtEn) b --- | Monadic traversal of the numbers bounded by @n@--- in descending order.------ > descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0-descendM_ :: forall m a n. Applicative m-  => Nat n -- ^ Upper bound-  -> (Fin n -> m a) -- ^ Effectful interpretion-  -> m ()-{-# inline descendM_ #-}+{- | Monadic traversal of the numbers bounded by @n@+in descending order.++> descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0+-}+descendM_ ::+  forall m a n.+  (Applicative m) =>+  -- | Upper bound+  Nat n ->+  -- | Effectful interpretion+  (Fin n -> m a) ->+  m ()+{-# INLINE descendM_ #-} descendM_ !n f = go n Lte.reflexive-  where+ where   go :: Nat p -> p <= n -> m ()   go !m !pLteEn = case Nat.monus m Nat.one of     Nothing -> pure ()     Just (Difference (mpred :: Nat c) cPlusOneEqP) ->       let !cLtEn = descendLemma cPlusOneEqP pLteEn-      in f (Fin mpred cLtEn) *> go mpred (Lte.fromStrict cLtEn)+       in f (Fin mpred cLtEn) *> go mpred (Lte.fromStrict cLtEn) --- | Generate all values of a finite set in ascending order.------ >>> ascending (Nat.constant @3)--- [Fin 0,Fin 1,Fin 2]+{- | Generate all values of a finite set in ascending order.++>>> ascending (Nat.constant @3)+[Fin 0,Fin 1,Fin 2]+-} ascending :: forall n. Nat n -> [Fin n] ascending !n = go Nat.zero-  where+ where   go :: Nat m -> [Fin n]   go !m = case m <? n of     Nothing -> []     Just lt -> Fin m lt : go (Nat.succ m) --- | Generate all values of a finite set in descending order.------ >>> descending (Nat.constant @3)--- [Fin 2,Fin 1,Fin 0]+{- | Generate all values of a finite set in descending order.++>>> descending (Nat.constant @3)+[Fin 2,Fin 1,Fin 0]+-} descending :: forall n. Nat n -> [Fin n] descending !n = go n Lte.reflexive-  where-    go :: Nat p -> (p <= n) -> [Fin n]-    go !m !pLteEn = case Nat.monus m Nat.one of-      Nothing -> []-      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->-        let !cLtEn = descendLemma cPlusOneEqP pLteEn-        in Fin mpred cLtEn : go mpred (Lte.fromStrict cLtEn)+ where+  go :: Nat p -> (p <= n) -> [Fin n]+  go !m !pLteEn = case Nat.monus m Nat.one of+    Nothing -> []+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->+      let !cLtEn = descendLemma cPlusOneEqP pLteEn+       in Fin mpred cLtEn : go mpred (Lte.fromStrict cLtEn) --- | Generate 'len' values starting from 'off' in ascending order.------ >>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)--- [Fin 2,Fin 3,Fin 4]-ascendingSlice-  :: forall n off len-  .  Nat off-  -> Nat len-  -> off + len <= n-  -> [Fin n]-{-# inline ascendingSlice #-}+{- | Generate 'len' values starting from 'off' in ascending order.++>>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)+[Fin 2,Fin 3,Fin 4]+-}+ascendingSlice ::+  forall n off len.+  Nat off ->+  Nat len ->+  off + len <= n ->+  [Fin n]+{-# INLINE ascendingSlice #-} ascendingSlice off len !offPlusLenLteEn = go Nat.zero-  where-    go :: Nat m -> [Fin n]-    go !m = case m <? len of-      Nothing -> []-      Just emLtLen ->-        let !offPlusEmLtOffPlusLen = Lt.incrementL @off emLtLen-            !offPlusEmLtEn = Lt.transitiveNonstrictR offPlusEmLtOffPlusLen offPlusLenLteEn-         in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m)+ where+  go :: Nat m -> [Fin n]+  go !m = case m <? len of+    Nothing -> []+    Just emLtLen ->+      let !offPlusEmLtOffPlusLen = Lt.incrementL @off emLtLen+          !offPlusEmLtEn = Lt.transitiveNonstrictR offPlusEmLtOffPlusLen offPlusLenLteEn+       in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m) --- | Generate 'len' values starting from 'off + len - 1' in descending order.------ >>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)--- [Fin 4,Fin 3,Fin 2]-descendingSlice-  :: forall n off len-  .  Nat off-  -> Nat len-  -> off + len <= n-  -> [Fin n]-{-# inline descendingSlice #-}+{- | Generate 'len' values starting from 'off + len - 1' in descending order.++>>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)+[Fin 4,Fin 3,Fin 2]+-}+descendingSlice ::+  forall n off len.+  Nat off ->+  Nat len ->+  off + len <= n ->+  [Fin n]+{-# INLINE descendingSlice #-} descendingSlice !off !len !offPlusLenLteEn =   go len Lte.reflexive-  where-    go :: Nat m -> m <= len -> [Fin n]-    go !m !mLteEn = case Nat.monus m Nat.one of-      Nothing -> []-      Just (Difference (mpred :: Nat c) cPlusOneEqEm) ->-        let !cLtLen = Lt.transitiveNonstrictR+ where+  go :: Nat m -> m <= len -> [Fin n]+  go !m !mLteEn = case Nat.monus m Nat.one of+    Nothing -> []+    Just (Difference (mpred :: Nat c) cPlusOneEqEm) ->+      let !cLtLen =+            Lt.transitiveNonstrictR               (Lt.substituteR (Plus.commutative @1 @c) (Lt.plus Lt.zero Lte.reflexive))               -- c < c + 1               (Lte.substituteL (Eq.symmetric cPlusOneEqEm) mLteEn)-              -- c + 1 <= len-            !cPlusOffLtEn = Lt.transitiveNonstrictR-              (Lt.substituteR-                (Plus.commutative @len @off)-                (Lt.plus cLtLen (Lte.reflexive @off)))+          -- c + 1 <= len+          !cPlusOffLtEn =+            Lt.transitiveNonstrictR+              ( Lt.substituteR+                  (Plus.commutative @len @off)+                  (Lt.plus cLtLen (Lte.reflexive @off))+              )               -- c + off < off + len               offPlusLenLteEn-        in Fin (mpred `Nat.plus` off) cPlusOffLtEn : go mpred (Lte.fromStrict cLtLen)+       in Fin (mpred `Nat.plus` off) cPlusOffLtEn : go mpred (Lte.fromStrict cLtLen) --- | Extract the 'Int' from a 'Fin n'. This is intended to be used--- at a boundary where a safe interface meets the unsafe primitives--- on top of which it is built.+{- | Extract the 'Int' from a 'Fin n'. This is intended to be used+at a boundary where a safe interface meets the unsafe primitives+on top of which it is built.+-} demote :: Fin n -> Int-{-# inline demote #-}+{-# INLINE demote #-} demote (Fin i _) = Nat.demote i +demote# :: Fin# n -> Int#+{-# INLINE demote# #-}+demote# (Fin# i) = i++demote32# :: Fin32# n -> Int32#+{-# INLINE demote32# #-}+demote32# (Fin32# i) = i+ lift :: Unsafe.Fin# n -> Fin n-{-# inline lift #-}+{-# INLINE lift #-} lift (Unsafe.Fin# i) = Fin (Unsafe.Nat (I# i)) Unsafe.Lt  unlift :: Fin n -> Unsafe.Fin# n-{-# inline unlift #-}+{-# INLINE unlift #-} unlift (Fin (Unsafe.Nat (I# i)) _) = Unsafe.Fin# i  -- | Consume the natural number and the proof in the Fin. with :: Fin n -> (forall i. (i < n) -> Nat i -> a) -> a-{-# inline with #-}+{-# INLINE with #-} with (Fin i lt) f = f lt i  -- | Variant of 'with' for unboxed argument and result types.-with# :: Fin# n -> (forall i. (i < n) -> Nat# i -> a) -> a-{-# inline with# #-}-with# (Unsafe.Fin# i) f = f Unsafe.Lt (Unsafe.Nat# i)+with# :: Fin# n -> (forall i. (i <# n) -> Nat# i -> a) -> a+{-# INLINE with# #-}+with# (Unsafe.Fin# i) f = f (Unsafe.Lt# (# #)) (Unsafe.Nat# i) -construct# :: (i < n) -> Nat# i -> Fin# n-{-# inline construct# #-}+construct# :: (i <# n) -> Nat# i -> Fin# n+{-# INLINE construct# #-} construct# _ (Unsafe.Nat# x) = Unsafe.Fin# x++{- | Return the successor of the Fin or return nothing if the+argument is the greatest inhabitant.+-}+succ :: Nat n -> Fin n -> Maybe (Fin n)+{-# INLINE succ #-}+succ n (Fin ix _) = case ix' <? n of+  Nothing -> Nothing+  Just lt -> Just (Fin ix' lt)+ where+  ix' = Nat.succ ix++-- | Variant of 'succ' for unlifted finite numbers.+succ# :: Nat# n -> Fin# n -> MaybeFin# n+{-# INLINE succ# #-}+succ# (Nat# n) (Fin# ix) = case ix' Exts.<# n of+  0# -> MaybeFinNothing#+  _ -> MaybeFinJust# (Fin# ix')+ where+  !ix' = ix +# 1#++{- | Convert an Int to a finite number, testing that it is+less than the upper bound. This crashes with an uncatchable+exception when given a negative number.+-}+fromInt ::+  -- | exclusive upper bound+  Nat n ->+  Int ->+  Maybe (Fin n)+{-# INLINE fromInt #-}+fromInt bound i+  | i < 0 = errorWithoutStackTrace "Arithmetic.Fin.fromInt: negative argument"+  | otherwise = Nat.with i $ \number -> case number <? bound of+      Just lt -> Just (Fin number lt)+      Nothing -> Nothing++-- | Unboxed variant of 'fromInt'.+fromInt# ::+  -- | exclusive upper bound+  Nat# n ->+  Int# ->+  MaybeFin# n+{-# INLINE fromInt# #-}+fromInt# (Nat# n) i+  | Exts.isTrue# (i Exts.<# 0#) =+      errorWithoutStackTrace "Arithmetic.Fin.fromInt#: negative argument"+  | Exts.isTrue# (i Exts.<# n) = MaybeFinJust# (Fin# i)+  | otherwise = MaybeFinNothing#++{- | This crashes if @n = 0@. Divides @i@ by @n@ and takes+the remainder.+-}+remInt# :: Int# -> Nat# n -> Fin# n+remInt# i (Nat# n) = case n of+  0# -> errorWithoutStackTrace "Arithmetic.Fin.remInt#: cannot divide by zero"+  _ -> Fin# (Exts.remInt# i n)++{- | This crashes if @n = 0@. Divides @i@ by @n@ and takes+the remainder.+-}+remWord# :: Word# -> Nat# n -> Fin# n+remWord# w (Nat# n) = case n of+  0# -> errorWithoutStackTrace "Arithmetic.Fin.remWord#: cannot divide by zero"+  _ -> Fin# (Exts.word2Int# (Exts.remWord# w (Exts.int2Word# n)))++nativeTo32# :: (n <=# 2147483648) -> Fin# n -> Fin32# n+{-# inline nativeTo32# #-}+nativeTo32# _ (Fin# x) = Fin32# (Exts.intToInt32# x)++nativeFrom32# :: Fin32# n -> Fin# n+{-# inline nativeFrom32# #-}+nativeFrom32# (Fin32# x) = Fin# (Exts.int32ToInt# x)++{- | Create an unlifted finite number from an unlifted natural number.+The upper bound is the first type argument so that user can use+type applications to clarify when it is helpful. For example:++>>> Fin.constant# @10 N4#+-}+constant# :: forall (b :: GHC.Nat) (a :: GHC.Nat). (CmpNat a b ~ 'LT) => Nat# a -> Fin# b+constant# (Nat# i) = Fin# i++equals# :: Fin# n -> Fin# n -> Bool+equals# (Fin# a) (Fin# b) = Exts.isTrue# (a ==# b)++substitute# :: (m :=:# n) -> Fin# m -> Fin# n+substitute# _ (Fin# x) = Fin# x++greatest# :: Nat# n -> Fin# (n + 1)+greatest# (Nat# i) = Fin# i
src/Arithmetic/Lt.hs view
@@ -1,155 +1,294 @@-{-# language AllowAmbiguousTypes #-}-{-# language DataKinds #-}-{-# language ExplicitForAll #-}-{-# language KindSignatures #-}-{-# language TypeFamilies #-}-{-# language TypeOperators #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}  module Arithmetic.Lt   ( -- * Special Inequalities     zero+  , zero#+     -- * Substitution   , substituteL   , substituteR+     -- * Increment   , incrementL+  , incrementL#   , incrementR+  , incrementR#+     -- * Decrement   , decrementL+  , decrementL#   , decrementR+  , decrementR#+     -- * Weaken   , weakenL+  , weakenL#   , weakenR+  , weakenR#+  , weakenLhsL#+  , weakenLhsR#+     -- * Composition   , plus+  , plus#   , transitive+  , transitive#   , transitiveNonstrictL+  , transitiveNonstrictL#   , transitiveNonstrictR+  , transitiveNonstrictR#+     -- * Multiplication and Division   , reciprocalA   , reciprocalB+     -- * Convert to Inequality   , toLteL   , toLteR+     -- * Absurdities   , absurd+     -- * Integration with GHC solver   , constant+  , constant#++    -- * Lift and Unlift+  , lift+  , unlift   ) where -import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))-import Arithmetic.Unsafe (type (<=)(Lte))-import GHC.TypeNats (CmpNat,type (+))+import Arithmetic.Unsafe (type (:=:) (Eq), type (<) (Lt), type (<#) (Lt#), type (<=) (Lte), type (<=#))+import GHC.TypeNats (CmpNat, type (+))  import qualified GHC.TypeNats as GHC  toLteR :: (a < b) -> (a + 1 <= b)-{-# inline toLteR #-}+{-# INLINE toLteR #-} toLteR Lt = Lte  toLteL :: (a < b) -> (1 + a <= b)-{-# inline toLteL #-}+{-# INLINE toLteL #-} toLteL Lt = Lte --- | Replace the left-hand side of a strict inequality--- with an equal number.+{- | Replace the left-hand side of a strict inequality+with an equal number.+-} substituteL :: (b :=: c) -> (b < a) -> (c < a)-{-# inline substituteL #-}+{-# INLINE substituteL #-} substituteL Eq Lt = Lt --- | Replace the right-hand side of a strict inequality--- with an equal number.+{- | Replace the right-hand side of a strict inequality+with an equal number.+-} substituteR :: (b :=: c) -> (a < b) -> (a < c)-{-# inline substituteR #-}+{-# INLINE substituteR #-} substituteR Eq Lt = Lt  -- | Add a strict inequality to a nonstrict inequality. plus :: (a < b) -> (c <= d) -> (a + c < b + d)-{-# inline plus #-}+{-# INLINE plus #-} plus Lt Lte = Lt --- | Add a constant to the left-hand side of both sides of--- the strict inequality.-incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a < b) -> (c + a < c + b)-{-# inline incrementL #-}+plus# :: (a <# b) -> (c <=# d) -> (a + c <# b + d)+{-# INLINE plus# #-}+plus# _ _ = Lt# (# #)++{- | Add a constant to the left-hand side of both sides of+the strict inequality.+-}+incrementL ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a < b) ->+  (c + a < c + b)+{-# INLINE incrementL #-} incrementL Lt = Lt --- | Add a constant to the right-hand side of both sides of--- the strict inequality.-incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a < b) -> (a + c < b + c)-{-# inline incrementR #-}+incrementL# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <# b) ->+  (c + a <# c + b)+{-# INLINE incrementL# #-}+incrementL# _ = Lt# (# #)++{- | Add a constant to the right-hand side of both sides of+the strict inequality.+-}+incrementR ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a < b) ->+  (a + c < b + c)+{-# INLINE incrementR #-} incrementR Lt = Lt --- | Subtract a constant from the left-hand side of both sides of--- the inequality. This is the opposite of 'incrementL'.-decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (c + a < c + b) -> (a < b)-{-# inline decrementL #-}+incrementR# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <# b) ->+  (a + c <# b + c)+{-# INLINE incrementR# #-}+incrementR# _ = Lt# (# #)++{- | Subtract a constant from the left-hand side of both sides of+the inequality. This is the opposite of 'incrementL'.+-}+decrementL ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (c + a < c + b) ->+  (a < b)+{-# INLINE decrementL #-} decrementL Lt = Lt --- | Subtract a constant from the right-hand side of both sides of--- the inequality. This is the opposite of 'incrementR'.-decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a + c < b + c) -> (a < b)-{-# inline decrementR #-}+decrementL# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  ((c + a) <# (c + b)) ->+  (a <# b)+{-# INLINE decrementL# #-}+decrementL# _ = Lt# (# #)++{- | Subtract a constant from the right-hand side of both sides of+the inequality. This is the opposite of 'incrementR'.+-}+decrementR ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a + c < b + c) ->+  (a < b)+{-# INLINE decrementR #-} decrementR Lt = Lt --- | Add a constant to the left-hand side of the right-hand side of--- the strict inequality.-weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a < b) -> (a < c + b)-{-# inline weakenL #-}+decrementR# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a + c <# b + c) ->+  (a <# b)+{-# INLINE decrementR# #-}+decrementR# _ = Lt# (# #)++{- | Add a constant to the left-hand side of the right-hand side of+the strict inequality.+-}+weakenL ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a < b) ->+  (a < c + b)+{-# INLINE weakenL #-} weakenL Lt = Lt --- | Add a constant to the right-hand side of the right-hand side of--- the strict inequality.-weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a < b) -> (a < b + c)-{-# inline weakenR #-}+weakenL# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <# b) ->+  (a <# c + b)+{-# INLINE weakenL# #-}+weakenL# _ = Lt# (# #)++weakenLhsL# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (c + a <# b) ->+  (a <# b)+{-# INLINE weakenLhsL# #-}+weakenLhsL# _ = Lt# (# #)++weakenLhsR# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a + c <# b) ->+  (a <# b)+{-# INLINE weakenLhsR# #-}+weakenLhsR# _ = Lt# (# #)++{- | Add a constant to the right-hand side of the right-hand side of+the strict inequality.+-}+weakenR ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a < b) ->+  (a < b + c)+{-# INLINE weakenR #-} weakenR Lt = Lt +weakenR# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <# b) ->+  (a <# b + c)+{-# INLINE weakenR# #-}+weakenR# _ = Lt# (# #)+ -- | Compose two strict inequalities using transitivity. transitive :: (a < b) -> (b < c) -> (a < c)-{-# inline transitive #-}+{-# INLINE transitive #-} transitive Lt Lt = Lt --- | Compose a strict inequality (the first argument) with a nonstrict--- inequality (the second argument).+transitive# :: (a <# b) -> (b <# c) -> (a <# c)+{-# INLINE transitive# #-}+transitive# _ _ = Lt# (# #)++{- | Compose a strict inequality (the first argument) with a nonstrict+inequality (the second argument).+-} transitiveNonstrictR :: (a < b) -> (b <= c) -> (a < c)-{-# inline transitiveNonstrictR #-}+{-# INLINE transitiveNonstrictR #-} transitiveNonstrictR Lt Lte = Lt +transitiveNonstrictR# :: (a <# b) -> (b <=# c) -> (a <# c)+{-# INLINE transitiveNonstrictR# #-}+transitiveNonstrictR# _ _ = Lt# (# #)+ transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c)-{-# inline transitiveNonstrictL #-}+{-# INLINE transitiveNonstrictL #-} transitiveNonstrictL Lte Lt = Lt +transitiveNonstrictL# :: (a <=# b) -> (b <# c) -> (a <# c)+{-# INLINE transitiveNonstrictL# #-}+transitiveNonstrictL# _ _ = Lt# (# #)+ -- | Zero is less than one. zero :: 0 < 1-{-# inline zero #-}+{-# INLINE zero #-} zero = Lt +zero# :: (# #) -> 0 <# 1+{-# INLINE zero# #-}+zero# _ = Lt# (# #)+ -- | Nothing is less than zero. absurd :: n < 0 -> void-{-# inline absurd #-}+{-# INLINE absurd #-} absurd Lt = errorWithoutStackTrace "Arithmetic.Nat.absurd: n < 0" --- | Use GHC's built-in type-level arithmetic to prove--- that one number is less than another. The type-checker--- only reduces 'CmpNat' if both arguments are constants.+{- | Use GHC's built-in type-level arithmetic to prove+that one number is less than another. The type-checker+only reduces 'CmpNat' if both arguments are constants.+-} constant :: forall a b. (CmpNat a b ~ 'LT) => (a < b)-{-# inline constant #-}+{-# INLINE constant #-} constant = Lt +constant# :: forall a b. (CmpNat a b ~ 'LT) => (# #) -> (a <# b)+{-# INLINE constant# #-}+constant# _ = Lt# (# #)+ -- | Given that @m < n/p@, we know that @p*m < n@.-reciprocalA :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).-  (m < GHC.Div n p) -> (p GHC.* m) < n-{-# inline reciprocalA #-}+reciprocalA ::+  forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).+  (m < GHC.Div n p) ->+  (p GHC.* m) < n+{-# INLINE reciprocalA #-} reciprocalA _ = Lt  -- | Given that @m < roundUp(n/p)@, we know that @p*m < n@.-reciprocalB :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).-  (m < GHC.Div (n GHC.- 1) p + 1) -> (p GHC.* m) < n-{-# inline reciprocalB #-}+reciprocalB ::+  forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).+  (m < GHC.Div (n GHC.- 1) p + 1) ->+  (p GHC.* m) < n+{-# INLINE reciprocalB #-} reciprocalB _ = Lt++unlift :: (a < b) -> (a <# b)+unlift _ = Lt# (# #)++lift :: (a <# b) -> (a < b)+lift _ = Lt
src/Arithmetic/Lte.hs view
@@ -1,127 +1,257 @@-{-# language DataKinds #-}-{-# language ExplicitForAll #-}-{-# language KindSignatures #-}-{-# language TypeFamilies #-}-{-# language TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}  module Arithmetic.Lte   ( -- * Special Inequalities     zero   , reflexive+  , reflexive#+     -- * Substitution   , substituteL+  , substituteL#   , substituteR+  , substituteR#+     -- * Increment   , incrementL+  , incrementL#   , incrementR+  , incrementR#+     -- * Decrement   , decrementL+  , decrementL#   , decrementR+  , decrementR#+     -- * Weaken   , weakenL+  , weakenL#   , weakenR+  , weakenR#+     -- * Composition   , transitive+  , transitive#   , plus+  , plus#+     -- * Convert Strict Inequality   , fromStrict+  , fromStrict#+  , fromStrictSucc+  , fromStrictSucc#+     -- * Integration with GHC solver   , constant++    -- * Lift and Unlift+  , lift+  , unlift   ) where -import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))-import Arithmetic.Unsafe (type (<=)(Lte))-import GHC.TypeNats (CmpNat,type (+))+import Arithmetic.Unsafe (type (:=:) (Eq), type (<) (Lt), type (<#), type (<=) (Lte), type (<=#) (Lte#))+import Arithmetic.Unsafe (type (:=:#))+import GHC.TypeNats (CmpNat, type (+))  import qualified GHC.TypeNats as GHC --- | Replace the left-hand side of a strict inequality--- with an equal number.+{- | Replace the left-hand side of a strict inequality+with an equal number.+-} substituteL :: (b :=: c) -> (b <= a) -> (c <= a)-{-# inline substituteL #-}+{-# INLINE substituteL #-} substituteL Eq Lte = Lte --- | Replace the right-hand side of a strict inequality--- with an equal number.+{- | Replace the right-hand side of a strict inequality+with an equal number.+-} substituteR :: (b :=: c) -> (a <= b) -> (a <= c)-{-# inline substituteR #-}+{-# INLINE substituteR #-} substituteR Eq Lte = Lte +substituteL# :: (b :=:# c) -> (b <=# a) -> (c <=# a)+{-# INLINE substituteL# #-}+substituteL# _ _ = Lte# (# #)++substituteR# :: (b :=:# c) -> (a <=# b) -> (a <=# c)+{-# INLINE substituteR# #-}+substituteR# _ _ = Lte# (# #)+ -- | Add two inequalities. plus :: (a <= b) -> (c <= d) -> (a + c <= b + d)-{-# inline plus #-}+{-# INLINE plus #-} plus Lte Lte = Lte +plus# :: (a <=# b) -> (c <=# d) -> (a + c <=# b + d)+{-# INLINE plus# #-}+plus# _ _ = Lte# (# #)+ -- | Compose two inequalities using transitivity. transitive :: (a <= b) -> (b <= c) -> (a <= c)-{-# inline transitive #-}+{-# INLINE transitive #-} transitive Lte Lte = Lte +transitive# :: (a <=# b) -> (b <=# c) -> (a <=# c)+{-# INLINE transitive# #-}+transitive# _ _ = Lte# (# #)+ -- | Any number is less-than-or-equal-to itself. reflexive :: a <= a-{-# inline reflexive #-}+{-# INLINE reflexive #-} reflexive = Lte --- | Add a constant to the left-hand side of both sides of--- the inequality.-incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a <= b) -> (c + a <= c + b)-{-# inline incrementL #-}+reflexive# :: (# #) -> a <=# a+{-# INLINE reflexive# #-}+reflexive# _ = Lte# (# #)++{- | Add a constant to the left-hand side of both sides of+the inequality.+-}+incrementL ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <= b) ->+  (c + a <= c + b)+{-# INLINE incrementL #-} incrementL Lte = Lte --- | Add a constant to the right-hand side of both sides of--- the inequality.-incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a <= b) -> (a + c <= b + c)-{-# inline incrementR #-}+incrementL# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <=# b) ->+  (c + a <=# c + b)+{-# INLINE incrementL# #-}+incrementL# _ = Lte# (# #)++{- | Add a constant to the right-hand side of both sides of+the inequality.+-}+incrementR ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <= b) ->+  (a + c <= b + c)+{-# INLINE incrementR #-} incrementR Lte = Lte --- | Add a constant to the left-hand side of the right-hand side of--- the inequality.-weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a <= b) -> (a <= c + b)-{-# inline weakenL #-}+incrementR# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <=# b) ->+  (a + c <=# b + c)+{-# INLINE incrementR# #-}+incrementR# _ = Lte# (# #)++{- | Add a constant to the left-hand side of the right-hand side of+the inequality.+-}+weakenL ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <= b) ->+  (a <= c + b)+{-# INLINE weakenL #-} weakenL Lte = Lte --- | Add a constant to the right-hand side of the right-hand side of--- the inequality.-weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a <= b) -> (a <= b + c)-{-# inline weakenR #-}+weakenL# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <=# b) ->+  (a <=# c + b)+{-# INLINE weakenL# #-}+weakenL# _ = Lte# (# #)++{- | Add a constant to the right-hand side of the right-hand side of+the inequality.+-}+weakenR ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <= b) ->+  (a <= b + c)+{-# INLINE weakenR #-} weakenR Lte = Lte --- | Subtract a constant from the left-hand side of both sides of--- the inequality. This is the opposite of 'incrementL'.-decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (c + a <= c + b) -> (a <= b)-{-# inline decrementL #-}+weakenR# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a <=# b) ->+  (a <=# b + c)+{-# INLINE weakenR# #-}+weakenR# _ = Lte# (# #)++{- | Subtract a constant from the left-hand side of both sides of+the inequality. This is the opposite of 'incrementL'.+-}+decrementL ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (c + a <= c + b) ->+  (a <= b)+{-# INLINE decrementL #-} decrementL Lte = Lte --- | Subtract a constant from the right-hand side of both sides of--- the inequality. This is the opposite of 'incrementR'.-decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).-  (a + c <= b + c) -> (a <= b)-{-# inline decrementR #-}+decrementL# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (c + a <=# c + b) ->+  (a <=# b)+{-# INLINE decrementL# #-}+decrementL# _ = Lte# (# #)++{- | Subtract a constant from the right-hand side of both sides of+the inequality. This is the opposite of 'incrementR'.+-}+decrementR ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a + c <= b + c) ->+  (a <= b)+{-# INLINE decrementR #-} decrementR Lte = Lte +decrementR# ::+  forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat).+  (a + c <=# b + c) ->+  (a <=# b)+{-# INLINE decrementR# #-}+decrementR# _ = Lte# (# #)+ -- | Weaken a strict inequality to a non-strict inequality. fromStrict :: (a < b) -> (a <= b)-{-# inline fromStrict #-}+{-# INLINE fromStrict #-} fromStrict Lt = Lte +fromStrict# :: (a <# b) -> (a <=# b)+{-# INLINE fromStrict# #-}+fromStrict# _ = Lte# (# #)++{- | Weaken a strict inequality to a non-strict inequality, incrementing+the right-hand argument by one.+-}+fromStrictSucc :: (a < b) -> (a + 1 <= b)+{-# INLINE fromStrictSucc #-}+fromStrictSucc Lt = Lte++fromStrictSucc# :: (a <# b) -> (a + 1 <=# b)+{-# INLINE fromStrictSucc# #-}+fromStrictSucc# _ = Lte# (# #)+ -- | Zero is less-than-or-equal-to any number. zero :: 0 <= a-{-# inline zero #-}+{-# INLINE zero #-} zero = Lte --- | Use GHC's built-in type-level arithmetic to prove--- that one number is less-than-or-equal-to another. The type-checker--- only reduces 'CmpNat' if both arguments are constants.+{- | Use GHC's built-in type-level arithmetic to prove+that one number is less-than-or-equal-to another. The type-checker+only reduces 'CmpNat' if both arguments are constants.+-} constant :: forall a b. (IsLte (CmpNat a b) ~ 'True) => (a <= b)-{-# inline constant #-}+{-# INLINE constant #-} constant = Lte  type family IsLte (o :: Ordering) :: Bool where   IsLte 'GT = 'False   IsLte 'LT = 'True   IsLte 'EQ = 'True++unlift :: (a <= b) -> (a <=# b)+unlift _ = Lte# (# #)++lift :: (a <=# b) -> (a <= b)+lift _ = Lte
src/Arithmetic/Nat.hs view
@@ -1,122 +1,204 @@-{-# language DataKinds #-}-{-# language ExplicitForAll #-}-{-# language KindSignatures #-}-{-# language MagicHash #-}-{-# language RankNTypes #-}-{-# language ScopedTypeVariables #-}-{-# language TypeOperators #-}-{-# language UnboxedTuples #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}  module Arithmetic.Nat   ( -- * Addition     plus   , plus#+     -- * Subtraction   , monus+     -- * Division   , divide   , divideRoundingUp+     -- * Multiplication   , times+     -- * Successor   , succ+  , succ#+     -- * Compare   , testEqual+  , testEqual#   , testLessThan+  , testLessThan#   , testLessThanEqual+  , testLessThanEqual#   , testZero+  , testZero#   , (=?)   , (<?)+  , (<?#)   , (<=?)+  , (<=?#)+     -- * Constants   , zero   , one   , two   , three   , constant+  , constant#+     -- * Unboxed Constants   , zero#+  , one#++    -- * Unboxed Pattern Synonyms+  , pattern N0#+  , pattern N1#+  , pattern N2#+  , pattern N3#+  , pattern N4#+  , pattern N5#+  , pattern N6#+  , pattern N7#+  , pattern N8#+  , pattern N16#+  , pattern N32#+  , pattern N64#+  , pattern N128#+  , pattern N256#+  , pattern N512#+  , pattern N1024#+  , pattern N2048#+  , pattern N4096#+  , pattern N8192#+  , pattern N16384#+     -- * Convert   , demote+  , demote#   , unlift   , lift   , with+  , with#++    -- * Substitute+  , substitute#   ) where  import Prelude hiding (succ)  import Arithmetic.Types-import Arithmetic.Unsafe ((:=:)(Eq), type (<=)(Lte))-import Arithmetic.Unsafe (Nat(Nat),Nat#(Nat#),type (<)(Lt))-import GHC.Exts (Proxy#,proxy#,(+#))-import GHC.TypeNats (type (+),type (-),Div,KnownNat,natVal')-import GHC.Int (Int(I#))+import Arithmetic.Unsafe (Nat (Nat), Nat# (Nat#), (:=:) (Eq), (:=:#) (Eq#), type (<) (Lt), type (<#) (Lt#), type (<=) (Lte))+import Arithmetic.Unsafe (type (<=#) (Lte#))+import Data.Either.Void (EitherVoid#, pattern LeftVoid#, pattern RightVoid#)+import Data.Maybe.Void (MaybeVoid#, pattern JustVoid#, pattern NothingVoid#)+import GHC.Exts (Int#, Proxy#, proxy#, (+#), (<#), (==#))+import GHC.Int (Int (I#))+import GHC.TypeNats (Div, KnownNat, natVal', type (+), type (-))  import qualified GHC.TypeNats as GHC  -- | Infix synonym of 'testLessThan'. (<?) :: Nat a -> Nat b -> Maybe (a < b)-{-# inline (<?) #-}+{-# INLINE (<?) #-} (<?) = testLessThan  -- | Infix synonym of 'testLessThanEqual'. (<=?) :: Nat a -> Nat b -> Maybe (a <= b)-{-# inline (<=?) #-}+{-# INLINE (<=?) #-} (<=?) = testLessThanEqual  -- | Infix synonym of 'testEqual'. (=?) :: Nat a -> Nat b -> Maybe (a :=: b)-{-# inline (=?) #-}+{-# INLINE (=?) #-} (=?) = testEqual --- | Is the first argument strictly less than the second--- argument?+(<?#) :: Nat# a -> Nat# b -> MaybeVoid# (a <# b)+{-# INLINE (<?#) #-}+(<?#) = testLessThan#++(<=?#) :: Nat# a -> Nat# b -> MaybeVoid# (a <=# b)+{-# INLINE (<=?#) #-}+(<=?#) = testLessThanEqual#++{- | Is the first argument strictly less than the second+argument?+-} testLessThan :: Nat a -> Nat b -> Maybe (a < b)-{-# inline testLessThan #-}-testLessThan (Nat x) (Nat y) = if x < y-  then Just Lt-  else Nothing+{-# INLINE testLessThan #-}+testLessThan (Nat x) (Nat y) =+  if x < y+    then Just Lt+    else Nothing --- | Is the first argument less-than-or-equal-to the second--- argument?+testLessThan# :: Nat# a -> Nat# b -> MaybeVoid# (a <# b)+{-# INLINE testLessThan# #-}+testLessThan# (Nat# x) (Nat# y) = case x <# y of+  0# -> NothingVoid#+  _ -> JustVoid# (Lt# (# #))++{- | Is the first argument less-than-or-equal-to the second+argument?+-} testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)-{-# inline testLessThanEqual #-}-testLessThanEqual (Nat x) (Nat y) = if x <= y-  then Just Lte-  else Nothing+{-# INLINE testLessThanEqual #-}+testLessThanEqual (Nat x) (Nat y) =+  if x <= y+    then Just Lte+    else Nothing +testLessThanEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a <=# b)+{-# INLINE testLessThanEqual# #-}+testLessThanEqual# (Nat# x) (Nat# y) = case x <# y of+  0# -> NothingVoid#+  _ -> JustVoid# (Lte# (# #))+ -- | Are the two arguments equal to one another? testEqual :: Nat a -> Nat b -> Maybe (a :=: b)-{-# inline testEqual #-}-testEqual (Nat x) (Nat y) = if x == y-  then Just Eq-  else Nothing+{-# INLINE testEqual #-}+testEqual (Nat x) (Nat y) =+  if x == y+    then Just Eq+    else Nothing +testEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a :=:# b)+{-# INLINE testEqual# #-}+testEqual# (Nat# x) (Nat# y) = case x ==# y of+  0# -> NothingVoid#+  _ -> JustVoid# (Eq# (# #))+ -- | Is zero equal to this number or less than it? testZero :: Nat a -> Either (0 :=: a) (0 < a)-{-# inline testZero #-}+{-# INLINE testZero #-} testZero (Nat x) = case x of   0 -> Left Eq   _ -> Right Lt +testZero# :: Nat# a -> EitherVoid# (0 :=:# a) (0 <# a)+testZero# (Nat# x) = case x of+  0# -> LeftVoid# (Eq# (# #))+  _ -> RightVoid# (Lt# (# #))+ -- | Add two numbers. plus :: Nat a -> Nat b -> Nat (a + b)-{-# inline plus #-}+{-# INLINE plus #-} plus (Nat x) (Nat y) = Nat (x + y)  -- | Variant of 'plus' for unboxed nats. plus# :: Nat# a -> Nat# b -> Nat# (a + b)-{-# inline plus# #-}+{-# INLINE plus# #-} plus# (Nat# x) (Nat# y) = Nat# (x +# y)  -- | Divide two numbers. Rounds down (towards zero) divide :: Nat a -> Nat b -> Nat (Div a b)-{-# inline divide #-}+{-# INLINE divide #-} divide (Nat x) (Nat y) = Nat (div x y)  -- | Divide two numbers. Rounds up (away from zero) divideRoundingUp :: Nat a -> Nat b -> Nat (Div (a - 1) b + 1)-{-# inline divideRoundingUp #-}+{-# INLINE divideRoundingUp #-} divideRoundingUp (Nat x) (Nat y) =   -- Implementation note. We must use div so that when x=0,   -- the result is (-1) and not 0. Then when we add 1, we get 0.@@ -124,71 +206,161 @@  -- | Multiply two numbers. times :: Nat a -> Nat b -> Nat (a GHC.* b)-{-# inline times #-}+{-# INLINE times #-} times (Nat x) (Nat y) = Nat (x * y)  -- | The successor of a number. succ :: Nat a -> Nat (a + 1)-{-# inline succ #-}+{-# INLINE succ #-} succ n = plus n one +-- | Unlifted variant of 'succ'.+succ# :: Nat# a -> Nat# (a + 1)+{-# INLINE succ# #-}+succ# n = plus# n (one# (# #))+ -- | Subtract the second argument from the first argument. monus :: Nat a -> Nat b -> Maybe (Difference a b)-{-# inline monus #-}-monus (Nat a) (Nat b) = let c = a - b in if c >= 0-  then Just (Difference (Nat c) Eq)-  else Nothing+{-# INLINE monus #-}+monus (Nat a) (Nat b) =+  let c = a - b+   in if c >= 0+        then Just (Difference (Nat c) Eq)+        else Nothing  -- | The number zero. zero :: Nat 0-{-# inline zero #-}+{-# INLINE zero #-} zero = Nat 0  -- | The number one. one :: Nat 1-{-# inline one #-}+{-# INLINE one #-} one = Nat 1  -- | The number two. two :: Nat 2-{-# inline two #-}+{-# INLINE two #-} two = Nat 2  -- | The number three. three :: Nat 3-{-# inline three #-}+{-# INLINE three #-} three = Nat 3 --- | Use GHC's built-in type-level arithmetic to create a witness--- of a type-level number. This only reduces if the number is a--- constant.-constant :: forall n. KnownNat n => Nat n-{-# inline constant #-}+{- | Use GHC's built-in type-level arithmetic to create a witness+of a type-level number. This only reduces if the number is a+constant.+-}+constant :: forall n. (KnownNat n) => Nat n+{-# INLINE constant #-} constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n))) +constant# :: forall n. (KnownNat n) => (# #) -> Nat# n+{-# INLINE constant# #-}+constant# _ = case fromIntegral (natVal' (proxy# :: Proxy# n)) of+  I# i -> Nat# i+ -- | The number zero. Unboxed. zero# :: (# #) -> Nat# 0 zero# _ = Nat# 0# --- | Extract the 'Int' from a 'Nat'. This is intended to be used--- at a boundary where a safe interface meets the unsafe primitives--- on top of which it is built.+-- | The number one. Unboxed.+one# :: (# #) -> Nat# 1+one# _ = Nat# 1#++{- | Extract the 'Int' from a 'Nat'. This is intended to be used+at a boundary where a safe interface meets the unsafe primitives+on top of which it is built.+-} demote :: Nat n -> Int-{-# inline demote #-}+{-# INLINE demote #-} demote (Nat n) = n --- | Run a computation on a witness of a type-level number. The--- argument 'Int' must be greater than or equal to zero. This is--- not checked. Failure to upload this invariant will lead to a--- segfault.+demote# :: Nat# n -> Int#+{-# INLINE demote# #-}+demote# (Nat# n) = n++{- | Run a computation on a witness of a type-level number. The+argument 'Int' must be greater than or equal to zero. This is+not checked. Failure to upload this invariant will lead to a+segfault.+-} with :: Int -> (forall n. Nat n -> a) -> a-{-# inline with #-}+{-# INLINE with #-} with i f = f (Nat i) +with# :: Int# -> (forall n. Nat# n -> a) -> a+{-# INLINE with# #-}+with# i f = f (Nat# i)+ unlift :: Nat n -> Nat# n-{-# inline unlift #-}+{-# INLINE unlift #-} unlift (Nat (I# i)) = Nat# i  lift :: Nat# n -> Nat n-{-# inline lift #-}+{-# INLINE lift #-} lift (Nat# i) = Nat (I# i)++pattern N0# :: Nat# 0+pattern N0# = Nat# 0#++pattern N1# :: Nat# 1+pattern N1# = Nat# 1#++pattern N2# :: Nat# 2+pattern N2# = Nat# 2#++pattern N3# :: Nat# 3+pattern N3# = Nat# 3#++pattern N4# :: Nat# 4+pattern N4# = Nat# 4#++pattern N5# :: Nat# 5+pattern N5# = Nat# 5#++pattern N6# :: Nat# 6+pattern N6# = Nat# 6#++pattern N7# :: Nat# 7+pattern N7# = Nat# 7#++pattern N8# :: Nat# 8+pattern N8# = Nat# 8#++pattern N16# :: Nat# 16+pattern N16# = Nat# 16#++pattern N32# :: Nat# 32+pattern N32# = Nat# 32#++pattern N64# :: Nat# 64+pattern N64# = Nat# 64#++pattern N128# :: Nat# 128+pattern N128# = Nat# 128#++pattern N256# :: Nat# 256+pattern N256# = Nat# 256#++pattern N512# :: Nat# 512+pattern N512# = Nat# 512#++pattern N1024# :: Nat# 1024+pattern N1024# = Nat# 1024#++pattern N2048# :: Nat# 2048+pattern N2048# = Nat# 2048#++pattern N4096# :: Nat# 4096+pattern N4096# = Nat# 4096#++pattern N8192# :: Nat# 8192+pattern N8192# = Nat# 8192#++pattern N16384# :: Nat# 16384+pattern N16384# = Nat# 16384#++substitute# :: (m :=:# n) -> Nat# m -> Nat# n+substitute# _ (Nat# x) = Nat# x
src/Arithmetic/Plus.hs view
@@ -1,17 +1,21 @@-{-# language DataKinds #-}-{-# language TypeOperators #-}-{-# language KindSignatures #-}-{-# language ExplicitForAll #-}-{-# language AllowAmbiguousTypes #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}  module Arithmetic.Plus   ( zeroL   , zeroR   , commutative+  , commutative#   , associative   ) where -import Arithmetic.Unsafe (type (:=:)(Eq))+import Arithmetic.Unsafe (type (:=:) (Eq))+import Arithmetic.Unsafe (type (:=:#) (Eq#)) import GHC.TypeNats (type (+))  -- | Any number plus zero is equal to the original number.@@ -25,6 +29,9 @@ -- | Addition is commutative. commutative :: forall a b. a + b :=: b + a commutative = Eq++commutative# :: forall a b. (# #) -> a + b :=:# b + a+commutative# _ = Eq# (# #)  -- | Addition is associative. associative :: forall a b c. (a + b) + c :=: a + (b + c)
src/Arithmetic/Types.hs view
@@ -1,45 +1,66 @@-{-# language DataKinds #-}-{-# language MagicHash #-}-{-# language ExplicitNamespaces #-}-{-# language GADTs #-}-{-# language KindSignatures #-}-{-# language RankNTypes #-}-{-# language TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE ViewPatterns #-}  module Arithmetic.Types   ( Nat   , Nat#-  , WithNat(..)-  , Difference(..)-  , Fin(..)+  , WithNat (..)+  , Difference (..)+  , Fin (..)   , Fin#+  , Fin32#++    -- * Maybe Fin+  , MaybeFin#+  , pattern MaybeFinJust#+  , pattern MaybeFinNothing#++    -- * Either Fin+  , EitherFin#+  , pattern EitherFinLeft#+  , pattern EitherFinRight#++    -- * Infix Operators   , type (<)   , type (<=)+  , type (<#)+  , type (<=#)   , type (:=:)+  , type (:=:#)   ) where -import Arithmetic.Unsafe (Fin#,Nat#,Nat(getNat), type (<=))-import Arithmetic.Unsafe (type (<), type (:=:))+import Arithmetic.Unsafe (EitherFin# (..), Fin# (Fin#), Fin32#, MaybeFin# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#)) import Data.Kind (type Type)+import GHC.Exts ((-#), (<#)) import GHC.TypeNats (type (+))  import qualified GHC.TypeNats as GHC  data WithNat :: (GHC.Nat -> Type) -> Type where   WithNat ::-       {-# UNPACK #-} !(Nat n)-    -> f n-    -> WithNat f+    {-# UNPACK #-} !(Nat n) ->+    f n ->+    WithNat f  -- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }' data Fin :: GHC.Nat -> Type where-  Fin :: forall m n.+  Fin ::+    forall m n.     { index :: !(Nat m)     , proof :: !(m < n)-    } -> Fin n+    } ->+    Fin n --- | Proof that the first argument can be expressed as the--- sum of the second argument and some other natural number.+{- | Proof that the first argument can be expressed as the+sum of the second argument and some other natural number.+-} data Difference :: GHC.Nat -> GHC.Nat -> Type where   -- It is safe for users of this library to use this data constructor   -- freely. However, note that the interesting Difference values come@@ -54,3 +75,32 @@  instance Ord (Fin n) where   Fin x _ `compare` Fin y _ = compare (getNat x) (getNat y)++pattern EitherFinLeft# :: Fin# m -> EitherFin# m n+pattern EitherFinLeft# f <- (eitherFinToSum# -> (# f | #))+  where+    EitherFinLeft# (Fin# i) = EitherFin# ((-1#) -# i)++pattern EitherFinRight# :: Fin# n -> EitherFin# m n+pattern EitherFinRight# f <- (eitherFinToSum# -> (# | f #))+  where+    EitherFinRight# (Fin# i) = EitherFin# i++eitherFinToSum# :: EitherFin# m n -> (# Fin# m | Fin# n #)+eitherFinToSum# (EitherFin# i) = case i <# 0# of+  1# -> (# Fin# ((-1#) -# i) | #)+  _ -> (# | Fin# i #)++pattern MaybeFinJust# :: Fin# n -> MaybeFin# n+pattern MaybeFinJust# f <- (maybeFinToFin# -> (# | f #))+  where+    MaybeFinJust# (Fin# i) = MaybeFin# i++pattern MaybeFinNothing# :: MaybeFin# n+pattern MaybeFinNothing# = MaybeFin# (-1#)++maybeFinToFin# :: MaybeFin# n -> (# (# #) | Fin# n #)+{-# INLINE maybeFinToFin# #-}+maybeFinToFin# (MaybeFin# i) = case i of+  -1# -> (# (# #) | #)+  _ -> (# | Fin# i #)
src/Arithmetic/Unsafe.hs view
@@ -1,29 +1,35 @@-{-# language DataKinds #-}-{-# language DerivingStrategies #-}-{-# language ExplicitNamespaces #-}-{-# language GADTSyntax #-}-{-# language GeneralizedNewtypeDeriving #-}-{-# language KindSignatures #-}-{-# language MagicHash #-}-{-# language RoleAnnotations #-}-{-# language StandaloneDeriving #-}-{-# language TypeOperators #-}-{-# language UnliftedNewtypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GADTSyntax #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}+{-# LANGUAGE UnliftedNewtypes #-}  module Arithmetic.Unsafe-  ( Nat(..)-  , Nat#(..)-  , Fin#(..)-  , type (<)(Lt)-  , type (<=)(Lte)-  , type (:=:)(Eq)+  ( Nat (..)+  , Nat# (..)+  , Fin# (..)+  , MaybeFin# (..)+  , EitherFin# (..)+  , Fin32# (..)+  , type (<#) (Lt#)+  , type (<=#) (Lte#)+  , type (<) (Lt)+  , type (<=) (Lte)+  , type (:=:) (Eq)+  , type (:=:#) (Eq#)   ) where -import Prelude hiding ((>=),(<=))+import Prelude hiding ((<=), (>=))  import Control.Category (Category) import Data.Kind (Type)-import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep))+import GHC.Exts (Int#, Int32#, RuntimeRep (Int32Rep, IntRep, TupleRep), TYPE)  import qualified Control.Category import qualified GHC.TypeNats as GHC@@ -36,10 +42,14 @@  infix 4 < infix 4 <=+infix 4 <#+infix 4 <=# infix 4 :=:+infix 4 :=:#  -- | A value-level representation of a natural number @n@.-newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int }+newtype Nat (n :: GHC.Nat) = Nat {getNat :: Int}+ type role Nat nominal  deriving newtype instance Show (Nat n)@@ -47,26 +57,63 @@ -- | Unboxed variant of Nat. newtype Nat# :: GHC.Nat -> TYPE 'IntRep where   Nat# :: Int# -> Nat# n+ type role Nat# nominal  -- | Finite numbers without the overhead of carrying around a proof. newtype Fin# :: GHC.Nat -> TYPE 'IntRep where   Fin# :: Int# -> Fin# n+ type role Fin# nominal --- | Proof that the first argument is strictly less than the--- second argument.+{- | Either a @Fin#@ or Nothing. Internally, this uses negative+one to mean Nothing.+-}+newtype MaybeFin# :: GHC.Nat -> TYPE 'IntRep where+  MaybeFin# :: Int# -> MaybeFin# n++type role MaybeFin# nominal++{- | Either a @Fin#@ bounded by the left natural or one bounded+by the right natural.+-}+newtype EitherFin# :: GHC.Nat -> GHC.Nat -> TYPE 'IntRep where+  -- Implementation note: Left is represented by (-m + 1), and+  -- right is represented by n.+  EitherFin# :: Int# -> EitherFin# m n++type role EitherFin# nominal nominal++-- | Variant of 'Fin#' that only allows 32-bit integers.+newtype Fin32# :: GHC.Nat -> TYPE 'Int32Rep where+  Fin32# :: Int32# -> Fin32# n++type role Fin32# nominal++{- | Proof that the first argument is strictly less than the+second argument.+-} data (<) :: GHC.Nat -> GHC.Nat -> Type where   Lt :: a < b --- | Proof that the first argument is less than or equal to the--- second argument.+newtype (<#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where+  Lt# :: (# #) -> a <# b++{- | Proof that the first argument is less than or equal to the+second argument.+-} data (<=) :: GHC.Nat -> GHC.Nat -> Type where   Lte :: a <= b +newtype (<=#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where+  Lte# :: (# #) -> a <=# b+ -- | Proof that the first argument is equal to the second argument. data (:=:) :: GHC.Nat -> GHC.Nat -> Type where   Eq :: a :=: b++newtype (:=:#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where+  Eq# :: (# #) -> a :=:# b  instance Category (<=) where   id = Lte