------------------------------------------------------------------------
-- The extraction function.
------------------------------------------------------------------------

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

-- Extraction for prodrec when the match is not erased.

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

-- The extraction function.

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) = β†―

-- Extraction of substitutions.

eraseSubst : U.Subst m n β†’ T.Subst m n
eraseSubst Οƒ x = erase (Οƒ x)

-- Extraction of weakenings.

eraseWk : U.Wk m n β†’ T.Wk m n
eraseWk id = id
eraseWk (step ρ) = step (eraseWk ρ)
eraseWk (lift ρ) = lift (eraseWk ρ)