module CC.Term.Eval

import CC.Name
import CC.Term
import CC.Thinning

-- Evaluation ------------------------------------------------------------------

export
app : Closure ctx -> Lazy (Value ctx) -> Value ctx
export
eval : Env local global -> Term local -> Value global

app (Close n env t) v = assert_total $ eval (env :< (n, v)) t

eval env (Var k n prf) = index env k prf
eval env (Abs n t) = VAbs (Close n env t)
eval env (App t u) =
  case eval env t of
    Ntrl n => Ntrl $ VApp n (eval env u)
    VAbs close => app close (eval env u)
eval env (Let n t u) = eval (env :< (n, eval env t)) u

-- Quoting ---------------------------------------------------------------------

export
quote : {ctx : _} -> Value ctx -> Term ctx
quoteNtrl : {ctx : _} -> Neutral ctx -> Term ctx

quote (Ntrl n) = quoteNtrl n
quote (VAbs close@(Close n _ _)) =
  Abs n $
  assert_total $
  quote $
  app (wknClose close (drop id)) (Ntrl $ VVar 0 n $ Here $ reflexive {rel = (~~)})

quoteNtrl (VVar k n prf) = Var k n prf
quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v)

export
normalise : {global : _} -> Env local global -> Term local -> Term global
normalise env t = quote $ eval env t