blob: 8e6603b9219f35f5746de1de744f6e067bc3cf58 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary using (REL; _Respects_; Setoid)
module Cfe.Type.Base
{c ℓ} (over : Setoid c ℓ)
where
open Setoid over using (trans) renaming (Carrier to C; _≈_ to _∼_)
open import Cfe.Language over hiding (_∙_; _≈_)
open import Data.Bool renaming (_∨_ to _∨ᵇ_; _≤_ to _≤ᵇ_)
open import Data.Empty.Polymorphic using (⊥)
open import Data.Product using (_×_)
open import Data.Sum using (_⊎_; map)
open import Function
open import Level
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary using (¬_)
private
variable
a b fℓ lℓ fℓ₁ lℓ₁ fℓ₂ lℓ₂ : Level
------------------------------------------------------------------------
-- Definitions
infix 2 _⇒_
_⇒_ : Bool → (C → Set a) → C → Set a
false ⇒ A = const ⊥
true ⇒ A = A
record Type fℓ lℓ : Set (c ⊔ ℓ ⊔ suc (fℓ ⊔ lℓ)) where
field
null : Bool
first : C → Set fℓ
flast : C → Set lℓ
first-cong : first Respects _∼_
flast-cong : flast Respects _∼_
------------------------------------------------------------------------
-- Special Types
τ⊥ : Type fℓ lℓ
τ⊥ = record
{ null = false
; first = const ⊥
; flast = const ⊥
; first-cong = λ _ ()
; flast-cong = λ _ ()
}
τε : Type fℓ lℓ
τε = record
{ null = true
; first = const ⊥
; flast = const ⊥
; first-cong = λ _ ()
; flast-cong = λ _ ()
}
τ[_] : C → Type ℓ ℓ
τ[ c ] = record
{ null = false
; first = c ∼_
; flast = const ⊥
; first-cong = flip trans
; flast-cong = λ _ ()
}
------------------------------------------------------------------------
-- Type Operations
infix 7 _∙_
infix 6 _∨_
_∙_ : Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂)
τ₁ ∙ τ₂ = record
{ null = τ₁.null ∧ τ₂.null
; first = λ c → τ₁.first c ⊎ (τ₁.null ⇒ τ₂.first) c
; flast = λ c → τ₂.flast c ⊎ (τ₂.null ⇒ λ c → τ₂.first c ⊎ τ₁.flast c) c
; first-cong = λ {c} {c′} c∼c′ →
map
(τ₁.first-cong c∼c′)
(case τ₁.null
return (λ b → (b ⇒ τ₂.first) c → (b ⇒ τ₂.first) c′)
of λ
{ true → τ₂.first-cong c∼c′
; false → id
})
; flast-cong = λ {c} {c′} c∼c′ →
map
(τ₂.flast-cong c∼c′)
(case τ₂.null
return (λ b →
(b ⇒ λ c → τ₂.first c ⊎ τ₁.flast c) c →
(b ⇒ λ c → τ₂.first c ⊎ τ₁.flast c) c′)
of λ
{ true → map (τ₂.first-cong c∼c′) (τ₁.flast-cong c∼c′)
; false → id
})
}
where
module τ₁ = Type τ₁
module τ₂ = Type τ₂
_∨_ : Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ lℓ₂)
τ₁ ∨ τ₂ = record
{ null = τ₁.null ∨ᵇ τ₂.null
; first = λ c → τ₁.first c ⊎ τ₂.first c
; flast = λ c → τ₁.flast c ⊎ τ₂.flast c
; first-cong = λ c∼c′ → map (τ₁.first-cong c∼c′) (τ₂.first-cong c∼c′)
; flast-cong = λ c∼c′ → map (τ₁.flast-cong c∼c′) (τ₂.flast-cong c∼c′)
}
where
module τ₁ = Type τ₁
module τ₂ = Type τ₂
------------------------------------------------------------------------
-- Relations
infix 4 _≈_ _≤_ _≥_ _⊨_ _⊛_ _#_
record _≈_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
module τ₁ = Type τ₁
module τ₂ = Type τ₂
field
n≡n : τ₁.null ≡ τ₂.null
f₁⊆f₂ : ∀ {c} → τ₁.first c → τ₂.first c
f₁⊇f₂ : ∀ {c} → τ₂.first c → τ₁.first c
l₁⊆l₂ : ∀ {c} → τ₁.flast c → τ₂.flast c
l₁⊇l₂ : ∀ {c} → τ₂.flast c → τ₁.flast c
record _≤_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
module τ₁ = Type τ₁
module τ₂ = Type τ₂
field
n≤n : τ₁.null ≤ᵇ τ₂.null
f⊆f : ∀ {c} → τ₁.first c → τ₂.first c
l⊆l : ∀ {c} → τ₁.flast c → τ₂.flast c
_≥_ : REL (Type fℓ₁ lℓ₁) (Type fℓ₂ lℓ₂) _
_≥_ = flip _≤_
record _⊨_ (A : Language a) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
module τ = Type τ
field
n⇒n : Null A → T (τ.null)
f⇒f : ∀ {c} → First A c → τ.first c
l⇒l : ∀ {c} → Flast A c → τ.flast c
record _⊛_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ lℓ₁ ⊔ fℓ₂) where
private
module τ₁ = Type τ₁
module τ₂ = Type τ₂
field
∄[l₁∩f₂] : ∀ {c} → ¬ (τ₁.flast c × τ₂.first c)
¬n₁ : ¬ T (τ₁.null)
record _#_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ fℓ₂) where
private
module τ₁ = Type τ₁
module τ₂ = Type τ₂
field
∄[f₁∩f₂] : ∀ {c} → ¬ (τ₁.first c × τ₂.first c)
¬n₁∨¬n₂ : ¬ (T τ₁.null × T τ₂.null)
|
