{-# LANGUAGE Safe #-}
module DeBruijn.Wk (
    Wk(IdWk, SkipWk, KeepWk),
    -- * Combinators
    wk1,
    compWk,
    -- * Index weakening
    weakenIdx,
    -- * Size weakening
    weakenSize,
    contractSize,
    -- * Environment contraction
    weakenEnv,
    setWeakenEnv,
    overWeakenEnv,
) where

import Data.Kind (Type)

import DeBruijn.Ctx
import DeBruijn.Env
import DeBruijn.Idx
import DeBruijn.Size

-- $setup
-- >>> :set -XGADTs
-- >>> import DeBruijn
-- >>> import Data.Function ((&))
-- >>> import Data.Char (toUpper)

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

type Wk1 :: Ctx -> Ctx -> Type
data Wk1 ctx ctx' where
    Wk1     ::                 Wk1    ctx   (S ctx)
    KeepWk1 :: Wk1 ctx ctx' -> Wk1 (S ctx)  (S ctx')
    SkipWk1 :: Wk1 ctx ctx' -> Wk1    ctx   (S ctx')

deriving instance Eq (Wk ctx ctx')
deriving instance Eq (Wk1 ctx ctx')

-- | Keep variable.
keepWk :: Wk ctx ctx' -> Wk (S ctx) (S ctx')
keepWk :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Wk (S ctx) (S ctx')
keepWk Wk ctx ctx'
IdWk     = Wk (S ctx) (S ctx)
Wk (S ctx) ('S ctx')
forall (ctx :: Ctx). Wk ctx ctx
IdWk
keepWk (NeWk Wk1 ctx ctx'
w) = Wk1 (S ctx) ('S ctx') -> Wk (S ctx) ('S ctx')
forall (ctx :: Ctx) (ctx' :: Ctx). Wk1 ctx ctx' -> Wk ctx ctx'
NeWk (Wk1 ctx ctx' -> Wk1 (S ctx) ('S ctx')
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Wk1 (S ctx) (S ctx')
KeepWk1 Wk1 ctx ctx'
w)

-- | Skip variable.
skipWk :: Wk ctx ctx' -> Wk ctx (S ctx')
skipWk :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Wk ctx (S ctx')
skipWk Wk ctx ctx'
IdWk     = Wk ctx (S ctx)
Wk ctx ('S ctx')
forall (ctx :: Ctx). Wk ctx (S ctx)
wk1
skipWk (NeWk Wk1 ctx ctx'
w) = Wk1 ctx ('S ctx') -> Wk ctx ('S ctx')
forall (ctx :: Ctx) (ctx' :: Ctx). Wk1 ctx ctx' -> Wk ctx ctx'
NeWk (Wk1 ctx ctx' -> Wk1 ctx ('S ctx')
forall (ctx :: Ctx) (ctx :: Ctx). Wk1 ctx ctx -> Wk1 ctx (S ctx)
SkipWk1 Wk1 ctx ctx'
w)

viewWk :: Wk ctx ctx' -> ViewWk ctx ctx'
viewWk :: forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> ViewWk ctx ctx'
viewWk Wk ctx ctx'
IdWk               = ViewWk ctx ctx
ViewWk ctx ctx'
forall (ctx :: Ctx). ViewWk ctx ctx
IdWk'
viewWk (NeWk Wk1 ctx ctx'
Wk1)         = Wk ctx ctx -> ViewWk ctx ('S ctx)
forall (ctx :: Ctx) (ctx :: Ctx). Wk ctx ctx -> ViewWk ctx (S ctx)
SkipWk' Wk ctx ctx
forall (ctx :: Ctx). Wk ctx ctx
IdWk
viewWk (NeWk (SkipWk1 Wk1 ctx ctx'
w)) = Wk ctx ctx' -> ViewWk ctx ('S ctx')
forall (ctx :: Ctx) (ctx :: Ctx). Wk ctx ctx -> ViewWk ctx (S ctx)
SkipWk' (Wk1 ctx ctx' -> Wk ctx ctx'
forall (ctx :: Ctx) (ctx' :: Ctx). Wk1 ctx ctx' -> Wk ctx ctx'
NeWk Wk1 ctx ctx'
w)
viewWk (NeWk (KeepWk1 Wk1 ctx ctx'
w)) = Wk ctx ctx' -> ViewWk ('S ctx) ('S ctx')
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> ViewWk (S ctx) (S ctx')
KeepWk' (Wk1 ctx ctx' -> Wk ctx ctx'
forall (ctx :: Ctx) (ctx' :: Ctx). Wk1 ctx ctx' -> Wk ctx ctx'
NeWk Wk1 ctx ctx'
w)

type ViewWk :: Ctx -> Ctx -> Type
data ViewWk ctx ctx' where
    IdWk'   :: ViewWk ctx ctx
    SkipWk' :: Wk ctx ctx' -> ViewWk    ctx  (S ctx')
    KeepWk' :: Wk ctx ctx' -> ViewWk (S ctx) (S ctx')

pattern KeepWk :: () => (a ~ S a', b ~ S b') => Wk a' b' -> Wk a b
pattern $mKeepWk :: forall {r} {a :: Ctx} {b :: Ctx}.
Wk a b
-> (forall {a' :: Ctx} {b' :: Ctx}.
    (a ~ S a', b ~ S b') =>
    Wk a' b' -> r)
-> ((# #) -> r)
-> r
$bKeepWk :: forall (a :: Ctx) (b :: Ctx) (a' :: Ctx) (b' :: Ctx).
(a ~ S a', b ~ S b') =>
Wk a' b' -> Wk a b
KeepWk w <- (viewWk -> KeepWk' w)
  where KeepWk Wk a' b'
w = Wk a' b' -> Wk (S a') (S b')
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Wk (S ctx) (S ctx')
keepWk Wk a' b'
w

pattern SkipWk :: () => (b ~ S b') => Wk a b' -> Wk a b
pattern $mSkipWk :: forall {r} {b :: Ctx} {a :: Ctx}.
Wk a b
-> (forall {b' :: Ctx}. (b ~ S b') => Wk a b' -> r)
-> ((# #) -> r)
-> r
$bSkipWk :: forall (b :: Ctx) (a :: Ctx) (b' :: Ctx).
(b ~ S b') =>
Wk a b' -> Wk a b
SkipWk w <- (viewWk -> SkipWk' w)
  where SkipWk Wk a b'
w = Wk a b' -> Wk a (S b')
forall (ctx :: Ctx) (ctx' :: Ctx). Wk ctx ctx' -> Wk ctx (S ctx')
skipWk Wk a b'
w

{-# COMPLETE IdWk, SkipWk, KeepWk #-}

instance Show (Wk ctx ctx') where
    showsPrec :: Int -> Wk ctx ctx' -> ShowS
showsPrec Int
_ Wk ctx ctx'
IdWk       = String -> ShowS
showString String
"IdWk"
    showsPrec Int
d (KeepWk Wk a' b'
w) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"KeepWk " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Wk a' b' -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Wk a' b'
w
    showsPrec Int
d (SkipWk Wk ctx b'
w) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"SkipWk " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Wk ctx b' -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Wk ctx b'
w

-- | Weaken by one. @'wk1' = 'SkipWk' 'IdWk'@.
wk1 :: Wk ctx (S ctx)
wk1 :: forall (ctx :: Ctx). Wk ctx (S ctx)
wk1 = Wk1 ctx (S ctx) -> Wk ctx (S ctx)
forall (ctx :: Ctx) (ctx' :: Ctx). Wk1 ctx ctx' -> Wk ctx ctx'
NeWk Wk1 ctx (S ctx)
forall (ctx :: Ctx). Wk1 ctx (S ctx)
Wk1

-- | Weakening composition.
compWk :: Wk a b -> Wk b c -> Wk a c
compWk :: forall (a :: Ctx) (b :: Ctx) (c :: Ctx). Wk a b -> Wk b c -> Wk a c
compWk Wk a b
IdWk     Wk b c
w'        = Wk a c
Wk b c
w'
compWk (NeWk Wk1 a b
w) Wk b c
IdWk      = Wk1 a c -> Wk a c
forall (ctx :: Ctx) (ctx' :: Ctx). Wk1 ctx ctx' -> Wk ctx ctx'
NeWk Wk1 a b
Wk1 a c
w
compWk (NeWk Wk1 a b
w) (NeWk Wk1 b c
w') = Wk1 a c -> Wk a c
forall (ctx :: Ctx) (ctx' :: Ctx). Wk1 ctx ctx' -> Wk ctx ctx'
NeWk (Wk1 a b -> Wk1 b c -> Wk1 a c
forall (a :: Ctx) (b :: Ctx) (c :: Ctx).
Wk1 a b -> Wk1 b c -> Wk1 a c
compWk1 Wk1 a b
w Wk1 b c
w')

compWk1 :: Wk1  a b -> Wk1 b c -> Wk1 a c
compWk1 :: forall (a :: Ctx) (b :: Ctx) (c :: Ctx).
Wk1 a b -> Wk1 b c -> Wk1 a c
compWk1 Wk1 a b
w           Wk1 b c
Wk1          = Wk1 a b -> Wk1 a ('S b)
forall (ctx :: Ctx) (ctx :: Ctx). Wk1 ctx ctx -> Wk1 ctx (S ctx)
SkipWk1 Wk1 a b
w
compWk1 Wk1 a b
w           (SkipWk1 Wk1 b ctx'
w') = Wk1 a ctx' -> Wk1 a ('S ctx')
forall (ctx :: Ctx) (ctx :: Ctx). Wk1 ctx ctx -> Wk1 ctx (S ctx)
SkipWk1 (Wk1 a b -> Wk1 b ctx' -> Wk1 a ctx'
forall (a :: Ctx) (b :: Ctx) (c :: Ctx).
Wk1 a b -> Wk1 b c -> Wk1 a c
compWk1 Wk1 a b
w Wk1 b ctx'
w')
compWk1 Wk1 a b
Wk1         (KeepWk1 Wk1 ctx ctx'
w') = Wk1 a ctx' -> Wk1 a ('S ctx')
forall (ctx :: Ctx) (ctx :: Ctx). Wk1 ctx ctx -> Wk1 ctx (S ctx)
SkipWk1 Wk1 a ctx'
Wk1 ctx ctx'
w'
compWk1 (SkipWk1 Wk1 a ctx'
w) (KeepWk1 Wk1 ctx ctx'
w') = Wk1 a ctx' -> Wk1 a ('S ctx')
forall (ctx :: Ctx) (ctx :: Ctx). Wk1 ctx ctx -> Wk1 ctx (S ctx)
SkipWk1 (Wk1 a ctx' -> Wk1 ctx' ctx' -> Wk1 a ctx'
forall (a :: Ctx) (b :: Ctx) (c :: Ctx).
Wk1 a b -> Wk1 b c -> Wk1 a c
compWk1 Wk1 a ctx'
w Wk1 ctx' ctx'
Wk1 ctx ctx'
w')
compWk1 (KeepWk1 Wk1 ctx ctx'
w) (KeepWk1 Wk1 ctx ctx'
w') = Wk1 ctx ctx' -> Wk1 ('S ctx) ('S ctx')
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Wk1 (S ctx) (S ctx')
KeepWk1 (Wk1 ctx ctx' -> Wk1 ctx' ctx' -> Wk1 ctx ctx'
forall (a :: Ctx) (b :: Ctx) (c :: Ctx).
Wk1 a b -> Wk1 b c -> Wk1 a c
compWk1 Wk1 ctx ctx'
w Wk1 ctx' ctx'
Wk1 ctx ctx'
w')

-- | Weaken 'Idx', i.e. map index from smaller to larger context.
weakenIdx :: Wk ctx ctx' -> Idx ctx -> Idx ctx'
weakenIdx :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Idx ctx -> Idx ctx'
weakenIdx Wk ctx ctx'
IdWk     Idx ctx
x = Idx ctx
Idx ctx'
x
weakenIdx (NeWk Wk1 ctx ctx'
w) Idx ctx
x = Wk1 ctx ctx' -> Idx ctx -> Idx ctx'
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Idx ctx -> Idx ctx'
weaken1Idx Wk1 ctx ctx'
w Idx ctx
x

weaken1Idx :: Wk1 ctx ctx' -> Idx ctx -> Idx ctx'
weaken1Idx :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Idx ctx -> Idx ctx'
weaken1Idx Wk1 ctx ctx'
Wk1         Idx ctx
x      = Idx ctx -> Idx ('S ctx)
forall (n1 :: Ctx). Idx n1 -> Idx ('S n1)
IS Idx ctx
x
weaken1Idx (SkipWk1 Wk1 ctx ctx'
w) Idx ctx
x      = Idx ctx' -> Idx ('S ctx')
forall (n1 :: Ctx). Idx n1 -> Idx ('S n1)
IS (Wk1 ctx ctx' -> Idx ctx -> Idx ctx'
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Idx ctx -> Idx ctx'
weaken1Idx Wk1 ctx ctx'
w Idx ctx
x)
weaken1Idx (KeepWk1 Wk1 ctx ctx'
_) Idx ctx
IZ     = Idx ctx'
Idx ('S ctx')
forall (n1 :: Ctx). Idx ('S n1)
IZ
weaken1Idx (KeepWk1 Wk1 ctx ctx'
w) (IS Idx n1
x) = Idx ctx' -> Idx ('S ctx')
forall (n1 :: Ctx). Idx n1 -> Idx ('S n1)
IS (Wk1 ctx ctx' -> Idx ctx -> Idx ctx'
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Idx ctx -> Idx ctx'
weaken1Idx Wk1 ctx ctx'
w Idx ctx
Idx n1
x)

-- | Weaken 'Size'.
weakenSize :: Wk ctx ctx' -> Size ctx -> Size ctx'
weakenSize :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Size ctx -> Size ctx'
weakenSize Wk ctx ctx'
IdWk     Size ctx
x = Size ctx
Size ctx'
x
weakenSize (NeWk Wk1 ctx ctx'
w) Size ctx
x = Wk1 ctx ctx' -> Size ctx -> Size ctx'
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Size ctx -> Size ctx'
weaken1Size Wk1 ctx ctx'
w Size ctx
x

weaken1Size :: Wk1 ctx ctx' -> Size ctx -> Size ctx'
weaken1Size :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Size ctx -> Size ctx'
weaken1Size Wk1 ctx ctx'
Wk1         Size ctx
x      = Size ctx -> Size ('S ctx)
forall (ctx1 :: Ctx). Size ctx1 -> Size ('S ctx1)
SS Size ctx
x
weaken1Size (SkipWk1 Wk1 ctx ctx'
w) Size ctx
x      = Size ctx' -> Size ('S ctx')
forall (ctx1 :: Ctx). Size ctx1 -> Size ('S ctx1)
SS (Wk1 ctx ctx' -> Size ctx -> Size ctx'
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Size ctx -> Size ctx'
weaken1Size Wk1 ctx ctx'
w Size ctx
x)
weaken1Size (KeepWk1 Wk1 ctx ctx'
w) (SS Size ctx1
x) = Size ctx' -> Size ('S ctx')
forall (ctx1 :: Ctx). Size ctx1 -> Size ('S ctx1)
SS (Wk1 ctx ctx' -> Size ctx -> Size ctx'
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Size ctx -> Size ctx'
weaken1Size Wk1 ctx ctx'
w Size ctx
Size ctx1
x)

contractSize :: Wk ctx ctx' -> Size ctx' -> Size ctx
contractSize :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk ctx ctx' -> Size ctx' -> Size ctx
contractSize Wk ctx ctx'
IdWk     Size ctx'
x = Size ctx
Size ctx'
x
contractSize (NeWk Wk1 ctx ctx'
w) Size ctx'
x = Wk1 ctx ctx' -> Size ctx' -> Size ctx
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Size ctx' -> Size ctx
contract1Size Wk1 ctx ctx'
w Size ctx'
x

contract1Size :: Wk1 ctx ctx' -> Size ctx' -> Size ctx
contract1Size :: forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Size ctx' -> Size ctx
contract1Size Wk1 ctx ctx'
Wk1         (SS Size ctx1
x) = Size ctx
Size ctx1
x
contract1Size (SkipWk1 Wk1 ctx ctx'
w) (SS Size ctx1
x) = Wk1 ctx ctx' -> Size ctx' -> Size ctx
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Size ctx' -> Size ctx
contract1Size Wk1 ctx ctx'
w Size ctx'
Size ctx1
x
contract1Size (KeepWk1 Wk1 ctx ctx'
w) (SS Size ctx1
x) = Size ctx -> Size ('S ctx)
forall (ctx1 :: Ctx). Size ctx1 -> Size ('S ctx1)
SS (Wk1 ctx ctx' -> Size ctx' -> Size ctx
forall (ctx :: Ctx) (ctx' :: Ctx).
Wk1 ctx ctx' -> Size ctx' -> Size ctx
contract1Size Wk1 ctx ctx'
w Size ctx'
Size ctx1
x)

-- | Contract 'Env' i.e. drop elements from larger context.
--
-- This function explains the 'KeepWk' and 'SkipWk' constructor names:
--
-- >>> weakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b' :> 'c' :> 'd' :> 'e')
-- EmptyEnv :> 'a' :> 'b' :> 'c' :> 'e'
--
weakenEnv :: Wk ctx ctx' -> Env ctx' a -> Env ctx a
weakenEnv :: forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk ctx ctx' -> Env ctx' a -> Env ctx a
weakenEnv Wk ctx ctx'
IdWk     Env ctx' a
xs = Env ctx a
Env ctx' a
xs
weakenEnv (NeWk Wk1 ctx ctx'
w) Env ctx' a
xs = Wk1 ctx ctx' -> Env ctx' a -> Env ctx a
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk1 ctx ctx' -> Env ctx' a -> Env ctx a
weaken1Env Wk1 ctx ctx'
w Env ctx' a
xs

weaken1Env :: Wk1 ctx ctx' -> Env ctx' a -> Env ctx a
weaken1Env :: forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk1 ctx ctx' -> Env ctx' a -> Env ctx a
weaken1Env Wk1 ctx ctx'
Wk1         (Env ctx1 a
xs :> a
_) = Env ctx a
Env ctx1 a
xs
weaken1Env (SkipWk1 Wk1 ctx ctx'
w) (Env ctx1 a
xs :> a
_) = Wk1 ctx ctx' -> Env ctx' a -> Env ctx a
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk1 ctx ctx' -> Env ctx' a -> Env ctx a
weaken1Env Wk1 ctx ctx'
w Env ctx' a
Env ctx1 a
xs
weaken1Env (KeepWk1 Wk1 ctx ctx'
w) (Env ctx1 a
xs :> a
x) = Wk1 ctx ctx' -> Env ctx' a -> Env ctx a
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk1 ctx ctx' -> Env ctx' a -> Env ctx a
weaken1Env Wk1 ctx ctx'
w Env ctx' a
Env ctx1 a
xs Env ctx a -> a -> Env ('S ctx) a
forall (ctx1 :: Ctx) a. Env ctx1 a -> a -> Env ('S ctx1) a
:> a
x

-- | 'setWeakenEnv' and 'weakenEnv' together form a lens.
--
-- >>> setWeakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b') (EmptyEnv :> 'x' :> 'y' :> 'z')
-- EmptyEnv :> 'a' :> 'y' :> 'b'
--
setWeakenEnv :: Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
setWeakenEnv :: forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
setWeakenEnv Wk ctx ctx'
IdWk     Env ctx a
env Env ctx' a
_    = Env ctx a
Env ctx' a
env
setWeakenEnv (NeWk Wk1 ctx ctx'
w) Env ctx a
env Env ctx' a
env' = Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
setWeaken1Env Wk1 ctx ctx'
w Env ctx a
env Env ctx' a
env'

-- | Setter made from 'setWeakenEnv' and 'weakenEnv'.
--
-- >>> overWeakenEnv (IdWk & SkipWk & KeepWk) (fmap toUpper) (EmptyEnv :> 'a' :> 'x' :> 'y' :> 'z')
-- EmptyEnv :> 'A' :> 'X' :> 'y' :> 'Z'
--
overWeakenEnv :: Wk ctx ctx' -> (Env ctx a -> Env ctx a) -> Env ctx' a -> Env ctx' a
overWeakenEnv :: forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk ctx ctx' -> (Env ctx a -> Env ctx a) -> Env ctx' a -> Env ctx' a
overWeakenEnv Wk ctx ctx'
w Env ctx a -> Env ctx a
f Env ctx' a
env = Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
setWeakenEnv Wk ctx ctx'
w (Env ctx a -> Env ctx a
f (Wk ctx ctx' -> Env ctx' a -> Env ctx a
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk ctx ctx' -> Env ctx' a -> Env ctx a
weakenEnv Wk ctx ctx'
w Env ctx' a
env)) Env ctx' a
env

setWeaken1Env :: Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
setWeaken1Env :: forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
setWeaken1Env Wk1 ctx ctx'
Wk1         Env ctx a
xs        (Env ctx1 a
_ :> a
y)  = Env ctx a
xs Env ctx a -> a -> Env ('S ctx) a
forall (ctx1 :: Ctx) a. Env ctx1 a -> a -> Env ('S ctx1) a
:> a
y
setWeaken1Env (SkipWk1 Wk1 ctx ctx'
w) Env ctx a
xs        (Env ctx1 a
ys :> a
y) = Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
setWeaken1Env Wk1 ctx ctx'
w Env ctx a
xs Env ctx' a
Env ctx1 a
ys Env ctx' a -> a -> Env ('S ctx') a
forall (ctx1 :: Ctx) a. Env ctx1 a -> a -> Env ('S ctx1) a
:> a
y
setWeaken1Env (KeepWk1 Wk1 ctx ctx'
w) (Env ctx1 a
xs :> a
x) (Env ctx1 a
ys :> a
_) = Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
forall (ctx :: Ctx) (ctx' :: Ctx) a.
Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
setWeaken1Env Wk1 ctx ctx'
w Env ctx a
Env ctx1 a
xs Env ctx' a
Env ctx1 a
ys Env ctx' a -> a -> Env ('S ctx') a
forall (ctx1 :: Ctx) a. Env ctx1 a -> a -> Env ('S ctx1) a
:> a
x