diff --git a/src/Main.java b/src/Main.java index 053d306..be3a996 100644 --- a/src/Main.java +++ b/src/Main.java @@ -1,10 +1,13 @@ import java.util.ArrayList; +import java.util.HashMap; import java.util.List; +import java.util.Map; import inference.ProofSystem; import lombok.SneakyThrows; import models.algebra.Expression; import models.algebra.Type; +import models.algebra.Variable; import models.dataConstraintModel.DataConstraintModel; import models.dataFlowModel.DataTransferModel; import models.formulas.DependencyFormula; @@ -13,7 +16,9 @@ import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; +import models.terms.RDLTerm; import models.terms.ResourceVariable; +import models.terms.meta.OrderVariableConstraint; import parser.Parser; import parser.Parser.TokenStream; @@ -64,6 +69,29 @@ } System.out.println("=================="); System.out.println(conclusion.getRightSideHand().linearRightNormalize().toString()); + + + sandbox1(); + } + + static void sandbox1() { + System.out.println("------------------------------------------------------------sandbox1"); + ResourceVariable a = new ResourceVariable("A", INT, 2); + ResourceVariable b = new ResourceVariable("B", INT, 2); + ResourceVariable c = new ResourceVariable("C", INT, 2); + ResourceVariable ap = new ResourceVariable("A'", INT, 2); + ResourceVariable bp = new ResourceVariable("B''", INT, 2); + ResourceVariable cp = new ResourceVariable("C''", INT, 2); + + DependencyTerm d1 = new DependencyTerm(a, b, c); + DependencyTerm d11 = new DependencyTerm(a, b, c); + DependencyTerm d2 = new DependencyTerm(ap, bp, cp); + EquationFormula conclu1 = new EquationFormula(d1, d11); + Map binding = new HashMap<>(); + Map orderConstraint = new HashMap<>(); + boolean tmp1 = ProofSystem.REFLEXIVE_LAW.check(List.of(), conclu1, binding, orderConstraint); + boolean tmp2 = ProofSystem.RIGHT_REPLACEMENT.check(List.of(), conclu1, binding, orderConstraint); + System.out.println(tmp1); } @SneakyThrows diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java index e99e7c4..da86702 100644 --- a/src/inference/InferenceRule.java +++ b/src/inference/InferenceRule.java @@ -52,32 +52,36 @@ this.defaultOrderConstraint = null; } - public boolean check(Collection assumptions, Formula conclusion) { + public boolean check(Collection assumptions, Formula conclusion, + Map binding, Map orderConstraints) { if (this.assumptions.size() > assumptions.size()) { return false; } for(List assumption : permutation(assumptions, this.assumptions.size())) { - if (check(assumption, conclusion)) { + if (check(assumption, conclusion, binding, orderConstraints)) { return true; } } return false; } - private boolean check(List assumptions, Formula conclusion) { - Map binding = new HashMap<>(); - Map orderConstraints = new HashMap<>(); + private boolean check(List assumptions, Formula conclusion, + Map binding, Map orderConstraints) { + Map tmpBinding = new HashMap<>(binding); + Map tmpOrderConstraints = new HashMap<>(orderConstraints); for (int i = 0; i < assumptions.size(); i++) { - if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraints)) { + if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), tmpBinding, tmpOrderConstraints)) { return false; } } - if (! this.conclusion.isMatchedBy(conclusion, binding, orderConstraints)) { + if (! this.conclusion.isMatchedBy(conclusion, tmpBinding, tmpOrderConstraints)) { return false; } if (this.defaultOrderConstraint != null) { - return defaultOrderConstraint.check(orderConstraints); + return defaultOrderConstraint.check(tmpOrderConstraints); } + binding.putAll(tmpBinding); + orderConstraints.putAll(tmpOrderConstraints); return true; } diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java index 9d3d3b4..5ce155e 100644 --- a/src/inference/ProofSystem.java +++ b/src/inference/ProofSystem.java @@ -17,14 +17,14 @@ public class ProofSystem { - private final static InferenceRule REFLEXIVE_LAW = new InferenceRule("relfexive law", List.of(), + public final static InferenceRule REFLEXIVE_LAW = new InferenceRule("relfexive law", List.of(), new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("te")))); - private final static InferenceRule SYMMETRIC_LAW = new InferenceRule("symmetric law", + public final static InferenceRule SYMMETRIC_LAW = new InferenceRule("symmetric law", List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("se")))), new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te")))); - private final static InferenceRule TRANSITIVE_LAW = new InferenceRule("transitive law", + public final static InferenceRule TRANSITIVE_LAW = new InferenceRule("transitive law", List.of( new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te"))), new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue"))) @@ -32,12 +32,12 @@ new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("ue"))) ); - private final static InferenceRule IDENTITY_MAPPING = new InferenceRule("identity mapping", + public final static InferenceRule IDENTITY_MAPPING = new InferenceRule("identity mapping", List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v")))), new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v"))) ); - private final static InferenceRule COMPOSITE_MAPPING = new InferenceRule("composite mapping", + public final static InferenceRule COMPOSITE_MAPPING = new InferenceRule("composite mapping", List.of( new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v"))), new MetaDependencyFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w"))) @@ -45,7 +45,7 @@ new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("w"))) ); - private final static InferenceRule LEFT_PROJECTION = new InferenceRule("left projection", + public final static InferenceRule LEFT_PROJECTION = new InferenceRule("left projection", List.of(new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), @@ -59,7 +59,7 @@ ) ); - private final static InferenceRule RIGHT_PROJECTION = new InferenceRule("left projection", + public final static InferenceRule RIGHT_PROJECTION = new InferenceRule("left projection", List.of(new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), @@ -73,7 +73,7 @@ ) ); - private final static InferenceRule CONSTANT_MAPPING = new InferenceRule("constant mapping", + public final static InferenceRule CONSTANT_MAPPING = new InferenceRule("constant mapping", List.of(), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), @@ -82,13 +82,13 @@ new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) ); // 定値写像?? - private final static InferenceRule ORDER_DESCENTING = new InferenceRule("order descenting", + public final static InferenceRule ORDER_DESCENTING = new InferenceRule("order descenting", List.of(new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")))), new MetaDependencyFormula(new MetaRDLTerm(new MetaDependencyVariable(new Variable("d"), new Variable("n")))), new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) ); // 階数降下?? - private final static InferenceRule RIGHT_REPLACEMENT = new InferenceRule("right replacement", + public final static InferenceRule RIGHT_REPLACEMENT = new InferenceRule("right replacement", List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue")))), new MetaEquationFormula( new MetaRDLTerm( @@ -104,7 +104,7 @@ ) ); - private final static InferenceRule IDENTITY_LAW = new InferenceRule("identity law", + public final static InferenceRule IDENTITY_LAW = new InferenceRule("identity law", List.of(new MetaInFormula( new MetaEvaluatableTermVariable(new Variable("te")), new MetaRDLTerm(new MetaResourceVariable(new Variable("v")))) @@ -119,7 +119,7 @@ ) ); - private final static InferenceRule JOIN = new InferenceRule("join", + public final static InferenceRule JOIN = new InferenceRule("join", List.of(new MetaEquationFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))), new MetaEquationFormula( new MetaRDLTerm( @@ -139,7 +139,7 @@ ) ); - private final static InferenceRule CONSTANT_VALUE_LAW = new InferenceRule("constant value law", + public final static InferenceRule CONSTANT_VALUE_LAW = new InferenceRule("constant value law", List.of(new MetaInFormula( new MetaEvaluatableTermVariable(new Variable("t")), new MetaRDLTerm(new MetaResourceVariable(new Variable("v"), new Variable("m")))) @@ -155,7 +155,7 @@ new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) );//定値性?? - private final static InferenceRule RIGHT_NORMALIZE = new InferenceRule("right normalize", + public final static InferenceRule RIGHT_NORMALIZE = new InferenceRule("right normalize", List.of( new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te")), @@ -189,7 +189,7 @@ new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) ); - private final static InferenceRule PSEUDO_IDENTITY_LAW = new InferenceRule("pseudo identity law", + public final static InferenceRule PSEUDO_IDENTITY_LAW = new InferenceRule("pseudo identity law", List.of( new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), @@ -207,7 +207,7 @@ new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) );//疑似恒等性?? - private final static InferenceRule SET_EQUIVALENCE = new InferenceRule("set equivalence", + public final static InferenceRule SET_EQUIVALENCE = new InferenceRule("set equivalence", List.of(new MetaEquationFormula( new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) @@ -219,7 +219,7 @@ new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) );//集合同値性?? - private final static InferenceRule HOMOMORPHISM = new InferenceRule("homomorphism", + public final static InferenceRule HOMOMORPHISM = new InferenceRule("homomorphism", List.of(new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("se")), new MetaResourceVariable(new Variable("v")) diff --git a/src/tests/inferencerule/InferenceRuleTest.java b/src/tests/inferencerule/InferenceRuleTest.java index f1e89bb..05f2b34 100644 --- a/src/tests/inferencerule/InferenceRuleTest.java +++ b/src/tests/inferencerule/InferenceRuleTest.java @@ -5,6 +5,7 @@ import org.junit.jupiter.api.Test; +import java.util.HashMap; import java.util.List; import inference.InferenceRule; @@ -44,7 +45,7 @@ DependencyFormula df1 = new DependencyFormula(d1); // a : b DependencyFormula df2 = new DependencyFormula(d2); // b : c DependencyFormula df3 = new DependencyFormula(d3); // a : c - assertTrue(goseShazo.check(List.of(df1, df2), df3)); + assertTrue(goseShazo.check(List.of(df1, df2), df3, new HashMap<>(), new HashMap<>())); } @@ -73,7 +74,7 @@ EquationFormula assump2 = new EquationFormula(a, xyz); // a = [x : y -> z] EquationFormula concl2 = new EquationFormula(new DependencyTerm(c, d, a), new DependencyTerm(c, d, xyz)); // [c : d -> a] = [c : d -> [x : y -> z]] - assertTrue(rightReplacement.check(List.of(assump2), concl2)); + assertTrue(rightReplacement.check(List.of(assump2), concl2, new HashMap<>(), new HashMap<>())); } }