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

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 l : Nat
    Ī“ : Con U.Term n
    A t tā€² u : U.Term n
    v vā€² w : T.Term n
    p : M

-- If the first argument is strict, then the result isĀ ā†Æ (which is a
-- value), but if the first argument is non-strict, then the result is
-- loopĀ non-strict (which does not reduce to a value).

loop? : Strictness ā†’ T.Term n
loop? non-strict = loop non-strict
loop? strict     = ā†Æ

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

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

-- A function application that is used when the grade isĀ šŸ˜.
--
-- The argument is removed entirely if the boolean is true.

app-šŸ˜ā€² : Bool ā†’ Strictness ā†’ T.Term n ā†’ T.Term n
app-šŸ˜ā€² false s t = t T.āˆ˜āŸØ s āŸ© loop? s
app-šŸ˜ā€² true  _ t = t

-- A variant of app-šŸ˜.

app-šŸ˜ : Strictness ā†’ T.Term n ā†’ T.Term n
app-šŸ˜ s = app-šŸ˜ā€² (s == non-strict) s

mutual

  -- The extraction function.
  --
  -- Function and constructor applications are made strict if the
  -- first argument is "strict".
  --
  -- Erasable arguments are removed entirely if the first argument is
  -- "non-strict".
  --
  -- A non-terminating term, loopĀ s, is used in some places. The idea
  -- is that it should be safe to replace this term with, say, a term
  -- that throws an exception. The term loop?Ā s is equal to loopĀ s
  -- when s is non-strict, but if s is strict, then loop?Ā s isĀ ā†Æ,
  -- which is a value.

  erase : Strictness ā†’ U.Term n ā†’ T.Term n
  erase s = eraseā€² (s == non-strict) s

  -- A variant of the extraction function.
  --
  -- If the boolean is true, then erasable arguments are removed
  -- entirely.

  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 _ _ 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

  -- Extraction of substitutions.

  eraseSubst : Strictness ā†’ U.Subst m n ā†’ T.Subst m n
  eraseSubst = eraseSubstā€² false

  -- A variant of eraseSubst.

  eraseSubstā€² : Bool ā†’ Strictness ā†’ U.Subst m n ā†’ T.Subst m n
  eraseSubstā€² b s Ļƒ x = eraseā€² b s (Ļƒ x)