The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Tue, Jan 20, 2009 at 12:48:55PM +0000, Ashish Darbari wrote:
> I'm having problems able to use the FMapAVL.
> It works out quite fine if I want the keys 
> to have the type z (IMap), but since I want to use
> this map in ocaml extracted code where keys
> will be ocaml integers, I want to define the
> equivalent module (IMap1) in Coq on Ints, but
> when I do it as shown below, I get an error,
> No such label lt. 
> 
> What am I missing?
> 
> Thanks
> Ashish
> 
> Require Import ZArith.
> Require Import OrderedType.
> Require Import OrderedTypeEx.
> Require Import FMapAVL.
> Require Import Int.
> 
> 
> Module IMap := FMapAVL.Make(Z_as_OT).
> 
> Module IMap1 := FMapAVL.Make(Z_as_Int).
> 
> 

Hi

I think you're mixing two notions: 

- First, these AVL trees are parametrized with respect to their data.
  These data correspond to the OrderedType interface, the only
  interesting part in this interface is that we should have a compare
  function over the data. Z_as_OT provides such an OrderedType for
  type Z.

- Second, these AVL use internally some integers to store the size of
  trees. On these integers, we need things like max and plus. This
  correspond to interface Int in Int.v, and Z_as_Int is an
  instantiation of Int based on Z, in order to be able to compute
  inside Coq.

Hence the most general functor in FSetAVL, named IntMake, expects
_both_ an Int (such as Z_as_Int) and a OrderedType (such as Z_as_OT).
And FSetAVL.Make is just a particular case of IntMake where the Int is
Z_as_Int, but where the OrderedType part is still to be given later.
This FSetAVL.Make is the functor aimed at casual Coq users. But if
you're interested in optimized extraction, you should use
FSetAVL.IntMap directly.

Now there are several possible ways to get ocaml int after extraction:

* For instance, you can axiomatize everything in Coq:

  Parameter int : Set.
  Parameter compare : int -> int -> comparison.
  Parameter max : int -> int -> int.
  ...
  
  then teach the extraction what to do with them
 
  Extract Constant int => "int".
  ...

  then create both an Int and an OrderedType based on your int
  
  Module IntInt <: Int.
   Definition int:=int.
   ...
  End.

  Module IntOrderedType <: OrderedType.
   Definition t := int.
   ...
  End.

  Then you can use IMap := FSetAVL.IntMake(IntInt)(IntOrderedType).

* Another approach is to do your whole development under a functor
  expecting both an Int module and an Orderedtype, for instance:

  Module MyDev (I:Int)(O:OrderedType with Definition O.t := I.int).
   ...
   Module IMap := FSetAVL.IntMake(I)(O).
   ...
   (*your development here. might be splitted in several file
     via repeated functors and/or use of include*)
   ...
  End.

  Then you extract this functor, and then create _in ocaml_ some
  instance of Int and OrderedType based on ocaml's int, and finally
  do the functor application in ocaml.

Hope this help...

Pierre L.