z-snails/idris2-hashmap

Hash-array map tries in Idris2

idris2-hashmap's Issues

`keys` and `toList` omits the second element.

This is despite the key being considered present in the hashmap.

Minimal example:

module Main
import Data.HashMap
%default total

{- Create test cases with upt to 5 elements -}
Test1 : HashMap String Nat ; Test1 = insert "foo"  0 empty
Test2 : HashMap String Nat ; Test2 = insert "bar"  1 Test1
Test3 : HashMap String Nat ; Test3 = insert "baz"  2 Test2
Test4 : HashMap String Nat ; Test4 = insert "quux" 3 Test3
Test5 : HashMap String Nat ; Test5 = insert "frob" 4 Test4

{- check a single property -}
check : Show a => String -> a -> IO ()
check name prop = do
  putStrLn (name ++ ": " ++ show prop)

{- check all the properties for the given test case -}
test : String -> HashMap String Nat -> IO ()
test name testCase = do
  check (name ++ " Has Bar"   )      (lookup "bar" testCase == Just 1)
  check (name ++ " keys"      )      (keys testCase)
  check (name ++ " has bar in keys") (elem "bar" (keys testCase))

main : IO ()
main = do
  test "Test1" Test1
  test "Test2" Test2
  test "Test3" Test3
  test "Test4" Test4
  test "Test5" Test5

This results in the following output, which I'll summarize in a table below:

Test1 Has Bar: False
Test1 keys: ["foo"]
Test1 has bar in keys: False
Test2 Has Bar: True
Test2 keys: ["foo"]
Test2 has bar in keys: False
Test3 Has Bar: True
Test3 keys: ["foo", "baz"]
Test3 has bar in keys: False
Test4 Has Bar: True
Test4 keys: ["foo", "quux", "baz"]
Test4 has bar in keys: False
Test5 Has Bar: True
Test5 keys: ["foo", "frob", "quux", "baz"]
Test5 has bar in keys: False

Name	Has Bar	Keys	Bar in Keys	Expected
Test1	False	["foo"]	False	False
Test2	True	["foo"]	False	True
Test3	True	["foo", "baz"]	False	True
Test4	True	["foo", "quux", "baz"]	False	True
Test5	True	["foo", "frob", "quux", "baz"]	False	True

Sometihng is broken

I'm fairly sure it doesn't work 100% of the time.

Most likely this is due to collision2 or something to do with collision.