public List match()

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;
      }
    });
  }