public static RingKind getTermCompilerKind()

in meta/src/main/java/org/arend/lib/meta/solver/BaseTermCompiler.java [80:96]

• 17 lines of code
• 11 McCabe index (conditional complexity)

  public static RingKind getTermCompilerKind(CoreExpression instance, EquationMeta meta) {
    CoreExpression instanceNorm = instance.normalize(NormalizationMode.WHNF);
    CoreFunctionDefinition instanceDef = instanceNorm instanceof CoreFunCallExpression ? ((CoreFunCallExpression) instanceNorm).getDefinition() : null;
    RingKind kind = instanceDef == meta.NatSemiring ? RingKind.NAT : instanceDef == meta.IntRing ? RingKind.INT : instanceDef == meta.RatField ? RingKind.RAT : RingKind.NONE;
    if (kind != RingKind.NONE) return kind;
    CoreExpression type = instanceNorm.computeType().normalize(NormalizationMode.WHNF);
    if (type instanceof CoreClassCallExpression classCall && classCall.getDefinition().isSubClassOf(meta.ext.linearSolverMeta.OrderedAAlgebra)) {
      CoreExpression ringImpl = classCall.getAbsImplementationHere(meta.ext.linearSolverMeta.moduleRing);
      if (ringImpl != null) {
        ringImpl = ringImpl.normalize(NormalizationMode.WHNF);
        if (ringImpl instanceof CoreFunCallExpression funCall && funCall.getDefinition() == meta.RatField) {
          return RingKind.RAT_ALG;
        }
      }
    }
    return RingKind.NONE;
  }