1		% (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(chr_set_membership,[chr_subset/2, chr_not_subset/2,
6		chr_subset_strict/2, chr_not_subset_strict/2,
7		chr_member/2, chr_not_member/2]).
8
9		:- use_module(library(chr)).
10		:- chr_option(check_guard_bindings,off).
11		:- chr_option(optimize,full).
12
13		% restore operators overwritten by chr library
14		% otherwise, unary operators might not be parseable
15		:- op(200, fy, [+,-]).
16		:- op(500, yfx, \).
17
18		% assumes we use CLP(FD) to complement it
19
20		chr_subset(S1,S2) :- subset(S1,S2).
21		chr_not_subset(S1,S2) :- not_subset(S1,S2).
22
23		chr_subset_strict(S1,S2) :- subset_strict(S1,S2) .
24		chr_not_subset_strict(S1,S2) :- not_subset_strict(S1,S2).
25
26		chr_member(E,S) :- member_of(E,S).
27		chr_not_member(E,S) :- not_member_of(E,S).
28		% TODO: reification-trigger: when can we infer membership or non-membership
29
30		:- chr_constraint subset/2, not_subset/2.
31		:- chr_constraint subset_strict/2, not_subset_strict/2.
32		:- chr_constraint member_of/2, not_member_of/2.
33
34		:- public '@'/2.
35		contradiction @ subset(X,Y), not_subset(X,Y) <=> fail.
36		reflexivity @ subset(X,X) <=> true.
37		antisymmetry @ subset(X,Y), subset(Y,X) <=> X = Y.
38		idempotence @ subset(X,Y) \ subset(X,Y) <=> true.
39		transitivity @ subset(X,Y), subset(Y,Z) ==> subset(X,Z).
40		%checking @ subset(X,Y) <=> nonvar(X),nonvar(Y) | X =< Y.
41
42		contradiction @ subset_strict(X,Y), not_subset_strict(X,Y) <=> fail.
43		contradiction @ subset_strict(X,Y), not_subset(X,Y) <=> fail.
44		antireflexivity @ subset_strict(X,X) <=> fail.
45		idempotence @ subset_strict(X,Y) \ subset_strict(X,Y) <=> true.
46		transitivity @ subset_strict(X,Y), subset(Y,Z) ==> subset_strict(X,Z).
47		transitivity @ subset(X,Y), subset_strict(Y,Z) ==> subset_strict(X,Z).
48		transitivity @ subset_strict(X,Y), subset_strict(Y,Z) ==> subset_strict(X,Z).
49		%checking @ lt(X,Y) <=> nonvar(X),nonvar(Y) | X < Y.
50
51		idempotence @ member_of(X,Y) \ member_of(X,Y) <=> true.
52		idempotence @ not_member_of(X,Y) \ not_member_of(X,Y) <=> true.
53		contradiction @ member_of(X,Y), not_member_of(X,Y) <=> fail.
54		contradiction @ member_of(X,Y), not_member_of(X,Z), subset(Y,Z) <=> fail.
55		contradiction @ member_of(X,Y), not_member_of(X,Z), subset_strict(Y,Z) <=> fail.
56
57		% member_of(X,Y) => not_empty(Y)
58		% not_empty(X), empty(X) <=> fail.
59		% subset(X,Y), not_empty(X) => not_empty(Y).
60		% subset_strict(X,Y) => not_empty(Y).