diff --git a/debruijn-safe.cabal b/debruijn-safe.cabal --- a/debruijn-safe.cabal +++ b/debruijn-safe.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: debruijn-safe -version: 0.1 +version: 0.2 license: BSD-3-Clause license-file: LICENSE category: Development @@ -13,7 +13,7 @@ author: Oleg Grenrus maintainer: Oleg Grenrus build-type: Simple -tested-with: GHC ==9.2.8 || ==9.4.8 || ==9.6.4 || ==9.8.1 +tested-with: GHC ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2 || ==9.10.1 source-repository head type: git @@ -27,13 +27,13 @@ -- GHC-boot libraries build-depends: - , base ^>=4.16.3.0 || ^>=4.17.0.0 || ^>=4.18.0.0 || ^>=4.19.0.0 + , base ^>=4.16.3.0 || ^>=4.17.0.0 || ^>=4.18.0.0 || ^>=4.19.0.0 || ^>=4.20.0.0 , deepseq ^>=1.4.6.1 || ^>=1.5.0.0 -- rest of the dependencies build-depends: - , fin ^>=0.3 - , some ^>=1.0.5 + , fin ^>=0.3.1 + , some ^>=1.0.6 exposed-modules: DeBruijn diff --git a/src-common/DeBruijn/Ren.hs b/src-common/DeBruijn/Ren.hs --- a/src-common/DeBruijn/Ren.hs +++ b/src-common/DeBruijn/Ren.hs @@ -15,11 +15,12 @@ renameIdxA, keepRenA, unusedIdx, - -- * Renamable things + -- * Renameble things IdxMapping (..), keepAdd, - Renamable (..), - RenamableA (..), + Weaken (..), + Rename (..), + RenameA (..), defaultRename, defaultWeaken, ) where @@ -98,7 +99,7 @@ unusedIdx s = MkRenA $ tabulateEnv (SS s) $ unIdx Nothing Just ------------------------------------------------------------------------------- --- Renamable & RenamableA +-- Renameble & RenamebleA ------------------------------------------------------------------------------- -- | 'IdxMapping' generalizes over various index mappings, also effectful ones. @@ -145,25 +146,27 @@ renameIdxA :: RenA f ctx ctx' -> Idx ctx -> f (Idx ctx') renameIdxA (MkRenA js) i = lookupEnv i js --- | Renamable things. +-- | Renameble things. -- --- For most terms it's enough to define a single traversal: an instance of 'RenamableA' type-class, --- and then define 'Renamable' as: +-- For most terms it's enough to define a single traversal: an instance of 'RenamebleA' type-class, +-- and then define 'Renameble' as: -- -- @ --- instance 'Renamable' Term where 'rename' = 'defaultRename'; 'weaken' = 'defaultWeaken' +-- instance 'Renameble' Term where 'rename' = 'defaultRename'; 'weaken' = 'defaultWeaken' -- @ -- -class Renamable t where - rename :: Ren n m -> t n -> t m +class Weaken t where weaken :: Wk n m -> t n -> t m +class Weaken t => Rename t where + rename :: Ren n m -> t n -> t m + -- | 'rename' implementation using 'grename'. -defaultRename :: forall t n m. RenamableA t => Ren n m -> t n -> t m +defaultRename :: forall t n m. RenameA t => Ren n m -> t n -> t m defaultRename = coerce (grename @t @Ren @Identity @n @m) -- | 'weaken' implementation using 'grename'. -defaultWeaken :: forall t n m. RenamableA t => Wk n m -> t n -> t m +defaultWeaken :: forall t n m. RenameA t => Wk n m -> t n -> t m defaultWeaken = coerce (grename @t @Wk @Identity @n @m) -- | Effectful renamings. @@ -174,27 +177,33 @@ -- Just t' <- 'renameA' 'unusedIdx' t -- @ -- -class Renamable t => RenamableA t where +class Rename t => RenameA t where renameA :: forall f ctx ctx'. Applicative f => RenA f ctx ctx' -> t ctx -> f (t ctx') renameA = grename -- | Generic renaming of a term @t@ using any 'IdxMapping'. grename :: forall m f ctx ctx'. IdxMapping f m => m ctx ctx' -> t ctx -> f (t ctx') -instance Renamable Proxy where +instance Weaken Proxy where + weaken _ _ = Proxy + +instance Rename Proxy where rename _ _ = Proxy - weaken _ _ = Proxy -instance RenamableA Proxy where +instance RenameA Proxy where grename _ _ = pure Proxy -instance Renamable Idx where - rename = renameIdx +instance Weaken Idx where weaken = weakenIdx -instance RenamableA Idx where +instance Rename Idx where + rename = renameIdx + +instance RenameA Idx where grename = mapIdx -instance Renamable (Ren n) where - rename r r' = compRen r' r +instance Weaken (Ren n) where weaken w (MkRen js) = MkRen (fmap (weaken w) js) + +instance Rename (Ren n) where + rename r r' = compRen r' r diff --git a/src-common/DeBruijn/Sub.hs b/src-common/DeBruijn/Sub.hs --- a/src-common/DeBruijn/Sub.hs +++ b/src-common/DeBruijn/Sub.hs @@ -45,7 +45,7 @@ snocSub :: Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx' snocSub (MkSub s) t = MkSub (s :> t) -keepSub :: (Renamable t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx') +keepSub :: (Rename t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx') keepSub (MkSub ts) = MkSub (fmap (weaken wk1) ts :> var IZ) -- | Precompose 'Sub' with weakening. @@ -53,7 +53,7 @@ weakenSub w (MkSub ts) = MkSub (weakenEnv w ts) -- TODO: -nameMe :: Renamable t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx'' +nameMe :: Rename t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx'' nameMe (MkSub ts) w = MkSub (fmap (weaken w) ts) ------------------------------------------------------------------------------- diff --git a/src-common/DeBruijn/Wk.hs b/src-common/DeBruijn/Wk.hs --- a/src-common/DeBruijn/Wk.hs +++ b/src-common/DeBruijn/Wk.hs @@ -6,6 +6,7 @@ compWk, -- * Index weakening weakenIdx, + contractIdx, -- * Size weakening weakenSize, contractSize, @@ -133,6 +134,12 @@ compWk1 (KeepWk1 w) (KeepWk1 w') = KeepWk1 (compWk1 w w') -- | Weaken 'Idx', i.e. map index from smaller to larger context. +-- +-- >>> IS IZ +-- 1 +-- +-- >>> weakenIdx wk1 (IS IZ) +-- 2 weakenIdx :: Wk ctx ctx' -> Idx ctx -> Idx ctx' weakenIdx IdWk x = x weakenIdx (NeWk w) x = weaken1Idx w x @@ -142,6 +149,29 @@ weaken1Idx (SkipWk1 w) x = IS (weaken1Idx w x) weaken1Idx (KeepWk1 _) IZ = IZ weaken1Idx (KeepWk1 w) (IS x) = IS (weaken1Idx w x) + +-- | Contract 'Idx', i.e. map index from larger to smaller context. +-- +-- >>> contractIdx wk1 (IS IZ) +-- Just 0 +-- +-- >>> contractIdx wk1 IZ +-- Nothing +-- +-- >>> contractIdx (SkipWk (KeepWk wk1)) <$> [IZ, IS IZ, IS (IS IZ), IS (IS IZ), IS (IS (IS IZ)), IS (IS (IS (IS IZ)))] +-- [Nothing,Just 0,Nothing,Nothing,Just 1,Just 2] +-- +contractIdx :: Wk ctx ctx' -> Idx ctx' -> Maybe (Idx ctx) +contractIdx IdWk x = Just x +contractIdx (NeWk w) x = contract1Idx w x + +contract1Idx :: Wk1 ctx ctx' -> Idx ctx' -> Maybe (Idx ctx) +contract1Idx Wk1 IZ = Nothing +contract1Idx Wk1 (IS x) = Just x +contract1Idx (SkipWk1 _) IZ = Nothing +contract1Idx (SkipWk1 w) (IS x) = contract1Idx w x +contract1Idx (KeepWk1 _) IZ = Just IZ +contract1Idx (KeepWk1 w) (IS x) = IS <$> contract1Idx w x -- | Weaken 'Size'. weakenSize :: Wk ctx ctx' -> Size ctx -> Size ctx' diff --git a/src/DeBruijn/RenExtras.hs b/src/DeBruijn/RenExtras.hs --- a/src/DeBruijn/RenExtras.hs +++ b/src/DeBruijn/RenExtras.hs @@ -11,7 +11,7 @@ -- | Weaken closed term to arbitrary context. -- -- Note: this has different requirements than 'sinkSize'. -weakenUsingSize :: Renamable t => Size ctx -> t EmptyCtx -> t ctx +weakenUsingSize :: Rename t => Size ctx -> t EmptyCtx -> t ctx weakenUsingSize s0 = weaken (go s0) where go :: Size ctx -> Wk EmptyCtx ctx go SZ = IdWk