Verified Commit 1fbd26e9 authored by Camil Staps's avatar Camil Staps 🚀

Add uniqueness attributes to maps

parent 63c72973
Pipeline #32588 failed with stage
in 1 minute and 7 seconds
......@@ -11,7 +11,9 @@ definition module Data.IntMap.Base
*
* @property-test-with a = ()
*/
from StdOverloaded import class ==
from StdBool import not
from StdInt import bitand, bitxor
from StdOverloaded import class ==(==), class ~(~)
from Data.Functor import class Functor
from Data.Maybe import :: Maybe
......@@ -36,7 +38,10 @@ equal :: !(IntMap a) !(IntMap a) -> Bool | == a
bin :: !Prefix !Mask !(IntMap a) !(IntMap a) -> IntMap a
nomatch :: !Int !Prefix !Mask -> Bool
zero i m :== (i bitand m) == 0
//nomatch :: !Int !Prefix !Mask -> Bool
nomatch i p m :== not (mask i m == p)
empty :: IntMap a
......@@ -54,7 +59,7 @@ union :: !(IntMap a) !(IntMap a) -> IntMap a
unions :: ![IntMap a] -> IntMap a
mask :: !Int !Mask -> Prefix
mask i m :== i bitand (~m bitxor m)
shorter :: !Mask !Mask -> Bool
......
implementation module Data.IntMap.Base
import StdEnv
from StdBool import &&, ||, not
from StdClass import class Eq(..), class Ord(..)
import StdFunctions
from StdInt import bitand, bitor, bitxor, >>, bitnot, IF_INT_64_OR_32,
instance == Int, instance < Int, instance ~ Int, instance + Int, instance ^ Int
from StdList import foldl
from StdMisc import abort
from StdOverloaded import class <(<), class +(+), class ^(^), class ~(~)
from StdTuple import snd
import Control.Applicative
import Control.Monad
......@@ -1549,17 +1557,17 @@ bin _ _ l Nil = l
bin _ _ Nil r = r
bin p m l r = Bin p m l r
zero :: !Int !Mask -> Bool
zero i m = (i bitand m) == 0
//zero :: !Int !Mask -> Bool
//zero i m = (i bitand m) == 0
nomatch :: !Int !Prefix !Mask -> Bool
nomatch i p m = mask i m <> p
//nomatch :: !Int !Prefix !Mask -> Bool
//nomatch i p m = mask i m <> p
match :: !Int !Prefix !Mask -> Bool
match i p m = mask i m == p
mask :: !Int !Mask -> Prefix
mask i m = i bitand (~m bitxor m)
//mask :: !Int !Mask -> Prefix
//mask i m = i bitand (~m bitxor m)
// we have to treat the masks as unsigned ints
// this means that the sign bit has to be inverted to preserve order
......
......@@ -2,11 +2,8 @@ implementation module Data.IntMap.Strict
// Copied from Haskell's Data.IntMap 13 January 2015 by Jurriën Stutterheim
from StdFunc import o, id, const
from StdMisc import abort
from StdString import instance == {#Char}
from StdInt import class < (..), instance < Int, instance == Int, class + (..), instance + Int, bitand
from StdList import foldl
import StdEnv
from Data.GenEq import generic gEq
import Data.Maybe, Data.Either, Data.Functor
from Data.IntMap.Base import :: IntMap (..), :: Prefix, :: Mask, nomatch, bin, empty, fromDistinctAscList, mask, shorter, branchMask
......
......@@ -107,7 +107,7 @@ import StdClass
* sizes_correct r
*/
:: Map k v
= Bin !Int !k !v !(Map k v) !(Map k v)
= Bin !Int !k !v !.(Map k v) !.(Map k v)
| Tip
instance Monoid (Map k v) | < k
......@@ -145,7 +145,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 -> .Map k v
/**
* The number of elements in a Map.
......@@ -169,7 +169,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 !a !u:(Map k a) -> u:Map k a | < k
/**
* Searches for a value at a given key position. Works only for non-unique
......@@ -193,7 +193,7 @@ get k m :== get` k m
/**
* Searches for a value at a given key position. Works also for unique mappings.
*/
getU :: !k !w:(Map k v) -> x:(!Maybe v, !y:(Map k v)) | == k & < k, [ x <= y, w <= y]
getU :: !k !u:(Map k v) -> (!Maybe v, !u:(Map k v)) | == k & < k
/**
* Removes the value at a given key position. The mapping itself can be spine unique.
......@@ -215,8 +215,8 @@ del :: !k !(Map k a) -> Map k a | < k
*/
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]
foldrWithKey :: !(k v u:a -> u:a) !u:a !(Map k v) -> u:a
foldlWithKey :: !(.a -> .(k -> .(v -> .a))) !.a !(Map k v) -> .a
foldrWithKey :: !(k v u:a -> u:a) !u:a !.(Map k v) -> u:a
foldlWithKey :: !(.a -> .(k -> .(v -> .a))) !.a !.(Map k v) -> .a
//* @type (v a -> a) a (Map k v) -> a
foldrNoKey f x m :== foldrWithKey (\_ v acc -> f v acc) x m
......@@ -239,6 +239,9 @@ filterWithKey :: !(k v -> Bool) !(Map k v) -> Map k v
*/
keys m :== foldrWithKey (\k _ ks -> [k : ks]) [] m
//* Like `keys`, but also works with unique maps.
keysU :: !u:(Map k v) -> (![k], !u:Map k v)
/**
* A list of the elements in a Map.
* @type (Map k v) -> [v]
......
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