I’m working on developing a compiler in Coq, and I need to use sets & maps. So far I’ve been using FSetAVL and FMapAVL, which let me compute examples in Coq and extract nicely to OCaml. But I’d really just like to use OCaml’s sets and maps. I realize this defeats the purpose of having verified set/map implementations, but I’d like the extracted code to be as concise as possible, and when I tried manually editing the extracted code to use OCaml’s sets and maps it improved performance significantly.
For reference, I’m using FSetAVL and FMapAVL in this file.
I thought something like the following might work:
Module FSet := FSetAVL.Make(Coq.Structures.OrderedTypeEx.Nat_as_OT). Extract Constant FSet.union => "...". Recursive Extraction FSet.union.
But this doesn’t seem to do anything. It just extracts the normal AVL implementation.
I could axiomatize maps/sets and use “Extract Constant” on my axiomatization, but I don’t want break my existing proofs and I like being able to compute examples within Coq.