HSubst.idr

module HSubst

%default total

infixr 0 >>>
data Ty = O | (>>>) Ty Ty
%name Ty a, b, c

namespace Ctx
  data Ctx = Nil | (::) Ty Ctx
  %name Ctx ctx, ctx'

data Var : Ctx -> Ty -> Type where
  Z : Var (a :: ctx) a
  S : Var ctx a -> Var (b :: ctx) a
%name H.Var x, y, z

(-) : (ctx : _) -> Var ctx a -> Ctx
[]         - Z     impossible
[]         - (S _) impossible
(t :: ctx) - Z     = ctx
(a :: ctx) - (S x) = a :: (ctx - x)

wkv : (x : Var ctx a) -> Var (ctx - x) b -> Var ctx b
wkv Z y         = S y
wkv (S x) Z     = Z
wkv (S x) (S y) = S (wkv x y)


data EqV : Var ctx a -> Var ctx b -> Type where
  Same : EqV a a
  Diff : (x : Var ctx a) -> (y : Var (ctx - x) b) -> EqV x (wkv x y)

eq : (x : Var ctx a) -> (y : Var ctx b) -> EqV x y
eq Z Z = Same
eq Z (S x) = Diff Z x
eq (S x) Z = Diff (S x) Z
eq (S x) (S y) with (eq x y)
  eq (S x) (S x)         | Same       = Same
  eq (S x) (S (wkv x z)) | (Diff x z) = Diff (S x) (S z)

mutual
  data Nf : Ctx -> Ty -> Type where
    L : Nf (a :: ctx) b -> Nf ctx (a >>> b)
    N : Ne ctx O -> Nf ctx O
  %name Nf n, m

  data Ne : Ctx -> Ty -> Type where
    A : Var ctx a -> Sp ctx a b -> Ne ctx b
  %name Ne n, m

  namespace Sp
    data Sp : Ctx -> Ty -> Ty -> Type where
      Nil : Sp ctx a a
      (::) : Nf ctx a -> Sp ctx b c -> Sp ctx (a >>> b) c
    %name Sp s, r

mutual
  wkNf : (x : Var ctx a) -> Nf (ctx - x) b -> Nf ctx b
  wkNf x (L n) = L $ wkNf (S x) n
  wkNf x (N (A y s)) = N $ A (wkv x y) (wkSp x s)

  wkSp : (x : Var ctx a) -> Sp (ctx - x) c b -> Sp ctx c b

appSp : Sp ctx a (b >>> c) -> Nf ctx b -> Sp ctx a c
appSp []       n = [n]
appSp (m :: s) n = m :: appSp s n


mutual
  nvar : Var ctx a -> Nf ctx a
  nvar x = ne2nf $ A x []

  ne2nf : Ne ctx a -> Nf ctx a
  ne2nf {a = O}         n       = N n
  ne2nf {a = (a >>> b)} (A x s) = L $ ne2nf $ A (S x) $ appSp (wkSp Z s) (nvar Z)


mutual
  napp : Nf ctx (a >>> b) -> Nf ctx a -> Nf ctx b
  napp (L n) m = substNf n Z m

  substNf : Nf ctx a -> (x : Var ctx b) -> Nf (ctx - x) b -> Nf (ctx - x) a
  substNf (L n) x m = L $ substNf n (S x) (wkNf Z m)
  substNf (N (A y s)) x m with (eq x y)
    substNf (N (A y s))         y m | Same =
        nfsp m (substSp s y m)
    substNf (N (A (wkv x w) s)) x m | (Diff x w) =
        N $ A w $ substSp s x m

  substSp : Sp ctx a b -> (x : Var ctx c) -> Nf (ctx - x) c ->
            Sp (ctx - x) a b
  substSp [] x n = []
  substSp (m :: s) x n = substNf m x n :: substSp s x n

  nfsp : Nf ctx a -> Sp ctx a b -> Nf ctx b
  nfsp n [] = n
  nfsp n (m :: s) = nfsp (napp n m) s