packages feed

data-debruijn (empty) → 0.1.0.0

raw patch · 25 files changed

+2796/−0 lines, 25 filesdep +QuickCheckdep +basedep +containers

Dependencies added: QuickCheck, base, containers, data-debruijn, deepseq, ghc-bignum, ghc-prim, skew-list

Files

+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for debruijn++## 0.1.0.0 -- 2025-06-08++- First version.
+ data-debruijn.cabal view
@@ -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
+ src-arbitrary/Data/DeBruijn/Index/Arbitrary.hs view
@@ -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
+ src-arbitrary/Data/DeBruijn/Index/Fast/Arbitrary.hs view
@@ -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]
+ src-arbitrary/Data/DeBruijn/Index/Safe/Arbitrary.hs view
@@ -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]
+ src-arbitrary/Data/DeBruijn/Thinning/Arbitrary.hs view
@@ -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
+ src-arbitrary/Data/DeBruijn/Thinning/Fast/Arbitrary.hs view
@@ -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 #-}
+ src-arbitrary/Data/DeBruijn/Thinning/Safe/Arbitrary.hs view
@@ -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 #-}
+ src-arbitrary/Data/Type/Nat/Singleton/Arbitrary.hs view
@@ -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
+ src-arbitrary/Data/Type/Nat/Singleton/Fast/Arbitrary.hs view
@@ -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
+ src-arbitrary/Data/Type/Nat/Singleton/Safe/Arbitrary.hs view
@@ -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
+ src-arbitrary/Test/QuickCheck/Extra.hs view
@@ -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)
+ src-fast/Data/DeBruijn/Environment/Fast.hs view
@@ -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
+ src-fast/Data/DeBruijn/Index/Fast.hs view
@@ -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)
+ src-fast/Data/DeBruijn/Thinning/Fast.hs view
@@ -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 -}
+ src-fast/Data/Type/Nat/Singleton/Fast.hs view
@@ -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
+ src-safe/Data/DeBruijn/Environment/Safe.hs view
@@ -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
+ src-safe/Data/DeBruijn/Index/Safe.hs view
@@ -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))
+ src-safe/Data/DeBruijn/Thinning/Safe.hs view
@@ -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'
+ src-safe/Data/Type/Nat/Singleton/Safe.hs view
@@ -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
+ src-typenats/Data/Type/Nat.hs view
@@ -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
+ src/Data/DeBruijn/Environment.hs view
@@ -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
+ src/Data/DeBruijn/Index.hs view
@@ -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
+ src/Data/DeBruijn/Thinning.hs view
@@ -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
+ src/Data/Type/Nat/Singleton.hs view
@@ -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