pi/src/Core/Normalize.idr

module Core.Normalize

import Core.Term
import Core.Value
import Core.Misc

import Control.Monad.RWS
import Control.Monad.Identity
import Control.Monad.Either

import Data.Nat
import Data.Vect

%default total

mutual
  public export
  app : Value -> Value -> PI Value
  app (VClos env (TLam sc))       x = eval (x :: env) sc

  app (VClos env (TTopInd c st)) VTop = eval env st
  app f@(VClos env (TTopInd c st))  x = logS ("⊤-ind applied to " ++ show x)
                                               >> pure (VApp f x)

  app (VClos env (TNatInd _ z s)) (VNatTr n) = do
    z'  <- eval env z
    s'  <- eval env s
    assert_total (nind z' s' n) -- :(
    where
      nind : Value -> Value -> Nat -> PI Value
      nind z s 0     = pure z
      nind z s (S n) = do
        rec <- nind z s n
        sn <- app s (VNatTr n)
        app sn rec

  app f@(VClos env (TNatInd _ z s)) x = logS ("ℕ-ind applied to " ++ show x)
                                        >> pure (VApp f x)

  app (VClos env (TSigInd _ _ c f)) (VPair a b) = do
    f' <- eval env f
    fa <- app f' a
    app fa b

  app f@(VClos env (TSigInd _ _ c p)) x = logS ("Σ-ind applied to " ++ show x)
                                          >> pure (VApp f x)

  app f x = pure (VApp f x)

  public export
  eval : Ctx n -> Term n -> PI Value
  eval env (TVar i)   = pure (index i env)
  eval env TType       = pure VType
  eval env TTop        = pure VTop
  eval env TStar       = pure VStar
  eval env TBot        = pure VBot
  eval env TNat        = pure VNat
  eval env TZero       = pure (VNatTr 0)
  eval env (TApp f x)  = do
    f' <- eval env f
    x' <- eval env x
    assert_total (app f' x') -- :(

  eval env (TSuc n)    = do
    n' <- eval env n
    case n' of
         VNatTr n => pure (VNatTr (S n))
         x        => logS ("suc applied to " ++ show x)
                     >> pure (VClos env (TSuc n))

  eval env (TPair a b) = do
    a' <- eval env a
    b' <- eval env b
    pure (VPair a' b')

  eval env (TLet ty tr tri) = do
    tr' <- eval env tr
    eval (tr' :: env) tri

  eval env tr         = pure (VClos env tr)

public export
whnf : Value -> PI Value
whnf (VClos env tr) = eval env tr
whnf (VApp f x) = do
  f' <- whnf f
  x' <- whnf x
  app f' x'
whnf (VPair a b) = do
  a' <- whnf a
  b' <- whnf b
  pure (VPair a' b')
whnf v              = pure v