diff --git a/src/Main.java b/src/Main.java index 19d505d..3c10aa9 100644 --- a/src/Main.java +++ b/src/Main.java @@ -3,6 +3,8 @@ import inference.ProofSystem; import inference.equivalence.SemanticEquivalenceProofSystem; import inference.equivalence.SemanticEquivalenceRelation; +import inference.rewrite.Position; +import inference.rewrite.ResourceTree; import inference.rewrite.RewriteInferenceSystem; import lombok.SneakyThrows; import models.algebra.Expression; @@ -35,7 +37,8 @@ // sandbox3(); // sandbox4(); // ProofSystem.debug(); - sandbox6(); +// sandbox6(); + sandbox7(); } static void sandbox1() { @@ -181,6 +184,35 @@ } + static void sandbox7() { + Resource A = new Resource("A", INT, 1); + Resource B = new Resource("B", INT, 1); + Resource C = new Resource("C", INT, 1); + Resource D = new Resource("D", INT, 1); + Resource E = new Resource("E", INT, 1); + Resource F = new Resource("F", INT, 1); + Resource G = new Resource("G", INT, 1); + Resource H = new Resource("H", INT, 1); + Resource I = new Resource("I", INT, 1); + Resource J = new Resource("J", INT, 1); + Resource K = new Resource("K", INT, 1); + Resource L = new Resource("L", INT, 1); + Resource M = new Resource("M", INT, 1); + Resource N = new Resource("N", INT, 1); + Resource O = new Resource("O", INT, 1); + + DependencyTerm t1 = new DependencyTerm(A, B, C); + DependencyTerm t2 = new DependencyTerm(I, J, K); + DependencyTerm t3 = new DependencyTerm(M, N, O); + DependencyTerm t4 = new DependencyTerm(E, F, G, H, t2); + DependencyTerm t5 = new DependencyTerm(t1, D, t4, L, t3); + + ResourceTree rt = new ResourceTree(t5); + System.out.println(rt); + rt.debug(new Position(List.of(0))); + } + + @SneakyThrows static Expression parse(String expr) { stream.addLine(expr); diff --git a/src/inference/rewrite/Position.java b/src/inference/rewrite/Position.java new file mode 100644 index 0000000..6fb1315 --- /dev/null +++ b/src/inference/rewrite/Position.java @@ -0,0 +1,43 @@ +package inference.rewrite; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +import lombok.Getter; + +public class Position { + + @Getter + private List paths; + + public Position(List paths) { + this.paths = Collections.unmodifiableList(paths); + } + + public Position addPath(int index) { + List nextPaths = new ArrayList<>(paths); + nextPaths.add(index); + return new Position(Collections.unmodifiableList(nextPaths)); + } + + @Override + public boolean equals(Object another) { + if (! (another instanceof Position)) { + return false; + } + Position position = (Position) another; + return paths.equals(position.getPaths()); + } + + @Override + public int hashCode() { + return this.paths.hashCode(); + } + + @Override + public String toString() { + return paths.toString(); + } + +} diff --git a/src/inference/rewrite/ResourceTree.java b/src/inference/rewrite/ResourceTree.java new file mode 100644 index 0000000..8ecdd14 --- /dev/null +++ b/src/inference/rewrite/ResourceTree.java @@ -0,0 +1,65 @@ +package inference.rewrite; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +import models.terms.DependencyTerm; +import models.terms.EvaluatableTerm; +import models.terms.Resource; + +public class ResourceTree { + + private Resource root; + private Map> tree; + private Map resourceMap; + + public ResourceTree(EvaluatableTerm term) { + tree = new HashMap<>(); + resourceMap = new HashMap<>(); + constructResourceTree(term, new Position(List.of(0))); + } + + private Position constructResourceTree(EvaluatableTerm term, Position top) { + if (term instanceof Resource resource) { + resourceMap.put(top, resource); + return top; + } else if (term instanceof DependencyTerm depTerm) { + EvaluatableTerm dependingTerm = depTerm.getDependingTerm(); + List dependedResources = depTerm.getDependedResources(); + List argumentTerms = depTerm.getArgumentTerms(); + Position nextPosition = constructResourceTree(dependingTerm, top); + Position resultPosition = nextPosition; + tree.put(nextPosition, new ArrayList<>()); + for (int i = 0; i < dependedResources.size(); i++) { + Position nextPos = nextPosition.addPath(i); + tree.get(nextPosition).add(nextPos); + resultPosition = constructResourceTree(dependedResources.get(i), nextPos); + Position nextNextPos = resultPosition.addPath(0); + tree.put(resultPosition, new ArrayList<>()); + tree.get(resultPosition).add(nextNextPos); + resultPosition = constructResourceTree(argumentTerms.get(i), nextNextPos); + } + return resultPosition; + } else { + return null; + } + } + + @Override + public String toString() { + return tree.toString(); + } + + public void debug(Position pos) { + System.out.println(pos + ", " + resourceMap.get(pos)); + if (tree.containsKey(pos)) { + for (Position nextPos : tree.get(pos)) { + debug(nextPos); + } + } + } + +} + diff --git a/src/inference/rewrite/RewriteInferenceSystem.java b/src/inference/rewrite/RewriteInferenceSystem.java index 303ea2e..15ef228 100644 --- a/src/inference/rewrite/RewriteInferenceSystem.java +++ b/src/inference/rewrite/RewriteInferenceSystem.java @@ -1,7 +1,8 @@ package inference.rewrite; +import java.util.ArrayDeque; import java.util.ArrayList; -import java.util.HashMap; +import java.util.Deque; import java.util.List; import java.util.Map; @@ -22,6 +23,7 @@ List otherFormulas = new ArrayList<>(); Formula conclusion; + public RewriteInferenceSystem(List assumptions, Formula conclusion) { for (Formula assumption : assumptions) { if (inputFormulaCheck(assumption)) { @@ -53,9 +55,25 @@ } public boolean inference() { - Map> resourceTree = new HashMap<>(); - Resource root = parseDependencyTerm(inputFormula.getLeftSideHand(), resourceTree, new ArrayList<>()); - System.out.println(resourceTree); +// Map> inputFormulaTree = new HashMap<>(); +// Resource root = parseDependencyTerm(inputFormula.getLeftSideHand(), inputFormulaTree, new ArrayList<>()); +// ResourceTree inputResourceTree = new ResourceTree(root, inputFormulaTree); +// List otherRoots = new ArrayList<>(); +// for (Formula formula : constraintFormulas) { +// if (formula instanceof EquationFormula equation) { +// Map> resourceTree = new HashMap<>(); +// Resource treeRoot = parseDependencyTerm(equation.getRightSideHand(), resourceTree, new ArrayList<>()); +// otherRoots.add(new ResourceTree(treeRoot, resourceTree)); +// } +// } +// for (Formula formula : conditionalFormulas) { +// if (formula instanceof EquationFormula equation) { +// Map> resourceTree = new HashMap<>(); +// Resource treeRoot = parseDependencyTerm(equation.getLeftSideHand(), resourceTree, new ArrayList<>()); +// otherRoots.add(new ResourceTree(treeRoot, resourceTree)); +// } +// } +// System.out.println(inputResourceTree); return false; } @@ -92,6 +110,45 @@ return root; } +// private Map> joinTree(Map> baseTree, Map> joinTree) { +// +// } +// + private ResourceTree joinTreeLeft(ResourceTree baseTree, ResourceTree joinTree) { + +// ResourceTree result = new ResourceTree(baseTree.root(), new HashMap<>(baseTree.tree())); +// +// Deque curRootQue = new ArrayDeque<>(); +// curRootQue.add(joinTree.root()); +// +// while (! curRootQue.isEmpty()) { +// Resource curRoot = curRootQue.pollFirst(); +// if (isTreeMatch(result.tree(), curRoot, joinTree.tree())) { +// +// } +// curRootQue.addAll(joinTree.tree.get(curRoot)); +// } + +// return result; + return null; + } + + private boolean isTreeMatch(Map> baseTree, Resource joinRoot, Map> joinTree) { + Deque joinCurResourceStack = new ArrayDeque<>(); + joinCurResourceStack.add(joinRoot); + while (! joinCurResourceStack.isEmpty()) { + Resource joinCurResource = joinCurResourceStack.pollLast(); + if (! baseTree.keySet().contains(joinCurResource)) { + return false; + } + if (! baseTree.get(joinCurResource).equals(joinTree.get(joinCurResource))) { + return false; + } + joinCurResourceStack.addAll(joinTree.get(joinCurResource)); + } + + return true; + } private boolean inputFormulaCheck(Formula formula) { if (! (formula instanceof EquationFormula equation)) {