public TypedExpression invoke()

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