rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

add converse υ rule for elim

Browse source 
i think this just means type preservation is modulo subtyping. which is
probably fine....?
This commit is contained in:
rhiannon morris 2022-04-27 20:04:29 +02:00
parent 81e1f331e0
commit 6bffd6a11c
1 changed files with 18 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Quox/Reduce.idr
View file

@ -5,7 +5,7 @@ import public Quox.Syntax
public export public export
data IsRedexT : Term d n -> Type where data IsRedexT : Term d n -> Type where
IsUpsilon : IsRedexT $ E (_ :# _) IsUpsilonT : IsRedexT $ E (_ :# _)
IsCloT : IsRedexT $ CloT {} IsCloT : IsRedexT $ CloT {}
IsDCloT : IsRedexT $ DCloT {} IsDCloT : IsRedexT $ DCloT {}
@ -15,6 +15,7 @@ NotRedexT = Not . IsRedexT
public export public export
data IsRedexE : Elim d n -> Type where data IsRedexE : Elim d n -> Type where
IsUpsilonE : IsRedexE $ E _ :# _
IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _ IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _
IsCloE : IsRedexE $ CloE {} IsCloE : IsRedexE $ CloE {}
IsDCloE : IsRedexE $ DCloE {} IsDCloE : IsRedexE $ DCloE {}
@ -26,7 +27,7 @@ NotRedexE = Not . IsRedexE
export %inline export %inline
isRedexT : (t : Term d n) -> Dec (IsRedexT t) isRedexT : (t : Term d n) -> Dec (IsRedexT t)
isRedexT (E (_ :# _)) = Yes IsUpsilon isRedexT (E (_ :# _)) = Yes IsUpsilonT
isRedexT (CloT {}) = Yes IsCloT isRedexT (CloT {}) = Yes IsCloT
isRedexT (DCloT {}) = Yes IsDCloT isRedexT (DCloT {}) = Yes IsDCloT
isRedexT (TYPE _) = No $ \x => case x of {} isRedexT (TYPE _) = No $ \x => case x of {}
@ -40,6 +41,7 @@ isRedexT (E (DCloE {})) = No $ \x => case x of {}
export %inline export %inline
isRedexE : (e : Elim d n) -> Dec (IsRedexE e) isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
isRedexE (E _ :# _) = Yes IsUpsilonE
isRedexE ((Lam {} :# Pi {}) :@ _) = Yes IsBetaLam isRedexE ((Lam {} :# Pi {}) :@ _) = Yes IsBetaLam
isRedexE (CloE {}) = Yes IsCloE isRedexE (CloE {}) = Yes IsCloE
isRedexE (DCloE {}) = Yes IsDCloE isRedexE (DCloE {}) = Yes IsDCloE
@ -60,7 +62,11 @@ isRedexE ((CloT {} :# _) :@ _) = No $ \x => case x of {}
isRedexE ((DCloT {} :# _) :@ _) = No $ \x => case x of {} isRedexE ((DCloT {} :# _) :@ _) = No $ \x => case x of {}
isRedexE (CloE {} :@ _) = No $ \x => case x of {} isRedexE (CloE {} :@ _) = No $ \x => case x of {}
isRedexE (DCloE {} :@ _) = No $ \x => case x of {} isRedexE (DCloE {} :@ _) = 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 {} :# _) = No $ \x => case x of {}
isRedexE (CloT {} :# _) = No $ \x => case x of {}
isRedexE (DCloT {} :# _) = No $ \x => case x of {}
public export %inline public export %inline
@ -89,7 +95,7 @@ substScope arg argTy (TUnused body) = body
export %inline export %inline
stepT' : (s : Term d n) -> IsRedexT s -> Term d n stepT' : (s : Term d n) -> IsRedexT s -> Term d n
stepT' (E (s :# _)) IsUpsilon = s stepT' (E (s :# _)) IsUpsilonT = s
stepT' (CloT s th) IsCloT = pushSubstsTWith' id th s stepT' (CloT s th) IsCloT = pushSubstsTWith' id th s
stepT' (DCloT s th) IsDCloT = pushSubstsTWith' th id s stepT' (DCloT s th) IsDCloT = pushSubstsTWith' th id s
@ -99,6 +105,7 @@ stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
export %inline export %inline
stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
stepE' (E e :# _) IsUpsilonE = e
stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam = stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
substScope s arg body :# substScope s arg res substScope s arg body :# substScope s arg res
stepE' (CloE e th) IsCloE = pushSubstsEWith' id th e stepE' (CloE e th) IsCloE = pushSubstsEWith' id th e