debruijn 0.3 → 0.3.1
raw patch · 6 files changed
+222/−27 lines, 6 filesdep +QuickCheckdep +debruijndep +tastydep ~basePVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: QuickCheck, debruijn, tasty, tasty-quickcheck
Dependency ranges changed: base
API changes (from Hackage documentation)
+ DeBruijn.Env: zipWithEnv :: forall a b c (ctx :: Ctx). (a -> b -> c) -> Env ctx a -> Env ctx b -> Env ctx c
+ DeBruijn.Internal.Env: zipWithEnv :: forall a b c (ctx :: Ctx). (a -> b -> c) -> Env ctx a -> Env ctx b -> Env ctx c
- 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: 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: pattern AS :: () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p
+ DeBruijn.Add: pattern AS :: forall n p m n' p'. () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p
- 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: 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: pattern (:>) :: () => ctx ~ S ctx' => Env ctx' a -> a -> Env ctx a
+ DeBruijn.Env: pattern (:>) :: forall ctx a ctx'. () => ctx ~ S ctx' => Env ctx' a -> a -> Env ctx 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: data Idx j
+ DeBruijn.Idx: data Idx (ctx :: Ctx)
- DeBruijn.Idx: idxToInt :: Idx ctx -> 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.Internal.Add: UnsafeAdd :: Int -> Add n m p
+ DeBruijn.Internal.Add: UnsafeAdd :: Int -> Add (n :: Ctx) (m :: Ctx) (p :: Ctx)
- DeBruijn.Internal.Add: addToInt :: Add n m p -> Int
+ DeBruijn.Internal.Add: addToInt :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int
- DeBruijn.Internal.Add: addToSize :: Add n m p -> Size n
+ DeBruijn.Internal.Add: addToSize :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Size n
- DeBruijn.Internal.Add: adding :: Size n -> Some (Add n ctx)
+ DeBruijn.Internal.Add: adding :: forall (n :: Ctx) (ctx :: Ctx). Size n -> Some (Add n ctx)
- DeBruijn.Internal.Add: lsuccAdd :: Add n m p -> Add (S n) m (S p)
+ DeBruijn.Internal.Add: lsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Add (S n) m (S p)
- DeBruijn.Internal.Add: lzeroAdd :: Size n -> Add EmptyCtx n n
+ DeBruijn.Internal.Add: lzeroAdd :: forall (n :: Ctx). Size n -> Add EmptyCtx n n
- DeBruijn.Internal.Add: newtype Add n m p
+ DeBruijn.Internal.Add: newtype Add (n :: Ctx) (m :: Ctx) (p :: Ctx)
- DeBruijn.Internal.Add: pattern AS :: () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p
+ DeBruijn.Internal.Add: pattern AS :: forall n p m n' p'. () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p
- DeBruijn.Internal.Add: rsuccAdd :: Add n m p -> Add n (S m) (S p)
+ DeBruijn.Internal.Add: rsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Add n (S m) (S p)
- DeBruijn.Internal.Add: rzeroAdd :: Size n -> Add n EmptyCtx n
+ DeBruijn.Internal.Add: rzeroAdd :: forall (n :: Ctx). Size n -> Add n EmptyCtx n
- DeBruijn.Internal.Add: swapAdd :: Add n (S m) p -> Add (S n) m p
+ DeBruijn.Internal.Add: swapAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n (S m) p -> Add (S n) m p
- DeBruijn.Internal.Add: unlsuccAdd :: Add (S n) m (S p) -> Add n m p
+ DeBruijn.Internal.Add: unlsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add (S n) m (S p) -> Add n m p
- DeBruijn.Internal.Add: unlzeroAdd :: Add EmptyCtx n m -> n :~: m
+ DeBruijn.Internal.Add: unlzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add EmptyCtx n m -> n :~: m
- DeBruijn.Internal.Add: unrsuccAdd :: Add n (S m) (S p) -> Add n m p
+ DeBruijn.Internal.Add: unrsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n (S m) (S p) -> Add n m p
- DeBruijn.Internal.Add: unrzeroAdd :: Add n EmptyCtx m -> n :~: m
+ DeBruijn.Internal.Add: unrzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add n EmptyCtx m -> n :~: m
- DeBruijn.Internal.Add: unswapAdd :: Add (S n) m p -> Add n (S m) p
+ DeBruijn.Internal.Add: unswapAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add (S n) m p -> Add n (S m) p
- DeBruijn.Internal.Env: UnsafeEnv :: SkewList a -> Env ctx a
+ DeBruijn.Internal.Env: UnsafeEnv :: SkewList a -> Env (ctx :: Ctx) a
- DeBruijn.Internal.Env: lookupEnv :: Idx ctx -> Env ctx a -> a
+ DeBruijn.Internal.Env: lookupEnv :: forall (ctx :: Ctx) a. Idx ctx -> Env ctx a -> a
- DeBruijn.Internal.Env: newtype Env ctx a
+ DeBruijn.Internal.Env: newtype Env (ctx :: Ctx) a
- DeBruijn.Internal.Env: pattern (:>) :: () => ctx ~ S ctx' => Env ctx' a -> a -> Env ctx a
+ DeBruijn.Internal.Env: pattern (:>) :: forall ctx a ctx'. () => ctx ~ S ctx' => Env ctx' a -> a -> Env ctx a
- DeBruijn.Internal.Env: sizeEnv :: Env n a -> Size n
+ DeBruijn.Internal.Env: sizeEnv :: forall (n :: Ctx) a. Env n a -> Size n
- DeBruijn.Internal.Env: tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a
+ DeBruijn.Internal.Env: tabulateEnv :: forall (ctx :: Ctx) a. Size ctx -> (Idx ctx -> a) -> Env ctx a
- DeBruijn.Internal.Idx: UnsafeIdx :: Int -> Idx j
+ DeBruijn.Internal.Idx: UnsafeIdx :: Int -> Idx (ctx :: Ctx)
- DeBruijn.Internal.Idx: idxToInt :: Idx ctx -> Int
+ DeBruijn.Internal.Idx: idxToInt :: forall (ctx :: Ctx). Idx ctx -> Int
- DeBruijn.Internal.Idx: newtype Idx j
+ DeBruijn.Internal.Idx: newtype Idx (ctx :: Ctx)
- DeBruijn.Internal.Idx: pattern I9 :: () => m ~ S (S (S (S (S (S (S (S (S (S n))))))))) => Idx m
+ DeBruijn.Internal.Idx: pattern I9 :: forall m (n :: Ctx). () => m ~ S (S (S (S (S (S (S (S (S (S n))))))))) => Idx m
- DeBruijn.Internal.Idx: unIdx :: a -> (Idx n -> a) -> Idx (S n) -> a
+ DeBruijn.Internal.Idx: unIdx :: forall a (n :: Ctx). a -> (Idx n -> a) -> Idx (S n) -> a
- DeBruijn.Internal.Lvl: UnsafeLvl :: Int -> Lvl ctx
+ DeBruijn.Internal.Lvl: UnsafeLvl :: Int -> Lvl (ctx :: Ctx)
- DeBruijn.Internal.Lvl: class Sinkable t
+ DeBruijn.Internal.Lvl: class Sinkable (t :: Ctx -> Type)
- DeBruijn.Internal.Lvl: idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx
+ DeBruijn.Internal.Lvl: idxToLvl :: forall (ctx :: Ctx). Size ctx -> Idx ctx -> Lvl ctx
- DeBruijn.Internal.Lvl: lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx
+ DeBruijn.Internal.Lvl: lvlToIdx :: forall (ctx :: Ctx). Size ctx -> Lvl ctx -> Idx ctx
- DeBruijn.Internal.Lvl: lvlZ :: Size ctx -> Lvl (S ctx)
+ DeBruijn.Internal.Lvl: lvlZ :: forall (ctx :: Ctx). Size ctx -> Lvl (S ctx)
- DeBruijn.Internal.Lvl: mapLvl :: Sinkable t => Lte ctx ctx' -> t ctx -> t ctx'
+ DeBruijn.Internal.Lvl: mapLvl :: forall (ctx :: Ctx) (ctx' :: Ctx). Sinkable t => Lte ctx ctx' -> t ctx -> t ctx'
- DeBruijn.Internal.Lvl: mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))
+ DeBruijn.Internal.Lvl: mapSink :: forall f t (ctx :: Ctx). (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))
- DeBruijn.Internal.Lvl: mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')
+ DeBruijn.Internal.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.Internal.Lvl: mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)
+ DeBruijn.Internal.Lvl: mapSinkSize :: forall f t (ctx :: Ctx). (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)
- DeBruijn.Internal.Lvl: newtype Lvl ctx
+ DeBruijn.Internal.Lvl: newtype Lvl (ctx :: Ctx)
- DeBruijn.Internal.Lvl: sink :: Sinkable t => t ctx -> t (S ctx)
+ DeBruijn.Internal.Lvl: sink :: forall t (ctx :: Ctx). Sinkable t => t ctx -> t (S ctx)
- DeBruijn.Internal.Lvl: sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'
+ DeBruijn.Internal.Lvl: sinkAdd :: forall t (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx). Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'
- DeBruijn.Internal.Lvl: sinkLvl :: Lvl n -> Lvl (S n)
+ DeBruijn.Internal.Lvl: sinkLvl :: forall (n :: Ctx). Lvl n -> Lvl (S n)
- DeBruijn.Internal.Lvl: sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx
+ DeBruijn.Internal.Lvl: sinkSize :: forall t (ctx :: Ctx). Sinkable t => Size ctx -> t EmptyCtx -> t ctx
- DeBruijn.Internal.Size: UnsafeSize :: Int -> Size ctx
+ DeBruijn.Internal.Size: UnsafeSize :: Int -> Size (ctx :: Ctx)
- DeBruijn.Internal.Size: newtype Size ctx
+ DeBruijn.Internal.Size: newtype Size (ctx :: Ctx)
- DeBruijn.Internal.Size: sizeToInt :: Size ctx -> Int
+ DeBruijn.Internal.Size: sizeToInt :: forall (ctx :: Ctx). Size ctx -> Int
- DeBruijn.Internal.Size: unSS :: Size (S ctx) -> Size ctx
+ DeBruijn.Internal.Size: unSS :: forall (ctx :: Ctx). Size (S ctx) -> Size ctx
- 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: idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx
+ DeBruijn.Lvl: idxToLvl :: forall (ctx :: Ctx). Size ctx -> Idx ctx -> Lvl 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: 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
- CHANGELOG.md +4/−0
- debruijn.cabal +49/−26
- src/DeBruijn/Env.hs +1/−0
- src/DeBruijn/Internal/Env.hs +21/−0
- src/DeBruijn/Internal/Idx.hs +1/−1
- tests/debruijn-tests.hs +146/−0
CHANGELOG.md view
@@ -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
debruijn.cabal view
@@ -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 <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+ 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
src/DeBruijn/Env.hs view
@@ -4,6 +4,7 @@ lookupEnv, sizeEnv, tabulateEnv,+ zipWithEnv, ) where import DeBruijn.Internal.Env
src/DeBruijn/Internal/Env.hs view
@@ -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')
src/DeBruijn/Internal/Idx.hs view
@@ -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
+ tests/debruijn-tests.hs view
@@ -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