SWISH -- SWI-Prolog for SHaring

/* `is_struct(S)` is true if `S` is the name of a struct
 * (as opposed to a union). */
is_struct(some_struct).

/* `type_of(F, S)` maps from a field name to the type
 * in which it is defined. */
type_of(f0, some_struct).
type_of(f1, some_struct).
type_of(u0, some_union).
type_of(u1, some_union).

/* Two distinct variables are disjoint */
disjoint(var(V0), var(V1)) :- V0 \= V1.

/* Two paths `p.f` and `p.g` are disjoint
 * if the fields `f` and `g` are disjoint. */
disjoint(field(P, F0), field(P, F1)) :- disjoint_fields(F0, F1).

/* Two paths `p.f` and `q` are disjoint
 * if `p` is disjoint from `q`. */
disjoint(field(P0, _), P1) :- disjoint(P0, P1).
disjoint(P0, field(P1, _)) :- disjoint(P0, P1).

/* Two distinct fields in the same struct are disjoint. */
disjoint_fields(F0, F1) :-
    type_of(F0, S),
    type_of(F1, S),
    is_struct(S),
    F0 \= F1.

/* Fields declared in two distinct types are disjoint. */
disjoint_fields(F0, F1) :-
    type_of(F0, S0),
    type_of(F1, S1),
    S0 \= S1.

/** <examples>
?- disjoint(field(var(a), f0), field(var(b), f0)).
?- disjoint(field(var(a), f0), var(b)).
?- disjoint(field(var(a), f0), field(var(a), f1)).
?- disjoint(field(var(a), u0), field(var(a), u1)).
?- disjoint(field(field(var(a), u0), f0), field(field(var(a), u1), f1)).
*/