in base/src/main/java/org/arend/typechecking/implicitargs/equations/TwoStageEquations.java [86:264]
public boolean addEquation(Expression origExpr1, Expression origExpr2, Expression type, CMP cmp, Concrete.SourceNode sourceNode, InferenceVariable stuckVar1, InferenceVariable stuckVar2, boolean normalize) {
origExpr1 = origExpr1.accept(new UnfoldVisitor(Collections.emptySet(), null, false, UnfoldVisitor.UnfoldFields.ONLY_PARAMETERS), null);
origExpr2 = origExpr2.accept(new UnfoldVisitor(Collections.emptySet(), null, false, UnfoldVisitor.UnfoldFields.ONLY_PARAMETERS), null);
Expression expr1 = normalize ? origExpr1.normalize(NormalizationMode.WHNF) : origExpr1;
Expression expr2 = normalize ? origExpr2.normalize(NormalizationMode.WHNF) : origExpr2;
if (expr1 instanceof SubstExpression && !(expr2 instanceof SubstExpression)) {
Pair<Expression, ExprSubstitution> pair = reverseSubstitution(expr1);
if (pair != null) {
origExpr1 = expr1 = pair.proj1;
SubstVisitor substVisitor = new SubstVisitor(pair.proj2, LevelSubstitution.EMPTY, false);
expr2 = expr2.accept(substVisitor, null);
origExpr2 = normalize ? origExpr2.accept(substVisitor, null) : expr2;
}
} else if (expr2 instanceof SubstExpression && !(expr1 instanceof SubstExpression)) {
Pair<Expression, ExprSubstitution> pair = reverseSubstitution(expr2);
if (pair != null) {
origExpr2 = expr2 = pair.proj1;
SubstVisitor substVisitor = new SubstVisitor(pair.proj2, LevelSubstitution.EMPTY, false);
expr1 = expr1.accept(substVisitor, null);
origExpr1 = normalize ? origExpr1.accept(substVisitor, null) : expr1;
}
}
InferenceVariable inf1 = expr1.getInferenceVariable();
InferenceVariable inf2 = expr2.getInferenceVariable();
// expr1 == expr2 == ?x
if (inf1 == inf2 && inf1 != null) {
return true;
}
if (inf1 == null && inf2 == null) {
// expr1 == field call
FieldCallExpression fieldCall1 = expr1.dropArguments().cast(FieldCallExpression.class);
InferenceVariable variable = fieldCall1 == null ? null : fieldCall1.getArgument().getInferenceVariable();
if (variable instanceof TypeClassInferenceVariable) {
// expr1 == class field call
Boolean result = solveInstance((TypeClassInferenceVariable) variable, fieldCall1, expr2);
if (result != null) {
return result || CompareVisitor.compare(this, cmp, expr1, expr2, type, sourceNode);
}
}
// expr2 == field call
if (variable == null) {
FieldCallExpression fieldCall2 = expr2.dropArguments().cast(FieldCallExpression.class);
variable = fieldCall2 == null ? null : fieldCall2.getArgument().getInferenceVariable();
if (variable instanceof TypeClassInferenceVariable) {
// expr2 == class field call
Boolean result = solveInstance((TypeClassInferenceVariable) variable, fieldCall2, expr1);
if (result != null) {
return result || CompareVisitor.compare(this, cmp, expr1, expr2, type, sourceNode);
}
}
}
}
CMP origCmp = cmp;
// expr1 == ?x && expr2 /= ?y || expr1 /= ?x && expr2 == ?y
if (inf1 == null && inf2 != null && inf2.isSolvableFromEquations() || inf2 == null && inf1 != null && inf1.isSolvableFromEquations()) {
InferenceVariable cInf = inf1 != null ? inf1 : inf2;
Expression cType = inf1 != null ? expr2 : expr1;
if (inf1 != null) {
cmp = cmp.not();
}
// cType /= Pi, cType /= Type, cType /= Class, cType /= stuck on ?X
if (!(cType instanceof PiExpression) && !(cType instanceof UniverseExpression) && (!(cType instanceof ClassCallExpression) || cmp == CMP.GE && ((ClassCallExpression) cType).getNumberOfNotImplementedFields() == 0) && cType.getStuckInferenceVariable() == null) {
cmp = CMP.EQ;
}
if (cType instanceof UniverseExpression && ((UniverseExpression) cType).getSort().isProp()) {
if (cmp == CMP.LE) {
myProps.add(cInf);
return true;
} else {
cmp = CMP.EQ;
}
}
// If cType is not pi, classCall, universe, or a stuck expression, then solve immediately.
if (cmp != CMP.EQ) {
Expression cod = cType;
while (cod instanceof PiExpression) {
cod = ((PiExpression) cod).getCodomain().getUnderlyingExpression();
}
if (!(cod instanceof ClassCallExpression) && !(cod instanceof UniverseExpression) && cod.getStuckInferenceVariable() == null) {
cmp = CMP.EQ;
}
}
// ?x == _
if (cmp == CMP.EQ) {
InferenceReferenceExpression infRef = cType instanceof FieldCallExpression ? ((FieldCallExpression) cType).getArgument().cast(InferenceReferenceExpression.class) : null;
if (infRef == null || !(infRef.getVariable() instanceof TypeClassInferenceVariable)) {
Expression typeType = cType.getType().normalize(NormalizationMode.WHNF);
boolean useOrig = !(typeType instanceof UniverseExpression || typeType instanceof DataCallExpression && ((DataCallExpression) typeType).getDefinition() == Prelude.FIN);
Expression solution = useOrig ? (inf1 != null ? origExpr2 : origExpr1) : cType;
if (solve(cInf, solution, false, cInf instanceof TypeClassInferenceVariable, true, true) != SolveResult.NOT_SOLVED) {
return true;
}
if (useOrig && solution != cType && solve(cInf, cType, false, cInf instanceof TypeClassInferenceVariable, true, true) != SolveResult.NOT_SOLVED) {
return true;
}
}
}
// ?x <> Pi
if (cType instanceof PiExpression) {
List<PiExpression> pis = new ArrayList<>();
Expression cod = cType;
while (cod instanceof PiExpression) {
pis.add((PiExpression) cod);
cod = ((PiExpression) cod).getCodomain().normalize(NormalizationMode.WHNF);
}
Sort codSort = Sort.generateInferVars(this, false, sourceNode);
try (var ignore = new Utils.RefContextSaver(myVisitor.getContext(), myVisitor.getLocalExpressionPrettifier())) {
for (PiExpression pi : pis) {
for (SingleDependentLink link = pi.getParameters(); link.hasNext(); link = link.getNext()) {
myVisitor.addBinding(null, link);
}
}
InferenceVariable infVar = new DerivedInferenceVariable(cInf.getName() + "-cod", cInf, new UniverseExpression(codSort), myVisitor.getAllBindings());
Expression newRef = InferenceReferenceExpression.make(infVar, this);
Expression solution = newRef;
Sort piSort = codSort;
for (int i = pis.size() - 1; i >= 0; i--) {
piSort = PiExpression.generateUpperBound(pis.get(i).getParameters().getType().getSortOfType(), piSort, this, sourceNode);
solution = new PiExpression(piSort, pis.get(i).getParameters(), solution);
}
solve(cInf, solution, false);
return addEquation(cod, newRef, Type.OMEGA, cmp, sourceNode, cod.getStuckInferenceVariable(), infVar);
}
}
// ?x <> Type
if (cType instanceof UniverseExpression) {
Sort genSort = Sort.generateInferVars(this, true, cInf.getSourceNode());
solve(cInf, new UniverseExpression(genSort), false);
Sort sort = ((UniverseExpression) cType).getSort();
if (cmp == CMP.LE) {
Sort.compare(sort, genSort, CMP.LE, this, sourceNode);
} else {
if (!sort.getPLevel().isInfinity()) {
addLevelEquation(genSort.getPLevel().getVar(), sort.getPLevel().getVar(), sort.getPLevel().getConstant(), sort.getPLevel().getMaxConstant(), sourceNode);
}
if (!sort.getHLevel().isInfinity()) {
addLevelEquation(genSort.getHLevel().getVar(), sort.getHLevel().getVar(), sort.getHLevel().getConstant(), sort.getHLevel().getMaxConstant(), sourceNode);
}
}
return true;
}
}
if (cmp == CMP.EQ && (inf1 != null && inf2 == null || inf2 != null && inf1 == null)) {
Expression prev = myNotSolvableFromEquationsVars.putIfAbsent(inf1 != null ? inf1 : inf2, inf1 != null ? expr2 : expr1);
if (prev != null) {
return CompareVisitor.compare(this, CMP.EQ, prev, inf1 != null ? expr2 : expr1, type, sourceNode);
}
}
Equation equation = new Equation(expr1, expr2, type, origCmp, sourceNode);
myEquations.add(equation);
if (inf1 != null && inf2 != null) {
inf1.addListener(equation);
inf2.addListener(equation);
} else {
if (stuckVar1 != null) {
stuckVar1.addListener(equation);
}
if (stuckVar2 != null) {
stuckVar2.addListener(equation);
}
}
return true;
}