private ConcreteExpression provePropDataType()

in meta/src/main/java/org/arend/lib/level/StdLevelProver.java [82:159]
74 lines of code
21 McCabe index (conditional complexity)

  private ConcreteExpression provePropDataType(CoreDataCallExpression dataCall, ConcreteReferenceExpression leftExpr, ConcreteReferenceExpression rightExpr, ConcreteSourceNode marker, ConcreteFactory factory) {
    if (!dataCall.getDefinition().getRecursiveDefinitions().isEmpty()) {
      return null;
    }
    List<CoreDataCallExpression.ConstructorWithDataArguments> constructors = dataCall.computeMatchedConstructorsWithDataArguments();
    if (constructors == null) {
      return null;
    }
    for (CoreDataCallExpression.ConstructorWithDataArguments constructor : constructors) {
      if (!constructor.getParameters().hasNext() || !constructor.getParameters().getNext().hasNext()) {
        continue;
      }

      Set<CoreBinding> bindings = new HashSet<>();
      for (CoreParameter parameter = constructor.getParameters(); parameter.hasNext(); parameter = parameter.getNext()) {
        if (parameter.getTypeExpr().findFreeBindings(bindings) != null) {
          return null;
        }
        bindings.add(parameter.getBinding());
      }
    }

    List<ConcreteClause> clauses = new ArrayList<>();
    for (CoreDataCallExpression.ConstructorWithDataArguments con1 : constructors) {
      for (CoreDataCallExpression.ConstructorWithDataArguments con2 : constructors) {
        List<ConcretePattern> subPatterns1 = new ArrayList<>();
        List<ConcretePattern> subPatterns2 = new ArrayList<>();
        CoreDefinition def1 = con1.getConstructor();
        CoreDefinition def2 = con2.getConstructor();
        List<ArendRef> refs1 = def1 == def2 ? new ArrayList<>() : null;
        List<ArendRef> refs2 = def1 == def2 ? new ArrayList<>() : null;
        for (CoreParameter param = con1.getParameters(); param.hasNext(); param = param.getNext()) {
          ArendRef ref = factory.local(ext.renamerFactory.getNameFromBinding(param.getBinding(), null) + "1");
          subPatterns1.add(factory.refPattern(ref, null));
          if (refs1 != null) {
            refs1.add(ref);
          }
        }
        for (CoreParameter param = con2.getParameters(); param.hasNext(); param = param.getNext()) {
          ArendRef ref = factory.local(ext.renamerFactory.getNameFromBinding(param.getBinding(), null) + "2");
          subPatterns2.add(factory.refPattern(ref, null));
          if (refs2 != null) {
            refs2.add(ref);
          }
        }

        // We need a meta here because the context changes and we use it in both proveProp and ContradictionMeta.check
        clauses.add(factory.clause(Arrays.asList(factory.conPattern(def1.getRef(), subPatterns1), factory.conPattern(def2.getRef(), subPatterns2)), factory.meta("case_" + def1.getName() + "_" + def2.getName(), new MetaDefinition() {
          @Override
          public @Nullable TypedExpression invokeMeta(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) {
            ConcreteExpression result;
            if (def1 == def2) {
              CoreParameter conParam = con1.getParameters();
              if (conParam.hasNext()) {
                ArendRef iRef = factory.local("i");
                ConcreteExpression iExpr = factory.ref(iRef);
                List<ConcreteArgument> args = new ArrayList<>();
                for (int i = 0; conParam.hasNext(); conParam = conParam.getNext(), i++) {
                  ConcreteExpression expr = proveProp(conParam.getTypeExpr(), factory.ref(refs1.get(i)), factory.ref(refs2.get(i)), marker, factory, typechecker);
                  if (expr == null) {
                    return null;
                  }
                  args.add(factory.arg(factory.app(factory.ref(ext.prelude.getAtRef()), true, Arrays.asList(expr, iExpr)), conParam.isExplicit()));
                }
                result = factory.app(factory.ref(ext.prelude.getPathConRef()), true, Collections.singletonList(factory.lam(Collections.singletonList(factory.param(iRef)), factory.app(factory.ref(def1.getRef()), args))));
              } else {
                result = factory.ref(ext.prelude.getIdp().getRef());
              }
            } else {
              result = ext.contradictionMeta.check(null, null, true, marker, typechecker);
            }
            return result == null ? null : typechecker.typecheck(result, contextData.getExpectedType());
          }
        })));
      }
    }
    return factory.caseExpr(false, Arrays.asList(factory.caseArg(leftExpr, null), factory.caseArg(rightExpr, null)), factory.app(factory.ref(ext.prelude.getEquality().getRef()), true, Arrays.asList(leftExpr, rightExpr)), null, clauses);
  }