in base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java [3941:4121]
public TypecheckingResult visitCase(Concrete.CaseExpression expr, Expression expectedType) {
if (expectedType == null && expr.getResultType() == null) {
errorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.CASE_RESULT_TYPE, expr));
return null;
}
List<? extends Concrete.CaseArgument> caseArgs = expr.getArguments();
LinkList list = new LinkList();
List<Expression> expressions = new ArrayList<>(caseArgs.size());
ExprSubstitution substitution = new ExprSubstitution();
Type resultType = null;
Expression resultExpr;
Integer level = expr.level >= -1 ? expr.level : null;
Expression resultTypeLevel = null;
Map<Referable, Binding> origElimBindings = new HashMap<>();
ExprSubstitution elimSubst = new ExprSubstitution();
Set<Binding> allowedBindings = new HashSet<>();
try (var ignored = new Utils.RefContextSaver(context, myLocalPrettifier)) {
for (int i = 0; i < caseArgs.size(); i++) {
Concrete.CaseArgument caseArg = caseArgs.get(i);
Type argType = null;
if (caseArg.type != null) {
argType = checkType(caseArg.type, Type.OMEGA);
}
Expression argTypeExpr = argType == null ? null : argType.getExpr().subst(substitution);
TypecheckingResult exprResult = checkExpr(caseArg.expression, argTypeExpr);
if (exprResult == null) return null;
if (caseArg.isElim && !(exprResult.expression instanceof ReferenceExpression)) {
errorReporter.report(new TypecheckingError("Expected a variable", caseArg.expression));
return null;
}
if (argType == null && Prelude.ARRAY_CONS != null) {
boolean hasConstructors = false;
for (Concrete.FunctionClause clause : expr.getClauses()) {
if (clause.getPatterns().size() > i && clause.getPatterns().get(i) instanceof Concrete.ConstructorPattern conPattern && (conPattern.getConstructor() == Prelude.EMPTY_ARRAY.getReferable() || conPattern.getConstructor() == Prelude.ARRAY_CONS.getReferable())) {
hasConstructors = true;
break;
}
}
if (hasConstructors && !caseArg.isElim) {
Expression normType = exprResult.type.normalize(NormalizationMode.WHNF);
if (normType instanceof ClassCallExpression classCall && classCall.getDefinition() == Prelude.DEP_ARRAY && classCall.isImplementedHere(Prelude.ARRAY_LENGTH)) {
boolean ok = true;
Sort lamSort = null;
Expression type = null;
Expression elementsType = classCall.getAbsImplementationHere(Prelude.ARRAY_ELEMENTS_TYPE);
if (elementsType != null) {
elementsType = elementsType.normalize(NormalizationMode.WHNF);
if (elementsType instanceof LamExpression) {
type = elementsType.removeConstLam();
if (type == null) {
ok = false;
} else {
lamSort = ((LamExpression) elementsType).getResultSort();
}
}
}
if (ok) {
Map<ClassField, Expression> newImpls = new LinkedHashMap<>(classCall.getImplementedHere());
newImpls.remove(Prelude.ARRAY_LENGTH);
ClassCallExpression newClassCall = new ClassCallExpression(Prelude.DEP_ARRAY, classCall.getLevels(), newImpls, classCall.getSort(), classCall.getUniverseKind());
if (type != null) newImpls.put(Prelude.ARRAY_ELEMENTS_TYPE, new LamExpression(lamSort, new TypedSingleDependentLink(true, null, ExpressionFactory.Fin(FieldCallExpression.make(Prelude.ARRAY_LENGTH, new ReferenceExpression(newClassCall.getThisBinding())))), type));
newClassCall.setSort(Prelude.DEP_ARRAY.computeSort(newImpls, newClassCall.getThisBinding()));
exprResult.type = newClassCall;
}
}
}
}
if (argType == null || caseArg.isElim) {
exprResult.type = checkedSubst(exprResult.type, elimSubst, allowedBindings, caseArg.expression);
}
Referable asRef = caseArg.isElim ? ((Concrete.ReferenceExpression) caseArg.expression).getReferent() : caseArg.referable;
DependentLink link = ExpressionFactory.parameter(asRef == null ? null : asRef.textRepresentation(), argType != null ? argType : exprResult.type instanceof Type ? (Type) exprResult.type : new TypeExpression(exprResult.type, getSortOfType(exprResult.type, expr)));
list.append(link);
if (caseArg.isElim) {
if (argTypeExpr != null) {
errorReporter.report(new TypecheckingError("Explicit type annotation is not allowed with \\elim", caseArg.expression));
return null;
}
Binding origBinding = ((ReferenceExpression) exprResult.expression).getBinding();
origElimBindings.put(asRef, origBinding);
elimSubst.add(origBinding, new ReferenceExpression(link));
Set<Object> notEliminated = new HashSet<>();
for (Binding allowedBinding : allowedBindings) {
if (allowedBinding.getTypeExpr().findBinding(origBinding)) {
notEliminated.add(allowedBinding);
}
}
if (!notEliminated.isEmpty()) {
replaceWithReferables(notEliminated, origElimBindings);
replaceWithReferables(notEliminated, context);
errorReporter.report(new ElimSubstError(asRef, notEliminated, caseArg.expression));
return null;
}
allowedBindings.add(origBinding);
}
addBinding(asRef, link);
Expression substExpr = exprResult.expression.subst(substitution);
expressions.add(substExpr);
substitution.add(link, substExpr);
}
if (expr.getResultType() != null) {
resultType = checkType(expr.getResultType(), Type.OMEGA);
}
if (resultType == null && expectedType == null) {
return null;
}
resultExpr = resultType != null ? resultType.getExpr() : !(expectedType instanceof Type && ((Type) expectedType).isOmega()) ? checkedSubst(expectedType, elimSubst, allowedBindings, expr.getResultType() != null ? expr.getResultType() : expr) : new UniverseExpression(Sort.generateInferVars(myEquations, false, expr));
if (expr.getResultTypeLevel() != null) {
TypecheckingResult levelResult = checkExpr(expr.getResultTypeLevel(), null);
if (levelResult != null) {
resultTypeLevel = levelResult.expression;
level = minInteger(level, getExpressionLevel(EmptyDependentLink.getInstance(), levelResult.type, resultExpr, myEquations, expr.getResultTypeLevel()));
}
}
}
List<Referable> addedRefs = new ArrayList<>();
for (Map.Entry<Referable, Binding> entry : origElimBindings.entrySet()) {
removeBinding(entry.getKey());
VeryFakeLocalReferable ref = new VeryFakeLocalReferable(entry.getValue().getName());
context.put(ref, entry.getValue());
addedRefs.add(ref);
}
// Check if the level of the result type is specified explicitly
if (expr.getResultTypeLevel() == null && expr.getResultType() instanceof Concrete.TypedExpression) {
Concrete.Expression typeType = ((Concrete.TypedExpression) expr.getResultType()).type;
if (typeType instanceof Concrete.UniverseExpression universeType && universeType.getHLevel() instanceof Concrete.NumberLevelExpression) {
level = minInteger(level, Math.max(((Concrete.NumberLevelExpression) universeType.getHLevel()).getNumber(), -1));
}
}
// Try to infer level from \\use annotations of the definition in the result type.
if (expr.getResultTypeLevel() == null) {
DefCallExpression defCall = resultExpr.cast(DefCallExpression.class);
Integer level2 = defCall == null ? null : defCall.getUseLevel();
if (level2 == null) {
defCall = resultExpr.getPiParameters(null, false).cast(DefCallExpression.class);
if (defCall != null) {
level2 = defCall.getUseLevel();
}
}
level = minInteger(level, level2);
}
Level actualLevel;
{
Sort sort = resultType == null ? null : resultType.getSortOfType();
actualLevel = sort != null ? sort.getHLevel() : Level.INFINITY;
}
List<ExtElimClause> clauses;
try {
PatternTypechecking patternTypechecking = new PatternTypechecking(PatternTypechecking.Mode.CASE, this, false, expressions, Collections.emptyList());
clauses = patternTypechecking.typecheckClauses(expr.getClauses(), list.getFirst(), resultExpr);
} finally {
for (Referable ref : addedRefs) {
removeBinding(ref);
}
context.putAll(origElimBindings);
}
if (clauses == null) {
return null;
}
ElimBody elimBody = new ElimTypechecking(errorReporter, myEquations, resultExpr, PatternTypechecking.Mode.CASE, level, actualLevel, expr.isSCase(), expr.getClauses(), 0, expr).typecheckElim(clauses, list.getFirst());
if (elimBody == null) {
return null;
}
if (!(expr.isSCase() && actualLevel.isProp())) {
new ConditionsChecking(myEquations, errorReporter, expr).check(clauses, expr.getClauses(), elimBody);
}
TypecheckingResult result = new TypecheckingResult(new CaseExpression(expr.isSCase(), list.getFirst(), resultExpr, resultTypeLevel, elimBody, expressions), resultType != null ? resultExpr.subst(substitution) : expectedType instanceof Type && ((Type) expectedType).isOmega() ? resultExpr : expectedType);
return resultType == null ? result : checkResult(expectedType, result, expr);
}