-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | de Bruijn indices and levels
--   
--   de Bruijn indices and levels for well-scoped terms.
--   
--   This is "unsafe" (as it uses <a>unsafeCoerce</a>) implementation, but
--   it's fast. The API is the same as in <tt>debruin-safe</tt> package.
@package debruijn
@version 0.2

module DeBruijn.Ctx

-- | Context counts variables, in other words context is just a natural
--   number.
type Ctx = Nat

-- | Empty context is zero.
type EmptyCtx = Z

-- | And context extension is a successor.
type S = 'S
type Ctx1 = S EmptyCtx
type Ctx2 = S Ctx1
type Ctx3 = S Ctx2
type Ctx4 = S Ctx3
type Ctx5 = S Ctx4
type Ctx6 = S Ctx5
type Ctx7 = S Ctx6
type Ctx8 = S Ctx7
type Ctx9 = S Ctx8


-- | de Bruijn indices for well-scoped terms.
module DeBruijn.Internal.Idx

-- | de Bruijn indices.
--   
--   <pre>
--   &gt;&gt;&gt; IS (IS (IS IZ))
--   3
--   </pre>
newtype Idx j
UnsafeIdx :: Int -> Idx j
pattern IZ :: () => m ~ S n => Idx m
pattern IS :: () => m ~ S n => Idx n -> Idx m

-- | Derive anything from index into empty scope.
--   
--   Note: don't use <tt>EmptyCase</tt> on <a>Idx</a> as it doesn't work
--   for unsafe representation.
absurdIdx :: Idx EmptyCtx -> a

-- | Case on <a>Idx</a>. (compare to <a>maybe</a>).
unIdx :: a -> (Idx n -> a) -> Idx (S n) -> a

-- | Convert index to <a>Int</a>.
idxToInt :: Idx ctx -> Int
pattern I1 :: () => m ~ S (S n) => Idx m
pattern I2 :: () => m ~ S (S (S n)) => Idx m
pattern I3 :: () => m ~ S (S (S (S n))) => Idx m
pattern I4 :: () => m ~ S (S (S (S (S n)))) => Idx m
pattern I5 :: () => m ~ S (S (S (S (S (S n))))) => Idx m
pattern I6 :: () => m ~ S (S (S (S (S (S (S n)))))) => Idx m
pattern I7 :: () => m ~ S (S (S (S (S (S (S (S n))))))) => Idx m
pattern I8 :: () => m ~ S (S (S (S (S (S (S (S (S n)))))))) => Idx m
pattern I9 :: () => m ~ S (S (S (S (S (S (S (S (S (S n))))))))) => Idx m
instance GHC.Classes.Eq (DeBruijn.Internal.Idx.Idx n)
instance GHC.Classes.Ord (DeBruijn.Internal.Idx.Idx n)
instance GHC.Show.Show (DeBruijn.Internal.Idx.Idx j)


-- | de Bruijn indices for well-scoped terms.
module DeBruijn.Idx

-- | de Bruijn indices.
--   
--   <pre>
--   &gt;&gt;&gt; IS (IS (IS IZ))
--   3
--   </pre>
data Idx j
pattern IZ :: () => m ~ S n => Idx m
pattern IS :: () => m ~ S n => Idx n -> Idx m

-- | Derive anything from index into empty scope.
--   
--   Note: don't use <tt>EmptyCase</tt> on <a>Idx</a> as it doesn't work
--   for unsafe representation.
absurdIdx :: Idx EmptyCtx -> a

-- | Case on <a>Idx</a>. (compare to <a>maybe</a>).
unIdx :: a -> (Idx n -> a) -> Idx (S n) -> a

-- | Convert index to <a>Int</a>.
idxToInt :: Idx ctx -> Int
pattern I1 :: () => m ~ S (S n) => Idx m
pattern I2 :: () => m ~ S (S (S n)) => Idx m
pattern I3 :: () => m ~ S (S (S (S n))) => Idx m
pattern I4 :: () => m ~ S (S (S (S (S n)))) => Idx m
pattern I5 :: () => m ~ S (S (S (S (S (S n))))) => Idx m
pattern I6 :: () => m ~ S (S (S (S (S (S (S n)))))) => Idx m
pattern I7 :: () => m ~ S (S (S (S (S (S (S (S n))))))) => Idx m
pattern I8 :: () => m ~ S (S (S (S (S (S (S (S (S n)))))))) => Idx m
pattern I9 :: () => m ~ S (S (S (S (S (S (S (S (S (S n))))))))) => Idx m

module DeBruijn.Internal.Size

-- | Term level witness of the size of a context.
--   
--   <pre>
--   &gt;&gt;&gt; SZ
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; SS (SS SZ)
--   2
--   </pre>
newtype Size ctx
UnsafeSize :: Int -> Size ctx
pattern SZ :: () => m ~ EmptyCtx => Size m
pattern SS :: () => m ~ S n => Size n -> Size m

-- | Unapply <a>SS</a>. Occasionally more useful than pattern matching.
unSS :: Size (S ctx) -> Size ctx

-- | Convert <a>Size</a> to 'Int.
sizeToInt :: Size ctx -> Int
pattern S1 :: () => m ~ Ctx1 => Size m
pattern S2 :: () => m ~ Ctx2 => Size m
pattern S3 :: () => m ~ Ctx3 => Size m
pattern S4 :: () => m ~ Ctx4 => Size m
pattern S5 :: () => m ~ Ctx5 => Size m
pattern S6 :: () => m ~ Ctx6 => Size m
pattern S7 :: () => m ~ Ctx7 => Size m
pattern S8 :: () => m ~ Ctx8 => Size m
pattern S9 :: () => m ~ Ctx9 => Size m
instance GHC.Show.Show (DeBruijn.Internal.Size.Size ctx)
instance Data.GADT.Internal.GShow DeBruijn.Internal.Size.Size
instance GHC.Classes.Eq (DeBruijn.Internal.Size.Size ctx)
instance GHC.Classes.Ord (DeBruijn.Internal.Size.Size ctx)
instance Data.EqP.EqP DeBruijn.Internal.Size.Size
instance Data.OrdP.OrdP DeBruijn.Internal.Size.Size
instance Data.GADT.Internal.GEq DeBruijn.Internal.Size.Size
instance Data.GADT.Internal.GCompare DeBruijn.Internal.Size.Size
instance Data.Type.Equality.TestEquality DeBruijn.Internal.Size.Size

module DeBruijn.Internal.Env

-- | Environment
--   
--   <pre>
--   &gt;&gt;&gt; EmptyEnv :&gt; 'a' :&gt; 'b'
--   EmptyEnv :&gt; 'a' :&gt; 'b'
--   </pre>
newtype Env ctx a
UnsafeEnv :: SkewList a -> Env ctx a
pattern EmptyEnv :: () => ctx ~ EmptyCtx => Env ctx a
pattern (:>) :: () => ctx ~ S ctx' => Env ctx' a -> a -> Env ctx a
infixl 5 :>

-- | Lookup in the context.
--   
--   <pre>
--   &gt;&gt;&gt; lookupEnv IZ (EmptyEnv :&gt; 'a' :&gt; 'b')
--   'b'
--   </pre>
lookupEnv :: Idx ctx -> Env ctx a -> a

-- | Size of the environment.
--   
--   <pre>
--   &gt;&gt;&gt; sizeEnv (EmptyEnv :&gt; 'a' :&gt; 'b')
--   2
--   </pre>
sizeEnv :: Env n a -> Size n

-- | Create <a>Env</a> by creating elements given an <a>Idx</a>.
--   
--   <pre>
--   &gt;&gt;&gt; tabulateEnv S4 id
--   EmptyEnv :&gt; 3 :&gt; 2 :&gt; 1 :&gt; 0
--   </pre>
tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a
instance GHC.Base.Functor (DeBruijn.Internal.Env.Env ctx)
instance Data.Foldable.Foldable (DeBruijn.Internal.Env.Env ctx)
instance Data.Traversable.Traversable (DeBruijn.Internal.Env.Env ctx)
instance GHC.Show.Show a => GHC.Show.Show (DeBruijn.Internal.Env.Env ctx a)

module DeBruijn.Env

-- | Environment
--   
--   <pre>
--   &gt;&gt;&gt; EmptyEnv :&gt; 'a' :&gt; 'b'
--   EmptyEnv :&gt; 'a' :&gt; 'b'
--   </pre>
data Env ctx a
pattern EmptyEnv :: () => ctx ~ EmptyCtx => Env ctx a
pattern (:>) :: () => ctx ~ S ctx' => Env ctx' a -> a -> Env ctx a
infixl 5 :>

-- | Lookup in the context.
--   
--   <pre>
--   &gt;&gt;&gt; lookupEnv IZ (EmptyEnv :&gt; 'a' :&gt; 'b')
--   'b'
--   </pre>
lookupEnv :: Idx ctx -> Env ctx a -> a

-- | Size of the environment.
--   
--   <pre>
--   &gt;&gt;&gt; sizeEnv (EmptyEnv :&gt; 'a' :&gt; 'b')
--   2
--   </pre>
sizeEnv :: Env n a -> Size n

-- | Create <a>Env</a> by creating elements given an <a>Idx</a>.
--   
--   <pre>
--   &gt;&gt;&gt; tabulateEnv S4 id
--   EmptyEnv :&gt; 3 :&gt; 2 :&gt; 1 :&gt; 0
--   </pre>
tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a

module DeBruijn.Internal.Add

-- | <tt><a>Add</a> n m p</tt> is an evidence that <tt>n + m = p</tt>.
--   
--   Useful when you have an arity <tt>n</tt> thing and need to extend a
--   context <tt>ctx</tt> with: <tt><a>Add</a> n ctx ctx'</tt>.
--   
--   Using a type representing a graph of a type function is often more
--   convenient than defining type-family to begin with.
newtype Add n m p
UnsafeAdd :: Int -> Add n m p
pattern AZ :: () => (n ~ EmptyCtx, m ~ p) => Add n m p
pattern AS :: () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p
addToInt :: Add n m p -> Int
addToSize :: Add n m p -> Size n

-- | Add <tt>n</tt> to some context <tt>ctx</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; adding (SS (SS SZ))
--   Some 2
--   </pre>
adding :: Size n -> Some (Add n ctx)

-- | <pre>
--   n + 0 ≡ 0
--   </pre>
rzeroAdd :: Size n -> Add n EmptyCtx n

-- | <pre>
--   n + 0 ≡ m → n ≡ m
--   </pre>
unrzeroAdd :: Add n EmptyCtx m -> n :~: m

-- | <pre>
--   0 + n ≡ 0
--   </pre>
lzeroAdd :: Size n -> Add EmptyCtx n n

-- | <pre>
--   0 + n ≡ m → n ≡ m
--   </pre>
unlzeroAdd :: Add EmptyCtx n m -> n :~: m

-- | <pre>
--   n + m ≡ p → n + S m ≡ S p
--   </pre>
rsuccAdd :: Add n m p -> Add n (S m) (S p)

-- | <pre>
--   n + S m ≡ S p → n + m ≡ p
--   </pre>
unrsuccAdd :: Add n (S m) (S p) -> Add n m p

-- | <pre>
--   n + m ≡ p → S n + m ≡ S p
--   </pre>
lsuccAdd :: Add n m p -> Add (S n) m (S p)

-- | <pre>
--   S n + m ≡ S p → n + m ≡ p
--   </pre>
unlsuccAdd :: Add (S n) m (S p) -> Add n m p

-- | <pre>
--   n + S m ≡ p → S n + m ≡ p
--   </pre>
swapAdd :: Add n (S m) p -> Add (S n) m p

-- | <pre>
--   S n + m ≡ p → n + S m ≡ p
--   </pre>
unswapAdd :: Add (S n) m p -> Add n (S m) p
instance GHC.Show.Show (DeBruijn.Internal.Add.Add n m p)
instance Data.GADT.Internal.GShow (DeBruijn.Internal.Add.Add n m)

module DeBruijn.Add

-- | <tt><a>Add</a> n m p</tt> is an evidence that <tt>n + m = p</tt>.
--   
--   Useful when you have an arity <tt>n</tt> thing and need to extend a
--   context <tt>ctx</tt> with: <tt><a>Add</a> n ctx ctx'</tt>.
--   
--   Using a type representing a graph of a type function is often more
--   convenient than defining type-family to begin with.
data Add n m p
pattern AZ :: () => (n ~ EmptyCtx, m ~ p) => Add n m p
pattern AS :: () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p
addToInt :: Add n m p -> Int
addToSize :: Add n m p -> Size n

-- | Add <tt>n</tt> to some context <tt>ctx</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; adding (SS (SS SZ))
--   Some 2
--   </pre>
adding :: Size n -> Some (Add n ctx)

-- | <pre>
--   n + 0 ≡ 0
--   </pre>
rzeroAdd :: Size n -> Add n EmptyCtx n

-- | <pre>
--   n + 0 ≡ m → n ≡ m
--   </pre>
unrzeroAdd :: Add n EmptyCtx m -> n :~: m

-- | <pre>
--   0 + n ≡ 0
--   </pre>
lzeroAdd :: Size n -> Add EmptyCtx n n

-- | <pre>
--   0 + n ≡ m → n ≡ m
--   </pre>
unlzeroAdd :: Add EmptyCtx n m -> n :~: m

-- | <pre>
--   n + m ≡ p → n + S m ≡ S p
--   </pre>
rsuccAdd :: Add n m p -> Add n (S m) (S p)

-- | <pre>
--   n + S m ≡ S p → n + m ≡ p
--   </pre>
unrsuccAdd :: Add n (S m) (S p) -> Add n m p

-- | <pre>
--   n + m ≡ p → S n + m ≡ S p
--   </pre>
lsuccAdd :: Add n m p -> Add (S n) m (S p)

-- | <pre>
--   S n + m ≡ S p → n + m ≡ p
--   </pre>
unlsuccAdd :: Add (S n) m (S p) -> Add n m p

-- | <pre>
--   n + S m ≡ p → S n + m ≡ p
--   </pre>
swapAdd :: Add n (S m) p -> Add (S n) m p

-- | <pre>
--   S n + m ≡ p → n + S m ≡ p
--   </pre>
unswapAdd :: Add (S n) m p -> Add n (S m) p

module DeBruijn.Lte

-- | <tt><a>Lte</a> ctx ctx'</tt> is evidence that <tt>ctx'</tt> is smaller
--   than of <tt><tt>ctx</tt></tt>, <i>less-than-or-equal</i>, and produced
--   by simple skipping only, i.e. nothing is inserted into <tt>ctx</tt>,
--   only appended to the end.
data Lte ctx ctx'
[LZ] :: Lte ctx ctx
[LS] :: !Lte ctx ctx' -> Lte ctx (S ctx')


-- | de Bruijn levels for well-scoped terms.
module DeBruijn.Internal.Lvl

-- | de Bruijn levels.
newtype Lvl ctx
UnsafeLvl :: Int -> Lvl ctx

-- | Convert level to index.
--   
--   <pre>
--   &gt;&gt;&gt; lvlToIdx S2 (lvlZ S1)
--   0
--   </pre>
lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx
idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx

-- | Last level.
--   
--   <pre>
--   &gt;&gt;&gt; lvlZ S1
--   1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; lvlZ S5
--   5
--   </pre>
lvlZ :: Size ctx -> Lvl (S ctx)

-- | Sink <a>Lvl</a> into a larger context.
--   
--   <pre>
--   &gt;&gt;&gt; sinkLvl (lvlZ S3)
--   3
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; sink (lvlZ S3)
--   3
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mapLvl (LS LZ) (lvlZ S3)
--   3
--   </pre>
sinkLvl :: Lvl n -> Lvl (S n)

-- | Sinkable terms can be weakened (sunk) cheaply.
class Sinkable t
mapLvl :: Sinkable t => Lte ctx ctx' -> t ctx -> t ctx'

-- | Sink term.
sink :: Sinkable t => t ctx -> t (S ctx)

-- | Essentially <tt><a>fmap</a> <a>sink</a></tt>
mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))

-- | Sink term from empty context to a context of given size.
sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx

-- | Essentially <tt><a>fmap</a> . <a>sinkSize</a></tt>
mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)
sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'
mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')
instance GHC.Classes.Ord (DeBruijn.Internal.Lvl.Lvl ctx)
instance GHC.Classes.Eq (DeBruijn.Internal.Lvl.Lvl ctx)
instance DeBruijn.Internal.Lvl.Sinkable DeBruijn.Internal.Lvl.Lvl
instance DeBruijn.Internal.Lvl.Sinkable Data.Proxy.Proxy
instance GHC.Show.Show (DeBruijn.Internal.Lvl.Lvl ctx)

module DeBruijn.Lvl

-- | de Bruijn levels.
data Lvl ctx

-- | Convert level to index.
--   
--   <pre>
--   &gt;&gt;&gt; lvlToIdx S2 (lvlZ S1)
--   0
--   </pre>
lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx

-- | Last level.
--   
--   <pre>
--   &gt;&gt;&gt; lvlZ S1
--   1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; lvlZ S5
--   5
--   </pre>
lvlZ :: Size ctx -> Lvl (S ctx)
idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx

-- | Sinkable terms can be weakened (sunk) cheaply.
class Sinkable t
mapLvl :: Sinkable t => Lte ctx ctx' -> t ctx -> t ctx'

-- | Sink term.
sink :: Sinkable t => t ctx -> t (S ctx)

-- | Sink term from empty context to a context of given size.
sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx
sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'

-- | Essentially <tt><a>fmap</a> <a>sink</a></tt>
mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))

-- | Essentially <tt><a>fmap</a> . <a>sinkSize</a></tt>
mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)
mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')

module DeBruijn.Size

-- | Term level witness of the size of a context.
--   
--   <pre>
--   &gt;&gt;&gt; SZ
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; SS (SS SZ)
--   2
--   </pre>
data Size ctx
pattern SZ :: () => m ~ EmptyCtx => Size m
pattern SS :: () => m ~ S n => Size n -> Size m

-- | Unapply <a>SS</a>. Occasionally more useful than pattern matching.
unSS :: Size (S ctx) -> Size ctx

-- | Convert <a>Size</a> to 'Int.
sizeToInt :: Size ctx -> Int
pattern S1 :: () => m ~ Ctx1 => Size m
pattern S2 :: () => m ~ Ctx2 => Size m
pattern S3 :: () => m ~ Ctx3 => Size m
pattern S4 :: () => m ~ Ctx4 => Size m
pattern S5 :: () => m ~ Ctx5 => Size m
pattern S6 :: () => m ~ Ctx6 => Size m
pattern S7 :: () => m ~ Ctx7 => Size m
pattern S8 :: () => m ~ Ctx8 => Size m
pattern S9 :: () => m ~ Ctx9 => Size m

module DeBruijn.Wk

-- | Weakenings, order preserving embeddings.
--   
--   <tt>Wk n m</tt> could be represented as <tt>m</tt> bit field with
--   popCount of <tt>n</tt>.
--   
--   Constructor names make sense when you look at the implementation of
--   <a>weakenEnv</a>.
--   
--   Note: usually 'ViewWk is defined as
--   
--   <pre>
--   data Wk ctx ctx' where
--       WkNil  :: Wk EmptyCtx EmptyCtx
--       KeepWk :: Wk ctx ctx' -&gt; Wk (S ctx)  (S ctx')
--       SkipWk :: Wk ctx ctx' -&gt; Wk    ctx   (S ctx')
--   </pre>
--   
--   However that representation doesn't allow to make <tt><tt>wkId</tt> ::
--   'ViewWk ctx ctx</tt> without knowing the size of context. Therefore we
--   morally use a representation closer to
--   
--   <pre>
--   data <a>Wk</a> ctx ctx' where
--       <a>IdWk</a>   :: Wk ctx ctx
--       <a>KeepWk</a> :: Wk ctx ctx' -&gt; Wk (S ctx)  (S ctx')
--       <a>SkipWk</a> :: Wk ctx ctx' -&gt; Wk    ctx   (S ctx')
--   </pre>
--   
--   But we keep an invariant that identity weakenings are always
--   represented by <a>IdWk</a>.
--   
--   <pre>
--   &gt;&gt;&gt; KeepWk IdWk
--   IdWk
--   </pre>
--   
--   And <a>KeepWk</a> pattern doesn't match on identity weakenings.
--   
--   <pre>
--   &gt;&gt;&gt; case IdWk :: Wk Ctx2 Ctx2 of { KeepWk _ -&gt; "keep"; SkipWk _ -&gt; "skip"; IdWk -&gt; "id" } :: String
--   "id"
--   </pre>
data Wk ctx ctx'
[IdWk] :: Wk ctx ctx
pattern SkipWk :: () => b ~ S b' => Wk a b' -> Wk a b
pattern KeepWk :: () => (a ~ S a', b ~ S b') => Wk a' b' -> Wk a b

-- | Weaken by one. <tt><a>wk1</a> = <a>SkipWk</a> <a>IdWk</a></tt>.
wk1 :: Wk ctx (S ctx)

-- | Weakening composition.
compWk :: Wk a b -> Wk b c -> Wk a c

-- | Weaken <a>Idx</a>, i.e. map index from smaller to larger context.
--   
--   <pre>
--   &gt;&gt;&gt; IS IZ
--   1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; weakenIdx wk1 (IS IZ)
--   2
--   </pre>
weakenIdx :: Wk ctx ctx' -> Idx ctx -> Idx ctx'

-- | Contract <a>Idx</a>, i.e. map index from larger to smaller context.
--   
--   <pre>
--   &gt;&gt;&gt; contractIdx wk1 (IS IZ)
--   Just 0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; contractIdx wk1 IZ
--   Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; contractIdx (SkipWk (KeepWk wk1)) &lt;$&gt; [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]
--   </pre>
contractIdx :: Wk ctx ctx' -> Idx ctx' -> Maybe (Idx ctx)

-- | Weaken <a>Size</a>.
weakenSize :: Wk ctx ctx' -> Size ctx -> Size ctx'
contractSize :: Wk ctx ctx' -> Size ctx' -> Size ctx

-- | Contract <a>Env</a> i.e. drop elements from larger context.
--   
--   This function explains the <a>KeepWk</a> and <a>SkipWk</a> constructor
--   names:
--   
--   <pre>
--   &gt;&gt;&gt; weakenEnv (IdWk &amp; SkipWk &amp; KeepWk) (EmptyEnv :&gt; 'a' :&gt; 'b' :&gt; 'c' :&gt; 'd' :&gt; 'e')
--   EmptyEnv :&gt; 'a' :&gt; 'b' :&gt; 'c' :&gt; 'e'
--   </pre>
weakenEnv :: Wk ctx ctx' -> Env ctx' a -> Env ctx a

-- | <a>setWeakenEnv</a> and <a>weakenEnv</a> together form a lens.
--   
--   <pre>
--   &gt;&gt;&gt; setWeakenEnv (IdWk &amp; SkipWk &amp; KeepWk) (EmptyEnv :&gt; 'a' :&gt; 'b') (EmptyEnv :&gt; 'x' :&gt; 'y' :&gt; 'z')
--   EmptyEnv :&gt; 'a' :&gt; 'y' :&gt; 'b'
--   </pre>
setWeakenEnv :: Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a

-- | Setter made from <a>setWeakenEnv</a> and <a>weakenEnv</a>.
--   
--   <pre>
--   &gt;&gt;&gt; overWeakenEnv (IdWk &amp; SkipWk &amp; KeepWk) (fmap toUpper) (EmptyEnv :&gt; 'a' :&gt; 'x' :&gt; 'y' :&gt; 'z')
--   EmptyEnv :&gt; 'A' :&gt; 'X' :&gt; 'y' :&gt; 'Z'
--   </pre>
overWeakenEnv :: Wk ctx ctx' -> (Env ctx a -> Env ctx a) -> Env ctx' a -> Env ctx' a
instance GHC.Classes.Eq (DeBruijn.Wk.Wk ctx ctx')
instance GHC.Classes.Eq (DeBruijn.Wk.Wk1 ctx ctx')
instance GHC.Show.Show (DeBruijn.Wk.Wk ctx ctx')

module DeBruijn.Ren

-- | Renamings are mappings of de Bruijn indices.
--   
--   One possible representation is just <tt>Idx ctx -&gt; Idx ctx'</tt>,
--   but using <a>Env</a> makes this representation inspectable and
--   (hopefully) makes <a>renameIdx</a> perform better.
--   
--   On the other hand, <a>idRen</a> requires <tt><a>Size</a> ctx</tt>.
--   However this isn't an issue, as either there is <a>Size</a> or using
--   <a>Wk</a> is an option.
newtype Ren ctx ctx'
MkRen :: Env ctx (Idx ctx') -> Ren ctx ctx'

-- | Rename de Bruijn index.
renameIdx :: Ren ctx ctx' -> Idx ctx -> Idx ctx'

-- | Lift renaming (used when going under a binder).
keepRen :: Ren ctx ctx' -> Ren (S ctx) (S ctx')
skipRen :: Ren ctx ctx' -> Ren ctx (S ctx')

-- | It's simple to have no indices in any context.
absurdRen :: Ren EmptyCtx ctx

-- | Convert <a>Wk</a> to <a>Ren</a>.
--   
--   Note post and precompositions won't need <a>Size</a>.
wkToRen :: Size ctx -> Wk ctx ctx' -> Ren ctx ctx'

-- | Identity renaming.
idRen :: Size ctx -> Ren ctx ctx

-- | Renaming composition.
compRen :: Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''
newtype RenA f ctx ctx'
MkRenA :: Env ctx (f (Idx ctx')) -> RenA f ctx ctx'
renameIdxA :: RenA f ctx ctx' -> Idx 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')
unusedIdx :: Size ctx -> RenA Maybe (S ctx) ctx

-- | <a>IdxMapping</a> generalizes over various index mappings, also
--   effectful ones.
class Applicative f => IdxMapping f t | t -> f

-- | <a>IdxMapping</a> action.
mapIdx :: IdxMapping f t => t ctx ctx' -> Idx ctx -> f (Idx ctx')

-- | <a>keep</a> is often called <tt>lift</tt>, but we stick with <a>Wk</a>
--   terminology. One benefit is that the name <a>keep</a> is less likely
--   to clash.
keep :: IdxMapping f t => 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 <tt>bound</tt>'s <tt>Scope</tt> possibly lifting
--   whole term).
weakenIdxMapping :: IdxMapping f t => Wk ctx ctx' -> t ctx' ctx'' -> t ctx ctx''

-- | <a>keep</a> <a>IdxMapping</a> <tt>arity</tt> times.
keepAdd :: IdxMapping f m => Add arity ctxA ctxA' -> m ctxA ctxB -> (forall ctxB'. Add arity ctxB ctxB' -> m ctxA' ctxB' -> r) -> r

-- | Renameble things.
--   
--   For most terms it's enough to define a single traversal: an instance
--   of <tt>RenamebleA</tt> type-class, and then define <tt>Renameble</tt>
--   as:
--   
--   <pre>
--   instance <tt>Renameble</tt> Term where <a>rename</a> = <a>defaultRename</a>; <a>weaken</a> = <a>defaultWeaken</a>
--   </pre>
class Weaken t
weaken :: Weaken t => Wk n m -> t n -> t m
class Weaken t => Rename t
rename :: Rename t => Ren n m -> t n -> t m

-- | Effectful renamings.
--   
--   An common example is checking whether a binding is used:
--   
--   <pre>
--   Just t' &lt;- <a>renameA</a> <a>unusedIdx</a> t
--   </pre>
class Rename t => RenameA t
renameA :: forall f ctx ctx'. (RenameA t, Applicative f) => RenA f ctx ctx' -> t ctx -> f (t ctx')

-- | Generic renaming of a term <tt>t</tt> using any <a>IdxMapping</a>.
grename :: forall m f ctx ctx'. (RenameA t, IdxMapping f m) => m ctx ctx' -> t ctx -> f (t ctx')

-- | <a>rename</a> implementation using <a>grename</a>.
defaultRename :: forall t n m. RenameA t => Ren n m -> t n -> t m

-- | <a>weaken</a> implementation using <a>grename</a>.
defaultWeaken :: forall t n m. RenameA t => Wk n m -> t n -> t m
instance DeBruijn.Ren.RenameA Data.Proxy.Proxy
instance DeBruijn.Ren.RenameA DeBruijn.Internal.Idx.Idx
instance DeBruijn.Ren.Rename Data.Proxy.Proxy
instance DeBruijn.Ren.Rename DeBruijn.Internal.Idx.Idx
instance DeBruijn.Ren.Rename (DeBruijn.Ren.Ren n)
instance DeBruijn.Ren.Weaken Data.Proxy.Proxy
instance DeBruijn.Ren.Weaken DeBruijn.Internal.Idx.Idx
instance DeBruijn.Ren.Weaken (DeBruijn.Ren.Ren n)
instance DeBruijn.Ren.IdxMapping Data.Functor.Identity.Identity DeBruijn.Wk.Wk
instance DeBruijn.Ren.IdxMapping Data.Functor.Identity.Identity DeBruijn.Ren.Ren
instance GHC.Base.Applicative f => DeBruijn.Ren.IdxMapping f (DeBruijn.Ren.RenA f)

module DeBruijn.Sub

-- | Substitutions.
newtype Sub t ctx ctx'
MkSub :: Env ctx (t ctx') -> Sub t ctx ctx'
unSub :: Sub t ctx ctx' -> Env ctx (t ctx')

-- | Substitute index.
substIdx :: Sub t ctx ctx' -> Idx ctx -> t ctx'

-- | Substitution from empty context.
emptySub :: Sub t EmptyCtx ctx'
snocSub :: Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx'
keepSub :: (Rename t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx')

-- | Precompose <a>Sub</a> with weakening.
weakenSub :: Wk ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''
nameMe :: Rename t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''

-- | Identity substitution
idSub :: Var t => Size ctx -> Sub t ctx ctx

-- | Substitution composition.
compSub :: Subst t => Sub t ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''

-- | Terms which contain indices as variables.
class Var t
var :: Var t => Idx ctx -> t ctx

-- | Terms which we can subsitute into.
class Var t => Subst t
subst :: Subst t => Sub t ctx ctx' -> t ctx -> t ctx'
instance DeBruijn.Sub.Subst Data.Proxy.Proxy
instance DeBruijn.Sub.Subst DeBruijn.Internal.Idx.Idx
instance DeBruijn.Sub.Var Data.Proxy.Proxy
instance DeBruijn.Sub.Var DeBruijn.Internal.Idx.Idx

module DeBruijn

-- | Weaken closed term to arbitrary context.
--   
--   Note: this has different requirements than <tt>sinkSize</tt>.
weakenUsingSize :: Rename t => Size ctx -> t EmptyCtx -> t ctx