FMapFullAVL
This file contains some complements to
FMapAVL.
- Functor AvlProofs proves that trees of FMapAVL are not only
binary search trees, but moreover well-balanced ones. This is done
by proving that all operations preserve the balancing.
- We then pack the previous elements in a IntMake functor
similar to the one of
FMapAVL, but richer.
- In final IntMake_ord functor, the compare function is
different from the one in
FMapAVL: this non-structural
version is closer to the original Ocaml code.
Encapsulation
We can implement
S with balanced binary search trees.
When compared to
FMapAVL, we maintain here two invariants
(bst and avl) instead of only bst, which is enough for fulfilling
the FMap interface.