The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Hello Beta

Well, I've been trying to write a library and this was part of my attempt at learning how to write interfaces/module types.

I've figured it out now though. It has to do with the incremental style (of the std lib) of building interfaces. The Import statement is there because we want the 'k's  arbitrary as possible (specifically, we don't know they're ordered) and then later on build another interface where they are.

I've include a worked example.

Warm regards
Chris

On 5 June 2014 00:22, Beta Ziliani <beta AT mpi-sws.org> wrote:

On Wed, Jun 4, 2014 at 5:04 AM, Christopher Ernest Sally
<christopherernestsally AT gmail.com> wrote:
> Hi all
>
> I'm trying to learn how to write modules/module types.
>
> I tried out the example at cocorico and am now try to do a
> interface-implementation thing, but am getting the error incompatible module
> type when I try to close the implementation module (called "Implementation"
> in file B.v)
>
> I include the files here. Could any point out what I'm doing wrong? Thanks!

What is exactly what you want to do?  At first sight I (and I guess
Coq) cannot make the connection between the type ht and the product
type.  If you move ht into A and provide ht as  [list (X.t * Y.t)], it
should work.

Best,
Beta

>
> Warm regards
> Chris
>
> (* file A.v *)
> Module Type TKV.
> Parameter ht k v : Type.
> End TKV.
>
>
> Require Import Orders Equalities.
>
> Module Type Interface (K : OrderedType)(V : DecidableType)
> (Import T : TKV).
>
> Parameter empty : ht.
>
> End Interface.
> (* A.v *)
>
>
> (* B.v *)
> Require A. (* of course I have already compiled A *)
> Include A.
> Require Import List Bool Orders Equalities.
>
> Module Implementation (X : OrderedType)(Y : DecidableType)
>
> <: A.Interface X Y.
>
> Definition empty := @nil (prod X.t Y.t) .
>
> End Implementation.
> (* B.v *)

Require Import Utf8 Orders Equalities.

Module Type TKV.
  Parameter k v m : Type.
End TKV.

Module Type Interface' (Import T: TKV).
(* These give an interface where we know nothing about the keys or vals.
   Which is why we had to import the *)
  Parameter empty : m.
End Interface'.

Module Type Interface (K : OrderedType)(V : DecidableType).
(* Here however, we now know that keys must be ordered and vals decidable. *)
  Definition k := K.t.
  Definition v := V.t.
  Parameter  m :  Type.

  Include Interface'.

  Parameter add : k → v → m → m.

End Interface.

Require Import List Bool Orders Equalities.

Module Implementation (X : OrderedType)(Y : DecidableType) <: Interface X Y.

  Definition kvp := prod X.t Y.t.
  Definition k := X.t.
  Definition v := Y.t.  
  Definition m := list kvp.

  Definition empty : m := nil.

  Definition add (x:k) (y:v) lst := cons (x,y) lst.

End Implementation.

Print Module Type Interface.
Print Module Type Implementation.