sint (empty) → 0.1.0.0
raw patch · 5 files changed
+572/−0 lines, 5 filesdep +QuickCheckdep +basedep +portray
Dependencies added: QuickCheck, base, portray, portray-diff, sint, test-framework, test-framework-quickcheck2
Files
- CHANGELOG.md +3/−0
- LICENSE +202/−0
- sint.cabal +64/−0
- src/Data/SInt.hs +203/−0
- test/Main.hs +100/−0
+ CHANGELOG.md view
@@ -0,0 +1,3 @@+# 0.1.0.0++Initial version.
+ LICENSE view
@@ -0,0 +1,202 @@++ 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.
+ sint.cabal view
@@ -0,0 +1,64 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.33.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: ceb4a5946c62e4214f0149eb3292465831eb7758e6dd5435ab1fb3d771813708++name: sint+version: 0.1.0.0+synopsis: A singleton type for `Nat` represented as `Int`.+description: This package implements a type `SInt` that links a runtime `Int` with a+ type-level `Nat`, along with some arithmetic and reflection capabilities.+ .+ This is useful when mixing type-level `Nat`s with GHC array primitives that+ expect `Int`s as sizes and indices.+ .+ See the module intro of `Data.SInt` for more details.+category: Data+homepage: https://github.com/google/hs-fin-vec#readme+bug-reports: https://github.com/google/hs-fin-vec/issues+author: Andrew Pritchard <awpr@google.com>+maintainer: Andrew Pritchard <awpr@google.com>+copyright: 2021 Google LLC+license: Apache-2.0+license-file: LICENSE+build-type: Simple+extra-source-files:+ CHANGELOG.md++source-repository head+ type: git+ location: https://github.com/google/hs-fin-vec+ subdir: sint++library+ exposed-modules:+ Data.SInt+ other-modules:+ Paths_sint+ hs-source-dirs:+ src+ build-depends:+ base >=4.12 && <4.16+ , portray >=0.1 && <0.2+ , portray-diff >=0.1 && <0.2+ default-language: Haskell2010++test-suite SInt-test+ type: exitcode-stdio-1.0+ main-is: Main.hs+ other-modules:+ Paths_sint+ hs-source-dirs:+ test+ build-depends:+ QuickCheck+ , base >=4.12 && <4.16+ , portray >=0.1 && <0.2+ , portray-diff >=0.1 && <0.2+ , sint+ , test-framework+ , test-framework-quickcheck2+ default-language: Haskell2010
+ src/Data/SInt.hs view
@@ -0,0 +1,203 @@+-- Copyright 2021 Google LLC+--+-- 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.++-- | Provides a singleton type for a subset of 'Nat's, represented by 'Int'.+--+-- This is particularly useful when working with length-indexed array types,+-- since the array primitives generally expect lengths and indices to be+-- 'Int's. Thus, there's no need to pay the runtime cost of lugging around+-- 'Natural's to handle greater-than-maxInt-length arrays, since the underlying+-- primitives don't handle them either.+--+-- An @'SInt' n@ is trusted absolutely by downstream code to contain an 'Int'+-- @n'@ s.t. @fromIntegral n' == natVal' \@n Proxy#@. In particular, this+-- trust extends to a willingness to use two runtime-equal 'SInt's as proof+-- that their type parameters are equal, or to use GHC primitives in a way+-- that's only memory-safe if this property holds. This means it should be+-- considered /unsafe/ to construct an 'SInt' in any way that's not statically+-- guaranteed to produce the correct runtime value, and to construct one with+-- an incorrect runtime value is equivalent to using 'unsafeCoerce'+-- incorrectly.+--+-- 'SInt' should be seen as a more efficient implementation of+-- @data SNat n = KnownNat n => SNat@, so that constructing an incorrect 'SInt'+-- would be equivalent to producing an incorrect 'KnownNat' instance.+--+-- 'SInt's are constructed safely by 'staticSIntVal' with no overhead,+-- by 'sintVal' with runtime bounds checks based on a 'KnownNat' instance, or+-- by various arithmetic functions.++{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}++#include "MachDeps.h"++module Data.SInt+ ( SInt(SI#, unSInt), trySIntVal, sintVal, reifySInt, withSInt+ , addSInt, subSInt, subSIntLE, subSIntL, mulSInt, divSIntL, divSIntR+ , staticSIntVal+ -- * Internal+ , IntMaxP1+ ) where++import Data.Proxy (Proxy(..))+import GHC.Exts (Int(I#), addIntC#, mulIntMayOflo#, proxy#)+import GHC.Stack (HasCallStack)+import GHC.TypeNats+ ( type (<=), type (+), type (-), type (*), type (^), CmpNat+ , KnownNat, Nat, natVal', SomeNat(..), someNatVal+ )+import Numeric.Natural (Natural)++import Data.Portray (Portray)+import Data.Portray.Diff (Diff)++#if MIN_VERSION_base(4,15,0)+import Unsafe.Coerce (unsafeEqualityProof, UnsafeEquality(..))+#else+import Data.Type.Equality ((:~:)(..))+import Unsafe.Coerce (unsafeCoerce)+#endif++-- | A singleton type linking a runtime 'Int' and a type-level 'Nat'.+newtype SInt (n :: Nat) = MkSInt Int+ deriving newtype (Show, Portray, Diff)++-- We must take care to prevent 'SInt's from being coerced across @n@.+type role SInt nominal++-- | Construct an 'SInt' unsafely. Incorrect uses cause undefined behavior.+--+-- See the module intro for more details; prefer to use safe methods to+-- construct 'SInt's, and treat this constructor equivalently to+-- 'unsafeCoerce'.+pattern SI# :: Int -> SInt n+pattern SI# {unSInt} = MkSInt unSInt+{-# COMPLETE SI# #-}++-- | Use an 'Int' as an existentially-quantified 'SInt'.+withSInt :: HasCallStack => Int -> (forall n. SInt n -> r) -> r+withSInt n f+ | n < 0 = error "withSInt: negative value"+ | otherwise = f (SI# n)++maxInt :: Natural+maxInt = fromIntegral (maxBound :: Int)++-- | Produce an 'SInt' for a given 'KnownNat', or 'Nothing' if out of range.+trySIntVal :: forall n. KnownNat n => Maybe (SInt n)+trySIntVal =+ let n = natVal' @n proxy#+ in if n <= maxInt then Just (MkSInt (fromIntegral n)) else Nothing+{-# INLINE trySIntVal #-}++-- | Produce an 'SInt' for a given 'KnownNat', or 'error' if out of range.+sintVal :: forall n. (HasCallStack, KnownNat n) => SInt n+sintVal = case trySIntVal of+ Just n -> n+ Nothing -> error $+ "Nat " ++ show (natVal' @n proxy#) ++ " out of range for Int."+{-# INLINE sintVal #-}++-- | One more than the maximum representable 'Int' on the current platform.+type IntMaxP1 = 2 ^ (WORD_SIZE_IN_BITS - 1)++-- | Like 'sintVal', but with static proof that it's in-bounds.+--+-- This optimizes down to an actual primitive literal wrapped in the+-- appropriate constructors, unlike 'sintVal', where the bounds checking gets+-- in the way. If you're constructing a statically-known 'SInt', use+-- 'staticSIntVal'; while if you're constructing an 'SInt' from a runtime+-- 'KnownNat' instance, you'll have to use 'sintVal'.+staticSIntVal :: forall n. (CmpNat n IntMaxP1 ~ 'LT, KnownNat n) => SInt n+staticSIntVal = MkSInt (fromIntegral (natVal' @n proxy#))+{-# INLINE staticSIntVal #-}++-- | Add two 'SInt's with bounds checks; 'error' if the result overflows.+addSInt :: HasCallStack => SInt m -> SInt n -> SInt (m + n)+addSInt (SI# (I# m)) (SI# (I# n)) =+ case addIntC# m n of+ (# mn, ovf #)+ | I# ovf == 0 -> SI# (I# mn)+ | otherwise -> error $+ "Nat " +++ show (fromIntegral (I# m) + fromIntegral (I# n) :: Natural) +++ " out of range for Int."++-- | Multiply two 'SInt's with bounds checks; 'error' if the result overflows.+mulSInt :: HasCallStack => SInt m -> SInt n -> SInt (m * n)+mulSInt (SI# m@(I# m')) (SI# n@(I# n')) =+ case mulIntMayOflo# m' n' of+ ovf+ | I# ovf == 0 -> SI# mn+ | mn > 0 && fromIntegral mn == mnNat -> SI# mn+ | otherwise -> error $ "Nat " ++ show mnNat ++ " out of range for Int."+ where+ mn = m * n+ mnNat = fromIntegral m * fromIntegral n :: Natural++-- | Subtract two 'SInt's with bounds checks; 'error' if the result is negative.+subSInt :: HasCallStack => SInt m -> SInt n -> SInt (m - n)+subSInt (SI# m) (SI# n)+ | n > m = error $ "Nat " ++ show (m - n) ++ " out of range."+ | otherwise = SI# (m - n)++-- | Subtract two 'SInt's, using an inequality constraint to rule out overflow.+subSIntLE :: n <= m => SInt m -> SInt n -> SInt (m - n)+subSIntLE (SI# m) (SI# n) = SI# (m - n)++-- | "Un-add" an 'SInt' from another 'SInt', on the left.+--+-- This form of 'subSInt' is more convenient in certain cases when a type+-- signature ensures a particular 'SInt' is of the form @m + n@.+subSIntL :: SInt (m + n) -> SInt m -> SInt n+subSIntL (SI# mn) (SI# m) = SI# (mn - m)++-- | "Un-multiply" an 'SInt' by another 'SInt', on the left.+--+-- This form of @divSInt@ is more convenient in certain cases when a type+-- signature ensures a particular 'SInt' is of the form @m * n@.+divSIntL :: SInt (m * n) -> SInt m -> SInt n+divSIntL (SI# mn) (SI# m) = SI# (mn `div` m)++-- | "Un-multiply" an 'SInt' by another 'SInt', on the right.+--+-- This form of @divSInt@ is more convenient in certain cases when a type+-- signature ensures a particular 'SInt' is of the form @m * n@.+divSIntR :: SInt (m * n) -> SInt n -> SInt m+divSIntR (SI# mn) (SI# n) = SI# (mn `div` n)++-- | Bring an 'SInt' back into the type level as a 'KnownNat' instance.+reifySInt :: forall n r. SInt n -> (KnownNat n => r) -> r+reifySInt (SI# n) r =+ case someNatVal (fromIntegral n) of+ SomeNat (Proxy :: Proxy m) ->+#if MIN_VERSION_base(4,15,0)+ case unsafeEqualityProof @m @n of UnsafeRefl -> r+#else+ case unsafeCoerce Refl :: m :~: n of Refl -> r+#endif
+ test/Main.hs view
@@ -0,0 +1,100 @@+-- Copyright 2021 Google LLC+--+-- 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.++{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++module Main where++import Control.Exception (evaluate, try)+import Data.Bifunctor (first)+import Data.Functor (void)+import Data.Proxy (Proxy(..))+import GHC.Exception (ErrorCall)+import GHC.TypeNats (SomeNat(..), someNatVal, natVal)+import Numeric.Natural (Natural)++import Test.Framework (defaultMain)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.QuickCheck+ ( (===), (==>), forAll, Gen, arbitrary, ioProperty, scale+ , Positive(..), Negative(..), Property+ )++import Data.SInt++maxInt :: Natural+maxInt = fromIntegral (maxBound @Int)++naturals :: Gen Natural+naturals = fromInteger . getPositive <$> arbitrary++raisesError :: a -> Property+raisesError x = ioProperty $ do+ r <- try @ErrorCall $ evaluate x+ return $ void (first (const ()) r) === Left ()++main :: IO ()+main = defaultMain+ [ testProperty "trySIntVal in bounds" $ forAll naturals $+ \x -> x <= maxInt ==> case someNatVal x of+ SomeNat (Proxy :: Proxy n) ->+ fmap (fromIntegral . unSInt) (trySIntVal @n) === Just x++ , testProperty "trySIntVal out of bounds" $ forAll naturals $+ \x -> case someNatVal (maxInt + x) of+ SomeNat (Proxy :: Proxy n) ->+ void (trySIntVal @n) === Nothing++ , testProperty "withSInt negative raises" $ \ (Negative x) ->+ raisesError $ withSInt x $ const ()++ , testProperty "withSInt positive" $ \ (Positive x) ->+ withSInt x unSInt === x++ , testProperty "addSInt" $+ \ (Positive x) (Positive y) ->+ withSInt x $ \x' ->+ withSInt y $ \y' ->+ let xy = fromIntegral x + fromIntegral y :: Natural+ in if xy > maxInt+ then raisesError $ addSInt x' y'+ else fromIntegral (unSInt (addSInt x' y')) === xy++ , testProperty "addSInt out of range" $+ raisesError $ withSInt maxBound $ \x -> withSInt 1 (unSInt . addSInt x)++ , testProperty "subSInt" $+ \ (Positive x) (Positive y) ->+ withSInt x $ \x' ->+ withSInt y $ \y' ->+ if x < y+ then raisesError $ subSInt x' y'+ else unSInt (subSInt x' y') === x - y++ , testProperty "mulSInt" $+ forAll (scale (*1000000000) arbitrary) $ \ (Positive x) ->+ forAll (scale (*1000000000) arbitrary) $ \ (Positive y) ->+ withSInt x $ \x' ->+ withSInt y $ \y' ->+ let xy = fromIntegral x * fromIntegral y :: Natural+ in if xy > maxInt+ then raisesError $ mulSInt x' y'+ else fromIntegral (unSInt (mulSInt x' y')) === xy++ , testProperty "reifySInt" $+ \ (Positive x) ->+ withSInt x $ \ (x' :: SInt n) ->+ fromIntegral x === reifySInt x' (natVal @n Proxy)+ ]