static FunctionMatcher makeFieldMatcher()

in meta/src/main/java/org/arend/lib/meta/equation/binop_matcher/FunctionMatcher.java [17:48]


  static FunctionMatcher makeFieldMatcher(CoreClassCallExpression classCall, TypedExpression instance, CoreClassField field, ExpressionTypechecker typechecker, ConcreteFactory factory, ConcreteSourceNode marker, StdExtension ext, int numberOfArguments) {
    CoreExpression expr = classCall.getImplementation(field, instance);
    if (numberOfArguments == 0 && expr != null) {
      return new ExpressionFunctionMatcher(typechecker, factory, marker, expr.computeTyped(), null, 0);
    }
    if (!(expr instanceof CoreLamExpression)) {
      return new DefinitionFunctionMatcher(field, numberOfArguments);
    }

    CoreExpression body = ((CoreLamExpression) expr).getBody();
    CoreParameter param1 = ((CoreLamExpression) expr).getParameters();
    CoreParameter param2 = param1.getNext();
    if (!param2.hasNext() && body instanceof CoreLamExpression) {
      param2 = ((CoreLamExpression) body).getParameters();
      body = ((CoreLamExpression) body).getBody();
    }
    if (param2.hasNext() && !param2.getNext().hasNext() && body instanceof CoreFunCallExpression) {
      CoreFunCallExpression funCall = (CoreFunCallExpression) body;
      if (funCall.getDefinition() == ext.append) {
        List<? extends CoreExpression> args = funCall.getDefCallArguments();
        if (args.get(1) instanceof CoreReferenceExpression && ((CoreReferenceExpression) args.get(1)).getBinding() == param1.getBinding() && args.get(2) instanceof CoreReferenceExpression && ((CoreReferenceExpression) args.get(2)).getBinding() == param2.getBinding()) {
          return new ListFunctionMatcher(typechecker, factory, ext);
        }
      } else if (funCall.getDefinition() == ext.prelude.getPlus()) {
        List<? extends CoreExpression> args = funCall.getDefCallArguments();
        if (args.get(0) instanceof CoreReferenceExpression && ((CoreReferenceExpression) args.get(0)).getBinding() == param1.getBinding() && args.get(1) instanceof CoreReferenceExpression && ((CoreReferenceExpression) args.get(1)).getBinding() == param2.getBinding()) {
          return new NatFunctionMatcher(typechecker, factory, ext);
        }
      }
    }
    return new ExpressionFunctionMatcher(typechecker, factory, marker, expr.computeTyped(), ((CoreLamExpression) expr).getParameters().getTypeExpr(), numberOfArguments);
  }