coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Hints, Modules signatures and computation

From: Elie Soubiran <soubiran AT lix.polytechnique.fr>
To: Thomas Braibant <thomas.braibant AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Hints, Modules signatures and computation
Date: Fri, 17 Apr 2009 13:55:55 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; b=XVGuyG7lkZoSXG6rkRS1fCtKdWCcJh2gQrqxGeL1SBaFMSyzP+v7FoTeaAPnt83j5s q1pqykDpWYag72VXSO2d1M7INPgWfGFN4tuV0wuaoz6yM/+Si2svh7IOt83ccn+abPFA p/0xjfVpN6qJjQFCQ9rIp3OLdq04UYT/T+hv8=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello Thomas,

There is a little trick to perform transparent sealing in Coq:

Require Import FSets.

Module NatSet := FSetList.Make(Nat_as_OT).

Module F ( X : FSetInterface.S).
� Include X.
End F.

Module NatSet2 := F NatSet.

The only drawback of this is that it is buggy (one more time it is my fault) in the first release of 8.2, but it works in the current svn version of 8.2.

Elie

On Fri, Apr 17, 2009 at 10:38 AM, Thomas Braibant <thomas.braibant AT gmail.com> wrote:

Hi Coq-clubbers,

When going through the standard library, I often find Hints declared
in Module signatures, like FSetInterface.S ... So, in order to get
these Hints, it seems that I must enforce the output module type of
FSetAVL.Make to meet this interface. But, the latter solution prevents
the unfolding of all symbols (like, e.g. all the computation
functions), and it seems a little bit tedious to export everything
useful.

Is there another solution to get the Hints, and keep everything transparent ?

Here is a code sample that summarizes what I have tried ...
<<
Require Import FSets.

Module NatSet := FSetList.Make(Nat_as_OT).
Check (O : NatSet.elt).
(* Print HintDb set. No such Hint database *)

Module NatSetChecked <: FSetInterface.S := FSetList.Make(Nat_as_OT).
Check (O : NatSetChecked.elt).
(* Print HintDb set. No such Hint database *)

Module NatSetCoerced : FSetInterface.S := FSetList.Make(Nat_as_OT).
(* Check (O : NatSetCoerced.elt). � NatSetCoerced.elt is opaque *)
�Print HintDb set. (* Here I get all the hints I want *)

Module NatSetCoerced2 : FSetInterface.S with Module E := Nat_as_OT :=
FSetList.Make(Nat_as_OT).
Check (O : NatSetCoerced2.elt). �(* OK *)
Print HintDb set. (* Here I get all the hints I want *)
Eval vm_compute in (NatSetCoerced2.exists_ (fun u => if le_lt_dec 0 u
then true else false) NatSetCoerced2.empty). (* NatSetCoerced2.empty
is opaque *)

>>

--
thomas

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
� � � � �http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Coq-Club] Hints, Modules signatures and computation, Thomas Braibant
- Re: [Coq-Club] Hints, Modules signatures and computation, Elie Soubiran