This package implements map from integer key to values. Data structure can be used as persistent array. Implementation is based on article about patricia trees and on existing Haskell implementation from containers
package. Dependent types can help to ensure some invariants for data structure.
λΠ> the (Int32Map String) $ insert 3 "a" Empty
Leaf (MkBits 3) "a" : IntBitMap 32 String
λΠ> the (Int32Map String) $ delete 3 $ insert 3 "a" Empty
Empty : IntBitMap 32 String
λΠ> the (Int32Map String) $ insert 2 "c" $ insert 4 "b" $ insert 3 "a" Empty
Bin (MkBits 3)
(FS (FS FZ))
(Bin (MkBits 2) FZ (Leaf (MkBits 2) "c") (Leaf (MkBits 3) "a"))
(Leaf (MkBits 4) "b") : IntBitMap 32 String
λΠ> toList $ the (IntBitMap 32 String) $ insert 2 "c" $ insert 4 "b" $ insert 3 "a" Empty
["c", "a", "b"] : List String
Just run this command to build project and run tests.
nix-shell -A idris-patricia --command "bash install-dependencies.sh && idris --testpkg patricia-nix.ipkg --idrispath dependencies/specdris/src"
- Install
specdris
following instructions from repository. - Run
idris --testpkg patricia.ipkg
.