module Quox.Reduce

import public Quox.Syntax

%default total


public export
data IsRedexT : Term d n -> Type where
  IsUpsilonT : IsRedexT $ E (_ :# _)
  IsCloT     : IsRedexT $ CloT {}
  IsDCloT    : IsRedexT $ DCloT {}

public export %inline
NotRedexT : Term d n -> Type
NotRedexT = Not . IsRedexT

public export
data IsRedexE : Elim d n -> Type where
  IsUpsilonE : IsRedexE $ E _ :# _
  IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
  IsCloE     : IsRedexE $ CloE {}
  IsDCloE    : IsRedexE $ DCloE {}

public export %inline
NotRedexE : Elim d n -> Type
NotRedexE = Not . IsRedexE


export %inline
isRedexT : (t : Term d n) -> Dec (IsRedexT t)
isRedexT (E (_ :# _))   = Yes IsUpsilonT
isRedexT (CloT {})      = Yes IsCloT
isRedexT (DCloT {})     = Yes IsDCloT
isRedexT (TYPE _)       = No $ \x => case x of {}
isRedexT (Pi {})        = No $ \x => case x of {}
isRedexT (Lam {})       = No $ \x => case x of {}
isRedexT (E (F _))      = No $ \x => case x of {}
isRedexT (E (B _))      = No $ \x => case x of {}
isRedexT (E (_ :@ _))   = No $ \x => case x of {}
isRedexT (E (CloE {}))  = No $ \x => case x of {}
isRedexT (E (DCloE {})) = No $ \x => case x of {}

export %inline
isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
isRedexE (E _ :# _)                    = Yes IsUpsilonE
isRedexE ((Lam {} :# Pi {}) :@ _)      = Yes IsBetaLam
isRedexE (CloE {})                     = Yes IsCloE
isRedexE (DCloE {})                    = Yes IsDCloE
isRedexE (F x)                         = No $ \x => case x of {}
isRedexE (B i)                         = No $ \x => case x of {}
isRedexE (F _                    :@ _) = No $ \x => case x of {}
isRedexE (B _                    :@ _) = No $ \x => case x of {}
isRedexE (_ :@ _                 :@ _) = No $ \x => case x of {}
isRedexE ((TYPE _   :# _)        :@ _) = No $ \x => case x of {}
isRedexE ((Pi {}    :# _)        :@ _) = No $ \x => case x of {}
isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
isRedexE ((CloT {}  :# _)        :@ _) = No $ \x => case x of {}
isRedexE ((DCloT {} :# _)        :@ _) = No $ \x => case x of {}
isRedexE (CloE {}                :@ _) = No $ \x => case x of {}
isRedexE (DCloE {}               :@ _) = No $ \x => case x of {}
isRedexE (TYPE _   :# _)               = No $ \x => case x of {}
isRedexE (Pi {}    :# _)               = No $ \x => case x of {}
isRedexE (Lam {}   :# _)               = No $ \x => case x of {}
isRedexE (CloT {}  :# _)               = No $ \x => case x of {}
isRedexE (DCloT {} :# _)               = No $ \x => case x of {}


public export %inline
RedexTerm : Nat -> Nat -> Type
RedexTerm d n = Subset (Term d n) IsRedexT

public export %inline
NonRedexTerm : Nat -> Nat -> Type
NonRedexTerm d n = Subset (Term d n) NotRedexT


public export %inline
RedexElim : Nat -> Nat -> Type
RedexElim d n = Subset (Elim d n) IsRedexE

public export %inline
NonRedexElim : Nat -> Nat -> Type
NonRedexElim d n = Subset (Elim d n) NotRedexE


||| substitute a term with annotation for the bound variable of a `ScopeTerm`
export %inline
substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
substScope arg argTy (TUnused body) = body

export %inline
stepT' : (s : Term d n) -> IsRedexT s -> Term d n
stepT' (E (s :# _)) IsUpsilonT = s
stepT' (CloT  s th) IsCloT     = pushSubstsTWith' id th s
stepT' (DCloT s th) IsDCloT    = pushSubstsTWith' th id s

export %inline
stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n

export %inline
stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
stepE' (E e :# _) IsUpsilonE = e
stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
  substScope s arg body :# substScope s arg res
stepE' (CloE  e th) IsCloE  = pushSubstsEWith' id th e
stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e

export %inline
stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n

export covering
whnfT : Term d n -> NonRedexTerm d n
whnfT s = case stepT s of
               Right s'   => whnfT s'
               Left  done => Element s done

export covering
whnfE : Elim d n -> NonRedexElim d n
whnfE e = case stepE e of
               Right e'   => whnfE e'
               Left  done => Element e done