kowainik / idris-patricia Goto Github PK

There was an attempt to ensure some invariants on IntMap:

https://github.com/ChShersh/idris-patricia/blob/22f8e41283d42bd8979a6e0260615c257deee0ac/Patricia/IntMap.idr#L64

This implementation is not working. But it's needed to be done. And probably different approach should be applied to this problem (using external proofs rather than internal).

Currently there's believe_me in the proof part:

https://github.com/ChShersh/idris-patricia/blob/22f8e41283d42bd8979a6e0260615c257deee0ac/Patricia/BitsUtils.idr#L65

This should be rewritten using proofs for bits from this package:

https://github.com/sbp/idris-bi

Probably, it's not ready yet though...

Usually, it's better to use a proper build tool:

• https://github.com/elba/elba

It would be good to add CODEOWNERS file to this repository making me as a default CODEOWNER and @arbuztw as CODEOWNER of IntSet module.

Simple tests are running extremely slow. I know that current implementation is far from optimal. But maybe something can be done to improve this...

Currently there's only IntMap data structure. But it would be good to have IntSet as well.

This can be implemented easily by creating simple wrapper around IntMap like it's done here for AVL tree:

https://github.com/jfdm/idris-containers/blob/master/Data/AVL/Set.idr

All functions for IntMap should be duplicated:

• size
• member
• insert
• delete

If some functions from #5 will be implemented earlier than IntSet then those functions should be duplicated as well if possible.

Currently only few functions are available for IntMap. It would be really good to move as many functions as possible from Haskell containers package to Idris.

You can create Pull Request for each single function. You don't need to implement all functions in one PR. Let others to contribute into this package :) But please, create similar function for IntSet once #4 is done.

Installing dependencies...
1: Specdris
Cloning into 'specdris'...
remote: Enumerating objects: 399, done.
remote: Total 399 (delta 0), reused 0 (delta 0), pack-reused 399
Receiving objects: 100% (399/399), 61.60 KiB | 152.00 KiB/s, done.
Resolving deltas: 100% (197/197), done.
Entering directory `./src'
Can't find import Builtins
Can't find import Prelude
Can't find import System
Can't find import Builtins
Can't find import Prelude
Can't find import Data/Bits

I really want to have CI in this repository.

It would be really good to use nix like in this repo:

https://github.com/jfdm/idris-containers

But instructions to install specdris are also required:

https://github.com/pheymann/specdris

It was announced recently. Probably a good idea to update 🙂

• https://github.com/edwinb/Idris2