{-# LANGUAGE Safe #-}
module DeBruijn.RenExtras (
    weakenUsingSize,
) where

import DeBruijn.Ctx
import DeBruijn.Ren
import DeBruijn.Size
import DeBruijn.Wk

-- | Weaken closed term to arbitrary context.
--
-- Note: this has different requirements than 'sinkSize'.
weakenUsingSize :: Renamable t => Size ctx -> t EmptyCtx -> t ctx
weakenUsingSize :: forall (t :: Ctx -> *) (ctx :: Ctx).
Renamable t =>
Size ctx -> t EmptyCtx -> t ctx
weakenUsingSize Size ctx
s0 = Wk EmptyCtx ctx -> t EmptyCtx -> t ctx
forall (n :: Ctx) (m :: Ctx). Wk n m -> t n -> t m
forall (t :: Ctx -> *) (n :: Ctx) (m :: Ctx).
Renamable t =>
Wk n m -> t n -> t m
weaken (Size ctx -> Wk EmptyCtx ctx
forall (ctx :: Ctx). Size ctx -> Wk EmptyCtx ctx
go Size ctx
s0) where
    go :: Size ctx -> Wk EmptyCtx ctx
    go :: forall (ctx :: Ctx). Size ctx -> Wk EmptyCtx ctx
go Size ctx
SZ     = Wk EmptyCtx ctx
Wk EmptyCtx EmptyCtx
forall (ctx :: Ctx). Wk ctx ctx
IdWk
    go (SS Size ctx1
s) = Wk EmptyCtx ctx1 -> Wk EmptyCtx ctx
forall (b :: Ctx) (a :: Ctx) (b' :: Ctx).
(b ~ S b') =>
Wk a b' -> Wk a b
SkipWk (Size ctx1 -> Wk EmptyCtx ctx1
forall (ctx :: Ctx). Size ctx -> Wk EmptyCtx ctx
go Size ctx1
s)