debruijn-safe 0.3 → 0.3.1
raw patch · 4 files changed
+41/−13 lines, 4 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- DeBruijn.Idx: instance GHC.Classes.Eq (DeBruijn.Idx.Idx n)
- DeBruijn.Idx: instance GHC.Classes.Ord (DeBruijn.Idx.Idx n)
- DeBruijn.Lvl: sinkLvl :: Lvl ctx -> Lvl (S ctx)
+ DeBruijn.Env: zipWithEnv :: forall a b c (ctx :: Ctx). (a -> b -> c) -> Env ctx a -> Env ctx b -> Env ctx c
+ DeBruijn.Idx: instance GHC.Classes.Eq (DeBruijn.Idx.Idx ctx)
+ DeBruijn.Idx: instance GHC.Classes.Ord (DeBruijn.Idx.Idx ctx)
+ DeBruijn.Lvl: idxToLvl :: forall (ctx :: Ctx). Size ctx -> Idx ctx -> Lvl ctx
- DeBruijn: weakenUsingSize :: Weaken t => Size ctx -> t EmptyCtx -> t ctx
+ DeBruijn: weakenUsingSize :: forall t (ctx :: Ctx). Weaken t => Size ctx -> t EmptyCtx -> t ctx
- DeBruijn.Add: [AS] :: !Add n ctx ctx' -> Add (S n) ctx (S ctx')
+ DeBruijn.Add: [AS] :: forall (n1 :: Ctx) (m :: Ctx) (ctx' :: Ctx). !Add n1 m ctx' -> Add ('S n1) m ('S ctx')
- DeBruijn.Add: [AZ] :: Add EmptyCtx ctx ctx
+ DeBruijn.Add: [AZ] :: forall (m :: Ctx). Add 'Z m m
- DeBruijn.Add: addToInt :: Add n m p -> Int
+ DeBruijn.Add: addToInt :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int
- DeBruijn.Add: addToSize :: Add n m p -> Size n
+ DeBruijn.Add: addToSize :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Size n
- DeBruijn.Add: adding :: Size n -> Some (Add n ctx)
+ DeBruijn.Add: adding :: forall (n :: Ctx) (ctx :: Ctx). Size n -> Some (Add n ctx)
- DeBruijn.Add: data Add n m p
+ DeBruijn.Add: data Add (n :: Ctx) (m :: Ctx) (p :: Ctx)
- DeBruijn.Add: lsuccAdd :: Add n m p -> Add (S n) m (S p)
+ DeBruijn.Add: lsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Add (S n) m (S p)
- DeBruijn.Add: lzeroAdd :: Size n -> Add EmptyCtx n n
+ DeBruijn.Add: lzeroAdd :: forall (n :: Ctx). Size n -> Add EmptyCtx n n
- DeBruijn.Add: rsuccAdd :: Add n m p -> Add n (S m) (S p)
+ DeBruijn.Add: rsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Add n (S m) (S p)
- DeBruijn.Add: rzeroAdd :: Size n -> Add n EmptyCtx n
+ DeBruijn.Add: rzeroAdd :: forall (n :: Ctx). Size n -> Add n EmptyCtx n
- DeBruijn.Add: swapAdd :: Add n (S m) p -> Add (S n) m p
+ DeBruijn.Add: swapAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n (S m) p -> Add (S n) m p
- DeBruijn.Add: unlsuccAdd :: Add (S n) m (S p) -> Add n m p
+ DeBruijn.Add: unlsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add (S n) m (S p) -> Add n m p
- DeBruijn.Add: unlzeroAdd :: Add EmptyCtx n m -> n :~: m
+ DeBruijn.Add: unlzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add EmptyCtx n m -> n :~: m
- DeBruijn.Add: unrsuccAdd :: Add n (S m) (S p) -> Add n m p
+ DeBruijn.Add: unrsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n (S m) (S p) -> Add n m p
- DeBruijn.Add: unrzeroAdd :: Add n EmptyCtx m -> n :~: m
+ DeBruijn.Add: unrzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add n EmptyCtx m -> n :~: m
- DeBruijn.Add: unswapAdd :: Add (S n) m p -> Add n (S m) p
+ DeBruijn.Add: unswapAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add (S n) m p -> Add n (S m) p
- DeBruijn.Ctx: type EmptyCtx = Z
+ DeBruijn.Ctx: type EmptyCtx = 'Z
- DeBruijn.Env: [:>] :: Env ctx a -> a -> Env (S ctx) a
+ DeBruijn.Env: [:>] :: forall (ctx1 :: Ctx) a. Env ctx1 a -> a -> Env ('S ctx1) a
- DeBruijn.Env: [EmptyEnv] :: Env EmptyCtx a
+ DeBruijn.Env: [EmptyEnv] :: forall a. Env 'Z a
- DeBruijn.Env: data Env ctx a
+ DeBruijn.Env: data Env (ctx :: Ctx) a
- DeBruijn.Env: lookupEnv :: Idx ctx -> Env ctx a -> a
+ DeBruijn.Env: lookupEnv :: forall (ctx :: Ctx) a. Idx ctx -> Env ctx a -> a
- DeBruijn.Env: sizeEnv :: Env n a -> Size n
+ DeBruijn.Env: sizeEnv :: forall (n :: Ctx) a. Env n a -> Size n
- DeBruijn.Env: tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a
+ DeBruijn.Env: tabulateEnv :: forall (ctx :: Ctx) a. Size ctx -> (Idx ctx -> a) -> Env ctx a
- DeBruijn.Idx: [IS] :: !Idx n -> Idx (S n)
+ DeBruijn.Idx: [IS] :: forall (ctx1 :: Ctx). !Idx ctx1 -> Idx ('S ctx1)
- DeBruijn.Idx: [IZ] :: Idx (S n)
+ DeBruijn.Idx: [IZ] :: forall (ctx1 :: Ctx). Idx ('S ctx1)
- DeBruijn.Idx: data Idx n
+ DeBruijn.Idx: data Idx (ctx :: Ctx)
- DeBruijn.Idx: idxToInt :: Idx n -> Int
+ DeBruijn.Idx: idxToInt :: forall (ctx :: Ctx). Idx ctx -> Int
- DeBruijn.Idx: pattern I9 :: () => m ~ S (S (S (S (S (S (S (S (S (S n))))))))) => Idx m
+ DeBruijn.Idx: pattern I9 :: forall m (n :: Ctx). () => m ~ S (S (S (S (S (S (S (S (S (S n))))))))) => Idx m
- DeBruijn.Idx: unIdx :: a -> (Idx n -> a) -> Idx (S n) -> a
+ DeBruijn.Idx: unIdx :: forall a (n :: Ctx). a -> (Idx n -> a) -> Idx (S n) -> a
- DeBruijn.Lte: [LS] :: !Lte ctx ctx' -> Lte ctx (S ctx')
+ DeBruijn.Lte: [LS] :: forall (ctx :: Ctx) (ctx'1 :: Ctx). !Lte ctx ctx'1 -> Lte ctx ('S ctx'1)
- DeBruijn.Lte: [LZ] :: Lte ctx ctx
+ DeBruijn.Lte: [LZ] :: forall (ctx :: Ctx). Lte ctx ctx
- DeBruijn.Lte: data Lte ctx ctx'
+ DeBruijn.Lte: data Lte (ctx :: Ctx) (ctx' :: Ctx)
- DeBruijn.Lvl: class Sinkable t
+ DeBruijn.Lvl: class Sinkable (t :: Ctx -> Type)
- DeBruijn.Lvl: data Lvl ctx
+ DeBruijn.Lvl: data Lvl (ctx :: Ctx)
- DeBruijn.Lvl: lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx
+ DeBruijn.Lvl: lvlToIdx :: forall (ctx :: Ctx). Size ctx -> Lvl ctx -> Idx ctx
- DeBruijn.Lvl: lvlZ :: Size ctx -> Lvl (S ctx)
+ DeBruijn.Lvl: lvlZ :: forall (ctx :: Ctx). Size ctx -> Lvl (S ctx)
- DeBruijn.Lvl: mapLvl :: Sinkable t => Lte ctx ctx' -> t ctx -> t ctx'
+ DeBruijn.Lvl: mapLvl :: forall (ctx :: Ctx) (ctx' :: Ctx). Sinkable t => Lte ctx ctx' -> t ctx -> t ctx'
- DeBruijn.Lvl: mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))
+ DeBruijn.Lvl: mapSink :: forall f t (ctx :: Ctx). (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))
- DeBruijn.Lvl: mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')
+ DeBruijn.Lvl: mapSinkAdd :: forall f t (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx). (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')
- DeBruijn.Lvl: mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)
+ DeBruijn.Lvl: mapSinkSize :: forall f t (ctx :: Ctx). (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)
- DeBruijn.Lvl: sink :: Sinkable t => t ctx -> t (S ctx)
+ DeBruijn.Lvl: sink :: forall t (ctx :: Ctx). Sinkable t => t ctx -> t (S ctx)
- DeBruijn.Lvl: sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'
+ DeBruijn.Lvl: sinkAdd :: forall t (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx). Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'
- DeBruijn.Lvl: sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx
+ DeBruijn.Lvl: sinkSize :: forall t (ctx :: Ctx). Sinkable t => Size ctx -> t EmptyCtx -> t ctx
- DeBruijn.Ren: MkRen :: Env ctx (Idx ctx') -> Ren ctx ctx'
+ DeBruijn.Ren: MkRen :: Env ctx (Idx ctx') -> Ren (ctx :: Ctx) (ctx' :: Ctx)
- DeBruijn.Ren: absurdRen :: Ren EmptyCtx ctx
+ DeBruijn.Ren: absurdRen :: forall (ctx :: Ctx). Ren EmptyCtx ctx
- DeBruijn.Ren: class Contract t
+ DeBruijn.Ren: class Contract (t :: Ctx -> Type)
- DeBruijn.Ren: class Keep t
+ DeBruijn.Ren: class Keep (t :: Ctx -> Ctx -> Type)
- DeBruijn.Ren: class Weaken t => Rename t
+ DeBruijn.Ren: class Weaken t => Rename (t :: Ctx -> Type)
- DeBruijn.Ren: class Weaken t
+ DeBruijn.Ren: class Weaken (t :: Ctx -> Type)
- DeBruijn.Ren: compRen :: Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''
+ DeBruijn.Ren: compRen :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''
- DeBruijn.Ren: contract :: Contract t => Wk m n -> t n -> Maybe (t m)
+ DeBruijn.Ren: contract :: forall (m :: Ctx) (n :: Ctx). Contract t => Wk m n -> t n -> Maybe (t m)
- DeBruijn.Ren: idRen :: Size ctx -> Ren ctx ctx
+ DeBruijn.Ren: idRen :: forall (ctx :: Ctx). Size ctx -> Ren ctx ctx
- DeBruijn.Ren: keep :: Keep t => t ctx ctx' -> t (S ctx) (S ctx')
+ DeBruijn.Ren: keep :: forall (ctx :: Ctx) (ctx' :: Ctx). Keep t => t ctx ctx' -> t (S ctx) (S ctx')
- DeBruijn.Ren: keepAdd :: Keep m => Add arity ctxA ctxA' -> m ctxA ctxB -> (forall ctxB'. Add arity ctxB ctxB' -> m ctxA' ctxB' -> r) -> r
+ DeBruijn.Ren: keepAdd :: forall m (arity :: Ctx) (ctxA :: Ctx) (ctxA' :: Ctx) (ctxB :: Ctx) r. Keep m => Add arity ctxA ctxA' -> m ctxA ctxB -> (forall (ctxB' :: Ctx). () => Add arity ctxB ctxB' -> m ctxA' ctxB' -> r) -> r
- DeBruijn.Ren: keepRen :: Ren ctx ctx' -> Ren (S ctx) (S ctx')
+ DeBruijn.Ren: keepRen :: forall (ctx :: Ctx) (ctx' :: Ctx). Ren ctx ctx' -> Ren (S ctx) (S ctx')
- DeBruijn.Ren: newtype Ren ctx ctx'
+ DeBruijn.Ren: newtype Ren (ctx :: Ctx) (ctx' :: Ctx)
- DeBruijn.Ren: rename :: Rename t => Ren n m -> t n -> t m
+ DeBruijn.Ren: rename :: forall (n :: Ctx) (m :: Ctx). Rename t => Ren n m -> t n -> t m
- DeBruijn.Ren: renameIdx :: Ren ctx ctx' -> Idx ctx -> Idx ctx'
+ DeBruijn.Ren: renameIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). Ren ctx ctx' -> Idx ctx -> Idx ctx'
- DeBruijn.Ren: skipRen :: Ren ctx ctx' -> Ren ctx (S ctx')
+ DeBruijn.Ren: skipRen :: forall (ctx :: Ctx) (ctx' :: Ctx). Ren ctx ctx' -> Ren ctx (S ctx')
- DeBruijn.Ren: unusedIdx :: Wk ctx (S ctx)
+ DeBruijn.Ren: unusedIdx :: forall (ctx :: Ctx). Wk ctx (S ctx)
- DeBruijn.Ren: weaken :: Weaken t => Wk n m -> t n -> t m
+ DeBruijn.Ren: weaken :: forall (n :: Ctx) (m :: Ctx). Weaken t => Wk n m -> t n -> t m
- DeBruijn.Ren: wkToRen :: Size ctx -> Wk ctx ctx' -> Ren ctx ctx'
+ DeBruijn.Ren: wkToRen :: forall (ctx :: Ctx) (ctx' :: Ctx). Size ctx -> Wk ctx ctx' -> Ren ctx ctx'
- DeBruijn.Size: [SS] :: !Size ctx -> Size (S ctx)
+ DeBruijn.Size: [SS] :: forall (ctx1 :: Ctx). !Size ctx1 -> Size ('S ctx1)
- DeBruijn.Size: [SZ] :: Size EmptyCtx
+ DeBruijn.Size: [SZ] :: Size 'Z
- DeBruijn.Size: data Size ctx
+ DeBruijn.Size: data Size (ctx :: Ctx)
- DeBruijn.Size: sizeToInt :: Size ctx -> Int
+ DeBruijn.Size: sizeToInt :: forall (ctx :: Ctx). Size ctx -> Int
- DeBruijn.Size: unSS :: Size (S ctx) -> Size ctx
+ DeBruijn.Size: unSS :: forall (ctx :: Ctx). Size (S ctx) -> Size ctx
- DeBruijn.Sub: MkSub :: Env ctx (t ctx') -> Sub t ctx ctx'
+ DeBruijn.Sub: MkSub :: Env ctx (t ctx') -> Sub (t :: Ctx -> Type) (ctx :: Ctx) (ctx' :: Ctx)
- DeBruijn.Sub: class Var t => Subst t
+ DeBruijn.Sub: class Var t => Subst (t :: Ctx -> Type)
- DeBruijn.Sub: class Var t
+ DeBruijn.Sub: class Var (t :: Ctx -> Type)
- DeBruijn.Sub: compSub :: Subst t => Sub t ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''
+ DeBruijn.Sub: compSub :: forall (t :: Ctx -> Type) (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Subst t => Sub t ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''
- DeBruijn.Sub: emptySub :: Sub t EmptyCtx ctx'
+ DeBruijn.Sub: emptySub :: forall (t :: Ctx -> Type) (ctx' :: Ctx). Sub t EmptyCtx ctx'
- DeBruijn.Sub: idSub :: Var t => Size ctx -> Sub t ctx ctx
+ DeBruijn.Sub: idSub :: forall (t :: Ctx -> Type) (ctx :: Ctx). Var t => Size ctx -> Sub t ctx ctx
- DeBruijn.Sub: keepSub :: (Weaken t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx')
+ DeBruijn.Sub: keepSub :: forall (t :: Ctx -> Type) (ctx :: Ctx) (ctx' :: Ctx). (Weaken t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx')
- DeBruijn.Sub: nameMe :: Weaken t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''
+ DeBruijn.Sub: nameMe :: forall (t :: Ctx -> Type) (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx). Weaken t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''
- DeBruijn.Sub: newtype Sub t ctx ctx'
+ DeBruijn.Sub: newtype Sub (t :: Ctx -> Type) (ctx :: Ctx) (ctx' :: Ctx)
- DeBruijn.Sub: snocSub :: Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx'
+ DeBruijn.Sub: snocSub :: forall t (ctx :: Ctx) (ctx' :: Ctx). Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx'
- DeBruijn.Sub: subst :: Subst t => Sub t ctx ctx' -> t ctx -> t ctx'
+ DeBruijn.Sub: subst :: forall (ctx :: Ctx) (ctx' :: Ctx). Subst t => Sub t ctx ctx' -> t ctx -> t ctx'
- DeBruijn.Sub: substIdx :: Sub t ctx ctx' -> Idx ctx -> t ctx'
+ DeBruijn.Sub: substIdx :: forall t (ctx :: Ctx) (ctx' :: Ctx). Sub t ctx ctx' -> Idx ctx -> t ctx'
- DeBruijn.Sub: unSub :: Sub t ctx ctx' -> Env ctx (t ctx')
+ DeBruijn.Sub: unSub :: forall t (ctx :: Ctx) (ctx' :: Ctx). Sub t ctx ctx' -> Env ctx (t ctx')
- DeBruijn.Sub: var :: Var t => Idx ctx -> t ctx
+ DeBruijn.Sub: var :: forall (ctx :: Ctx). Var t => Idx ctx -> t ctx
- DeBruijn.Sub: weakenSub :: Wk ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''
+ DeBruijn.Sub: weakenSub :: forall (ctx :: Ctx) (ctx' :: Ctx) (t :: Ctx -> Type) (ctx'' :: Ctx). Wk ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''
- DeBruijn.Wk: [IdWk] :: Wk ctx ctx
+ DeBruijn.Wk: [IdWk] :: forall (ctx :: Ctx). Wk ctx ctx
- DeBruijn.Wk: compWk :: Wk a b -> Wk b c -> Wk a c
+ DeBruijn.Wk: compWk :: forall (a :: Ctx) (b :: Ctx) (c :: Ctx). Wk a b -> Wk b c -> Wk a c
- DeBruijn.Wk: contractIdx :: Wk ctx ctx' -> Idx ctx' -> Maybe (Idx ctx)
+ DeBruijn.Wk: contractIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Idx ctx' -> Maybe (Idx ctx)
- DeBruijn.Wk: contractSize :: Wk ctx ctx' -> Size ctx' -> Size ctx
+ DeBruijn.Wk: contractSize :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Size ctx' -> Size ctx
- DeBruijn.Wk: data Wk ctx ctx'
+ DeBruijn.Wk: data Wk (ctx :: Ctx) (ctx' :: Ctx)
- DeBruijn.Wk: overWeakenEnv :: Wk ctx ctx' -> (Env ctx a -> Env ctx a) -> Env ctx' a -> Env ctx' a
+ DeBruijn.Wk: overWeakenEnv :: forall (ctx :: Ctx) (ctx' :: Ctx) a. Wk ctx ctx' -> (Env ctx a -> Env ctx a) -> Env ctx' a -> Env ctx' a
- DeBruijn.Wk: pattern KeepWk :: () => (a ~ S a', b ~ S b') => Wk a' b' -> Wk a b
+ DeBruijn.Wk: pattern KeepWk :: forall a b a' b'. () => (a ~ S a', b ~ S b') => Wk a' b' -> Wk a b
- DeBruijn.Wk: setWeakenEnv :: Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
+ DeBruijn.Wk: setWeakenEnv :: forall (ctx :: Ctx) (ctx' :: Ctx) a. Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
- DeBruijn.Wk: weakenEnv :: Wk ctx ctx' -> Env ctx' a -> Env ctx a
+ DeBruijn.Wk: weakenEnv :: forall (ctx :: Ctx) (ctx' :: Ctx) a. Wk ctx ctx' -> Env ctx' a -> Env ctx a
- DeBruijn.Wk: weakenIdx :: Wk ctx ctx' -> Idx ctx -> Idx ctx'
+ DeBruijn.Wk: weakenIdx :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Idx ctx -> Idx ctx'
- DeBruijn.Wk: weakenSize :: Wk ctx ctx' -> Size ctx -> Size ctx'
+ DeBruijn.Wk: weakenSize :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Size ctx -> Size ctx'
- DeBruijn.Wk: wk1 :: Wk ctx (S ctx)
+ DeBruijn.Wk: wk1 :: forall (ctx :: Ctx). Wk ctx (S ctx)
Files
- debruijn-safe.cabal +9/−3
- src/DeBruijn/Env.hs +12/−1
- src/DeBruijn/Idx.hs +6/−6
- src/DeBruijn/Lvl.hs +14/−3
debruijn-safe.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: debruijn-safe-version: 0.3+version: 0.3.1 license: BSD-3-Clause license-file: LICENSE category: Development@@ -13,7 +13,13 @@ 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.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 source-repository head type: git@@ -27,7 +33,7 @@ -- 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 -- rest of the dependencies
src/DeBruijn/Env.hs view
@@ -4,6 +4,7 @@ lookupEnv, sizeEnv, tabulateEnv,+ zipWithEnv, ) where import Data.Kind (Type)@@ -72,7 +73,7 @@ -- 'b' -- lookupEnv :: Idx ctx -> Env ctx a -> a-lookupEnv IZ (_ :> x) = x+lookupEnv IZ (_ :> x) = x lookupEnv (IS n) (xs :> _) = lookupEnv n xs -- | Size of the environment.@@ -87,3 +88,13 @@ tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a tabulateEnv SZ _ = EmptyEnv tabulateEnv (SS s) f = tabulateEnv s (f . IS) :> f IZ++-- |+--+-- >>> 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 _ EmptyEnv EmptyEnv = EmptyEnv+zipWithEnv f (xs :> x) (ys :> y) = zipWithEnv f xs ys :> f x y
src/DeBruijn/Idx.hs view
@@ -33,16 +33,16 @@ type Idx :: Ctx -> Type type role Idx nominal -data Idx n where- IZ :: Idx (S n)- IS :: !(Idx n) -> Idx (S n)+data Idx ctx where+ IZ :: Idx (S ctx)+ IS :: !(Idx ctx) -> Idx (S ctx) ------------------------------------------------------------------------------- -- Combinators ------------------------------------------------------------------------------- -- | Convert index to 'Int'.-idxToInt :: Idx n -> Int+idxToInt :: Idx ctx -> Int idxToInt = go 0 where go :: Int -> Idx j -> Int go !acc IZ = acc@@ -58,8 +58,8 @@ -- Instances ------------------------------------------------------------------------------- -deriving instance Eq (Idx n)-deriving instance Ord (Idx n)+deriving instance Eq (Idx ctx)+deriving instance Ord (Idx ctx) instance Show (Idx j) where showsPrec d = showsPrec d . idxToInt
src/DeBruijn/Lvl.hs view
@@ -3,13 +3,14 @@ Lvl, lvlToIdx, lvlZ,- sinkLvl,+ idxToLvl,+ -- * Sinking Sinkable (..), sink,- mapSink, sinkSize,- mapSinkSize, sinkAdd,+ mapSink,+ mapSinkSize, mapSinkAdd, ) where @@ -58,6 +59,14 @@ lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx lvlToIdx _ (MkLvl _ x) = x +-- | Convert index to level.+--+-- >>> idxToLvl S2 (IS IZ)+-- 1+--+idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx+idxToLvl s x = (MkLvl (sizeToInt s - idxToInt x) x)+ -- | Last level. -- -- >>> lvlZ S1@@ -69,6 +78,7 @@ lvlZ :: Size ctx -> Lvl (S ctx) lvlZ s = MkLvl (sizeToInt s) IZ +{- TODO? -- | Sink 'Lvl' into a larger context. -- -- >>> sinkLvl (lvlZ S3)@@ -83,6 +93,7 @@ -- sinkLvl :: Lvl ctx -> Lvl (S ctx) sinkLvl (MkLvl s i) = MkLvl s (IS i)+-} ------------------------------------------------------------------------------- -- Sinkable