Commit d2befbab authored by Camil Staps's avatar Camil Staps 🙂

Merge branch 'getU' into 'master'

adapt types of function on Data.Map to work on maps with unique values

See merge request !337
parents 4dc09c14 28784f9a
Pipeline #42893 passed with stage
in 2 minutes and 18 seconds
......@@ -151,7 +151,7 @@ newMap :: w:(Map k u:v), [ w <= u]
* Create a Map with one element.
* @complexity O(1)
*/
singleton :: !k !v -> Map k v
singleton :: !k !v:v -> u:Map k v:v, [u <= v]
/**
* The number of elements in a Map.
......@@ -160,6 +160,13 @@ singleton :: !k !v -> Map k v
*/
mapSize :: !(Map k v) -> Int
/**
* The number of elements in a possibly unique Map.
* @property corresponds to mapSize: A.m :: Map k v:
* fst (mapSizeU m) =.= mapSize m
*/
mapSizeU :: !u:(Map k v:v) -> (!Int, !u:Map k v:v), [u <= v]
/**
* Adds or replaces the value for a given key.
*
......@@ -175,7 +182,7 @@ mapSize :: !(Map k v) -> Int
* m` = put k v m
* @complexity O(log n)
*/
put :: !k !a !(Map k a) -> Map k a | < k
put :: !k !v:v !u:(Map k v:v) -> u:Map k v:v | < k
special k=Int; k=String
/**
......@@ -222,8 +229,8 @@ del :: !k !(Map k a) -> Map k a | < k
/**
* Removes the value at a given key position. The mapping can be unique.
*/
delU :: !a !.(Map a b) -> u:(!v:(Maybe b), !Map a b) | == a & < a, [u <= v] // !k !w:(Map k u:v) -> x:(Maybe u:v, !y:(Map k u:v)) | == k & < k, [ w y <= u, x <= y, w <= y]
special a=Int; a=String
delU :: !k !w:(Map k u:v) -> x:(Maybe u:v, !y:(Map k u:v)) | == k & < k, [ w y <= u, x <= y, w <= y]
special k=Int; k=String
foldrWithKey :: !(k v u:a -> u:a) !u:a !(Map k v) -> u:a
foldlWithKey :: !(.a -> .(k -> .(v -> .a))) !.a !(Map k v) -> .a
......
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment