[Why3-club] (no subject)

Julia Lawall julia.lawall at lip6.fr
Wed Jan 30 14:31:17 CET 2019



On Wed, 30 Jan 2019, François Bobot wrote:

> Le 30/01/2019 à 13:36, Julia Lawall a écrit :
> > I have the following orgnization of modules:
> >
> > A parameterized by f
> >
> > B uses A
> >
> > C uses A and B and is parameterized by g
> >
> > D uses A, B and C and provides a definition for f and for g
> > The definition for g relies on things defined in A and B.
> >
> > How can I set this up?  In D, I cannot just clone C, because I can't make
> > the definition of g without having A and B.  If I clone B, then define g,
> > then clone C providing the definitions of both f and g, I get a type
> > mismatch related to a type defined in B.
> >
>
> In a similar example, I was able to move the problematic type definition out of all these modules by
> making it polymorphic.
>
> Then you can more easily instantiate functions repeatedly in all the modules.
>
> Does that work in your case?

I don't think so.  There are many types involved, but the one it is
actually complaining about is a data structure containing arrays and
matrices on which there are invariants.

thanks,
julia


More information about the Why3-club mailing list