------------------------------------------------------------------------
-- A modality for linear types.
------------------------------------------------------------------------

open import Tools.Bool using (T; false)
open import Tools.Level
open import Tools.Sum

open import Graded.Modality.Instances.Zero-one-many false as πŸ˜πŸ™Ο‰

module Graded.Modality.Instances.Linearity where

open πŸ˜πŸ™Ο‰ renaming (Zero-one-many to Linearity) public

open import Graded.Modality Linearity
import Graded.Mode.Instances.Zero-one.Variant
import Graded.Mode.Instances.Zero-one
import Graded.Modality.Properties
import Graded.FullReduction.Assumptions
import Graded.Usage.Restrictions

open import Definition.Untyped using (BMΞ£; 𝕀; 𝕨)
import Definition.Typed.Restrictions
import Graded.Usage.Restrictions

open import Tools.Bool
open import Tools.Empty
open import Tools.Function
open import Tools.Nat using (Sequence)
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Relation

-- A "linear types" modality.

linearityModality : Modality
linearityModality = zero-one-many-modality

private variable
  pα΅’ : Sequence Linearity

-- The nr function zero-one-many-has-nr.nr is
-- incomparable to (neither bounded from below nor from above by) the
-- nr function zero-one-many-greatest-star-nr.nr

incomparable :
 let nr₁ = zero-one-many-has-nr .Has-nr.nr
     nrβ‚‚ = zero-one-many-greatest-star-nr .Has-nr.nr
  in
  (βˆƒβ‚… Ξ» p r z s n β†’ Β¬ nr₁ p r z s n ≀ nrβ‚‚ p r z s n) Γ—
  (βˆƒβ‚… Ξ» p r z s n β†’ Β¬ nrβ‚‚ p r z s n ≀ nr₁ p r z s n)
incomparable =
    (𝟘 , πŸ™ , 𝟘 , 𝟘 , πŸ™ , (Ξ» ()))
  , (𝟘 , πŸ™ , πŸ™ , 𝟘 , πŸ™ , (Ξ» ()))

instance

  -- The "linear types" modality has a well-behaved zero.

  linearity-has-well-behaved-zero :
    Has-well-behaved-zero linearityModality
  linearity-has-well-behaved-zero = zero-one-many-has-well-behaved-zero

open Graded.Modality.Properties linearityModality
open Graded.Mode.Instances.Zero-one.Variant linearityModality

opaque

  -- If πŸ™ is the greatest lower bounds of a sequence then the sequence is
  -- constantly πŸ™

  πŸ™-GLB-inv :
    Modality.Greatest-lower-bound zero-one-many-modality πŸ™ pα΅’ β†’
    βˆ€ i β†’ pα΅’ i ≑ πŸ™
  πŸ™-GLB-inv πŸ™-glb i = lemma _ (πŸ™-glb .proj₁ i)
    where
    lemma : βˆ€ p β†’ πŸ™ ≀ p β†’ p ≑ πŸ™
    lemma 𝟘 ()
    lemma πŸ™ _ = refl
    lemma Ο‰ ()

opaque

  -- If the greatest lower bound of nrᡒ r z s is 𝟘 then z = s 𝟘.

  nrᡒ-GLB-𝟘-inv :
   let 𝕄 = zero-one-many-modality in
    βˆ€ r z s β†’
    Modality.Greatest-lower-bound 𝕄 𝟘 (Modality.nrα΅’ 𝕄 r z s) β†’
    z ≑ 𝟘 Γ— s ≑ 𝟘
  nrα΅’-GLB-𝟘-inv r 𝟘 𝟘 (πŸ˜β‰€ , _) = refl , refl
  nrα΅’-GLB-𝟘-inv 𝟘 𝟘 πŸ™ (πŸ˜β‰€ , _) = case πŸ˜β‰€ 1 of Ξ» ()
  nrα΅’-GLB-𝟘-inv πŸ™ 𝟘 πŸ™ (πŸ˜β‰€ , _) = case πŸ˜β‰€ 1 of Ξ» ()
  nrα΅’-GLB-𝟘-inv Ο‰ 𝟘 πŸ™ (πŸ˜β‰€ , _) = case πŸ˜β‰€ 1 of Ξ» ()
  nrα΅’-GLB-𝟘-inv r 𝟘 Ο‰ (πŸ˜β‰€ , _) = case πŸ˜β‰€ 1 of Ξ» ()
  nrα΅’-GLB-𝟘-inv r πŸ™ s (πŸ˜β‰€ , _) = case πŸ˜β‰€ 0 of Ξ» ()
  nrα΅’-GLB-𝟘-inv r Ο‰ s (πŸ˜β‰€ , _) = case πŸ˜β‰€ 0 of Ξ» ()

opaque

  -- If the greatest lower bound of nrα΅’Β rΒ zΒ s is πŸ™ then either
  -- r=πŸ™, z=πŸ™, sβ‰‘πŸ˜
  -- rβ‰‘πŸ˜, zβ‰‘πŸ™, sβ‰‘πŸ™

  nrα΅’-GLB-πŸ™-inv :
   let 𝕄 = zero-one-many-modality in
    βˆ€ r z s β†’
    Modality.Greatest-lower-bound 𝕄 πŸ™ (Modality.nrα΅’ 𝕄 r z s) β†’
    r ≑ πŸ™ Γ— z ≑ πŸ™ Γ— s ≑ 𝟘 ⊎ r ≑ 𝟘 Γ— z ≑ πŸ™ Γ— s ≑ πŸ™
  nrα΅’-GLB-πŸ™-inv 𝟘 𝟘 𝟘 (πŸ™β‰€ , glb) = case glb 𝟘 (Ξ» i β†’ ≀-reflexive (sym (nrα΅’-𝟘 i))) of Ξ» ()
  nrα΅’-GLB-πŸ™-inv πŸ™ 𝟘 𝟘 (πŸ™β‰€ , glb) = case glb 𝟘 (Ξ» i β†’ ≀-reflexive (sym (nrα΅’-𝟘 i))) of Ξ» ()
  nrα΅’-GLB-πŸ™-inv Ο‰ 𝟘 𝟘 (πŸ™β‰€ , glb) = case glb 𝟘 (Ξ» i β†’ ≀-reflexive (sym (nrα΅’-𝟘 i))) of Ξ» ()
  nrα΅’-GLB-πŸ™-inv 𝟘 𝟘 πŸ™ (πŸ™β‰€ , _) = case πŸ™β‰€ 0 of Ξ» ()
  nrα΅’-GLB-πŸ™-inv πŸ™ 𝟘 πŸ™ (πŸ™β‰€ , _) = case πŸ™β‰€ 2 of Ξ» ()
  nrα΅’-GLB-πŸ™-inv Ο‰ 𝟘 πŸ™ (πŸ™β‰€ , _) = case πŸ™β‰€ 2 of Ξ» ()
  nrα΅’-GLB-πŸ™-inv r 𝟘 Ο‰ (πŸ™β‰€ , _) = case πŸ™β‰€ 1 of Ξ» ()
  nrα΅’-GLB-πŸ™-inv 𝟘 πŸ™ 𝟘 (πŸ™β‰€ , _) = case πŸ™β‰€ 1 of Ξ» ()
  nrα΅’-GLB-πŸ™-inv πŸ™ πŸ™ 𝟘 (πŸ™β‰€ , _) = inj₁ (refl , refl , refl)
  nrα΅’-GLB-πŸ™-inv Ο‰ πŸ™ 𝟘 (πŸ™β‰€ , _) = case πŸ™β‰€ 1 of Ξ» ()
  nrα΅’-GLB-πŸ™-inv 𝟘 πŸ™ πŸ™ (πŸ™β‰€ , _) = injβ‚‚ (refl , refl , refl)
  nrα΅’-GLB-πŸ™-inv πŸ™ πŸ™ πŸ™ (πŸ™β‰€ , _) = case πŸ™β‰€ 1 of Ξ» ()
  nrα΅’-GLB-πŸ™-inv Ο‰ πŸ™ πŸ™ (πŸ™β‰€ , _) = case πŸ™β‰€ 1 of Ξ» ()
  nrα΅’-GLB-πŸ™-inv r πŸ™ Ο‰ (πŸ™β‰€ , _) = case πŸ™β‰€ 1 of Ξ» ()
  nrα΅’-GLB-πŸ™-inv r Ο‰ s (πŸ™β‰€ , _) = case πŸ™β‰€ 0 of Ξ» ()

opaque

  -- The greatest lower bound of nrα΅’Β rΒ πŸ™Β p is πŸ™ only if
  -- p ≑ 𝟘 and r ≑ πŸ™ or p ≑ πŸ™ and r ≑ 𝟘

  nrα΅’-rπŸ™p-GLB-πŸ™-inv :
    let 𝕄 = zero-one-many-modality in
      βˆ€ p r β†’
    Modality.Greatest-lower-bound 𝕄 πŸ™ (Modality.nrα΅’ 𝕄 r πŸ™ p) β†’
    p ≑ 𝟘 Γ— r ≑ πŸ™ ⊎ p ≑ πŸ™ Γ— r ≑ 𝟘
  nrα΅’-rπŸ™p-GLB-πŸ™-inv p r glb =
    case nrα΅’-GLB-πŸ™-inv r πŸ™ p glb of Ξ» where
      (inj₁ (rβ‰‘πŸ™ , _ , pβ‰‘πŸ˜)) β†’ inj₁ (pβ‰‘πŸ˜ , rβ‰‘πŸ™)
      (injβ‚‚ (rβ‰‘πŸ˜ , _ , pβ‰‘πŸ™)) β†’ injβ‚‚ (pβ‰‘πŸ™ , rβ‰‘πŸ˜)

------------------------------------------------------------------------
-- Properties relating to the Zero-one mode structure

module _ {𝟘ᡐ-allowed : Bool} where

  private
    variant : Mode-variant
    variant = record
      { 𝟘ᡐ-allowed = 𝟘ᡐ-allowed
      ; 𝟘-well-behaved = Ξ» _ β†’ linearity-has-well-behaved-zero
      }

  open Graded.Mode.Instances.Zero-one   variant
  open Definition.Typed.Restrictions    linearityModality
  open Graded.Usage.Restrictions        linearityModality Zero-one-isMode
  open Graded.FullReduction.Assumptions variant

  private variable
    rs : Type-restrictions
    us : Usage-restrictions

  -- Instances of Type-restrictions and Usage-restrictions are suitable
  -- for the full reduction theorem if
  -- * whenever UnitΛ’-allowed holds, then StarΛ’-sink holds,
  -- * UnitΚ·-allowed and UnitΚ·-Ξ· do not both hold,
  -- * Σ˒-allowed 𝟘 p does not hold, and
  -- * Ξ£Λ’-allowed ω p does not hold.

  Suitable-for-full-reduction :
    Type-restrictions β†’ Usage-restrictions β†’ Set
  Suitable-for-full-reduction rs us =
    (UnitΛ’-allowed β†’ StarΛ’-sink) Γ—
    (UnitΚ·-allowed β†’ Β¬ UnitΚ·-Ξ·) Γ—
    (βˆ€ p β†’ Β¬ Ξ£Λ’-allowed 𝟘 p) Γ—
    (βˆ€ p β†’ Β¬ Ξ£Λ’-allowed Ο‰ p)
    where
    open Type-restrictions rs
    open Usage-restrictions us

  -- Given an instance of Type-restrictions one can create a "suitable"
  -- instance.

  suitable-for-full-reduction :
    Type-restrictions β†’ βˆƒ Ξ» rs β†’ Suitable-for-full-reduction rs us
  suitable-for-full-reduction {us} rs =
      record rs
        { Unit-allowed = Ξ» where
            𝕨 β†’ UnitΚ·-allowed Γ— Β¬ UnitΚ·-Ξ·
            𝕀 β†’ UnitΛ’-allowed Γ— StarΛ’-sink
        ; Ξ Ξ£-allowed = Ξ» b p q β†’
            Ξ Ξ£-allowed b p q Γ— (b ≑ BMΞ£ 𝕀 β†’ p ≑ πŸ™)
        ; []-cong-allowed = Ξ» where
            𝕨 β†’ []-congΚ·-allowed Γ— Β¬ UnitΚ·-Ξ·
            𝕀 β†’ βŠ₯
        ; []-cong→Erased = λ where
            {s = 𝕨} (ok , no-Ξ·) β†’
                ([]-congβ†’Erased ok .proj₁ , no-Ξ·)
              , []-cong→Erased ok .proj₂
              , Ξ» ()
            {s = 𝕀} ()
        ; []-congβ†’Β¬Trivial = Ξ» { {s = 𝕨} _ (); {s = 𝕀} () }
        }
    , projβ‚‚
    , projβ‚‚
    , (Ξ» _ β†’ ((Ξ» ()) βˆ˜β†’ (_$ refl)) βˆ˜β†’ projβ‚‚)
    , (Ξ» _ β†’ ((Ξ» ()) βˆ˜β†’ (_$ refl)) βˆ˜β†’ projβ‚‚)
    where
    open Type-restrictions rs
    open Usage-restrictions us

  -- The full reduction assumptions hold for linearityModality and any
  -- "suitable" Type-restrictions and Usage-restrictions.

  full-reduction-assumptions :
    Suitable-for-full-reduction rs us β†’
    Full-reduction-assumptions rs us
  full-reduction-assumptions (sink , no-Ξ· , ¬𝟘 , ¬ω) = record
    { sinkβŠŽπŸ™β‰€πŸ˜ = Ξ» where
        {s = 𝕀} ok _         β†’ inj₁ (refl , sink ok)
        {s = 𝕨} _  (inj₁ ())
        {s = 𝕨} ok (injβ‚‚ Ξ·)  β†’ βŠ₯-elim (no-Ξ· ok Ξ·)
    ; β‰‘πŸ™βŠŽπŸ™β‰€πŸ˜   = Ξ» where
        {p = 𝟘} ok β†’ βŠ₯-elim (¬𝟘 _ ok)
        {p = Ο‰} ok β†’ βŠ₯-elim (¬ω _ ok)
        {p = πŸ™} _  β†’ inj₁ refl
    }

  -- Type and usage restrictions that satisfy the full reduction
  -- assumptions are "suitable".

  full-reduction-assumptions-suitable :
    Full-reduction-assumptions rs us β†’ Suitable-for-full-reduction rs us
  full-reduction-assumptions-suitable {us = us} as =
      (Ξ» ok β†’ case sinkβŠŽπŸ™β‰€πŸ˜ ok (inj₁ refl) of Ξ» where
         (inj₁ (_ , sink)) β†’ sink
         (injβ‚‚ ()))
    , (Ξ» ok Ξ· β†’ case sinkβŠŽπŸ™β‰€πŸ˜ ok (injβ‚‚ Ξ·) of Ξ» where
         (inj₁ (() , _))
         (injβ‚‚ ()))
    , (Ξ» p Ξ£-ok β†’ case β‰‘πŸ™βŠŽπŸ™β‰€πŸ˜ Ξ£-ok of Ξ» where
        (inj₁ ())
        (injβ‚‚ (_ , _ , ())))
    , (Ξ» p Ξ£-ok β†’ case β‰‘πŸ™βŠŽπŸ™β‰€πŸ˜ Ξ£-ok of Ξ» where
        (inj₁ ())
        (injβ‚‚ (() , _)))
    where
    open Full-reduction-assumptions _ _ as
    open Usage-restrictions us