diff --git a/src/main/java/Main.java b/src/main/java/Main.java index a9b6dbc..89cd088 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,22 +1,14 @@ import java.util.List; -import inference.ProofSystem; import inference.rewrite.Position; import inference.rewrite.ResourceTree; -import inference.rewrite.RewriteInferenceSystem; import lombok.SneakyThrows; import models.algebra.Expression; import models.algebra.Type; import models.dataConstraintModel.DataConstraintModel; import models.dataFlowModel.DataTransferModel; -import models.formulas.DependencyFormula; -import models.formulas.EquationFormula; -import models.formulas.InFormula; -import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.Resource; -import models.terms.ResourceConstant; -import models.terms.SetEvaluatableTerm; import parser.Parser; import parser.Parser.TokenStream; @@ -29,154 +21,53 @@ static Type INT = DataConstraintModel.typeInt; public static void main(String[] args) { -// sandbox1(); -// sandbox2(); -// sandbox3(); -// sandbox4(); -// ProofSystem.debug(); -// sandbox6(); - sandbox7(); + sandbox2(); } -// static void sandbox1() { -// Resource A = new Resource("A", INT, 2); -// Resource Ap = new Resource("A'", INT, 2); -// Resource B = new Resource("B", INT, 2); -// Resource Bp = new Resource("B'", Utils.INT, 2); -// Resource C = new Resource("C", Utils.INT, 2); -// Resource Cp = new Resource("C'", Utils.INT, 2); -// Resource D = new Resource("D", Utils.INT, 2); -// Resource E = new Resource("E", Utils.INT, 1); -// Resource F = new Resource("F", Utils.INT, 1); -// Resource G = new Resource("G", Utils.INT, 0); -// DependencyTerm t1 = new DependencyTerm(A, B, C); -// DependencyTerm t2 = new DependencyTerm(Ap, Bp, Cp); -// EquationFormula assumptionFormula = new EquationFormula(t1, t2); -// EquationFormula conclusionFormula = new EquationFormula( -// new DependencyTerm(new DependencyTerm(new DependencyTerm(A, B, C), D, E), F, G), -// new DependencyTerm(new DependencyTerm(new DependencyTerm(Ap, Bp, Cp), D, E), F, G) -// ); -// -// SemanticEquivalenceProofSystem proofSystem = new SemanticEquivalenceProofSystem( -// List.of(new SemanticEquivalenceRelation(assumptionFormula, 2)), -// conclusionFormula -// ); -// SemanticEquivalenceProofSystem.debug(); -// System.out.println(); -// System.out.println(assumptionFormula); -// System.out.println(conclusionFormula); -//// System.out.println(conclusionFormula.linearRightNormalized()); -// System.out.println(proofSystem.proof()); -// } + static void sandbox1() { + 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); + DependencyTerm t1 = new DependencyTerm(A, B, C, D, E); + DependencyTerm t2 = new DependencyTerm(t1, F, G); + System.out.println(t2); + ResourceTree rt = new ResourceTree(t2); + System.out.println(rt); + rt.debug(new Position(List.of(0))); + } static void sandbox2() { - ProofSystem.debug(); - } - - static void sandbox3() { - Resource followee = new Resource("followee", INT, 2); - Resource fno = new Resource("fno", INT, 2); - ResourceConstant one = new ResourceConstant("1"); - ResourceConstant A = new ResourceConstant("A"); - ResourceConstant C = new ResourceConstant("C"); - Resource aid = new Resource("aid", INT, 1); - DependencyTerm t1 = new DependencyTerm(followee, fno, one); - Dependency d1 = new Dependency(t1, aid); - DependencyTerm t2 = new DependencyTerm(one, aid, A); - DependencyTerm t3 = new DependencyTerm(new SetEvaluatableTerm(fno), aid, A); - DependencyTerm t4 = new DependencyTerm(t1, aid, A); + 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); + Resource P = new Resource("P", INT, 1); + Resource Q = new Resource("Q", INT, 1); - DependencyFormula f1 = new DependencyFormula(d1); - InFormula f2 = new InFormula(t2, t3); - EquationFormula f3 = new EquationFormula(t4, C); - DependencyFormula f4 = new DependencyFormula(new Dependency(new SetEvaluatableTerm(followee), aid)); - InFormula f5 = new InFormula(A, new SetEvaluatableTerm(aid)); - InFormula conclusion = new InFormula(C, new SetEvaluatableTerm(new SetEvaluatableTerm(followee))); - - System.out.println(f1); - System.out.println(f2); - System.out.println(f3); - System.out.println(conclusion); - System.out.println(); - boolean result = ProofSystem.check(List.of(f1, f2, f3, f4, f5), conclusion); - System.out.println(); - System.out.println(result); - } - - static void sandbox4() { - Resource X = new Resource("X", INT, 1); - Resource Y= new Resource("Y", INT, 1); - Resource U = new Resource("U", INT, 1); - Resource W = new Resource("W", INT, 1); - - EquationFormula f1 = new EquationFormula(X, Y); - DependencyFormula f2 = new DependencyFormula(X, U); - DependencyFormula f3 = new DependencyFormula(U, W); - DependencyTerm t1 = new DependencyTerm(X, U, U); - DependencyTerm t2 = new DependencyTerm(t1, W, W); - DependencyTerm t3 = new DependencyTerm(Y, U, U); - DependencyTerm t4 = new DependencyTerm(t3, W, W); -// EquationFormula f4 = new EquationFormula(t1, X); -// EquationFormula f4 = new EquationFormula(X, t1); -// EquationFormula f4 = new EquationFormula(t2, X); -// EquationFormula f4 = new EquationFormula(t3, Y); -// EquationFormula f4 = new EquationFormula(t4, Y); - EquationFormula f4 = new EquationFormula(t2, t4); -// DependencyFormula f4 = new DependencyFormula(Y, U); - System.out.println(f1 + ", " + f2 + ", " + f3); - boolean result = ProofSystem.check(List.of(f1, f2, f3), f4); - System.out.println(result); - } - - static void sandbox5() { - 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 x = new Resource("x", INT, 0); - Resource y = new Resource("y", INT, 0); - DependencyTerm t1 = new DependencyTerm(a, b, c, d, e); - DependencyTerm t2 = new DependencyTerm(t1, f, x); - EquationFormula fm = new EquationFormula(t2, y); - System.out.println(t1); - System.out.println(t2); - System.out.println(fm); - RewriteInferenceSystem tmp = new RewriteInferenceSystem(List.of(fm), null); - tmp.debug(); - tmp.inference(); - } - - static void sandbox6() { - Resource uid = new Resource("uid", INT, 1); - Resource org = new Resource("org", INT, 1); - Resource uadd = new Resource("uadd", INT, 1); - Resource cid = new Resource("cid", INT, 1); - Resource add = new Resource("add", INT, 1); - Resource addP = new Resource("add'", INT, 1); - Resource cidP = new Resource("cid'", INT, 1); - Resource orgP = new Resource("org'", INT, 1); - Resource uidP = new Resource("uid'", INT, 1); - Resource uaddP = new Resource("uadd'", INT, 1); - Resource x = new Resource("x", INT, 0); - Resource y = new Resource("y", INT, 0); - Resource z = new Resource("z", INT, 0); - - DependencyTerm t1 = new DependencyTerm(add, cid, org); - DependencyTerm t2 = new DependencyTerm(addP, cidP, orgP); - DependencyTerm t3 = new DependencyTerm(orgP, uidP, x); - DependencyTerm t4 = new DependencyTerm(add, cid, y); - DependencyTerm t5 = new DependencyTerm(uaddP, uidP, x); - - EquationFormula f1 = new EquationFormula(uadd, t1); - EquationFormula f2 = new EquationFormula(uaddP, t2); - EquationFormula f3 = new EquationFormula(t3, y); - EquationFormula f4 = new EquationFormula(t4, t5); - - RewriteInferenceSystem tmp = new RewriteInferenceSystem(List.of(f1, f2, f3), f4); - tmp.debug(); - tmp.inference(); + DependencyTerm t1 = new DependencyTerm(A, B, C, D, E); + DependencyTerm t2 = new DependencyTerm(G, H, I, J, K); + DependencyTerm t3 = new DependencyTerm(M, N, O, P, Q); + DependencyTerm t4 = new DependencyTerm(t1, F, t2, L, t3); + System.out.println(t4); + ResourceTree rt = new ResourceTree(t4); + System.out.println(rt); + rt.debug(new Position()); + rt.debugAllPath(); } diff --git a/src/main/java/inference/rewrite/Position.java b/src/main/java/inference/rewrite/Position.java index 6fb1315..f8dc549 100644 --- a/src/main/java/inference/rewrite/Position.java +++ b/src/main/java/inference/rewrite/Position.java @@ -15,6 +15,10 @@ this.paths = Collections.unmodifiableList(paths); } + public Position() { + this.paths = Collections.unmodifiableList(List.of(0)); + } + public Position addPath(int index) { List nextPaths = new ArrayList<>(paths); nextPaths.add(index); diff --git a/src/main/java/inference/rewrite/ResourceTree.java b/src/main/java/inference/rewrite/ResourceTree.java index 8ecdd14..881a778 100644 --- a/src/main/java/inference/rewrite/ResourceTree.java +++ b/src/main/java/inference/rewrite/ResourceTree.java @@ -4,13 +4,16 @@ import java.util.HashMap; import java.util.List; import java.util.Map; +import java.util.stream.Collectors; +import lombok.Getter; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; import models.terms.Resource; public class ResourceTree { + @Getter private Resource root; private Map> tree; private Map resourceMap; @@ -19,29 +22,35 @@ tree = new HashMap<>(); resourceMap = new HashMap<>(); constructResourceTree(term, new Position(List.of(0))); + root = resourceMap.get(new Position(List.of(0))); } - private Position constructResourceTree(EvaluatableTerm term, Position top) { + private List constructResourceTree(EvaluatableTerm term, Position top) { if (term instanceof Resource resource) { resourceMap.put(top, resource); - return top; + return List.of(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); + List dependingTermPositions = constructResourceTree(dependingTerm, top); + List resultPositions = new ArrayList<>(); + for (Position pos: dependingTermPositions) { + tree.put(pos, new ArrayList<>()); } - return resultPosition; + for (int i = 0; i < dependedResources.size(); i++) { + for (Position pos : dependingTermPositions) { + Position nextPos = pos.addPath(i); + tree.get(pos).add(nextPos); + Position dependedResourcePosition= constructResourceTree(dependedResources.get(i), nextPos).get(0); + tree.put(dependedResourcePosition, new ArrayList<>()); + Position argumentTermPosition = dependedResourcePosition.addPath(0); + tree.get(dependedResourcePosition).add(argumentTermPosition); + tree.put(argumentTermPosition, new ArrayList<>()); + resultPositions.addAll(constructResourceTree(argumentTerms.get(i), argumentTermPosition)); + } + } + return resultPositions; } else { return null; } @@ -61,5 +70,21 @@ } } + public void debugAllPath() { + debugAllPath(new Position(), new ArrayList<>()); + } + + private void debugAllPath(Position pos, List curPath) { + curPath.add(resourceMap.get(pos)); + if (tree.get(pos).size() == 0) { + System.out.println(curPath.stream().map(Resource::toString).collect(Collectors.joining("-"))); + } else { + for (Position nextPos: tree.get(pos)) { + debugAllPath(nextPos, curPath); + } + } + curPath.remove(curPath.size() - 1); + } + }