public ArgParameters()

in meta/src/main/java/org/arend/lib/meta/CasesMeta.java [210:238]


    public ArgParameters(ConcreteExpression expr, ErrorReporter errorReporter, boolean allowType) {
      if (expr instanceof ConcreteAppExpression && ((ConcreteAppExpression) expr).getFunction() instanceof ConcreteReferenceExpression && ((ConcreteReferenceExpression) ((ConcreteAppExpression) expr).getFunction()).getReferent() == argRef) {
        List<? extends ConcreteArgument> parameters = ((ConcreteAppExpression) expr).getArguments();
        Map<ArendRef, ConcreteExpression> params = new HashMap<>();
        Set<ArendRef> flags = new HashSet<>();
        parameter.getAllValues(parameters.get(1).getExpression(), params, flags, null, errorReporter);
        ConcreteExpression nameExpr = params.get(nameRef);
        name = nameExpr instanceof ConcreteReferenceExpression ? ((ConcreteReferenceExpression) nameExpr).getReferent() : null;
        addPath = flags.contains(addPathRef);
        ConcreteExpression asExpr = params.get(asRef);
        as = asExpr instanceof ConcreteReferenceExpression ? ((ConcreteReferenceExpression) asExpr).getReferent() : null;
        expression = parameters.get(0).getExpression();
        type = allowType && parameters.size() > 2 ? parameters.get(2).getExpression() : null;
        if (!allowType && parameters.size() > 2) {
          errorReporter.report(new TypecheckingError(GeneralError.Level.WARNING_UNUSED, "Type is ignored", parameters.get(2).getExpression()));
        }
      } else {
        name = null;
        addPath = false;
        as = null;
        if (allowType && expr instanceof ConcreteTypedExpression) {
          expression = ((ConcreteTypedExpression) expr).getExpression();
          type = ((ConcreteTypedExpression) expr).getType();
        } else {
          expression = expr;
          type = null;
        }
      }
    }