MissingJoin

From HB Require Import structures.

Module MissingJoin.

HB.mixin Record isTop M := { }.
HB.structure Definition Top := {M of isTop M}.

HB.mixin Record isA1 M of Top M := { }.
HB.structure Definition A1 := {M of isA1 M & isTop M}.

HB.mixin Record isA2 M of Top M := { }.
HB.structure Definition A2 := {M of isA2 M & isTop M}.

HB.mixin Record isB1 M of A1 M := { }.
HB.structure Definition B1 := {M of isB1 M & }.

HB.mixin Record isB2 M of A2 M := { }.
HB.structure Definition B2 :=  {M of isB2 M & isA2 M }.

HB.structure Definition B2A1 := {M of B2 M & A1 M }.

Fail HB.structure Definition A2B1 := {M of A2 M & B1 M }.

HB.graph "missing_join.dot".

End MissingJoin.

If we tred missing_join.dot | xdot - we see this (where the red node is the one we failed to add)

The solution is to declare a structure which both A2B1 and B2A1 can inherit from.

From HB Require Import structures.

Module GoodJoin.

HB.mixin Record isTop M := { }.
HB.structure Definition Top := {M of isTop M}.

HB.mixin Record isA1 M of Top M := { }.
HB.structure Definition A1 := {M of isA1 M & isTop M}.

HB.mixin Record isA2 M of Top M := { }.
HB.structure Definition A2 := {M of isA2 M & isTop M}.

HB.mixin Record isB1 M of A1 M := { }.
HB.structure Definition B1 := {M of isB1 M & }.

HB.mixin Record isB2 M of A2 M := { }.
HB.structure Definition B2 :=  {M of isB2 M & isA2 M }.

HB.structure Definition join := {M of A1 M & A2 M }.


HB.structure Definition B2A1 := {M of B2 M & A1 M }.
HB.structure Definition A2B1 := {M of A2 M & B1 M }.

HB.graph "good_join.dot".

End GoodJoin.