private boolean checkElimPattern()

in base/src/main/java/org/arend/typechecking/doubleChecker/CoreExpressionChecker.java [603:729]
116 lines of code
50 McCabe index (conditional complexity)

  private boolean checkElimPattern(Expression type, Pattern pattern, List<Binding> newBindings, ExprSubstitution idpSubst, ExprSubstitution patternSubst, ExprSubstitution reversePatternSubst, Expression errorExpr) {
    if (pattern instanceof BindingPattern) {
      Expression actualType = pattern.getFirstBinding().getTypeExpr();
      if (pattern.getFirstBinding() instanceof TypedDependentLink) {
        actualType.accept(this, Type.OMEGA);
      }
      Binding newBinding = new TypedBinding(pattern.getFirstBinding().getName(), type);
      newBindings.add(newBinding);
      patternSubst.add(pattern.getFirstBinding(), new ReferenceExpression(newBinding));
      reversePatternSubst.add(newBinding, new ReferenceExpression(pattern.getFirstBinding()));
      addBinding(pattern.getFirstBinding(), errorExpr);
      return true;
    }

    if (pattern instanceof ConstructorPattern && pattern.getDefinition() == Prelude.IDP) {
      FunCallExpression equality = type.toEquality();
      if (equality == null || !(type instanceof DataCallExpression)) {
        throw new CoreException(CoreErrorWrapper.make(new TypeMismatchError(type, DocFactory.text("_ = _"), mySourceNode), errorExpr));
      }
      Expression left = equality.getDefCallArguments().get(1).subst(patternSubst).normalize(NormalizationMode.WHNF).subst(patternSubst);
      Expression right = equality.getDefCallArguments().get(2).subst(patternSubst).normalize(NormalizationMode.WHNF).subst(patternSubst);
      ReferenceExpression refExprLeft = left.cast(ReferenceExpression.class);
      ReferenceExpression refExprRight = right.cast(ReferenceExpression.class);
      Binding refLeft = refExprLeft == null ? null : refExprLeft.getBinding();
      Binding refRight = refExprRight == null ? null : refExprRight.getBinding();
      if (refLeft == null && refRight == null) {
        throw new CoreException(CoreErrorWrapper.make(new IdpPatternError(null, IdpPatternError.noVariable(), (DataCallExpression) type, mySourceNode), errorExpr));
      }

      Binding var = null;
      for (Binding binding : newBindings) {
        if (binding == refLeft) {
          var = binding;
        } else if (binding == refRight) {
          var = binding;
        }
      }
      if (var == null) {
        throw new CoreException(CoreErrorWrapper.make(new IdpPatternError(null, IdpPatternError.noParameter(), (DataCallExpression) type, mySourceNode), errorExpr));
      }
      Expression otherExpr = ElimBindingVisitor.elimBinding(var == refLeft ? right : left, var);
      if (otherExpr == null) {
        throw new CoreException(CoreErrorWrapper.make(new IdpPatternError(null, IdpPatternError.variable(var.getName()), (DataCallExpression) type, mySourceNode), errorExpr));
      }

      Set<Binding> freeVars = FreeVariablesCollector.getFreeVariables(otherExpr);
      Binding banVar = null;
      for (int i = newBindings.size() - 1; i >= 0; i--) {
        Binding binding = newBindings.get(i);
        if (binding == var) {
          break;
        }
        if (freeVars.contains(binding)) {
          banVar = binding;
        }
        if (banVar != null && binding.getTypeExpr().findBinding(var)) {
          throw new CoreException(CoreErrorWrapper.make(new IdpPatternError(null, IdpPatternError.subst(var.getName(), binding.getName(), banVar.getName()), null, mySourceNode), errorExpr));
        }
      }

      var = ((ReferenceExpression) reversePatternSubst.get(var)).getBinding();
      if (myContext != null) myContext.remove(var);
      idpSubst.add(var, otherExpr.subst(reversePatternSubst));
      return true;
    }

    if (pattern instanceof ConstructorPattern && pattern.getConstructor() == null) {
      if (type instanceof SigmaExpression) {
        return checkElimPatterns(((SigmaExpression) type).getParameters(), pattern.getSubPatterns(), new ExprSubstitution(), newBindings, idpSubst, patternSubst, reversePatternSubst, errorExpr, null);
      } else if (type instanceof ClassCallExpression) {
        return checkElimPatterns(((ClassCallExpression) type).getClassFieldParameters(), pattern.getSubPatterns(), new ExprSubstitution(), newBindings, idpSubst, patternSubst, reversePatternSubst, errorExpr, null);
      } else {
        throw new CoreException(CoreErrorWrapper.make(new TypeMismatchError(DocFactory.text("a sigma type or a class call"), type, mySourceNode), errorExpr));
      }
    }

    if (pattern instanceof ConstructorPattern && pattern.getConstructor() instanceof DConstructor constructor) {
      if (constructor != Prelude.EMPTY_ARRAY && constructor != Prelude.ARRAY_CONS) {
        throw new CoreException(CoreErrorWrapper.make(new TypecheckingError("Expected either '" + Prelude.EMPTY_ARRAY.getName() + "' or '" + Prelude.ARRAY_CONS.getName() + "'", mySourceNode), errorExpr));
      }
      if (!(type instanceof ClassCallExpression classCall && classCall.getDefinition() == Prelude.DEP_ARRAY)) {
        throw new CoreException(CoreErrorWrapper.make(new TypeMismatchError(new ClassCallExpression(Prelude.DEP_ARRAY, LevelPair.STD), type, mySourceNode), errorExpr));
      }
      Expression length = classCall.getAbsImplementationHere(Prelude.ARRAY_LENGTH);
      if (length != null) length = length.normalize(NormalizationMode.WHNF);
      if (length != null && !(length instanceof IntegerExpression || length instanceof ConCallExpression && ((ConCallExpression) length).getDefinition() == Prelude.SUC)) {
        throw new CoreException(CoreErrorWrapper.make(new ImpossibleEliminationError(classCall, mySourceNode), errorExpr));
      }
      Boolean isEmpty = length == null ? null : length instanceof IntegerExpression && ((IntegerExpression) length).isZero();
      if (isEmpty != null && isEmpty != (constructor == Prelude.EMPTY_ARRAY)) {
        throw new CoreException(CoreErrorWrapper.make(new TypeMismatchError(DocFactory.text(Prelude.DEP_ARRAY.getName() + " " + (isEmpty ? "0" : "(" + Prelude.SUC + " _)")), type, mySourceNode), errorExpr));
      }
      return checkElimPatterns(constructor.getArrayParameters(classCall), pattern.getSubPatterns(), new ExprSubstitution(), newBindings, idpSubst, patternSubst, reversePatternSubst, errorExpr, null);
    }

    if (!(type instanceof DataCallExpression dataCall)) {
      throw new CoreException(CoreErrorWrapper.make(new TypeMismatchError(DocFactory.text("a data type"), type, mySourceNode), errorExpr));
    }

    if (pattern instanceof EmptyPattern) {
      List<ConCallExpression> conCalls = dataCall.getMatchedConstructors();
      if (conCalls == null) {
        throw new CoreException(CoreErrorWrapper.make(new ImpossibleEliminationError(dataCall, mySourceNode, null, null, null, null, null), errorExpr));
      }
      if (!conCalls.isEmpty()) {
        throw new CoreException(CoreErrorWrapper.make(new DataTypeNotEmptyError(dataCall, DataTypeNotEmptyError.getConstructors(conCalls), mySourceNode), errorExpr));
      }
      return false;
    }

    assert pattern instanceof ConstructorPattern;
    var conPattern = (ConstructorPattern<?>) pattern;
    if (!(conPattern.getDefinition() instanceof Constructor)) {
      throw new CoreException(CoreErrorWrapper.make(new TypecheckingError("Expected a constructor", mySourceNode), errorExpr));
    }

    List<ConCallExpression> conCalls = new ArrayList<>(1);
    if (!dataCall.getMatchedConCall((Constructor) conPattern.getDefinition(), conCalls)) {
      throw new CoreException(CoreErrorWrapper.make(new ImpossibleEliminationError(dataCall, mySourceNode, null, null, null, null, null), errorExpr));
    }
    if (conCalls.isEmpty()) {
      throw new CoreException(CoreErrorWrapper.make(new DataTypeNotEmptyError(dataCall, DataTypeNotEmptyError.getConstructors(conCalls), mySourceNode), errorExpr));
    }

    ConCallExpression conCall = conCalls.get(0);
    return checkElimPatterns(DependentLink.Helper.subst(conCall.getDefinition().getParameters(), new ExprSubstitution().add(conCall.getDefinition().getDataTypeParameters(), conCall.getDataTypeArguments())), pattern.getSubPatterns(), new ExprSubstitution(), newBindings, idpSubst, patternSubst, reversePatternSubst, errorExpr, null);
  }