module Graded.Restrictions {a} {M : Set a} where
open import Tools.Bool
open import Tools.Function
open import Tools.Level
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Unit
open import Graded.Modality M
open import Graded.Usage.Restrictions M
open import Definition.Typed.Restrictions M
no-type-restrictions : Type-restrictions
no-type-restrictions = λ where
.Unit-allowed → Lift _ ⊤
.ΠΣ-allowed → λ _ _ _ → Lift _ ⊤
where
open Type-restrictions
no-usage-restrictions : Usage-restrictions
no-usage-restrictions = λ where
.Prodrec-allowed → λ _ _ _ → Lift _ ⊤
where
open Usage-restrictions
equal-binder-quantities : Type-restrictions → Type-restrictions
equal-binder-quantities R = record R
{ ΠΣ-allowed = λ b p q → ΠΣ-allowed b p q × p ≡ q
}
where
open Type-restrictions R
second-ΠΣ-quantities-𝟘 :
Modality → Type-restrictions → Type-restrictions
second-ΠΣ-quantities-𝟘 𝕄 R = record R
{ ΠΣ-allowed = λ b p q → ΠΣ-allowed b p q × q ≡ 𝟘
}
where
open Modality 𝕄
open Type-restrictions R
second-ΠΣ-quantities-𝟘-or-ω :
M → Modality → Type-restrictions → Type-restrictions
second-ΠΣ-quantities-𝟘-or-ω ω 𝕄 R = record R
{ ΠΣ-allowed = λ b p q →
ΠΣ-allowed b p q ×
(p ≡ ω → q ≡ ω) ×
(p ≢ ω → q ≡ 𝟘)
}
where
open Modality 𝕄
open Type-restrictions R
No-erased-matches : Modality → Usage-restrictions → Set a
No-erased-matches 𝕄 R =
𝟙 ≢ 𝟘 → ∀ {r p q} → Prodrec-allowed r p q → r ≢ 𝟘
where
open Modality 𝕄
open Usage-restrictions R
no-erased-matches : Modality → Usage-restrictions → Usage-restrictions
no-erased-matches 𝕄 R = record R
{ Prodrec-allowed = λ r p q →
Prodrec-allowed r p q × (𝟙 ≢ 𝟘 → r ≢ 𝟘)
}
where
open Modality 𝕄
open Usage-restrictions R
No-erased-matches-no-erased-matches :
∀ 𝕄 R → No-erased-matches 𝕄 (no-erased-matches 𝕄 R)
No-erased-matches-no-erased-matches
𝕄 R 𝟙≢𝟘 {r = r} {p = p} {q = q} =
Prodrec-allowed r p q × (𝟙 ≢ 𝟘 → r ≢ 𝟘) →⟨ proj₂ ⟩
(𝟙 ≢ 𝟘 → r ≢ 𝟘) →⟨ _$ 𝟙≢𝟘 ⟩
r ≢ 𝟘 □
where
open Modality 𝕄
open Usage-restrictions R