Extracting FSet and FMap to OCaml

Using Coq
1

Hi,

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.

Any tips?

Thanks.

2

One idea is to use modular extraction: isolate the Map and Set instantiations in their own module(s), and swap out the corresponding extracted files for custom ones which implement the same interface. You may have to be extra careful to not expose the internals of Map and Set in the rest of your code, e.g., definitions using Eval _ in _ or tactics should not leave partially evaluated Map and Set operations.

3

Good idea. That is easier than messing around with definition of sets in Coq.