From 0331b67f16ef2d1bece322cb9c363bfa1c8c58f9 Mon Sep 17 00:00:00 2001 From: Brian McKeon Date: Fri, 2 Feb 2024 20:41:03 -0500 Subject: [PATCH] Prepare 0.2.1.0 release. Reformatted. Added workflows. Updated package metadata. --- .github/CODEOWNERS | 1 + .github/workflows/build.yaml | 12 + .github/workflows/release.yaml | 12 + .gitignore | 1 + CHANGELOG.md | 3 +- Setup.hs | 2 - fourmolu.yaml | 51 +++ natural-arithmetic.cabal | 55 +-- src/Arithmetic/Equal.hs | 26 +- src/Arithmetic/Fin.hs | 686 +++++++++++++++++++-------------- src/Arithmetic/Lt.hs | 245 +++++++----- src/Arithmetic/Lte.hs | 203 ++++++---- src/Arithmetic/Nat.hs | 164 ++++---- src/Arithmetic/Plus.hs | 12 +- src/Arithmetic/Types.hs | 58 +-- src/Arithmetic/Unsafe.hs | 71 ++-- 16 files changed, 946 insertions(+), 656 deletions(-) create mode 100644 .github/CODEOWNERS create mode 100644 .github/workflows/build.yaml create mode 100644 .github/workflows/release.yaml delete mode 100644 Setup.hs create mode 100644 fourmolu.yaml diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS new file mode 100644 index 0000000..f6c0b22 --- /dev/null +++ b/.github/CODEOWNERS @@ -0,0 +1 @@ +@byteverse/l3c diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml new file mode 100644 index 0000000..085bbaf --- /dev/null +++ b/.github/workflows/build.yaml @@ -0,0 +1,12 @@ +name: build +on: + pull_request: + branches: + - "*" + +jobs: + call-workflow: + uses: byteverse/.github/.github/workflows/build.yaml@main + secrets: inherit + with: + release: false diff --git a/.github/workflows/release.yaml b/.github/workflows/release.yaml new file mode 100644 index 0000000..bd0bbd5 --- /dev/null +++ b/.github/workflows/release.yaml @@ -0,0 +1,12 @@ +name: release +on: + push: + tags: + - "*" + +jobs: + call-workflow: + uses: byteverse/.github/.github/workflows/build.yaml@main + secrets: inherit + with: + release: true diff --git a/.gitignore b/.gitignore index 28d589b..cde1485 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +.vscode/ dist dist-* cabal-dev diff --git a/CHANGELOG.md b/CHANGELOG.md index d08d329..04b11bd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,8 +1,9 @@ # Revision history for natural-arithmetic -## 0.2.1.0 -- 2024-??-?? +## 0.2.1.0 -- 2024-02-02 * Add `fromInt` and `fromInt#` to `Arithmetic.Fin`. +* Update package metadata. ## 0.2.0.0 -- 2024-01-09 diff --git a/Setup.hs b/Setup.hs deleted file mode 100644 index 9a994af..0000000 --- a/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/fourmolu.yaml b/fourmolu.yaml new file mode 100644 index 0000000..40cd005 --- /dev/null +++ b/fourmolu.yaml @@ -0,0 +1,51 @@ +# Number of spaces per indentation step +indentation: 2 + +# Max line length for automatic line breaking +column-limit: 200 + +# Styling of arrows in type signatures (choices: trailing, leading, or leading-args) +function-arrows: trailing + +# How to place commas in multi-line lists, records, etc. (choices: leading or trailing) +comma-style: leading + +# Styling of import/export lists (choices: leading, trailing, or diff-friendly) +import-export-style: leading + +# Whether to full-indent or half-indent 'where' bindings past the preceding body +indent-wheres: false + +# Whether to leave a space before an opening record brace +record-brace-space: true + +# Number of spaces between top-level declarations +newlines-between-decls: 1 + +# How to print Haddock comments (choices: single-line, multi-line, or multi-line-compact) +haddock-style: multi-line + +# How to print module docstring +haddock-style-module: null + +# Styling of let blocks (choices: auto, inline, newline, or mixed) +let-style: auto + +# How to align the 'in' keyword with respect to the 'let' keyword (choices: left-align, right-align, or no-space) +in-style: right-align + +# Whether to put parentheses around a single constraint (choices: auto, always, or never) +single-constraint-parens: always + +# Output Unicode syntax (choices: detect, always, or never) +unicode: never + +# Give the programmer more choice on where to insert blank lines +respectful: true + +# Fixity information for operators +fixities: [] + +# Module reexports Fourmolu should know about +reexports: [] + diff --git a/natural-arithmetic.cabal b/natural-arithmetic.cabal index 64bc4a3..a821b78 100644 --- a/natural-arithmetic.cabal +++ b/natural-arithmetic.cabal @@ -1,7 +1,7 @@ -cabal-version: 2.2 -name: natural-arithmetic -version: 0.2.1.0 -synopsis: Arithmetic of natural numbers +cabal-version: 2.2 +name: natural-arithmetic +version: 0.2.1.0 +synopsis: Arithmetic of natural numbers description: A search for terms like `arithmetic` and `natural` on hackage reveals no shortage of libraries for handling the arithmetic of natural @@ -18,7 +18,7 @@ description: application code, not in library code. This is because libraries should not require the presence of typechecker plugins. Technically, they can (you could document it), but many developers will not - use libraries that have unusual install procedures like this. + use libraries that have unusual install procedures like this. . This library, in places, requires users to use the 'TypeApplications` language extension. This is done when a number is only need at @@ -28,7 +28,7 @@ description: in `Arithmetic.Lt` and `Arithmetic.Lte`. This is done in the interest of making it easy for user to assemble proofs. Recall that proof assembly is done by hand rather than by an SMT solver, so removing - some tediousness from this is helpful to users. + some tediousness from this is helpful to users. . This library provides left and variants variants of several functions. For example, `Arithmetic.Lte` provides both `substituteL` and @@ -54,29 +54,40 @@ description: * Decrement: Decrease an upper bound along with the bounded value . * Substitute: Replace a number with an equal number -homepage: https://github.com/andrewthad/natural-arithmetic -bug-reports: https://github.com/andrewthad/natural-arithmetic/issues -license: BSD-3-Clause -license-file: LICENSE -author: Andrew Martin -maintainer: andrew.thaddeus@gmail.com -copyright: 2019 Andrew Martin -category: Math -extra-source-files: CHANGELOG.md + +homepage: https://github.com/byteverse/natural-arithmetic +bug-reports: https://github.com/byteverse/natural-arithmetic/issues +license: BSD-3-Clause +license-file: LICENSE +author: Andrew Martin +maintainer: amartin@layer3com.com +copyright: 2019 Andrew Martin +category: Math +extra-doc-files: CHANGELOG.md + +common build-settings + default-language: Haskell2010 + ghc-options: -Wall -Wunused-packages library + import: build-settings exposed-modules: - Arithmetic.Fin Arithmetic.Equal + Arithmetic.Fin Arithmetic.Lt Arithmetic.Lte Arithmetic.Nat + Arithmetic.Plus Arithmetic.Types Arithmetic.Unsafe - Arithmetic.Plus + build-depends: - , base>=4.14 && <5 - , unlifted >=0.2.1 - hs-source-dirs: src - default-language: Haskell2010 - ghc-options: -Wall -O2 + , base >=4.14 && <5 + , unlifted >=0.2.1 + + hs-source-dirs: src + ghc-options: -O2 + +source-repository head + type: git + location: git://github.com/byteverse/natural-arithmetic.git diff --git a/src/Arithmetic/Equal.hs b/src/Arithmetic/Equal.hs index 467b1ee..a3ede27 100644 --- a/src/Arithmetic/Equal.hs +++ b/src/Arithmetic/Equal.hs @@ -1,9 +1,9 @@ -{-# language DataKinds #-} -{-# language ExplicitForAll #-} -{-# language KindSignatures #-} -{-# language MagicHash #-} -{-# language TypeOperators #-} -{-# language UnboxedTuples #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} module Arithmetic.Equal ( symmetric @@ -14,29 +14,29 @@ module Arithmetic.Equal , lift ) where -import Arithmetic.Unsafe (type (:=:)(Eq), type (:=:#)(Eq#)) +import Arithmetic.Unsafe (type (:=:) (Eq), type (:=:#) (Eq#)) import GHC.TypeNats (type (+)) symmetric :: (m :=: n) -> (n :=: m) -{-# inline symmetric #-} +{-# INLINE symmetric #-} symmetric Eq = Eq plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n) -{-# inline plusL #-} +{-# INLINE plusL #-} plusL Eq = Eq plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c) -{-# inline plusR #-} +{-# INLINE plusR #-} plusR Eq = Eq plusL# :: forall c m n. (m :=:# n) -> (c + m :=:# c + n) -{-# inline plusL# #-} +{-# INLINE plusL# #-} plusL# _ = Eq# (# #) plusR# :: forall c m n. (m :=:# n) -> (m + c :=:# n + c) -{-# inline plusR# #-} +{-# INLINE plusR# #-} plusR# _ = Eq# (# #) lift :: (m :=:# n) -> (m :=: n) -{-# inline lift #-} +{-# INLINE lift #-} lift _ = Eq diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs index 4127395..c43b4b3 100644 --- a/src/Arithmetic/Fin.hs +++ b/src/Arithmetic/Fin.hs @@ -1,15 +1,15 @@ -{-# language BangPatterns #-} -{-# language DataKinds #-} -{-# language ExplicitNamespaces #-} -{-# language GADTs #-} -{-# language KindSignatures #-} -{-# language MagicHash #-} -{-# language PatternSynonyms #-} -{-# language RankNTypes #-} -{-# language ScopedTypeVariables #-} -{-# language TypeApplications #-} -{-# language TypeOperators #-} -{-# language UnboxedTuples #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} + module Arithmetic.Fin ( -- * Modification incrementL @@ -20,7 +20,9 @@ module Arithmetic.Fin , weakenR , succ , succ# + -- * Traverse + -- | These use the terms @ascend@ and @descend@ rather than the -- more popular @l@ (left) and @r@ (right) that pervade the Haskell -- ecosystem. The general rule is that ascending functions pair @@ -43,180 +45,218 @@ module Arithmetic.Fin , descending , ascendingSlice , descendingSlice + -- * Absurdities , absurd + -- * Demote , demote , demote# + -- * Deconstruct , with , with# + -- * Construct , construct# , remInt# , remWord# , fromInt , fromInt# + -- * Lift and Unlift , lift , unlift ) where -import Prelude hiding (last,succ) +import Prelude hiding (last, succ) import Arithmetic.Nat (( Fin n -> Fin (n + m) -{-# inline incrementR #-} +{-# INLINE incrementR #-} incrementR m (Fin i pf) = Fin (Nat.plus i m) (Lt.incrementR @m pf) incrementR# :: forall n m. Nat# m -> Fin# n -> Fin# (n + m) -{-# inline incrementR# #-} +{-# INLINE incrementR# #-} incrementR# (Nat# n) (Fin# i) = Fin# (n +# i) --- | Raise the index by @m@ and weaken the bound by @m@, adding --- @m@ to the left-hand side of @n@. +{- | Raise the index by @m@ and weaken the bound by @m@, adding +@m@ to the left-hand side of @n@. +-} incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n) -{-# inline incrementL #-} +{-# INLINE incrementL #-} incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf) --- | Weaken the bound by @m@, adding it to the left-hand side of --- the existing bound. This does not change the index. +{- | Weaken the bound by @m@, adding it to the left-hand side of +the existing bound. This does not change the index. +-} weakenL :: forall n m. Fin n -> Fin (m + n) -{-# inline weakenL #-} -weakenL (Fin i pf) = Fin i - ( Lt.substituteR - (Plus.commutative @n @m) - (Lt.plus pf (Lte.zero @m)) - ) - --- | Weaken the bound by @m@, adding it to the right-hand side of --- the existing bound. This does not change the index. +{-# INLINE weakenL #-} +weakenL (Fin i pf) = + Fin + i + ( Lt.substituteR + (Plus.commutative @n @m) + (Lt.plus pf (Lte.zero @m)) + ) + +{- | Weaken the bound by @m@, adding it to the right-hand side of +the existing bound. This does not change the index. +-} weakenR :: forall n m. Fin n -> Fin (n + m) -{-# inline weakenR #-} +{-# INLINE weakenR #-} weakenR (Fin i pf) = Fin i (Lt.plus pf Lte.zero) --- | Weaken the bound, replacing it by another number greater than --- or equal to itself. This does not change the index. +{- | Weaken the bound, replacing it by another number greater than +or equal to itself. This does not change the index. +-} weaken :: forall n m. (n <= m) -> Fin n -> Fin m -{-# inline weaken #-} +{-# INLINE weaken #-} weaken lt (Fin i pf) = Fin i (Lt.transitiveNonstrictR pf lt) -- | A finite set of no values is impossible. absurd :: Fin 0 -> void -{-# inline absurd #-} +{-# INLINE absurd #-} absurd (Fin _ pf) = Lt.absurd pf --- | Fold over the numbers bounded by @n@ in descending --- order. This is lazy in the accumulator. For convenince, --- this differs from @foldr@ in the order of the parameters. --- --- > descend 4 z f = f 0 (f 1 (f 2 (f 3 z))) -descend :: forall a n. - Nat n -- ^ Upper bound - -> a -- ^ Initial accumulator - -> (Fin n -> a -> a) -- ^ Update accumulator - -> a -{-# inline descend #-} +{- | Fold over the numbers bounded by @n@ in descending +order. This is lazy in the accumulator. For convenince, +this differs from @foldr@ in the order of the parameters. + +> descend 4 z f = f 0 (f 1 (f 2 (f 3 z))) +-} +descend :: + forall a n. + -- | Upper bound + Nat n -> + -- | Initial accumulator + a -> + -- | Update accumulator + (Fin n -> a -> a) -> + a +{-# INLINE descend #-} descend !n b0 f = go Nat.zero - where + where go :: Nat m -> a go !m = case m b0 Just lt -> f (Fin m lt) (go (Nat.succ m)) -descend# :: forall a n. - Nat# n -- ^ Upper bound - -> a -- ^ Initial accumulator - -> (Fin# n -> a -> a) -- ^ Update accumulator - -> a -{-# inline descend# #-} +descend# :: + forall a n. + -- | Upper bound + Nat# n -> + -- | Initial accumulator + a -> + -- | Update accumulator + (Fin# n -> a -> a) -> + a +{-# INLINE descend# #-} descend# !n b0 f = descend (Nat.lift n) b0 (\ix a -> f (unlift ix) a) --- | Fold over the numbers bounded by @n@ in descending --- order. This is strict in the accumulator. For convenince, --- this differs from @foldr'@ in the order of the parameters. --- --- > descend 4 z f = f 0 (f 1 (f 2 (f 3 z))) -descend' :: forall a n. - Nat n -- ^ Upper bound - -> a -- ^ Initial accumulator - -> (Fin n -> a -> a) -- ^ Update accumulator - -> a -{-# inline descend' #-} +{- | Fold over the numbers bounded by @n@ in descending +order. This is strict in the accumulator. For convenince, +this differs from @foldr'@ in the order of the parameters. + +> descend 4 z f = f 0 (f 1 (f 2 (f 3 z))) +-} +descend' :: + forall a n. + -- | Upper bound + Nat n -> + -- | Initial accumulator + a -> + -- | Update accumulator + (Fin n -> a -> a) -> + a +{-# INLINE descend' #-} descend' !n !b0 f = go n Lte.reflexive b0 - where - go :: Nat p -> p <= n -> a -> a - go !m pLteEn !b = case Nat.monus m Nat.one of - Nothing -> b - Just (Difference (mpred :: Nat c) cPlusOneEqP) -> - let !cLtEn = descendLemma cPlusOneEqP pLteEn - in go mpred (Lte.fromStrict cLtEn) (f (Fin mpred cLtEn) b) - --- | Fold over the numbers bounded by @n@ in ascending order. This --- is lazy in the accumulator. --- --- > ascend 4 z f = f 3 (f 2 (f 1 (f 0 z))) -ascend :: forall a n. - Nat n - -> a - -> (Fin n -> a -> a) - -> a -{-# inline ascend #-} + where + go :: Nat p -> p <= n -> a -> a + go !m pLteEn !b = case Nat.monus m Nat.one of + Nothing -> b + Just (Difference (mpred :: Nat c) cPlusOneEqP) -> + let !cLtEn = descendLemma cPlusOneEqP pLteEn + in go mpred (Lte.fromStrict cLtEn) (f (Fin mpred cLtEn) b) + +{- | Fold over the numbers bounded by @n@ in ascending order. This +is lazy in the accumulator. + +> ascend 4 z f = f 3 (f 2 (f 1 (f 0 z))) +-} +ascend :: + forall a n. + Nat n -> + a -> + (Fin n -> a -> a) -> + a +{-# INLINE ascend #-} ascend !n !b0 f = go n Lte.reflexive - where - go :: Nat p -> (p <= n) -> a - go !m pLteEn = case Nat.monus m Nat.one of - Nothing -> b0 - Just (Difference (mpred :: Nat c) cPlusOneEqP) -> - let !cLtEn = descendLemma cPlusOneEqP pLteEn - in f (Fin mpred cLtEn) (go mpred (Lte.fromStrict cLtEn)) - --- | Strict fold over the numbers bounded by @n@ in ascending --- order. For convenince, this differs from @foldl'@ in the --- order of the parameters. --- --- > ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z))) -ascend' :: forall a n. - Nat n -- ^ Upper bound - -> a -- ^ Initial accumulator - -> (Fin n -> a -> a) -- ^ Update accumulator - -> a -{-# inline ascend' #-} + where + go :: Nat p -> (p <= n) -> a + go !m pLteEn = case Nat.monus m Nat.one of + Nothing -> b0 + Just (Difference (mpred :: Nat c) cPlusOneEqP) -> + let !cLtEn = descendLemma cPlusOneEqP pLteEn + in f (Fin mpred cLtEn) (go mpred (Lte.fromStrict cLtEn)) + +{- | Strict fold over the numbers bounded by @n@ in ascending +order. For convenince, this differs from @foldl'@ in the +order of the parameters. + +> ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z))) +-} +ascend' :: + forall a n. + -- | Upper bound + Nat n -> + -- | Initial accumulator + a -> + -- | Update accumulator + (Fin n -> a -> a) -> + a +{-# INLINE ascend' #-} ascend' !n !b0 f = go Nat.zero b0 - where + where go :: Nat m -> a -> a go !m !b = case m b Just lt -> go (Nat.succ m) (f (Fin m lt) b) --- | Generalization of @ascend'@ that lets the caller pick the starting index: --- --- > ascend' === ascendFrom' 0 -ascendFrom' :: forall a m n. - Nat m -- ^ Index to start at - -> Nat n -- ^ Number of steps to take - -> a -- ^ Initial accumulator - -> (Fin (m + n) -> a -> a) -- ^ Update accumulator - -> a -{-# inline ascendFrom' #-} +{- | Generalization of @ascend'@ that lets the caller pick the starting index: + +> ascend' === ascendFrom' 0 +-} +ascendFrom' :: + forall a m n. + -- | Index to start at + Nat m -> + -- | Number of steps to take + Nat n -> + -- | Initial accumulator + a -> + -- | Update accumulator + (Fin (m + n) -> a -> a) -> + a +{-# INLINE ascendFrom' #-} ascendFrom' !m0 !n !b0 f = go m0 b0 - where + where end = Nat.plus m0 n go :: Nat k -> a -> a go !m !b = case m go (Nat.succ m) (f (Fin m lt) b) -- | Variant of @ascendFrom'@ with unboxed arguments. -ascendFrom'# :: forall a m n. - Nat# m -- ^ Index to start at - -> Nat# n -- ^ Number of steps to take - -> a -- ^ Initial accumulator - -> (Fin# (m + n) -> a -> a) -- ^ Update accumulator - -> a -{-# inline ascendFrom'# #-} +ascendFrom'# :: + forall a m n. + -- | Index to start at + Nat# m -> + -- | Number of steps to take + Nat# n -> + -- | Initial accumulator + a -> + -- | Update accumulator + (Fin# (m + n) -> a -> a) -> + a +{-# INLINE ascendFrom'# #-} ascendFrom'# !m0 !n !b0 f = ascendFrom' (Nat.lift m0) (Nat.lift n) b0 (\ix -> f (unlift ix)) --- | Strict monadic left fold over the numbers bounded by @n@ --- in ascending order. Roughly: --- --- > ascendM 4 z0 f = --- > f 0 z0 >>= \z1 -> --- > f 1 z1 >>= \z2 -> --- > f 2 z2 >>= \z3 -> --- > f 3 z3 -ascendM :: forall m a n. Monad m - => Nat n -- ^ Upper bound - -> a -- ^ Initial accumulator - -> (Fin n -> a -> m a) -- ^ Update accumulator - -> m a -{-# inline ascendM #-} +{- | Strict monadic left fold over the numbers bounded by @n@ +in ascending order. Roughly: + +> ascendM 4 z0 f = +> f 0 z0 >>= \z1 -> +> f 1 z1 >>= \z2 -> +> f 2 z2 >>= \z3 -> +> f 3 z3 +-} +ascendM :: + forall m a n. + (Monad m) => + -- | Upper bound + Nat n -> + -- | Initial accumulator + a -> + -- | Update accumulator + (Fin n -> a -> m a) -> + m a +{-# INLINE ascendM #-} ascendM !n !b0 f = go Nat.zero b0 - where + where go :: Nat p -> a -> m a go !m !b = case m pure b Just lt -> go (Nat.succ m) =<< f (Fin m lt) b --- | Variant of @ascendM@ that takes an unboxed Nat and provides --- an unboxed Fin to the callback. -ascendM# :: forall m a n. Monad m - => Nat# n -- ^ Upper bound - -> a -- ^ Initial accumulator - -> (Fin# n -> a -> m a) -- ^ Update accumulator - -> m a -{-# inline ascendM# #-} +{- | Variant of @ascendM@ that takes an unboxed Nat and provides +an unboxed Fin to the callback. +-} +ascendM# :: + forall m a n. + (Monad m) => + -- | Upper bound + Nat# n -> + -- | Initial accumulator + a -> + -- | Update accumulator + (Fin# n -> a -> m a) -> + m a +{-# INLINE ascendM# #-} ascendM# n !a0 f = ascendM (Nat.lift n) a0 (\ix a -> f (unlift ix) a) --- | Monadic traversal of the numbers bounded by @n@ --- in ascending order. --- --- > ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3 -ascendM_ :: forall m a n. Applicative m - => Nat n -- ^ Upper bound - -> (Fin n -> m a) -- ^ Effectful interpretion - -> m () -{-# inline ascendM_ #-} +{- | Monadic traversal of the numbers bounded by @n@ +in ascending order. + +> ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3 +-} +ascendM_ :: + forall m a n. + (Applicative m) => + -- | Upper bound + Nat n -> + -- | Effectful interpretion + (Fin n -> m a) -> + m () +{-# INLINE ascendM_ #-} ascendM_ !n f = go Nat.zero - where + where go :: Nat p -> m () go !m = case m pure () Just lt -> f (Fin m lt) *> go (Nat.succ m) --- | Variant of @ascendM_@ that takes an unboxed Nat and provides --- an unboxed Fin to the callback. -ascendM_# :: forall m a n. Monad m - => Nat# n -- ^ Upper bound - -> (Fin# n -> m a) -- ^ Update accumulator - -> m () -{-# inline ascendM_# #-} +{- | Variant of @ascendM_@ that takes an unboxed Nat and provides +an unboxed Fin to the callback. +-} +ascendM_# :: + forall m a n. + (Monad m) => + -- | Upper bound + Nat# n -> + -- | Update accumulator + (Fin# n -> m a) -> + m () +{-# INLINE ascendM_# #-} ascendM_# n f = ascendM_ (Nat.lift n) (\ix -> f (unlift ix)) descendLemma :: forall a b c. a + 1 :=: b -> b <= c -> a < c -{-# inline descendLemma #-} -descendLemma !aPlusOneEqB !bLteC = id - $ Lt.transitiveNonstrictR - (Lt.substituteR (Plus.commutative @1 @a) - (Lt.plus Lt.zero Lte.reflexive)) - $ Lte.substituteL (Eq.symmetric aPlusOneEqB) bLteC - --- | Strict monadic left fold over the numbers bounded by @n@ --- in descending order. Roughly: --- --- > descendM 4 z f = --- > f 3 z0 >>= \z1 -> --- > f 2 z1 >>= \z2 -> --- > f 1 z2 >>= \z3 -> --- > f 0 z3 -descendM :: forall m a n. Monad m - => Nat n - -> a - -> (Fin n -> a -> m a) - -> m a -{-# inline descendM #-} +{-# INLINE descendLemma #-} +descendLemma !aPlusOneEqB !bLteC = + id + $ Lt.transitiveNonstrictR + ( Lt.substituteR + (Plus.commutative @1 @a) + (Lt.plus Lt.zero Lte.reflexive) + ) + $ Lte.substituteL (Eq.symmetric aPlusOneEqB) bLteC + +{- | Strict monadic left fold over the numbers bounded by @n@ +in descending order. Roughly: + +> descendM 4 z f = +> f 3 z0 >>= \z1 -> +> f 2 z1 >>= \z2 -> +> f 1 z2 >>= \z3 -> +> f 0 z3 +-} +descendM :: + forall m a n. + (Monad m) => + Nat n -> + a -> + (Fin n -> a -> m a) -> + m a +{-# INLINE descendM #-} descendM !n !b0 f = go n Lte.reflexive b0 - where - go :: Nat p -> p <= n -> a -> m a - go !m pLteEn !b = case Nat.monus m Nat.one of - Nothing -> pure b - Just (Difference (mpred :: Nat c) cPlusOneEqP) -> - let !cLtEn = descendLemma cPlusOneEqP pLteEn - in go mpred (Lte.fromStrict cLtEn) =<< f (Fin mpred cLtEn) b - --- | Monadic traversal of the numbers bounded by @n@ --- in descending order. --- --- > descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0 -descendM_ :: forall m a n. Applicative m - => Nat n -- ^ Upper bound - -> (Fin n -> m a) -- ^ Effectful interpretion - -> m () -{-# inline descendM_ #-} + where + go :: Nat p -> p <= n -> a -> m a + go !m pLteEn !b = case Nat.monus m Nat.one of + Nothing -> pure b + Just (Difference (mpred :: Nat c) cPlusOneEqP) -> + let !cLtEn = descendLemma cPlusOneEqP pLteEn + in go mpred (Lte.fromStrict cLtEn) =<< f (Fin mpred cLtEn) b + +{- | Monadic traversal of the numbers bounded by @n@ +in descending order. + +> descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0 +-} +descendM_ :: + forall m a n. + (Applicative m) => + -- | Upper bound + Nat n -> + -- | Effectful interpretion + (Fin n -> m a) -> + m () +{-# INLINE descendM_ #-} descendM_ !n f = go n Lte.reflexive - where + where go :: Nat p -> p <= n -> m () go !m !pLteEn = case Nat.monus m Nat.one of Nothing -> pure () Just (Difference (mpred :: Nat c) cPlusOneEqP) -> let !cLtEn = descendLemma cPlusOneEqP pLteEn - in f (Fin mpred cLtEn) *> go mpred (Lte.fromStrict cLtEn) + in f (Fin mpred cLtEn) *> go mpred (Lte.fromStrict cLtEn) + +{- | Generate all values of a finite set in ascending order. --- | Generate all values of a finite set in ascending order. --- --- >>> ascending (Nat.constant @3) --- [Fin 0,Fin 1,Fin 2] +>>> ascending (Nat.constant @3) +[Fin 0,Fin 1,Fin 2] +-} ascending :: forall n. Nat n -> [Fin n] ascending !n = go Nat.zero - where + where go :: Nat m -> [Fin n] go !m = case m [] Just lt -> Fin m lt : go (Nat.succ m) --- | Generate all values of a finite set in descending order. --- --- >>> descending (Nat.constant @3) --- [Fin 2,Fin 1,Fin 0] +{- | Generate all values of a finite set in descending order. + +>>> descending (Nat.constant @3) +[Fin 2,Fin 1,Fin 0] +-} descending :: forall n. Nat n -> [Fin n] descending !n = go n Lte.reflexive - where - go :: Nat p -> (p <= n) -> [Fin n] - go !m !pLteEn = case Nat.monus m Nat.one of - Nothing -> [] - Just (Difference (mpred :: Nat c) cPlusOneEqP) -> - let !cLtEn = descendLemma cPlusOneEqP pLteEn - in Fin mpred cLtEn : go mpred (Lte.fromStrict cLtEn) - --- | Generate 'len' values starting from 'off' in ascending order. --- --- >>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6) --- [Fin 2,Fin 3,Fin 4] -ascendingSlice - :: forall n off len - . Nat off - -> Nat len - -> off + len <= n - -> [Fin n] -{-# inline ascendingSlice #-} + where + go :: Nat p -> (p <= n) -> [Fin n] + go !m !pLteEn = case Nat.monus m Nat.one of + Nothing -> [] + Just (Difference (mpred :: Nat c) cPlusOneEqP) -> + let !cLtEn = descendLemma cPlusOneEqP pLteEn + in Fin mpred cLtEn : go mpred (Lte.fromStrict cLtEn) + +{- | Generate 'len' values starting from 'off' in ascending order. + +>>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6) +[Fin 2,Fin 3,Fin 4] +-} +ascendingSlice :: + forall n off len. + Nat off -> + Nat len -> + off + len <= n -> + [Fin n] +{-# INLINE ascendingSlice #-} ascendingSlice off len !offPlusLenLteEn = go Nat.zero - where - go :: Nat m -> [Fin n] - go !m = case m [] - Just emLtLen -> - let !offPlusEmLtOffPlusLen = Lt.incrementL @off emLtLen - !offPlusEmLtEn = Lt.transitiveNonstrictR offPlusEmLtOffPlusLen offPlusLenLteEn - in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m) - --- | Generate 'len' values starting from 'off + len - 1' in descending order. --- --- >>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6) --- [Fin 4,Fin 3,Fin 2] -descendingSlice - :: forall n off len - . Nat off - -> Nat len - -> off + len <= n - -> [Fin n] -{-# inline descendingSlice #-} + where + go :: Nat m -> [Fin n] + go !m = case m [] + Just emLtLen -> + let !offPlusEmLtOffPlusLen = Lt.incrementL @off emLtLen + !offPlusEmLtEn = Lt.transitiveNonstrictR offPlusEmLtOffPlusLen offPlusLenLteEn + in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m) + +{- | Generate 'len' values starting from 'off + len - 1' in descending order. + +>>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6) +[Fin 4,Fin 3,Fin 2] +-} +descendingSlice :: + forall n off len. + Nat off -> + Nat len -> + off + len <= n -> + [Fin n] +{-# INLINE descendingSlice #-} descendingSlice !off !len !offPlusLenLteEn = go len Lte.reflexive - where - go :: Nat m -> m <= len -> [Fin n] - go !m !mLteEn = case Nat.monus m Nat.one of - Nothing -> [] - Just (Difference (mpred :: Nat c) cPlusOneEqEm) -> - let !cLtLen = Lt.transitiveNonstrictR + where + go :: Nat m -> m <= len -> [Fin n] + go !m !mLteEn = case Nat.monus m Nat.one of + Nothing -> [] + Just (Difference (mpred :: Nat c) cPlusOneEqEm) -> + let !cLtLen = + Lt.transitiveNonstrictR (Lt.substituteR (Plus.commutative @1 @c) (Lt.plus Lt.zero Lte.reflexive)) -- c < c + 1 (Lte.substituteL (Eq.symmetric cPlusOneEqEm) mLteEn) - -- c + 1 <= len - !cPlusOffLtEn = Lt.transitiveNonstrictR - (Lt.substituteR - (Plus.commutative @len @off) - (Lt.plus cLtLen (Lte.reflexive @off))) + -- c + 1 <= len + !cPlusOffLtEn = + Lt.transitiveNonstrictR + ( Lt.substituteR + (Plus.commutative @len @off) + (Lt.plus cLtLen (Lte.reflexive @off)) + ) -- c + off < off + len offPlusLenLteEn - in Fin (mpred `Nat.plus` off) cPlusOffLtEn : go mpred (Lte.fromStrict cLtLen) + in Fin (mpred `Nat.plus` off) cPlusOffLtEn : go mpred (Lte.fromStrict cLtLen) --- | Extract the 'Int' from a 'Fin n'. This is intended to be used --- at a boundary where a safe interface meets the unsafe primitives --- on top of which it is built. +{- | Extract the 'Int' from a 'Fin n'. This is intended to be used +at a boundary where a safe interface meets the unsafe primitives +on top of which it is built. +-} demote :: Fin n -> Int -{-# inline demote #-} +{-# INLINE demote #-} demote (Fin i _) = Nat.demote i demote# :: Fin# n -> Int# -{-# inline demote# #-} +{-# INLINE demote# #-} demote# (Fin# i) = i lift :: Unsafe.Fin# n -> Fin n -{-# inline lift #-} +{-# INLINE lift #-} lift (Unsafe.Fin# i) = Fin (Unsafe.Nat (I# i)) Unsafe.Lt unlift :: Fin n -> Unsafe.Fin# n -{-# inline unlift #-} +{-# INLINE unlift #-} unlift (Fin (Unsafe.Nat (I# i)) _) = Unsafe.Fin# i -- | Consume the natural number and the proof in the Fin. with :: Fin n -> (forall i. (i < n) -> Nat i -> a) -> a -{-# inline with #-} +{-# INLINE with #-} with (Fin i lt) f = f lt i -- | Variant of 'with' for unboxed argument and result types. with# :: Fin# n -> (forall i. (i <# n) -> Nat# i -> a) -> a -{-# inline with# #-} +{-# INLINE with# #-} with# (Unsafe.Fin# i) f = f (Unsafe.Lt# (# #)) (Unsafe.Nat# i) construct# :: (i <# n) -> Nat# i -> Fin# n -{-# inline construct# #-} +{-# INLINE construct# #-} construct# _ (Unsafe.Nat# x) = Unsafe.Fin# x --- | Return the successor of the Fin or return nothing if the --- argument is the greatest inhabitant. +{- | Return the successor of the Fin or return nothing if the +argument is the greatest inhabitant. +-} succ :: Nat n -> Fin n -> Maybe (Fin n) -{-# inline succ #-} +{-# INLINE succ #-} succ n (Fin ix _) = case ix' Nothing Just lt -> Just (Fin ix' lt) - where + where ix' = Nat.succ ix -- | Variant of 'succ' for unlifted finite numbers. succ# :: Nat# n -> Fin# n -> MaybeFin# n -{-# inline succ# #-} +{-# INLINE succ# #-} succ# (Nat# n) (Fin# ix) = case ix' Exts.<# n of 0# -> MaybeFinNothing# _ -> MaybeFinJust# (Fin# ix') - where + where !ix' = ix +# 1# --- | Convert an Int to a finite number, testing that it is --- less than the upper bound. This crashes with an uncatchable --- exception when given a negative number. +{- | Convert an Int to a finite number, testing that it is +less than the upper bound. This crashes with an uncatchable +exception when given a negative number. +-} fromInt :: - Nat n -- ^ exclusive upper bound - -> Int - -> Maybe (Fin n) -{-# inline fromInt #-} + -- | exclusive upper bound + Nat n -> + Int -> + Maybe (Fin n) +{-# INLINE fromInt #-} fromInt bound i | i < 0 = errorWithoutStackTrace "Arithmetic.Fin.fromInt: negative argument" | otherwise = Nat.with i $ \number -> case number Int# - -> MaybeFin# n -{-# inline fromInt# #-} + -- | exclusive upper bound + Nat# n -> + Int# -> + MaybeFin# n +{-# INLINE fromInt# #-} fromInt# (Nat# n) i | Exts.isTrue# (i Exts.<# 0#) = errorWithoutStackTrace "Arithmetic.Fin.fromInt#: negative argument" | Exts.isTrue# (i Exts.<# n) = MaybeFinJust# (Fin# i) | otherwise = MaybeFinNothing# --- | This crashes if @n = 0@. Divides @i@ by @n@ and takes --- the remainder. +{- | This crashes if @n = 0@. Divides @i@ by @n@ and takes +the remainder. +-} remInt# :: Int# -> Nat# n -> Fin# n remInt# i (Nat# n) = case n of 0# -> errorWithoutStackTrace "Arithmetic.Fin.remInt#: cannot divide by zero" _ -> Fin# (Exts.remInt# i n) --- | This crashes if @n = 0@. Divides @i@ by @n@ and takes --- the remainder. +{- | This crashes if @n = 0@. Divides @i@ by @n@ and takes +the remainder. +-} remWord# :: Word# -> Nat# n -> Fin# n remWord# w (Nat# n) = case n of 0# -> errorWithoutStackTrace "Arithmetic.Fin.remWord#: cannot divide by zero" diff --git a/src/Arithmetic/Lt.hs b/src/Arithmetic/Lt.hs index 1fee54e..a9c233e 100644 --- a/src/Arithmetic/Lt.hs +++ b/src/Arithmetic/Lt.hs @@ -1,29 +1,32 @@ -{-# language AllowAmbiguousTypes #-} -{-# language DataKinds #-} -{-# language ExplicitForAll #-} -{-# language KindSignatures #-} -{-# language MagicHash #-} -{-# language UnboxedTuples #-} -{-# language TypeFamilies #-} -{-# language TypeOperators #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} module Arithmetic.Lt ( -- * Special Inequalities zero , zero# + -- * Substitution , substituteL , substituteR + -- * Increment , incrementL , incrementL# , incrementR , incrementR# + -- * Decrement , decrementL , decrementL# , decrementR , decrementR# + -- * Weaken , weakenL , weakenL# @@ -31,6 +34,7 @@ module Arithmetic.Lt , weakenR# , weakenLhsL# , weakenLhsR# + -- * Composition , plus , plus# @@ -40,202 +44,247 @@ module Arithmetic.Lt , transitiveNonstrictL# , transitiveNonstrictR , transitiveNonstrictR# + -- * Multiplication and Division , reciprocalA , reciprocalB + -- * Convert to Inequality , toLteL , toLteR + -- * Absurdities , absurd + -- * Integration with GHC solver , constant , constant# + -- * Lift and Unlift , lift , unlift ) where -import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq)) -import Arithmetic.Unsafe (type (<=)(Lte)) -import Arithmetic.Unsafe (type (<#)(Lt#),type (<=#)) -import GHC.TypeNats (CmpNat,type (+)) +import Arithmetic.Unsafe (type (:=:) (Eq), type (<) (Lt), type (<#) (Lt#), type (<=) (Lte), type (<=#)) +import GHC.TypeNats (CmpNat, type (+)) import qualified GHC.TypeNats as GHC toLteR :: (a < b) -> (a + 1 <= b) -{-# inline toLteR #-} +{-# INLINE toLteR #-} toLteR Lt = Lte toLteL :: (a < b) -> (1 + a <= b) -{-# inline toLteL #-} +{-# INLINE toLteL #-} toLteL Lt = Lte --- | Replace the left-hand side of a strict inequality --- with an equal number. +{- | Replace the left-hand side of a strict inequality +with an equal number. +-} substituteL :: (b :=: c) -> (b < a) -> (c < a) -{-# inline substituteL #-} +{-# INLINE substituteL #-} substituteL Eq Lt = Lt --- | Replace the right-hand side of a strict inequality --- with an equal number. +{- | Replace the right-hand side of a strict inequality +with an equal number. +-} substituteR :: (b :=: c) -> (a < b) -> (a < c) -{-# inline substituteR #-} +{-# INLINE substituteR #-} substituteR Eq Lt = Lt -- | Add a strict inequality to a nonstrict inequality. plus :: (a < b) -> (c <= d) -> (a + c < b + d) -{-# inline plus #-} +{-# INLINE plus #-} plus Lt Lte = Lt plus# :: (a <# b) -> (c <=# d) -> (a + c <# b + d) -{-# inline plus# #-} +{-# INLINE plus# #-} plus# _ _ = Lt# (# #) --- | Add a constant to the left-hand side of both sides of --- the strict inequality. -incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a < b) -> (c + a < c + b) -{-# inline incrementL #-} +{- | Add a constant to the left-hand side of both sides of +the strict inequality. +-} +incrementL :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a < b) -> + (c + a < c + b) +{-# INLINE incrementL #-} incrementL Lt = Lt -incrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <# b) -> (c + a <# c + b) -{-# inline incrementL# #-} +incrementL# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <# b) -> + (c + a <# c + b) +{-# INLINE incrementL# #-} incrementL# _ = Lt# (# #) --- | Add a constant to the right-hand side of both sides of --- the strict inequality. -incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a < b) -> (a + c < b + c) -{-# inline incrementR #-} +{- | Add a constant to the right-hand side of both sides of +the strict inequality. +-} +incrementR :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a < b) -> + (a + c < b + c) +{-# INLINE incrementR #-} incrementR Lt = Lt -incrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <# b) -> (a + c <# b + c) -{-# inline incrementR# #-} +incrementR# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <# b) -> + (a + c <# b + c) +{-# INLINE incrementR# #-} incrementR# _ = Lt# (# #) --- | Subtract a constant from the left-hand side of both sides of --- the inequality. This is the opposite of 'incrementL'. -decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (c + a < c + b) -> (a < b) -{-# inline decrementL #-} +{- | Subtract a constant from the left-hand side of both sides of +the inequality. This is the opposite of 'incrementL'. +-} +decrementL :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (c + a < c + b) -> + (a < b) +{-# INLINE decrementL #-} decrementL Lt = Lt -decrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - ((c + a) <# (c + b)) -> (a <# b) -{-# inline decrementL# #-} +decrementL# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + ((c + a) <# (c + b)) -> + (a <# b) +{-# INLINE decrementL# #-} decrementL# _ = Lt# (# #) --- | Subtract a constant from the right-hand side of both sides of --- the inequality. This is the opposite of 'incrementR'. -decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a + c < b + c) -> (a < b) -{-# inline decrementR #-} +{- | Subtract a constant from the right-hand side of both sides of +the inequality. This is the opposite of 'incrementR'. +-} +decrementR :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a + c < b + c) -> + (a < b) +{-# INLINE decrementR #-} decrementR Lt = Lt -decrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a + c <# b + c) -> (a <# b) -{-# inline decrementR# #-} +decrementR# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a + c <# b + c) -> + (a <# b) +{-# INLINE decrementR# #-} decrementR# _ = Lt# (# #) --- | Add a constant to the left-hand side of the right-hand side of --- the strict inequality. -weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a < b) -> (a < c + b) -{-# inline weakenL #-} +{- | Add a constant to the left-hand side of the right-hand side of +the strict inequality. +-} +weakenL :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a < b) -> + (a < c + b) +{-# INLINE weakenL #-} weakenL Lt = Lt -weakenL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <# b) -> (a <# c + b) -{-# inline weakenL# #-} +weakenL# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <# b) -> + (a <# c + b) +{-# INLINE weakenL# #-} weakenL# _ = Lt# (# #) -weakenLhsL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (c + a <# b) -> (a <# b) -{-# inline weakenLhsL# #-} +weakenLhsL# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (c + a <# b) -> + (a <# b) +{-# INLINE weakenLhsL# #-} weakenLhsL# _ = Lt# (# #) -weakenLhsR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a + c <# b) -> (a <# b) -{-# inline weakenLhsR# #-} +weakenLhsR# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a + c <# b) -> + (a <# b) +{-# INLINE weakenLhsR# #-} weakenLhsR# _ = Lt# (# #) --- | Add a constant to the right-hand side of the right-hand side of --- the strict inequality. -weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a < b) -> (a < b + c) -{-# inline weakenR #-} +{- | Add a constant to the right-hand side of the right-hand side of +the strict inequality. +-} +weakenR :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a < b) -> + (a < b + c) +{-# INLINE weakenR #-} weakenR Lt = Lt -weakenR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <# b) -> (a <# b + c) -{-# inline weakenR# #-} +weakenR# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <# b) -> + (a <# b + c) +{-# INLINE weakenR# #-} weakenR# _ = Lt# (# #) -- | Compose two strict inequalities using transitivity. transitive :: (a < b) -> (b < c) -> (a < c) -{-# inline transitive #-} +{-# INLINE transitive #-} transitive Lt Lt = Lt transitive# :: (a <# b) -> (b <# c) -> (a <# c) -{-# inline transitive# #-} +{-# INLINE transitive# #-} transitive# _ _ = Lt# (# #) --- | Compose a strict inequality (the first argument) with a nonstrict --- inequality (the second argument). +{- | Compose a strict inequality (the first argument) with a nonstrict +inequality (the second argument). +-} transitiveNonstrictR :: (a < b) -> (b <= c) -> (a < c) -{-# inline transitiveNonstrictR #-} +{-# INLINE transitiveNonstrictR #-} transitiveNonstrictR Lt Lte = Lt transitiveNonstrictR# :: (a <# b) -> (b <=# c) -> (a <# c) -{-# inline transitiveNonstrictR# #-} +{-# INLINE transitiveNonstrictR# #-} transitiveNonstrictR# _ _ = Lt# (# #) transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c) -{-# inline transitiveNonstrictL #-} +{-# INLINE transitiveNonstrictL #-} transitiveNonstrictL Lte Lt = Lt transitiveNonstrictL# :: (a <=# b) -> (b <# c) -> (a <# c) -{-# inline transitiveNonstrictL# #-} +{-# INLINE transitiveNonstrictL# #-} transitiveNonstrictL# _ _ = Lt# (# #) -- | Zero is less than one. zero :: 0 < 1 -{-# inline zero #-} +{-# INLINE zero #-} zero = Lt zero# :: (# #) -> 0 <# 1 -{-# inline zero# #-} +{-# INLINE zero# #-} zero# _ = Lt# (# #) -- | Nothing is less than zero. absurd :: n < 0 -> void -{-# inline absurd #-} +{-# INLINE absurd #-} absurd Lt = errorWithoutStackTrace "Arithmetic.Nat.absurd: n < 0" --- | Use GHC's built-in type-level arithmetic to prove --- that one number is less than another. The type-checker --- only reduces 'CmpNat' if both arguments are constants. +{- | Use GHC's built-in type-level arithmetic to prove +that one number is less than another. The type-checker +only reduces 'CmpNat' if both arguments are constants. +-} constant :: forall a b. (CmpNat a b ~ 'LT) => (a < b) -{-# inline constant #-} +{-# INLINE constant #-} constant = Lt constant# :: forall a b. (CmpNat a b ~ 'LT) => (# #) -> (a <# b) -{-# inline constant# #-} +{-# INLINE constant# #-} constant# _ = Lt# (# #) -- | Given that @m < n/p@, we know that @p*m < n@. -reciprocalA :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat). - (m < GHC.Div n p) -> (p GHC.* m) < n -{-# inline reciprocalA #-} +reciprocalA :: + forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat). + (m < GHC.Div n p) -> + (p GHC.* m) < n +{-# INLINE reciprocalA #-} reciprocalA _ = Lt -- | Given that @m < roundUp(n/p)@, we know that @p*m < n@. -reciprocalB :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat). - (m < GHC.Div (n GHC.- 1) p + 1) -> (p GHC.* m) < n -{-# inline reciprocalB #-} +reciprocalB :: + forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat). + (m < GHC.Div (n GHC.- 1) p + 1) -> + (p GHC.* m) < n +{-# INLINE reciprocalB #-} reciprocalB _ = Lt unlift :: (a < b) -> (a <# b) diff --git a/src/Arithmetic/Lte.hs b/src/Arithmetic/Lte.hs index e49fea0..c8e00b8 100644 --- a/src/Arithmetic/Lte.hs +++ b/src/Arithmetic/Lte.hs @@ -1,198 +1,237 @@ -{-# language DataKinds #-} -{-# language ExplicitForAll #-} -{-# language KindSignatures #-} -{-# language MagicHash #-} -{-# language TypeFamilies #-} -{-# language TypeOperators #-} -{-# language UnboxedTuples #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} module Arithmetic.Lte ( -- * Special Inequalities zero , reflexive , reflexive# + -- * Substitution , substituteL , substituteR + -- * Increment , incrementL , incrementL# , incrementR , incrementR# + -- * Decrement , decrementL , decrementL# , decrementR , decrementR# + -- * Weaken , weakenL , weakenL# , weakenR , weakenR# + -- * Composition , transitive , transitive# , plus , plus# + -- * Convert Strict Inequality , fromStrict , fromStrict# , fromStrictSucc , fromStrictSucc# + -- * Integration with GHC solver , constant + -- * Lift and Unlift , lift , unlift ) where -import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq)) -import Arithmetic.Unsafe (type (<=)(Lte)) -import Arithmetic.Unsafe (type (<=#)(Lte#),type (<#)) -import GHC.TypeNats (CmpNat,type (+)) +import Arithmetic.Unsafe (type (:=:) (Eq), type (<) (Lt), type (<#), type (<=) (Lte), type (<=#) (Lte#)) +import GHC.TypeNats (CmpNat, type (+)) import qualified GHC.TypeNats as GHC --- | Replace the left-hand side of a strict inequality --- with an equal number. +{- | Replace the left-hand side of a strict inequality +with an equal number. +-} substituteL :: (b :=: c) -> (b <= a) -> (c <= a) -{-# inline substituteL #-} +{-# INLINE substituteL #-} substituteL Eq Lte = Lte --- | Replace the right-hand side of a strict inequality --- with an equal number. +{- | Replace the right-hand side of a strict inequality +with an equal number. +-} substituteR :: (b :=: c) -> (a <= b) -> (a <= c) -{-# inline substituteR #-} +{-# INLINE substituteR #-} substituteR Eq Lte = Lte -- | Add two inequalities. plus :: (a <= b) -> (c <= d) -> (a + c <= b + d) -{-# inline plus #-} +{-# INLINE plus #-} plus Lte Lte = Lte plus# :: (a <=# b) -> (c <=# d) -> (a + c <=# b + d) -{-# inline plus# #-} +{-# INLINE plus# #-} plus# _ _ = Lte# (# #) -- | Compose two inequalities using transitivity. transitive :: (a <= b) -> (b <= c) -> (a <= c) -{-# inline transitive #-} +{-# INLINE transitive #-} transitive Lte Lte = Lte transitive# :: (a <=# b) -> (b <=# c) -> (a <=# c) -{-# inline transitive# #-} +{-# INLINE transitive# #-} transitive# _ _ = Lte# (# #) -- | Any number is less-than-or-equal-to itself. reflexive :: a <= a -{-# inline reflexive #-} +{-# INLINE reflexive #-} reflexive = Lte reflexive# :: (# #) -> a <=# a -{-# inline reflexive# #-} +{-# INLINE reflexive# #-} reflexive# _ = Lte# (# #) --- | Add a constant to the left-hand side of both sides of --- the inequality. -incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <= b) -> (c + a <= c + b) -{-# inline incrementL #-} +{- | Add a constant to the left-hand side of both sides of +the inequality. +-} +incrementL :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <= b) -> + (c + a <= c + b) +{-# INLINE incrementL #-} incrementL Lte = Lte -incrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <=# b) -> (c + a <=# c + b) -{-# inline incrementL# #-} +incrementL# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <=# b) -> + (c + a <=# c + b) +{-# INLINE incrementL# #-} incrementL# _ = Lte# (# #) --- | Add a constant to the right-hand side of both sides of --- the inequality. -incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <= b) -> (a + c <= b + c) -{-# inline incrementR #-} +{- | Add a constant to the right-hand side of both sides of +the inequality. +-} +incrementR :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <= b) -> + (a + c <= b + c) +{-# INLINE incrementR #-} incrementR Lte = Lte -incrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <=# b) -> (a + c <=# b + c) -{-# inline incrementR# #-} +incrementR# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <=# b) -> + (a + c <=# b + c) +{-# INLINE incrementR# #-} incrementR# _ = Lte# (# #) --- | Add a constant to the left-hand side of the right-hand side of --- the inequality. -weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <= b) -> (a <= c + b) -{-# inline weakenL #-} +{- | Add a constant to the left-hand side of the right-hand side of +the inequality. +-} +weakenL :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <= b) -> + (a <= c + b) +{-# INLINE weakenL #-} weakenL Lte = Lte -weakenL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <=# b) -> (a <=# c + b) -{-# inline weakenL# #-} +weakenL# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <=# b) -> + (a <=# c + b) +{-# INLINE weakenL# #-} weakenL# _ = Lte# (# #) --- | Add a constant to the right-hand side of the right-hand side of --- the inequality. -weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <= b) -> (a <= b + c) -{-# inline weakenR #-} +{- | Add a constant to the right-hand side of the right-hand side of +the inequality. +-} +weakenR :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <= b) -> + (a <= b + c) +{-# INLINE weakenR #-} weakenR Lte = Lte -weakenR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a <=# b) -> (a <=# b + c) -{-# inline weakenR# #-} +weakenR# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <=# b) -> + (a <=# b + c) +{-# INLINE weakenR# #-} weakenR# _ = Lte# (# #) --- | Subtract a constant from the left-hand side of both sides of --- the inequality. This is the opposite of 'incrementL'. -decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (c + a <= c + b) -> (a <= b) -{-# inline decrementL #-} +{- | Subtract a constant from the left-hand side of both sides of +the inequality. This is the opposite of 'incrementL'. +-} +decrementL :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (c + a <= c + b) -> + (a <= b) +{-# INLINE decrementL #-} decrementL Lte = Lte -decrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (c + a <=# c + b) -> (a <=# b) -{-# inline decrementL# #-} +decrementL# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (c + a <=# c + b) -> + (a <=# b) +{-# INLINE decrementL# #-} decrementL# _ = Lte# (# #) --- | Subtract a constant from the right-hand side of both sides of --- the inequality. This is the opposite of 'incrementR'. -decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a + c <= b + c) -> (a <= b) -{-# inline decrementR #-} +{- | Subtract a constant from the right-hand side of both sides of +the inequality. This is the opposite of 'incrementR'. +-} +decrementR :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a + c <= b + c) -> + (a <= b) +{-# INLINE decrementR #-} decrementR Lte = Lte -decrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). - (a + c <=# b + c) -> (a <=# b) -{-# inline decrementR# #-} +decrementR# :: + forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a + c <=# b + c) -> + (a <=# b) +{-# INLINE decrementR# #-} decrementR# _ = Lte# (# #) -- | Weaken a strict inequality to a non-strict inequality. fromStrict :: (a < b) -> (a <= b) -{-# inline fromStrict #-} +{-# INLINE fromStrict #-} fromStrict Lt = Lte fromStrict# :: (a <# b) -> (a <=# b) -{-# inline fromStrict# #-} +{-# INLINE fromStrict# #-} fromStrict# _ = Lte# (# #) --- | Weaken a strict inequality to a non-strict inequality, incrementing --- the right-hand argument by one. +{- | Weaken a strict inequality to a non-strict inequality, incrementing +the right-hand argument by one. +-} fromStrictSucc :: (a < b) -> (a + 1 <= b) -{-# inline fromStrictSucc #-} +{-# INLINE fromStrictSucc #-} fromStrictSucc Lt = Lte fromStrictSucc# :: (a <# b) -> (a + 1 <=# b) -{-# inline fromStrictSucc# #-} +{-# INLINE fromStrictSucc# #-} fromStrictSucc# _ = Lte# (# #) -- | Zero is less-than-or-equal-to any number. zero :: 0 <= a -{-# inline zero #-} +{-# INLINE zero #-} zero = Lte --- | Use GHC's built-in type-level arithmetic to prove --- that one number is less-than-or-equal-to another. The type-checker --- only reduces 'CmpNat' if both arguments are constants. +{- | Use GHC's built-in type-level arithmetic to prove +that one number is less-than-or-equal-to another. The type-checker +only reduces 'CmpNat' if both arguments are constants. +-} constant :: forall a b. (IsLte (CmpNat a b) ~ 'True) => (a <= b) -{-# inline constant #-} +{-# INLINE constant #-} constant = Lte type family IsLte (o :: Ordering) :: Bool where diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs index 05e48e4..5441a36 100644 --- a/src/Arithmetic/Nat.hs +++ b/src/Arithmetic/Nat.hs @@ -1,28 +1,31 @@ -{-# language DataKinds #-} -{-# language ExplicitForAll #-} -{-# language KindSignatures #-} -{-# language MagicHash #-} -{-# language PatternSynonyms #-} -{-# language RankNTypes #-} -{-# language ScopedTypeVariables #-} -{-# language TypeOperators #-} -{-# language UnboxedTuples #-} -{-# language UnboxedSums #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} module Arithmetic.Nat ( -- * Addition plus , plus# + -- * Subtraction , monus + -- * Division , divide , divideRoundingUp + -- * Multiplication , times + -- * Successor , succ , succ# + -- * Compare , testEqual , testEqual# @@ -35,6 +38,7 @@ module Arithmetic.Nat , ( Nat b -> Maybe (a < b) -{-# inline ( Nat b -> Maybe (a <= b) -{-# inline (<=?) #-} +{-# INLINE (<=?) #-} (<=?) = testLessThanEqual -- | Infix synonym of 'testEqual'. (=?) :: Nat a -> Nat b -> Maybe (a :=: b) -{-# inline (=?) #-} +{-# INLINE (=?) #-} (=?) = testEqual ( Nat# b -> MaybeVoid# (a <# b) -{-# inline ( Nat b -> Maybe (a < b) -{-# inline testLessThan #-} -testLessThan (Nat x) (Nat y) = if x < y - then Just Lt - else Nothing +{-# INLINE testLessThan #-} +testLessThan (Nat x) (Nat y) = + if x < y + then Just Lt + else Nothing testLessThan# :: Nat# a -> Nat# b -> MaybeVoid# (a <# b) -{-# inline testLessThan# #-} +{-# INLINE testLessThan# #-} testLessThan# (Nat# x) (Nat# y) = case x <# y of 0# -> NothingVoid# _ -> JustVoid# (Lt# (# #)) --- | Is the first argument less-than-or-equal-to the second --- argument? +{- | Is the first argument less-than-or-equal-to the second +argument? +-} testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b) -{-# inline testLessThanEqual #-} -testLessThanEqual (Nat x) (Nat y) = if x <= y - then Just Lte - else Nothing +{-# INLINE testLessThanEqual #-} +testLessThanEqual (Nat x) (Nat y) = + if x <= y + then Just Lte + else Nothing -- | Are the two arguments equal to one another? testEqual :: Nat a -> Nat b -> Maybe (a :=: b) -{-# inline testEqual #-} -testEqual (Nat x) (Nat y) = if x == y - then Just Eq - else Nothing +{-# INLINE testEqual #-} +testEqual (Nat x) (Nat y) = + if x == y + then Just Eq + else Nothing testEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a :=:# b) -{-# inline testEqual# #-} +{-# INLINE testEqual# #-} testEqual# (Nat# x) (Nat# y) = case x ==# y of 0# -> NothingVoid# _ -> JustVoid# (Eq# (# #)) -- | Is zero equal to this number or less than it? testZero :: Nat a -> Either (0 :=: a) (0 < a) -{-# inline testZero #-} +{-# INLINE testZero #-} testZero (Nat x) = case x of 0 -> Left Eq _ -> Right Lt @@ -154,22 +165,22 @@ testZero# (Nat# x) = case x of -- | Add two numbers. plus :: Nat a -> Nat b -> Nat (a + b) -{-# inline plus #-} +{-# INLINE plus #-} plus (Nat x) (Nat y) = Nat (x + y) -- | Variant of 'plus' for unboxed nats. plus# :: Nat# a -> Nat# b -> Nat# (a + b) -{-# inline plus# #-} +{-# INLINE plus# #-} plus# (Nat# x) (Nat# y) = Nat# (x +# y) -- | Divide two numbers. Rounds down (towards zero) divide :: Nat a -> Nat b -> Nat (Div a b) -{-# inline divide #-} +{-# INLINE divide #-} divide (Nat x) (Nat y) = Nat (div x y) -- | Divide two numbers. Rounds up (away from zero) divideRoundingUp :: Nat a -> Nat b -> Nat (Div (a - 1) b + 1) -{-# inline divideRoundingUp #-} +{-# INLINE divideRoundingUp #-} divideRoundingUp (Nat x) (Nat y) = -- Implementation note. We must use div so that when x=0, -- the result is (-1) and not 0. Then when we add 1, we get 0. @@ -177,55 +188,58 @@ divideRoundingUp (Nat x) (Nat y) = -- | Multiply two numbers. times :: Nat a -> Nat b -> Nat (a GHC.* b) -{-# inline times #-} +{-# INLINE times #-} times (Nat x) (Nat y) = Nat (x * y) -- | The successor of a number. succ :: Nat a -> Nat (a + 1) -{-# inline succ #-} +{-# INLINE succ #-} succ n = plus n one -- | Unlifted variant of 'succ'. succ# :: Nat# a -> Nat# (a + 1) -{-# inline succ# #-} +{-# INLINE succ# #-} succ# n = plus# n (one# (# #)) -- | Subtract the second argument from the first argument. monus :: Nat a -> Nat b -> Maybe (Difference a b) -{-# inline monus #-} -monus (Nat a) (Nat b) = let c = a - b in if c >= 0 - then Just (Difference (Nat c) Eq) - else Nothing +{-# INLINE monus #-} +monus (Nat a) (Nat b) = + let c = a - b + in if c >= 0 + then Just (Difference (Nat c) Eq) + else Nothing -- | The number zero. zero :: Nat 0 -{-# inline zero #-} +{-# INLINE zero #-} zero = Nat 0 -- | The number one. one :: Nat 1 -{-# inline one #-} +{-# INLINE one #-} one = Nat 1 -- | The number two. two :: Nat 2 -{-# inline two #-} +{-# INLINE two #-} two = Nat 2 -- | The number three. three :: Nat 3 -{-# inline three #-} +{-# INLINE three #-} three = Nat 3 --- | Use GHC's built-in type-level arithmetic to create a witness --- of a type-level number. This only reduces if the number is a --- constant. -constant :: forall n. KnownNat n => Nat n -{-# inline constant #-} +{- | Use GHC's built-in type-level arithmetic to create a witness +of a type-level number. This only reduces if the number is a +constant. +-} +constant :: forall n. (KnownNat n) => Nat n +{-# INLINE constant #-} constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n))) -constant# :: forall n. KnownNat n => (# #) -> Nat# n -{-# inline constant# #-} +constant# :: forall n. (KnownNat n) => (# #) -> Nat# n +{-# INLINE constant# #-} constant# _ = case fromIntegral (natVal' (proxy# :: Proxy# n)) of I# i -> Nat# i @@ -237,35 +251,37 @@ zero# _ = Nat# 0# one# :: (# #) -> Nat# 1 one# _ = Nat# 1# --- | Extract the 'Int' from a 'Nat'. This is intended to be used --- at a boundary where a safe interface meets the unsafe primitives --- on top of which it is built. +{- | Extract the 'Int' from a 'Nat'. This is intended to be used +at a boundary where a safe interface meets the unsafe primitives +on top of which it is built. +-} demote :: Nat n -> Int -{-# inline demote #-} +{-# INLINE demote #-} demote (Nat n) = n demote# :: Nat# n -> Int# -{-# inline demote# #-} +{-# INLINE demote# #-} demote# (Nat# n) = n --- | Run a computation on a witness of a type-level number. The --- argument 'Int' must be greater than or equal to zero. This is --- not checked. Failure to upload this invariant will lead to a --- segfault. +{- | Run a computation on a witness of a type-level number. The +argument 'Int' must be greater than or equal to zero. This is +not checked. Failure to upload this invariant will lead to a +segfault. +-} with :: Int -> (forall n. Nat n -> a) -> a -{-# inline with #-} +{-# INLINE with #-} with i f = f (Nat i) with# :: Int# -> (forall n. Nat# n -> a) -> a -{-# inline with# #-} +{-# INLINE with# #-} with# i f = f (Nat# i) unlift :: Nat n -> Nat# n -{-# inline unlift #-} +{-# INLINE unlift #-} unlift (Nat (I# i)) = Nat# i lift :: Nat# n -> Nat n -{-# inline lift #-} +{-# INLINE lift #-} lift (Nat# i) = Nat (I# i) pattern N0# :: Nat# 0 diff --git a/src/Arithmetic/Plus.hs b/src/Arithmetic/Plus.hs index 2454723..e948412 100644 --- a/src/Arithmetic/Plus.hs +++ b/src/Arithmetic/Plus.hs @@ -1,8 +1,8 @@ -{-# language DataKinds #-} -{-# language TypeOperators #-} -{-# language KindSignatures #-} -{-# language ExplicitForAll #-} -{-# language AllowAmbiguousTypes #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} module Arithmetic.Plus ( zeroL @@ -11,7 +11,7 @@ module Arithmetic.Plus , associative ) where -import Arithmetic.Unsafe (type (:=:)(Eq)) +import Arithmetic.Unsafe (type (:=:) (Eq)) import GHC.TypeNats (type (+)) -- | Any number plus zero is equal to the original number. diff --git a/src/Arithmetic/Types.hs b/src/Arithmetic/Types.hs index f0902fc..329c43b 100644 --- a/src/Arithmetic/Types.hs +++ b/src/Arithmetic/Types.hs @@ -1,27 +1,27 @@ -{-# language DataKinds #-} -{-# language MagicHash #-} -{-# language ExplicitNamespaces #-} -{-# language PatternSynonyms #-} -{-# language ViewPatterns #-} -{-# language GADTs #-} -{-# language KindSignatures #-} -{-# language RankNTypes #-} -{-# language TypeOperators #-} -{-# language UnboxedTuples #-} -{-# language UnboxedSums #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE ViewPatterns #-} module Arithmetic.Types ( Nat , Nat# - , WithNat(..) - , Difference(..) - , Fin(..) + , WithNat (..) + , Difference (..) + , Fin (..) , Fin# , Fin32# + -- * Maybe Fin , MaybeFin# , pattern MaybeFinJust# , pattern MaybeFinNothing# + -- * Infix Operators , type (<) , type (<=) @@ -31,11 +31,7 @@ module Arithmetic.Types , type (:=:#) ) where -import Arithmetic.Unsafe (Fin#(Fin#),Nat#,Nat(getNat), type (<=)) -import Arithmetic.Unsafe (Fin32#) -import Arithmetic.Unsafe (MaybeFin#(..)) -import Arithmetic.Unsafe (type (<), type (:=:)) -import Arithmetic.Unsafe (type (<#), type (<=#), (:=:#)) +import Arithmetic.Unsafe (Fin# (Fin#), Fin32#, MaybeFin# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), type (<=), type (<=#)) import Data.Kind (type Type) import GHC.TypeNats (type (+)) @@ -43,19 +39,22 @@ import qualified GHC.TypeNats as GHC data WithNat :: (GHC.Nat -> Type) -> Type where WithNat :: - {-# UNPACK #-} !(Nat n) - -> f n - -> WithNat f + {-# UNPACK #-} !(Nat n) -> + f n -> + WithNat f -- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }' data Fin :: GHC.Nat -> Type where - Fin :: forall m n. + Fin :: + forall m n. { index :: !(Nat m) , proof :: !(m < n) - } -> Fin n + } -> + Fin n --- | Proof that the first argument can be expressed as the --- sum of the second argument and some other natural number. +{- | Proof that the first argument can be expressed as the +sum of the second argument and some other natural number. +-} data Difference :: GHC.Nat -> GHC.Nat -> Type where -- It is safe for users of this library to use this data constructor -- freely. However, note that the interesting Difference values come @@ -72,14 +71,15 @@ instance Ord (Fin n) where Fin x _ `compare` Fin y _ = compare (getNat x) (getNat y) pattern MaybeFinJust# :: Fin# n -> MaybeFin# n -pattern MaybeFinJust# f <- (maybeFinToFin# -> (# | f #)) where - MaybeFinJust# (Fin# i) = MaybeFin# i +pattern MaybeFinJust# f <- (maybeFinToFin# -> (# | f #)) + where + MaybeFinJust# (Fin# i) = MaybeFin# i pattern MaybeFinNothing# :: MaybeFin# n pattern MaybeFinNothing# = MaybeFin# (-1#) maybeFinToFin# :: MaybeFin# n -> (# (# #) | Fin# n #) -{-# inline maybeFinToFin# #-} +{-# INLINE maybeFinToFin# #-} maybeFinToFin# (MaybeFin# i) = case i of -1# -> (# (# #) | #) _ -> (# | Fin# i #) diff --git a/src/Arithmetic/Unsafe.hs b/src/Arithmetic/Unsafe.hs index 61db44d..e141099 100644 --- a/src/Arithmetic/Unsafe.hs +++ b/src/Arithmetic/Unsafe.hs @@ -1,35 +1,34 @@ -{-# language DataKinds #-} -{-# language DerivingStrategies #-} -{-# language ExplicitNamespaces #-} -{-# language GADTSyntax #-} -{-# language GeneralizedNewtypeDeriving #-} -{-# language KindSignatures #-} -{-# language MagicHash #-} -{-# language RoleAnnotations #-} -{-# language StandaloneDeriving #-} -{-# language TypeOperators #-} -{-# language UnboxedTuples #-} -{-# language UnliftedNewtypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE UnliftedNewtypes #-} module Arithmetic.Unsafe - ( Nat(..) - , Nat#(..) - , Fin#(..) - , MaybeFin#(..) - , Fin32#(..) - , type (<#)(Lt#) - , type (<=#)(Lte#) - , type (<)(Lt) - , type (<=)(Lte) - , type (:=:)(Eq) - , type (:=:#)(Eq#) + ( Nat (..) + , Nat# (..) + , Fin# (..) + , MaybeFin# (..) + , Fin32# (..) + , type (<#) (Lt#) + , type (<=#) (Lte#) + , type (<) (Lt) + , type (<=) (Lte) + , type (:=:) (Eq) + , type (:=:#) (Eq#) ) where -import Prelude hiding ((>=),(<=)) +import Prelude hiding ((<=), (>=)) import Control.Category (Category) import Data.Kind (Type) -import GHC.Exts (Int#,Int32#,TYPE,RuntimeRep(IntRep,Int32Rep,TupleRep)) +import GHC.Exts (Int#, Int32#, RuntimeRep (Int32Rep, IntRep, TupleRep), TYPE) import qualified Control.Category import qualified GHC.TypeNats as GHC @@ -48,7 +47,8 @@ infix 4 :=: infix 4 :=:# -- | A value-level representation of a natural number @n@. -newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int } +newtype Nat (n :: GHC.Nat) = Nat {getNat :: Int} + type role Nat nominal deriving newtype instance Show (Nat n) @@ -56,34 +56,41 @@ deriving newtype instance Show (Nat n) -- | Unboxed variant of Nat. newtype Nat# :: GHC.Nat -> TYPE 'IntRep where Nat# :: Int# -> Nat# n + type role Nat# nominal -- | Finite numbers without the overhead of carrying around a proof. newtype Fin# :: GHC.Nat -> TYPE 'IntRep where Fin# :: Int# -> Fin# n + type role Fin# nominal --- | Either a @Fin#@ or Nothing. Internally, this uses negative --- one to mean Nothing. +{- | Either a @Fin#@ or Nothing. Internally, this uses negative +one to mean Nothing. +-} newtype MaybeFin# :: GHC.Nat -> TYPE 'IntRep where MaybeFin# :: Int# -> MaybeFin# n + type role MaybeFin# nominal -- | Variant of 'Fin#' that only allows 32-bit integers. newtype Fin32# :: GHC.Nat -> TYPE 'Int32Rep where Fin32# :: Int32# -> Fin32# n + type role Fin32# nominal --- | Proof that the first argument is strictly less than the --- second argument. +{- | Proof that the first argument is strictly less than the +second argument. +-} data (<) :: GHC.Nat -> GHC.Nat -> Type where Lt :: a < b newtype (<#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where Lt# :: (# #) -> a <# b --- | Proof that the first argument is less than or equal to the --- second argument. +{- | Proof that the first argument is less than or equal to the +second argument. +-} data (<=) :: GHC.Nat -> GHC.Nat -> Type where Lte :: a <= b