Context.hs

-- |
-- Module       : Rebound.Context
-- Description  : Typing contexts
module Rebound.Context(Ctx, emptyC, (+++), (++++)) where

import Rebound.Lib
import Rebound.Env
import Rebound.Classes

----------------------------------------------------------------
-- Typing context utilities for dependently-typed languages
----------------------------------------------------------------

-- | A typing context maps indices to type in the same scope.
type Ctx v n = Env v n n

-- This is not weakening --- it increments all variables by one
shiftC :: forall v n. (SubstVar v) => v n -> v (S n)
shiftC = applyE @v shift1E

shiftCtx :: (SubstVar v) => Env v n n -> Env v n (S n)
shiftCtx g = g .>> shift1E

-- | An empty context, that includes no variable assumptions
emptyC :: Ctx v N0
emptyC = zeroE

-- | "Snoc" a new definition to the end of the context
-- All existing types in the context need to be shifted (lazily)
(+++) :: forall v n. (SubstVar v) => Ctx v n -> v n -> Ctx v (S n)
g +++ a = applyE @v shift1E a .: (g .>> shift1E)


-- | Append contexts. Shifts all indices in the first argument by the length
-- of the second.
(++++) :: forall v n n' m. (SNatI n', SubstVar v) => Env v n m -> Env v n' (n' + m) -> Env v (n' + n) (n' + m)
l ++++ r =
  let p = snat @n'
   in r .++ (l .>> shiftNE p)


-- Example usage

data Exp n = Star | Var (Fin n) deriving Show
instance SubstVar Exp where var = Var
instance Subst Exp Exp where
    applyE s Star = Star
    applyE s (Var x) = applyEnv s x


-- c :: Ctx Exp N4
-- x : * , y : x, z : x , w : *
c = emptyC +++ Star +++ Var FZ +++ Var (FS FZ) +++ Star

-- >>> applyEnv c (FS FZ)
-- Var 3