debruijn-safe 0.2 → 0.3

raw patch · 4 files changed

+23/−79 lines, 4 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• debruijn-safe.cabal +1/−1
• src-common/DeBruijn/Ren.hs +19/−75
• src-common/DeBruijn/Sub.hs +2/−2
• src/DeBruijn/RenExtras.hs +1/−1

@@ -1,6 +1,6 @@ cabal-version: 2.4 name:          debruijn-safe-version:       0.2+version:       0.3 license:       BSD-3-Clause license-file:  LICENSE category:      Development

@@ -10,24 +10,18 @@     -- ** Category     idRen,     compRen,-    -- * Applicative renamings-    RenA (..),-    renameIdxA,-    keepRenA,+    -- * Contractions     unusedIdx,     -- * Renameble things-    IdxMapping (..),+    Keep (..),     keepAdd,     Weaken (..),+    Contract (..),     Rename (..),-    RenameA (..),-    defaultRename,-    defaultWeaken, ) where -import Data.Functor.Identity (Identity (..))-import Data.Kind             (Constraint, Type)-import Data.Proxy            (Proxy (..))+import Data.Kind  (Constraint, Type)+import Data.Proxy (Proxy (..))  import DeBruijn.Add import DeBruijn.Ctx@@ -36,8 +30,6 @@ import DeBruijn.Size import DeBruijn.Wk -import TrustworthyCompat (coerce)- ------------------------------------------------------------------------------- -- Renamings -------------------------------------------------------------------------------@@ -88,39 +80,22 @@ -- Applicative renamings ------------------------------------------------------------------------------- -type RenA :: (Type -> Type) -> Ctx -> Ctx -> Type-newtype RenA f ctx ctx' = MkRenA (Env ctx (f (Idx ctx')))---- | Lift renaming (used when going under a binder).-keepRenA :: Applicative f => RenA f ctx ctx' -> RenA f (S ctx) (S ctx')-keepRenA (MkRenA js) = MkRenA (fmap (fmap IS) js :> pure IZ)--unusedIdx :: Size ctx -> RenA Maybe (S ctx) ctx-unusedIdx s = MkRenA $ tabulateEnv (SS s) $ unIdx Nothing Just+unusedIdx :: Wk ctx (S ctx)+unusedIdx = wk1  ------------------------------------------------------------------------------- -- Renameble & RenamebleA ------------------------------------------------------------------------------- --- | 'IdxMapping' generalizes over various index mappings, also effectful ones.-type IdxMapping :: (Type -> Type) -> (Ctx -> Ctx -> Type) -> Constraint-class Applicative f => IdxMapping f t | t -> f where-    -- | 'IdxMapping' action.-    mapIdx :: t ctx ctx' -> Idx ctx -> f (Idx ctx')-+type Keep :: (Ctx -> Ctx -> Type) -> Constraint+class Keep t where     -- | 'keep' is often called @lift@, but we stick with 'Wk' terminology.     -- One benefit is that the name 'keep' is less likely to clash.     keep   :: t ctx ctx' -> t (S ctx) (S ctx') -    -- | Compose weakening with an index mapping.-    ---    -- This is useful when you have explicit weakening in your terms.-    -- (a similar idea as in @bound@'s @Scope@ possibly lifting whole term).-    weakenIdxMapping :: Wk ctx ctx' -> t ctx' ctx'' -> t ctx ctx''- -- | 'keep' 'IdxMapping' @arity@ times. keepAdd-    :: IdxMapping f m+    :: Keep m     => Add arity ctxA ctxA'     -> m ctxA ctxB     -> (forall ctxB'. Add arity ctxB ctxB' -> m ctxA' ctxB' -> r)@@ -128,24 +103,12 @@ keepAdd AZ     w kont = kont AZ w keepAdd (AS a) w kont = keepAdd a w $ \a' w' -> kont (AS a') (keep w') -instance IdxMapping Identity Wk where+instance Keep Wk where     keep = KeepWk-    mapIdx w x = Identity (weakenIdx w x)-    weakenIdxMapping = compWk -instance IdxMapping Identity Ren where+instance Keep Ren where     keep = keepRen-    mapIdx w x = Identity (renameIdx w x)-    weakenIdxMapping w (MkRen is) = MkRen (weakenEnv w is) -instance Applicative f => IdxMapping f (RenA f) where-    keep = keepRenA-    mapIdx = renameIdxA-    weakenIdxMapping w (MkRenA is) = MkRenA (weakenEnv w is)--renameIdxA :: RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')-renameIdxA (MkRenA js) i = lookupEnv i js- -- | Renameble things. -- -- For most terms it's enough to define a single traversal: an instance of 'RenamebleA' type-class,@@ -161,28 +124,9 @@ class Weaken t => Rename t where     rename :: Ren n m -> t n -> t m --- | 'rename' implementation using 'grename'.-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. RenameA t => Wk n m -> t n -> t m-defaultWeaken = coerce (grename @t @Wk @Identity @n @m)---- | Effectful renamings.------ An common example is checking whether a binding is used:------ @--- Just t' <- 'renameA' 'unusedIdx' t--- @----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')+-- | Contractions+class Contract t where+    contract :: Wk m n -> t n -> Maybe (t m)  instance Weaken Proxy where      weaken _ _ = Proxy@@ -190,8 +134,8 @@ instance Rename Proxy where     rename _ _ = Proxy -instance RenameA Proxy where-    grename _ _ = pure Proxy+instance Contract Proxy where+    contract _ _ = Just Proxy  instance Weaken Idx where     weaken = weakenIdx@@ -199,8 +143,8 @@ instance Rename Idx where     rename = renameIdx -instance RenameA Idx where-    grename = mapIdx+instance Contract Idx where+    contract = contractIdx  instance Weaken (Ren n) where     weaken w (MkRen js) = MkRen (fmap (weaken w) js)

@@ -45,7 +45,7 @@ snocSub :: Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx' snocSub (MkSub s) t = MkSub (s :> t) -keepSub :: (Rename t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx')+keepSub :: (Weaken 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 :: Rename t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''+nameMe :: Weaken t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx'' nameMe (MkSub ts) w = MkSub (fmap (weaken w) ts)  -------------------------------------------------------------------------------

@@ -11,7 +11,7 @@ -- | Weaken closed term to arbitrary context. -- -- Note: this has different requirements than 'sinkSize'.-weakenUsingSize :: Rename t => Size ctx -> t EmptyCtx -> t ctx+weakenUsingSize :: Weaken t => Size ctx -> t EmptyCtx -> t ctx weakenUsingSize s0 = weaken (go s0) where     go :: Size ctx -> Wk EmptyCtx ctx     go SZ     = IdWk