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). |