module CC.Term

import CC.Name

-- Definition ------------------------------------------------------------------

public export
Context : Type
Context = SnocList Name

public export
data IsVar : Nat -> Name -> Context -> Type where
  Here : (eq : m ~~ n) -> IsVar 0 m (ctx :< n)
  There : IsVar k n ctx -> IsVar (S k) n (ctx :< _)

public export
data Term : Context -> Type where
  Var : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Term ctx
  Abs : (n : Name) -> Term (ctx :< n) -> Term ctx
  App : Term ctx -> Term ctx -> Term ctx
  Let : (n : Name) -> Term ctx -> Term (ctx :< n) -> Term ctx

public export
data Value : Context -> Type
public export
data Neutral : Context -> Type
public export
data Closure : Context -> Type

public export
data Env : (local, global : Context) -> Type where
  Lin  : Env [<] global
  (:<) : Env local global -> (p : (Name, Lazy (Value global))) -> Env (local :< fst p) global

data Closure : Context -> Type where
  Close : (n : Name) -> Env local global -> Term (local :< n) -> Closure global

data Value where
  Ntrl : Neutral ctx -> Value ctx
  VAbs : Closure ctx -> Value ctx

data Neutral where
  VVar : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Neutral ctx
  VApp : Neutral ctx -> Lazy (Value ctx) -> Neutral ctx

%name IsVar prf
%name Term t, u
%name Value v
%name Neutral n
%name Closure close
%name Env env

-- Operations ------------------------------------------------------------------

export
index : Env local global -> (k : Nat) -> (0 prf : IsVar k n local) -> Value global
index (env :< (n, v)) 0 (Here eq) = v
index (env :< _) (S k) (There prf) = index env k prf