package inference.axioms;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import exceptions.SubstituteFailedException;
import inference.EquationAxiom;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDependencyTerm;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaDynamicDependencyTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;
import utils.ExpressionUtils;
public class Uncurrying extends EquationAxiom {
public Uncurrying() {
super("Uncurrying");
assumptions.add(
new MetaDependencyFormula(
new MetaDynamicDependency(
new MetaTermGenerator() {
@Override
public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
int i = maxDepth - curDepth;
context.put("" + curDepth, curIndex);
context.put("depth", curDepth + 1);
if (curDepth == maxDepth - 1 && curIndex == 0) {
return new MetaDynamicDependency(
new MetaTermGenerator() {
@Override
public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map<String, Object> context2) {
curIndex2 -= 2;
context2.put("" + curDepth2, curIndex2 + 1);
context2.put("depth", curDepth2);
return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2), new Variable("n"));
}
},
new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"))
);
} else if (curIndex == 0) {
return new MetaDynamicDependency(this);
}
curIndex -= 1;
return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i));
}
}
)
)
);
assumptions.add(
new MetaEquationFormula(
new MetaDependencyTerm(
new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m")),
new MetaEvaluatableTermVariable(new Variable("xxx")),
new MetaEvaluatableTermVariable(new Variable("yyy"))
),
new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m"))
)
);
assumptions.add(
new MetaEquationFormula(
new MetaDependencyTerm(
new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
new MetaEvaluatableTermVariable(new Variable("xxxx")),
new MetaEvaluatableTermVariable(new Variable("yyyy"))
),
new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m"))
)
);
conclusion = new MetaEquationFormula(
new MetaDynamicDependencyTerm(
new MetaTermGenerator() {
@Override
public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
int i = maxDepth - curDepth;
maxIndex = (Integer) context.get("" + curDepth);
if (curDepth == maxDepth - 1 && curIndex == 0) {
return new MetaDynamicDependencyTerm(
new MetaTermGenerator() {
@Override
public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map<String, Object> context2) {
curIndex2 -= 3;
maxIndex2 = (Integer) context.getOrDefault("" + curDepth2, 0);
if (curIndex2 >= maxIndex2 * 2) {
return null;
}
if (curIndex2 % 2 == 0) {
return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2 / 2), new Variable("n"));
}
return new MetaEvaluatableTermVariable(new Variable("x" + curDepth2 + "_" + curIndex2 / 2), new Variable("n"));
}
},
new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m"))
);
}
if (curIndex == 0) {
return new MetaDynamicDependency(this);
}
curIndex -= 1;
if (curIndex >= maxIndex * 2) {
return null;
}
if (curIndex % 2 == 0) {
return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
}
return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
}
}
),
new MetaDynamicDependencyTerm(
new MetaTermGenerator() {
@Override
public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
int m = (Integer) context.get("m");
int n = (Integer) context.get("n");
int i = maxDepth - curDepth;
maxIndex = (Integer) context.get("" + curDepth);
if (curDepth == maxDepth - 1 && curIndex == 0) {
return new MetaDynamicDependencyTerm(
new MetaTermGenerator() {
@Override
public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map<String, Object> context2) {
curIndex2 -= 3;
maxIndex2 = (Integer) context.getOrDefault("" + curDepth2, 0);
if (curIndex2 >= maxIndex2 * 2) {
return null;
}
if (curIndex2 % 2 == 0) {
return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2 / 2), new Variable("n"));
}
return new MetaEvaluatableTermVariable(new Variable("x" + curDepth2 + "_" + curIndex2 / 2), new Variable("n"));
}
},
new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m"))
);
}
if (curIndex == 0) {
return new MetaDynamicDependency(this);
}
curIndex -= 1;
if (n - i == m) {
if (curIndex == 0) {
return new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m"));
}
if (curIndex == 1) {
return new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m"));
}
curIndex -= 2;
if (curIndex >= maxIndex * 2) {
return null;
}
if (curIndex % 2 == 0) {
return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
}
return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
}
if (curIndex >= maxIndex * 2) {
return null;
}
if (curIndex % 2 == 0) {
return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
}
return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
}
}
)
);
}
@Override
protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
Set<MatchConstraint> result = new HashSet<>();
result.add(constraint);
if (assumptions.size() < 2) {
return new HashSet<>();
}
for (int i = 0; i < 3; i++) {
result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result);
if (result.isEmpty()) {
return new HashSet<>();
}
}
int count = 3;
int depth = (Integer) context.get("depth");
for (int d = 1; d < depth + 1; d++) {
if (! context.containsKey("" + d)) break;
for (int i = 0; i < (Integer) context.getOrDefault("" + d, 0); i++) {
Formula assumption = assumptions.get(count);
MetaEquationFormula mef = new MetaEquationFormula(
new MetaDependencyTerm(
new MetaEvaluatableTermVariable(new Variable("v" + d + "_" + i), ExpressionUtils.parse("n-" + (depth - d))),
new MetaEvaluatableTermVariable(new Variable("xxx" + d + "_" + i)),
new MetaEvaluatableTermVariable(new Variable("yyy" + d + "_" + i))
),
new MetaEvaluatableTermVariable(new Variable("x" + d + "_" + i), ExpressionUtils.parse("n-" + (depth - d)))
);
result = mef.isMatchedBy(assumption, result);
if (result.isEmpty()) {
return new HashSet<>();
}
count++;
}
}
Set<Formula> subRes = new HashSet<>();
for (MatchConstraint con: result) {
try {
int maxIndex = 10000;
int maxDepth = depth;
con.getContext().put("maxIndex", maxIndex);
con.getContext().put("maxDepth", maxDepth);
con.getContext().put("m", con.getOrderConstraint().get(new Variable("m")).getOrder());
con.getContext().put("n", con.getOrderConstraint().get(new Variable("n")).getOrder());
subRes.add(conclusion.substitution(con.getBinding(), con.getContext()));
} catch (SubstituteFailedException e) {
continue;
}
}
return subRes;
}
}
