module types and constraints in several layers

module types and constraints in several layers

[Christian Sternagel]

Hello all together, I have a problem using type constraints. There
are several module types in my sourcecode. Lets say

file A.mli --------
module type T = sig ...  end
-------------------

file B.mli --------
module type T = sig 
 ...
 module B1
 ... 
end
-------------------

file C.mli --------
module type T = sig ... end
-------------------

file D.mli --------
module type T = sig 
 ...
 moulde D1
 module D2
 module D3
 ...
end
-------------------

and then a couple of functors. Like

file b.ml ---------
module Make (A : A.T) : B.T = struct
 ...
 module B1 = A
 ...
end
-------------------

file d.ml ---------
module Make (B : B.T) (C : C.T) : D.T = struct
 ...
 module D1 = B.B1
 module D2 = B
 module D3 = C
 ...
end
-------------------

file e.ml ---------
module Make (D : D.T) = struct
 ...
 module E1 = D.D1
 module E2 = D.D2
 module E3 = D.D3
 module E4 = D
 ...
end
-------------------

Then I build a module like

module B = B.Make (A)
module D = D.Make (B) (C)
module E = E.make (D)

and from this point on only want to use E (so I want to access the
functions of the other modules though the submodules of E).
E.g.: 
E.E1 instead of A
E.E2 instead of B
etc...

but I was not able to tell the compiler (correctly) that after
building module E ist should be the case that for example
E.E1 = D.D1 = B.B1 = A = E4.D.D1 = E4.D.D2.B1 = ...

Is there a convenient way to make such a structure of modules?
And if yes, how ist it done?

cheers

christian

Re: [Caml-list] module types and constraints in several layers

[Chris King]

On 3/15/07, Christian Sternagel <christian.sternagel@uibk.ac.at> wrote:
> but I was not able to tell the compiler (correctly) that after
> building module E ist should be the case that for example
> E.E1 = D.D1 = B.B1 = A = E4.D.D1 = E4.D.D2.B1 = ...
>
> Is there a convenient way to make such a structure of modules?
> And if yes, how ist it done?

What's happening is that, when you specify the type of the results of
B.Make and D.Make, O'Caml throws away the info about how they were
created: since the type signatures B.T and D.T simply say "these
modules have some submodules" but don't say where the submodules come
from, that info becomes hidden (as it should be).  However you can
explicitly instruct the compiler not to hide this info:

module Make (A : A.T) : B.T with module B1 = A = struct
 ...
 module B1 = A
 ...
end

This just says "give the resulting module the signature B.T, but
retain the info that module B1 equals A".  Similarly:

module Make (B : B.T) (C : C.T) : D.T
    with module D1 = B.B1 and module D2 = B
    = struct
 ...
 module D1 = B.B1
 module D2 = B
 module D3 = C
 ...
end

You don't need to do this with E.Make since its signature is left intact.

You can do this with individual types too, see section 6.10 of the manual.

Re: [Caml-list] module types and constraints in several layers

[Christian Sternagel]

On Thu, Mar 15, 2007 at 08:25:08AM -0500, Chris King wrote:
> On 3/15/07, Christian Sternagel <christian.sternagel@uibk.ac.at> wrote:
> >but I was not able to tell the compiler (correctly) that after
> >building module E ist should be the case that for example
> >E.E1 = D.D1 = B.B1 = A = E4.D.D1 = E4.D.D2.B1 = ...
> >
> >Is there a convenient way to make such a structure of modules?
> >And if yes, how ist it done?
> 
> What's happening is that, when you specify the type of the results of
> B.Make and D.Make, O'Caml throws away the info about how they were
> created: since the type signatures B.T and D.T simply say "these
> modules have some submodules" but don't say where the submodules come
> from, that info becomes hidden (as it should be).  However you can
> explicitly instruct the compiler not to hide this info:
> 
> module Make (A : A.T) : B.T with module B1 = A = struct
> ...
> module B1 = A
> ...
> end
> 
> This just says "give the resulting module the signature B.T, but
> retain the info that module B1 equals A".  Similarly:
> 
> module Make (B : B.T) (C : C.T) : D.T
>    with module D1 = B.B1 and module D2 = B
>    = struct
In fact thats exactly what I did, but it only worked when a had not more than 1 layer of functors applied to functors. I may need to give my actual program structure in more detail in order to explain my problem better.

variable.mli:
module Make (Id : IDENT.T) : VARIABLE.T with module Id = Id

function.mli:
module Make (Id : IDENT.T) (Lab : LABEL.T) : FUNCTION.T
 with module Id = Id
 and module Lab = Lab

term.mli:
module Make (Var : VARIABLE.T) (Fun : FUNCTION_SYMBOL.T) : TERM.T
 with module Var = Var
 and module Lab = Fun.Lab
 and module Fun = Fun

TERM.mli:
module type T = sig
 type t
 module Fun
 val f1 : t -> t -> bool
 val f2 : t -> t
 val f3 : Fun.t Setx.set -> t -> t
end

rule.mli:
module Make (Term : TERM.T) : RULE.T
 with module Var = Term.Var
 and module Lab = Term.Lab
 and module Fun = Term.Fun
 and module Term = Term

trs.mli:
module Make (Rule : RULE.T) : TRS.T
 with module Var = Tule.Term.Var
 and module Lab = Rule.Term.Lab
 and module Fun = Rule.Term.Fun
 and module Term = Rule.Term
 and module Rule = Rule

TRS.mli:
module type T = sig
 type t
 module Fun : FUNCTION.T
 val f0 : t -> Fun.t Setx.set 
end

everythin compiles fine. Then I make the following in another file.

some.ml:
module Make (Trs : TRS.T) : SOME.T = struct
 module Var = Trs.Var
 module Lab = Trs.Lab
 module Fun = Trs.Fun
 module Term = Trs.Term
 module Rule = Trs.Rule
 module Trs = Trs
 ...
  let ds = Trs.f0 trs in
  Term.f1 (Term.f2 (Term.f3 d s)) t
                            ^
 ...
end

end try to compile an the resulting error message is:

This expression has type Trs.Fun.t Setx.set but is here used with type
Term.Fun.t Setx.set
Type Trs.Fun.t = Trs.Fun.t is not compatible with type
Term.Fun.t = Trs.Term.Fun.t 

where the ^ markes the ment expression

cheers

christian

> ...
> module D1 = B.B1
> module D2 = B
> module D3 = C
> ...
> end
> 
> You don't need to do this with E.Make since its signature is left intact.
> 
> You can do this with individual types too, see section 6.10 of the manual.
> 
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
> 

Re: [Caml-list] module types and constraints in several layers

[Chris King]

On 3/15/07, Christian Sternagel <christian.sternagel@uibk.ac.at> wrote:
> some.ml:
> module Make (Trs : TRS.T) : SOME.T = struct

This looks to be your problem... by specifying the type of Trs as
TRS.T, you are losing the information about the relation between the
types in the modules.  You can fix this by adding this relation to the
definition of TRS.T:

module type T = sig
 type t
 module Term: TERM.T
 module Fun : FUNCTION.T with type t = Term.Fun.t
 val f0 : t -> Fun.t Setx.set
end

Otherwise O'Caml presumes Term and Fun to be completely unrelated.

Hope this helps; module type constraints can get messy :)

Re: [Caml-list] module types and constraints in several layers

[Christian Sternagel]

On Thu, Mar 15, 2007 at 09:48:44AM -0500, Chris King wrote:
> On 3/15/07, Christian Sternagel <christian.sternagel@uibk.ac.at> wrote:
> >some.ml:
> >module Make (Trs : TRS.T) : SOME.T = struct
> 
> This looks to be your problem... by specifying the type of Trs as
> TRS.T, you are losing the information about the relation between the
> types in the modules.  You can fix this by adding this relation to the
> definition of TRS.T:
> 
> module type T = sig
> type t
> module Term: TERM.T
> module Fun : FUNCTION.T with type t = Term.Fun.t
> val f0 : t -> Fun.t Setx.set
> end
> 
> Otherwise O'Caml presumes Term and Fun to be completely unrelated.
> 
> Hope this helps; module type constraints can get messy :)
Thanks this helped a lot... no the only open problem is how
to constrain variant types.

i have 
module type TERM
 module Var : VAR
 module Fun : FUN
 module Lab : LAB
  with type t = Fun.Lab.t

 type t = Var of Var.t | Fun of Fun.t * t list
end

and in the module type  TRS I need to do something like

module type TRS
 module Rule : RULE
 module Term : TERM
  with module Var = Rule.Var
  and module Fun = Rule.Fun
  and module Lab = Rule.Lab
  and type t = Rule.Term.t
               ^^^^^^^^^^^

which yields a syntax error... is there a way to give such a 
constraint for variant types?

cheers

christian
> 
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>