diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,7 @@ +# 0.3.1 + +- Add `zipWithEnv :: (a -> b -> c) -> Env ctx a -> Env ctx b -> Env ctx c` + # 0.3 - Remove RenameA machinery diff --git a/debruijn.cabal b/debruijn.cabal --- a/debruijn.cabal +++ b/debruijn.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: debruijn -version: 0.3 +version: 0.3.1 license: BSD-3-Clause license-file: LICENSE category: Development @@ -14,7 +14,14 @@ author: Oleg Grenrus maintainer: Oleg Grenrus build-type: Simple -tested-with: GHC ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2 || ==9.10.1 +tested-with: + GHC ==9.2.8 + || ==9.4.8 + || ==9.6.7 + || ==9.8.4 + || ==9.10.2 + || ==9.12.2 + extra-doc-files: CHANGELOG.md source-repository head @@ -22,14 +29,38 @@ location: https://github.com/phadej/debruijn.git subdir: debruijn -library +common lang default-language: Haskell2010 ghc-options: -Wall -Wno-unticked-promoted-constructors - hs-source-dirs: src src-common + default-extensions: + BangPatterns + DataKinds + DeriveGeneric + DeriveTraversable + DerivingStrategies + EmptyCase + FlexibleInstances + FunctionalDependencies + GADTs + OverloadedStrings + PatternSynonyms + QuantifiedConstraints + RankNTypes + RoleAnnotations + ScopedTypeVariables + StandaloneDeriving + StandaloneKindSignatures + TypeApplications + TypeOperators + ViewPatterns +library + import: lang + hs-source-dirs: src src-common + -- GHC-boot libraries build-depends: - , base ^>=4.16.3.0 || ^>=4.17.0.0 || ^>=4.18.0.0 || ^>=4.19.0.0 || ^>=4.20.0.0 + , base ^>=4.16.3.0 || ^>=4.17.0.0 || ^>=4.18.0.0 || ^>=4.19.0.0 || ^>=4.20.0.0 || ^>=4.21.0.0 , deepseq ^>=1.4.6.1 || ^>=1.5.0.0 , transformers ^>=0.5.6.2 || ^>=0.6.1.0 @@ -64,24 +95,16 @@ DeBruijn.RenExtras TrustworthyCompat - default-extensions: - BangPatterns - DataKinds - DeriveGeneric - DeriveTraversable - DerivingStrategies - EmptyCase - FlexibleInstances - FunctionalDependencies - GADTs - OverloadedStrings - PatternSynonyms - QuantifiedConstraints - RankNTypes - RoleAnnotations - ScopedTypeVariables - StandaloneDeriving - StandaloneKindSignatures - TypeApplications - TypeOperators - ViewPatterns +test-suite debruijn-tests + import: lang + hs-source-dirs: tests + type: exitcode-stdio-1.0 + main-is: debruijn-tests.hs + build-depends: + , base + , debruijn + + build-depends: + , QuickCheck ^>=2.15.0.1 + , tasty ^>=1.5.3 + , tasty-quickcheck ^>=0.11.1 diff --git a/src/DeBruijn/Env.hs b/src/DeBruijn/Env.hs --- a/src/DeBruijn/Env.hs +++ b/src/DeBruijn/Env.hs @@ -4,6 +4,7 @@ lookupEnv, sizeEnv, tabulateEnv, + zipWithEnv, ) where import DeBruijn.Internal.Env diff --git a/src/DeBruijn/Internal/Env.hs b/src/DeBruijn/Internal/Env.hs --- a/src/DeBruijn/Internal/Env.hs +++ b/src/DeBruijn/Internal/Env.hs @@ -4,6 +4,7 @@ lookupEnv, sizeEnv, tabulateEnv, + zipWithEnv, ) where import Data.Coerce (coerce) @@ -123,3 +124,23 @@ -- tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a tabulateEnv (UnsafeSize s) f = UnsafeEnv $ SL.fromList $ map (coerce f) [0 .. s - 1] + +-- | +-- +-- >>> zipWithEnv (,) (EmptyEnv :> 'a') (EmptyEnv :> True) +-- EmptyEnv :> ('a',True) +-- +-- @since 0.3.1 +zipWithEnv :: (a -> b -> c) -> Env ctx a -> Env ctx b -> Env ctx c +zipWithEnv f (UnsafeEnv xs) (UnsafeEnv ys) = UnsafeEnv (skewListZipWith f xs ys) + +-- Possible TODO: we could be more efficient, keeping the structure of first +-- list and only unconsing the other one. +-- Probably doesn't matter efficiency-wise. +skewListZipWith :: (a -> b -> c) -> SkewList a -> SkewList b -> SkewList c +skewListZipWith f = go where + go xs ys = case SL.uncons xs of + Nothing -> SL.empty + Just (x, xs') -> case SL.uncons ys of + Nothing -> SL.empty + Just (y, ys') -> SL.cons (f x y) (go xs' ys') diff --git a/src/DeBruijn/Internal/Idx.hs b/src/DeBruijn/Internal/Idx.hs --- a/src/DeBruijn/Internal/Idx.hs +++ b/src/DeBruijn/Internal/Idx.hs @@ -35,7 +35,7 @@ type Idx :: Ctx -> Type type role Idx nominal -newtype Idx j = UnsafeIdx { _idxToInt :: Int } +newtype Idx ctx = UnsafeIdx { _idxToInt :: Int } ------------------------------------------------------------------------------- -- Combinators diff --git a/tests/debruijn-tests.hs b/tests/debruijn-tests.hs new file mode 100644 --- /dev/null +++ b/tests/debruijn-tests.hs @@ -0,0 +1,146 @@ +module Main (main) where + +import Test.Tasty (defaultMain, testGroup) +import Numeric.Natural (Natural) +import Test.Tasty.QuickCheck + +import DeBruijn + +main :: IO () +main = defaultMain $ testGroup "debruijn" + [ testProperty "wk-comp" $ + forAllShrink genWkNatural shrinkIntegral $ \n -> + forAllShrink genWkNatural shrinkIntegral $ \m -> + propWkComposition n m + , testProperty "wk-idx" $ + forAllShrink genIdxNatural shrinkIntegral $ \x -> + forAllShrink genWkNatural shrinkIntegral $ \w -> + propWkIdx x w + ] + +genWkNatural :: Gen Natural +genWkNatural = oneof + [ arbitrarySizedNatural + ] + +genIdxNatural :: Gen Natural +genIdxNatural = oneof + [ arbitrarySizedNatural + ] + +------------------------------------------------------------------------------- +-- Some weakening +------------------------------------------------------------------------------- + +data SomeWk where + SomeWk :: Wk n m -> SomeWk + +deriving instance Show SomeWk + +instance Eq SomeWk where + SomeWk w == SomeWk w' = eqWk w w' + +eqWk :: Wk n m -> Wk n' m' -> Bool +eqWk IdWk IdWk = True +eqWk (SkipWk w) (SkipWk w') = eqWk w w' +eqWk (KeepWk w) (KeepWk w') = eqWk w w' +eqWk _ _ = False + +keepSomeWk :: SomeWk -> SomeWk +keepSomeWk (SomeWk w) = SomeWk (KeepWk w) + +skipSomeWk :: SomeWk -> SomeWk +skipSomeWk (SomeWk w) = SomeWk (SkipWk w) + +compSomeWk :: SomeWk -> SomeWk -> SomeWk +compSomeWk w (SomeWk IdWk) = w +compSomeWk w (SomeWk (SkipWk w')) = skipSomeWk (compSomeWk w (SomeWk w')) +compSomeWk (SomeWk IdWk) w'@(SomeWk (KeepWk _)) = w' +compSomeWk (SomeWk (SkipWk w)) (SomeWk (KeepWk w')) = skipSomeWk (compSomeWk (SomeWk w) (SomeWk w')) +compSomeWk (SomeWk (KeepWk w)) (SomeWk (KeepWk w')) = keepSomeWk (compSomeWk (SomeWk w) (SomeWk w')) + +naturalToSomeWk :: Natural -> SomeWk +naturalToSomeWk n + | n <= 0 = SomeWk IdWk + | odd n = skipSomeWk (naturalToSomeWk (n `div` 2)) + | otherwise = keepSomeWk (naturalToSomeWk (n `div` 2)) + +------------------------------------------------------------------------------- +-- Some index +------------------------------------------------------------------------------- + +data SomeIdx where + SomeIdx :: Idx n -> SomeIdx + +deriving instance Show SomeIdx + +instance Eq SomeIdx where + SomeIdx i == SomeIdx j = eqIdx i j + +eqIdx :: Idx n -> Idx m -> Bool +eqIdx IZ IZ = True +eqIdx (IS i) (IS j) = eqIdx i j +eqIdx _ _ = False + +someIS :: SomeIdx -> SomeIdx +someIS (SomeIdx i) = SomeIdx (IS i) + +weakenSomeIdx :: SomeWk -> SomeIdx -> SomeIdx +weakenSomeIdx (SomeWk IdWk) i = i +weakenSomeIdx (SomeWk (SkipWk w)) i = someIS (weakenSomeIdx (SomeWk w) i) +weakenSomeIdx (SomeWk (KeepWk _)) (SomeIdx IZ) = SomeIdx IZ +weakenSomeIdx (SomeWk (KeepWk w)) (SomeIdx (IS i)) = someIS (weakenSomeIdx (SomeWk w) (SomeIdx i)) + +naturalToSomeIdx :: Natural -> SomeIdx +naturalToSomeIdx n + | n <= 0 = SomeIdx IZ + | otherwise = someIS (naturalToSomeIdx (n - 1)) + +------------------------------------------------------------------------------- +-- Composition of two weakenings +------------------------------------------------------------------------------- + +-- compatible pair of weakenings +data PairWk where + PairWk :: Wk n m -> Wk m p -> PairWk + +pairSomeWk :: SomeWk -> SomeWk -> PairWk +pairSomeWk (SomeWk w) (SomeWk w') = pairSomeWk' w w' + +pairSomeWk' :: Wk n m -> Wk p q -> PairWk +pairSomeWk' w IdWk = PairWk w IdWk +pairSomeWk' w (SkipWk w') = case pairSomeWk' w w' of PairWk u u' -> PairWk u (SkipWk u') +pairSomeWk' IdWk (KeepWk w') = PairWk IdWk (KeepWk w') +pairSomeWk' (SkipWk w) (KeepWk w') = case pairSomeWk' w w' of PairWk u u' -> PairWk (SkipWk u) (KeepWk u') +pairSomeWk' (KeepWk w) (KeepWk w') = case pairSomeWk' w w' of PairWk u u' -> PairWk (KeepWk u) (KeepWk u') + +propWkComposition :: Natural -> Natural -> Property +propWkComposition n n' = compSomeWk w w' === case pairSomeWk w w' of + PairWk u u' -> SomeWk (compWk u u') + where + w = naturalToSomeWk n + w' = naturalToSomeWk n' + +------------------------------------------------------------------------------- +-- Weakening of an index +------------------------------------------------------------------------------- + +-- compatible weakening and index +data SomeIdxWk where + SomeIdxWk :: Wk ctx ctx' -> Idx ctx -> SomeIdxWk + +someIdxWk :: SomeWk -> SomeIdx -> SomeIdxWk +someIdxWk (SomeWk w) (SomeIdx x) = someIdxWk' w x + +someIdxWk' :: Wk n m -> Idx p -> SomeIdxWk +someIdxWk' IdWk i = SomeIdxWk IdWk i +someIdxWk' (SkipWk w) i = case someIdxWk' w i of SomeIdxWk w' i' -> SomeIdxWk (SkipWk w') i' +someIdxWk' (KeepWk w) IZ = SomeIdxWk (KeepWk w) IZ +someIdxWk' (KeepWk w) (IS i) = case someIdxWk' w i of SomeIdxWk w' i' -> SomeIdxWk (KeepWk w') (IS i') + +propWkIdx :: Natural -> Natural -> Property +propWkIdx x w = weakenSomeIdx w' x' === case someIdxWk w' x' of + SomeIdxWk w'' x'' -> SomeIdx (weakenIdx w'' x'') + where + x' = naturalToSomeIdx x + w' = naturalToSomeWk w