← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Data/Sets.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-05-24 10:26:15 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110524102615-9tontf43bq9ym690
Tags: 0.5-1
http://bugs.debian.org/573807
http://bugs.debian.org/598708
* [9251e0b] Imported Upstream version 0.5
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [2c82171] Add watch file
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly
* [540ca3f] Improve short description
* [6b3e794] Add dependencies on compatible versions of the Agda library
* [7127678] Standards-Version bump to 3.9.2, no changes required
* [9d0ae30] Update to use ghc instead of ghc6
* [3f6879a] Set Maintainer to my d.o email address

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Sets.agda
1
 
------------------------------------------------------------------------
2
 
------------------------------------------------------------------------
3
 
 
4
 
module Data.Sets where
5
 
 
6
 
open import Relation.Nullary
7
 
open import Relation.Binary
8
 
open import Relation.Binary.OrderMorphism
9
 
open import Data.Function
10
 
open import Data.List as L using (List)
11
 
open import Data.Product using (∃; _×_)
12
 
open import Level
13
 
 
14
 
module Sets₁ (dto : DecTotalOrder zero zero zero) where
15
 
 
16
 
  open DecTotalOrder dto public using (_≈_)
17
 
  open DecTotalOrder dto hiding (_≈_)
18
 
 
19
 
  infixr 6 _∪_
20
 
  infix  5 _∈?_
21
 
  infix  4 _∈_ _|≈|_
22
 
 
23
 
  abstract postulate decSetoid : DecSetoid _ _
24
 
 
25
 
  <Set> : Set
26
 
  <Set> = DecSetoid.Carrier decSetoid
27
 
 
28
 
  _|≈|_ : Rel <Set> zero
29
 
  _|≈|_ = DecSetoid._≈_ decSetoid
30
 
 
31
 
  abstract
32
 
   postulate
33
 
    empty  : <Set>
34
 
    insert : Carrier → <Set> → <Set>
35
 
    _∪_    : <Set> → <Set> → <Set>
36
 
    _∈_    : Carrier → <Set> → Set
37
 
    _∈?_   : (x : Carrier) → (s : <Set>) → Dec (x ∈ s)
38
 
    toList : <Set> → List Carrier
39
 
 
40
 
   postulate
41
 
    prop-∈-insert₁ : ∀ {x y s} → x ≈ y → x ∈ insert y s
42
 
    prop-∈-insert₂ : ∀ {x y s} → x ∈ s → x ∈ insert y s
43
 
    prop-∈-insert₃ : ∀ {x y s} → ¬ x ≈ y → x ∈ insert y s → x ∈ s
44
 
 
45
 
    prop-∈-empty : ∀ {x} → ¬ x ∈ empty
46
 
 
47
 
    prop-∈-∪ : ∀ {x s₁ s₂} → x ∈ s₁ → x ∈ s₁ ∪ s₂
48
 
 
49
 
    prop-∪₁ : ∀ {s₁ s₂}    → s₁ ∪ s₂        |≈| s₂ ∪ s₁
50
 
    prop-∪₂ : ∀ {s₁ s₂ s₃} → s₁ ∪ (s₂ ∪ s₃) |≈| (s₁ ∪ s₂) ∪ s₃
51
 
 
52
 
    prop-∈-|≈| : ∀ {x} → (λ s → x ∈ s) Respects _|≈|_
53
 
    prop-∈-≈   : ∀ {s} → (λ x → x ∈ s) Respects  _≈_
54
 
 
55
 
    -- TODO: Postulates for toList.
56
 
 
57
 
  singleton : Carrier → <Set>
58
 
  singleton x = insert x empty
59
 
 
60
 
  ⋃_ : List <Set> → <Set>
61
 
  ⋃_ = L.foldr _∪_ empty
62
 
 
63
 
  fromList : List Carrier → <Set>
64
 
  fromList = L.foldr insert empty
65
 
 
66
 
  _⊆_ : <Set> → <Set> → Set
67
 
  s₁ ⊆ s₂ = ∀ x → x ∈ s₁ → x ∈ s₂
68
 
 
69
 
open Sets₁ public
70
 
open DecTotalOrder hiding (_≈_)
71
 
open _⇒-Poset_
72
 
 
73
 
abstract
74
 
 postulate
75
 
  map : ∀ {do₁ do₂} → do₁ ⇒-DTO do₂ → <Set> do₁ → <Set> do₂
76
 
  mapToSet : ∀ {do₁ do₂} →
77
 
             (Carrier do₁ → <Set> do₂) →
78
 
             <Set> do₁ → <Set> do₂
79
 
 
80
 
  prop-map-∈₁ : ∀ {do₁ do₂ f x s} →
81
 
                      x ⟨ _∈_ do₁ ⟩       s →
82
 
                fun f x ⟨ _∈_ do₂ ⟩ map f s
83
 
  prop-map-∈₂ : ∀ {do₁ do₂ f y s} →
84
 
                y ⟨ _∈_ do₂ ⟩ map f s →
85
 
                ∃ λ x → (fun f x ⟨ _≈_ do₂ ⟩ y) ×
86
 
                        (      x ⟨ _∈_ do₁ ⟩ s)
87
 
 
88
 
  prop-mapToSet₁ : ∀ {do₁ do₂ f x s} →
89
 
                     x ⟨ _∈_ do₁ ⟩            s →
90
 
                   f x ⟨ _⊆_ do₂ ⟩ mapToSet f s
91
 
  prop-mapToSet₂ : ∀ {do₁ do₂ f y s} →
92
 
                   y ⟨ _∈_ do₂ ⟩ mapToSet f s →
93
 
                   ∃ λ x → (y ⟨ _∈_ do₂ ⟩ f x) ×
94
 
                           (x ⟨ _∈_ do₁ ⟩ s)