in meta/src/main/java/org/arend/lib/meta/equation/binop_matcher/ExpressionFunctionMatcher.java [33:63]
public List<CoreExpression> match(CoreExpression expr) {
return typechecker.withCurrentState(tc -> {
List<CoreInferenceReferenceExpression> varExprs = new ArrayList<>(numberOfArguments);
List<ConcreteExpression> concreteExprs = new ArrayList<>(numberOfArguments);
for (int i = 0; i < numberOfArguments; i++) {
CoreInferenceReferenceExpression varExpr = typechecker.generateNewInferenceVariable("var" + (i + 1), carrierExpr, marker, true);
varExprs.add(varExpr);
concreteExprs.add(factory.core(varExpr.computeTyped()));
}
TypedExpression result = tc.typecheck(factory.app(factory.core(mulTyped), true, concreteExprs), null);
boolean ok = result != null && tc.compare(result.getExpression(), expr, CMP.EQ, marker, false, true, false);
if (ok) {
for (CoreInferenceReferenceExpression varExpr : varExprs) {
if (varExpr.getSubstExpression() == null) {
ok = false;
break;
}
}
}
if (ok) {
List<CoreExpression> args = new ArrayList<>(numberOfArguments);
for (CoreInferenceReferenceExpression varExpr : varExprs) {
args.add(varExpr.getSubstExpression());
}
return args;
} else {
tc.loadSavedState();
return null;
}
});
}