private Pair typecheckParameters()

in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [522:702]
166 lines of code
78 McCabe index (conditional complexity)

  private Pair<Sort,Expression> typecheckParameters(Concrete.GeneralDefinition def, Definition typedDef, LinkList list, LocalInstancePool localInstancePool, Sort expectedSort, DependentLink oldParameters, ClassField implementedField, List<Boolean> typedParameters) {
    Sort sort = Sort.PROP;

    PiExpression fieldType = implementedField == null ? null : implementedField.getType();
    if (oldParameters != null) {
      list.append(oldParameters);
      fieldType = null;
    }

    boolean isClassCoclause = def instanceof Concrete.CoClauseFunctionDefinition && ((Concrete.CoClauseFunctionDefinition) def).getKind() == FunctionKind.CLASS_COCLAUSE;
    DependentLink thisRef = fieldType == null || isClassCoclause ? null : fieldType.getParameters();
    Expression resultType = fieldType == null ? null : isClassCoclause ? fieldType : fieldType.getCodomain();
    ExprSubstitution substitution = fieldType == null ? null : new ExprSubstitution();
    int skip = def instanceof Concrete.CoClauseFunctionDefinition ? ((Concrete.CoClauseFunctionDefinition) def).getNumberOfExternalParameters() : 0;
    Expression expectedType = expectedSort == null ? Type.OMEGA : new UniverseExpression(expectedSort);

    boolean first = true;
    List<? extends Concrete.Parameter> parameters = def.getParameters();
    for (Concrete.Parameter parameter : parameters) {
      if (skip == 0 && resultType != null && !(resultType instanceof ErrorExpression)) {
        resultType = resultType.normalize(NormalizationMode.WHNF).getUnderlyingExpression();
      }

      Type paramResult = null;
      if (parameter.getType() != null) {
        paramResult = def instanceof Concrete.Constructor ? typechecker.checkType(parameter.getType(), expectedType) : typechecker.finalCheckType(parameter.getType(), expectedType, false);
        if (typedParameters != null) {
          typedParameters.add(true);
        }
      } else if (skip == 0) {
        if (resultType instanceof PiExpression && typedDef != null) {
          SingleDependentLink param = ((PiExpression) resultType).getParameters();
          if (param.isExplicit() != parameter.isExplicit()) {
            errorReporter.report(new ArgumentExplicitnessError(param.isExplicit(), parameter));
            break;
          }
          Type paramType = param.getType();
          if (thisRef != null && paramType.getExpr().findBinding(thisRef)) {
            errorReporter.report(new TypeFromFieldError(typechecker.getExpressionPrettifier(), TypeFromFieldError.parameter(), paramType.getExpr(), parameter));
          } else {
            paramResult = paramType.subst(new SubstVisitor(substitution, typedDef.makeIdLevels().makeSubstitution(implementedField.getParentClass())));
          }
        } else if (resultType == null || typedDef == null || !resultType.reportIfError(errorReporter, parameter)) {
          if (resultType == null || typedDef == null) {
            if (typedParameters != null && parameter instanceof Concrete.NameParameter) {
              typedParameters.add(false);
            } else {
              errorReporter.report(new TypecheckingError("Expected a typed parameter", parameter));
            }
          } else {
            errorReporter.report(new FieldTypeParameterError(typechecker.getExpressionPrettifier(), fieldType.getCodomain(), parameter));
            resultType = new ErrorExpression();
          }
        }
      }
      boolean isProperty = parameter.isProperty();
      if (paramResult == null) {
        if (typedParameters == null) {
          paramResult = new TypeExpression(new ErrorExpression(), Sort.SET0);
        }
      } else if (isProperty && !Sort.compare(paramResult.getSortOfType(), Sort.PROP, CMP.LE, typechecker.getEquations(), parameter)) {
        errorReporter.report(new TypecheckingError("The type of the parameter should live in \\Prop, but lives in " + paramResult.getSortOfType(), parameter));
        isProperty = false;
      }
      if (!(def instanceof Concrete.Constructor) && paramResult != null) {
        sort = sort.max(paramResult.getSortOfType());
      }

      DependentLink param;
      int numberOfParameters;
      boolean oldParametersOK = true;
      if (parameter instanceof Concrete.TelescopeParameter) {
        List<? extends Referable> referableList = parameter.getReferableList();
        if (referableList.isEmpty()) {
          errorReporter.report(new TypecheckingError("Empty parameter list", parameter));
          continue;
        }

        List<String> names = parameter.getNames();
        param = oldParameters != null ? oldParameters : paramResult == null ? null
          : referableList.size() == 1 && referableList.get(0) instanceof HiddenLocalReferable
            ? parameter(parameter.isExplicit(), isProperty, names.get(0), paramResult, true)
            : parameter(parameter.isExplicit(), isProperty, names, paramResult);
        numberOfParameters = names.size();

        if (oldParameters == null) {
          int i = 0;
          if (param != null) {
            for (DependentLink link = param; link.hasNext(); link = link.getNext(), i++) {
              typechecker.addBinding(referableList.get(i), link);
            }
          }
        } else {
          for (int i = 0; i < names.size(); i++) {
            if (oldParameters.hasNext()) {
              typechecker.addBinding(referableList.get(i), oldParameters);
              oldParameters = oldParameters.getNext();
            } else {
              oldParametersOK = false;
              break;
            }
          }
        }
      } else {
        numberOfParameters = 1;
        if (oldParameters != null) {
          param = oldParameters;
          if (oldParameters.hasNext()) {
            typechecker.addBinding(parameter instanceof Concrete.NameParameter ? ((Concrete.NameParameter) parameter).getReferable() : null, oldParameters);
            oldParameters = oldParameters.getNext();
          } else {
            oldParametersOK = false;
          }
        } else {
          Referable ref = parameter.getReferableList().get(0);
          param = paramResult == null ? null : parameter(parameter.isExplicit(), isProperty, Collections.singletonList(ref == null ? null : ref.getRefName()), paramResult);
          if (param != null) {
            typechecker.addBinding(ref, param);
          }
        }
      }
      if (!oldParametersOK) {
        errorReporter.report(new TypecheckingError("Cannot typecheck definition. Try to clear cache", parameter));
        return null;
      }

      if (resultType != null && skip == 0 && param != null) {
        for (DependentLink link = param; link.hasNext(); link = link.getNext()) {
          if (!(resultType instanceof PiExpression piExpr)) {
            if (!resultType.reportIfError(errorReporter, parameter)) {
              errorReporter.report(new FieldTypeParameterError(typechecker.getExpressionPrettifier(), fieldType, parameter));
              resultType = new ErrorExpression();
            }
            break;
          }

          substitution.add(piExpr.getParameters(), new ReferenceExpression(param));
          if (piExpr.getParameters().getNext().hasNext()) {
            resultType = new PiExpression(piExpr.getResultSort(), piExpr.getParameters().getNext(), piExpr.getCodomain());
          } else {
            resultType = piExpr.getCodomain().normalize(NormalizationMode.WHNF).getUnderlyingExpression();
          }
        }
      }

      if (localInstancePool != null && paramResult instanceof ClassCallExpression && param != null) {
        ClassDefinition classDef = ((ClassCallExpression) paramResult).getDefinition();
        if (!classDef.isRecord()) {
          ClassField classifyingField = classDef.getClassifyingField();
          int i = 0;
          for (DependentLink link = param; i < numberOfParameters; link = link.getNext(), i++) {
            ReferenceExpression reference = new ReferenceExpression(link);
            if (classifyingField == null) {
              localInstancePool.addLocalInstance(null, classDef, reference);
            } else {
              localInstancePool.addLocalInstance(FieldCallExpression.make(classifyingField, reference), classDef, reference);
            }
          }
        }

        if (first && def instanceof Concrete.Definition && ((Concrete.Definition) def).enclosingClass != null) {
          addEnclosingClassInstances((Concrete.Definition) def, param, localInstancePool);
        }
      }

      if (param != null) {
        if (oldParameters == null) {
          list.append(param);
        }

        if (first && myNewDef && typedDef != null) {
          typedDef.setParameters(param);
        }
      }

      first = false;
      if (skip > 0) skip--;
    }

    return new Pair<>(sort, resultType == null ? null : resultType.subst(substitution));
  }