------------------------------------------------------------------------
-- Target terms in the logical relation reduce to values
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
open import Graded.Erasure.LogicalRelation.Assumptions
open import Graded.Modality
import Graded.Mode.Instances.Zero-one
open import Graded.Mode.Instances.Zero-one.Variant
open import Graded.Usage.Restrictions

module Graded.Erasure.LogicalRelation.Value
  {a} {M : Set a}
  {𝕄 : Modality M}
  {R : Type-restrictions 𝕄}
  {variant : Mode-variant 𝕄}
  (open Graded.Mode.Instances.Zero-one variant)
  (UR : Usage-restrictions 𝕄 Zero-one-isMode)
  (as : Assumptions R)
  where

open Assumptions as

open import Definition.LogicalRelation.Simplified R
open import Definition.Untyped M

open import Graded.Erasure.LogicalRelation as
open import Graded.Erasure.LogicalRelation.Hidden UR as
open import Graded.Erasure.Target as T using (strict)
open import Graded.Erasure.Target.Properties

open import Tools.Function
open import Tools.Product as Σ
open import Tools.PropositionalEquality

private variable
  A t : Term _
  u   : T.Term _
  l   : Universe-level

opaque
  unfolding _®_∷_

  -- In the strict setting, if t is related to u, then u reduces to a
  -- value.

  reduces-to-value :
    str ≡ strict →
    t ® u ∷ A →
    ∃ λ v → T.Value v × vs T.⊢ u ⇒* v
  reduces-to-value refl (⊨A , t®u) = helper ⊨A t®u
    where
    helper :
      (⊨A : ts » Δ ⊨ A) →
      t ® u ∷ A / ⊨A →
      ∃ λ v → T.Value v × vs T.⊢ u ⇒* v
    helper = λ where
      (Levelᵣ _)        (U/Levelᵣ v⇒*↯)     → _ , T.↯    , v⇒*↯ refl
      (Uᵣ _)            (U/Levelᵣ v⇒*↯)     → _ , T.↯    , v⇒*↯ refl
      (ℕᵣ _)            (zeroᵣ _ v⇒*zero)   → _ , T.zero , v⇒*zero
      (ℕᵣ _)            (sucᵣ _ v⇒*suc _ _) → _ , T.suc  , v⇒*suc
      (Emptyᵣ _)        ()
      (Unitᵣ _)         (starᵣ _ v⇒*star)   → _ , T.star , v⇒*star
      (ne record{})     ()
      (Idᵣ _)           (rflᵣ _ v⇒*↯)       → _ , T.↯    , v⇒*↯ refl
      (Bᵣ BMΠ _ _ record{}) (u⇒*lam , _)    → _ , T.lam  ,
                                              u⇒*lam refl .proj₂
      (Liftᵣ′ _ ⊩B)     lower-t®u           → helper ⊩B lower-t®u
      (Bᵣ′ (BMΣ _) _ _ _ _ _ _ ⊨B) (_ , _ , _ , _ , _ , t₂®v₂ , more) →
        Σ-®-elim _ more
          (λ u⇒*v₂ _ →
             Σ.map idᶠ (Σ.map idᶠ (red*concat u⇒*v₂)) $
             helper (⊨B _) t₂®v₂)
          (λ _ u⇒*prod _ _ → _ , T.prod , u⇒*prod)
      (Quot ⊨A) (_ , _ , t®v) →
        helper (_⊨Quot_.⊨Data ⊨A) t®v

opaque

  -- In the strict setting, if t is related to u at type ℕ, then u
  -- reduces to a numeral.

  reduces-to-numeral :
    str ≡ strict →
    t ® u ∷ℕ →
    ∃ λ v → T.Numeral v × vs T.⊢ u ⇒* v
  reduces-to-numeral refl = λ where
    (zeroᵣ _ v⇒*zero)     → _ , T.zero    , v⇒*zero
    (sucᵣ _ v⇒*suc num _) → _ , T.suc num , v⇒*suc