The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 1 Feb 2013 23:55:48 +0200,
Dmitry Grebeniuk 
<gdsfh1 AT gmail.com>
 a écrit :

> Hello.
> 
>   Is there an easy way to FMapAVL with string keys?
>   I haven't found one, so I'm asking here.
> 
>   Also I've encountered many problems while trying
> to do this:
> 
> 1. I can't "Print Module Type" to understand what types
> should have module's structure items to be able to
> pass this module as an argument to the functor
> FMapAVL.Make.
> 
> 2. I can't figure out what type has
> "Coq.Structures.Orders.OrderedType" due to many
> module types' inclusions, and I have no explicitely
> written OrderedType module type.  (also links in
> http://coq.inria.fr/distrib/V8.4beta/stdlib/ doesn't
> work ("#anchor" is empty, at least in many links
> from page [1]))
> 
> 3. Writing ascii_lt / string_lt is a boring thing.  Can
> anybody share this code (if exists)?  Also other
> functions from OrderedType are in my interests too
> (sorry, can't say which types they should have,
> only names).
> 
> 
> [1] --
> http://coq.inria.fr/distrib/V8.4beta/stdlib/Coq.Structures.Equalities.html#

I agree that the Coq.Structures.Orders.OrderedType is a real pain to
implement due to all these inclusions. Furthermore, it is not the first
time someone asks for an example of implementation of such a module
(and especially with string).

Oh, and I just discovered, that there was the MSet (vs FSet), but no
MMap…

There is also the S. Lescuyer containers library which may be useful.

And last, I do not think that there lack some "Serializable"
module/type class in the standard library.

Something like:

Inductive data : Set :=
| Leaf : data
| Node : data → data → data.

Module Type Serialization.
  Parameter t : Type.
  Parameter serialize : t → data.
  Parameter unserialize : data → t.
  Hypothesis SerializeSection : ∀ x, unserialize (serialize x) = x.
End Serialization.

Module DataOrder.
 <code for data is an order>
End DataOrder.

Module SerializedOrder (M : Serialization).
 <code for M.t is an order>
End DataOrder.

could be very helpful.

The point is that serialization is often easy to get. And for any
serializable structure, we could have decidable equality as well.