in base/src/main/java/org/arend/core/expr/visitor/NormalizeVisitor.java [513:671]
public Expression eval(ElimBody elimBody, List<? extends Expression> arguments, ExprSubstitution substitution, LevelSubstitution levelSubstitution, Expression origExpr, NormalizationMode mode, boolean shouldProgress) {
Deque<Expression> stack = makeStack(arguments);
List<Expression> argList = new ArrayList<>();
Expression result = null;
List<Expression> conArgs = null;
int recursiveParam = -1;
int sucs = 0;
Expression resultExpr = origExpr;
ElimTree elimTree = elimBody.getElimTree();
while (true) {
for (int i = 0; i < elimTree.getSkip(); i++) {
argList.add(stack.pop());
}
if (elimTree instanceof LeafElimTree leafElimTree) {
ElimClause<Pattern> clause = elimBody.getClauses().get(leafElimTree.getClauseIndex());
int i = 0;
for (DependentLink link = clause.getParameters(); link.hasNext(); link = link.getNext(), i++) {
substitution.add(link, argList.get(leafElimTree.getArgumentIndex(i)));
}
resultExpr = Objects.requireNonNull(clause.getExpression());
if (mode == null) {
return resultExpr.subst(substitution, levelSubstitution);
}
while (true) {
if (mode != NormalizationMode.RNF && resultExpr instanceof LetExpression let) {
if (let.isStrict()) {
for (HaveClause letClause : let.getClauses()) {
substitution.add(letClause, LetExpression.normalizeClauseExpression(letClause.getPattern(), letClause.getExpression().subst(substitution, levelSubstitution), NormalizationMode.ENF));
}
} else {
for (HaveClause letClause : let.getClauses()) {
substitution.add(letClause, letClause instanceof LetClause
? new ReferenceExpression(LetClause.make(true, letClause.getName(), letClause.getPattern(), letClause.getExpression().subst(substitution, levelSubstitution)))
: LetExpression.normalizeClauseExpression(letClause.getPattern(), letClause.getExpression().subst(substitution, levelSubstitution)));
}
}
resultExpr = let.getExpression();
} else if (mode != NormalizationMode.WHNF && resultExpr instanceof ConCallExpression conCall) {
if (conCall.getDefinition() == Prelude.SUC) {
sucs++;
resultExpr = conCall.getDefCallArguments().get(0);
} else if (conCall.getDefinition().getRecursiveParameter() >= 0) {
int recParam = conCall.getDefinition().getRecursiveParameter();
List<Expression> newDataTypeArgs;
List<Expression> newConArgs;
if (substitution.isEmpty() && levelSubstitution.isEmpty()) {
newDataTypeArgs = conCall.getDataTypeArguments();
newConArgs = new ArrayList<>(conCall.getDefCallArguments());
} else {
newDataTypeArgs = new ArrayList<>(conCall.getDataTypeArguments().size());
for (Expression arg : conCall.getDataTypeArguments()) {
newDataTypeArgs.add(arg.subst(substitution, levelSubstitution));
}
newConArgs = new ArrayList<>(conCall.getDefCallArguments().size());
for (int j = 0; j < conCall.getDefCallArguments().size(); j++) {
if (j != recParam) {
newConArgs.add(conCall.getDefCallArguments().get(j).subst(substitution, levelSubstitution));
} else {
newConArgs.add(conCall.getDefCallArguments().get(j));
}
}
}
Expression newExpr = ConCallExpression.make(conCall.getDefinition(), conCall.getLevels().subst(levelSubstitution), newDataTypeArgs, newConArgs);
if (conArgs == null) {
result = newExpr;
} else {
conArgs.set(recursiveParam, newExpr);
}
conArgs = newConArgs;
recursiveParam = recParam;
resultExpr = conArgs.get(recursiveParam);
} else {
break;
}
} else if (resultExpr instanceof FunCallExpression funCall && funCall.getDefinition().getBody() instanceof Expression) {
resultExpr = Objects.requireNonNull((Expression) funCall.getDefinition().getBody()).subst(addArguments(new ExprSubstitution(), funCall.getDefCallArguments(), funCall.getDefinition()), funCall.getLevelSubstitution());
} else if (resultExpr instanceof ReferenceExpression && ((ReferenceExpression) resultExpr).getBinding() instanceof EvaluatingBinding) {
resultExpr = ((EvaluatingBinding) ((ReferenceExpression) resultExpr).getBinding()).getExpression();
} else if (resultExpr instanceof SubstExpression) {
Expression expr = ((SubstExpression) resultExpr).eval();
if (resultExpr == expr) {
break;
}
resultExpr = expr;
} else if (resultExpr instanceof ReferenceExpression) {
Binding binding = ((ReferenceExpression) resultExpr).getBinding();
Expression expr = substitution.get(binding);
if (!substitution.isEmpty()) {
substitution = new ExprSubstitution();
}
levelSubstitution = LevelSubstitution.EMPTY;
if (expr != null) {
resultExpr = expr;
} else {
break;
}
} else {
break;
}
}
if (resultExpr instanceof FunCallExpression && ((FunCallExpression) resultExpr).getDefinition().getBody() instanceof ElimBody && !isBlocked(((FunCallExpression) resultExpr).getDefinition()) || resultExpr instanceof CaseExpression && !((CaseExpression) resultExpr).isSCase()) {
FunCallExpression funCall = resultExpr instanceof FunCallExpression ? (FunCallExpression) resultExpr : null;
elimBody = funCall != null ? (ElimBody) funCall.getDefinition().getBody() : ((CaseExpression) resultExpr).getElimBody();
assert elimBody != null;
elimTree = elimBody.getElimTree();
argList.clear();
stack.clear();
ComputationRunner.checkCanceled();
List<? extends Expression> args = funCall != null ? funCall.getDefCallArguments() : ((CaseExpression) resultExpr).getArguments();
for (int j = args.size() - 1; j >= 0; j--) {
stack.push(resultExpr instanceof CaseExpression ? args.get(j).subst(substitution, levelSubstitution) : funCall.getDefinition().isStrict(j) ? args.get(j).subst(substitution, levelSubstitution).accept(this, NormalizationMode.ENF) : SubstExpression.make(args.get(j), substitution, levelSubstitution));
}
resultExpr = SubstExpression.make(resultExpr, substitution, levelSubstitution);
if (funCall != null) {
substitution = new ExprSubstitution();
levelSubstitution = funCall.getLevelSubstitution().subst(levelSubstitution);
}
continue;
}
resultExpr = resultExpr.subst(substitution, levelSubstitution);
if (result == null) {
result = resultExpr;
} else {
conArgs.set(recursiveParam, resultExpr);
}
return result == null ? null : addSucs(result, sucs).accept(this, mode);
}
elimTree = updateStack(stack, argList, (BranchElimTree) elimTree);
if (elimTree == null) {
if (resultExpr instanceof SubstExpression) {
resultExpr = ((SubstExpression) resultExpr).eval();
}
if (shouldProgress && resultExpr == origExpr) {
return null;
}
if (mode == NormalizationMode.WHNF && resultExpr instanceof FunCallExpression funCall && funCall.getDefinition().getBody() instanceof ElimBody) {
List<Expression> newArgs = ((ElimBody) Objects.requireNonNull(funCall.getDefinition().getBody())).getElimTree().normalizeArguments(funCall.getDefCallArguments());
resultExpr = FunCallExpression.make(funCall.getDefinition(), funCall.getLevels(), newArgs);
}
if (result == null) {
result = resultExpr;
} else {
conArgs.set(recursiveParam, resultExpr);
}
result = addSucs(result, sucs);
return mode == NormalizationMode.WHNF || mode == null || !(result instanceof DefCallExpression) ? (result != null && mode != NormalizationMode.WHNF && mode != null ? result.accept(this, mode) : result) : applyDefCall((DefCallExpression) result, mode);
}
}
}