18
20
using (BoundedVec; []; _∷_)
19
21
open import Data.Product using (_,_)
20
22
open import Data.Sum using (_⊎_; inj₁; inj₂)
21
open import Data.Function
22
25
open import Relation.Binary
23
26
import Relation.Binary.InducedPreorders as Ind
27
open import Relation.Binary.PropositionalEquality using (_≡_)
24
28
open import Relation.Nullary
25
29
open import Relation.Nullary.Negation
26
30
open RawMonad ¬¬-Monad
33
data Colist (A : Set) : Set where
37
data Colist {a} (A : Set a) : Set a where
35
39
_∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A
37
data Any {A} (P : A → Set) : Colist A → Set where
41
data Any {a p} {A : Set a} (P : A → Set p) :
42
Colist A → Set (a ⊔ p) where
38
43
here : ∀ {x xs} (px : P x) → Any P (x ∷ xs)
39
44
there : ∀ {x xs} (pxs : Any P (♭ xs)) → Any P (x ∷ xs)
41
data All {A} (P : A → Set) : Colist A → Set where
46
data All {a p} {A : Set a} (P : A → Set p) :
47
Colist A → Set (a ⊔ p) where
43
49
_∷_ : ∀ {x xs} (px : P x) (pxs : ∞ (All P (♭ xs))) → All P (x ∷ xs)
45
51
------------------------------------------------------------------------
48
null : ∀ {A} → Colist A → Bool
54
null : ∀ {a} {A : Set a} → Colist A → Bool
50
56
null (_ ∷ _) = false
52
length : ∀ {A} → Colist A → Coℕ
58
length : ∀ {a} {A : Set a} → Colist A → Coℕ
54
60
length (x ∷ xs) = suc (♯ length (♭ xs))
56
map : ∀ {A B} → (A → B) → Colist A → Colist B
62
map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Colist A → Colist B
58
64
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)
60
fromList : ∀ {A} → List A → Colist A
66
fromList : ∀ {a} {A : Set a} → List A → Colist A
62
68
fromList (x ∷ xs) = x ∷ ♯ fromList xs
64
take : ∀ {A} (n : ℕ) → Colist A → BoundedVec A n
70
take : ∀ {a} {A : Set a} (n : ℕ) → Colist A → BoundedVec A n
66
72
take (suc n) [] = []
67
73
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)
69
replicate : ∀ {A} → Coℕ → A → Colist A
75
replicate : ∀ {a} {A : Set a} → Coℕ → A → Colist A
70
76
replicate zero x = []
71
77
replicate (suc n) x = x ∷ ♯ replicate (♭ n) x
73
lookup : ∀ {A} → ℕ → Colist A → Maybe A
79
lookup : ∀ {a} {A : Set a} → ℕ → Colist A → Maybe A
74
80
lookup n [] = nothing
75
81
lookup zero (x ∷ xs) = just x
76
82
lookup (suc n) (x ∷ xs) = lookup n (♭ xs)
80
_++_ : ∀ {A} → Colist A → Colist A → Colist A
86
_++_ : ∀ {a} {A : Set a} → Colist A → Colist A → Colist A
82
88
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)
84
concat : ∀ {A} → Colist (List⁺ A) → Colist A
90
concat : ∀ {a} {A : Set a} → Colist (List⁺ A) → Colist A
86
92
concat ([ x ]⁺ ∷ xss) = x ∷ ♯ concat (♭ xss)
87
93
concat ((x ∷ xs) ∷ xss) = x ∷ ♯ concat (xs ∷ xss)
89
[_] : ∀ {A} → A → Colist A
95
[_] : ∀ {a} {A : Set a} → A → Colist A
92
98
------------------------------------------------------------------------
99
data _≈_ {A} : (xs ys : Colist A) → Set where
105
data _≈_ {a} {A : Set a} : (xs ys : Colist A) → Set a where
101
107
_∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys
103
109
-- The equality relation forms a setoid.
105
setoid : Set → Setoid _ _
111
setoid : ∀ {ℓ} → Set ℓ → Setoid _ _
106
112
setoid A = record
107
113
{ Carrier = Colist A
128
134
module ≈-Reasoning where
129
135
import Relation.Binary.EqReasoning as EqR
131
open module R {A : Set} = EqR (setoid A) public
137
open module R {a} {A : Set a} = EqR (setoid A) public
133
139
-- map preserves equality.
135
map-cong : ∀ {A B} (f : A → B) → _≈_ =[ map f ]⇒ _≈_
141
map-cong : ∀ {a b} {A : Set a} {B : Set b}
142
(f : A → B) → _≈_ =[ map f ]⇒ _≈_
136
143
map-cong f [] = []
137
144
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)
146
data _∈_ {A : Set} : A → Colist A → Set where
147
here : ∀ {x xs} → x ∈ x ∷ xs
148
there : ∀ {x y xs} (x∈xs : x ∈ ♭ xs) → x ∈ y ∷ xs
153
_∈_ : ∀ {a} → {A : Set a} → A → Colist A → Set a
154
x ∈ xs = Any (_≡_ x) xs
150
156
-- xs ⊆ ys means that xs is a subset of ys.
154
_⊆_ : {A : Set} → Colist A → Colist A → Set
160
_⊆_ : ∀ {a} → {A : Set a} → Colist A → Colist A → Set a
155
161
xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys
157
163
-- xs ⊑ ys means that xs is a prefix of ys.
161
data _⊑_ {A : Set} : Colist A → Colist A → Set where
167
data _⊑_ {a} {A : Set a} : Colist A → Colist A → Set a where
162
168
[] : ∀ {ys} → [] ⊑ ys
163
169
_∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys
165
171
-- Prefixes are subsets.
167
⊑⇒⊆ : {A : Set} → _⊑_ {A = A} ⇒ _⊆_
173
⊑⇒⊆ : ∀ {a} → {A : Set a} → _⊑_ {A = A} ⇒ _⊆_
169
⊑⇒⊆ (x ∷ xs⊑ys) here = here
175
⊑⇒⊆ (x ∷ xs⊑ys) (here ≡x) = here ≡x
170
176
⊑⇒⊆ (_ ∷ xs⊑ys) (there x∈xs) = there (⊑⇒⊆ (♭ xs⊑ys) x∈xs)
172
178
-- The prefix relation forms a poset.
174
⊑-Poset : Set → Poset _ _ _
180
⊑-Poset : ∀ {ℓ} → Set ℓ → Poset _ _ _
175
181
⊑-Poset A = record
176
182
{ Carrier = Colist A
196
201
trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)
198
⊑-resp-≈ˡ : {xs : Colist A} → (λ ys → xs ⊑ ys) Respects _≈_
200
⊑-resp-≈ˡ (x ∷ xs≈) (.x ∷ p) = x ∷ ♯ ⊑-resp-≈ˡ (♭ xs≈) (♭ p)
202
⊑-resp-≈ʳ : {ys : Colist A} → (λ xs → xs ⊑ ys) Respects _≈_
204
⊑-resp-≈ʳ (x ∷ xs≈) (.x ∷ p) = x ∷ ♯ ⊑-resp-≈ʳ (♭ xs≈) (♭ p)
206
203
antisym : Antisymmetric _≈_ _⊑_
207
204
antisym [] [] = []
208
205
antisym (x ∷ p₁) (.x ∷ p₂) = x ∷ ♯ antisym (♭ p₁) (♭ p₂)
210
207
module ⊑-Reasoning where
211
208
import Relation.Binary.PartialOrderReasoning as POR
213
open module R {A : Set} = POR (⊑-Poset A)
210
open module R {a} {A : Set a} = POR (⊑-Poset A)
214
211
public renaming (_≤⟨_⟩_ to _⊑⟨_⟩_)
216
213
-- The subset relation forms a preorder.
218
⊆-Preorder : Set → Preorder _ _ _
215
⊆-Preorder : ∀ {ℓ} → Set ℓ → Preorder _ _ _
220
217
Ind.InducedPreorder₂ (setoid A) _∈_
221
(λ xs≈ys → ⊑⇒⊆ $ ⊑P.reflexive xs≈ys)
218
(λ xs≈ys → ⊑⇒⊆ (⊑P.reflexive xs≈ys))
222
219
where module ⊑P = Poset (⊑-Poset A)
224
221
module ⊆-Reasoning where
225
222
import Relation.Binary.PreorderReasoning as PreR
227
open module R {A : Set} = PreR (⊆-Preorder A)
224
open module R {a} {A : Set a} = PreR (⊆-Preorder A)
228
225
public renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)
232
_∈⟨_⟩_ : ∀ {A : Set} (x : A) {xs ys} →
229
_∈⟨_⟩_ : ∀ {a} {A : Set a} (x : A) {xs ys} →
233
230
x ∈ xs → xs IsRelatedTo ys → x ∈ ys
234
231
x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs
236
233
-- take returns a prefix.
238
take-⊑ : ∀ {A} n (xs : Colist A) →
239
let toColist = fromList ∘ BVec.toList in
235
take-⊑ : ∀ {a} {A : Set a} n (xs : Colist A) →
236
let toColist = fromList {a} ∘ BVec.toList in
240
237
toColist (take n xs) ⊑ xs
241
238
take-⊑ zero xs = []
242
239
take-⊑ (suc n) [] = []
248
245
-- Finite xs means that xs has finite length.
250
data Finite {A : Set} : Colist A → Set where
247
data Finite {a} {A : Set a} : Colist A → Set a where
252
249
_∷_ : ∀ x {xs} (fin : Finite (♭ xs)) → Finite (x ∷ xs)
254
251
-- Infinite xs means that xs has infinite length.
256
data Infinite {A : Set} : Colist A → Set where
253
data Infinite {a} {A : Set a} : Colist A → Set a where
257
254
_∷_ : ∀ x {xs} (inf : ∞ (Infinite (♭ xs))) → Infinite (x ∷ xs)
259
256
-- Colists which are not finite are infinite.
261
258
not-finite-is-infinite :
262
{A : Set} (xs : Colist A) → ¬ Finite xs → Infinite xs
259
∀ {a} {A : Set a} (xs : Colist A) → ¬ Finite xs → Infinite xs
263
260
not-finite-is-infinite [] hyp with hyp []
265
262
not-finite-is-infinite (x ∷ xs) hyp =
266
263
x ∷ ♯ not-finite-is-infinite (♭ xs) (hyp ∘ _∷_ x)
268
265
-- Colists are either finite or infinite (classically).
267
-- TODO: Make this definition universe polymorphic.
270
269
finite-or-infinite :
271
270
{A : Set} (xs : Colist A) → ¬ ¬ (Finite xs ⊎ Infinite xs)
278
277
-- Colists are not both finite and infinite.
280
279
not-finite-and-infinite :
281
{A : Set} {xs : Colist A} → Finite xs → Infinite xs → ⊥
280
∀ {a} {A : Set a} {xs : Colist A} → Finite xs → Infinite xs → ⊥
282
281
not-finite-and-infinite [] ()
283
282
not-finite-and-infinite (x ∷ fin) (.x ∷ inf) =
284
283
not-finite-and-infinite fin (♭ inf)
added
removed
src/Data/Colist.agda
