open import Tools.Bool
open import Tools.Level
open import Graded.Modality.Instances.Zero-one-many true as ππΟ
open import Graded.Modality.Variant lzero
module Graded.Modality.Instances.Affine
(variant : Modality-variant)
where
open Modality-variant variant
open ππΟ renaming (Zero-one-many to Affine) public
open import Graded.Modality Affine
open import Graded.FullReduction.Assumptions
open import Definition.Typed.Restrictions Affine
open import Tools.Empty
open import Tools.Function
open import Tools.Nullary
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Sum
open import Tools.Unit
private variable
p : Affine
rs : Type-restrictions
affineModality : Modality
affineModality = zero-one-many-greatest variant _
affine-has-well-behaved-zero : Has-well-behaved-zero (Modality.semiring-with-meet affineModality)
affine-has-well-behaved-zero = zero-one-many-has-well-behaved-zero
β€π : p β€ π
β€π {p = π} = refl
β€π {p = π} = refl
β€π {p = Ο} = refl
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 Γ T πα΅-allowed Γ p β’ Ο
}
, (Ξ» _ β projβ ββ projβ)
, (Ξ» _ β (_$ refl) ββ projβ ββ projβ)
where
open Type-restrictions rs
full-reduction-assumptions :
Suitable-for-full-reduction rs β
Full-reduction-assumptions affineModality rs
full-reduction-assumptions (πβπα΅ , Β¬Ο) = record
{ πβ€π = Ξ» _ β refl
; β‘πβπβ€π = Ξ» where
{p = Ο} ok β β₯-elim (Β¬Ο _ ok)
{p = π} _ β injβ refl
{p = π} ok β injβ (refl , πβπα΅ _ ok , refl)
}