private Spec getSpec()

in meta/src/main/java/org/arend/lib/meta/SimpCoeMeta.java [329:468]
123 lines of code
50 McCabe index (conditional complexity)

  private Spec getSpec(CoreExpression arg, ExpressionTypechecker typechecker, ConcreteSourceNode marker, ConcreteFactory factory, List<CoreExpression> args, CoreClassField field, int proj, ConcreteExpression concreteArg, TypedExpression simpCoeArg, List<ConcreteArgument> excessiveArgs, boolean isForward) {
    arg = arg.normalize(NormalizationMode.WHNF);
    if (!(arg instanceof CoreLamExpression lam) || lam.getParameters().getNext().hasNext()) {
      return null;
    }

    CoreExpression body = lam.getBody().getUnderlyingExpression();
    if (body instanceof CoreFunCallExpression && ((CoreFunCallExpression) body).getDefinition() == ext.prelude.getEquality()) {
      return new EqualitySpec(lam.getParameters(), (CoreFunCallExpression) body, typechecker, marker, concreteArg, simpCoeArg, isForward);
    }

    body = body.normalize(NormalizationMode.WHNF);

    if (!args.isEmpty() && !(body instanceof CorePiExpression)) {
      return null;
    }

    if (body instanceof CorePiExpression) {
      if (args.isEmpty()) {
        List<ConcreteLetClause> letClauses = new ArrayList<>();
        PiTreeMaker piTreeMaker = new PiTreeMaker(ext, typechecker, factory, letClauses);
        PiTreeRoot piTree = piTreeMaker.make(body, Collections.singletonList(lam.getParameters()));
        return piTree.subtrees.isEmpty() ? null : new PiSpec(piTreeMaker, piTree, letClauses, concreteArg, simpCoeArg, excessiveArgs, isForward);
      } else {
        int s = 0;
        List<CoreParameter> parameters = new ArrayList<>();
        while (true) {
          CoreParameter param = ((CorePiExpression) body).getParameters();
          if (param.getTypeExpr().findFreeBinding(lam.getParameters().getBinding())) {
            return null;
          }

          int n = 0;
          for (; param.hasNext() && s < args.size(); param = param.getNext(), n++, s++) {
            parameters.add(param);
          }
          if (s == args.size()) {
            body = param.hasNext() ? ((CorePiExpression) body).dropParameters(n) : ((CorePiExpression) body).getCodomain();
            break;
          }
          body = ((CorePiExpression) body).getCodomain();
        }

        return new PiArgsSpec(args, lam, parameters, body, concreteArg, isForward);
      }
    }

    if (body instanceof CoreSigmaExpression || body instanceof CoreClassCallExpression) {
      CoreParameter parameters = body instanceof CoreSigmaExpression ? ((CoreSigmaExpression) body).getParameters() : ((CoreClassCallExpression) body).getClassFieldParameters();
      List<CoreClassField> classFields = body instanceof CoreClassCallExpression ? Utils.getNotImplementedField((CoreClassCallExpression) body) : null;
      if (proj == -1 && field == null) {
        List<CoreExpression> sigmaParamTypes = new ArrayList<>();
        List<Integer> indices = classFields == null ? new ArrayList<>() : null;
        Set<CoreBinding> bindings = new HashSet<>();
        int i = 0;
        for (CoreParameter param = parameters; param.hasNext(); param = param.getNext(), i++) {
          CoreExpression paramType = param.getTypeExpr();
          if (!(classFields != null && classFields.get(i).isProperty() || Utils.isProp(paramType))) {
            if (paramType.findFreeBindings(bindings) != null) {
              return null;
            }
            sigmaParamTypes.add(paramType);
            if (classFields == null) indices.add(i);
          } else if (classFields != null) {
            classFields.remove(i--);
          }
          bindings.add(param.getBinding());
        }

        if (classFields != null && concreteArg instanceof ConcreteClassExtExpression classExt) {
          ConcreteExpression baseExpr = classExt.getBaseClassExpression();
          CoreDefinition def = baseExpr instanceof ConcreteReferenceExpression ? ext.definitionProvider.getCoreDefinition(((ConcreteReferenceExpression) baseExpr).getReferent()) : null;
          CoreClassDefinition classDef = ((CoreClassCallExpression) body).getDefinition();
          if (!(def instanceof CoreClassDefinition && ((CoreClassDefinition) def).isSubClassOf(classDef))) {
            typechecker.getErrorReporter().report(new SubclassError(true, classDef.getRef(), baseExpr));
            return new ErrorSpec();
          }

          Map<ArendRef, ConcreteCoclause> implMap = new HashMap<>();
          for (ConcreteCoclause coclause : classExt.getCoclauses().getCoclauseList()) {
            if (coclause.getImplementation() == null) {
              typechecker.getErrorReporter().report(new TypecheckingError("Implementation is missing", coclause));
              return new ErrorSpec();
            }

            if (implMap.putIfAbsent(coclause.getImplementedRef(), coclause) != null) {
              typechecker.getErrorReporter().report(new RedundantCoclauseError(coclause));
            }
          }

          List<ConcreteExpression> tupleFields = new ArrayList<>(classFields.size());
          List<ArendRef> notImplemented = new ArrayList<>();
          for (CoreClassField classField : classFields) {
            ConcreteCoclause coclause = implMap.remove(classField.getRef());
            if (coclause != null) {
              tupleFields.add(coclause.getImplementation());
            } else {
              notImplemented.add(classField.getRef());
            }
          }

          for (ConcreteCoclause coclause : implMap.values()) {
            typechecker.getErrorReporter().report(new RedundantCoclauseError(coclause));
          }

          if (!notImplemented.isEmpty()) {
            typechecker.getErrorReporter().report(new FieldsImplementationError(false, classDef.getRef(), notImplemented, classExt.getCoclauses()));
            return new ErrorSpec();
          }

          concreteArg = tupleFields.size() == 1 ? tupleFields.get(0) : factory.withData(classExt.getData()).tuple(tupleFields);
        }

        return new SigmaSpec(lam, sigmaParamTypes, classFields, indices, concreteArg, isForward);
      } else {
        int i = 0;
        Set<CoreBinding> bindings = new HashSet<>();
        CoreExpression parameterType = null;
        for (CoreParameter param = parameters; param.hasNext(); param = param.getNext(), i++) {
          bindings.add(param.getBinding());
          if (i == proj || classFields != null && classFields.get(i) == field) {
            CoreExpression paramType = param.getTypeExpr();
            if (paramType.findFreeBindings(bindings) != null) {
              return null;
            }
            parameterType = paramType;
            break;
          }
        }
        return parameterType == null ? null : new SigmaProjSpec(lam, proj, field, parameterType, concreteArg, isForward);
      }
    }

    CoreFunCallExpression equality = body.toEquality();
    if (equality != null ) {
      return new EqualitySpec(lam.getParameters(), equality, typechecker, marker, concreteArg, simpCoeArg, isForward);
    }

    return null;
  }