public static CoreExpression eval()

in meta/src/main/java/org/arend/lib/pattern/PatternUtils.java [229:264]
36 lines of code
12 McCabe index (conditional complexity)

  public static CoreExpression eval(CoreElimBody body, LevelSubstitution levelSubst, List<? extends CorePattern> patterns, List<? extends TypedExpression> removedArgs, ExpressionTypechecker typechecker, StdExtension ext, ConcreteFactory factory, Map<CoreBinding, ArendRef> bindings) {
    loop:
    for (CoreElimClause clause : body.getClauses()) {
      Map<CoreBinding, CorePattern> subst1 = new HashMap<>();
      Map<CoreBinding, CorePattern> subst2 = new HashMap<>();
      if (unify(clause.getPatterns(), patterns, subst1, subst2)) {
        for (CorePattern value : subst2.values()) {
          if (value.getBinding() == null) {
            continue loop;
          }
        }
        AbstractedExpression expr = clause.getAbstractedExpression();
        if (expr == null) {
          return null;
        }
        CoreParameter param = getAllBindings(clause.getPatterns());
        if (param == null) {
          return (CoreExpression) expr;
        }
        Map<CoreBinding, TypedExpression> removedMap = new HashMap<>();
        for (int i = 0; i < removedArgs.size(); i++) {
          CoreBinding binding = clause.getPatterns().get(i).getBinding();
          if (removedArgs.get(i) != null && binding != null) {
            removedMap.put(binding, removedArgs.get(i));
          }
        }
        List<ConcreteExpression> args = new ArrayList<>();
        for (; param.hasNext(); param = param.getNext()) {
          TypedExpression removed = removedMap.get(param.getBinding());
          args.add(removed != null ? factory.core(removed) : toExpression(subst1.get(param.getBinding()), ext, factory, bindings));
        }
        return (CoreExpression) typechecker.substituteAbstractedExpression(expr, levelSubst, args, null);
      }
    }
    return null;
  }