open import Tools.Bool
open import Tools.Level
open import Graded.Modality.Instances.Zero-one-many true as ππΟ
module Graded.Modality.Instances.Affine where
open ππΟ renaming (Zero-one-many to Affine) public
open import Graded.Modality Affine
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
import Definition.Typed.Restrictions
open import Definition.Untyped
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
open import Tools.Sum
private variable
p : Affine
pα΅’ : Sequence Affine
affineModality : Modality
affineModality = zero-one-many-modality
open Graded.Mode.Instances.Zero-one.Variant affineModality
open Graded.Modality.Properties affineModality
alternative-greater :
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)
alternative-greater =
(π , π , π , π , π , (Ξ» ()))
, Ξ» where
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π Ο π β refl
π π π Ο π β refl
π π π Ο Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π Ο π β refl
π π π Ο π β refl
π π π Ο Ο β refl
π π Ο π π β refl
π π Ο π π β refl
π π Ο π Ο β refl
π π Ο π π β refl
π π Ο π π β refl
π π Ο π Ο β refl
π π Ο Ο π β refl
π π Ο Ο π β refl
π π Ο Ο Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π Ο π β refl
π π π Ο π β refl
π π π Ο Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π Ο π β refl
π π π Ο π β refl
π π π Ο Ο β refl
π π Ο π π β refl
π π Ο π π β refl
π π Ο π Ο β refl
π π Ο π π β refl
π π Ο π π β refl
π π Ο π Ο β refl
π π Ο Ο π β refl
π π Ο Ο π β refl
π π Ο Ο Ο β refl
π Ο π π π β refl
π Ο π π π β refl
π Ο π π Ο β refl
π Ο π π π β refl
π Ο π π π β refl
π Ο π π Ο β refl
π Ο π Ο π β refl
π Ο π Ο π β refl
π Ο π Ο Ο β refl
π Ο π π π β refl
π Ο π π π β refl
π Ο π π Ο β refl
π Ο π π π β refl
π Ο π π π β refl
π Ο π π Ο β refl
π Ο π Ο π β refl
π Ο π Ο π β refl
π Ο π Ο Ο β refl
π Ο Ο π π β refl
π Ο Ο π π β refl
π Ο Ο π Ο β refl
π Ο Ο π π β refl
π Ο Ο π π β refl
π Ο Ο π Ο β refl
π Ο Ο Ο π β refl
π Ο Ο Ο π β refl
π Ο Ο Ο Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π Ο π β refl
π π π Ο π β refl
π π π Ο Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π Ο π β refl
π π π Ο π β refl
π π π Ο Ο β refl
π π Ο π π β refl
π π Ο π π β refl
π π Ο π Ο β refl
π π Ο π π β refl
π π Ο π π β refl
π π Ο π Ο β refl
π π Ο Ο π β refl
π π Ο Ο π β refl
π π Ο Ο Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π Ο π β refl
π π π Ο π β refl
π π π Ο Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π π π β refl
π π π π π β refl
π π π π Ο β refl
π π π Ο π β refl
π π π Ο π β refl
π π π Ο Ο β refl
π π Ο π π β refl
π π Ο π π β refl
π π Ο π Ο β refl
π π Ο π π β refl
π π Ο π π β refl
π π Ο π Ο β refl
π π Ο Ο π β refl
π π Ο Ο π β refl
π π Ο Ο Ο β refl
π Ο π π π β refl
π Ο π π π β refl
π Ο π π Ο β refl
π Ο π π π β refl
π Ο π π π β refl
π Ο π π Ο β refl
π Ο π Ο π β refl
π Ο π Ο π β refl
π Ο π Ο Ο β refl
π Ο π π π β refl
π Ο π π π β refl
π Ο π π Ο β refl
π Ο π π π β refl
π Ο π π π β refl
π Ο π π Ο β refl
π Ο π Ο π β refl
π Ο π Ο π β refl
π Ο π Ο Ο β refl
π Ο Ο π π β refl
π Ο Ο π π β refl
π Ο Ο π Ο β refl
π Ο Ο π π β refl
π Ο Ο π π β refl
π Ο Ο π Ο β refl
π Ο Ο Ο π β refl
π Ο Ο Ο π β refl
π Ο Ο Ο Ο β refl
Ο π π π π β refl
Ο π π π π β refl
Ο π π π Ο β refl
Ο π π π π β refl
Ο π π π π β refl
Ο π π π Ο β refl
Ο π π Ο π β refl
Ο π π Ο π β refl
Ο π π Ο Ο β refl
Ο π π π π β refl
Ο π π π π β refl
Ο π π π Ο β refl
Ο π π π π β refl
Ο π π π π β refl
Ο π π π Ο β refl
Ο π π Ο π β refl
Ο π π Ο π β refl
Ο π π Ο Ο β refl
Ο π Ο π π β refl
Ο π Ο π π β refl
Ο π Ο π Ο β refl
Ο π Ο π π β refl
Ο π Ο π π β refl
Ο π Ο π Ο β refl
Ο π Ο Ο π β refl
Ο π Ο Ο π β refl
Ο π Ο Ο Ο β refl
Ο π π π π β refl
Ο π π π π β refl
Ο π π π Ο β refl
Ο π π π π β refl
Ο π π π π β refl
Ο π π π Ο β refl
Ο π π Ο π β refl
Ο π π Ο π β refl
Ο π π Ο Ο β refl
Ο π π π π β refl
Ο π π π π β refl
Ο π π π Ο β refl
Ο π π π π β refl
Ο π π π π β refl
Ο π π π Ο β refl
Ο π π Ο π β refl
Ο π π Ο π β refl
Ο π π Ο Ο β refl
Ο π Ο π π β refl
Ο π Ο π π β refl
Ο π Ο π Ο β refl
Ο π Ο π π β refl
Ο π Ο π π β refl
Ο π Ο π Ο β refl
Ο π Ο Ο π β refl
Ο π Ο Ο π β refl
Ο π Ο Ο Ο β refl
Ο Ο π π π β refl
Ο Ο π π π β refl
Ο Ο π π Ο β refl
Ο Ο π π π β refl
Ο Ο π π π β refl
Ο Ο π π Ο β refl
Ο Ο π Ο π β refl
Ο Ο π Ο π β refl
Ο Ο π Ο Ο β refl
Ο Ο π π π β refl
Ο Ο π π π β refl
Ο Ο π π Ο β refl
Ο Ο π π π β refl
Ο Ο π π π β refl
Ο Ο π π Ο β refl
Ο Ο π Ο π β refl
Ο Ο π Ο π β refl
Ο Ο π Ο Ο β refl
Ο Ο Ο π π β refl
Ο Ο Ο π π β refl
Ο Ο Ο π Ο β refl
Ο Ο Ο π π β refl
Ο Ο Ο π π β refl
Ο Ο Ο π Ο β refl
Ο Ο Ο Ο π β refl
Ο Ο Ο Ο π β refl
Ο Ο Ο Ο Ο β refl
instance
affine-has-well-behaved-zero :
Has-well-behaved-zero affineModality
affine-has-well-behaved-zero = zero-one-many-has-well-behaved-zero
β€π : p β€ π
β€π {p = π} = refl
β€π {p = π} = refl
β€π {p = Ο} = refl
opaque
π-GLB-inv :
Modality.Greatest-lower-bound zero-one-many-modality π pα΅’ β
β i β pα΅’ i β‘ π β pα΅’ i β‘ π
π-GLB-inv π-glb i = lemma _ (π-glb .projβ i)
where
lemma : β p β π β€ p β p β‘ π β p β‘ π
lemma π _ = injβ refl
lemma π _ = injβ refl
lemma Ο ()
opaque
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
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 β‘ π β
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 π π π (πβ€ , _) = injβ (injβ (injβ (refl , refl , refl)))
nrα΅’-GLB-π-inv π π π (πβ€ , _) = case πβ€ 2 of Ξ» ()
nrα΅’-GLB-π-inv Ο π π (πβ€ , _) = case πβ€ 2 of Ξ» ()
nrα΅’-GLB-π-inv r π Ο (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv π π π (πβ€ , _) = injβ (injβ (injβ (refl , refl , refl)))
nrα΅’-GLB-π-inv π π π (πβ€ , _) = injβ (refl , refl , refl)
nrα΅’-GLB-π-inv Ο π π (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv π π π (πβ€ , _) = injβ (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
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 β‘ π β 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β (injβ (rβ‘π , _ , pβ‘π))) β injβ (injβ (pβ‘π , rβ‘π))
(injβ (injβ (injβ (_ , () , _))))
(injβ (injβ (injβ (rβ‘π , _ , pβ‘π)))) β injβ (injβ (pβ‘π , rβ‘π))
module _ {πα΅-allowed : Bool} where
private
variant : Mode-variant
variant = record
{ πα΅-allowed = πα΅-allowed
; π-well-behaved = Ξ» _ β affine-has-well-behaved-zero
}
open Graded.Mode.Instances.Zero-one variant
open Definition.Typed.Restrictions affineModality
open Graded.Usage.Restrictions affineModality Zero-one-isMode
open Graded.FullReduction.Assumptions variant
private variable
rs : Type-restrictions
us : Usage-restrictions
Suitable-for-full-reduction :
Type-restrictions β Set
Suitable-for-full-reduction rs =
(β p β Ξ£Λ’-allowed π p β T πα΅-allowed) Γ
(β p β Β¬ Ξ£Λ’-allowed Ο p)
where
open Type-restrictions rs
suitable-for-full-reduction :
Type-restrictions β β Suitable-for-full-reduction
suitable-for-full-reduction rs =
record rs
{ Ξ Ξ£-allowed = Ξ» b p q β
Ξ Ξ£-allowed b p q Γ
(b β‘ BMΞ£ π€ Γ p β‘ π β T πα΅-allowed) Γ
Β¬ (b β‘ BMΞ£ π€ Γ p β‘ Ο)
; []-cong-allowed = Ξ» s β
[]-cong-allowed s Γ T πα΅-allowed
; []-congβErased = Ξ» (okβ , okβ) β
[]-congβErased okβ .projβ , []-congβErased okβ .projβ
, (Ξ» _ β okβ) , Ξ» ()
; []-congβΒ¬Trivial =
Ξ» _ β non-trivial β¦ affine-has-well-behaved-zero β¦
}
, (Ξ» _ β (_$ (refl , refl)) ββ projβ ββ projβ)
, (Ξ» _ β (_$ (refl , refl)) ββ projβ ββ projβ)
where
open Type-restrictions rs
full-reduction-assumptions :
Suitable-for-full-reduction rs β
Full-reduction-assumptions rs us
full-reduction-assumptions (πβπα΅ , Β¬Ο) = record
{ sinkβπβ€π = Ξ» _ _ β injβ refl
; β‘πβπβ€π = Ξ» where
{p = Ο} ok β β₯-elim (Β¬Ο _ ok)
{p = π} _ β injβ refl
{p = π} ok β injβ (refl , πβπα΅ _ ok , refl)
}
full-reduction-assumptions-suitable :
Full-reduction-assumptions rs us β Suitable-for-full-reduction rs
full-reduction-assumptions-suitable as =
(Ξ» p Ξ£-ok β case β‘πβπβ€π Ξ£-ok of Ξ» where
(injβ ())
(injβ (_ , πα΅-ok , _)) β πα΅-ok)
, Ξ» p Ξ£-ok β case β‘πβπβ€π Ξ£-ok of Ξ» where
(injβ ())
(injβ (() , _))
where
open Full-reduction-assumptions _ _ as