open import Graded.Modality
module Graded.Erasure.Extraction
{a} {M : Set a}
(š : Modality M)
where
open Modality š
open import Tools.Bool
open import Tools.Function
open import Tools.Nat using (Nat; 2+)
open import Tools.Relation
open import Definition.Untyped M as U
open import Graded.Erasure.Target as T
open import Graded.Erasure.Target.Non-terminating
private
variable
m n : Nat
Ī : Con U.Term n
A t tā² u : U.Term n
v vā² w : T.Term n
p : M
loop? : Strictness ā T.Term n
loop? non-strict = loop non-strict
loop? strict = āÆ
erase-prodrecĻ :
Strictness ā M ā T.Term n ā T.Term (2+ n) ā T.Term n
erase-prodrecĻ s p t u = case is-š? p of Ī» where
(yes pā”š) ā T.lam (u T.[ T.liftSubst (T.sgSubst (loop s)) ])
T.āāØ s ā© t
(no pā¢š) ā T.prodrec t u
app-šā² : Bool ā Strictness ā T.Term n ā T.Term n
app-šā² false s t = t T.āāØ s ā© loop? s
app-šā² true _ t = t
app-š : Strictness ā T.Term n ā T.Term n
app-š s = app-šā² (s == non-strict) s
mutual
erase : Strictness ā U.Term n ā T.Term n
erase s = eraseā² (s == non-strict) s
eraseā² : Bool ā Strictness ā U.Term n ā T.Term n
eraseā² remove s = eraseā³
where
eraseā³ : U.Term n ā T.Term n
eraseā³ (var x) = T.var x
eraseā³ U = loop? s
eraseā³ (Ī Ī£āØ _ ā© _ , _ ā· _ ā¹ _) = loop? s
eraseā³ (U.lam p t) = case remove of Ī» where
false ā T.lam (eraseā³ t)
true ā case is-š? p of Ī» where
(no _) ā T.lam (eraseā³ t)
(yes _) ā eraseā³ t T.[ loop? s ]ā
eraseā³ (t U.āāØ p ā© u) = case is-š? p of Ī» where
(no _) ā eraseā³ t T.āāØ s ā© eraseā³ u
(yes _) ā app-šā² remove s (eraseā³ t)
eraseā³ (U.prod _ p t u) = case is-š? p of Ī» where
(no _) ā prodāØ s ā© (eraseā³ t) (eraseā³ u)
(yes _) ā eraseā³ u
eraseā³ (U.fst p t) = case is-š? p of Ī» where
(no _) ā T.fst (eraseā³ t)
(yes _) ā loop s
eraseā³ (U.snd p t) = case is-š? p of Ī» where
(no _) ā T.snd (eraseā³ t)
(yes _) ā eraseā³ t
eraseā³ (U.prodrec r p _ _ t u) = case is-š? r of Ī» where
(no _) ā erase-prodrecĻ s p (eraseā³ t) (eraseā³ u)
(yes _) ā eraseā³ u T.[ loop s , loop s ]āā
eraseā³ ā = loop? s
eraseā³ U.zero = T.zero
eraseā³ (U.suc t) = sucāØ s ā© (eraseā³ t)
eraseā³ (U.natrec p q r A t u v) =
T.natrec (eraseā³ t) (eraseā³ u) (eraseā³ v)
eraseā³ Unit! = loop? s
eraseā³ U.star! = T.star
eraseā³ (U.unitrec p q A t u) = case is-š? p of Ī» where
(no _) ā T.unitrec (eraseā³ t) (eraseā³ u)
(yes _) ā eraseā³ u
eraseā³ Empty = loop? s
eraseā³ (emptyrec p A t) = loop s
eraseā³ (Id _ _ _) = loop? s
eraseā³ U.rfl = loop? s
eraseā³ (J _ _ _ _ _ u _ _) = eraseā³ u
eraseā³ (K _ _ _ _ u _) = eraseā³ u
eraseā³ ([]-cong _ _ _ _ _) = loop? s
mutual
eraseSubst : Strictness ā U.Subst m n ā T.Subst m n
eraseSubst = eraseSubstā² false
eraseSubstā² : Bool ā Strictness ā U.Subst m n ā T.Subst m n
eraseSubstā² b s Ļ x = eraseā² b s (Ļ x)