open import Graded.Modality
open import Tools.Nullary
open import Tools.PropositionalEquality
module Graded.Erasure.Extraction {a} {M : Set a} (π : Modality M)
(open Modality π)
(is-π? : (p : M) β Dec (p β‘ π)) where
open import Tools.Function
open import Tools.Nat
open import Definition.Untyped M as U
open import Graded.Erasure.Target as T
private
variable
m n : Nat
Ξ : Con U.Term n
A t tβ² u : U.Term n
v vβ² w : T.Term n
p : M
erase-prodrecΟ : (p : M) (t : T.Term n) (u : T.Term (1+ (1+ n)))
β T.Term n
erase-prodrecΟ p t u = case is-π? p of Ξ» where
(yes pβ‘π) β T.prodrec (T.prod β― t) u
(no pβ’π) β T.prodrec t u
erase : U.Term n β T.Term n
erase (var x) = T.var x
erase U = β―
erase (Ξ Ξ£β¨ _ β© _ , _ β· _ βΉ _) = β―
erase (U.lam p t) = T.lam (erase t)
erase (t ββ¨ p β© u) = case is-π? p of Ξ» where
(yes pβ‘π) β erase t T.β β―
(no pβ’π) β erase t T.β erase u
erase (U.prod _ p t u) = case is-π? p of Ξ» where
(yes pβ‘π) β erase u
(no pβ’π) β T.prod (erase t) (erase u)
erase (U.fst p t) = case is-π? p of Ξ» where
(yes pβ‘π) β β―
(no pβ’π) β T.fst (erase t)
erase (U.snd p t) = case is-π? p of Ξ» where
(yes pβ‘π) β erase t
(no pβ’π) β T.snd (erase t)
erase (U.prodrec r p _ _ t u) = case is-π? r of Ξ» where
(yes rβ‘π) β T.prodrec (T.prod β― β―) (erase u)
(no rβ’π) β erase-prodrecΟ p (erase t) (erase u)
erase β = β―
erase U.zero = T.zero
erase (U.suc t) = T.suc (erase t)
erase (U.natrec p q r A z s n) = T.natrec (erase z) (erase s) (erase n)
erase Unit = β―
erase U.star = T.star
erase Empty = β―
erase (emptyrec p A t) = β―
eraseSubst : U.Subst m n β T.Subst m n
eraseSubst Ο x = erase (Ο x)
eraseWk : U.Wk m n β T.Wk m n
eraseWk id = id
eraseWk (step Ο) = step (eraseWk Ο)
eraseWk (lift Ο) = lift (eraseWk Ο)