diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for debruijn + +## 0.1.0.0 -- 2025-06-08 + +- First version. diff --git a/data-debruijn.cabal b/data-debruijn.cabal new file mode 100644 --- /dev/null +++ b/data-debruijn.cabal @@ -0,0 +1,191 @@ +cabal-version: 3.4 +name: data-debruijn +version: 0.1.0.0 +synopsis: Fast and safe implementation of common compiler machinery. +description: + This package provides a safe interface to optimised implementations of common + machinery used in compilers and type checkers. + + [Type-Level Naturals]: + "Data.Type.Nat" + + "Data.Type.Nat.Singleton" + + [DeBruijn Indexes] + "Data.DeBruijn.Index" + + [Thinnings] + "Data.DeBruijn.Thinning" + + [Environments] + "Data.DeBruijn.Environment" + +license: AGPL-3.0-only +author: Wen Kokke +maintainer: wenkokke@users.noreply.github.com +copyright: + 2023-2025 (c) Wen Kokke + 2025 (c) April Gonçalves + 2025 (c) Well-Typed LLC + +category: Development +build-type: Simple +extra-doc-files: CHANGELOG.md +tested-with: GHC ==9.6.7 || ==9.8.4 || ==9.10.2 || ==9.12.2 + +source-repository head + type: git + location: https://github.com/wenkokke/data-debruijn + +source-repository this + type: git + location: https://github.com/wenkokke/data-debruijn + tag: v0.1.0.0 + +-------------------------------------------------------------------------------- +-- Feature Flags for Underlying Representation +-------------------------------------------------------------------------------- + +-- Representation: Use safe inductive definitions for all types. +flag safe + description: Export the safe API. + manual: True + default: False + +flag th-as-word64 + description: + Use a Word to represent thinnings. + The default is Natural. + + manual: True + default: False + +-- Representation: Environments +flag env-as-skew-list + description: + Use SkewList from the skew-list package to represent environments. + The default is Seq from the containers package. + + manual: True + default: False + +common language + ghc-options: + -Wall -Wcompat -Widentities -Wprepositive-qualified-module + -Wredundant-constraints -Wunticked-promoted-constructors + -Wunused-packages + + default-language: GHC2021 + default-extensions: + ImportQualifiedPost + NoFieldSelectors + +library + import: language + hs-source-dirs: src + default-extensions: NoImplicitPrelude + build-depends: data-debruijn:typenats + reexported-modules: Data.Type.Nat + exposed-modules: + Data.DeBruijn.Environment + Data.DeBruijn.Index + Data.DeBruijn.Thinning + Data.Type.Nat.Singleton + + if flag(safe) + build-depends: data-debruijn:safe + cpp-options: -DEXPORT_SAFE_API + + else + build-depends: data-debruijn:fast + + -- NOTE: GHC does not detect that the package "data-debruijn:typenats" + -- is used by the "reexported-modules" declaration. + ghc-options: -Wno-unused-packages + +library typenats + import: language + visibility: public + hs-source-dirs: src-typenats + exposed-modules: Data.Type.Nat + build-depends: base >=4.17 && <5 + +library fast + import: language + visibility: public + hs-source-dirs: src-fast + exposed-modules: + Data.DeBruijn.Environment.Fast + Data.DeBruijn.Index.Fast + Data.DeBruijn.Thinning.Fast + Data.Type.Nat.Singleton.Fast + + build-depends: + , base >=4.17 && <5 + , data-debruijn:typenats + , deepseq ^>=1.4 || ^>=1.5 + + -- Representation: Natural Number Singletons + cpp-options: -DSNAT_AS_INT + + -- Representation: Indexes + cpp-options: -DIX_AS_INT + + -- Representation: Thinnings + if flag(th-as-word64) + cpp-options: -DTH_AS_WORD64 + build-depends: ghc-prim ^>=0.9 || ^>=0.10 || ^>=0.11 || ^>=0.12 || ^>=0.13 + + else + cpp-options: -DTH_AS_NATURAL + build-depends: + , ghc-bignum ^>=1.3 + , ghc-prim ^>=0.9 || ^>=0.10 || ^>=0.11 || ^>=0.12 || ^>=0.13 + + -- Representation: Environments + if flag(env-as-skew-list) + cpp-options: -DENV_AS_SKEW_LIST + build-depends: skew-list ^>=0.1 + + else + cpp-options: -DENV_AS_SEQ + build-depends: containers >=0.6.7 && <0.9 + +library safe + import: language + visibility: public + hs-source-dirs: src-safe + exposed-modules: + Data.DeBruijn.Environment.Safe + Data.DeBruijn.Index.Safe + Data.DeBruijn.Thinning.Safe + Data.Type.Nat.Singleton.Safe + + build-depends: + , base >=4.17 && <5 + , data-debruijn:fast + , data-debruijn:typenats + , deepseq ^>=1.4 || ^>=1.5 + +library arbitrary + import: language + visibility: public + hs-source-dirs: src-arbitrary + other-modules: Test.QuickCheck.Extra + exposed-modules: + Data.DeBruijn.Index.Arbitrary + Data.DeBruijn.Index.Fast.Arbitrary + Data.DeBruijn.Index.Safe.Arbitrary + Data.DeBruijn.Thinning.Arbitrary + Data.DeBruijn.Thinning.Fast.Arbitrary + Data.DeBruijn.Thinning.Safe.Arbitrary + Data.Type.Nat.Singleton.Arbitrary + Data.Type.Nat.Singleton.Fast.Arbitrary + Data.Type.Nat.Singleton.Safe.Arbitrary + + build-depends: + , base + , data-debruijn:fast + , data-debruijn:safe + , data-debruijn:typenats + , QuickCheck >=2.9 && <3.0 diff --git a/src-arbitrary/Data/DeBruijn/Index/Arbitrary.hs b/src-arbitrary/Data/DeBruijn/Index/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Data/DeBruijn/Index/Arbitrary.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE DerivingStrategies #-} + +module Data.DeBruijn.Index.Arbitrary ( + SomeIxRep (..), +) where + +import Data.DeBruijn.Index.Fast (IxRep, snatRepToIxRep) +import Data.Type.Nat.Singleton.Fast (SNatRep) +import Test.QuickCheck.Arbitrary (Arbitrary (..)) +import Test.QuickCheck.Extra (chooseSizedBoundedIntegral) +import Test.QuickCheck.Gen (Gen) +import Test.QuickCheck.Modifiers (Positive (..)) + +data SomeIxRep = SomeIxRep !SNatRep !IxRep + deriving stock (Eq, Show) + +instance Arbitrary SomeIxRep where + arbitrary :: Gen SomeIxRep + arbitrary = do + nRep <- getPositive <$> arbitrary + iRep <- chooseSizedBoundedIntegral (0, snatRepToIxRep (nRep - 1)) + pure $ SomeIxRep nRep iRep diff --git a/src-arbitrary/Data/DeBruijn/Index/Fast/Arbitrary.hs b/src-arbitrary/Data/DeBruijn/Index/Fast/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Data/DeBruijn/Index/Fast/Arbitrary.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Data.DeBruijn.Index.Fast.Arbitrary ( + arbitraryIx, +) where + +import Data.DeBruijn.Index.Arbitrary (SomeIxRep (..)) +import Data.DeBruijn.Index.Fast (Ix (..), SomeIx (..), toSomeIxRaw) +import Data.Type.Nat (Nat (..)) +import Data.Type.Nat.Singleton.Fast (SNat (..)) +import Data.Type.Nat.Singleton.Fast.Arbitrary () +import Test.QuickCheck.Arbitrary (Arbitrary (..)) +import Test.QuickCheck.Gen (Gen, oneof) + +instance Arbitrary SomeIx where + arbitrary :: Gen SomeIx + arbitrary = do + SomeIxRep n i <- arbitrary + pure $ toSomeIxRaw (n, i) + +instance Arbitrary (Ix (S Z)) where + arbitrary :: Gen (Ix (S Z)) + arbitrary = pure FZ + +instance (forall m. Arbitrary (Ix (S m))) => Arbitrary (Ix (S (S n))) where + arbitrary :: Gen (Ix (S (S n))) + arbitrary = oneof [pure FZ, FS <$> arbitrary] + +arbitraryIx :: SNat (S n) -> Gen (Ix (S n)) +arbitraryIx (S Z) = pure FZ +arbitraryIx (S n@(S _)) = oneof [pure FZ, FS <$> arbitraryIx n] diff --git a/src-arbitrary/Data/DeBruijn/Index/Safe/Arbitrary.hs b/src-arbitrary/Data/DeBruijn/Index/Safe/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Data/DeBruijn/Index/Safe/Arbitrary.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Data.DeBruijn.Index.Safe.Arbitrary ( + arbitraryIx, +) where + +import Data.DeBruijn.Index.Arbitrary (SomeIxRep (..)) +import Data.DeBruijn.Index.Safe (Ix (..), SomeIx (..), toSomeIxRaw) +import Data.Type.Nat (Nat (..)) +import Data.Type.Nat.Singleton.Safe (SNat (..)) +import Test.QuickCheck.Arbitrary (Arbitrary (..)) +import Test.QuickCheck.Gen (Gen, oneof) + +instance Arbitrary SomeIx where + arbitrary :: Gen SomeIx + arbitrary = do + SomeIxRep n i <- arbitrary + pure $ toSomeIxRaw (n, i) + +instance Arbitrary (Ix (S Z)) where + arbitrary :: Gen (Ix (S Z)) + arbitrary = pure FZ + +instance (forall m. Arbitrary (Ix (S m))) => Arbitrary (Ix (S (S n))) where + arbitrary :: Gen (Ix (S (S n))) + arbitrary = oneof [pure FZ, FS <$> arbitrary] + +arbitraryIx :: SNat (S n) -> Gen (Ix (S n)) +arbitraryIx (S Z) = pure FZ +arbitraryIx (S n@(S _)) = oneof [pure FZ, FS <$> arbitraryIx n] diff --git a/src-arbitrary/Data/DeBruijn/Thinning/Arbitrary.hs b/src-arbitrary/Data/DeBruijn/Thinning/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Data/DeBruijn/Thinning/Arbitrary.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingStrategies #-} + +module Data.DeBruijn.Thinning.Arbitrary ( + SomeThRep (..), + SomeThBoundRep (..), + getSomeThBoundRep, +) where + +import Control.Exception (assert) +import Data.Bits (Bits (..)) +import Data.DeBruijn.Thinning.Fast (ThRep, bitsToThRep, thRepToBits) +import Data.Type.Nat.Singleton.Fast (SNatRep, intToSNatRep) +import Test.QuickCheck.Arbitrary (Arbitrary (..)) +import Test.QuickCheck.Extra (chooseSizedBoundedIntegral, chooseSizesBoundedPositiveIntegral) +import Test.QuickCheck.Gen (Gen, chooseInteger) +import Test.QuickCheck.Modifiers (NonNegative (..), Positive (..)) +import Text.Printf (printf) + +data SomeThRep = SomeThRep !SNatRep !ThRep + deriving stock (Eq) + +instance Show SomeThRep where + showsPrec :: Int -> SomeThRep -> ShowS + showsPrec p (SomeThRep nRep nmRep) = + let mRep = nRep + intToSNatRep (popCount nmRep) + in showParen (p > 10) . showString $ + printf ("SomeThRep %d 0b%0" <> show mRep <> "b") nRep (thRepToBits @Integer nmRep) + +instance Arbitrary SomeThRep where + arbitrary :: Gen SomeThRep + arbitrary = do + mRep <- maybe (getPositive <$> arbitrary) chooseSizesBoundedPositiveIntegral (bitSizeMaybe (undefined :: ThRep)) + nmRep <- bitsToThRep <$> chooseInteger (0, 2 ^ mRep - 1) + let nRep = mRep - intToSNatRep (popCount nmRep) + assert (nRep >= 0) $ pure () + pure $ SomeThRep nRep nmRep + +-------------------------------------------------------------------------------- +-- QuickCheck instances for SomeThBoundRep + +newtype SomeThBoundRep = SomeThBoundRep SNatRep + deriving stock (Eq, Show) + +getSomeThBoundRep :: SomeThBoundRep -> SNatRep +getSomeThBoundRep (SomeThBoundRep nRep) = nRep + +instance Arbitrary SomeThBoundRep where + arbitrary :: Gen SomeThBoundRep + arbitrary = case bitSizeMaybe (undefined :: ThRep) of + Nothing -> SomeThBoundRep . getNonNegative <$> arbitrary + Just thSize -> SomeThBoundRep <$> chooseSizedBoundedIntegral (0, thSize) + + shrink :: SomeThBoundRep -> [SomeThBoundRep] + shrink (SomeThBoundRep nRep) = SomeThBoundRep <$> shrink nRep diff --git a/src-arbitrary/Data/DeBruijn/Thinning/Fast/Arbitrary.hs b/src-arbitrary/Data/DeBruijn/Thinning/Fast/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Data/DeBruijn/Thinning/Fast/Arbitrary.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Data.DeBruijn.Thinning.Fast.Arbitrary ( + arbitraryTh, +) where + +import Data.DeBruijn.Thinning.Arbitrary (SomeThRep (..)) +import Data.DeBruijn.Thinning.Fast (SomeTh (..), dropAll, toSomeThRaw, type (:<=) (DropOne, KeepAll, KeepOne)) +import Data.Proxy (Proxy (..)) +import Data.Type.Equality (type (:~:) (Refl)) +import Data.Type.Nat (type (+)) +import Data.Type.Nat.Singleton.Fast (SNat (..), plusCommS, plusUnitR) +import Data.Type.Nat.Singleton.Fast.Arbitrary () +import Test.QuickCheck.Arbitrary (Arbitrary (..)) +import Test.QuickCheck.Gen (Gen, oneof) + +instance Arbitrary SomeTh where + arbitrary :: Gen SomeTh + arbitrary = do + SomeThRep n nm <- arbitrary + pure $ toSomeThRaw (n, nm) + +arbitraryTh :: SNat n -> SNat m -> Gen (n :<= (n + m)) +arbitraryTh n Z = case plusUnitR n of Refl -> pure KeepAll +arbitraryTh Z m = pure (dropAll m) +arbitraryTh n@(S n') m@(S m') = oneof [keepOne, dropOne] + where + keepOne = KeepOne <$> arbitraryTh n' m + dropOne = case plusCommS n' (erase m') of Refl -> DropOne <$> arbitraryTh n m' + +-------------------------------------------------------------------------------- +-- Helper Functions +-------------------------------------------------------------------------------- + +-- | @`erase` x@ erases the content of @x@ to a @`Proxy`@. +erase :: f a -> Proxy a +erase _ = Proxy +{-# INLINE erase #-} diff --git a/src-arbitrary/Data/DeBruijn/Thinning/Safe/Arbitrary.hs b/src-arbitrary/Data/DeBruijn/Thinning/Safe/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Data/DeBruijn/Thinning/Safe/Arbitrary.hs @@ -0,0 +1,117 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Data.DeBruijn.Thinning.Safe.Arbitrary ( + arbitraryTh, + SomeThinIxArgs (..), + SomeThickIxArgs (..), + SomeThinThArgs (..), +) where + +import Data.DeBruijn.Index.Safe (Ix) +import Data.DeBruijn.Index.Safe.Arbitrary (arbitraryIx) +import Data.DeBruijn.Thinning.Arbitrary (SomeThBoundRep (..), SomeThRep (..)) +import Data.DeBruijn.Thinning.Safe (SomeTh (..), dropAll, toSomeThRaw, type (:<=) (DropOne, KeepAll, KeepOne)) +import Data.Proxy (Proxy (..)) +import Data.Type.Equality (type (:~:) (Refl)) +import Data.Type.Nat (type (+)) +import Data.Type.Nat.Singleton.Safe (SNat (..), SomeSNat (..), plusCommS, plusUnitR, toSomeSNatRaw) +import Data.Type.Nat.Singleton.Safe qualified as Safe +import Data.Type.Nat.Singleton.Safe.Arbitrary () +import Test.QuickCheck.Arbitrary (Arbitrary (..)) +import Test.QuickCheck.Extra (chooseSizedBoundedIntegral) +import Test.QuickCheck.Gen (Gen, oneof) + +instance Arbitrary SomeTh where + arbitrary :: Gen SomeTh + arbitrary = do + SomeThRep n nm <- arbitrary + pure $ toSomeThRaw (n, nm) + +arbitraryTh :: SNat n -> SNat d -> Gen (n :<= (n + d)) +arbitraryTh n Z = case plusUnitR n of Refl -> pure KeepAll +arbitraryTh Z m = pure (dropAll m) +arbitraryTh n@(S n') m@(S m') = oneof [keepOne, dropOne] + where + keepOne = KeepOne <$> arbitraryTh n' m + dropOne = case plusCommS n' (erase m') of Refl -> DropOne <$> arbitraryTh n m' + +-------------------------------------------------------------------------------- +-- QuickCheck instances for SomeThBound + +data SomeThBound = forall n. SomeThBound !(SNat n) + +deriving stock instance Show SomeThBound + +instance Arbitrary SomeThBound where + arbitrary :: Gen SomeThBound + arbitrary = do + SomeThBoundRep nRep <- arbitrary + pure $ + case toSomeSNatRaw nRep of + SomeSNat n -> SomeThBound n + +-------------------------------------------------------------------------------- +-- QuickCheck instances for SomeThinIxArgs + +data SomeThinIxArgs = forall n m. SomeThinIxArgs (SNat n) (SNat m) (n :<= m) (Ix n) + +deriving stock instance Show SomeThinIxArgs + +instance Arbitrary SomeThinIxArgs where + arbitrary :: Gen SomeThinIxArgs + arbitrary = do + SomeThBound n' <- arbitrary + SomeThBound d <- arbitrary + let n = Safe.S n' + let m = n `Safe.plus` d + SomeThinIxArgs n m <$> arbitraryTh n d <*> arbitraryIx n + +-------------------------------------------------------------------------------- +-- QuickCheck instances for SomeThickIxArgs + +data SomeThickIxArgs = forall n m. SomeThickIxArgs (SNat n) (SNat m) (n :<= m) (Ix m) + +deriving stock instance Show SomeThickIxArgs + +instance Arbitrary SomeThickIxArgs where + arbitrary :: Gen SomeThickIxArgs + arbitrary = do + SomeThBound n' <- arbitrary + SomeThBound d <- arbitrary + let n = Safe.S n' + let m = n `Safe.plus` d + SomeThickIxArgs n m <$> arbitraryTh n d <*> arbitraryIx m + +-------------------------------------------------------------------------------- +-- QuickCheck instances for SomeThinThArgs + +data SomeThinThArgs = forall l n m. SomeThinThArgs (SNat l) (SNat n) (SNat m) (n :<= m) (l :<= n) + +deriving stock instance Show SomeThinThArgs + +instance Arbitrary SomeThinThArgs where + arbitrary :: Gen SomeThinThArgs + arbitrary = do + SomeThBoundRep mRep <- arbitrary + nRep <- chooseSizedBoundedIntegral (0, mRep) + let dmRep = mRep - nRep + lRep <- chooseSizedBoundedIntegral (0, nRep) + let dnRep = nRep - lRep + case (Safe.toSomeSNatRaw lRep, Safe.toSomeSNatRaw dnRep, Safe.toSomeSNatRaw dmRep) of + (Safe.SomeSNat l, Safe.SomeSNat dn, Safe.SomeSNat dm) -> do + let n = l `Safe.plus` dn + let m = n `Safe.plus` dm + SomeThinThArgs l n m <$> arbitraryTh n dm <*> arbitraryTh l dn + +-------------------------------------------------------------------------------- +-- Helper Functions +-------------------------------------------------------------------------------- + +-- | @`erase` x@ erases the content of @x@ to a @`Proxy`@. +erase :: f a -> Proxy a +erase _ = Proxy +{-# INLINE erase #-} diff --git a/src-arbitrary/Data/Type/Nat/Singleton/Arbitrary.hs b/src-arbitrary/Data/Type/Nat/Singleton/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Data/Type/Nat/Singleton/Arbitrary.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE DerivingStrategies #-} + +module Data.Type.Nat.Singleton.Arbitrary (SomeSNatRep (..), getSNatRep) where + +import Data.Type.Nat.Singleton.Fast (SNatRep) +import Test.QuickCheck.Arbitrary (Arbitrary (..)) +import Test.QuickCheck.Gen (Gen) +import Test.QuickCheck.Modifiers (NonNegative (getNonNegative)) + +-------------------------------------------------------------------------------- +-- QuickCheck instances for SomeSNat +-------------------------------------------------------------------------------- + +newtype SomeSNatRep = SomeSNatRep SNatRep + deriving stock (Eq, Show) + +getSNatRep :: SomeSNatRep -> SNatRep +getSNatRep (SomeSNatRep nRep) = nRep + +instance Arbitrary SomeSNatRep where + arbitrary :: Gen SomeSNatRep + arbitrary = SomeSNatRep . getNonNegative <$> arbitrary + + shrink :: SomeSNatRep -> [SomeSNatRep] + shrink (SomeSNatRep nRep) = SomeSNatRep <$> shrink nRep diff --git a/src-arbitrary/Data/Type/Nat/Singleton/Fast/Arbitrary.hs b/src-arbitrary/Data/Type/Nat/Singleton/Fast/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Data/Type/Nat/Singleton/Fast/Arbitrary.hs @@ -0,0 +1,28 @@ +{-# OPTIONS_GHC -Wno-orphans #-} + +module Data.Type.Nat.Singleton.Fast.Arbitrary () where + +import Data.Type.Nat.Singleton.Arbitrary (getSNatRep) +import Data.Type.Nat.Singleton.Fast (SomeSNat (..), fromSomeSNatRaw, toSomeSNatRaw) +import Test.QuickCheck.Arbitrary (Arbitrary (..), CoArbitrary (..), shrinkIntegral) +import Test.QuickCheck.Function (Function (..), functionMap, (:->)) +import Test.QuickCheck.Gen (Gen) + +-------------------------------------------------------------------------------- +-- QuickCheck instances for SomeSNat +-------------------------------------------------------------------------------- + +instance Arbitrary SomeSNat where + arbitrary :: Gen SomeSNat + arbitrary = toSomeSNatRaw . getSNatRep <$> arbitrary + + shrink :: SomeSNat -> [SomeSNat] + shrink = fmap toSomeSNatRaw . shrinkIntegral . fromSomeSNatRaw + +instance CoArbitrary SomeSNat where + coarbitrary :: SomeSNat -> Gen b -> Gen b + coarbitrary = coarbitrary . fromSomeSNatRaw + +instance Function SomeSNat where + function :: (SomeSNat -> b) -> SomeSNat :-> b + function = functionMap fromSomeSNatRaw toSomeSNatRaw diff --git a/src-arbitrary/Data/Type/Nat/Singleton/Safe/Arbitrary.hs b/src-arbitrary/Data/Type/Nat/Singleton/Safe/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Data/Type/Nat/Singleton/Safe/Arbitrary.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Data.Type.Nat.Singleton.Safe.Arbitrary () where + +import Data.Type.Nat.Singleton.Arbitrary (getSNatRep) +import Data.Type.Nat.Singleton.Safe (SomeSNat (..), fromSomeSNatRaw, toSomeSNatRaw) +import Test.QuickCheck.Arbitrary (Arbitrary (..), CoArbitrary (..), shrinkIntegral) +import Test.QuickCheck.Function (Function (..), functionMap, (:->)) +import Test.QuickCheck.Gen (Gen) + +-------------------------------------------------------------------------------- +-- QuickCheck instances for SomeSNat +-------------------------------------------------------------------------------- + +instance Arbitrary SomeSNat where + arbitrary :: Gen SomeSNat + arbitrary = toSomeSNatRaw . getSNatRep <$> arbitrary + + shrink :: SomeSNat -> [SomeSNat] + shrink = fmap toSomeSNatRaw . shrinkIntegral . fromSomeSNatRaw + +instance CoArbitrary SomeSNat where + coarbitrary :: SomeSNat -> Gen b -> Gen b + coarbitrary = coarbitrary . fromSomeSNatRaw + +instance Function SomeSNat where + function :: (SomeSNat -> b) -> SomeSNat :-> b + function = functionMap fromSomeSNatRaw toSomeSNatRaw diff --git a/src-arbitrary/Test/QuickCheck/Extra.hs b/src-arbitrary/Test/QuickCheck/Extra.hs new file mode 100644 --- /dev/null +++ b/src-arbitrary/Test/QuickCheck/Extra.hs @@ -0,0 +1,38 @@ +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} + +module Test.QuickCheck.Extra ( + chooseSizedBoundedIntegral, + chooseSizesBoundedPositiveIntegral, +) where + +import Control.Exception (assert) +import Data.Bits (Bits (..)) +import Test.QuickCheck.Gen (Gen, chooseInteger, sized) + +chooseSizedBoundedIntegral :: (Integral a) => (a, a) -> Gen a +chooseSizedBoundedIntegral (mn, mx) = + assert (mn >= 0 && mx >= mn) $ + let ilog2 1 = 0 + ilog2 n | n > 0 = 1 + ilog2 (n `div` 2) + + -- How many bits are needed to represent this type? + -- (This number is an upper bound, not exact.) + bits = ilog2 (toInteger mx - toInteger mn + 1) + in sized $ \k -> + let + -- Reach maximum size by k=80, or quicker for small integer types + power = ((bits `max` 40) * k) `div` 80 + + -- Bounds should be 2^power, but: + -- * clamp the result to minBound/maxBound + -- * clamp power to 'bits', in case k is a huge number + lo = toInteger mn `max` (-1 `shiftL` (power `min` bits)) + hi = toInteger mx `min` (1 `shiftL` (power `min` bits)) + in + fmap fromInteger (chooseInteger (lo, hi)) +{-# INLINEABLE chooseSizedBoundedIntegral #-} +{-# ANN chooseSizedBoundedIntegral ("HLint: ignore Avoid partial function" :: String) #-} +{-# ANN chooseSizedBoundedIntegral ("HLint: ignore Parenthesize unary negation" :: String) #-} + +chooseSizesBoundedPositiveIntegral :: (Integral a) => a -> Gen a +chooseSizesBoundedPositiveIntegral n = chooseSizedBoundedIntegral (1, n) diff --git a/src-fast/Data/DeBruijn/Environment/Fast.hs b/src-fast/Data/DeBruijn/Environment/Fast.hs new file mode 100644 --- /dev/null +++ b/src-fast/Data/DeBruijn/Environment/Fast.hs @@ -0,0 +1,152 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-duplicate-exports #-} + +module Data.DeBruijn.Environment.Fast ( + -- * Environments + Env (Nil, (:>)), + (!), + + -- * Fast + EnvRep, + Env (UnsafeEnv, envRep), +) where + +import Data.DeBruijn.Index.Fast (Ix (ixRep), ixRepToInt) +import Data.Kind (Type) +import Data.Type.Nat (Nat (..), Pos, Pred) +import Unsafe.Coerce (unsafeCoerce) + +-------------------------------------------------------------------------------- +-- Conditional Imports +-------------------------------------------------------------------------------- + +#if defined(ENV_AS_SEQ) +import Data.Sequence (Seq) +import Data.Sequence qualified as Seq +import Data.Maybe (fromJust) +#elif defined(ENV_AS_SKEW_LIST) +import Data.SkewList.Strict (SkewList) +import Data.SkewList.Strict qualified as SkewList +#endif + +-------------------------------------------------------------------------------- +-- Environment Representation +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +-- Environment Representation: Finger Tree +#if defined(ENV_AS_SEQ) + +type EnvRep a = Seq a + +mkNilRep :: EnvRep a +mkNilRep = Seq.empty +{-# INLINE mkNilRep #-} + +mkSnocRep :: EnvRep a -> a -> EnvRep a +mkSnocRep xs x = xs Seq.:|> x +{-# INLINE mkSnocRep #-} + +elEnvRep :: b -> (EnvRep a -> a -> b) -> EnvRep a -> b +elEnvRep ifNil ifSnoc = \case + Seq.Empty -> ifNil + xs Seq.:|> x -> ifSnoc xs x +{-# INLINE elEnvRep #-} + +lookupRep :: Int -> EnvRep a -> a +lookupRep = (fromJust .) . Seq.lookup +{-# INLINE lookupRep #-} +{-# ANN lookupRep ("HLint: ignore Avoid partial function" :: String) #-} + +-------------------------------------------------------------------------------- +-- Environment Representation: Skew List +#elif defined(ENV_AS_SKEW_LIST) + +type EnvRep a = SkewList a + +mkNilRep :: EnvRep a +mkNilRep = SkewList.Nil +{-# INLINE mkNilRep #-} + +mkSnocRep :: EnvRep a -> a -> EnvRep a +mkSnocRep xs x = SkewList.Cons x xs +{-# INLINE mkSnocRep #-} + +elEnvRep :: b -> (EnvRep a -> a -> b) -> EnvRep a -> b +elEnvRep ifNil ifSnoc = \case + SkewList.Nil -> ifNil + SkewList.Cons x xs -> ifSnoc xs x +{-# INLINE elEnvRep #-} + +lookupRep :: Int -> EnvRep a -> a +lookupRep = flip (SkewList.!) +{-# INLINE lookupRep #-} +{-# ANN lookupRep ("HLint: ignore Avoid partial function" :: String) #-} + +-------------------------------------------------------------------------------- +-- Environment Representation: None +#elif !defined(__HLINT__) +#error "cpp: define one of [ENV_AS_SEQ, ENV_AS_SKEW_LIST]" +#endif + +-------------------------------------------------------------------------------- +-- Environments +-------------------------------------------------------------------------------- + +type Env :: Nat -> Type -> Type +newtype Env n a = UnsafeEnv {envRep :: EnvRep a} + +type role Env nominal representational + +deriving stock instance Functor (Env n) + +deriving stock instance Foldable (Env n) + +deriving stock instance Traversable (Env n) + +mkNil :: Env Z a +mkNil = UnsafeEnv mkNilRep +{-# INLINE mkNil #-} + +mkSnoc :: Env n a -> a -> Env (S n) a +mkSnoc = (UnsafeEnv .) . mkSnocRep . (.envRep) +{-# INLINE mkSnoc #-} + +elEnv :: b -> (Env (Pred n) a -> a -> b) -> Env n a -> b +elEnv ifNil ifSnoc = elEnvRep ifNil (ifSnoc . UnsafeEnv) . (.envRep) +{-# INLINE elEnv #-} + +type EnvF :: (Nat -> Type -> Type) -> Nat -> Type -> Type +data EnvF env n a where + NilF :: EnvF env Z a + SnocF :: env n a -> a -> EnvF env (S n) a + +projectEnv :: Env n a -> EnvF Env n a +projectEnv = elEnv (unsafeCoerce NilF) (unsafeCoerce . SnocF) +{-# INLINE projectEnv #-} + +embedEnv :: EnvF Env n a -> Env n a +embedEnv = \case + NilF -> mkNil + SnocF xs x -> mkSnoc xs x +{-# INLINE embedEnv #-} + +pattern Nil :: () => (n ~ Z) => Env n a +pattern Nil <- (projectEnv -> NilF) where Nil = embedEnv NilF +{-# INLINE Nil #-} + +pattern (:>) :: () => (Pos n) => Env (Pred n) a -> a -> Env n a +pattern (:>) xs x <- (projectEnv -> SnocF xs x) where (:>) xs x = embedEnv (SnocF xs x) +{-# INLINE (:>) #-} + +{-# COMPLETE Nil, (:>) #-} + +(!) :: Env n a -> Ix n -> a +xs ! i = lookupRep (ixRepToInt i.ixRep) xs.envRep diff --git a/src-fast/Data/DeBruijn/Index/Fast.hs b/src-fast/Data/DeBruijn/Index/Fast.hs new file mode 100644 --- /dev/null +++ b/src-fast/Data/DeBruijn/Index/Fast.hs @@ -0,0 +1,317 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-duplicate-exports #-} + +module Data.DeBruijn.Index.Fast ( + -- * DeBruijn Indexes + Ix (FZ, FS), + eqIx, + fromIx, + fromIxRaw, + isPos, + thin, + thick, + inject, + raise, + + -- * Existential Wrapper + SomeIx (..), + withSomeIx, + toSomeIx, + toSomeIxRaw, + fromSomeIx, + fromSomeIxRaw, + + -- * Fast + IxRep, + intToIxRep, + ixRepToInt, + snatRepToIxRep, + ixRepToSNatRep, + Ix (UnsafeIx, ixRep), +) where + +import Control.DeepSeq (NFData (..)) +import Data.Bifunctor (Bifunctor (..)) +import Data.Kind (Type) +import Data.Type.Equality (type (:~:) (Refl)) +import Data.Type.Nat (Nat (..), Pos, Pred, type (+)) +import Data.Type.Nat.Singleton.Fast (SNat (..), SNatRep, decSNat) +import Text.Printf (printf) +import Unsafe.Coerce (unsafeCoerce) + +#if defined(IX_AS_WORD8) || defined(SNAT_AS_WORD8) +import Control.Exception (ArithException (Overflow, Underflow), throw) +import Data.Word (Word8) +#endif + +{- $setup +>>> import Data.DeBruijn.Index.Fast.Arbitrary +-} + +-------------------------------------------------------------------------------- +-- DeBruijn Index Representation +-------------------------------------------------------------------------------- + +#if defined(IX_AS_WORD8) +type IxRep = Word8 +#elif defined(IX_AS_INT) +type IxRep = Int +#elif !defined(__HLINT__) +#error "cpp: define one of [IX_AS_WORD8, IX_AS_INT]" +#endif + +mkFZRep :: IxRep +mkFZRep = 0 +{-# INLINE mkFZRep #-} + +mkFSRep :: IxRep -> IxRep +mkFSRep = (1 +) +{-# INLINE mkFSRep #-} + +unFSRep :: IxRep -> IxRep +unFSRep = subtract 1 +{-# INLINE unFSRep #-} + +elIxRep :: a -> (IxRep -> a) -> IxRep -> a +elIxRep ifZ ifS i = + if i == mkFZRep then ifZ else ifS (unFSRep i) +{-# INLINE elIxRep #-} + +thinRep :: IxRep -> IxRep -> IxRep +thinRep i j + | i <= j = mkFSRep j + | otherwise = j + +thickRep :: IxRep -> IxRep -> Maybe IxRep +thickRep i j = case i `compare` j of + LT -> Just (unFSRep j) + EQ -> Nothing + GT -> Just j + +-------------------------------------------------------------------------------- +-- DeBruijn Indexes +-------------------------------------------------------------------------------- + +-- | @'Ix' n@ is the type of DeBruijn indices less than @n@. +type Ix :: Nat -> Type +newtype Ix n = UnsafeIx {ixRep :: IxRep} + +type role Ix nominal + +eqIx :: Ix n -> Ix m -> Bool +eqIx i j = fromIxRaw i == fromIxRaw j + +instance Eq (Ix n) where + (==) :: Ix n -> Ix n -> Bool + (==) = eqIx + +instance Show (Ix n) where + showsPrec :: Int -> Ix n -> ShowS + showsPrec p = + showParen (p > 10) . \case + FZ -> showString "FZ" + FS n -> showString "FS " . showsPrec 11 n + +instance NFData (Ix n) where + rnf :: Ix n -> () + rnf (UnsafeIx u) = rnf u + +mkFZ :: Ix (S n) +mkFZ = UnsafeIx mkFZRep +{-# INLINE mkFZ #-} + +mkFS :: Ix n -> Ix (S n) +mkFS = UnsafeIx . mkFSRep . (.ixRep) +{-# INLINE mkFS #-} + +elIx :: a -> (Ix (Pred n) -> a) -> Ix n -> a +elIx ifFZ ifFS = elIxRep ifFZ (ifFS . UnsafeIx) . (.ixRep) +{-# INLINE elIx #-} + +-- | @'fromSNat' n@ returns the numeric representation of 'SNat n'. +fromIx :: (Integral i) => Ix n -> i +fromIx = fromInteger . toInteger . (.ixRep) +{-# INLINE fromIx #-} + +-- | @'fromIxRaw' n@ returns the raw numeric representation of 'SNat n'. +fromIxRaw :: Ix n -> IxRep +fromIxRaw = (.ixRep) +{-# INLINE fromIxRaw #-} + +-- | @'IxF'@ is the base functor of @'Ix'@. +data IxF (ix :: Nat -> Type) (n :: Nat) :: Type where + FZF :: IxF ix (S m) + FSF :: !(ix m) -> IxF ix (S m) + +projectIx :: Ix n -> IxF Ix n +projectIx = elIx (unsafeCoerce FZF) (unsafeCoerce . FSF) +{-# INLINE projectIx #-} + +embedIx :: IxF Ix n -> Ix n +embedIx = \case + FZF -> mkFZ + FSF i -> mkFS i +{-# INLINE embedIx #-} + +-- NOTE: +-- Type signatures for pattern synonyms are weird, see: +-- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.html#typing-of-pattern-synonyms + +pattern FZ :: () => (Pos n) => Ix n +pattern FZ <- (projectIx -> FZF) where FZ = embedIx FZF +{-# INLINE FZ #-} + +pattern FS :: () => (Pos n) => Ix (Pred n) -> Ix n +pattern FS i <- (projectIx -> FSF i) where FS i = embedIx (FSF i) +{-# INLINE FS #-} + +{-# COMPLETE FZ, FS #-} + +-- | If any value of type @'Ix' n@ exists, @n@ must have a predecessor. +isPos :: Ix n -> ((Pos n) => a) -> a +isPos FZ r = r +isPos (FS _) r = r + +-- | Thinning. +thin :: Ix (S n) -> Ix n -> Ix (S n) +thin i j = UnsafeIx (thinRep i.ixRep j.ixRep) + +-- | Thickening. +thick :: Ix (S n) -> Ix (S n) -> Maybe (Ix n) +thick i j = UnsafeIx <$> thickRep i.ixRep j.ixRep + +-- | Inject. +inject :: Ix n -> SNat m -> Ix (n + m) +inject i _m = UnsafeIx i.ixRep + +-- | Raise. +raise :: SNat n -> Ix m -> Ix (n + m) +raise n j = UnsafeIx (snatRepToIxRep n.snatRep + j.ixRep) + +-- | Convert an 'IxRep' to an 'Int'. +intToIxRep :: Int -> IxRep +#ifdef IX_AS_WORD8 +-- TODO: Make this safe. +intToIxRep int + | int < 0 = throw Underflow + | int > fromIntegral (maxBound @Word8) = throw Overflow + | otherwise = fromIntegral @Int @Word8 int +{-# INLINE intToIxRep #-} +#else +intToIxRep = id @Int +{-# INLINE intToIxRep #-} +#endif + +-- | Convert an 'IxRep' to an 'Int'. +ixRepToInt :: IxRep -> Int +#ifdef IX_AS_WORD8 +ixRepToInt = fromIntegral @Word8 @Int +{-# INLINE ixRepToInt #-} +#else +ixRepToInt = id @Int +{-# INLINE ixRepToInt #-} +#endif + +-- | Convert an 'SNatRep' to an 'IxRep'. +snatRepToIxRep :: SNatRep -> IxRep +#ifdef SNAT_AS_WORD8 +#ifdef IX_AS_WORD8 +snatRepToIxRep = id @Word8 +{-# INLINE snatRepToIxRep #-} +#else +snatRepToIxRep = fromIntegral @Word8 @Int +{-# INLINE snatRepToIxRep #-} +#endif +#else +#ifdef IX_AS_WORD8 +-- Int -> Word8 +snatRepToIxRep snatRep + | snatRep < 0 = throw Underflow + | snatRep > fromIntegral (maxBound @Word8) = throw Overflow + | otherwise = fromIntegral snatRep +#else +snatRepToIxRep = id @Int +{-# INLINE snatRepToIxRep #-} +#endif +#endif + +-- | Convert an 'IxRep' to an 'SNatRep'. +ixRepToSNatRep :: IxRep -> SNatRep +#ifdef SNAT_AS_WORD8 +#ifdef IX_AS_WORD8 +ixRepToSNatRep = id @Word8 +{-# INLINE ixRepToSNatRep #-} +#else +ixRepToSNatRep ixRep + | ixRep < 0 = throw Underflow + | ixRep > fromIntegral (maxBound @Word8) = throw Overflow + | otherwise = fromIntegral ixRep +{-# INLINE ixRepToSNatRep #-} +#endif +#else +#ifdef IX_AS_WORD8 +ixRepToSNatRep = fromIntegral @Int @Word8 +#else +ixRepToSNatRep = id @Int +{-# INLINE ixRepToSNatRep #-} +#endif +#endif + +-------------------------------------------------------------------------------- +-- Existential Wrapper +-------------------------------------------------------------------------------- + +-- | An existential wrapper around indexes. +type SomeIx :: Type +data SomeIx = forall (n :: Nat). SomeIx + { bound :: {-# UNPACK #-} !(SNat n) + , index :: {-# UNPACK #-} !(Ix n) + } + +instance NFData SomeIx where + rnf :: SomeIx -> () + rnf (SomeIx n i) = rnf n `seq` rnf i + +instance Eq SomeIx where + (==) :: SomeIx -> SomeIx -> Bool + SomeIx n i == SomeIx m j + | Just Refl <- decSNat n m = eqIx i j + | otherwise = False + +deriving instance Show SomeIx + +withSomeIx :: (forall n. SNat n -> Ix n -> a) -> SomeIx -> a +withSomeIx action (SomeIx n i) = action n i + +{-| @'toSomeIx' n@ constructs the index @n@ at type @'Ix' n@ from the number @n@. + +prop> toSomeIx (fromSomeIx i) == i +-} +toSomeIx :: (Integral n, Integral i) => (n, i) -> SomeIx +toSomeIx = toSomeIxRaw . bimap fromIntegral fromIntegral + +{-| @'toSomeIxRaw' n@ constructs the index @n@ at type @'Ix' n@ from the 'Int' @n@. + +prop> toSomeIxRaw (fromSomeIxRaw i) == i +-} +toSomeIxRaw :: (SNatRep, IxRep) -> SomeIx +toSomeIxRaw (n, i) + | i < 0 = error $ printf "index cannot contain negative value, found index %d" i + | snatRepToIxRep n <= i = error $ printf "bound must be larger than index, found bound %d and index %d" n i + | otherwise = SomeIx (UnsafeSNat n) (UnsafeIx i) + +-- | @'fromSomeSNat' n@ returns the numeric representation of the wrapped index. +fromSomeIx :: (Integral n, Integral i) => SomeIx -> (n, i) +fromSomeIx = bimap fromIntegral fromIntegral . fromSomeIxRaw + +-- | @'fromSomeSNat' n@ returns the 'Int' representation of the wrapped index. +fromSomeIxRaw :: SomeIx -> (SNatRep, IxRep) +fromSomeIxRaw (SomeIx (UnsafeSNat bound) (UnsafeIx index)) = (bound, index) diff --git a/src-fast/Data/DeBruijn/Thinning/Fast.hs b/src-fast/Data/DeBruijn/Thinning/Fast.hs new file mode 100644 --- /dev/null +++ b/src-fast/Data/DeBruijn/Thinning/Fast.hs @@ -0,0 +1,481 @@ +{-# LANGUAGE CApiFFI #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-duplicate-exports #-} + +#if defined(TH_AS_NATURAL) || defined(TH_AS_WORD64) +{-# LANGUAGE MagicHash #-} +#endif + +#if defined(TH_AS_NATURAL) +#include "MachDeps.h" +#endif + +module Data.DeBruijn.Thinning.Fast ( + -- * Thinnings + (:<=) (KeepAll, KeepOne, DropOne), + dropAll, + toBools, + fromTh, + fromThRaw, + + -- * Existential Wrapper + SomeTh (..), + fromBools, + toSomeTh, + toSomeThRaw, + fromSomeTh, + fromSomeThRaw, + + -- * The action of thinnings on 'Nat'-indexed types + Thin (..), + + -- * Fast + ThRep, + bitsToThRep, + thRepToBits, + (:<=) (UnsafeTh, thRep), +) where + +import Control.DeepSeq (NFData (..)) +import Data.Bifunctor (Bifunctor (..)) +import Data.Bits (Bits (..)) +import Data.DeBruijn.Index.Fast (Ix (..), isPos) +import Data.Kind (Constraint, Type) +import Data.Type.Equality (type (:~:) (Refl)) +import Data.Type.Nat (Nat (..), Pos, Pred) +import Data.Type.Nat.Singleton.Fast (SNat (..), SNatRep, SomeSNat (..), decSNat, plus, toSomeSNat, toSomeSNatRaw) +import Unsafe.Coerce (unsafeCoerce) + +#if defined(TH_AS_BITVEC) +import Data.Bit (Bit) +import Data.Vector.Unboxed (Vector) +#elif defined(TH_AS_INTEGER) +-- No import needed for Integer +#elif defined(TH_AS_NATURAL) + +import GHC.Num.BigNat (BigNat#, bigNatFromWord#, bigNatIndex#, bigNatShiftL#, bigNatShiftR#, bigNatOrWord#, bigNatTestBit#, bigNatSize#) +import GHC.Num.Natural (Natural (..), naturalZero) +import GHC.Prim (and#, clz#, geWord#, leWord#, minusWord#, neWord#, popCnt#, uncheckedShiftL#, uncheckedShiftRL#) +import GHC.Types (isTrue#) +#elif defined(TH_AS_WORD64) +import Control.Exception (ArithException (Overflow), throw) +import Data.Bits (FiniteBits (..)) +import GHC.Types (Word (W#)) +#endif +-- Import for specialised thinning for Word +#if defined(TH_AS_WORD64) || defined(TH_AS_NATURAL) +import GHC.Prim (Word#, or#, not#, pdep#) +#endif + +-------------------------------------------------------------------------------- +-- Thinning Representation +-------------------------------------------------------------------------------- + +#if defined(TH_AS_BITVEC) +type ThRep = Vector Bit +#elif defined(TH_AS_INTEGER) +type ThRep = Integer +#elif defined(TH_AS_NATURAL) +type ThRep = Natural +#elif defined(TH_AS_WORD64) +type ThRep = Word +#elif !defined(__HLINT__) +#error "cpp: define one of [TH_AS_BITVEC, TH_AS_INTEGER, TH_AS_NATURAL, TH_AS_WORD64]" +#endif + +-------------------------------------------------------------------------------- +-- Thinning Representation: Natural +-- +-- NOTE: +-- The implementation for Natural manually inlines the 'shift' and 'setBit' +-- operations, as these functions are marked with 'NOINLINE' in ghc-bignum. +#if defined(TH_AS_NATURAL) + +mkKeepAllRep :: ThRep +mkKeepAllRep = naturalZero +{-# INLINE mkKeepAllRep #-} + +mkKeepOneRep :: ThRep -> ThRep +mkKeepOneRep v@(NS x) + | 0## <- x = v + | isTrue# (clz# x `geWord#` 1##) = NS (x `uncheckedShiftL#` 1#) + | True = NB (bigNatFromWord# x `bigNatShiftL#` 1##) +mkKeepOneRep (NB x) = NB (x `bigNatShiftL#` 1##) +{-# INLINE mkKeepOneRep #-} + +mkDropOneRep :: ThRep -> ThRep +mkDropOneRep (NS x) + | 0## <- x = NS 1## + | isTrue# (clz# x `geWord#` 1##) = NS ((x `uncheckedShiftL#` 1#) `or#` 1##) + | True = NB ((bigNatFromWord# x `bigNatShiftL#` 1##) `bigNatOrWord#` 1##) +mkDropOneRep (NB x) = NB ((x `bigNatShiftL#` 1##) `bigNatOrWord#` 1##) +{-# INLINE mkDropOneRep #-} + +elThRep :: a -> (ThRep -> a) -> (ThRep -> a) -> ThRep -> a +elThRep ifKeepAll ifKeepOne ifDropOne = go + where + go (NS w) + | 0## <- w = ifKeepAll + | isTrue# ((w `and#` 1##) `neWord#` 0##) = ifDropOne thRepArg + | otherwise = ifKeepOne thRepArg + where + thRepArg = NS (w `uncheckedShiftRL#` 1#) + go (NB bn) + | isTrue# (bigNatTestBit# bn 0##) = ifDropOne thRepArg + | otherwise = ifKeepOne thRepArg + where + thRepArg = thRepFromBigNat# (bn `bigNatShiftR#` 1##) +{-# INLINE elThRep #-} + +thRepFromBigNat# :: BigNat# -> ThRep +thRepFromBigNat# x = case bigNatSize# x of + 0# -> naturalZero + 1# -> NS (bigNatIndex# x 0#) + _ -> NB x + +-------------------------------------------------------------------------------- +-- Thinning Representation: Bits +#elif defined(TH_AS_BITVEC) || defined(TH_AS_INTEGER) + +mkKeepAllRep :: ThRep +mkKeepAllRep = zeroBits +{-# INLINE mkKeepAllRep #-} + +mkKeepOneRep :: ThRep -> ThRep +mkKeepOneRep = (`unsafeShiftL` 1) +{-# INLINE mkKeepOneRep #-} + +mkDropOneRep :: ThRep -> ThRep +mkDropOneRep = (`setBit` 0) . (`unsafeShiftL` 1) +{-# INLINE mkDropOneRep #-} + +elThRep :: a -> (ThRep -> a) -> (ThRep -> a) -> ThRep -> a +elThRep ifKeepAll ifKeepOne ifDropOne th + | th == zeroBits = ifKeepAll + | testBit th 0 = ifDropOne (unsafeShiftR th 1) + | otherwise = ifKeepOne (unsafeShiftR th 1) +{-# INLINE elThRep #-} + +-------------------------------------------------------------------------------- +-- Thinning Representation: Finite Bits +#elif defined(TH_AS_WORD64) + +mkKeepAllRep :: ThRep +mkKeepAllRep = zeroBits +{-# INLINE mkKeepAllRep #-} + +mkKeepOneRep :: ThRep -> ThRep +mkKeepOneRep r + | countLeadingZeros r < 1 = throw Overflow + | otherwise = r `unsafeShiftL` 1 +{-# INLINE mkKeepOneRep #-} + +mkDropOneRep :: ThRep -> ThRep +mkDropOneRep r + | countLeadingZeros r < 1 = throw Overflow + | otherwise = r `unsafeShiftL` 1 .|. 1 +{-# INLINE mkDropOneRep #-} + +elThRep :: a -> (ThRep -> a) -> (ThRep -> a) -> ThRep -> a +elThRep ifKeepAll ifKeepOne ifDropOne r + | r == zeroBits = ifKeepAll + | testBit r 0 = ifDropOne (r `unsafeShiftR` 1) + | otherwise = ifKeepOne (r `unsafeShiftR` 1) +{-# INLINE elThRep #-} +#endif + +-------------------------------------------------------------------------------- +-- Specialised Implementation of thin for Word +#if defined(TH_AS_NATURAL) || defined(TH_AS_WORD64) +{- +12<=29: 0b0000000000000000000000000000000000010101101010111010111110000110 +04<=12: 0b0000000000000000000000000000000000000000000000000000111111110000 +expect: 0b0000000000000000000000000000000000011111111111111111111111000110 +not nm: 0b1111111111111111111111111111111111101010010101000101000001111001 +dep ln: 0b0000000000000000000000000000000000001010010101000101000001000000 +-} +thinWord# :: Word# -> Word# -> Word# +thinWord# nm# ln# = nm# `or#` (pdep# ln# (not# nm#)) +{-# INLINE thinWord# #-} +#endif + +-------------------------------------------------------------------------------- +-- Thinnings +-------------------------------------------------------------------------------- + +type (:<=) :: Nat -> Nat -> Type +newtype (:<=) n m = UnsafeTh {thRep :: ThRep} + +type role (:<=) nominal nominal + +mkKeepAll :: n :<= n +mkKeepAll = UnsafeTh mkKeepAllRep +{-# INLINE mkKeepAll #-} + +mkKeepOne :: n :<= m -> S n :<= S m +mkKeepOne = UnsafeTh . mkKeepOneRep . (.thRep) +{-# INLINE mkKeepOne #-} + +mkDropOne :: n :<= m -> n :<= S m +mkDropOne = UnsafeTh . mkDropOneRep . (.thRep) +{-# INLINE mkDropOne #-} + +elTh :: a -> (Pred n :<= Pred m -> a) -> (n :<= Pred m -> a) -> n :<= m -> a +elTh ifKeepAll ifKeepOne ifDropOne = + elThRep ifKeepAll (ifKeepOne . UnsafeTh) (ifDropOne . UnsafeTh) . (.thRep) +{-# INLINE elTh #-} + +data ThF (th :: Nat -> Nat -> Type) (n :: Nat) (m :: Nat) where + KeepAllF :: ThF th n n + KeepOneF :: !(th n m) -> ThF th (S n) (S m) + DropOneF :: !(th n m) -> ThF th n (S m) + +projectTh :: n :<= m -> ThF (:<=) n m +projectTh = + elTh (unsafeCoerce KeepAllF) (unsafeCoerce . KeepOneF) (unsafeCoerce . DropOneF) +{-# INLINE projectTh #-} + +embedTh :: ThF (:<=) n m -> n :<= m +embedTh = \case + KeepAllF -> mkKeepAll + KeepOneF n'm' -> mkKeepOne n'm' + DropOneF nm' -> mkDropOne nm' +{-# INLINE embedTh #-} + +pattern KeepAll :: () => (n ~ m) => n :<= m +pattern KeepAll <- (projectTh -> KeepAllF) where KeepAll = embedTh KeepAllF +{-# INLINE KeepAll #-} + +pattern KeepOne :: () => (Pos n, Pos m) => Pred n :<= Pred m -> n :<= m +pattern KeepOne nm <- (projectTh -> KeepOneF nm) where KeepOne nm = embedTh (KeepOneF nm) +{-# INLINE KeepOne #-} + +pattern DropOne :: () => (Pos m) => n :<= Pred m -> n :<= m +pattern DropOne nm <- (projectTh -> DropOneF nm) where DropOne nm = embedTh (DropOneF nm) +{-# INLINE DropOne #-} + +{-# COMPLETE KeepAll, KeepOne, DropOne #-} + +deriving newtype instance Eq (n :<= m) + +instance Show (n :<= m) where + showsPrec :: Int -> n :<= m -> ShowS + showsPrec p = + showParen (p > 10) . \case + KeepAll -> showString "KeepAll" + KeepOne n'm' -> showString "KeepOne " . showsPrec 11 n'm' + DropOne nm' -> showString "DropOne " . showsPrec 11 nm' + +deriving newtype instance NFData (n :<= m) + +-- | Drop all entries. +dropAll :: SNat m -> Z :<= m +dropAll Z = KeepAll +dropAll (S m') = DropOne (dropAll m') + +-- | Convert a thinning into a list of booleans. +toBools :: n :<= m -> [Bool] +toBools = \case + KeepAll -> [] + KeepOne n'm' -> False : toBools n'm' + DropOne nm' -> True : toBools nm' + +-- | Convert a thinning into a bit sequence. +fromTh :: (Bits bs) => n :<= m -> bs +fromTh = \case + KeepAll -> zeroBits + KeepOne n'm' -> (`unsafeShiftL` 1) . fromTh $ n'm' + DropOne nm' -> (`setBit` 0) . (`unsafeShiftL` 1) . fromTh $ nm' +{-# SPECIALIZE fromTh :: n :<= m -> ThRep #-} + +fromThRaw :: n :<= m -> ThRep +fromThRaw = (.thRep) +{-# INLINE fromThRaw #-} + +-------------------------------------------------------------------------------- +-- Existential Wrapper +-------------------------------------------------------------------------------- + +data SomeTh + = forall n m. + SomeTh + { lower :: SNat n + , upper :: SNat m + , value :: n :<= m + } + +instance Eq SomeTh where + (==) :: SomeTh -> SomeTh -> Bool + SomeTh n1 m1 n1m1 == SomeTh n2 m2 n2m2 + | Just Refl <- decSNat n1 n2 + , Just Refl <- decSNat m1 m2 = + n1m1 == n2m2 + | otherwise = False + +deriving stock instance Show SomeTh + +instance NFData SomeTh where + rnf :: SomeTh -> () + rnf SomeTh{..} = rnf lower `seq` rnf upper `seq` rnf value + +someKeepAll :: SomeSNat -> SomeTh +someKeepAll (SomeSNat bound) = + SomeTh + { lower = bound + , upper = bound + , value = KeepAll + } +{-# INLINE someKeepAll #-} + +someKeepOne :: SomeTh -> SomeTh +someKeepOne SomeTh{..} = + SomeTh + { lower = S lower + , upper = S upper + , value = KeepOne value + } +{-# INLINE someKeepOne #-} + +someDropOne :: SomeTh -> SomeTh +someDropOne SomeTh{..} = + SomeTh + { lower = lower + , upper = S upper + , value = DropOne value + } +{-# INLINE someDropOne #-} + +fromBools :: (Integral i) => i -> [Bool] -> SomeTh +fromBools bound = go + where + go [] = someKeepAll (toSomeSNat bound) + go (False : bools) = someKeepOne (go bools) + go (True : bools) = someDropOne (go bools) +{-# SPECIALIZE fromBools :: SNatRep -> [Bool] -> SomeTh #-} + +toSomeTh :: (Integral i, Bits bs) => (i, bs) -> SomeTh +toSomeTh (nRep, nmRep) = toSomeThRaw (fromIntegral nRep, copyBits nmRep) +{-# SPECIALIZE toSomeTh :: (SNatRep, ThRep) -> SomeTh #-} + +toSomeThRaw :: (SNatRep, ThRep) -> SomeTh +toSomeThRaw (nRep, nmRep) + | SomeSNat n <- toSomeSNatRaw nRep + , let dRep = popCount nmRep + , SomeSNat d <- toSomeSNat dRep + , let m = n `plus` d + , let nm = UnsafeTh nmRep = + SomeTh n m nm +{-# INLINE toSomeThRaw #-} + +withSomeTh :: (forall n m. SNat n -> SNat m -> n :<= m -> r) -> SomeTh -> r +withSomeTh action (SomeTh n m nm) = action n m nm +{-# INLINE withSomeTh #-} + +-- | Convert a thinning into a bit sequence. +fromSomeTh :: (Integral i, Bits bs) => SomeTh -> (i, bs) +fromSomeTh = bimap fromIntegral thRepToBits . fromSomeThRaw +{-# INLINE fromSomeTh #-} + +fromSomeThRaw :: SomeTh -> (SNatRep, ThRep) +fromSomeThRaw = withSomeTh (\n _m nm -> (n.snatRep, nm.thRep)) +{-# INLINE fromSomeThRaw #-} + +bitsToThRep :: (Bits bs) => bs -> ThRep +bitsToThRep = copyBits +{-# INLINE bitsToThRep #-} + +thRepToBits :: (Bits bs) => ThRep -> bs +thRepToBits = copyBits +{-# INLINE thRepToBits #-} + +-- TODO(optimise): +copyBits :: forall bs1 bs2. (Bits bs1, Bits bs2) => bs1 -> bs2 +copyBits bs = go 0 (unsafeShiftL zeroBits (bitCount bs)) bs + where + go :: Int -> bs2 -> bs1 -> bs2 + go i bs2 bs1 + | bs1 == zeroBits = bs2 + | testBit bs1 0 = go (i + 1) (setBit bs2 i) (unsafeShiftR bs1 1) + | otherwise = go (i + 1) bs2 (unsafeShiftR bs1 1) + +bitCount :: (Bits bs) => bs -> Int +bitCount bs + | bs == zeroBits = 0 + | otherwise = 1 + bitCount (unsafeShiftR bs 1) + +-------------------------------------------------------------------------------- +-- Thinning Class +-------------------------------------------------------------------------------- + +-- | The actions of thinnings on natural-indexed data types. +type Thin :: (Nat -> Type) -> Constraint +class Thin f where + thin :: n :<= m -> f n -> f m + thick :: n :<= m -> f m -> Maybe (f n) + +instance Thin Ix where + thin :: n :<= m -> Ix n -> Ix m + thin !t !i = isPos i $ + -- TODO(optimise): this can be done in constant time by converting the + -- index to a 1-thinning, applying constant-time thinning composition, + -- and finally converting back to a number. the conversions should be + -- `bit` and `log2`, both of which consist of one instruction. + case t of + KeepAll -> i + KeepOne n'm' -> + case i of + FZ -> FZ + FS i' -> FS (thin n'm' i') + DropOne nm' -> FS (thin nm' i) + + -- TODO(optimise): + thick :: n :<= m -> Ix m -> Maybe (Ix n) + thick KeepAll i = Just i + thick (KeepOne _n'm') FZ = Just FZ + thick (KeepOne n'm') (FS i') = FS <$> thick n'm' i' + thick (DropOne _nm') FZ = Nothing + thick (DropOne nm') (FS i') = thick nm' i' + +instance Thin ((:<=) l) where + thin :: n :<= m -> l :<= n -> l :<= m +#if defined(TH_AS_NATURAL) + thin (UnsafeTh (NS nm#)) (UnsafeTh (NS ln#)) + | isTrue# (WORD_SIZE_IN_BITS## `minusWord#` clz# ln# `leWord#` popCnt# (not# nm#)) + = UnsafeTh (NS (thinWord# nm# ln#)) + -- TODO(optimise): this can be done for the `NB` case by iterating the + -- `thinWord#` over all components of the `BigNat`. + thin nm KeepAll = nm + thin KeepAll ln = ln + thin (KeepOne n'm') (KeepOne l'n') = KeepOne (thin n'm' l'n') + thin (KeepOne n'm') (DropOne ln') = DropOne (thin n'm' ln') + thin (DropOne nm') ln = DropOne (thin nm' ln) +#elif defined(TH_AS_WORD64) + thin (UnsafeTh (W# nm#)) (UnsafeTh (W# ln#)) = UnsafeTh (W# (thinWord# nm# ln#)) +#else + thin nm KeepAll = nm + thin KeepAll ln = ln + thin (KeepOne n'm') (KeepOne l'n') = KeepOne (thin n'm' l'n') + thin (KeepOne n'm') (DropOne ln') = DropOne (thin n'm' ln') + thin (DropOne nm') ln = DropOne (thin nm' ln) +#endif + +{- ORMOLU_DISABLE -} + -- TODO(optimise): + thick :: n :<= m -> l :<= m -> Maybe (l :<= n) + thick KeepAll lm = Just lm + thick (KeepOne n'm') KeepAll = KeepOne <$> thick n'm' KeepAll + thick (KeepOne n'm') (KeepOne l'n') = KeepOne <$> thick n'm' l'n' + thick (KeepOne n'm') (DropOne ln') = DropOne <$> thick n'm' ln' + thick (DropOne _nm') KeepAll = Nothing + thick (DropOne _nm') (KeepOne _l'n') = Nothing + thick (DropOne nm') (DropOne ln') = thick nm' ln' +{- ORMOLU_ENABLE -} diff --git a/src-fast/Data/Type/Nat/Singleton/Fast.hs b/src-fast/Data/Type/Nat/Singleton/Fast.hs new file mode 100644 --- /dev/null +++ b/src-fast/Data/Type/Nat/Singleton/Fast.hs @@ -0,0 +1,300 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-duplicate-exports #-} + +module Data.Type.Nat.Singleton.Fast ( + -- * Natural Number Singletons + SNat (Z, S), + fromSNat, + fromSNatRaw, + plus, + decSNat, + + -- * Existential Wrapper + SomeSNat (..), + withSomeSNat, + toSomeSNat, + toSomeSNatRaw, + fromSomeSNat, + fromSomeSNatRaw, + + -- * Laws + plusUnitL, + plusUnitR, + plusCommS, + plusComm, + plusAssoc, + + -- * Linking Type-Level and Value-Level + KnownNat (..), + withKnownNat, + + -- * Fast + SNatRep, + intToSNatRep, + snatRepToInt, + SNat (UnsafeSNat, snatRep), +) where + +import Control.DeepSeq (NFData (..)) +import Control.Exception (assert) +import Data.Kind (Constraint, Type) +import Data.Maybe (isJust) +import Data.Proxy (Proxy (..)) +import Data.Type.Equality (type (:~:) (Refl)) +import Data.Type.Nat (Nat (..), Pos, Pred, type (+)) +import GHC.TypeLits qualified as GHC +import Text.Printf (printf) +import Unsafe.Coerce (unsafeCoerce) + +#ifdef SNAT_AS_WORD8 +import Control.Exception (throw, ArithException (Overflow, Underflow)) +import Data.Word (Word8) +#endif + +{- $setup +>>> import Data.Type.Nat.Singleton.Fast.Arbitrary +-} + +-------------------------------------------------------------------------------- +-- Natural Number Singleton Representation +-------------------------------------------------------------------------------- + +#if defined(SNAT_AS_WORD8) +type SNatRep = Word8 +#elif defined(SNAT_AS_INT) +type SNatRep = Int +#elif !defined(__HLINT__) +#error "cpp: define one of [SNAT_AS_WORD8, SNAT_AS_INT]" +#endif + +isValidSNatRep :: SNatRep -> Bool +isValidSNatRep = (>= 0) + +mkZRep :: SNatRep +mkZRep = 0 +{-# INLINE mkZRep #-} + +mkSRep :: SNatRep -> SNatRep +mkSRep = (1 +) +{-# INLINE mkSRep #-} + +unSRep :: SNatRep -> SNatRep +unSRep = subtract 1 +{-# INLINE unSRep #-} + +elSNatRep :: a -> (SNatRep -> a) -> SNatRep -> a +elSNatRep ifZ ifS n = + assert (isValidSNatRep n) $ + if n == mkZRep + then ifZ + else ifS (unSRep n) +{-# INLINE elSNatRep #-} + +-------------------------------------------------------------------------------- +-- Natural Number Singletons +-------------------------------------------------------------------------------- + +-- | @'SNat' n@ is the singleton type for natural numbers. +type SNat :: Nat -> Type +newtype SNat n = UnsafeSNat {snatRep :: SNatRep} + +type role SNat nominal + +mkZ :: SNat Z +mkZ = UnsafeSNat mkZRep +{-# INLINE mkZ #-} + +mkS :: SNat n -> SNat (S n) +mkS = UnsafeSNat . mkSRep . (.snatRep) +{-# INLINE mkS #-} + +-- | @'SNatF'@ is the base functor of @'SNat'@. +data SNatF (snat :: Nat -> Type) (n :: Nat) where + ZF :: SNatF snat Z + SF :: !(snat n) -> SNatF snat (S n) + +projectSNat :: SNat n -> SNatF SNat n +projectSNat = + elSNatRep (unsafeCoerce ZF) (unsafeCoerce . SF . UnsafeSNat) . (.snatRep) +{-# INLINE projectSNat #-} + +embedSNat :: SNatF SNat n -> SNat n +embedSNat = \case + ZF -> mkZ + SF n -> mkS n +{-# INLINE embedSNat #-} + +pattern Z :: () => (n ~ Z) => SNat n +pattern Z <- (projectSNat -> ZF) where Z = embedSNat ZF +{-# INLINE Z #-} + +pattern S :: () => (Pos n) => SNat (Pred n) -> SNat n +pattern S n <- (projectSNat -> SF n) where S n = embedSNat (SF n) +{-# INLINE S #-} + +{-# COMPLETE Z, S #-} + +instance Eq (SNat n) where + (==) :: SNat n -> SNat n -> Bool + m == n = isJust (decSNat m n) + +instance Show (SNat n) where + showsPrec :: Int -> SNat n -> ShowS + showsPrec p = \case + Z -> showString "Z" + S n -> showParen (p > 10) $ showString "S " . showsPrec 11 n + +deriving newtype instance NFData (SNat n) + +-- | @'fromSNat' n@ returns the numeric representation of 'SNat n'. +fromSNat :: (Integral i) => SNat n -> i +fromSNat = fromInteger . toInteger . (.snatRep) + +-- | @'fromSNatRaw' n@ returns the raw underlying representation of 'SNat n'. +fromSNatRaw :: SNat n -> SNatRep +fromSNatRaw = (.snatRep) + +-- | Addition for natural number singletons. +plus :: SNat n -> SNat m -> SNat (n + m) +n `plus` m = UnsafeSNat (n.snatRep + m.snatRep) + +-- | Decidable equality for natural number singletons. +decSNat :: SNat n -> SNat m -> Maybe (n :~: m) +decSNat n m = + if n.snatRep == m.snatRep + then Just (unsafeCoerce Refl) + else Nothing + +-- | Convert an 'Int' to an 'SNatRep'. +intToSNatRep :: Int -> SNatRep +#ifdef SNAT_AS_WORD8 +-- TODO: Make this safe. +intToSNatRep int + | int < 0 = throw Underflow + | int > fromIntegral (maxBound @Word8) = throw Overflow + | otherwise = fromIntegral @Int @Word8 int +{-# INLINE intToSNatRep #-} +#else +intToSNatRep = id +{-# INLINE intToSNatRep #-} +#endif + +-- | Convert an 'SNatRep' to an 'Int'. +snatRepToInt :: SNatRep -> Int +#ifdef SNAT_AS_WORD8 +snatRepToInt = fromIntegral @Word8 @Int +{-# INLINE snatRepToInt #-} +#else +snatRepToInt = id +{-# INLINE snatRepToInt #-} +#endif + +-------------------------------------------------------------------------------- +-- Existential Wrapper +-------------------------------------------------------------------------------- + +-- | An existential wrapper around natural number singletons. +type SomeSNat :: Type +data SomeSNat = forall (n :: Nat). SomeSNat !(SNat n) + +instance Eq SomeSNat where + (==) :: SomeSNat -> SomeSNat -> Bool + SomeSNat m == SomeSNat n = isJust (decSNat m n) + +deriving instance Show SomeSNat + +instance NFData SomeSNat where + rnf :: SomeSNat -> () + rnf (SomeSNat n) = rnf n + +-- | Evaluate a term with access to the underlying @'SNat'@. +withSomeSNat :: (forall n. SNat n -> a) -> SomeSNat -> a +withSomeSNat action (SomeSNat n) = action n + +{-| @'toSomeSNat' n@ constructs the singleton @'SNat' n@. + +prop> toSomeSNat (fromSomeSNat n) == n +-} +toSomeSNat :: (Integral i) => i -> SomeSNat +toSomeSNat r + | r < 0 = error $ printf "cannot convert %d to natural number singleton" (toInteger r) + | otherwise = SomeSNat (UnsafeSNat (fromIntegral r)) + +{-| @'toSomeSNat' n@ constructs the singleton @'SNat' n@. + +prop> toSomeSNatRaw (fromSomeSNatRaw n) == n +-} +toSomeSNatRaw :: SNatRep -> SomeSNat +toSomeSNatRaw r + | r < 0 = error $ printf "cannot convert %d to natural number singleton" + | otherwise = SomeSNat (UnsafeSNat r) + +-- | @'fromSomeSNat' n@ returns the numeric representation of the wrapped singleton. +fromSomeSNat :: (Integral i) => SomeSNat -> i +fromSomeSNat = withSomeSNat fromSNat + +-- | @'fromSomeSNat' n@ returns the numeric representation of the wrapped singleton. +fromSomeSNatRaw :: SomeSNat -> SNatRep +fromSomeSNatRaw (SomeSNat (UnsafeSNat r)) = r + +-------------------------------------------------------------------------------- +-- Laws +-------------------------------------------------------------------------------- + +plusUnitL :: Proxy n -> Z + n :~: n +plusUnitL _ = Refl + +plusUnitR :: SNat n -> n + Z :~: n +plusUnitR _ = unsafeCoerce Refl + +plusCommS :: SNat n -> Proxy m -> S (n + m) :~: n + S m +plusCommS _ _ = unsafeCoerce Refl + +plusComm :: SNat n -> SNat m -> n + m :~: m + n +plusComm _ _ = unsafeCoerce Refl + +plusAssoc :: SNat n -> Proxy m -> Proxy l -> (n + m) + l :~: n + (m + l) +plusAssoc _ _ _ = unsafeCoerce Refl + +-------------------------------------------------------------------------------- +-- Linking Type-Level and Value-Level +-------------------------------------------------------------------------------- + +type FromNat :: Nat -> GHC.Nat +type family FromNat n where + FromNat Z = 0 + FromNat (S n) = FromNat n GHC.+ 1 + +type KnownNat :: Nat -> Constraint +class KnownNat n where + natSing :: SNat n + +instance KnownNat Z where + natSing :: SNat Z + natSing = Z + +instance (KnownNat n) => KnownNat (S n) where + natSing :: SNat (S n) + natSing = S natSing + +data Dict (c :: Constraint) :: Type where + Dict :: (c) => Dict c + +data FakeKnownNat n = FakeKnownNat (SNat n) +{-# ANN FakeKnownNat ("HLint: ignore Use newtype instead of data" :: String) #-} + +withKnownNat :: SNat n -> ((KnownNat n) => r) -> r +withKnownNat n action = case knownNat n of Dict -> action + where + knownNat :: SNat n -> Dict (KnownNat n) + knownNat = unsafeCoerce . FakeKnownNat diff --git a/src-safe/Data/DeBruijn/Environment/Safe.hs b/src-safe/Data/DeBruijn/Environment/Safe.hs new file mode 100644 --- /dev/null +++ b/src-safe/Data/DeBruijn/Environment/Safe.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE QuantifiedConstraints #-} + +module Data.DeBruijn.Environment.Safe ( + Env (Nil, (:>)), + decEnvLen, + (!), +) where + +import Control.DeepSeq (NFData (..)) +import Data.DeBruijn.Index.Safe (Ix (FS, FZ), isPos) +import Data.Kind (Type) +import Data.Type.Equality ((:~:) (Refl)) +import Data.Type.Nat (type Nat (..)) +import Prelude hiding (lookup) + +-- | @'Env' n@ is the type of environments with @n@ elements. +type Env :: Nat -> Type -> Type +data Env n a where + Nil :: Env Z a + (:>) :: Env n a -> a -> Env (S n) a + +deriving stock instance Functor (Env n) + +deriving stock instance Foldable (Env n) + +deriving stock instance Traversable (Env n) + +decEnvLen :: Env n a -> Env m a -> Maybe (n :~: m) +decEnvLen Nil Nil = Just Refl +decEnvLen (xs :> _x) (ys :> _y) = (\Refl -> Refl) <$> decEnvLen xs ys +decEnvLen _ _ = Nothing + +instance (NFData a) => NFData (Env n a) where + rnf :: Env n a -> () + rnf Nil = () + rnf (xs :> x) = rnf x `seq` rnf xs + +instance (Eq a) => Eq (Env n a) where + (==) :: Env n a -> Env n a -> Bool + Nil == Nil = True + xs :> x == ys :> y = x == y && xs == ys + +deriving instance (Show a) => Show (Env n a) + +(!) :: Env n a -> Ix n -> a +xs ! i = isPos i $ case (xs, i) of + (_ys :> y, FZ) -> y + (ys :> _y, FS j) -> ys ! j diff --git a/src-safe/Data/DeBruijn/Index/Safe.hs b/src-safe/Data/DeBruijn/Index/Safe.hs new file mode 100644 --- /dev/null +++ b/src-safe/Data/DeBruijn/Index/Safe.hs @@ -0,0 +1,176 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.DeBruijn.Index.Safe ( + -- * DeBruijn indices + Ix (FZ, FS), + eqIx, + toSafe, + fromSafe, + fromIx, + fromIxRaw, + isPos, + thin, + thick, + inject, + raise, + + -- * Existential Wrapper + SomeIx (..), + withSomeIx, + toSomeIx, + toSomeIxRaw, + fromSomeIx, + fromSomeIxRaw, + + -- * Specialised target for conversion + IxRep, +) where + +import Control.DeepSeq (NFData (..)) +import Data.DeBruijn.Index.Fast (IxRep) +import Data.DeBruijn.Index.Fast qualified as Fast +import Data.Kind (Type) +import Data.Type.Equality ((:~:) (Refl)) +import Data.Type.Nat (type Nat (..), type Pos, type (+)) +import Data.Type.Nat.Singleton.Safe (SNat (..), SNatRep, SomeSNat (..), decSNat, fromSNat, fromSNatRaw, plusUnitR, toSomeSNat) +import Text.Printf (printf) + +{- $setup +>>> import Data.DeBruijn.Index.Safe.Arbitrary +-} + +-------------------------------------------------------------------------------- +-- DeBruijn Indexes +-------------------------------------------------------------------------------- + +-- | @'Ix' n@ is the type of DeBruijn indices less than @n@. +type Ix :: Nat -> Type +data Ix n where + FZ :: Ix (S n) + FS :: Ix n -> Ix (S n) + +eqIx :: Ix n -> Ix m -> Bool +eqIx FZ FZ = True +eqIx (FS i) (FS j) = eqIx i j +eqIx _ _ = False + +instance Eq (Ix n) where + (==) :: Ix n -> Ix n -> Bool + (==) = eqIx + +instance Show (Ix n) where + showsPrec :: Int -> Ix n -> ShowS + showsPrec p = + showParen (p > 10) . \case + FZ -> showString "FZ" + FS n -> showString "FS " . showsPrec 11 n + +instance NFData (Ix n) where + rnf :: Ix n -> () + rnf FZ = () + rnf (FS i) = rnf i + +-- | Convert from the efficient representation 'Fast.Ix' to the safe representation 'Ix'. +toSafe :: Fast.Ix n -> Ix n +toSafe Fast.FZ = FZ +toSafe (Fast.FS i) = FS (toSafe i) + +-- | Convert from the safe representation 'Ix' to the efficient representation 'Fast.Ix'. +fromSafe :: Ix n -> Fast.Ix n +fromSafe FZ = Fast.FZ +fromSafe (FS i) = Fast.FS (fromSafe i) + +-- | Convert an 'Ix' to 'Word'. +fromIx :: (Integral i) => Ix n -> i +fromIx = \case + FZ -> 0 + FS i -> 1 + fromIx i +{-# SPECIALIZE fromIx :: Ix n -> IxRep #-} + +fromIxRaw :: Ix n -> IxRep +fromIxRaw = fromIx +{-# INLINE fromIxRaw #-} + +-- | If any value of type @'Ix' n@ exists, @n@ must have a predecessor. +isPos :: Ix n -> ((Pos n) => a) -> a +isPos FZ r = r +isPos (FS _) r = r + +-- | Thinning. +thin :: Ix (S n) -> Ix n -> Ix (S n) +thin FZ j = FS j +thin (FS _) FZ = FZ +thin (FS i) (FS j) = FS (thin i j) + +-- | Thickening. +thick :: Ix (S n) -> Ix (S n) -> Maybe (Ix n) +thick FZ FZ = Nothing +thick FZ (FS j) = Just j +thick (FS i) FZ = isPos i $ Just FZ +thick (FS i) (FS j) = isPos i $ FS <$> thick i j + +-- | Inject. +inject :: Ix n -> SNat m -> Ix (n + m) +inject FZ m = case plusUnitR m of Refl -> FZ +inject (FS i) n = FS (inject i n) + +-- | Raise. +raise :: SNat n -> Ix m -> Ix (n + m) +raise Z j = j +raise (S n) j = FS (raise n j) + +-------------------------------------------------------------------------------- +-- Existential Wrapper +-------------------------------------------------------------------------------- + +-- | An existential wrapper around indexes. +type SomeIx :: Type +data SomeIx = forall (n :: Nat). SomeIx + { bound :: !(SNat n) + , index :: !(Ix n) + } + +instance Eq SomeIx where + (==) :: SomeIx -> SomeIx -> Bool + SomeIx n i == SomeIx m j + | Just Refl <- decSNat n m = eqIx i j + | otherwise = False + +deriving instance Show SomeIx + +instance NFData SomeIx where + rnf :: SomeIx -> () + rnf SomeIx{..} = rnf bound `seq` rnf index + +withSomeIx :: (forall n. SNat n -> Ix n -> a) -> SomeIx -> a +withSomeIx action (SomeIx n i) = action n i + +{-| @'toSomeIx' n@ constructs the index @n@ at type @'Ix' n@ from the number @n@. + +prop> toSomeIx (fromSomeIx i) == i +-} +toSomeIx :: (Integral n, Integral i) => (n, i) -> SomeIx +toSomeIx (bound, index) + | index < 0 = error $ printf "index cannot contain negative value, found index %d" (toInteger index) + | bound <= fromIntegral index = error $ printf "bound must be larger than index, found bound %d and index %d" (toInteger bound) (toInteger index) + | bound >= 1, index == 0, SomeSNat n <- toSomeSNat (pred bound) = SomeIx (S n) FZ + | SomeIx n i <- toSomeIx (pred bound, pred index) = SomeIx (S n) (FS i) + +{-| @'toSomeIxRaw' n@ constructs the index @n@ at type @'Ix' n@ from the 'IxRep' @n@. + +prop> toSomeIxRaw (fromSomeIxRaw i) == i +-} +toSomeIxRaw :: (SNatRep, IxRep) -> SomeIx +toSomeIxRaw = toSomeIx + +-- | @'fromSomeSNat' n@ returns the numeric representation of the wrapped index. +fromSomeIx :: (Integral n, Integral i) => SomeIx -> (n, i) +fromSomeIx = withSomeIx (\n i -> (fromSNat n, fromIx i)) + +-- | @'fromSomeSNat' n@ returns the 'IxRep' representation of the wrapped index. +fromSomeIxRaw :: SomeIx -> (SNatRep, IxRep) +fromSomeIxRaw = withSomeIx (\n i -> (fromSNatRaw n, fromIxRaw i)) diff --git a/src-safe/Data/DeBruijn/Thinning/Safe.hs b/src-safe/Data/DeBruijn/Thinning/Safe.hs new file mode 100644 --- /dev/null +++ b/src-safe/Data/DeBruijn/Thinning/Safe.hs @@ -0,0 +1,237 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.DeBruijn.Thinning.Safe ( + -- * Thinnings + (:<=) (KeepAll, KeepOne, DropOne), + toSafe, + fromSafe, + dropAll, + toBools, + fromTh, + fromThRaw, + + -- * Existential Wrapper + SomeTh (..), + fromBools, + toSomeTh, + toSomeThRaw, + fromSomeTh, + fromSomeThRaw, + + -- * The action of thinnings on 'Nat'-indexed types + Thin (..), + + -- * Specialised target for conversion + ThRep, +) where + +import Control.DeepSeq (NFData (..)) +import Data.Bits (Bits (..)) +import Data.DeBruijn.Index.Safe (Ix (..), isPos) +import Data.DeBruijn.Thinning.Fast (ThRep) +import Data.DeBruijn.Thinning.Fast qualified as Fast +import Data.Kind (Constraint, Type) +import Data.Type.Equality (type (:~:) (Refl)) +import Data.Type.Nat (Nat (..), Pos, Pred) +import Data.Type.Nat.Singleton.Fast (SNatRep) +import Data.Type.Nat.Singleton.Safe (SNat (..), SomeSNat (..), decSNat, fromSNat, toSomeSNat) + +-------------------------------------------------------------------------------- +-- Thinnings +-------------------------------------------------------------------------------- + +-- | @n ':<=' m@ is the type of thinnings from @m@ to @n@. +type (:<=) :: Nat -> Nat -> Type +data (:<=) n m where + KeepAll :: n :<= n + KeepOne_ :: n :<= m -> S n :<= S m + DropOne :: n :<= m -> n :<= S m + +keepOne :: n :<= m -> S n :<= S m +keepOne KeepAll = KeepAll +keepOne n'm' = KeepOne_ n'm' + +pattern KeepOne :: () => (Pos n, Pos m) => Pred n :<= Pred m -> n :<= m +pattern KeepOne n'm' <- KeepOne_ n'm' where KeepOne n'm' = keepOne n'm' + +{-# COMPLETE KeepAll, KeepOne, DropOne #-} + +deriving stock instance Eq (n :<= m) + +instance Show (n :<= m) where + showsPrec :: Int -> n :<= m -> ShowS + showsPrec p = + showParen (p > 10) . \case + KeepAll -> showString "KeepAll" + KeepOne n'm' -> showString "KeepOne " . showsPrec 11 n'm' + DropOne nm' -> showString "DropOne " . showsPrec 11 nm' + +instance NFData (n :<= m) where + rnf :: n :<= m -> () + rnf KeepAll = () + rnf (KeepOne n'm') = rnf n'm' + rnf (DropOne nm') = rnf nm' + +-- | Convert from the efficient representation 'Fast.:<=' to the safe representation ':<='. +toSafe :: n Fast.:<= m -> n :<= m +toSafe = \case + Fast.KeepAll -> KeepAll + Fast.KeepOne n'm' -> KeepOne (toSafe n'm') + Fast.DropOne nm' -> DropOne (toSafe nm') + +-- | Convert from the safe representation ':<=' to the efficient representation 'Fast.:<='. +fromSafe :: n :<= m -> n Fast.:<= m +fromSafe = \case + KeepAll -> Fast.KeepAll + KeepOne n'm' -> Fast.KeepOne (fromSafe n'm') + DropOne nm' -> Fast.DropOne (fromSafe nm') + +-- | Drop all entries. +dropAll :: SNat m -> Z :<= m +dropAll Z = KeepAll +dropAll (S m') = DropOne (dropAll m') + +-- | Convert a thinning into a list of booleans. +toBools :: n :<= m -> [Bool] +toBools = \case + KeepAll -> [] + KeepOne n'm' -> False : toBools n'm' + DropOne nm' -> True : toBools nm' + +-- | Convert a thinning into a bit sequence. +fromTh :: (Bits bs) => n :<= m -> bs +fromTh = \case + KeepAll -> zeroBits + KeepOne n'm' -> (`unsafeShiftL` 1) . fromTh $ n'm' + DropOne nm' -> (`setBit` 0) . (`unsafeShiftL` 1) . fromTh $ nm' +{-# SPECIALIZE fromTh :: n :<= m -> ThRep #-} + +fromThRaw :: n :<= m -> ThRep +fromThRaw = fromTh + +-------------------------------------------------------------------------------- +-- Existential Wrapper +-------------------------------------------------------------------------------- + +data SomeTh + = forall n m. + SomeTh + { lower :: SNat n + , upper :: SNat m + , value :: n :<= m + } + +instance Eq SomeTh where + (==) :: SomeTh -> SomeTh -> Bool + SomeTh n1 m1 n1m1 == SomeTh n2 m2 n2m2 + | Just Refl <- decSNat n1 n2 + , Just Refl <- decSNat m1 m2 = + n1m1 == n2m2 + | otherwise = False + +deriving stock instance Show SomeTh + +instance NFData SomeTh where + rnf :: SomeTh -> () + rnf SomeTh{..} = rnf lower `seq` rnf upper `seq` rnf value + +someKeepAll :: SomeSNat -> SomeTh +someKeepAll (SomeSNat bound) = + SomeTh + { lower = bound + , upper = bound + , value = KeepAll + } + +someKeepOne :: SomeTh -> SomeTh +someKeepOne SomeTh{..} = + SomeTh + { lower = S lower + , upper = S upper + , value = KeepOne value + } + +someDropOne :: SomeTh -> SomeTh +someDropOne SomeTh{..} = + SomeTh + { lower = lower + , upper = S upper + , value = DropOne value + } + +fromBools :: SomeSNat -> [Bool] -> SomeTh +fromBools bound = go + where + go [] = someKeepAll bound + go (False : bools) = someKeepOne (go bools) + go (True : bools) = someDropOne (go bools) + +toSomeTh :: (Show i, Show bs, Integral i, Bits bs) => (i, bs) -> SomeTh +toSomeTh (nRep, nmRep) + | nmRep == zeroBits = someKeepAll (toSomeSNat nRep) + | testBit nmRep 0 = someDropOne (toSomeTh (nRep, unsafeShiftR nmRep 1)) + | otherwise = someKeepOne (toSomeTh (nRep - 1, unsafeShiftR nmRep 1)) +{-# SPECIALIZE toSomeTh :: (SNatRep, ThRep) -> SomeTh #-} + +toSomeThRaw :: (SNatRep, ThRep) -> SomeTh +toSomeThRaw = toSomeTh + +withSomeTh :: (forall n m. SNat n -> SNat m -> n :<= m -> r) -> SomeTh -> r +withSomeTh action (SomeTh n m nm) = action n m nm + +fromSomeTh :: (Integral i, Bits bs) => SomeTh -> (i, bs) +fromSomeTh = withSomeTh (\n _m nm -> (fromSNat n, fromTh nm)) +{-# SPECIALIZE fromSomeTh :: SomeTh -> (SNatRep, ThRep) #-} + +fromSomeThRaw :: SomeTh -> (SNatRep, ThRep) +fromSomeThRaw = fromSomeTh + +-------------------------------------------------------------------------------- +-- Thinning Class +-------------------------------------------------------------------------------- + +-- | The actions of thinnings on natural-indexed data types. +type Thin :: (Nat -> Type) -> Constraint +class Thin f where + thin :: n :<= m -> f n -> f m + thick :: n :<= m -> f m -> Maybe (f n) + +instance Thin Ix where + thin :: n :<= m -> Ix n -> Ix m + thin !t !i = isPos i $ + case t of + KeepAll -> i + KeepOne n'm' -> + case i of + FZ -> FZ + FS i' -> FS (thin n'm' i') + DropOne nm' -> FS (thin nm' i) + + thick :: n :<= m -> Ix m -> Maybe (Ix n) + thick KeepAll i = Just i + thick (KeepOne _n'm') FZ = Just FZ + thick (KeepOne n'm') (FS i') = FS <$> thick n'm' i' + thick (DropOne _nm') FZ = Nothing + thick (DropOne nm') (FS i') = thick nm' i' + +instance Thin ((:<=) l) where + thin :: n :<= m -> l :<= n -> l :<= m + thin nm KeepAll = nm + thin KeepAll ln = ln + thin (KeepOne n'm') (KeepOne l'n') = KeepOne (thin n'm' l'n') + thin (KeepOne n'm') (DropOne ln') = DropOne (thin n'm' ln') + thin (DropOne nm') ln = DropOne (thin nm' ln) + + thick :: n :<= m -> l :<= m -> Maybe (l :<= n) + thick KeepAll lm = Just lm + thick (KeepOne n'm') KeepAll = KeepOne <$> thick n'm' KeepAll + thick (KeepOne n'm') (KeepOne l'n') = KeepOne <$> thick n'm' l'n' + thick (KeepOne n'm') (DropOne ln') = DropOne <$> thick n'm' ln' + thick (DropOne _nm') KeepAll = Nothing + thick (DropOne _nm') (KeepOne _l'n') = Nothing + thick (DropOne nm') (DropOne ln') = thick nm' ln' diff --git a/src-safe/Data/Type/Nat/Singleton/Safe.hs b/src-safe/Data/Type/Nat/Singleton/Safe.hs new file mode 100644 --- /dev/null +++ b/src-safe/Data/Type/Nat/Singleton/Safe.hs @@ -0,0 +1,211 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE TypeFamilies #-} + +module Data.Type.Nat.Singleton.Safe ( + -- * Natural Number Singletons + SNat (..), + toSafe, + fromSafe, + fromSNat, + fromSNatRaw, + plus, + decSNat, + + -- * Existential Wrapper + SomeSNat (..), + withSomeSNat, + toSomeSNat, + toSomeSNatRaw, + fromSomeSNat, + fromSomeSNatRaw, + + -- * Laws + plusUnitL, + plusUnitR, + plusCommS, + plusComm, + plusAssoc, + + -- * Linking Type-Level and Value-Level + KnownNat (..), + withKnownNat, + + -- * Specialised target for conversion + SNatRep, +) where + +import Control.DeepSeq (NFData (..)) +import Data.Kind (Constraint, Type) +import Data.Maybe (isJust) +import Data.Proxy (Proxy (..)) +import Data.Type.Equality (type (:~:) (Refl)) +import Data.Type.Equality qualified as Eq +import Data.Type.Nat (Nat (..), type (+)) +import Data.Type.Nat.Singleton.Fast (SNatRep) +import Data.Type.Nat.Singleton.Fast qualified as Fast + +{- $setup +>>> import Data.Type.Nat.Singleton.Safe.Arbitrary +-} + +-------------------------------------------------------------------------------- +-- Natural Number Singletons +-------------------------------------------------------------------------------- + +-- | @'SNat' n@ is the singleton type for natural numbers. +type SNat :: Nat -> Type +data SNat n where + Z :: SNat Z + S :: SNat n -> SNat (S n) + +instance Eq (SNat n) where + (==) :: SNat n -> SNat n -> Bool + m == n = isJust (decSNat m n) + +instance Show (SNat n) where + showsPrec :: Int -> SNat n -> ShowS + showsPrec p = \case + Z -> showString "Z" + S n -> showParen (p > 10) $ showString "S " . showsPrec 11 n + +instance NFData (SNat n) where + rnf :: SNat n -> () + rnf Z = () + rnf (S n) = rnf n + +-- | Convert from the efficient representation 'Fast.SNat' to the safe representation 'SNat'. +toSafe :: Fast.SNat n -> SNat n +toSafe Fast.Z = Z +toSafe (Fast.S n) = S (toSafe n) + +-- | Convert from the safe representation 'SNat' to the efficient representation 'Fast.SNat'. +fromSafe :: SNat n -> Fast.SNat n +fromSafe Z = Fast.Z +fromSafe (S n) = Fast.S (fromSafe n) + +-- | @'fromSNat' n@ returns the numeric representation of 'SNat n'. +fromSNat :: (Integral i) => SNat n -> i +fromSNat Z = 0 +fromSNat (S n') = 1 + fromSNat n' +{-# SPECIALIZE fromSNat :: SNat n -> SNatRep #-} + +fromSNatRaw :: SNat n -> SNatRep +fromSNatRaw = fromSNat +{-# INLINE fromSNatRaw #-} + +-- | Addition for natural number singletons. +plus :: SNat n -> SNat m -> SNat (n + m) +Z `plus` m = m +S n `plus` m = S (n `plus` m) + +-- | Decidable equality for natural number singletons. +decSNat :: SNat m -> SNat n -> Maybe (m :~: n) +decSNat Z Z = Just Refl +decSNat (S m') (S n') = (\Refl -> Refl) <$> decSNat m' n' +decSNat _m _n = Nothing + +-------------------------------------------------------------------------------- +-- Existential Wrapper +-------------------------------------------------------------------------------- + +-- | An existential wrapper around natural number singletons. +type SomeSNat :: Type +data SomeSNat = forall (n :: Nat). SomeSNat !(SNat n) + +instance NFData SomeSNat where + rnf :: SomeSNat -> () + rnf (SomeSNat n) = rnf n + +deriving instance Show SomeSNat + +instance Eq SomeSNat where + (==) :: SomeSNat -> SomeSNat -> Bool + SomeSNat m == SomeSNat n = isJust (decSNat m n) + +-- | Evaluate a term with access to the underlying @'SNat'@. +withSomeSNat :: (forall n. SNat n -> a) -> SomeSNat -> a +withSomeSNat action (SomeSNat n) = action n + +{-| @'toSomeSNat' n@ constructs the singleton @'SNat' n@. + +prop> toSomeSNat (fromSomeSNat n) == n +-} +toSomeSNat :: (Integral i) => i -> SomeSNat +toSomeSNat n = iterate' n (withSomeSNat $ SomeSNat . S) (SomeSNat Z) + +{-| @'toSomeSNat' n@ constructs the singleton @'SNat' n@. + +prop> toSomeSNatRaw (fromSomeSNatRaw n) == n +-} +toSomeSNatRaw :: SNatRep -> SomeSNat +toSomeSNatRaw = toSomeSNat + +-- | @'fromSomeSNat' n@ returns the numeric representation of the wrapped singleton. +fromSomeSNat :: (Integral i) => SomeSNat -> i +fromSomeSNat = withSomeSNat fromSNat + +-- | @'fromSomeSNat' n@ returns the 'SNatRep' representation of the wrapped singleton. +fromSomeSNatRaw :: SomeSNat -> SNatRep +fromSomeSNatRaw = fromSomeSNat + +-------------------------------------------------------------------------------- +-- Laws +-------------------------------------------------------------------------------- + +plusUnitL :: Proxy n -> Z + n :~: n +plusUnitL _ = Refl + +plusUnitR :: SNat n -> n + Z :~: n +plusUnitR Z = Refl +plusUnitR (S n') = + case plusUnitR n' of + Refl -> Refl + +plusCommS :: SNat n -> Proxy m -> S (n + m) :~: n + S m +plusCommS Z _ = Refl +plusCommS (S n') m = Eq.apply Refl (plusCommS n' m) + +plusComm :: SNat n -> SNat m -> n + m :~: m + n +plusComm Z m = Eq.sym (plusUnitR m) +plusComm (S n') m = Eq.apply Refl (plusComm n' m) `Eq.trans` plusCommS m (erase n') + +plusAssoc :: SNat n -> Proxy m -> Proxy l -> (n + m) + l :~: n + (m + l) +plusAssoc Z _m _l = Refl +plusAssoc (S n') m l = Eq.apply Refl (plusAssoc n' m l) + +-------------------------------------------------------------------------------- +-- Linking Type-Level and Value-Level +-------------------------------------------------------------------------------- + +type KnownNat :: Nat -> Constraint +class KnownNat n where + natSing :: SNat n + +instance KnownNat Z where + natSing :: SNat Z + natSing = Z + +instance (KnownNat n) => KnownNat (S n) where + natSing :: SNat (S n) + natSing = S natSing + +withKnownNat :: SNat n -> ((KnownNat n) => r) -> r +withKnownNat Z action = action +withKnownNat (S n) action = withKnownNat n action + +-------------------------------------------------------------------------------- +-- Helper Functions +-------------------------------------------------------------------------------- + +-- | @`erase` x@ erases the content of @x@ to a @`Proxy`@. +erase :: f a -> Proxy a +erase _ = Proxy +{-# INLINE erase #-} + +-- | @`iterate'` i f@ applies @f@ @i@ times. +iterate' :: (Integral i) => i -> (a -> a) -> a -> a +iterate' i f x + | i <= 0 = x + | otherwise = iterate' (i - 1) f $! f x diff --git a/src-typenats/Data/Type/Nat.hs b/src-typenats/Data/Type/Nat.hs new file mode 100644 --- /dev/null +++ b/src-typenats/Data/Type/Nat.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeData #-} +{-# LANGUAGE TypeFamilies #-} + +module Data.Type.Nat ( + type Nat (..), + type (+), + type Pred, + type Pos, + type (<=), +) where + +import Data.Kind (Constraint) + +-- | Type-level natural numbers. +type data Nat = Z | S Nat + +-- | Addition of type-level naturals. +type (+) :: Nat -> Nat -> Nat +type family (+) n m where + Z + m = m + S n + m = S (n + m) + +-- | Predecessor of type-level naturals. +type Pred :: Nat -> Nat +type family Pred n where + Pred (S n) = n + +-- | @'Pos' n@ holds if @n@ is non-zero. +type Pos :: Nat -> Constraint +type Pos (n :: Nat) = n ~ S (Pred n) + +-- | Less-than-or-equal for type-level naturals. +type (<=) :: Nat -> Nat -> Bool +type family (<=) n m where + Z <= m = 'True + S n <= Z = 'False + S n <= S m = n <= m diff --git a/src/Data/DeBruijn/Environment.hs b/src/Data/DeBruijn/Environment.hs new file mode 100644 --- /dev/null +++ b/src/Data/DeBruijn/Environment.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE CPP #-} + +module Data.DeBruijn.Environment ( + -- * Environments + Env (Nil, (:>)), + (!), +) where + +#ifdef EXPORT_SAFE_API +import Data.DeBruijn.Environment.Safe ( + Env (Nil, (:>)), + (!), + ) +#else +import Data.DeBruijn.Environment.Fast ( + Env (Nil, (:>)), + (!), + ) +#endif diff --git a/src/Data/DeBruijn/Index.hs b/src/Data/DeBruijn/Index.hs new file mode 100644 --- /dev/null +++ b/src/Data/DeBruijn/Index.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE CPP #-} + +module Data.DeBruijn.Index ( + -- * DeBruijn Indexes + Ix (FZ, FS), + eqIx, + fromIx, + fromIxRaw, + isPos, + thin, + thick, + inject, + raise, + + -- * Existential Wrapper + SomeIx (..), + withSomeIx, + toSomeIx, + toSomeIxRaw, + fromSomeIx, + fromSomeIxRaw, + + -- * Specialised target for conversion + IxRep, +) where + +#ifdef EXPORT_SAFE_API +import Data.DeBruijn.Index.Safe ( + Ix (FS, FZ), + SomeIx (..), + eqIx, + fromIx, + fromIxRaw, + fromSomeIx, + fromSomeIxRaw, + inject, + isPos, + raise, + thick, + thin, + toSomeIx, + toSomeIxRaw, + withSomeIx, + IxRep, + ) +#else +import Data.DeBruijn.Index.Fast ( + Ix (FS, FZ), + SomeIx (..), + eqIx, + fromIx, + fromIxRaw, + fromSomeIx, + fromSomeIxRaw, + inject, + isPos, + raise, + thick, + thin, + toSomeIx, + toSomeIxRaw, + withSomeIx, + IxRep, + ) +#endif diff --git a/src/Data/DeBruijn/Thinning.hs b/src/Data/DeBruijn/Thinning.hs new file mode 100644 --- /dev/null +++ b/src/Data/DeBruijn/Thinning.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ExplicitNamespaces #-} + +module Data.DeBruijn.Thinning ( + -- * Thinnings + (:<=) (KeepAll, KeepOne, DropOne), + dropAll, + toBools, + fromTh, + fromThRaw, + + -- * Existential Wrapper + SomeTh (..), + fromBools, + toSomeTh, + toSomeThRaw, + + -- * The action of thinnings on 'Nat'-indexed types + Thin (..), + + -- * Specialised target for conversion + ThRep, +) where + +#ifdef EXPORT_SAFE_API +import Data.DeBruijn.Thinning.Safe ( + SomeTh (..), + Thin (..), + dropAll, + toSomeTh, + toSomeThRaw, + fromBools, + toBools, + fromTh, + fromThRaw, + (:<=) (DropOne, KeepAll, KeepOne), + ThRep, + ) +#else +import Data.DeBruijn.Thinning.Fast ( + SomeTh (..), + Thin (..), + dropAll, + toSomeTh, + toSomeThRaw, + fromBools, + toBools, + fromTh, + fromThRaw, + (:<=) (DropOne, KeepAll, KeepOne), + ThRep, + ) +#endif diff --git a/src/Data/Type/Nat/Singleton.hs b/src/Data/Type/Nat/Singleton.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Nat/Singleton.hs @@ -0,0 +1,78 @@ +{-# LANGUAGE CPP #-} + +module Data.Type.Nat.Singleton ( + -- * Natural Number Singletons + SNat (Z, S), + fromSNat, + fromSNatRaw, + plus, + decSNat, + + -- * Existential Wrapper + SomeSNat (..), + withSomeSNat, + toSomeSNat, + toSomeSNatRaw, + fromSomeSNat, + fromSomeSNatRaw, + + -- * Laws + plusUnitL, + plusUnitR, + plusCommS, + plusComm, + plusAssoc, + + -- * Linking Type-Level and Value-Level + KnownNat (..), + withKnownNat, + + -- * Specialised target for conversion + SNatRep, +) where + +#ifdef EXPORT_SAFE_API +import Data.Type.Nat.Singleton.Safe ( + SNat (S, Z), + SomeSNat (..), + plus, + decSNat, + fromSNat, + fromSNatRaw, + fromSomeSNat, + fromSomeSNatRaw, + toSomeSNat, + toSomeSNatRaw, + withSomeSNat, + SNatRep, + KnownNat (..), + withKnownNat, + plusUnitL, + plusUnitR, + plusCommS, + plusComm, + plusAssoc, + ) +#else +import Data.Type.Nat.Singleton.Fast ( + SNat (S, Z), + SomeSNat (..), + plus, + decSNat, + fromSNat, + fromSNatRaw, + fromSomeSNat, + fromSomeSNatRaw, + toSomeSNat, + toSomeSNatRaw, + withSomeSNat, + KnownNat (..), + withKnownNat, + SNatRep, + plusUnitL, + plusUnitR, + plusCommS, + plusComm, + plusAssoc, + ) +#endif