some bug fixes

This commit is contained in:
Brendan Hansknecht 2022-11-20 11:53:28 -08:00
parent 4fc0dd9dd9
commit 28835d5bf3
No known key found for this signature in database
GPG key ID: 0EA784685083E75B
8 changed files with 47 additions and 61 deletions

View file

@ -96,9 +96,7 @@ Dict k v := {
dataIndices : List Nat,
data : List (T k v),
size : Nat,
}
# TODO: re-add type definition one #4408 is fixed
# | k has Hash & Eq
} | k has Hash & Eq
## Return an empty dictionary.
empty : Dict k v | k has Hash & Eq
@ -457,13 +455,13 @@ insertAll = \xs, ys ->
keepShared : Dict k v, Dict k v -> Dict k v | k has Hash & Eq
keepShared = \xs, ys ->
walk
ys
xs
(\state, k, _ ->
if contains state k then
state
empty
(\state, k, v ->
if contains ys k then
insert state k v
else
remove state k
state
)
## Remove the key-value pairs in the first input that are also in the second

View file

@ -19,17 +19,18 @@ interface Set
Bool.{ Bool, Eq },
Dict.{ Dict },
Num.{ Nat },
Hash.{ Hasher, Hash },
Hash.{ Hash },
]
# We should have this line above the next has.
# It causes the formatter to fail currently.
# | k has Hash & Eq
Set k := Dict.Dict k {}
# TODO: re-add type definition one #4408 is fixed
# | k has Hash & Eq
has [
Eq {
isEq,
},
]
has [
Eq {
isEq,
},
]
isEq : Set k, Set k -> Bool | k has Hash & Eq
isEq = \_, _ -> Bool.true
@ -42,9 +43,6 @@ single : k -> Set k | k has Hash & Eq
single = \key ->
Dict.single key {} |> @Set
## Make sure never to insert a *NaN* to a [Set]! Because *NaN* is defined to be
## unequal to *NaN*, adding a *NaN* results in an entry that can never be
## retrieved or removed from the [Set].
insert : Set k, k -> Set k | k has Hash & Eq
insert = \@Set dict, key ->
Dict.insert dict key {} |> @Set