fin-int (empty) → 0.1.0.0
raw patch · 5 files changed
+1111/−0 lines, 5 filesdep +QuickCheckdep +attenuationdep +base
Dependencies added: QuickCheck, attenuation, base, data-default-class, deepseq, portray, portray-diff, sint
Files
- CHANGELOG.md +3/−0
- LICENSE +202/−0
- fin-int.cabal +50/−0
- src/Data/Fin/Int.hs +315/−0
- src/Data/Fin/Int/Explicit.hs +541/−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.
+ fin-int.cabal view
@@ -0,0 +1,50 @@+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: 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+ length-indexed vectors.+category: Data+homepage: https://github.com/google/hs-fin-vec#readme+bug-reports: https://github.com/google/hs-fin-vec/issues+author: Lennart Augustsson <lennart@augustsson.net>+maintainer: Andrew Pritchard <awpr@google.com>+copyright: 2017-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: 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+ , 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+ default-language: Haskell2010
+ src/Data/Fin/Int.hs view
@@ -0,0 +1,315 @@+-- Copyright 2017-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 AllowAmbiguousTypes #-} -- for knownFin+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++-- | Finite natural numbers, with upper bound as part of the type.+--+-- A value of type @'Fin' n@ ranges from @0@ to @n - 1@.+--+-- Operations that can cause numbers to be out-of-range come with variants that+-- throw runtime errors, return 'Maybe', or return results modulo the bound.+--+-- In contrast to "Data.Fin.Int.Explicit", this module provides an API that+-- accepts the bounds values implicitly via 'KnownNat'. This can be more+-- convenient when there's no arithmetic involved in the bounds, but may cost+-- more runtime 'Numeric.Natural.Natural'-to-'Int' conversions.+--+-- When type-level arithmetic is involved, the+-- [ghc-typelits-knownnat](https://hackage.haskell.org/package/ghc-typelits-knownnat)+-- plugin may be useful to derive 'KnownNat' instances for bounds automatically.++module Data.Fin.Int+ ( -- * Finite Natural Numbers+ Fin, FinSize+ -- * Conversion+ , fin, finFromIntegral, knownFin, tryFin, finMod, finDivMod, finToInt+ -- * Bound Manipulation+ , embed, unembed, tryUnembed+ , shiftFin, unshiftFin, tryUnshiftFin, splitFin, concatFin+ , weaken, strengthen+ -- * Enumeration+ , minFin, maxFin+ , enumFin, enumFinDown, enumDownFrom, enumDownTo, enumDownFromTo+ -- * Arithmetic+ -- ** In 'Maybe'+ , tryAdd, trySub, tryMul+ , (+?), (-?), (*?)+ -- ** Checked+ , chkAdd, chkSub, chkMul+ , (+!), (-!), (*!)+ -- ** Modular arithmetic+ , modAdd, modSub, modMul, modNegate+ , (+%), (-%), (*%)+ -- ** Miscellaneous+ , divModFin+ , complementFin, twice, half, quarter+ , crossFin+ -- * Attenuations+ , attLT, attPlus, attMinus, attInt+ -- * Unsafe, fast+ , unsafeFin, unsafePred, unsafeSucc, unsafeCoFin, unsafeCoInt+ ) where++import Data.SInt (sintVal)+import GHC.Stack (HasCallStack)+import GHC.TypeNats (type (*), type (+), type (-), type (<=), KnownNat)++import Data.Fin.Int.Explicit+ ( Fin, FinSize, unsafeFin, unsafeSucc, unsafePred+ , unsafeCoFin, unsafeCoInt+ , attInt, attMinus, attPlus, attLT+ , half, quarter+ , embed, weaken, finToInt+ , modSub, trySub, minFin+ )+import qualified Data.Fin.Int.Explicit as E++-- | Construct a 'Fin' from an 'Int', with bounds checks.+{-# INLINE fin #-}+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.+{-# INLINE finFromIntegral #-}+finFromIntegral+ :: forall n a+ . (HasCallStack, KnownNat n, Integral a, Show a)+ => 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).+knownFin :: forall i n. (KnownNat i, i <= n - 1) => Fin n+knownFin = E.knownFin (sintVal @i)+{-# INLINE knownFin #-}++-- | Convert a number to a @Fin@, or @Nothing@ if out of range.+tryFin :: forall n a. (Integral a, KnownNat n) => a -> Maybe (Fin n)+tryFin = E.tryFin sintVal++-- | @finMod \@n x@ is equivalent to @fin \@n (x `mod` (valueOf \@n))@+--+-- This raises an exception iff @n ~ 0@. It could have been written with a+-- @0 < n@ constraint instead, but that would be annoying to prove repeatedly.+finMod :: forall n a . (HasCallStack, Integral a, KnownNat n) => a -> Fin n+finMod = E.finMod sintVal++-- | Decompose a number into a component modulo @n@ and the rest.+--+-- This raises an exception iff @n ~ 0@. See 'finMod'.+finDivMod+ :: forall n a+ . (HasCallStack, Integral a, KnownNat n)+ => a -> (a, Fin n)+finDivMod = E.finDivMod sintVal++-- | Reverse the order of the values of a 'Fin' type.+complementFin :: forall n. (KnownNat n) => Fin n -> Fin n+complementFin = E.complementFin sintVal++-- | (*2), but works even if 2 is out-of-bounds.+twice :: KnownNat n => Fin n -> Fin n+twice = E.twice sintVal++-- | The maximal value of the given inhabited 'Fin' type (i.e @n - 1@).+maxFin :: (1 <= n, KnownNat n) => Fin n+maxFin = E.maxFin sintVal+{-# INLINE maxFin #-}++-- | Enumerate the entire domain in ascending order. This is equivalent+-- to @enumFrom 0@ or @enumFrom minBound@, but without introducing a+-- spurious @(1 <= n)@ constraint.+enumFin :: forall n. KnownNat n => [Fin n]+enumFin = E.enumFin sintVal+{-# INLINE enumFin #-}++-- | Enumerate the entire domain in descending order. This is equivalent+-- to @reverse enumFin@, but without introducing a spurious @(1 <= n)@+-- constraint or breaking list-fusion.+enumFinDown :: forall n. KnownNat n => [Fin n]+enumFinDown = E.enumFinDown sintVal+{-# INLINE enumFinDown #-}++-- | Equivalent to @reverse (enumFromTo 0 x)@ but without introducing+-- a spurious @(1 <= n)@ constraint or breaking list-fusion.+enumDownFrom :: forall n. KnownNat n => Fin n -> [Fin n]+enumDownFrom = E.enumDownFrom sintVal+{-# INLINE enumDownFrom #-}++-- | Equivalent to @reverse (enumFromTo x maxBound)@ but without+-- introducing a spurious @(1 <= n)@ constraint or breaking list-fusion.+enumDownTo :: forall n. KnownNat n => Fin n -> [Fin n]+enumDownTo = E.enumDownTo sintVal+{-# INLINE enumDownTo #-}++-- | Equivalent to @reverse (enumFromTo y x)@ but without introducing+-- a spurious @(1 <= n)@ constraint or breaking list-fusion.+enumDownFromTo :: forall n. KnownNat n => Fin n -> Fin n -> [Fin n]+enumDownFromTo = E.enumDownFromTo sintVal+{-# INLINE enumDownFromTo #-}++-- TODO(awpr): it's possible to implement 'modAdd' and 'modSub' without+-- partiality, but it'd be slower. We should probably improve this somehow.++-- | Add modulo /n/.+--+-- Raises error when intermediate results overflow Int.+--+-- 'modAdd' and ('+%') are different names for the same function.+modAdd, (+%) :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n+modAdd = E.modAdd sintVal+(+%) = E.modAdd sintVal+{-# INLINEABLE modAdd #-}+{-# INLINEABLE (+%) #-}++-- | Subtract modulo /n/.+--+-- 'modSub' and ('-%') are different names for the same function.+(-%) :: forall n. KnownNat n => Fin n -> Fin n -> Fin n+(-%) = E.modSub sintVal+{-# INLINEABLE (-%) #-}++-- | Multiply modulo /n/.+--+-- Raises error when intermediate results overflow Int.+--+-- 'modMul' and ('*%') are different names for the same function.+modMul, (*%) :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n+modMul = E.modMul sintVal+(*%) = E.modMul sintVal+{-# INLINEABLE modMul #-}+{-# INLINEABLE (*%) #-}++-- | Negate modulo /n/.+--+-- Compared to 'complementFin', this is shifted by 1:+-- @complementFin 0 :: Fin n = n - 1@, while @modNegate 0 :: Fin n = 0@.+modNegate :: forall n. KnownNat n => Fin n -> Fin n+modNegate = E.modNegate sintVal++-- | Add, returning Nothing for out-of-range results.+tryAdd, (+?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)+tryAdd = E.tryAdd sintVal+(+?) = E.tryAdd sintVal+{-# INLINEABLE tryAdd #-}+{-# INLINEABLE (+?) #-}++-- | Subtract, returning Nothing for out-of-range results.+(-?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)+(-?) = E.trySub+{-# INLINEABLE (-?) #-}++-- | Multiply, returning Nothing for out-of-range results.+tryMul, (*?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)+tryMul = E.tryMul sintVal+(*?) = E.tryMul sintVal+{-# INLINEABLE tryMul #-}+{-# INLINEABLE (*?) #-}++-- | Split a 'Fin' of the form @d*x + y@ into @(x, y)@.+divModFin :: forall m d. KnownNat m => Fin (d * m) -> (Fin d, Fin m)+divModFin = E.divModFin sintVal++-- | Add and assert the result is in-range.+--+-- 'chkAdd' and ('+!') are different names for the same function.+chkAdd, (+!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n+chkAdd = E.chkAdd sintVal+(+!) = E.chkAdd sintVal+{-# INLINEABLE chkAdd #-}+{-# INLINEABLE (+!) #-}++-- | Subtract and assert the result is in-range.+--+-- 'chkSub' and ('-!') are different names for the same function.+chkSub, (-!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n+chkSub = E.chkSub sintVal+(-!) = E.chkSub sintVal+{-# INLINEABLE chkSub #-}+{-# INLINEABLE (-!) #-}++-- | Multiply and assert the result is in-range.+--+-- 'chkMul' and ('*!') are different names for the same function.+chkMul, (*!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n+chkMul = E.chkMul sintVal+(*!) = E.chkMul sintVal+{-# INLINEABLE chkMul #-}+{-# INLINEABLE (*!) #-}++-- | Shrink the bound by one if possible.+strengthen :: forall n. KnownNat n => Fin (n+1) -> Maybe (Fin n)+strengthen = E.strengthen sintVal++-- | 'shiftFin' increases the value and bound of a Fin both by @m@.+shiftFin :: forall m n. KnownNat m => Fin n -> Fin (m+n)+shiftFin = E.shiftFin sintVal++-- | 'unshiftFin' decreases the value and bound of a Fin both by @m@.+unshiftFin+ :: forall m n+ . (HasCallStack, KnownNat m, KnownNat n)+ => Fin (m+n) -> Fin n+unshiftFin = E.unshiftFin sintVal sintVal++-- | 'tryUnshiftFin' decreases the value and bound of a Fin both by @m@.+tryUnshiftFin+ :: forall m n+ . (KnownNat m, KnownNat n)+ => Fin (m+n) -> Maybe (Fin n)+tryUnshiftFin = E.tryUnshiftFin sintVal sintVal++-- | Deconstructs the given Fin into one of two cases depending where it lies+-- in the given range.+splitFin :: forall m n. KnownNat m => Fin (m + n) -> Either (Fin m) (Fin n)+splitFin = E.splitFin sintVal++-- | The inverse of 'splitFin'.+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.+{-# 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.+{-# INLINE tryUnembed #-}+tryUnembed :: KnownNat n => Fin m -> Maybe (Fin n)+tryUnembed = E.tryUnembed sintVal++-- | Given two 'Fin's, returns one the size of the inputs' cartesian product.+--+-- The second argument is the lower-order one, i.e.+--+-- > crossFin @_ @n (x+1) y = n + crossFin @_ @n x y+-- > crossFin @_ @n x (y+1) = 1 + crossFin @_ @n x y+crossFin :: forall m n. KnownNat n => Fin m -> Fin n -> Fin (m * n)+crossFin = E.crossFin sintVal
+ src/Data/Fin/Int/Explicit.hs view
@@ -0,0 +1,541 @@+-- Copyright 2017-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 BangPatterns #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}++-- | Finite natural numbers, with upper bound as part of the type.+--+-- A value of type @'Fin' n@ ranges from @0@ to @n - 1@.+--+-- Operations that can cause numbers to be out-of-range come with variants that+-- throw runtime errors, return 'Maybe', or return results modulo the bound.+--+-- In contrast to "Data.Fin.Int", this module provides an API where runtime+-- values of bound parameters are provided explicitly by 'SInt's, which can be+-- more intuitive than passing implicitly via 'KnownNat', and can avoid some+-- runtime 'Numeric.Natural.Natural'-to-'Int' conversions and bounds checks+-- resulting from 'KnownNat', at the cost of making some code more tedious+-- where the bounds "should" be obvious.++module Data.Fin.Int.Explicit+ ( -- * Finite Natural Numbers+ Fin, FinSize+ -- * Conversion+ , fin, finFromIntegral, knownFin, tryFin, finMod, finDivMod, finToInt+ -- * Bound Manipulation+ , embed, unembed, tryUnembed+ , shiftFin, unshiftFin, tryUnshiftFin, splitFin, concatFin+ , weaken, strengthen+ -- * Enumeration+ , minFin, maxFin+ , enumFin, enumFinDown, enumDownFrom, enumDownTo, enumDownFromTo+ -- * Arithmetic+ -- ** In 'Maybe'+ , tryAdd, trySub, tryMul+ -- ** Checked+ , chkAdd, chkSub, chkMul+ -- ** Modular arithmetic+ , modAdd, modSub, modMul, modNegate+ -- ** Miscellaneous+ , divModFin+ , complementFin, twice, half, quarter+ , crossFin+ -- * Attenuations+ , attLT, attPlus, attMinus, attInt+ -- * Unsafe, fast+ , 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.Type.Coercion (Coercion(..))+import GHC.Stack (HasCallStack, withFrozenCallStack)+import GHC.TypeNats+ ( type (*), type (+), type (-), type (<=)+ , Nat, KnownNat+ )++import Data.Default.Class (Default(..))+import Data.Portray (Portray)+import Data.Portray.Diff (Diff)+import Data.Type.Attenuation (Attenuation, coercible)+import Test.QuickCheck (Arbitrary(..), arbitraryBoundedEnum)++import Data.SInt (SInt, unSInt, sintVal)++-- We could use representation type Integer.+-- We use Int since this is likely to be the most efficient type,+-- partly because it's the natural word size for the machine, but also+-- because it's the type used to index into containers such as Data.Vector.+type FinRep = Int++-- | Naturals bounded above by @n@.+newtype Fin (n :: Nat) = Fin FinRep+ deriving (Eq, Ord, Data)+ -- Fin Read/Show behave like other numeric newtypes: drop the \"Fin\".+ deriving newtype (Show, Portray, Diff)++-- | 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++instance FinSize n => Arbitrary (Fin n) where+ arbitrary = arbitraryBoundedEnum++instance NFData (Fin n) where rnf (Fin x) = rnf x++-- | Construct a 'Fin' from an 'Int', with bounds checks.+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 #-}+finFromIntegral+ :: (HasCallStack, Integral a, Show a)+ => SInt n -> a -> Fin n+finFromIntegral n =+ -- We make sure to do the comparisons in a large integer type (namely FinRep)+ -- rather than something like Fin. Otherwise we'd always fail in the+ -- conversion @fin :: Fin 3 -> Fin 4@.+ fin n . fromIntegral++{-# INLINE ufin #-}+ufin :: HasCallStack => SInt n -> FinRep -> Fin n+ufin sn i+ | i >= n = error $ "Fin: number out of range " ++ show i ++ " >= " ++ show n+ | otherwise = Fin i+ where+ n = unSInt sn++-- | Like 'fin', but doesn't do any bounds checks. However, unlike+-- 'unsafeFin', this is safe (by virtue of the type constraints).+knownFin :: (i <= n - 1) => SInt i -> Fin n+knownFin = unsafeFin . unSInt+{-# INLINE knownFin #-}++-- | Like 'fin', but doesn't do any bounds checks.+{-# INLINE unsafeFin #-}+unsafeFin :: Integral a => a -> Fin n+unsafeFin = Fin . fromIntegral++-- | Convert a number to a @Fin@, or @Nothing@ if out of range.+tryFin :: Integral a => SInt n -> a -> Maybe (Fin n)+tryFin n x =+ if x >= 0 && x < fromIntegral (unSInt n)+ then Just (Fin (fromIntegral x))+ else Nothing++-- | @finMod \@n x@ is equivalent to @fin \@n (x `mod` (valueOf \@n))@+--+-- This raises an exception iff @n ~ 0@. It could have been written with a+-- @0 < n@ constraint instead, but that would be annoying to prove repeatedly.+finMod :: forall n a . (HasCallStack, Integral a) => SInt n -> a -> Fin n+finMod n = snd . finDivMod n++-- | Decompose a number into a component modulo @n@ and the rest.+--+-- This raises an exception iff @n ~ 0@. See 'finMod'.+finDivMod+ :: forall n a+ . (HasCallStack, Integral a)+ => SInt n -> a -> (a, Fin n)+finDivMod sn x+ | n == 0 = error "finDivMod: zero modulus."+ | otherwise = (fromIntegral d, Fin (fromIntegral m))+ where+ -- Do arithmetic in Integer because some types we could get for @a@ can't+ -- represent @valueOf @n@ (specifically, @Fin m@ with m <= n). We don't use+ -- @FinRep@ because that could make this incorrect for types larger than+ -- @FinRep@.+ (d, m) = divMod (fromIntegral x :: Integer) n+ n = toInteger $ unSInt sn++-- | Reverse the order of the values of a 'Fin' type.+complementFin :: SInt n -> Fin n -> Fin n+-- Cannot use (maxBound - x) because it would introduce a spurious (1 <= n)+-- constraint. We're not concerned about the n=0 case here because Fin 0 is+-- uninhabited so x can only ever be bottom. In this case, unsafeFin will+-- briefly create an invalid Fin, but evaluating the subtraction will end up+-- 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.+finToInt :: Fin n -> Int+finToInt (Fin i) = i+{-# INLINE finToInt #-}++-- | (*2), but works even if 2 is out-of-bounds.+twice :: SInt n -> Fin n -> Fin n+twice sn (Fin i) = ufin sn $ i * 2++-- | Divide by 2, rounding down.+half :: Fin n -> Fin n+half (Fin n) = Fin (n `quot` 2)++-- | Divide by 4, rounding down.+quarter :: Fin n -> Fin n+quarter (Fin n) = Fin (n `quot` 4)++-- | Decrement by 1, without the validity checks of 'pred'.+unsafePred :: Fin n -> Fin n+unsafePred (Fin x) = Fin (x - 1)+{-# INLINE unsafePred #-}++-- | Increment by 1, without the validity checks of 'succ'.+unsafeSucc :: Fin n -> Fin n+unsafeSucc (Fin x) = Fin (x + 1)+{-# INLINE unsafeSucc #-}++-- Note [Enumerations of Fins]+--+-- Enumerating lists of Fins is implemented by making the corresponding list of+-- Ints and coercing them via @map coerce@. This ensures that these functions+-- are "good list producers" (in the build/foldr fusion sense), by reusing the+-- same property of the Enum instance for Int. Using Fins directly doesn't work+-- (because 0 might be out of range), and coercing the whole list doesn't work+-- either because it interferes with fusion.++-- | Enumerate the entire domain in ascending order. This is equivalent+-- to @enumFrom 0@ or @enumFrom minBound@, but without introducing a+-- spurious @(1 <= n)@ constraint.+enumFin :: SInt n -> [Fin n]+-- See Note [Enumerations of Fins]+enumFin sn = map coerce [0 .. unSInt sn - 1]+{-# INLINE enumFin #-}++-- | Enumerate the entire domain in descending order. This is equivalent+-- to @reverse enumFin@, but without introducing a spurious @(1 <= n)@+-- constraint or breaking list-fusion.+enumFinDown :: SInt n -> [Fin n]+-- See Note [Enumerations of Fins]+enumFinDown sn = map coerce [unSInt sn - 1, unSInt sn - 2 .. 0]+{-# INLINE enumFinDown #-}++-- | Equivalent to @reverse (enumFromTo 0 x)@ but without introducing+-- a spurious @(1 <= n)@ constraint or breaking list-fusion.+enumDownFrom :: SInt n -> Fin n -> [Fin n]+-- See Note [Enumerations of Fins]+enumDownFrom _sn (Fin x) = map coerce [x, x - 1 .. 0]+{-# INLINE enumDownFrom #-}++-- | Equivalent to @reverse (enumFromTo x maxBound)@ but without+-- introducing a spurious @(1 <= n)@ constraint or breaking list-fusion.+enumDownTo :: SInt n -> Fin n -> [Fin n]+-- See Note [Enumerations of Fins]+enumDownTo sn (Fin x) = map coerce [unSInt sn - 1, unSInt sn - 2 .. x]+{-# INLINE enumDownTo #-}++-- | Equivalent to @reverse (enumFromTo y x)@ but without introducing+-- a spurious @(1 <= n)@ constraint or breaking list-fusion.+enumDownFromTo :: SInt n -> Fin n -> Fin n -> [Fin n]+-- See Note [Enumerations of Fins]+enumDownFromTo _sn (Fin x) (Fin y) = map coerce [x, x - 1 .. y]+{-# INLINE enumDownFromTo #-}++instance KnownNat n => Enum (Fin n) where+ pred (Fin x)+ | x > 0 = Fin (x - 1)+ | otherwise = error $+ "pred @(Fin " ++ show (unSInt @n sintVal) +++ "): no predecessor of 0"+ succ (Fin x)+ | x < n - 1 = Fin (x + 1)+ | otherwise = error $+ "succ @(Fin " ++ show n ++ "): no successor of " ++ show n+ where !n = unSInt @n sintVal+ toEnum = fin sintVal+ fromEnum = finToInt+ -- See Note [Enumerations of Fins]+ enumFrom (Fin x) =+ map coerce [x .. unSInt @n sintVal - 1]+ enumFromThen (Fin x) (Fin y) =+ map coerce [x, y .. unSInt @n sintVal - 1]+ enumFromTo (Fin x) (Fin z) = map coerce [x .. z]+ enumFromThenTo (Fin x) (Fin y) (Fin z) = map coerce [x, y .. z]+ {-# INLINE pred #-}+ {-# INLINE succ #-}+ {-# INLINE toEnum #-}+ {-# INLINE fromEnum #-}+ {-# INLINE enumFrom #-}+ {-# INLINE enumFromThen #-}+ {-# INLINE enumFromTo #-}+ {-# INLINE enumFromThenTo #-}++-- | The minimal value of the given inhabited 'Fin' type (i.e. @0@).+minFin :: 1 <= n => Fin n+minFin = Fin 0++-- | The maximal value of the given inhabited 'Fin' type (i.e @n - 1@).+maxFin :: 1 <= n => SInt n -> Fin n+maxFin sn = Fin (unSInt sn - 1)++instance FinSize n => Bounded (Fin n) where+ minBound = minFin+ maxBound = maxFin sintVal+ {-# INLINE minBound #-}+ {-# INLINE maxBound #-}++-- XXX This should have context 1<=n, but that stops deriving from+-- working for types containing a Fin.+instance KnownNat n => Default (Fin n) where+ def = fin sintVal (0 :: FinRep)++overflowedError+ :: forall n a+ . HasCallStack+ => SInt n -> String -> Fin n -> Fin n -> a+overflowedError sn nm x y = error $+ showString nm .+ showString " @" .+ shows (unSInt sn) .+ showString " " .+ shows x .+ showString " " .+ shows y $+ " overflowed FinRep."++outOfRangeError+ :: forall n a+ . HasCallStack+ => SInt n -> String -> Fin n -> Fin n -> FinRep -> a+outOfRangeError sn nm x y r = error $+ showString nm .+ showString " @" .+ shows (unSInt sn) .+ showString " " .+ shows x .+ showString " " .+ shows y .+ showString " = " .+ shows r $+ " out of range."++add_ :: SInt n -> Fin n -> Fin n -> Maybe (Bool, FinRep)+add_ sn = \ (Fin x) (Fin y) ->+ let z = x + y+ in if z < x+ then Nothing -- Overflowed Int.+ else Just (z < unSInt sn, z)+{-# INLINE add_ #-}++sub_ :: Fin n -> Fin n -> Maybe (Bool, FinRep)+sub_ = \ (Fin x) (Fin y) -> let z = x - y in Just (z >= 0, z)+{-# INLINE sub_ #-}++mul_ :: SInt n -> Fin n -> Fin n -> Maybe (Bool, FinRep)+mul_ sn = \ (Fin x) (Fin y) ->+ let z = x * y+ in if x /= 0 && z `div` x /= y+ then Nothing -- Overflowed Int.+ else Just (z < unSInt sn, z)+{-# INLINE mul_ #-}++mkMod+ :: HasCallStack+ => SInt n+ -> String+ -> (Fin n -> Fin n -> Maybe (Bool, FinRep)) -> Fin n -> Fin n -> Fin n+mkMod sn nm op = \ x y -> case x `op` y of+ Just (_ok, z) -> finMod sn z+ Nothing -> overflowedError sn nm x y+{-# INLINE mkMod #-}++-- TODO(awpr): it's possible to implement 'modAdd' and 'modSub' without+-- partiality, but it'd be slower. We should probably improve this somehow.++-- | Add modulo /n/.+--+-- Raises error when intermediate results overflow Int.+modAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n+modAdd sn = withFrozenCallStack mkMod sn "modAdd" (add_ sn)+{-# INLINEABLE modAdd #-}++-- | Subtract modulo /n/.+modSub :: SInt n -> Fin n -> Fin n -> Fin n+-- Cannot fail, so no HasCallStack.+modSub sn = mkMod sn "modSub" sub_+{-# INLINEABLE modSub #-}++-- | Multiply modulo /n/.+--+-- Raises error when intermediate results overflow Int.+modMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n+modMul sn = withFrozenCallStack mkMod sn "modMul" (mul_ sn)+{-# INLINEABLE modMul #-}++-- | Negate modulo /n/.+--+-- Compared to 'complementFin', this is shifted by 1:+-- @complementFin 0 :: Fin n = n - 1@, while @modNegate 0 :: Fin n = 0@.+modNegate :: SInt n -> Fin n -> Fin n+modNegate _ (Fin 0) = Fin 0+modNegate sn (Fin x) = Fin (unSInt sn - x)++mkTry+ :: (Fin n -> Fin n -> Maybe (Bool, FinRep))+ -> Fin n -> Fin n -> Maybe (Fin n)+mkTry op = \x y -> case op x y of+ Just (True, z) -> Just (Fin z)+ _ -> Nothing+{-# INLINE mkTry #-}++-- | Add, returning Nothing for out-of-range results.+tryAdd :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)+tryAdd = mkTry . add_+{-# INLINEABLE tryAdd #-}++-- | Subtract, returning Nothing for out-of-range results.+trySub :: Fin n -> Fin n -> Maybe (Fin n)+trySub = mkTry sub_+{-# INLINEABLE trySub #-}++-- | Multiply, returning Nothing for out-of-range results.+tryMul :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)+tryMul = mkTry . mul_+{-# INLINEABLE tryMul #-}++-- | Split a 'Fin' of the form @d*x + y@ into @(x, y)@.+divModFin :: SInt m -> Fin (d * m) -> (Fin d, Fin m)+divModFin sm (Fin x) = (Fin d, Fin r)+ where+ (d, r) = divMod x (unSInt sm)+{-# INLINEABLE divModFin #-}++mkChk+ :: HasCallStack+ => SInt n+ -> String+ -> (Fin n -> Fin n -> Maybe (Bool, FinRep))+ -> Fin n -> Fin n -> Fin n+mkChk sn nm op = \x y -> case op x y of+ Just (ok, z) -> if ok then Fin z else outOfRangeError sn nm x y z+ Nothing -> overflowedError sn nm x y+{-# INLINE mkChk #-}++-- | Add and assert the result is in-range.+chkAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n+chkAdd sn = withFrozenCallStack mkChk sn "chkAdd" (add_ sn)+{-# INLINEABLE chkAdd #-}++-- | Subtract and assert the result is in-range.+chkSub :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n+chkSub sn = withFrozenCallStack mkChk sn "chkSub" sub_+{-# INLINEABLE chkSub #-}++-- | Multiply and assert the result is in-range.+chkMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n+chkMul sn = withFrozenCallStack mkChk sn "chkMul" (mul_ sn)+{-# INLINEABLE chkMul #-}++-- | Restricted coercion to larger Fin types.+attLT :: (n <= m) => Attenuation (Fin n) (Fin m)+attLT = coercible++-- | Restricted coercion to larger Fin types.+attPlus :: Attenuation (Fin n) (Fin (n + k))+attPlus = coercible++-- | Restricted coercion to larger Fin types.+attMinus :: Attenuation (Fin (n - k)) (Fin n)+attMinus = coercible++-- | Restricted coercion to Int.+attInt :: Attenuation (Fin n) Int+attInt = coercible++-- | Unsafe coercion between any Fin types.+unsafeCoFin :: Coercion (Fin n) (Fin m)+unsafeCoFin = Coercion++-- | Unsafe coercion to and from Int.+unsafeCoInt :: Coercion (Fin n) Int+unsafeCoInt = Coercion++-- | 'embed' increasing the bound by exactly one.+weaken :: Fin n -> Fin (n+1)+weaken (Fin x) = Fin x++-- | Shrink the bound by one if possible.+strengthen :: SInt n -> Fin (n+1) -> Maybe (Fin n)+strengthen sn (Fin x) = if x == unSInt sn then Nothing else Just (Fin x)++-- | 'shiftFin' increases the value and bound of a Fin both by @m@.+shiftFin :: SInt m -> Fin n -> Fin (m+n)+shiftFin sm (Fin x) = Fin (unSInt sm + x)++-- | 'tryUnshiftFin' decreases the value and bound of a Fin both by @m@.+tryUnshiftFin :: SInt m -> SInt n -> Fin (m+n) -> Maybe (Fin n)+tryUnshiftFin sm sn (Fin x) = tryFin sn (x - unSInt sm)++-- | 'unshiftFin' decreases the value and bound of a Fin both by @m@.+unshiftFin :: HasCallStack => SInt m -> SInt n -> Fin (m+n) -> Fin n+unshiftFin sm sn (Fin x) = fin sn (x - unSInt sm)++-- | Deconstructs the given Fin into one of two cases depending where it lies+-- in the given range.+splitFin :: SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)+splitFin sm (Fin x)+ | x < unSInt sm = Left $ Fin x+ | otherwise = Right $ Fin (x - unSInt sm)++-- | The inverse of 'splitFin'.+concatFin :: SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)+concatFin sm e = case e of+ Left (Fin x) -> Fin x+ Right x -> shiftFin sm x++-- | Convert to a bigger type.+{-# 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.+{-# 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.+tryUnembed :: SInt n -> Fin m -> Maybe (Fin n)+tryUnembed sn (Fin i) = tryFin sn i++-- | Given two 'Fin's, returns one the size of the inputs' cartesian product.+--+-- The second argument is the lower-order one, i.e.+--+-- > crossFin @_ @n (x+1) y = n + crossFin @_ @n x y+-- > crossFin @_ @n x (y+1) = 1 + crossFin @_ @n x y+crossFin :: SInt n -> Fin m -> Fin n -> Fin (m * n)+crossFin sn (Fin x) (Fin y) = Fin (x * unSInt sn + y)