module CC.Term.Eval

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

import Data.SnocList.Elem

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

export
app : (n : Name) -> Env local global -> Term (local :< n) -> Lazy (Value global) -> Value global
export
eval : Env local global -> Term local -> Value global

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

eval env (Var k n prf) = index env k prf
eval env (Let n ty val t) = eval (env :< (n, eval env val)) t
eval env Set = VSet
eval env (Pi Nothing t u) = VFunc env t u
eval env (Pi (Just n) t u) = VPi n (eval env t) env u
eval env (Abs n t) = VAbs env n t
eval env (App t u) =
  case eval env t of
    Ntrl n => Ntrl $ VApp n (eval env u)
    VAbs env' n t => assert_total $ app n env' t (eval env u)
    _ => assert_total $ idris_crash "eval invariant broken"

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

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

quote (Ntrl n) = quoteNtrl n
quote VSet = Set
quote (VPi n t env u) =
  Pi (Just n)
    (quote t)
    (assert_total $ quote $ eval (liftEnv [<n] env) u)
quote (VFunc env t u) =
  Pi Nothing
    (assert_total $ quote $ eval env t)
    (assert_total $ quote $ eval env u)
quote (VAbs env n t) =
  Abs n $ assert_total $ quote $ app n (wknEnv env (drop id)) t (Ntrl $ VVar 0 _ $ fromElem Here)

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

-- Conversion ------------------------------------------------------------------

export
convert : {ctx : Context} -> Value ctx -> Value ctx -> Bool
convertNtrl : {ctx : Context} -> Neutral ctx -> Neutral ctx -> Bool

convert VSet VSet = True

convert (VFunc env t u) (VFunc env' t' u') =
  assert_total $
  convert (eval env t) (eval env' t') &&
  convert (eval env u) (eval env' u')
convert (VFunc env t u) (VPi m t' env' u') =
  assert_total $
  convert (eval env t) t' &&
  convert (eval (wknEnv env (drop id)) u) (eval (liftEnv [<m] env') u')
convert (VPi n t env u) (VFunc env' t' u') =
  assert_total $
  convert t (eval env' t') &&
  convert (eval (liftEnv [<n] env) u) (eval (wknEnv env' (drop id)) u')
convert (VPi n t env u) (VPi m t' env' u') =
  convert t t' &&
  (assert_total $ convert (eval (liftEnv [<n] env) u) (eval (liftEnv [<n] env') $ renTerm Refl u'))

convert (VAbs env n t) (VAbs env' m u) =
  assert_total $
  convert (eval (liftEnv [<n] env) t) (eval (liftEnv [<n] env') $ renTerm Refl u)
convert (VAbs env n t) (Ntrl m) =
  assert_total $
  convert
    (eval (liftEnv [<n] env) t)
    (Ntrl (VApp (wknNtrl m (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here)))
convert (Ntrl n)  (VAbs env m t) =
  assert_total $
  convert
    (Ntrl (VApp (wknNtrl n (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here)))
    (eval (liftEnv [<m] env) t)

convert (Ntrl n) (Ntrl m) = convertNtrl n m

convert _ _ = False

convertNtrl (VVar k _ _) (VVar j _ _) = k == j
convertNtrl (VApp n v) (VApp m u) = convertNtrl n m && convert v u
convertNtrl _ _ = False