fin-int 0.1.0.0 → 0.2.0.1
raw patch · 5 files changed
Files
- CHANGELOG.md +11/−1
- README.md +3/−0
- fin-int.cabal +17/−20
- src/Data/Fin/Int.hs +11/−6
- src/Data/Fin/Int/Explicit.hs +45/−10
CHANGELOG.md view
@@ -1,3 +1,13 @@-# 0.1.0.0+# 0.2.0.1 (2023-03-12)++* Fix build on GHC 9.4 and 9.6 by adding `UndecidableInstances`.++# 0.2.0 (2021-10-11)++* Add a type role for `Fin`, which was formerly `Coercible` in unsafe ways.+* Fix the `Read` instance erroring on out-of-range values; it now merely fails.+* Add `Attenuable` instances for `attenuation-0.2.0`.++# 0.1.0.0 (2021-09-07) Initial version.
+ README.md view
@@ -0,0 +1,3 @@+# fin-int++Implements size-indexed bounded natural number types as a newtype over Int.
fin-int.cabal view
@@ -1,50 +1,47 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.33.0.+-- This file has been generated from package.yaml by hpack version 0.35.1. -- -- see: https://github.com/sol/hpack------ hash: 7c84a39433ed8a33ecfb2a72df2187a958991c0069c5db23021bc938a85c54d2 name: fin-int-version: 0.1.0.0-synopsis: The type of finite sets with elements identified by the ordinals.-description: This provides a newtype Fin containing an Int with an invariant that its- value is less than its type-level Nat bound. It aims to have low overhead- compared to Ints, and is suitable for use as the index type of+version: 0.2.0.1+synopsis: Finite sets of static size+description: This provides a newtype @Fin@ containing an @Int@ with an invariant that+ its value is less than its type-level @Nat@ bound. It aims to have low+ overhead compared to @Int@s, and is suitable for use as the index type of length-indexed vectors. category: Data-homepage: https://github.com/google/hs-fin-vec#readme-bug-reports: https://github.com/google/hs-fin-vec/issues+homepage: https://github.com/awpr/fin-vec#readme+bug-reports: https://github.com/awpr/fin-vec/issues author: Lennart Augustsson <lennart@augustsson.net>-maintainer: Andrew Pritchard <awpr@google.com>-copyright: 2017-2021 Google LLC+maintainer: Andrew Pritchard <awpritchard@gmail.com>+copyright: 2017-2021 Google LLC; 2022 Andrew Pritchard license: Apache-2.0 license-file: LICENSE build-type: Simple extra-source-files: CHANGELOG.md+ README.md source-repository head type: git- location: https://github.com/google/hs-fin-vec+ location: https://github.com/awpr/fin-vec subdir: fin-int library exposed-modules: Data.Fin.Int Data.Fin.Int.Explicit- other-modules:- Paths_fin_int hs-source-dirs: src build-depends: QuickCheck >=2.5 && <2.15- , attenuation >=0.1 && <0.2- , base >=4.12 && <4.16+ , attenuation >=0.1 && <0.3+ , base >=4.12 && <4.19 , data-default-class >=0.0 && <0.2 , deepseq >=1.1 && <1.5- , portray >=0.1 && <0.2- , portray-diff >=0.1 && <0.2- , sint >=0.1 && <0.2+ , portray >=0.1 && <0.4+ , portray-diff ==0.1.*+ , sint >=0.1 && <0.3 default-language: Haskell2010
src/Data/Fin/Int.hs view
@@ -95,7 +95,7 @@ fin :: forall n. (HasCallStack, KnownNat n) => Int -> Fin n fin = E.fin sintVal --- | This is similar to 'fromInteger', but you get a stack trace on error.+-- | Generalized 'fin' that works on any 'Integral' type. {-# INLINE finFromIntegral #-} finFromIntegral :: forall n a@@ -103,8 +103,7 @@ => a -> Fin n finFromIntegral = E.finFromIntegral sintVal --- | Like 'fin', but doesn't do any bounds checks. However, unlike--- 'unsafeFin', this is safe (by virtue of the type constraints).+-- | Construct a 'Fin' from a 'GHC.TypeNats.Nat' known to be in-bounds. knownFin :: forall i n. (KnownNat i, i <= n - 1) => Fin n knownFin = E.knownFin (sintVal @i) {-# INLINE knownFin #-}@@ -272,6 +271,8 @@ shiftFin = E.shiftFin sintVal -- | 'unshiftFin' decreases the value and bound of a Fin both by @m@.+--+-- Raises an exception if the result would be negative. unshiftFin :: forall m n . (HasCallStack, KnownNat m, KnownNat n)@@ -294,13 +295,17 @@ concatFin :: forall m n. KnownNat m => Either (Fin m) (Fin n) -> Fin (m + n) concatFin = E.concatFin sintVal --- | Convert to a possibly smaller type.--- This function fails if the number is too big.+-- | Convert to a 'Fin' with a (potentially) smaller bound.+--+-- This function throws an exception if the number is out of range of the+-- target type. {-# INLINE unembed #-} unembed :: (HasCallStack, KnownNat n) => Fin m -> Fin n unembed = E.unembed sintVal --- | Convert to a possibly smaller type or return Nothing if out of bounds.+-- | Convert to a 'Fin' with a (potentially) smaller bound.+--+-- Returns 'Nothing' if the number is out of range of the target type. {-# INLINE tryUnembed #-} tryUnembed :: KnownNat n => Fin m -> Maybe (Fin n) tryUnembed = E.tryUnembed sintVal
src/Data/Fin/Int/Explicit.hs view
@@ -1,4 +1,5 @@ -- Copyright 2017-2021 Google LLC+-- Copyright 2022 Andrew Pritchard -- -- Licensed under the Apache License, Version 2.0 (the "License"); -- you may not use this file except in compliance with the License.@@ -21,11 +22,15 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} -- | Finite natural numbers, with upper bound as part of the type.@@ -71,10 +76,10 @@ , unsafeFin, unsafePred, unsafeSucc, unsafeCoFin, unsafeCoInt ) where -import Control.Arrow (first) import Control.DeepSeq (NFData(rnf)) import Data.Coerce (coerce) import Data.Data (Data)+import Data.Maybe (mapMaybe) import Data.Type.Coercion (Coercion(..)) import GHC.Stack (HasCallStack, withFrozenCallStack) import GHC.TypeNats@@ -85,7 +90,12 @@ import Data.Default.Class (Default(..)) import Data.Portray (Portray) import Data.Portray.Diff (Diff)-import Data.Type.Attenuation (Attenuation, coercible)+import Data.Type.Attenuation+ ( Attenuation, coercible+#if MIN_VERSION_attenuation(0, 2, 0)+ , Attenuable(..)+#endif+ ) import Test.QuickCheck (Arbitrary(..), arbitraryBoundedEnum) import Data.SInt (SInt, unSInt, sintVal)@@ -102,26 +112,39 @@ -- Fin Read/Show behave like other numeric newtypes: drop the \"Fin\". deriving newtype (Show, Portray, Diff) +-- Prevent 'Coercible' across 'Fin's of different bounds.+--+-- For the safe direction, we have 'Attenuable' instead.+type role Fin nominal+ -- | Constraint synonym for naturals @n@ s.t. @'Fin' n@ is inhabited. type FinSize n = (KnownNat n, 1 <= n) instance KnownNat n => Read (Fin n) where- readsPrec p s = first (finFromIntegral sintVal) <$> readsPrec @Integer p s+ readsPrec p s =+ mapMaybe (\ (x, s') -> (,s') <$> tryFin sintVal x) $+ readsPrec @Integer p s instance FinSize n => Arbitrary (Fin n) where arbitrary = arbitraryBoundedEnum instance NFData (Fin n) where rnf (Fin x) = rnf x +#if MIN_VERSION_attenuation(0,2,0)+instance Attenuable (Fin n) Int+instance m <= n => Attenuable (Fin m) (Fin n)+#endif+ -- | Construct a 'Fin' from an 'Int', with bounds checks.+{-# INLINE fin #-} fin :: HasCallStack => SInt n -> Int -> Fin n fin (unSInt -> !n) i | i < 0 = error $ "Fin: number out of range " ++ show i ++ " < 0" | i >= n = error $ "Fin: number out of range " ++ show i ++ " >= " ++ show n | otherwise = Fin i --- | This is similar to 'fromInteger', but you get a stack trace on error.-{-# INLINE fin #-}+-- | Generalized 'fin' that works on any 'Integral' type.+{-# INLINE finFromIntegral #-} finFromIntegral :: (HasCallStack, Integral a, Show a) => SInt n -> a -> Fin n@@ -191,7 +214,7 @@ -- raising the error inside of x, so an invalid Fin can never be returned. complementFin sn x = unsafeFin (unSInt sn - 1 - finToInt x) --- | This is like 'fromIntegral', but without the annoying context.+-- | Convert a 'Fin' to the underlying 'Int' representing it. finToInt :: Fin n -> Int finToInt (Fin i) = i {-# INLINE finToInt #-}@@ -460,6 +483,8 @@ {-# INLINEABLE chkMul #-} -- | Restricted coercion to larger Fin types.+--+-- This is also available as an 'Attenuable' instance. attLT :: (n <= m) => Attenuation (Fin n) (Fin m) attLT = coercible @@ -472,6 +497,8 @@ attMinus = coercible -- | Restricted coercion to Int.+--+-- This is also available as an 'Attenuable' instance. attInt :: Attenuation (Fin n) Int attInt = coercible @@ -500,6 +527,8 @@ tryUnshiftFin sm sn (Fin x) = tryFin sn (x - unSInt sm) -- | 'unshiftFin' decreases the value and bound of a Fin both by @m@.+--+-- Raises an exception if the result would be negative. unshiftFin :: HasCallStack => SInt m -> SInt n -> Fin (m+n) -> Fin n unshiftFin sm sn (Fin x) = fin sn (x - unSInt sm) @@ -516,18 +545,24 @@ Left (Fin x) -> Fin x Right x -> shiftFin sm x --- | Convert to a bigger type.+-- | Convert to a 'Fin' with a larger bound.+--+-- This is equivalent to a specialization of 'Data.Type.Attenuation.attenuate'. {-# INLINE embed #-} embed :: (m <= n) => Fin m -> Fin n embed (Fin i) = Fin i --- | Convert to a possibly smaller type.--- This function fails if the number is too big.+-- | Convert to a 'Fin' with a (potentially) smaller bound.+--+-- This function throws an exception if the number is out of range of the+-- target type. {-# INLINE unembed #-} unembed :: HasCallStack => SInt n -> Fin m -> Fin n unembed sn (Fin i) = ufin sn i --- | Convert to a possibly smaller type or return Nothing if out of bounds.+-- | Convert to a 'Fin' with a (potentially) smaller bound.+--+-- Returns 'Nothing' if the number is out of range of the target type. tryUnembed :: SInt n -> Fin m -> Maybe (Fin n) tryUnembed sn (Fin i) = tryFin sn i