quox/lib/Quox/Displace.idr
2023-09-18 21:53:38 +02:00

90 lines
3.5 KiB
Idris

module Quox.Displace
import Quox.Syntax
%default total
parameters (k : Universe)
namespace Term
export doDisplace : Term d n -> Term d n
export doDisplaceS : ScopeTermN s d n -> ScopeTermN s d n
export doDisplaceDS : DScopeTermN s d n -> DScopeTermN s d n
namespace Elim
export doDisplace : Elim d n -> Elim d n
namespace Term
doDisplace (TYPE l loc) = TYPE (k + l) loc
doDisplace (Pi qty arg res loc) =
Pi qty (doDisplace arg) (doDisplaceS res) loc
doDisplace (Lam body loc) = Lam (doDisplaceS body) loc
doDisplace (Sig fst snd loc) = Sig (doDisplace fst) (doDisplaceS snd) loc
doDisplace (Pair fst snd loc) = Pair (doDisplace fst) (doDisplace snd) loc
doDisplace (Enum cases loc) = Enum cases loc
doDisplace (Tag tag loc) = Tag tag loc
doDisplace (Eq ty l r loc) =
Eq (doDisplaceDS ty) (doDisplace l) (doDisplace r) loc
doDisplace (DLam body loc) = DLam (doDisplaceDS body) loc
doDisplace (Nat loc) = Nat loc
doDisplace (Zero loc) = Zero loc
doDisplace (Succ p loc) = Succ (doDisplace p) loc
doDisplace (BOX qty ty loc) = BOX qty (doDisplace ty) loc
doDisplace (Box val loc) = Box (doDisplace val) loc
doDisplace (E e) = E (doDisplace e)
doDisplace (CloT (Sub t th)) =
CloT (Sub (doDisplace t) (assert_total $ map doDisplace th))
doDisplace (DCloT (Sub t th)) =
DCloT (Sub (doDisplace t) th)
doDisplaceS (S names (Y body)) = S names $ Y $ doDisplace body
doDisplaceS (S names (N body)) = S names $ N $ doDisplace body
doDisplaceDS (S names (Y body)) = S names $ Y $ doDisplace body
doDisplaceDS (S names (N body)) = S names $ N $ doDisplace body
namespace Elim
doDisplace (F x u loc) = F x (k + u) loc
doDisplace (B i loc) = B i loc
doDisplace (App fun arg loc) = App (doDisplace fun) (doDisplace arg) loc
doDisplace (CasePair qty pair ret body loc) =
CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc
doDisplace (Fst pair loc) = Fst (doDisplace pair) loc
doDisplace (Snd pair loc) = Snd (doDisplace pair) loc
doDisplace (CaseEnum qty tag ret arms loc) =
CaseEnum qty (doDisplace tag) (doDisplaceS ret)
(assert_total $ map doDisplace arms) loc
doDisplace (CaseNat qty qtyIH nat ret zero succ loc) =
CaseNat qty qtyIH (doDisplace nat) (doDisplaceS ret)
(doDisplace zero) (doDisplaceS succ) loc
doDisplace (CaseBox qty box ret body loc) =
CaseBox qty (doDisplace box) (doDisplaceS ret) (doDisplaceS body) loc
doDisplace (DApp fun arg loc) =
DApp (doDisplace fun) arg loc
doDisplace (Ann tm ty loc) =
Ann (doDisplace tm) (doDisplace ty) loc
doDisplace (Coe ty p q val loc) =
Coe (doDisplaceDS ty) p q (doDisplace val) loc
doDisplace (Comp ty p q val r zero one loc) =
Comp (doDisplace ty) p q (doDisplace val) r
(doDisplaceDS zero) (doDisplaceDS one) loc
doDisplace (TypeCase ty ret arms def loc) =
TypeCase (doDisplace ty) (doDisplace ret)
(assert_total $ map doDisplaceS arms) (doDisplace def) loc
doDisplace (CloE (Sub e th)) =
CloE (Sub (doDisplace e) (assert_total $ map doDisplace th))
doDisplace (DCloE (Sub e th)) =
DCloE (Sub (doDisplace e) th)
namespace Term
export
displace : Universe -> Term d n -> Term d n
displace 0 t = t
displace u t = doDisplace u t
namespace Elim
export
displace : Universe -> Elim d n -> Elim d n
displace 0 t = t
displace u t = doDisplace u t