------------------------------------------------------------------------
-- Definitions related to type and usage restrictions for the Zero-one
-- mode instance
------------------------------------------------------------------------

import Graded.Modality
import Graded.Mode.Instances.Zero-one.Variant

module Graded.Restrictions.Zero-one
  {a} {M : Set a}
  (open Graded.Modality M)
  (𝕄 : Modality)
  (open Graded.Mode.Instances.Zero-one.Variant 𝕄)
  (variant : Mode-variant)
  where

open Modality 𝕄

open import Tools.Bool
open import Tools.Empty
open import Tools.Function
open import Tools.Level
open import Tools.Product as Ξ£
open import Tools.PropositionalEquality
open import Tools.Relation as Dec
open import Tools.Sum
open import Tools.Unit

open import Graded.Modality.Properties 𝕄
open import Graded.Mode.Instances.Zero-one variant hiding (_β‰Ÿ_)
import Graded.Usage.Decidable.Assumptions as UD
open import Graded.Usage.Erased-matches
open import Graded.Usage.Restrictions 𝕄 Zero-one-isMode
open import Graded.Usage.Restrictions.Natrec 𝕄

import Definition.Typechecking.Decidable.Assumptions as TD
open import Definition.Typed.Restrictions 𝕄
open import Definition.Typed.Variant
open import Definition.Untyped.NotParametrised
open import Definition.Untyped.Properties.NotParametrised

open import Graded.Restrictions 𝕄 Zero-one-isMode public
  hiding (nr-available-UR; no-usage-restrictions;
          No-erased-matches; No-erased-matchesβ€²)
import Graded.Restrictions 𝕄 Zero-one-isMode as GR

private variable
  TR : Type-restrictions
  UR : Usage-restrictions
  b  : Bool
  ok : T _
  s  : Strength
  nm : Natrec-mode

------------------------------------------------------------------------
-- A lemma used below

opaque

  -- If a reflexive property holds for modes πŸ™α΅ and 𝟘ᡐ? then it holds
  -- for all modes m ≀ᡐ mβ€²

  πŸ™α΅πŸ˜α΅β†’β‰€α΅ :
    (P : (m mβ€² : Mode) β†’ Set) β†’
    (βˆ€ {ok} β†’ P πŸ™α΅ 𝟘ᡐ[ ok ]) β†’
    (βˆ€ {m} β†’ P m m) β†’
    βˆ€ {m mβ€²} β†’ m ≀ᡐ mβ€² β†’ P m mβ€²
  πŸ™α΅πŸ˜α΅β†’β‰€α΅ P ok₁₀ okα΅£ {(𝟘ᡐ)} {(𝟘ᡐ)} m≀ᡐmβ€² = subst (P _) 𝟘ᡐ-cong okα΅£
  πŸ™α΅πŸ˜α΅β†’β‰€α΅ P ok₁₀ okα΅£ {(𝟘ᡐ)} {(πŸ™α΅)} ()
  πŸ™α΅πŸ˜α΅β†’β‰€α΅ P ok₁₀ okα΅£ {(πŸ™α΅)} {(𝟘ᡐ[ ok ])} m≀ᡐmβ€² = subst (P _) 𝟘ᡐ-cong (ok₁₀ {ok})
  πŸ™α΅πŸ˜α΅β†’β‰€α΅ P ok₁₀ okα΅£ {(πŸ™α΅)} {(πŸ™α΅)} m≀ᡐmβ€² = okα΅£

------------------------------------------------------------------------
-- Functions that construct Usage-restrictions

-- No restrictions for prodrec, unitrec or emptyrec, all erased
-- matches are allowed for J andΒ K, the natrec mode can be anything,
-- Id-erased is inhabited if the first boolean is true, and starΛ’
-- is treated as a sink if the second boolean is true.

no-usage-restrictions :
  (nm : Natrec-mode) β†’
  Bool β†’ Bool β†’ Usage-restrictions
no-usage-restrictions nm =
  GR.no-usage-restrictions nm
    (Ξ» { ⦃ (Nr) ⦄ β†’ Zero-one-supports-nr ⦃ Natrec-mode-Has-nr Nr ⦄ })

-- A function used to define not-all-erased-matches-JK.

not-all-for-πŸ™α΅ : (Mode β†’ Erased-matches) β†’ Mode β†’ Erased-matches
not-all-for-πŸ™α΅ f 𝟘ᡐ = f 𝟘ᡐ
not-all-for-πŸ™α΅ f πŸ™α΅ with f πŸ™α΅
… | all = some
… | em  = em

-- The function adds the restriction that, for the modeΒ πŸ™α΅, "all"
-- erased matches are not allowed for J andΒ K.

not-all-erased-matches-JK : Usage-restrictions β†’ Usage-restrictions
not-all-erased-matches-JK UR = record UR
  { erased-matches-for-J =
      not-all-for-πŸ™α΅ erased-matches-for-J
  ; erased-matches-for-J-≀ᡉᡐ =
     πŸ™α΅πŸ˜α΅β†’β‰€α΅ (Ξ» m mβ€² β†’ not-all-for-πŸ™α΅ erased-matches-for-J m ≀ᡉᡐ not-all-for-πŸ™α΅ erased-matches-for-J mβ€²)
       (not-all-for-πŸ™α΅-≀ᡉᡐ erased-matches-for-J (erased-matches-for-J-≀ᡉᡐ πŸ™α΅β‰€))
       ≀ᡉᡐ-reflexive
  ; erased-matches-for-K =
      not-all-for-πŸ™α΅ erased-matches-for-K
  ; erased-matches-for-K-≀ᡉᡐ =
    πŸ™α΅πŸ˜α΅β†’β‰€α΅ (Ξ» m mβ€² β†’ not-all-for-πŸ™α΅ erased-matches-for-K m ≀ᡉᡐ not-all-for-πŸ™α΅ erased-matches-for-K mβ€²)
      (not-all-for-πŸ™α΅-≀ᡉᡐ erased-matches-for-K (erased-matches-for-K-≀ᡉᡐ πŸ™α΅β‰€))
      ≀ᡉᡐ-reflexive
  }
  where
  open Usage-restrictions UR

  opaque

    not-all-for-πŸ™α΅-≀ᡉᡐ :
      (f : Mode β†’ Erased-matches) β†’
      f πŸ™α΅ ≀ᡉᡐ f 𝟘ᡐ[ ok ] β†’
      not-all-for-πŸ™α΅ f πŸ™α΅ ≀ᡉᡐ not-all-for-πŸ™α΅ f 𝟘ᡐ[ ok ]
    not-all-for-πŸ™α΅-≀ᡉᡐ f f-≀ᡉᡐ with f πŸ™α΅
    … | all  = ≀ᡉᡐ-transitive _ f-≀ᡉᡐ
    … | some = f-≀ᡉᡐ
    … | none = f-≀ᡉᡐ

-- The function adds the restriction that certain erased matches are
-- not allowed for the modeΒ πŸ™α΅. No restriction is added for emptyrec
-- or unitrec. For prodrec the added restriction only applies to
-- non-trivial modalities.

only-some-erased-matches : Usage-restrictions β†’ Usage-restrictions
only-some-erased-matches UR = record UR
  { Prodrec-allowed = Ξ» m r p q β†’
      Prodrec-allowed m r p q Γ—
      (m ≑ πŸ™α΅ β†’ Β¬ Trivial β†’ r β‰’ 𝟘)
  ; Prodrec-allowed-upwards-closed = Ξ» (ok , rβ‰’πŸ˜) m≀mβ€² β†’
      Prodrec-allowed-upwards-closed ok m≀mβ€² , Ξ» { refl β†’ rβ‰’πŸ˜ (≀ᡐ-πŸ™α΅β†’ m≀mβ€²) }
  ; erased-matches-for-J =
      f (erased-matches-for-J 𝟘ᡐ?)
  ; erased-matches-for-J-≀ᡉᡐ =
      πŸ™α΅πŸ˜α΅β†’β‰€α΅ (Ξ» m mβ€² β†’ f _ m ≀ᡉᡐ f _ mβ€²) _ ≀ᡉᡐ-reflexive
  ; erased-matches-for-K =
      f (erased-matches-for-K 𝟘ᡐ?)
  ; erased-matches-for-K-≀ᡉᡐ =
      πŸ™α΅πŸ˜α΅β†’β‰€α΅ (Ξ» m mβ€² β†’ f _ m ≀ᡉᡐ f _ mβ€²) _ ≀ᡉᡐ-reflexive
  }
  where
  open Usage-restrictions UR
  f : Erased-matches β†’ Mode β†’ Erased-matches
  f _  πŸ™α΅ = none
  f em 𝟘ᡐ = em

-- The function adds the restriction that certain erased matches are
-- not allowed for the modeΒ πŸ™α΅. No restriction is added for emptyrec.
-- For prodrec and unitrec the added restriction only applies to
-- non-trivial modalities, and for unitrec the added restriction only
-- applies if Ξ·-equality is not allowed for weak unit types.

no-erased-matches-UR :
  Type-restrictions β†’ Usage-restrictions β†’ Usage-restrictions
no-erased-matches-UR TR UR = record (only-some-erased-matches UR)
  { Unitrec-allowed = Ξ» m p q β†’
      Unitrec-allowed m p q Γ—
      (m ≑ πŸ™α΅ β†’ Β¬ Trivial β†’ p ≑ 𝟘 β†’ UnitΚ·-Ξ·)
  ; Unitrec-allowed-upwards-closed = Ξ» (ok , Ξ·) m≀mβ€² β†’
      Unitrec-allowed-upwards-closed ok m≀mβ€² , Ξ» { refl β†’ Ξ· (≀ᡐ-πŸ™α΅β†’ m≀mβ€²) }
  }
  where
  open Type-restrictions TR
  open Usage-restrictions UR

-- The function updates the usage restrictions to use the usage rule
-- natrecβ‚˜ for natrec using a given nr function.

nr-available-UR :
  (has-nr : Has-nr 𝕄) β†’
  Usage-restrictions β†’ Usage-restrictions
nr-available-UR has-nr UR = record UR
  { natrec-mode      = Nr ⦃ has-nr ⦄
  ; mode-supports-nr = Ξ» { ⦃ (Nr) ⦄ β†’ Zero-one-supports-nr}
  }

-- A function used to define no-[]-cong-UR.

at-least-some : (Mode β†’ Erased-matches) β†’ Mode β†’ Erased-matches
at-least-some f m = case f m of Ξ» where
  none β†’ some
  em   β†’ em

-- The function no-[]-cong-UR disables support for []-cong but enables
-- "some" erased matches for J.

no-[]-cong-UR : Usage-restrictions β†’ Usage-restrictions
no-[]-cong-UR UR = record UR
  { []-cong-allowed-mode                = Ξ» _ _ β†’ Lift _ βŠ₯
  ; []-cong-allowed-mode-upwards-closed = Ξ» ()
  ; erased-matches-for-J     = at-least-some erased-matches-for-J
  ; erased-matches-for-J-≀ᡉᡐ =
      πŸ™α΅πŸ˜α΅β†’β‰€α΅ (Ξ» m mβ€² β†’ at-least-some erased-matches-for-J m ≀ᡉᡐ at-least-some erased-matches-for-J mβ€²)
        at-least-some-≀ᡉᡐ ≀ᡉᡐ-reflexive
  }
  where
  open Usage-restrictions UR

  at-least-some-≀ᡉᡐ :
    at-least-some erased-matches-for-J πŸ™α΅ ≀ᡉᡐ
    at-least-some erased-matches-for-J 𝟘ᡐ[ ok ]
  at-least-some-≀ᡉᡐ {ok}
    with erased-matches-for-J πŸ™α΅
       | erased-matches-for-J 𝟘ᡐ[ ok ]
       | erased-matches-for-J-≀ᡉᡐ {m = πŸ™α΅} {mβ€² = 𝟘ᡐ[ ok ]} πŸ™α΅β‰€
  … | none       | none       | _  = _
  … | none       | some       | _  = _
  … | none       | all        | _  = _
  … | all        | none       | ()
  … | some       | none       | ()
  … | not-none _ | not-none _ | r  = r

------------------------------------------------------------------------
-- Only-some-erased-matches

-- The property of not allowing certain erased matches:
-- * Erased matches are allowed for emptyrec and unitrec.
-- * "Erased" matches are allowed for trivial modalities.
-- * Erased matches are allowed when the mode is notΒ πŸ™α΅, except for
--   []-cong.

Only-some-erased-matches :
  Type-restrictions β†’ Usage-restrictions β†’ Set a
Only-some-erased-matches TR UR =
  Β¬ Trivial β†’
  (βˆ€ {r p q} β†’ Prodrec-allowed πŸ™α΅ r p q β†’ r β‰’ 𝟘) Γ—
  (βˆ€ {s} β†’ Β¬ ([]-cong-allowed s)) Γ—
  erased-matches-for-J πŸ™α΅ ≑ none Γ—
  erased-matches-for-K πŸ™α΅ ≑ none
  where
  open Type-restrictions TR
  open Usage-restrictions UR

opaque

  -- Certain restrictions obtained from no-erased-matches-TR and
  -- only-some-erased-matches satisfy Only-some-erased-matches.

  Only-some-erased-matches-only-some-erased-matches :
    βˆ€ TR UR β†’
    Only-some-erased-matches
      (no-erased-matches-TR 𝕀 (no-erased-matches-TR 𝕨 TR))
      (only-some-erased-matches UR)
  Only-some-erased-matches-only-some-erased-matches _ _ πŸ™β‰’πŸ˜ =
      (Ξ» x β†’ x refl πŸ™β‰’πŸ˜) βˆ˜β†’ projβ‚‚
    , (Ξ» where
         {s = 𝕀} β†’ (_$ refl) βˆ˜β†’ projβ‚‚
         {s = 𝕨} β†’ (_$ refl) βˆ˜β†’ projβ‚‚ βˆ˜β†’ proj₁)
    , refl
    , refl

------------------------------------------------------------------------
-- No-erased-matches

-- The property of not allowing (certain) erased matches:
-- * Erased matches are allowed for emptyrec.
-- * "Erased" matches are allowed for unitrec if Ξ·-equality is allowed
--   for weak unit types.
-- * "Erased" matches are allowed for trivial modalities.
-- * Erased matches are allowed when the mode is notΒ πŸ™α΅, except for
--   []-cong. (Note that a variant of []-cong that works when the mode
--   is not πŸ™α΅ can be defined without the use of []-cong, see
--   Graded.Box-cong.β–Έ[]-cong-J-𝟘ᡐ.)

No-erased-matches : Type-restrictions β†’ Usage-restrictions β†’ Set a
No-erased-matches TR UR =
  Β¬ Trivial β†’
  (βˆ€ {r p q} β†’ Prodrec-allowed πŸ™α΅ r p q β†’ r β‰’ 𝟘) Γ—
  (βˆ€ {p q}   β†’ Unitrec-allowed πŸ™α΅ p q   β†’ p ≑ 𝟘 β†’ UnitΚ·-Ξ·) Γ—
  (βˆ€ {s} β†’ Β¬ ([]-cong-allowed s)) Γ—
  erased-matches-for-J πŸ™α΅ ≑ none Γ—
  erased-matches-for-K πŸ™α΅ ≑ none
  where
  open Type-restrictions TR
  open Usage-restrictions UR

-- Certain restrictions obtained from no-erased-matches-TR and
-- no-erased-matches-UR satisfy No-erased-matches.

No-erased-matches-no-erased-matches :
  βˆ€ TR UR β†’
  let TRβ€² = no-erased-matches-TR 𝕀 (no-erased-matches-TR 𝕨 TR) in
  No-erased-matches TRβ€² (no-erased-matches-UR TRβ€² UR)
No-erased-matches-no-erased-matches TR UR πŸ™β‰’πŸ˜ =
  case Only-some-erased-matches-only-some-erased-matches TR UR πŸ™β‰’πŸ˜ of Ξ»
    (pr , rest) β†’
    (Ξ» {_ _ _} β†’ pr)
  , (Ξ» {_ _} β†’ (Ξ» x β†’ x refl πŸ™β‰’πŸ˜) βˆ˜β†’ projβ‚‚)
  , rest

opaque

  -- If UnitΚ·-Ξ· holds for TR, then Only-some-erased-matchesΒ TRΒ UR
  -- implies No-erased-matchesΒ TRΒ UR.

  Only-some-erased-matches→No-erased-matches :
    βˆ€ TR UR β†’
    Type-restrictions.UnitΚ·-Ξ· TR β†’
    Only-some-erased-matches TR UR β†’ No-erased-matches TR UR
  Only-some-erased-matches→No-erased-matches _ _ η =
    Ξ£.map idαΆ  ((Ξ» {_ _} _ _ β†’ Ξ·) ,_) βˆ˜β†’_

-- An alternative to No-erased-matches that refers to
-- Type-variant instead of Type-restrictions

No-erased-matchesβ€² : Type-variant β†’ Usage-restrictions β†’ Set a
No-erased-matchesβ€² TV UR =
  Β¬ Trivial β†’
  (βˆ€ {r p q} β†’ Prodrec-allowed πŸ™α΅ r p q β†’ r β‰’ 𝟘) Γ—
  (βˆ€ {p q}   β†’ Unitrec-allowed πŸ™α΅ p q   β†’ p ≑ 𝟘 β†’ UnitΚ·-Ξ·) Γ—
  (βˆ€ {s} β†’ Β¬ ([]-cong-allowed-mode s πŸ™α΅)) Γ—
  erased-matches-for-J πŸ™α΅ ≑ none Γ—
  erased-matches-for-K πŸ™α΅ ≑ none
  where
  open Type-variant TV
  open Usage-restrictions UR

------------------------------------------------------------------------
-- Some lemmas related to UD.Assumptions

opaque

  -- If grade equality is decidable and the modality supports usage
  -- inference for a given natrec-mode nm, UD.Assumptions holds for
  -- no-usage-restrictionsΒ nmΒ bΒ false.

  Assumptions-no-usage-restrictions :
    ⦃ ok : Natrec-mode-supports-usage-inference nm ⦄ β†’
    Decidable (_≑_ {A = M}) β†’
    UD.Assumptions (no-usage-restrictions nm b false)
  Assumptions-no-usage-restrictions dec = Ξ» where
      ._β‰Ÿ_                       β†’ dec
      .Prodrec-allowed? _ _ _ _  β†’ yes _
      .Unitrec-allowed? _ _ _    β†’ yes _
      .Emptyrec-allowed? _ _     β†’ yes _
      .[]-cong-allowed-mode? _ _ β†’ yes _
      .no-sink-or-β‰€πŸ˜             β†’ inj₁ idαΆ 
    where
    open UD.Assumptions

opaque

  -- The function not-all-erased-matches-JK preserves UD.Assumptions.

  Assumptions-not-all-erased-matches-JK :
    UD.Assumptions UR β†’ UD.Assumptions (not-all-erased-matches-JK UR)
  Assumptions-not-all-erased-matches-JK as = Ξ» where
      ._β‰Ÿ_                   β†’ A._β‰Ÿ_
      .Prodrec-allowed?      β†’ A.Prodrec-allowed?
      .Unitrec-allowed?      β†’ A.Unitrec-allowed?
      .Emptyrec-allowed?     β†’ A.Emptyrec-allowed?
      .[]-cong-allowed-mode? β†’ A.[]-cong-allowed-mode?
      .no-sink-or-β‰€πŸ˜         β†’ A.no-sink-or-β‰€πŸ˜
    where
    module A = UD.Assumptions as
    open UD.Assumptions

opaque

  -- The function only-some-erased-matches preserves UD.Assumptions.

  Assumptions-only-some-erased-matches :
    UD.Assumptions UR β†’ UD.Assumptions (only-some-erased-matches UR)
  Assumptions-only-some-erased-matches as = Ξ» where
      ._β‰Ÿ_                       β†’ A._β‰Ÿ_
      .Prodrec-allowed? m r p q  β†’ A.Prodrec-allowed? m r p q
                                    Γ—-dec
                                  Dec.map (Ξ» β‰‘πŸ™ β†’ trans (sym (⌞⌜⌝⌟ _)) (trans (⌞⌟-cong β‰‘πŸ™) βŒžπŸ™βŒŸ))
                                    (Ξ» { refl β†’ βŒœπŸ™α΅βŒ}) (⌜ m ⌝ A.β‰Ÿ πŸ™)
                                    β†’-dec
                                  Β¬? trivial?
                                    β†’-dec
                                  Β¬? (r A.β‰Ÿ 𝟘)
      .Unitrec-allowed?       β†’ A.Unitrec-allowed?
      .Emptyrec-allowed?      β†’ A.Emptyrec-allowed?
      .[]-cong-allowed-mode?  β†’ A.[]-cong-allowed-mode?
      .no-sink-or-β‰€πŸ˜          β†’ A.no-sink-or-β‰€πŸ˜
    where
    module A = UD.Assumptions as
    open UD.Assumptions

opaque

  -- The function no-erased-matches-URΒ TR preserves UD.Assumptions.

  Assumptions-no-erased-matches-UR :
    βˆ€ TR β†’ UD.Assumptions UR β†’
    UD.Assumptions (no-erased-matches-UR TR UR)
  Assumptions-no-erased-matches-UR TR as = Ξ» where
      ._β‰Ÿ_                    β†’ A._β‰Ÿ_
      .Prodrec-allowed?        β†’ A.Prodrec-allowed?
      .Unitrec-allowed? m p q  β†’ A.Unitrec-allowed? m p q
                                    Γ—-dec
                                 (Dec.map (Ξ» β‰‘πŸ™ β†’ trans (sym (⌞⌜⌝⌟ _)) (trans (⌞⌟-cong β‰‘πŸ™) βŒžπŸ™βŒŸ))
                                    (Ξ» { refl β†’ βŒœπŸ™α΅βŒ}) (⌜ m ⌝ A.β‰Ÿ πŸ™)
                                    β†’-dec
                                   Β¬? trivial?
                                    β†’-dec
                                   p A.β‰Ÿ 𝟘
                                    β†’-dec
                                   UnitΚ·-Ξ·?)
      .Emptyrec-allowed?     β†’ A.Emptyrec-allowed?
      .[]-cong-allowed-mode? β†’ A.[]-cong-allowed-mode?
      .no-sink-or-β‰€πŸ˜         β†’ A.no-sink-or-β‰€πŸ˜
    where
    module A = UD.Assumptions (Assumptions-only-some-erased-matches as)
    open UD.Assumptions
    open Type-restrictions TR