{-# LANGUAGE Safe #-}
module DeBruijn.Ren (
    -- * Renamings
    Ren (..),
    renameIdx,
    keepRen,
    skipRen,
    absurdRen,
    wkToRen,
    -- ** Category
    idRen,
    compRen,
    -- * Applicative renamings
    RenA (..),
    renameIdxA,
    keepRenA,
    unusedIdx,
    -- * Renameble things
    IdxMapping (..),
    keepAdd,
    Weaken (..),
    Rename (..),
    RenameA (..),
    defaultRename,
    defaultWeaken,
) where

import Data.Functor.Identity (Identity (..))
import Data.Kind             (Constraint, Type)
import Data.Proxy            (Proxy (..))

import DeBruijn.Add
import DeBruijn.Ctx
import DeBruijn.Env
import DeBruijn.Idx
import DeBruijn.Size
import DeBruijn.Wk

import TrustworthyCompat (coerce)

-------------------------------------------------------------------------------
-- Renamings
-------------------------------------------------------------------------------

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

-- | Rename de Bruijn index.
renameIdx :: Ren ctx ctx' -> Idx ctx -> Idx ctx'
renameIdx :: forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Idx ctx -> Idx ctx'
renameIdx (MkRen Env ctx (Idx ctx')
js) Idx ctx
i = Idx ctx -> Env ctx (Idx ctx') -> Idx ctx'
forall (ctx :: Ctx) a. Idx ctx -> Env ctx a -> a
lookupEnv Idx ctx
i Env ctx (Idx ctx')
js

-- | Identity renaming.
idRen :: Size ctx -> Ren ctx ctx
idRen :: forall (ctx :: Ctx). Size ctx -> Ren ctx ctx
idRen Size ctx
s = Env ctx (Idx ctx) -> Ren ctx ctx
forall (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (Idx ctx') -> Ren ctx ctx'
MkRen (Env ctx (Idx ctx) -> Ren ctx ctx)
-> Env ctx (Idx ctx) -> Ren ctx ctx
forall a b. (a -> b) -> a -> b
$ Size ctx -> (Idx ctx -> Idx ctx) -> Env ctx (Idx ctx)
forall (ctx :: Ctx) a. Size ctx -> (Idx ctx -> a) -> Env ctx a
tabulateEnv Size ctx
s Idx ctx -> Idx ctx
forall a. a -> a
id

-- | Lift renaming (used when going under a binder).
keepRen :: Ren ctx ctx' -> Ren (S ctx) (S ctx')
keepRen :: forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Ren (S ctx) (S ctx')
keepRen (MkRen Env ctx (Idx ctx')
js) = Env (S ctx) (Idx (S ctx')) -> Ren (S ctx) (S ctx')
forall (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (Idx ctx') -> Ren ctx ctx'
MkRen ((Idx ctx' -> Idx (S ctx'))
-> Env ctx (Idx ctx') -> Env ctx (Idx (S ctx'))
forall a b. (a -> b) -> Env ctx a -> Env ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Idx ctx' -> Idx (S ctx')
forall (m :: Ctx) (n :: Ctx). (m ~ S n) => Idx n -> Idx m
IS Env ctx (Idx ctx')
js Env ctx (Idx (S ctx'))
-> Idx (S ctx') -> Env (S ctx) (Idx (S ctx'))
forall (ctx :: Ctx) a (ctx' :: Ctx).
(ctx ~ S ctx') =>
Env ctx' a -> a -> Env ctx a
:> Idx (S ctx')
forall (m :: Ctx) (n :: Ctx). (m ~ S n) => Idx m
IZ)

skipRen :: Ren ctx ctx' -> Ren ctx (S ctx')
skipRen :: forall (ctx :: Ctx) (ctx' :: Ctx). Ren ctx ctx' -> Ren ctx (S ctx')
skipRen (MkRen Env ctx (Idx ctx')
js) = Env ctx (Idx (S ctx')) -> Ren ctx (S ctx')
forall (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (Idx ctx') -> Ren ctx ctx'
MkRen ((Idx ctx' -> Idx (S ctx'))
-> Env ctx (Idx ctx') -> Env ctx (Idx (S ctx'))
forall a b. (a -> b) -> Env ctx a -> Env ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Idx ctx' -> Idx (S ctx')
forall (m :: Ctx) (n :: Ctx). (m ~ S n) => Idx n -> Idx m
IS Env ctx (Idx ctx')
js)

-- | Convert 'Wk' to 'Ren'.
--
-- Note post and precompositions won't need 'Size'.
wkToRen :: Size ctx -> Wk ctx ctx' -> Ren ctx ctx'
wkToRen :: forall (ctx :: Ctx) (ctx' :: Ctx).
Size ctx -> Wk ctx ctx' -> Ren ctx ctx'
wkToRen Size ctx
s      Wk ctx ctx'
IdWk       = Size ctx -> Ren ctx ctx
forall (ctx :: Ctx). Size ctx -> Ren ctx ctx
idRen Size ctx
s
wkToRen Size ctx
s      (SkipWk Wk ctx b'
w) = Ren ctx b' -> Ren ctx (S b')
forall (ctx :: Ctx) (ctx' :: Ctx). Ren ctx ctx' -> Ren ctx (S ctx')
skipRen (Size ctx -> Wk ctx b' -> Ren ctx b'
forall (ctx :: Ctx) (ctx' :: Ctx).
Size ctx -> Wk ctx ctx' -> Ren ctx ctx'
wkToRen Size ctx
s Wk ctx b'
w)
wkToRen (SS Size n
s) (KeepWk Wk a' b'
w) = Ren n b' -> Ren (S n) (S b')
forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Ren (S ctx) (S ctx')
keepRen (Size n -> Wk n b' -> Ren n b'
forall (ctx :: Ctx) (ctx' :: Ctx).
Size ctx -> Wk ctx ctx' -> Ren ctx ctx'
wkToRen Size n
s Wk n b'
Wk a' b'
w)

-- | Renaming composition.
compRen :: Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''
compRen :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx).
Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''
compRen (MkRen Env ctx (Idx ctx')
r) Ren ctx' ctx''
r' = Env ctx (Idx ctx'') -> Ren ctx ctx''
forall (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (Idx ctx') -> Ren ctx ctx'
MkRen ((Idx ctx' -> Idx ctx'')
-> Env ctx (Idx ctx') -> Env ctx (Idx ctx'')
forall a b. (a -> b) -> Env ctx a -> Env ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ren ctx' ctx'' -> Idx ctx' -> Idx ctx''
forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Idx ctx -> Idx ctx'
forall (t :: Ctx -> *) (n :: Ctx) (m :: Ctx).
Rename t =>
Ren n m -> t n -> t m
rename Ren ctx' ctx''
r') Env ctx (Idx ctx')
r)

-- | It's simple to have no indices in any context.
absurdRen :: Ren EmptyCtx ctx
absurdRen :: forall (ctx :: Ctx). Ren EmptyCtx ctx
absurdRen = Env EmptyCtx (Idx ctx) -> Ren EmptyCtx ctx
forall (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (Idx ctx') -> Ren ctx ctx'
MkRen Env EmptyCtx (Idx ctx)
forall (ctx :: Ctx) a. (ctx ~ EmptyCtx) => Env ctx a
EmptyEnv

-------------------------------------------------------------------------------
-- 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 :: forall (f :: * -> *) (ctx :: Ctx) (ctx' :: Ctx).
Applicative f =>
RenA f ctx ctx' -> RenA f (S ctx) (S ctx')
keepRenA (MkRenA Env ctx (f (Idx ctx'))
js) = Env (S ctx) (f (Idx (S ctx'))) -> RenA f (S ctx) (S ctx')
forall (f :: * -> *) (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (f (Idx ctx')) -> RenA f ctx ctx'
MkRenA ((f (Idx ctx') -> f (Idx (S ctx')))
-> Env ctx (f (Idx ctx')) -> Env ctx (f (Idx (S ctx')))
forall a b. (a -> b) -> Env ctx a -> Env ctx b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Idx ctx' -> Idx (S ctx')) -> f (Idx ctx') -> f (Idx (S ctx'))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Idx ctx' -> Idx (S ctx')
forall (m :: Ctx) (n :: Ctx). (m ~ S n) => Idx n -> Idx m
IS) Env ctx (f (Idx ctx'))
js Env ctx (f (Idx (S ctx')))
-> f (Idx (S ctx')) -> Env (S ctx) (f (Idx (S ctx')))
forall (ctx :: Ctx) a (ctx' :: Ctx).
(ctx ~ S ctx') =>
Env ctx' a -> a -> Env ctx a
:> Idx (S ctx') -> f (Idx (S ctx'))
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Idx (S ctx')
forall (m :: Ctx) (n :: Ctx). (m ~ S n) => Idx m
IZ)

unusedIdx :: Size ctx -> RenA Maybe (S ctx) ctx
unusedIdx :: forall (ctx :: Ctx). Size ctx -> RenA Maybe (S ctx) ctx
unusedIdx Size ctx
s = Env (S ctx) (Maybe (Idx ctx)) -> RenA Maybe (S ctx) ctx
forall (f :: * -> *) (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (f (Idx ctx')) -> RenA f ctx ctx'
MkRenA (Env (S ctx) (Maybe (Idx ctx)) -> RenA Maybe (S ctx) ctx)
-> Env (S ctx) (Maybe (Idx ctx)) -> RenA Maybe (S ctx) ctx
forall a b. (a -> b) -> a -> b
$ Size (S ctx)
-> (Idx (S ctx) -> Maybe (Idx ctx))
-> Env (S ctx) (Maybe (Idx ctx))
forall (ctx :: Ctx) a. Size ctx -> (Idx ctx -> a) -> Env ctx a
tabulateEnv (Size ctx -> Size (S ctx)
forall (m :: Ctx) (n :: Ctx). (m ~ S n) => Size n -> Size m
SS Size ctx
s) ((Idx (S ctx) -> Maybe (Idx ctx)) -> Env (S ctx) (Maybe (Idx ctx)))
-> (Idx (S ctx) -> Maybe (Idx ctx))
-> Env (S ctx) (Maybe (Idx ctx))
forall a b. (a -> b) -> a -> b
$ Maybe (Idx ctx)
-> (Idx ctx -> Maybe (Idx ctx)) -> Idx (S ctx) -> Maybe (Idx ctx)
forall a (n :: Ctx). a -> (Idx n -> a) -> Idx (S n) -> a
unIdx Maybe (Idx ctx)
forall a. Maybe a
Nothing Idx ctx -> Maybe (Idx ctx)
forall a. a -> Maybe a
Just

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

    -- | '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
    => Add arity ctxA ctxA'
    -> m ctxA ctxB
    -> (forall ctxB'. Add arity ctxB ctxB' -> m ctxA' ctxB' -> r)
    -> r
keepAdd :: forall (f :: * -> *) (m :: Ctx -> Ctx -> *) (arity :: Ctx)
       (ctxA :: Ctx) (ctxA' :: Ctx) (ctxB :: Ctx) r.
IdxMapping f m =>
Add arity ctxA ctxA'
-> m ctxA ctxB
-> (forall (ctxB' :: Ctx).
    Add arity ctxB ctxB' -> m ctxA' ctxB' -> r)
-> r
keepAdd Add arity ctxA ctxA'
AZ     m ctxA ctxB
w forall (ctxB' :: Ctx). Add arity ctxB ctxB' -> m ctxA' ctxB' -> r
kont = Add arity ctxB ctxB -> m ctxA' ctxB -> r
forall (ctxB' :: Ctx). Add arity ctxB ctxB' -> m ctxA' ctxB' -> r
kont Add arity ctxB ctxB
forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
(n ~ EmptyCtx, m ~ p) =>
Add n m p
AZ m ctxA ctxB
m ctxA' ctxB
w
keepAdd (AS Add n' ctxA p'
a) m ctxA ctxB
w forall (ctxB' :: Ctx). Add arity ctxB ctxB' -> m ctxA' ctxB' -> r
kont = Add n' ctxA p'
-> m ctxA ctxB
-> (forall {ctxB' :: Ctx}. Add n' ctxB ctxB' -> m p' ctxB' -> r)
-> r
forall (f :: * -> *) (m :: Ctx -> Ctx -> *) (arity :: Ctx)
       (ctxA :: Ctx) (ctxA' :: Ctx) (ctxB :: Ctx) r.
IdxMapping f m =>
Add arity ctxA ctxA'
-> m ctxA ctxB
-> (forall (ctxB' :: Ctx).
    Add arity ctxB ctxB' -> m ctxA' ctxB' -> r)
-> r
keepAdd Add n' ctxA p'
a m ctxA ctxB
w ((forall {ctxB' :: Ctx}. Add n' ctxB ctxB' -> m p' ctxB' -> r)
 -> r)
-> (forall {ctxB' :: Ctx}. Add n' ctxB ctxB' -> m p' ctxB' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Add n' ctxB ctxB'
a' m p' ctxB'
w' -> Add arity ctxB (S ctxB') -> m ctxA' (S ctxB') -> r
forall (ctxB' :: Ctx). Add arity ctxB ctxB' -> m ctxA' ctxB' -> r
kont (Add n' ctxB ctxB' -> Add arity ctxB (S ctxB')
forall (n :: Ctx) (p :: Ctx) (m :: Ctx) (n' :: Ctx) (p' :: Ctx).
(n ~ S n', p ~ S p') =>
Add n' m p' -> Add n m p
AS Add n' ctxB ctxB'
a') (m p' ctxB' -> m (S p') (S ctxB')
forall (ctx :: Ctx) (ctx' :: Ctx). m ctx ctx' -> m (S ctx) (S ctx')
forall (f :: * -> *) (t :: Ctx -> Ctx -> *) (ctx :: Ctx)
       (ctx' :: Ctx).
IdxMapping f t =>
t ctx ctx' -> t (S ctx) (S ctx')
keep m p' ctxB'
w')

instance IdxMapping Identity Wk where
    keep :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Wk (S ctx) (S ctx')
keep = Wk ctx ctx' -> Wk (S ctx) (S ctx')
forall (a :: Ctx) (b :: Ctx) (a' :: Ctx) (b' :: Ctx).
(a ~ S a', b ~ S b') =>
Wk a' b' -> Wk a b
KeepWk
    mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Idx ctx -> Identity (Idx ctx')
mapIdx Wk ctx ctx'
w Idx ctx
x = Idx ctx' -> Identity (Idx ctx')
forall a. a -> Identity a
Identity (Wk ctx ctx' -> Idx ctx -> Idx ctx'
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Idx ctx -> Idx ctx'
weakenIdx Wk ctx ctx'
w Idx ctx
x)
    weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx).
Wk ctx ctx' -> Wk ctx' ctx'' -> Wk ctx ctx''
weakenIdxMapping = Wk ctx ctx' -> Wk ctx' ctx'' -> Wk ctx ctx''
forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx).
Wk ctx ctx' -> Wk ctx' ctx'' -> Wk ctx ctx''
compWk

instance IdxMapping Identity Ren where
    keep :: forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Ren (S ctx) (S ctx')
keep = Ren ctx ctx' -> Ren (S ctx) (S ctx')
forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Ren (S ctx) (S ctx')
keepRen
    mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Idx ctx -> Identity (Idx ctx')
mapIdx Ren ctx ctx'
w Idx ctx
x = Idx ctx' -> Identity (Idx ctx')
forall a. a -> Identity a
Identity (Ren ctx ctx' -> Idx ctx -> Idx ctx'
forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Idx ctx -> Idx ctx'
renameIdx Ren ctx ctx'
w Idx ctx
x)
    weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx).
Wk ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''
weakenIdxMapping Wk ctx ctx'
w (MkRen Env ctx' (Idx ctx'')
is) = Env ctx (Idx ctx'') -> Ren ctx ctx''
forall (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (Idx ctx') -> Ren ctx ctx'
MkRen (Wk ctx ctx' -> Env ctx' (Idx ctx'') -> Env ctx (Idx ctx'')
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk ctx ctx' -> Env ctx' a -> Env ctx a
weakenEnv Wk ctx ctx'
w Env ctx' (Idx ctx'')
is)

instance Applicative f => IdxMapping f (RenA f) where
    keep :: forall (ctx :: Ctx) (ctx' :: Ctx).
RenA f ctx ctx' -> RenA f (S ctx) (S ctx')
keep = RenA f ctx ctx' -> RenA f (S ctx) (S ctx')
forall (f :: * -> *) (ctx :: Ctx) (ctx' :: Ctx).
Applicative f =>
RenA f ctx ctx' -> RenA f (S ctx) (S ctx')
keepRenA
    mapIdx :: forall (ctx :: Ctx) (ctx' :: Ctx).
RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')
mapIdx = RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')
forall (f :: * -> *) (ctx :: Ctx) (ctx' :: Ctx).
RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')
renameIdxA
    weakenIdxMapping :: forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx).
Wk ctx ctx' -> RenA f ctx' ctx'' -> RenA f ctx ctx''
weakenIdxMapping Wk ctx ctx'
w (MkRenA Env ctx' (f (Idx ctx''))
is) = Env ctx (f (Idx ctx'')) -> RenA f ctx ctx''
forall (f :: * -> *) (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (f (Idx ctx')) -> RenA f ctx ctx'
MkRenA (Wk ctx ctx' -> Env ctx' (f (Idx ctx'')) -> Env ctx (f (Idx ctx''))
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk ctx ctx' -> Env ctx' a -> Env ctx a
weakenEnv Wk ctx ctx'
w Env ctx' (f (Idx ctx''))
is)

renameIdxA :: RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')
renameIdxA :: forall (f :: * -> *) (ctx :: Ctx) (ctx' :: Ctx).
RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')
renameIdxA (MkRenA Env ctx (f (Idx ctx'))
js) Idx ctx
i = Idx ctx -> Env ctx (f (Idx ctx')) -> f (Idx ctx')
forall (ctx :: Ctx) a. Idx ctx -> Env ctx a -> a
lookupEnv Idx ctx
i Env ctx (f (Idx ctx'))
js

-- | Renameble things.
--
-- For most terms it's enough to define a single traversal: an instance of 'RenamebleA' type-class,
-- and then define 'Renameble' as:
--
-- @
-- instance 'Renameble' Term where 'rename' = 'defaultRename'; 'weaken' = 'defaultWeaken'
-- @
--
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. RenameA t => Ren n m -> t n -> t m
defaultRename :: forall (t :: Ctx -> *) (n :: Ctx) (m :: Ctx).
RenameA t =>
Ren n m -> t n -> t m
defaultRename = (Ren n m -> t n -> Identity (t m)) -> Ren n m -> t n -> t m
forall a b. Coercible a b => a -> b
coerce (forall (t :: Ctx -> *) (m :: Ctx -> Ctx -> *) (f :: * -> *)
       (ctx :: Ctx) (ctx' :: Ctx).
(RenameA t, IdxMapping f m) =>
m ctx ctx' -> t ctx -> f (t ctx')
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 :: forall (t :: Ctx -> *) (n :: Ctx) (m :: Ctx).
RenameA t =>
Wk n m -> t n -> t m
defaultWeaken = (Wk n m -> t n -> Identity (t m)) -> Wk n m -> t n -> t m
forall a b. Coercible a b => a -> b
coerce (forall (t :: Ctx -> *) (m :: Ctx -> Ctx -> *) (f :: * -> *)
       (ctx :: Ctx) (ctx' :: Ctx).
(RenameA t, IdxMapping f m) =>
m ctx ctx' -> t ctx -> f (t ctx')
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 = RenA f ctx ctx' -> t ctx -> f (t ctx')
forall (t :: Ctx -> *) (m :: Ctx -> Ctx -> *) (f :: * -> *)
       (ctx :: Ctx) (ctx' :: Ctx).
(RenameA t, IdxMapping f m) =>
m ctx ctx' -> t ctx -> f (t ctx')
forall (m :: Ctx -> Ctx -> *) (f :: * -> *) (ctx :: Ctx)
       (ctx' :: Ctx).
IdxMapping f m =>
m ctx ctx' -> t ctx -> f (t ctx')
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 Weaken Proxy where
     weaken :: forall (n :: Ctx) (m :: Ctx). Wk n m -> Proxy n -> Proxy m
weaken Wk n m
_ Proxy n
_ = Proxy m
forall {k} (t :: k). Proxy t
Proxy

instance Rename Proxy where
    rename :: forall (n :: Ctx) (m :: Ctx). Ren n m -> Proxy n -> Proxy m
rename Ren n m
_ Proxy n
_ = Proxy m
forall {k} (t :: k). Proxy t
Proxy

instance RenameA Proxy where
    grename :: forall (m :: Ctx -> Ctx -> *) (f :: * -> *) (ctx :: Ctx)
       (ctx' :: Ctx).
IdxMapping f m =>
m ctx ctx' -> Proxy ctx -> f (Proxy ctx')
grename m ctx ctx'
_ Proxy ctx
_ = Proxy ctx' -> f (Proxy ctx')
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Proxy ctx'
forall {k} (t :: k). Proxy t
Proxy

instance Weaken Idx where
    weaken :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Idx ctx -> Idx ctx'
weaken = Wk n m -> Idx n -> Idx m
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Idx ctx -> Idx ctx'
weakenIdx

instance Rename Idx where
    rename :: forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Idx ctx -> Idx ctx'
rename = Ren n m -> Idx n -> Idx m
forall (ctx :: Ctx) (ctx' :: Ctx).
Ren ctx ctx' -> Idx ctx -> Idx ctx'
renameIdx

instance RenameA Idx where
    grename :: forall (m :: Ctx -> Ctx -> *) (f :: * -> *) (ctx :: Ctx)
       (ctx' :: Ctx).
IdxMapping f m =>
m ctx ctx' -> Idx ctx -> f (Idx ctx')
grename = m ctx ctx' -> Idx ctx -> f (Idx ctx')
forall (ctx :: Ctx) (ctx' :: Ctx).
m ctx ctx' -> Idx ctx -> f (Idx ctx')
forall (f :: * -> *) (t :: Ctx -> Ctx -> *) (ctx :: Ctx)
       (ctx' :: Ctx).
IdxMapping f t =>
t ctx ctx' -> Idx ctx -> f (Idx ctx')
mapIdx

instance Weaken (Ren n) where
    weaken :: forall (n :: Ctx) (m :: Ctx). Wk n m -> Ren n n -> Ren n m
weaken Wk n m
w (MkRen Env n (Idx n)
js) = Env n (Idx m) -> Ren n m
forall (ctx :: Ctx) (ctx' :: Ctx).
Env ctx (Idx ctx') -> Ren ctx ctx'
MkRen ((Idx n -> Idx m) -> Env n (Idx n) -> Env n (Idx m)
forall a b. (a -> b) -> Env n a -> Env n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Wk n m -> Idx n -> Idx m
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Idx ctx -> Idx ctx'
forall (t :: Ctx -> *) (n :: Ctx) (m :: Ctx).
Weaken t =>
Wk n m -> t n -> t m
weaken Wk n m
w) Env n (Idx n)
js)

instance Rename (Ren n) where
    rename :: forall (n :: Ctx) (m :: Ctx). Ren n m -> Ren n n -> Ren n m
rename Ren n m
r Ren n n
r' = Ren n n -> Ren n m -> Ren n m
forall (ctx :: Ctx) (ctx' :: Ctx) (ctx'' :: Ctx).
Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''
compRen Ren n n
r' Ren n m
r