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
import Graded.Modality.Properties
open 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.Product
open import Tools.PropositionalEquality
open import Tools.Relation
open import Tools.Sum
open import Tools.Unit
private variable
p : Affine
affineModality : Modality
affineModality = zero-one-many-modality variant
open Definition.Typed.Restrictions affineModality
open Graded.Modality.Properties affineModality
open Graded.Usage.Restrictions affineModality
private variable
rs : Type-restrictions
us : Usage-restrictions
bad-affine-modality : Modality
bad-affine-modality = zero-one-many-greatest variant
alternative-greater :
(nr-available : Nr-available) β
let nrβ = affineModality
.Modality.has-nr nr-available .Has-nr.nr
nrβ = bad-affine-modality
.Modality.has-nr nr-available .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 (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 Γ
(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 ββ projβ
}
, (Ξ» _ β (_$ (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