diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,3 @@ +# 0.1.0.0 + +Initial version. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/fin-int.cabal b/fin-int.cabal new file mode 100644 --- /dev/null +++ b/fin-int.cabal @@ -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 +maintainer: Andrew Pritchard +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 diff --git a/src/Data/Fin/Int.hs b/src/Data/Fin/Int.hs new file mode 100644 --- /dev/null +++ b/src/Data/Fin/Int.hs @@ -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 diff --git a/src/Data/Fin/Int/Explicit.hs b/src/Data/Fin/Int/Explicit.hs new file mode 100644 --- /dev/null +++ b/src/Data/Fin/Int/Explicit.hs @@ -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)