diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-02-09 18:18:03 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-02-09 18:22:08 +0100 |
commit | 1f8a0c703b7c221e09333cca3208a084e0109269 (patch) | |
tree | fc9c8bf942b4a4fc6d08e667f2a602f9cecbad99 /subprojects/store/src | |
parent | refactor: Atom -> Literal naming convention (diff) | |
download | refinery-1f8a0c703b7c221e09333cca3208a084e0109269.tar.gz refinery-1f8a0c703b7c221e09333cca3208a084e0109269.tar.zst refinery-1f8a0c703b7c221e09333cca3208a084e0109269.zip |
refactor: EDSL for DNF literals
Diffstat (limited to 'subprojects/store/src')
9 files changed, 91 insertions, 45 deletions
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java index f7b27b81..1eb9ac76 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/Dnf.java | |||
@@ -1,5 +1,7 @@ | |||
1 | package tools.refinery.store.query; | 1 | package tools.refinery.store.query; |
2 | 2 | ||
3 | import tools.refinery.store.query.literal.CallPolarity; | ||
4 | import tools.refinery.store.query.literal.DnfCallLiteral; | ||
3 | import tools.refinery.store.query.literal.Literal; | 5 | import tools.refinery.store.query.literal.Literal; |
4 | 6 | ||
5 | import java.util.*; | 7 | import java.util.*; |
@@ -72,6 +74,22 @@ public final class Dnf implements RelationLike { | |||
72 | return clauses; | 74 | return clauses; |
73 | } | 75 | } |
74 | 76 | ||
77 | public DnfCallLiteral call(CallPolarity polarity, List<Variable> substitution) { | ||
78 | return new DnfCallLiteral(polarity, this, substitution); | ||
79 | } | ||
80 | |||
81 | public DnfCallLiteral call(CallPolarity polarity, Variable... substitution) { | ||
82 | return call(polarity, List.of(substitution)); | ||
83 | } | ||
84 | |||
85 | public DnfCallLiteral call(Variable... substitution) { | ||
86 | return call(CallPolarity.POSITIVE, substitution); | ||
87 | } | ||
88 | |||
89 | public DnfCallLiteral callTransitive(Variable left, Variable right) { | ||
90 | return call(CallPolarity.TRANSITIVE, List.of(left, right)); | ||
91 | } | ||
92 | |||
75 | public static Builder builder() { | 93 | public static Builder builder() { |
76 | return builder(null); | 94 | return builder(null); |
77 | } | 95 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java index 6a6831ae..2eb87649 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/Variable.java | |||
@@ -1,5 +1,8 @@ | |||
1 | package tools.refinery.store.query; | 1 | package tools.refinery.store.query; |
2 | 2 | ||
3 | import tools.refinery.store.query.literal.ConstantLiteral; | ||
4 | import tools.refinery.store.query.literal.EquivalenceLiteral; | ||
5 | |||
3 | import java.util.Objects; | 6 | import java.util.Objects; |
4 | 7 | ||
5 | public class Variable { | 8 | public class Variable { |
@@ -28,6 +31,18 @@ public class Variable { | |||
28 | return name != null; | 31 | return name != null; |
29 | } | 32 | } |
30 | 33 | ||
34 | public ConstantLiteral isConstant(int value) { | ||
35 | return new ConstantLiteral(this, value); | ||
36 | } | ||
37 | |||
38 | public EquivalenceLiteral isEquivalent(Variable other) { | ||
39 | return new EquivalenceLiteral(true, this, other); | ||
40 | } | ||
41 | |||
42 | public EquivalenceLiteral notEquivalent(Variable other) { | ||
43 | return new EquivalenceLiteral(false, this, other); | ||
44 | } | ||
45 | |||
31 | @Override | 46 | @Override |
32 | public boolean equals(Object o) { | 47 | public boolean equals(Object o) { |
33 | if (this == o) return true; | 48 | if (this == o) return true; |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java index ddea0221..84b4b771 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/CallPolarity.java | |||
@@ -22,7 +22,11 @@ public enum CallPolarity { | |||
22 | return transitive; | 22 | return transitive; |
23 | } | 23 | } |
24 | 24 | ||
25 | public static CallPolarity fromBoolean(boolean positive) { | 25 | public CallPolarity negate() { |
26 | return positive ? POSITIVE : NEGATIVE; | 26 | return switch (this) { |
27 | case POSITIVE -> NEGATIVE; | ||
28 | case NEGATIVE -> POSITIVE; | ||
29 | case TRANSITIVE -> throw new IllegalArgumentException("Transitive polarity cannot be negated"); | ||
30 | }; | ||
27 | } | 31 | } |
28 | } | 32 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java index e3410c21..86149b33 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java | |||
@@ -5,28 +5,13 @@ import tools.refinery.store.query.Variable; | |||
5 | 5 | ||
6 | import java.util.List; | 6 | import java.util.List; |
7 | 7 | ||
8 | public final class DnfCallLiteral extends CallLiteral<Dnf> { | 8 | public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiteral<DnfCallLiteral> { |
9 | public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> substitution) { | 9 | public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> substitution) { |
10 | super(polarity, target, substitution); | 10 | super(polarity, target, substitution); |
11 | } | 11 | } |
12 | 12 | ||
13 | public DnfCallLiteral(CallPolarity polarity, Dnf target, Variable... substitution) { | 13 | @Override |
14 | this(polarity, target, List.of(substitution)); | 14 | public DnfCallLiteral negate() { |
15 | } | 15 | return new DnfCallLiteral(getPolarity().negate(), getTarget(), getSubstitution()); |
16 | |||
17 | public DnfCallLiteral(boolean positive, Dnf target, List<Variable> substitution) { | ||
18 | this(CallPolarity.fromBoolean(positive), target, substitution); | ||
19 | } | ||
20 | |||
21 | public DnfCallLiteral(boolean positive, Dnf target, Variable... substitution) { | ||
22 | this(positive, target, List.of(substitution)); | ||
23 | } | ||
24 | |||
25 | public DnfCallLiteral(Dnf target, List<Variable> substitution) { | ||
26 | this(CallPolarity.POSITIVE, target, substitution); | ||
27 | } | ||
28 | |||
29 | public DnfCallLiteral(Dnf target, Variable... substitution) { | ||
30 | this(target, List.of(substitution)); | ||
31 | } | 16 | } |
32 | } | 17 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java index a1ec2c41..75afd50b 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java | |||
@@ -4,14 +4,16 @@ import tools.refinery.store.query.Variable; | |||
4 | 4 | ||
5 | import java.util.Set; | 5 | import java.util.Set; |
6 | 6 | ||
7 | public record EquivalenceLiteral(boolean positive, Variable left, Variable right) implements Literal { | 7 | public record EquivalenceLiteral(boolean positive, Variable left, Variable right) |
8 | public EquivalenceLiteral(Variable left, Variable right) { | 8 | implements PolarLiteral<EquivalenceLiteral> { |
9 | this(true, left, right); | ||
10 | } | ||
11 | |||
12 | @Override | 9 | @Override |
13 | public void collectAllVariables(Set<Variable> variables) { | 10 | public void collectAllVariables(Set<Variable> variables) { |
14 | variables.add(left); | 11 | variables.add(left); |
15 | variables.add(right); | 12 | variables.add(right); |
16 | } | 13 | } |
14 | |||
15 | @Override | ||
16 | public EquivalenceLiteral negate() { | ||
17 | return new EquivalenceLiteral(!positive, left, right); | ||
18 | } | ||
17 | } | 19 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java new file mode 100644 index 00000000..2c7e893f --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/Literals.java | |||
@@ -0,0 +1,11 @@ | |||
1 | package tools.refinery.store.query.literal; | ||
2 | |||
3 | public final class Literals { | ||
4 | private Literals() { | ||
5 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | ||
6 | } | ||
7 | |||
8 | public static <T extends PolarLiteral<T>> T not(PolarLiteral<T> literal) { | ||
9 | return literal.negate(); | ||
10 | } | ||
11 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java new file mode 100644 index 00000000..32523675 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java | |||
@@ -0,0 +1,5 @@ | |||
1 | package tools.refinery.store.query.literal; | ||
2 | |||
3 | public interface PolarLiteral<T extends PolarLiteral<T>> extends Literal { | ||
4 | T negate(); | ||
5 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java index e2106ba9..7fa99abb 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java | |||
@@ -5,28 +5,14 @@ import tools.refinery.store.query.view.AnyRelationView; | |||
5 | 5 | ||
6 | import java.util.List; | 6 | import java.util.List; |
7 | 7 | ||
8 | public final class RelationViewLiteral extends CallLiteral<AnyRelationView> { | 8 | public final class RelationViewLiteral extends CallLiteral<AnyRelationView> |
9 | implements PolarLiteral<RelationViewLiteral> { | ||
9 | public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List<Variable> substitution) { | 10 | public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List<Variable> substitution) { |
10 | super(polarity, target, substitution); | 11 | super(polarity, target, substitution); |
11 | } | 12 | } |
12 | 13 | ||
13 | public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, Variable... substitution) { | 14 | @Override |
14 | this(polarity, target, List.of(substitution)); | 15 | public RelationViewLiteral negate() { |
15 | } | 16 | return new RelationViewLiteral(getPolarity().negate(), getTarget(), getSubstitution()); |
16 | |||
17 | public RelationViewLiteral(boolean positive, AnyRelationView target, List<Variable> substitution) { | ||
18 | this(CallPolarity.fromBoolean(positive), target, substitution); | ||
19 | } | ||
20 | |||
21 | public RelationViewLiteral(boolean positive, AnyRelationView target, Variable... substitution) { | ||
22 | this(positive, target, List.of(substitution)); | ||
23 | } | ||
24 | |||
25 | public RelationViewLiteral(AnyRelationView target, List<Variable> substitution) { | ||
26 | this(CallPolarity.POSITIVE, target, substitution); | ||
27 | } | ||
28 | |||
29 | public RelationViewLiteral(AnyRelationView target, Variable... substitution) { | ||
30 | this(target, List.of(substitution)); | ||
31 | } | 17 | } |
32 | } | 18 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java index bbec1e73..0bea962d 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java +++ b/subprojects/store/src/main/java/tools/refinery/store/query/view/RelationView.java | |||
@@ -2,9 +2,13 @@ package tools.refinery.store.query.view; | |||
2 | 2 | ||
3 | import tools.refinery.store.map.CursorAsIterator; | 3 | import tools.refinery.store.map.CursorAsIterator; |
4 | import tools.refinery.store.model.Model; | 4 | import tools.refinery.store.model.Model; |
5 | import tools.refinery.store.query.Variable; | ||
6 | import tools.refinery.store.query.literal.CallPolarity; | ||
7 | import tools.refinery.store.query.literal.RelationViewLiteral; | ||
5 | import tools.refinery.store.representation.Symbol; | 8 | import tools.refinery.store.representation.Symbol; |
6 | import tools.refinery.store.tuple.Tuple; | 9 | import tools.refinery.store.tuple.Tuple; |
7 | 10 | ||
11 | import java.util.List; | ||
8 | import java.util.Objects; | 12 | import java.util.Objects; |
9 | import java.util.UUID; | 13 | import java.util.UUID; |
10 | 14 | ||
@@ -47,6 +51,22 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView { | |||
47 | return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter)); | 51 | return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter)); |
48 | } | 52 | } |
49 | 53 | ||
54 | public RelationViewLiteral call(CallPolarity polarity, List<Variable> substitution) { | ||
55 | return new RelationViewLiteral(polarity, this, substitution); | ||
56 | } | ||
57 | |||
58 | public RelationViewLiteral call(CallPolarity polarity, Variable... substitution) { | ||
59 | return call(polarity, List.of(substitution)); | ||
60 | } | ||
61 | |||
62 | public RelationViewLiteral call(Variable... substitution) { | ||
63 | return call(CallPolarity.POSITIVE, substitution); | ||
64 | } | ||
65 | |||
66 | public RelationViewLiteral callTransitive(Variable left, Variable right) { | ||
67 | return call(CallPolarity.TRANSITIVE, List.of(left, right)); | ||
68 | } | ||
69 | |||
50 | @Override | 70 | @Override |
51 | public boolean equals(Object o) { | 71 | public boolean equals(Object o) { |
52 | if (this == o) return true; | 72 | if (this == o) return true; |