in base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java [1123:1272]
private Boolean checkDefCallAndApp(Expression expr1, Expression expr2, boolean correctOrder) {
LeveledDefCallExpression defCall1 = expr1.cast(LeveledDefCallExpression.class);
if (!(defCall1 instanceof DataCallExpression || defCall1 instanceof ClassCallExpression || defCall1 instanceof FunCallExpression && ((FunCallExpression) defCall1).getDefinition().getKind() == CoreFunctionDefinition.Kind.TYPE)) return null;
AppExpression app2 = expr2.cast(AppExpression.class);
if (app2 == null) {
return null;
}
ClassCallExpression classCall1 = defCall1 instanceof ClassCallExpression ? (ClassCallExpression) defCall1 : null;
List<Expression> args = new ArrayList<>();
while (true) {
args.add(app2.getArgument());
Expression fun = app2.getFunction();
Expression funNorm = myNormalCompare ? fun.normalize(NormalizationMode.WHNF) : fun;
app2 = funNorm.cast(AppExpression.class);
if (app2 != null) {
continue;
}
TypeClassInferenceVariable variable;
FieldCallExpression fieldCall = funNorm.cast(FieldCallExpression.class);
if (fieldCall != null) {
while (true) {
funNorm = myNormalCompare ? fieldCall.getArgument().normalize(NormalizationMode.WHNF) : fieldCall.getArgument();
if (funNorm instanceof FieldCallExpression) {
fieldCall = (FieldCallExpression) funNorm;
} else {
break;
}
}
InferenceVariable infVar = funNorm.getInferenceVariable();
variable = infVar instanceof TypeClassInferenceVariable ? (TypeClassInferenceVariable) infVar : null;
} else {
variable = null;
}
if (variable == null || classCall1 == null && args.size() > defCall1.getDefCallArguments().size() || classCall1 != null && args.size() > classCall1.getDefinition().getNumberOfNotImplementedFields()) {
return null;
}
Collections.reverse(args);
DependentLink dataParams;
List<? extends Expression> oldDataArgs;
if (classCall1 == null) {
dataParams = defCall1.getDefinition().getParameters();
oldDataArgs = defCall1.getDefCallArguments();
} else {
List<Expression> classArgs = new ArrayList<>();
for (ClassField field : classCall1.getDefinition().getNotImplementedFields()) {
if (field.isProperty() || !field.getReferable().isParameterField()) {
break;
}
Expression implementation = classCall1.getAbsImplementationHere(field);
if (implementation != null) {
classArgs.add(implementation);
} else {
break;
}
}
if (args.size() > classArgs.size() || classCall1.getImplementedHere().size() > classArgs.size() && !(correctOrder && myCMP == CMP.LE || !correctOrder && myCMP == CMP.GE)) {
return null;
}
dataParams = new ClassCallExpression(classCall1.getDefinition(), classCall1.getLevels(), new LinkedHashMap<>(), classCall1.getDefinition().getSort(), classCall1.getDefinition().getUniverseKind()).getClassFieldParameters();
oldDataArgs = classArgs;
}
int numberOfOldArgs = oldDataArgs.size() - args.size();
ExprSubstitution substitution = new ExprSubstitution();
for (int i = 0; i < numberOfOldArgs; i++) {
substitution.add(dataParams, oldDataArgs.get(i));
dataParams = dataParams.getNext();
}
List<? extends Expression> oldList = oldDataArgs.subList(numberOfOldArgs, oldDataArgs.size());
if (!compareLists(correctOrder ? oldList : args, correctOrder ? args : oldList, null, defCall1.getDefinition(), substitution)) {
return false;
}
Expression lam;
Sort codSort;
List<SingleDependentLink> params = new ArrayList<>();
if (classCall1 == null) {
List<Expression> newDataArgs = new ArrayList<>(oldDataArgs.subList(0, numberOfOldArgs));
SingleDependentLink firstParam = null;
SingleDependentLink lastParam = null;
for (; dataParams.hasNext(); dataParams = dataParams.getNext()) {
SingleDependentLink link;
if (dataParams instanceof TypedDependentLink) {
link = new TypedSingleDependentLink(dataParams.isExplicit(), dataParams.getName(), dataParams.getType());
} else {
link = new UntypedSingleDependentLink(dataParams.getName());
}
newDataArgs.add(new ReferenceExpression(link));
if (firstParam == null) {
firstParam = link;
}
if (lastParam == null) {
lastParam = link;
} else {
lastParam.setNext(link);
}
if (link instanceof TypedSingleDependentLink) {
params.add(firstParam);
firstParam = null;
lastParam = null;
}
}
lam = defCall1.getDefinition().getDefCall(defCall1.getLevels(), newDataArgs);
codSort = defCall1 instanceof DataCallExpression ? ((DataCallExpression) defCall1).getDefinition().getSort() : ((UniverseExpression) ((FunCallExpression) defCall1).getDefinition().getResultType()).getSort();
} else {
Map<ClassField, Expression> implementations = new LinkedHashMap<>();
codSort = classCall1.getSortOfType();
ClassCallExpression classCall = new ClassCallExpression(classCall1.getDefinition(), classCall1.getLevels(), implementations, classCall1.getSort(), classCall1.getUniverseKind());
int i = 0;
for (ClassField field : classCall1.getDefinition().getNotImplementedFields()) {
if (i < oldDataArgs.size() - args.size()) {
implementations.put(field, classCall1.getImplementationHere(field, new ReferenceExpression(classCall.getThisBinding())));
i++;
} else {
PiExpression piType = classCall1.getDefinition().getFieldType(field, classCall1.getLevels(field.getParentClass()));
Expression type = piType.getCodomain();
TypedSingleDependentLink link = new TypedSingleDependentLink(field.getReferable().isExplicitField(), field.getName(), type instanceof Type ? (Type) type : new TypeExpression(type, piType.getResultSort()));
params.add(link);
implementations.put(field, new ReferenceExpression(link));
}
if (implementations.size() == oldDataArgs.size()) {
break;
}
}
classCall.updateHasUniverses();
lam = classCall;
}
for (int i = params.size() - 1; i >= 0; i--) {
if (!myNormalCompare || !myEquations.supportsLevels()) {
return false;
}
codSort = PiExpression.generateUpperBound(params.get(i).getType().getSortOfType(), codSort, myEquations, mySourceNode);
lam = new LamExpression(codSort, params.get(i), lam);
}
Expression finalExpr1 = correctOrder ? lam : substitute(fun);
Expression finalExpr2 = correctOrder ? fun : substitute(lam);
if (variable.isSolved()) {
CompareVisitor visitor = new CompareVisitor(myEquations, myCMP, variable.getSourceNode());
visitor.myNormalCompare = myNormalCompare;
return visitor.compare(finalExpr1, finalExpr2, null, true);
} else {
return myNormalCompare && myEquations.addEquation(finalExpr1, finalExpr2, null, myCMP, variable.getSourceNode(), correctOrder ? null : variable, correctOrder ? variable : null) ? true : null;
}
}
}