in meta/src/main/java/org/arend/lib/meta/util/ReplaceSubexpressionsMeta.java [31:57]
public TypedExpression invoke(@NotNull ExpressionTypechecker typechecker, @NotNull ConcreteSourceNode marker) {
return Utils.tryTypecheck(typechecker, tc -> {
UncheckedExpression replaced = expression.replaceSubexpressions(expr -> {
for (Pair<TypedExpression, Object> pair : substPairs) {
boolean ok = false;
if (pair.proj1 instanceof CoreReferenceExpression) {
if (expr instanceof CoreReferenceExpression && ((CoreReferenceExpression) pair.proj1).getBinding() == ((CoreReferenceExpression) expr).getBinding()) {
ok = true;
}
} else {
if (tc.compare(pair.proj1.getType(), expr.computeType(), CMP.LE, marker, false, true, false) && tc.compare(expr, pair.proj1.getExpression(), CMP.EQ, marker, false, true, true)) {
tc.updateSavedState();
ok = true;
} else {
tc.loadSavedState();
}
}
if (ok) {
CoreBinding binding = pair.proj2 instanceof CoreBinding ? (CoreBinding) pair.proj2 : tc.getFreeBinding((ArendRef) pair.proj2);
return binding == null ? null : binding.makeReference();
}
}
return null;
}, false);
return replaced == null ? null : typechecker.check(replaced, marker);
});
}