private ConcreteExpression proveProp()

in meta/src/main/java/org/arend/lib/level/StdLevelProver.java [47:80]
28 lines of code
13 McCabe index (conditional complexity)

  private ConcreteExpression proveProp(CoreExpression expression, ConcreteReferenceExpression leftExpr, ConcreteReferenceExpression rightExpr, ConcreteSourceNode marker, ConcreteFactory factory, ExpressionTypechecker typechecker) {
    CoreExpression type = expression.normalize(NormalizationMode.WHNF);
    CoreExpression typeType = type.computeType().normalize(NormalizationMode.WHNF);
    if (typeType instanceof CoreUniverseExpression && ((CoreUniverseExpression) typeType).getSort().isProp()) {
      return factory.app(factory.ref(ext.propIsProp.getRef()), true, Arrays.asList(leftExpr, rightExpr));
    }

    if (type instanceof CoreDataCallExpression) {
      ConcreteExpression result = provePropDataType((CoreDataCallExpression) type, leftExpr, rightExpr, marker, factory);
      if (result != null) {
        return result;
      }
    }

    for (CoreBinding binding : typechecker.getFreeBindingsList()) {
      List<CoreParameter> parameters = new ArrayList<>();
      CoreExpression codomain = binding.getTypeExpr().getPiParameters(parameters);
      if (parameters.size() != 2) {
        continue;
      }

      CoreFunCallExpression equality = codomain.toEquality();
      if (equality != null) {
        List<? extends CoreExpression> args = equality.getDefCallArguments();
        if (args.get(1) instanceof CoreReferenceExpression && args.get(2) instanceof CoreReferenceExpression && ((CoreReferenceExpression) args.get(1)).getBinding() == parameters.get(0).getBinding() && ((CoreReferenceExpression) args.get(2)).getBinding() == parameters.get(1).getBinding() && typechecker.compare(args.get(0), type, CMP.EQ, marker, false, true, false)) {
          return factory.app(factory.ref(binding), true, Arrays.asList(leftExpr, rightExpr));
        }
      }
    }

    // TODO: Sigma types, pi types, equality (i.e., rising level), heterogeneous path types, recursive data types, dependently typed constructors

    return ext.contradictionMeta.check(null, null, true, marker, typechecker);
  }