[Why3-club] (no subject)
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.
More information about the Why3-club