Implement IntMap using Patricia tree

[chshersh]

This pull request adds new data structure: IntMap based on patricia tree similar to haskell implementation. But it uses power of dependent types for:

• Store size of bits for key in type.
• Use Fin n data type for accessing to bits.
• TODO: Verify some invariants of data structure.

The last one isn't implemented. And I didn't implement all usual functions for Map-like data structure because I want to hear some feedback, what things are required to add and maybe some notes on how to prove some things. Currently supported functionality:

• size function in O(n) time
• lookup in O(min(n, w))
• insert in O(min(n,w))
• delete in O(min(n,w))
• Functor instance
• Foldable instance and also fromList and values functions

This data structure is supposed to be used as persistent and immutable array and should be much more efficient than AVLTree or RedBlackTree for integer keys. But, you know, we don't have criterion in Idris so I didn't perform benchmarks yet. Also IntMap can be used later to implement HashMap based on HAMT (which I was going to implement initiallyj, see some discussions about it). But HAMT requires arrays for efficient implementation and there're a lot for tricks to make HashMap fast. But good IntMap should be enough for first step.

[jfdm]

Thanks for the PR. Apologies for not addressing this sooner, I've been a bit behind in my work at the moment. Hopefully, I will get to this today or tomorrow.

[jfdm]

Right, I've had a time to look at this. I am not going to accept this, partly because I don't want to maintain it myself, and more importantly I think you should promote this in your own idris package on github.

An alternative, and highly recommended, option would be to make a PR to contrib in Idris dev itself. That is I see two useful contributions:

1) being the utilities for bit twiddling; and 2) the tree implementation itself.

I never intended my library to be the one stop shop for containers in Idris, and want to ensure that I can maintain my packages reasonably well.

Apologies.

Jan