import Graded.Modality
open import Graded.Usage.Restrictions
module Graded.Usage
{a} {M : Set a}
(open Graded.Modality M)
(π : Modality)
(R : Usage-restrictions π)
where
open Modality π
open Usage-restrictions R
open import Graded.Context π
open import Graded.Context.Properties π
open import Graded.Modality.Dedicated-nr π
open import Graded.Mode π
open import Graded.Usage.Erased-matches
open import Definition.Untyped M hiding (_β_)
open import Tools.Bool using (T; true; false)
open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat)
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Relation
open import Tools.Sum using (_β_)
infix 10 _βΈ[_]_
private
variable
n : Nat
p q r : M
Ξ³ Ξ³β² Ξ³β Ξ³β Ξ³β Ξ³β Ξ³β
Ξ³β Ξ΄ Ξ· ΞΈ Ο : Conβ n
A B F G : Term n
t u v w z : Term n
x : Fin n
m mβ² : Mode
b : BinderMode
s : Strength
em : Erased-matches
data ββ-view (A : Set a) (em : Erased-matches) : Set a where
is-all : em β‘ all β ββ-view A em
is-some-yes : em β‘ some β A β ββ-view A em
is-other : em β€α΅α΅ some β (em β‘ some β Β¬ A) β ββ-view A em
opaque
ββ-view-inhabited : {A : Set a} β Dec A β β em β ββ-view A em
ββ-view-inhabited _ all = is-all refl
ββ-view-inhabited (yes p) some = is-some-yes refl p
ββ-view-inhabited (no p) some = is-other _ (Ξ» _ β p)
ββ-view-inhabited _ none = is-other _ (Ξ» ())
opaque
J-view : β p q m β ββ-view (p β‘ π Γ q β‘ π) (erased-matches-for-J m)
J-view p q _ = ββ-view-inhabited (is-π? p Γ-dec is-π? q) _
opaque
K-view : β p m β ββ-view (p β‘ π) (erased-matches-for-K m)
K-view p _ = ββ-view-inhabited (is-π? p) _
infix 50 β_β
mutual
β_β :
β¦ has-nr : Has-nr semiring-with-meet β¦ β
Term n β Mode β Conβ n
β var x β m = παΆ , x β β m β
β U β _ = παΆ
β Ξ Ξ£β¨ _ β© p , q β· F βΉ G β m = β F β (m α΅Β· p) +αΆ tailβ (β G β m)
β lam p t β m = tailβ (β t β m)
β t ββ¨ p β© u β m = β t β m +αΆ p Β·αΆ β u β (m α΅Β· p)
β prod π¨ p t u β m = p Β·αΆ β t β (m α΅Β· p) +αΆ β u β m
β prod π€ p t u β m = p Β·αΆ β t β (m α΅Β· p) β§αΆ β u β m
β fst p t β m = β t β m
β snd p t β m = β t β m
β prodrec r _ _ _ t u β m =
r Β·αΆ β t β (m α΅Β· r) +αΆ tailβ (tailβ (β u β m))
β β β _ = παΆ
β zero β _ = παΆ
β suc t β m = β t β m
β natrec p _ r _ z s n β m =
nrαΆ p r (β z β m) (tailβ (tailβ (β s β m))) (β n β m)
β Unit! β _ = παΆ
β star! β _ = παΆ
β unitrec p q A t u β m = p Β·αΆ β t β (m α΅Β· p) +αΆ β u β m
β Empty β _ = παΆ
β emptyrec p _ t β m = p Β·αΆ β t β (m α΅Β· p)
β Id _ t u β m = case Id-erased? of Ξ» where
(yes _) β παΆ
(no _) β β t β m +αΆ β u β m
β rfl β _ = παΆ
β J p q _ t B u v w β m with J-view p q m
β¦ | is-all _ = β u β m
β¦ | is-some-yes _ _ = Ο Β·αΆ (tailβ (tailβ (β B β m)) +αΆ β u β m)
β¦ | is-other _ _ =
Ο Β·αΆ
(β t β m +αΆ tailβ (tailβ (β B β m)) +αΆ
β u β m +αΆ β v β m +αΆ β w β m)
β K p _ t B u v β m with K-view p m
β¦ | is-all _ = β u β m
β¦ | is-some-yes _ _ = Ο Β·αΆ (tailβ (β B β m) +αΆ β u β m)
β¦ | is-other _ _ =
Ο Β·αΆ (β t β m +αΆ tailβ (β B β m) +αΆ β u β m +αΆ β v β m)
β []-cong _ _ _ _ _ β _ = παΆ
data _β_β_ : (x : Fin n) (p : M) (Ξ³ : Conβ n) β Set a where
here : x0 β p β Ξ³ β p
there : (h : x β p β Ξ³) β (x +1) β p β Ξ³ β q
open import Graded.Modality.Dedicated-nr.Instance
data _βΈ[_]_ {n : Nat} : (Ξ³ : Conβ n) β Mode β Term n β Set a where
Uβ : παΆ βΈ[ m ] U
ββ : παΆ βΈ[ m ] β
Emptyβ : παΆ βΈ[ m ] Empty
Unitβ : παΆ βΈ[ m ] Unit s
Ξ Ξ£β : Ξ³ βΈ[ m α΅Β· p ] F
β Ξ΄ β β m β Β· q βΈ[ m ] G
β Ξ³ +αΆ Ξ΄ βΈ[ m ] Ξ Ξ£β¨ b β© p , q β· F βΉ G
var : (παΆ , x β β m β) βΈ[ m ] var x
lamβ : Ξ³ β β m β Β· p βΈ[ m ] t
β Ξ³ βΈ[ m ] lam p t
_ββ_ : Ξ³ βΈ[ m ] t
β Ξ΄ βΈ[ m α΅Β· p ] u
β Ξ³ +αΆ p Β·αΆ Ξ΄ βΈ[ m ] t ββ¨ p β© u
prodΚ·β : Ξ³ βΈ[ m α΅Β· p ] t
β Ξ΄ βΈ[ m ] u
β p Β·αΆ Ξ³ +αΆ Ξ΄ βΈ[ m ] prodΚ· p t u
prodΛ’β : Ξ³ βΈ[ m α΅Β· p ] t
β Ξ΄ βΈ[ m ] u
β p Β·αΆ Ξ³ β§αΆ Ξ΄ βΈ[ m ] prodΛ’ p t u
fstβ : β m
β Ξ³ βΈ[ m α΅Β· p ] t
β m α΅Β· p β‘ mβ²
β (mβ² β‘ πα΅ β p β€ π)
β Ξ³ βΈ[ mβ² ] fst p t
sndβ : Ξ³ βΈ[ m ] t
β Ξ³ βΈ[ m ] snd p t
prodrecβ : Ξ³ βΈ[ m α΅Β· r ] t
β Ξ΄ β β m β Β· r Β· p β β m β Β· r βΈ[ m ] u
β Ξ· β β πα΅? β Β· q βΈ[ πα΅? ] A
β Prodrec-allowed m r p q
β r Β·αΆ Ξ³ +αΆ Ξ΄ βΈ[ m ] prodrec r p q A t u
zeroβ : παΆ βΈ[ m ] zero
sucβ : Ξ³ βΈ[ m ] t
β Ξ³ βΈ[ m ] suc t
natrecβ : β {s n} β¦ has-nr : Dedicated-nr β¦
β Ξ³ βΈ[ m ] z
β Ξ΄ β β m β Β· p β β m β Β· r βΈ[ m ] s
β Ξ· βΈ[ m ] n
β ΞΈ β β πα΅? β Β· q βΈ[ πα΅? ] A
β nrαΆ p r Ξ³ Ξ΄ Ξ· βΈ[ m ] natrec p q r A z s n
natrec-no-nrβ :
β {n s} β¦ no-nr : No-dedicated-nr β¦
β Ξ³ βΈ[ m ] z
β Ξ΄ β β m β Β· p β β m β Β· r βΈ[ m ] s
β Ξ· βΈ[ m ] n
β ΞΈ β β πα΅? β Β· q βΈ[ πα΅? ] A
β Ο β€αΆ Ξ³
β (T πα΅-allowed β
Ο β€αΆ Ξ΄)
β (β¦ π-well-behaved :
Has-well-behaved-zero semiring-with-meet β¦ β
Ο β€αΆ Ξ·)
β Ο β€αΆ Ξ΄ +αΆ p Β·αΆ Ξ· +αΆ r Β·αΆ Ο
β Ο βΈ[ m ] natrec p q r A z s n
emptyrecβ : Ξ³ βΈ[ m α΅Β· p ] t
β Ξ΄ βΈ[ πα΅? ] A
β Emptyrec-allowed m p
β p Β·αΆ Ξ³ βΈ[ m ] emptyrec p A t
starΚ·β : παΆ βΈ[ m ] starΚ·
starΛ’β : (Β¬StarΛ’-sink β παΆ βαΆ Ξ³)
β β m β Β·αΆ Ξ³ βΈ[ m ] starΛ’
unitrecβ : Ξ³ βΈ[ m α΅Β· p ] t
β Ξ΄ βΈ[ m ] u
β Ξ· β β πα΅? β Β· q βΈ[ πα΅? ] A
β Unitrec-allowed m p q
β p Β·αΆ Ξ³ +αΆ Ξ΄ βΈ[ m ] unitrec p q A t u
Idβ : Β¬ Id-erased
β Ξ³ βΈ[ πα΅? ] A
β Ξ΄ βΈ[ m ] t
β Ξ· βΈ[ m ] u
β Ξ΄ +αΆ Ξ· βΈ[ m ] Id A t u
Idββ : Id-erased
β Ξ³ βΈ[ πα΅? ] A
β Ξ΄ βΈ[ πα΅? ] t
β Ξ· βΈ[ πα΅? ] u
β παΆ βΈ[ m ] Id A t u
rflβ : παΆ βΈ[ m ] rfl
Jβ : erased-matches-for-J m β€α΅α΅ some
β (erased-matches-for-J m β‘ some β Β¬ (p β‘ π Γ q β‘ π))
β Ξ³β βΈ[ πα΅? ] A
β Ξ³β βΈ[ m ] t
β Ξ³β β β m β Β· p β β m β Β· q βΈ[ m ] B
β Ξ³β βΈ[ m ] u
β Ξ³β
βΈ[ m ] v
β Ξ³β βΈ[ m ] w
β Ο Β·αΆ (Ξ³β +αΆ Ξ³β +αΆ Ξ³β +αΆ Ξ³β
+αΆ Ξ³β) βΈ[ m ] J p q A t B u v w
Jβββ : erased-matches-for-J m β‘ some
β p β‘ π
β q β‘ π
β Ξ³β βΈ[ πα΅? ] A
β Ξ³β βΈ[ πα΅? ] t
β Ξ³β β π β π βΈ[ m ] B
β Ξ³β βΈ[ m ] u
β Ξ³β
βΈ[ πα΅? ] v
β Ξ³β βΈ[ πα΅? ] w
β Ο Β·αΆ (Ξ³β +αΆ Ξ³β) βΈ[ m ] J p q A t B u v w
Jβββ : erased-matches-for-J m β‘ all
β Ξ³β βΈ[ πα΅? ] A
β Ξ³β βΈ[ πα΅? ] t
β Ξ³β β β πα΅? β Β· p β β πα΅? β Β· q βΈ[ πα΅? ] B
β Ξ³β βΈ[ m ] u
β Ξ³β
βΈ[ πα΅? ] v
β Ξ³β βΈ[ πα΅? ] w
β Ξ³β βΈ[ m ] J p q A t B u v w
Kβ : erased-matches-for-K m β€α΅α΅ some
β (erased-matches-for-K m β‘ some β p β’ π)
β Ξ³β βΈ[ πα΅? ] A
β Ξ³β βΈ[ m ] t
β Ξ³β β β m β Β· p βΈ[ m ] B
β Ξ³β βΈ[ m ] u
β Ξ³β
βΈ[ m ] v
β Ο Β·αΆ (Ξ³β +αΆ Ξ³β +αΆ Ξ³β +αΆ Ξ³β
) βΈ[ m ] K p A t B u v
Kβββ : erased-matches-for-K m β‘ some
β p β‘ π
β Ξ³β βΈ[ πα΅? ] A
β Ξ³β βΈ[ πα΅? ] t
β Ξ³β β π βΈ[ m ] B
β Ξ³β βΈ[ m ] u
β Ξ³β
βΈ[ πα΅? ] v
β Ο Β·αΆ (Ξ³β +αΆ Ξ³β) βΈ[ m ] K p A t B u v
Kβββ : erased-matches-for-K m β‘ all
β Ξ³β βΈ[ πα΅? ] A
β Ξ³β βΈ[ πα΅? ] t
β Ξ³β β β πα΅? β Β· p βΈ[ πα΅? ] B
β Ξ³β βΈ[ m ] u
β Ξ³β
βΈ[ πα΅? ] v
β Ξ³β βΈ[ m ] K p A t B u v
[]-congβ : Ξ³β βΈ[ πα΅? ] A
β Ξ³β βΈ[ πα΅? ] t
β Ξ³β βΈ[ πα΅? ] u
β Ξ³β βΈ[ πα΅? ] v
β παΆ βΈ[ m ] []-cong s A t u v
sub : Ξ³ βΈ[ m ] t
β Ξ΄ β€αΆ Ξ³
β Ξ΄ βΈ[ m ] t
starβ : παΆ {n} βΈ[ m ] star s
starβ {s = π€} =
sub (starΛ’β Ξ» _ β βαΆ-refl)
(β€αΆ-reflexive (βαΆ-sym (Β·αΆ-zeroΚ³ _)))
starβ {s = π¨} = starΚ·β