private boolean typecheckClause()

in base/src/main/java/org/arend/typechecking/patternmatching/PatternTypechecking.java [143:297]
137 lines of code
36 McCabe index (conditional complexity)

  private boolean typecheckClause(Concrete.FunctionClause clause, List<? extends Concrete.Parameter> abstractParameters, DependentLink parameters, Expression expectedType, List<ExtElimClause> resultClauses, FunctionDefinition definition) {
    assert myVisitor != null;
    try (var ignored = new Utils.RefContextSaver(myVisitor.getContext(), myVisitor.getLocalExpressionPrettifier())) {
      // Typecheck patterns
      myPathPatterns.clear();
      ExprSubstitution substitution = new ExprSubstitution();
      ExprSubstitution totalSubst = new ExprSubstitution();
      Result result = typecheckPatterns(clause.getPatterns(), abstractParameters, parameters, substitution, totalSubst, clause);
      if (result == null) {
        return false;
      }

      ExtElimClause elimClause = new ExtElimClause(result.patterns, null, totalSubst);

      // If we have the absurd pattern, then RHS is ignored
      if (result.hasEmptyPattern()) {
        if (clause.getExpression() != null) {
          myErrorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.BODY_IGNORED, clause.getExpression()));
        }
        resultClauses.add(elimClause);
        return true;
      } else {
        if (clause.getExpression() == null) {
          myErrorReporter.report(new TypecheckingError("Required a body", clause));
          return false;
        }
      }

      for (Map.Entry<Referable, Binding> entry : myContext.entrySet()) {
        Binding binding = entry.getValue();
        Expression expr = substitution.get(binding);
        Binding newBinding = expr instanceof ReferenceExpression
          ? ((ReferenceExpression) expr).getBinding()
          : expr != null
            ? new TypedEvaluatingBinding(binding.getName(), expr, binding.getTypeExpr())
            : null;
        if (newBinding != null) {
          entry.setValue(newBinding);
        }
      }
      expectedType = expectedType.subst(substitution);

      GlobalInstancePool globalInstancePool = myVisitor.getInstancePool();
      LocalInstancePool instancePool = globalInstancePool == null ? null : globalInstancePool.getLocalInstancePool();
      if (instancePool != null) {
        globalInstancePool.setInstancePool(instancePool.subst(substitution));
      }

      TypecheckingResult tcResult;
      try {
        List<Binding> intervalBindings;
        Expression exprType = expectedType;
        if (!myPathPatterns.isEmpty()) {
          Body body = new ElimTypechecking(null, null, null, myMode, null, Level.INFINITY, false, null, 0, null).typecheckElim(resultClauses, parameters, myElimParams);
          if (body == null) {
            myErrorReporter.report(new TypecheckingError("Cannot compute body", clause));
            return false;
          }
          if (!(body instanceof ElimBody)) {
            myErrorReporter.report(new TypecheckingError("Incorrect body", clause));
            return false;
          }
          Sort sort = expectedType.getSortOfType();
          if (sort == null) {
            myErrorReporter.report(new TypecheckingError("Cannot infer the sort of the type", clause));
            return false;
          }

          if (definition != null) definition.setBody(body);
          intervalBindings = new ArrayList<>();
          getIntervalBindings(result.patterns, 0, intervalBindings);

          List<TypedSingleDependentLink> lamBindings = new ArrayList<>(intervalBindings.size());
          ExprSubstitution intervalSubst = new ExprSubstitution();
          for (Binding binding : intervalBindings) {
            TypedSingleDependentLink link = new TypedSingleDependentLink(true, binding.getName(), binding.getType());
            lamBindings.add(link);
            intervalSubst.add(binding, new ReferenceExpression(link));
          }

          LevelPair levels = new LevelPair(sort.getPLevel(), sort.getHLevel());
          Sort hSort = new Sort(sort.getPLevel(), Level.INFINITY);
          exprType = expectedType.subst(intervalSubst);
          List<Expression> exprTypes = new ArrayList<>(intervalBindings.size());
          List<Expression> args = ExpressionPattern.toExpressions(result.patterns);
          for (int i = intervalBindings.size() - 1; i >= 0; i--) {
            exprTypes.add(exprType);
            Binding intervalBinding = intervalBindings.get(i);

            intervalSubst.add(intervalBinding, Left());
            Expression leftArg = evalBody(intervalSubst, (ElimBody) body, args);
            if (leftArg == null && definition != null) {
              leftArg = makeFunCall(definition, args, intervalSubst, clause);
            }

            intervalSubst.add(intervalBinding, Right());
            Expression rightArg = evalBody(intervalSubst, (ElimBody) body, args);
            if (rightArg == null && definition != null) {
              rightArg = makeFunCall(definition, args, intervalSubst, clause);
            }

            if (leftArg == null || rightArg == null) {
              myErrorReporter.report(new TypecheckingError("Cannot evaluate conditions", clause));
              return false;
            }

            if (definition != null) {
              leftArg = normalizeRecursiveCalls(leftArg, definition);
              rightArg = normalizeRecursiveCalls(rightArg, definition);
            }

            for (int j = intervalBindings.size() - 1, k = 0; j > i; j--, k++) {
              leftArg = new PathExpression(levels, new LamExpression(hSort, lamBindings.get(j), exprTypes.get(k).subst(lamBindings.get(i), Left())), new LamExpression(hSort, lamBindings.get(j), leftArg));
              rightArg = new PathExpression(levels, new LamExpression(hSort, lamBindings.get(j), exprTypes.get(k).subst(lamBindings.get(i), Right())), new LamExpression(hSort, lamBindings.get(j), rightArg));
            }

            intervalSubst.add(intervalBinding, new ReferenceExpression(lamBindings.get(i)));
            exprType = DataCallExpression.make(Prelude.PATH, levels, Arrays.asList(new LamExpression(hSort, lamBindings.get(i), exprType), leftArg, rightArg));
          }
        } else {
          intervalBindings = null;
        }

        // Typecheck the RHS
        tcResult = myVisitor.checkExpr(clause.getExpression(), exprType);
        if (intervalBindings != null && tcResult != null) {
          ErrorExpression errorExpr = tcResult.expression.cast(ErrorExpression.class);
          if (!(errorExpr != null && errorExpr.isGoal())) {
            Expression resultExpr = tcResult.expression;
            for (Binding binding : intervalBindings) {
              resultExpr = AtExpression.make(resultExpr, new ReferenceExpression(binding), false);
            }
            tcResult = new TypecheckingResult(resultExpr, expectedType);
          }
          if (errorExpr instanceof GoalErrorExpression) {
            ((GoalErrorExpression) errorExpr).goalError.removeConditions();
          }
        }
        if (myFinal) {
          tcResult = myVisitor.finalize(tcResult, clause.getExpression(), false);
        }
      } finally {
        if (definition != null) definition.setBody(null);
      }
      if (instancePool != null) {
        globalInstancePool.setInstancePool(instancePool);
      }
      if (tcResult == null) {
        return false;
      }
      elimClause.setExpression(tcResult.expression);
      resultClauses.add(elimClause);
      return true;
    }
  }