debruijn 0.1 → 0.2

raw patch · 5 files changed

+68/−29 lines, 5 filesdep ~basedep ~findep ~somePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, fin, some

API changes (from Hackage documentation)

Files

• debruijn.cabal +5/−5
• src-common/DeBruijn/Ren.hs +30/−21
• src-common/DeBruijn/Sub.hs +2/−2
• src-common/DeBruijn/Wk.hs +30/−0
• src/DeBruijn/RenExtras.hs +1/−1

@@ -1,6 +1,6 @@ cabal-version: 2.4 name:          debruijn-version:       0.1+version:       0.2 license:       BSD-3-Clause license-file:  LICENSE category:      Development@@ -14,7 +14,7 @@ author:        Oleg Grenrus <oleg.grenrus@iki.fi> maintainer:    Oleg Grenrus <oleg.grenrus@iki.fi> 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@@ -28,15 +28,15 @@    -- 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     , transformers  ^>=0.5.6.2  || ^>=0.6.1.0    -- rest of the dependencies   build-depends:-    , fin        ^>=0.3+    , fin        ^>=0.3.1     , skew-list  ^>=0.1-    , some       ^>=1.0.5+    , some       ^>=1.0.6    exposed-modules:     DeBruijn

@@ -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

@@ -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)  -------------------------------------------------------------------------------

@@ -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'

@@ -12,5 +12,5 @@ -- | 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 _ = unsafeCoerce