blob: e2706a02b07ba5c3d4b40a179c73048999eb11a3 (
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
|
module Bidir where
data Bool : Set where
true : Bool
false : Bool
not : Bool → Bool
not true = false
not false = true
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
equal? : ℕ -> ℕ -> Bool
equal? zero zero = true
equal? (suc n) (suc m) = equal? n m
equal? _ _ = false
data Maybe (A : Set) : Set where
nothing : Maybe A
just : A → Maybe A
maybeToBool : {A : Set} → Maybe A → Bool
maybeToBool nothing = false
maybeToBool (just _) = true
maybe′ : {A B : Set} → (A → Maybe B) → Maybe B → Maybe A → Maybe B
maybe′ y _ (just a) = y a
maybe′ _ n nothing = n
data _×_ (A B : Set) : Set where
_,_ : A → B → A × B
data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A
_++_ : {A : Set} → List A → List A → List A
_++_ [] ys = ys
_++_ (x ∷ xs) ys = x ∷ (xs ++ ys)
map : {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs
zip : {A B : Set} → List A → List B → List (A × B)
zip (a ∷ as) (b ∷ bs) = (a , b) ∷ zip as bs
zip _ _ = []
data _==_ {A : Set}(x : A) : A → Set where
refl : x == x
module NatMap where
NatMap : Set → Set
NatMap A = List (ℕ × A)
lookup : {A : Set} → ℕ → NatMap A → Maybe A
lookup n [] = nothing
lookup n ((m , a) ∷ xs) with equal? n m
lookup n ((m , a) ∷ xs) | true = just a
lookup n ((m , a) ∷ xs) | false = lookup n xs
notMember : {A : Set} → ℕ → NatMap A → Bool
notMember n m = not (maybeToBool (lookup n m))
-- For now we simply prepend the element. This may lead to duplicates.
insert : {A : Set} → ℕ → A → NatMap A → NatMap A
insert n a m = (n , a) ∷ m
fromAscList : {A : Set} → List (ℕ × A) → NatMap A
fromAscList [] = []
fromAscList ((n , a) ∷ xs) = insert n a (fromAscList xs)
empty : {A : Set} → NatMap A
empty = []
union : {A : Set} → NatMap A → NatMap A → NatMap A
union [] m = m
union ((n , a) ∷ xs) m = insert n a (union xs m)
open NatMap
checkInsert : {A : Set} → (A → A → Bool) → ℕ → A → NatMap A → Maybe (NatMap A)
checkInsert eq i b m with lookup i m
checkInsert eq i b m | just c with eq b c
checkInsert eq i b m | just c | true = just m
checkInsert eq i b m | just c | false = nothing
checkInsert eq i b m | nothing = just (insert i b m)
assoc : {A : Set} → (A → A → Bool) → List ℕ → List A → Maybe (NatMap A)
assoc _ [] [] = just empty
assoc eq (i ∷ is) (b ∷ bs) = maybe′ (checkInsert eq i b) nothing (assoc eq is bs)
assoc _ _ _ = nothing
--data Equal? where
-- same ...
-- different ...
generate : {A : Set} → (ℕ → A) → List ℕ → NatMap A
generate f [] = empty
generate f (n ∷ ns) = insert n (f n) (generate f ns)
-- this lemma is probably wrong, because two different NatMaps may represent the same semantic value.
lemma-1 : {τ : Set} → (eq : τ → τ → Bool) → (f : ℕ → τ) → (is : List ℕ) → assoc eq is (map f is) == just (generate f is)
lemma-1 eq f [] = refl
lemma-1 eq f (i ∷ is′) = {!!}
|
