130 lines
4.6 KiB
Idris
130 lines
4.6 KiB
Idris
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
|