in base/src/main/java/org/arend/core/expr/visitor/NormalizeVisitor.java [217:393]
private Expression visitFunctionDefCall(LeveledDefCallExpression expr, NormalizationMode mode) {
Definition definition = expr.getDefinition();
if (definition == Prelude.COERCE || definition == Prelude.COERCE2) {
LamExpression lamExpr = expr.getDefCallArguments().get(0).accept(this, NormalizationMode.WHNF).cast(LamExpression.class);
if (lamExpr != null) {
SingleDependentLink param = lamExpr.getParameters();
Expression body = param.getNext().hasNext() ? new LamExpression(lamExpr.getResultSort(), param.getNext(), lamExpr.getBody()) : lamExpr.getBody();
body = body.accept(this, NormalizationMode.WHNF);
FunCallExpression funCall = body.cast(FunCallExpression.class);
boolean checkSigma = true;
if (funCall != null && funCall.getDefinition() == Prelude.ISO && definition == Prelude.COERCE) {
List<? extends Expression> isoArgs = funCall.getDefCallArguments();
ReferenceExpression refExpr = isoArgs.get(isoArgs.size() - 1).accept(this, NormalizationMode.WHNF).cast(ReferenceExpression.class);
if (refExpr != null && refExpr.getBinding() == param) {
checkSigma = false;
ConCallExpression normedPtCon = expr.getDefCallArguments().get(2).accept(this, NormalizationMode.WHNF).cast(ConCallExpression.class);
if (normedPtCon != null && normedPtCon.getDefinition() == Prelude.RIGHT) {
boolean noFreeVar = true;
for (int i = 0; i < isoArgs.size() - 1; i++) {
if (NormalizingFindBindingVisitor.findBinding(isoArgs.get(i), param)) {
noFreeVar = false;
break;
}
}
if (noFreeVar) {
return AppExpression.make(isoArgs.get(2), expr.getDefCallArguments().get(1), true).accept(this, mode);
}
/* Stricter version of iso
if (!NormalizingFindBindingVisitor.findBinding(isoArgs.get(0), param) && !NormalizingFindBindingVisitor.findBinding(isoArgs.get(1), param) && !NormalizingFindBindingVisitor.findBinding(isoArgs.get(2), param)) {
return AppExpression.make(isoArgs.get(2), expr.getDefCallArguments().get(1), true).accept(this, mode);
}
*/
}
}
}
if (checkSigma && !NormalizingFindBindingVisitor.findBinding(body, param)) {
return expr.getDefCallArguments().get(definition == Prelude.COERCE ? 1 : 2).accept(this, mode);
}
}
}
if (definition == Prelude.MINUS) {
return normalizeMinus((FunCallExpression) expr, mode);
}
if (definition == Prelude.PLUS) {
return normalizePlus((FunCallExpression) expr, mode);
}
List<? extends Expression> defCallArgs = expr.getDefCallArguments();
if (definition == Prelude.MUL || definition == Prelude.DIV_MOD || definition == Prelude.DIV || definition == Prelude.MOD) {
Expression arg2 = defCallArgs.get(1).accept(this, NormalizationMode.WHNF);
IntegerExpression intExpr2 = arg2.cast(IntegerExpression.class);
if (intExpr2 != null) {
if (intExpr2.isZero()) {
if (definition == Prelude.MUL) {
return intExpr2;
} else if (definition == Prelude.DIV_MOD) {
Expression result = defCallArgs.get(0).accept(this, mode);
List<Expression> list = new ArrayList<>(2);
list.add(result);
list.add(result);
return new TupleExpression(list, finDivModType(Suc(result)));
} else {
return defCallArgs.get(0).accept(this, mode);
}
}
if (intExpr2.isOne()) {
if (definition == Prelude.DIV) {
return defCallArgs.get(0).accept(this, mode);
}
if (definition == Prelude.MOD) {
return Zero();
}
if (definition == Prelude.DIV_MOD) {
List<Expression> list = new ArrayList<>(2);
list.add(defCallArgs.get(0).accept(this, mode));
list.add(Zero());
return new TupleExpression(list, ExpressionFactory.finDivModType(new SmallIntegerExpression(1)));
}
}
Expression arg1 = defCallArgs.get(0).accept(this, NormalizationMode.WHNF);
IntegerExpression intArg1 = arg1.cast(IntegerExpression.class);
if (intArg1 != null) {
if (definition == Prelude.MUL) {
return intArg1.mul(intExpr2);
}
if (definition == Prelude.DIV_MOD) {
return intArg1.divMod(intExpr2);
}
if (definition == Prelude.DIV) {
return intArg1.div(intExpr2);
}
if (definition == Prelude.MOD) {
return intArg1.mod(intExpr2);
}
throw new IllegalStateException();
}
List<Expression> newDefCallArgs = new ArrayList<>(2);
newDefCallArgs.add(arg1);
newDefCallArgs.add(arg2);
defCallArgs = newDefCallArgs;
} else {
Expression arg1 = defCallArgs.get(0);
if (definition == Prelude.DIV_MOD || definition == Prelude.DIV || definition == Prelude.MOD) {
arg1 = arg1.accept(this, mode);
if (arg1 instanceof IntegerExpression intExpr) {
if (intExpr.isZero()) {
return definition == Prelude.DIV_MOD ? new TupleExpression(Arrays.asList(arg1, arg1), finDivModType(new SmallIntegerExpression(1))) : arg1;
}
int n = 0;
Expression arg2_ = arg2;
while (arg2_ instanceof ConCallExpression conCall && conCall.getDefinition() == Prelude.SUC) {
n++;
arg2_ = conCall.getDefCallArguments().get(0).normalize(NormalizationMode.WHNF);
}
if (intExpr.compare(n) < 0) {
return definition == Prelude.DIV_MOD ? new TupleExpression(Arrays.asList(Zero(), intExpr), finDivModType(Suc(intExpr))) : definition == Prelude.DIV ? Zero() : intExpr;
}
}
}
List<Expression> newDefCallArgs = new ArrayList<>(2);
newDefCallArgs.add(arg1);
newDefCallArgs.add(arg2);
defCallArgs = newDefCallArgs;
}
}
if (definition == Prelude.ARRAY_INDEX) {
Expression arg = defCallArgs.get(0).normalize(NormalizationMode.WHNF);
if (arg instanceof ArrayExpression) {
Expression numExpr = defCallArgs.get(1).normalize(NormalizationMode.WHNF);
int n = 0;
while (numExpr instanceof ConCallExpression && ((ConCallExpression) numExpr).getDefinition() == Prelude.SUC) {
n++;
numExpr = ((ConCallExpression) numExpr).getDefCallArguments().get(0).normalize(NormalizationMode.WHNF);
}
BigInteger num = numExpr instanceof IntegerExpression ? ((IntegerExpression) numExpr).getBigInteger().add(BigInteger.valueOf(n)) : numExpr instanceof ConCallExpression && ((ConCallExpression) numExpr).getDefinition() == Prelude.ZERO ? BigInteger.valueOf(n) : null;
if (num != null || n > 0) {
ArrayExpression array = (ArrayExpression) arg;
BigInteger s = BigInteger.valueOf(array.getElements().size());
if (num != null && num.compareTo(s) < 0) {
return array.getElements().get(num.intValue()).accept(this, mode);
}
if (array.getTail() != null) {
if (num != null) {
return FunCallExpression.make(Prelude.ARRAY_INDEX, expr.getLevels(), Arrays.asList(array.getTail(), new BigIntegerExpression(num.subtract(s)))).accept(this, mode);
}
if (n < array.getElements().size()) {
return FunCallExpression.make(Prelude.ARRAY_INDEX, expr.getLevels(), Arrays.asList(array.drop(n), numExpr));
}
for (int i = array.getElements().size(); i < n; i++) {
numExpr = Suc(numExpr);
}
return FunCallExpression.make(Prelude.ARRAY_INDEX, expr.getLevels(), Arrays.asList(array.getTail(), numExpr)).accept(this, mode);
}
}
} else {
Expression type = arg.getType().normalize(NormalizationMode.WHNF);
if (type instanceof ClassCallExpression) {
Expression at = ((ClassCallExpression) type).getImplementationHere(Prelude.ARRAY_AT, arg);
if (at != null) {
return AppExpression.make(at, defCallArgs.get(1), true).accept(this, mode);
}
}
}
return applyDefCall(expr, mode);
}
Expression result = visitBody(((Function) definition).getBody(), defCallArgs, expr, mode);
return result == null ? applyDefCall(expr, mode) : result;
}