-
Notifications
You must be signed in to change notification settings - Fork 2
feat: add Set/Map/MutMap without Order #80
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Draft
JonathanStarup
wants to merge
12
commits into
master
Choose a base branch
from
hashcollections
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Draft
Changes from all commits
Commits
Show all changes
12 commits
Select commit
Hold shift + click to select a range
f33b544
hashset
JonathanStarup f1067ab
work
JonathanStarup 43c2b47
work
JonathanStarup 330ac68
work
JonathanStarup 5865047
forgotfile
JonathanStarup 5b0a644
newlines
JonathanStarup 0b5188f
derive hash
JonathanStarup a0117d5
tests
JonathanStarup d5051a2
work
JonathanStarup 35dc2c5
work
JonathanStarup 8684e28
Merge branch 'master' into hashcollections
JonathanStarup 13c6bea
Merge branch 'master' into hashcollections
JonathanStarup File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,114 @@ | ||
| /// Keeps the log computational complexity of Set while removing | ||
| /// the `Order` constraint. | ||
| namespace HashMap { | ||
| use Hash.hash | ||
| use HashSet.HashSet | ||
|
|
||
| /// invariants: | ||
| /// <<A>> There are no mappings with empty lists | ||
| /// <<B>> there are no duplicates in the lists | ||
| pub opaque enum HashMap[k, v] with Eq, Hash { | ||
| case HashMap(Map[Int32, List[(k, v)]]) | ||
| } | ||
|
|
||
| pub def size(hm: HashMap[k, v]): Int32 = | ||
| // uses invariant <<B>> | ||
| unwrap(hm) |> Map.valuesOf |> List.sumWith(List.length) | ||
|
|
||
| pub def empty(): HashMap[k, v] = | ||
| HashMap(Map.empty()) | ||
|
|
||
| pub def insert(k: k, v: v, hm: HashMap[k, v]): HashMap[k, v] with Eq[k], Hash[k] = | ||
| let hashK = hash(k); | ||
| let HashMap(m) = hm; | ||
| let newList = match Map.get(hashK, m) { | ||
| case None => List.point((k, v)) | ||
| case Some(list) => listMapAdd(k, v, list) | ||
| }; | ||
| HashMap(Map.insert(hashK, newList, m)) | ||
|
|
||
| pub def remove(x: k, hm: HashMap[k, v]): HashMap[k, v] with Eq[k], Hash[k] = | ||
| let hashK = hash(x); | ||
| let HashMap(m) = hm; | ||
| match Map.get(hashK, m) { | ||
| case None => | ||
| hm | ||
| case Some(list) => | ||
| let newList = listMapRemove(x, list); | ||
| if (List.isEmpty(newList)) { | ||
| // uphold invariant <<A>> | ||
| HashMap(Map.remove(hashK, m)) | ||
| } else { | ||
| HashMap(Map.insert(hashK, newList, m)) | ||
| } | ||
| } | ||
|
|
||
| pub def isEmpty(hm: HashMap[k, v]): Bool = | ||
| // Uses invariant <<A>> | ||
| unwrap(hm) |> Map.isEmpty | ||
|
|
||
| pub def singleton(k: k, v: v): HashMap[k, v] with Eq[k], Hash[k]= | ||
| HashMap(Map#{hash(k) => List.point((k, v))}) | ||
|
|
||
| // todo: range | ||
|
|
||
| pub def get(k: k, hm: HashMap[k, v]): Option[v] with Eq[k], Hash[k] = | ||
| let HashMap(m) = hm; | ||
| let hashK = hash(k); | ||
| match Map.get(hashK, m) { | ||
| case None => | ||
| None | ||
| case Some(list) => | ||
| list |> List.findMap(match (k0, v) -> | ||
| (k0 == k) |> Utils.boolMap(_ -> v) | ||
| ) | ||
| } | ||
|
|
||
| pub def getWithDefault(k: k, d: v, hm: HashMap[k, v]): v with Eq[k], Hash[k] = | ||
| get(k, hm) |> Option.getWithDefault(d) | ||
|
|
||
| pub def memberOf(k: k, hm: HashMap[k, v]): Bool with Eq[k], Hash[k] = | ||
| let HashMap(m) = hm; | ||
| let hashK = hash(k); | ||
| match Map.get(hashK, m) { | ||
| case None => | ||
| false | ||
| case Some(list) => | ||
| List.exists(match (k0, _) -> k0 == k, list) | ||
| } | ||
|
|
||
| pub def keysOf(hm: HashMap[k, v]): HashSet[k] with Eq[k], Hash[k] = | ||
| let HashMap(m) = hm; | ||
| Map.valuesOf(m) |> | ||
| List.flatten |> | ||
| List.foldLeft( | ||
| (acc, mapping) -> HashSet.insert(fst(mapping), acc), | ||
| HashSet.empty() | ||
| ) | ||
|
|
||
| pub def valuesOf(hm: HashMap[k, v]): List[v] = | ||
| let HashMap(m) = hm; | ||
| Map.valuesOf(m) |> List.flatMap(List.map(snd)) | ||
|
|
||
| pub def fromList(l: List[(k, v)]): HashMap[k, v] with Eq[k], Hash[k] = | ||
| List.foldLeft(acc -> match (k, v) -> HashMap.insert(k, v, acc), HashMap.empty(), l) | ||
|
|
||
| // filterWithKey, mapWithKey, unzip, toList, filter, filterMap | ||
|
|
||
| // private | ||
|
|
||
| /// Alternative to let-match | ||
| def unwrap(hm: HashMap[k, v]): Map[Int32, List[(k, v)]] = | ||
| let HashMap(m) = hm; m | ||
|
|
||
| // Add mapping to list if key not present already, upholding <<A>>. | ||
| // Might reorder elements | ||
| def listMapAdd(k: k, v: v, c: List[(k, v)]): List[(k, v)] with Eq[k] = | ||
| (k, v) :: listMapRemove(k, c) | ||
|
|
||
| def listMapRemove(k: k, l: List[(k, v)]): List[(k, v)] with Eq[k] = | ||
| // Could maybe use invariant <<B>> for a little performance | ||
| // if a linked list like datastructure is used. | ||
| List.filter(match (k0, _) -> k != k0, l) | ||
|
|
||
| } | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,81 @@ | ||
| /// Keeps the log computational complexity of Set while removing | ||
| /// the `Order` constraint. | ||
| namespace HashSet { | ||
| use Hash.hash | ||
|
|
||
| /// invariants: | ||
| /// <<A>> There are no mappings with empty lists | ||
| /// <<B>> there are no duplicates in the lists | ||
| pub opaque enum HashSet[t] with Eq, Hash { | ||
| case HashSet(Map[Int32, List[t]]) | ||
| } | ||
|
|
||
| pub def size(s: HashSet[t]): Int32 = | ||
| // uses invariant <<B>> | ||
| unwrap(s) |> Map.valuesOf |> List.sumWith(List.length) | ||
|
|
||
| pub def empty(): HashSet[t] = | ||
| HashSet(Map.empty()) | ||
|
|
||
| pub def insert(x: t, s: HashSet[t]): HashSet[t] with Eq[t], Hash[t] = | ||
| let hashX = hash(x); | ||
| let HashSet(m) = s; | ||
| let newList = match Map.get(hashX, m) { | ||
| case None => List.point(x) | ||
| case Some(list) => listSetAdd(x, list) | ||
| }; | ||
| HashSet(Map.insert(hashX, newList, m)) | ||
|
|
||
| pub def remove(x: t, s: HashSet[t]): HashSet[t] with Eq[t], Hash[t] = | ||
| let hashX = hash(x); | ||
| let HashSet(m) = s; | ||
| match Map.get(hashX, m) { | ||
| case None => | ||
| s | ||
| case Some(list) => | ||
| let newList = listSetRemove(x, list); | ||
| if (List.isEmpty(newList)) { | ||
| // uphold invariant <<A>> | ||
| HashSet(Map.remove(hashX, m)) | ||
| } else { | ||
| HashSet(Map.insert(hashX, newList, m)) | ||
| } | ||
| } | ||
|
|
||
| pub def isEmpty(s: HashSet[a]): Bool = | ||
| // Uses invariant <<A>> | ||
| unwrap(s) |> Map.isEmpty | ||
|
|
||
| pub def singleton(x: t): HashSet[t] with Eq[t], Hash[t]= | ||
| HashSet(Map#{hash(x) => List.point(x)}) | ||
|
|
||
| // todo: range | ||
|
|
||
| pub def memberOf(x: t, s: HashSet[t]): Bool with Eq[t], Hash[t] = | ||
| let HashSet(m) = s; | ||
| let hashX = hash(x); | ||
| match Map.get(hashX, m) { | ||
| case None => false | ||
| case Some(list) => List.memberOf(x, list) | ||
| } | ||
|
|
||
| pub def fromList(l: List[t]): HashSet[t] with Eq[t], Hash[t] = | ||
| List.foldLeft((acc, e) -> HashSet.insert(e, acc), HashSet.empty(), l) | ||
|
|
||
| // private | ||
|
|
||
| /// Alternative to let-match | ||
| def unwrap(s: HashSet[t]): Map[Int32, List[t]] = | ||
| let HashSet(m) = s; m | ||
|
|
||
| // Add element to list if not present already, upholding <<A>>. | ||
| // Might reorder elements | ||
| def listSetAdd(x: t, c: List[t]): List[t] with Eq[t] = | ||
| x :: listSetRemove(x, c) | ||
|
|
||
| def listSetRemove(x: t, c: List[t]): List[t] with Eq[t] = | ||
| // Could maybe use invariant <<B>> for a little performance | ||
| // if a linked list like datastructure is used. | ||
| List.filter(y -> y != x, c) | ||
|
|
||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,118 @@ | ||
| /// Keeps the log computational complexity of Set while removing | ||
| /// the `Order` constraint. | ||
| namespace MutHashMap { | ||
| use Hash.hash | ||
| use HashSet.HashSet | ||
|
|
||
| /// invariants: | ||
| /// <<A>> There are no mappings with empty lists | ||
| /// <<B>> there are no duplicates in the lists | ||
| pub opaque enum MutHashMap[k: Type, v: Type, r: Region] { | ||
| case MutHashMap(MutMap[Int32, MutList[(k, v), r], r]) | ||
| } | ||
|
|
||
| instance Newable[MutHashMap[k, v]] { | ||
| pub def new(r: Region[r]): MutHashMap[k, v, r] & r = MutHashMap.new(r) | ||
| } | ||
|
|
||
| instance Scoped[MutHashMap[k, v]] { | ||
| pub def regionOf(_: MutHashMap[k, v, r]): Region[r] = () as Region[r] | ||
| } | ||
|
|
||
| pub def size(hm: MutHashMap[k, v, r]): Int32 \ Read(r) = | ||
| // uses invariant <<B>> | ||
| unwrap(hm) |> MutMap.valuesOf |> List.sumWith(MutList.length) | ||
|
|
||
| pub def new(r: Region[r]): MutHashMap[k, v, r] \ Write(r) = | ||
| MutHashMap(MutMap.new(r)) | ||
|
|
||
| pub def put!(k: k, v: v, hm: MutHashMap[k, v, r]): Unit \ {Read(r), Write(r)} with Eq[k], Hash[k] = | ||
| let hashK = hash(k); | ||
| let MutHashMap(m) = hm; | ||
| let r = Scoped.regionOf(hm); | ||
| match MutMap.get(hashK, m) { | ||
| case None => MutMap.put!(hashK, Utils/MutList.point(r, (k, v)), m) | ||
| case Some(list) => mutListMapAdd!(k, v, list) | ||
| } | ||
|
|
||
| pub def remove!(x: k, hm: MutHashMap[k, v, r]): Unit \ {Read(r), Write(r)} with Eq[k], Hash[k] = | ||
| let hashK = hash(x); | ||
| let MutHashMap(m) = hm; | ||
| match MutMap.get(hashK, m) { | ||
| case None => | ||
| () | ||
| case Some(list) => | ||
| mutListMapRemove!(x, list); | ||
| // uphold invariant <<A>> | ||
| MutList.isEmpty(list) |> | ||
| Utils.boolForeach(_ -> MutMap.remove!(hashK, m)) | ||
| } | ||
|
|
||
| pub def isEmpty(hm: MutHashMap[k, v, r]): Bool \ Read(r) = | ||
| // Uses invariant <<A>> | ||
| unwrap(hm) |> MutMap.isEmpty | ||
|
|
||
| pub def singleton(r: Region[r], k: k, v: v): MutHashMap[k, v, r] \ Write(r) with Eq[k], Hash[k] = | ||
| MutHashMap(MutMap.singleton(r, hash(k), Utils/MutList.point(r, (k, v)))) | ||
|
|
||
| // todo: range | ||
|
|
||
| pub def get(k: k, hm: MutHashMap[k, v, r]): Option[v] \ Read(r) with Eq[k], Hash[k] = | ||
| let MutHashMap(m) = hm; | ||
| let hashK = hash(k); | ||
| match MutMap.get(hashK, m) { | ||
| case None => | ||
| None | ||
| case Some(list) => | ||
| list |> | ||
| MutList.find(match (k0, _) -> (k0 == k)) |> | ||
| Option.map(snd) | ||
| } | ||
|
|
||
| pub def getWithDefault(k: k, d: v, hm: MutHashMap[k, v, r]): v \ Read(r) with Eq[k], Hash[k] = | ||
| get(k, hm) |> Option.getWithDefault(d) | ||
|
|
||
| pub def memberOf(k: k, hm: MutHashMap[k, v, r]): Bool \ Read(r) with Eq[k], Hash[k] = | ||
| let MutHashMap(m) = hm; | ||
| let hashK = hash(k); | ||
| match MutMap.get(hashK, m) { | ||
| case None => | ||
| false | ||
| case Some(list) => | ||
| MutList.exists(match (k0, _) -> k0 == k, list) | ||
| } | ||
|
|
||
| pub def keysOf(hm: MutHashMap[k, v, r]): HashSet[k] \ Read(r) with Eq[k], Hash[k] = | ||
| let MutHashMap(m) = hm; | ||
| MutMap.valuesOf(m) |> | ||
| List.map(MutList.toList) |> | ||
| List.flatten |> | ||
| List.foldLeft( | ||
| (acc, mapping) -> HashSet.insert(fst(mapping), acc), | ||
| HashSet.empty() | ||
| ) | ||
|
|
||
| pub def valuesOf(hm: MutHashMap[k, v, r]): List[v] \ Read(r) = | ||
| let MutHashMap(m) = hm; | ||
| MutMap.valuesOf(m) |> List.flatMap(ml -> ml |> MutList.toList |> List.map(snd)) | ||
|
|
||
| // filterWithKey, mapWithKey, unzip, toList, filter, filterMap | ||
|
|
||
| // private | ||
|
|
||
| /// Alternative to let-match | ||
| def unwrap(hm: MutHashMap[k, v, r]): MutMap[Int32, MutList[(k, v), r], r] = | ||
| let MutHashMap(m) = hm; m | ||
|
|
||
| // Add mapping to list if key not present already, upholding <<A>>. | ||
| // Might reorder elements | ||
| def mutListMapAdd!(k: k, v: v, l: MutList[(k, v), r]): Unit \ Write(r) with Eq[k] = | ||
| mutListMapRemove!(k, l); | ||
| MutList.push!((k, v), l) | ||
|
|
||
| def mutListMapRemove!(k: k, l: MutList[(k, v), r]): Unit \ {Read(r), Write(r)} with Eq[k] = | ||
| // Could maybe use invariant <<B>> for a little performance | ||
| // if a linked list like datastructure is used. | ||
| MutList.retain!(match (k0, _) -> k != k0, l) | ||
|
|
||
| } |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we express these as laws?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Or maybe laws are public and we need private ones?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't see any law usage in ex. List. How would you use it here (like syntax and everything, I've never used it :P).
Also, isn't laws on Magnus' chopping block?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually the first one you can take care of by using a Nel instead of a list.
For
Byou can do something like this I think:Alternatively you could introduce a
ListSettype which itself would have that law.