in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [2413:2597]
private boolean typecheckConstructor(Concrete.Constructor def, List<ExpressionPattern> patterns, DataDefinition dataDefinition, Set<DataDefinition> dataDefinitions) {
Constructor constructor = myNewDef ? new Constructor(def.getData(), dataDefinition) : null;
if (constructor != null) {
constructor.setPatterns(patterns);
}
Constructor oldConstructor = constructor != null ? constructor : (Constructor) def.getData().getTypechecked();
List<DependentLink> elimParams;
Expression constructorType = null;
LinkList list = new LinkList();
boolean ok;
try (var ignored = new Utils.RefContextSaver(typechecker.getContext(), typechecker.getLocalExpressionPrettifier())) {
if (constructor != null) {
def.getData().setTypechecked(constructor);
dataDefinition.addConstructor(constructor);
}
ok = typecheckParameters(def, constructor, list, null, dataDefinition.getSort(), null, null, null) != null;
if (constructor != null) {
constructor.setStrictParameters(getStrictParameters(def.getParameters()));
}
int i = 0;
for (DependentLink link = list.getFirst(); link.hasNext(); link = link.getNext(), i++) {
link = link.getNextTyped(null);
if (new RecursiveDataChecker(dataDefinitions, errorReporter, def, def.getParameters().get(i)).check(link.getTypeExpr())) {
if (constructor != null) {
constructor.setParameters(EmptyDependentLink.getInstance());
}
return false;
}
}
if (def.getResultType() != null) {
Type resultType = typechecker.checkType(def.getResultType(), Type.OMEGA);
if (resultType != null) {
constructorType = normalizePathExpression(resultType.getExpr(), oldConstructor, def.getResultType());
}
def.setResultType(null);
}
elimParams = def.getClauses().isEmpty() ? null : ElimTypechecking.getEliminatedParameters(def.getEliminatedReferences(), def.getClauses(), list.getFirst(), typechecker);
}
if (constructor != null && def.isCoerce()) {
dataDefinition.getCoerceData().addCoercingConstructor(constructor, errorReporter, def);
}
List<DependentLink> newParams = new ArrayList<>();
if (constructor != null && constructorType != null) {
int numberOfNewParameters = 0;
for (Expression type = constructorType; type instanceof DataCallExpression && ((DataCallExpression) type).getDefinition() == Prelude.PATH; type = ((LamExpression) ((DataCallExpression) type).getDefCallArguments().get(0)).getBody()) {
numberOfNewParameters++;
}
if (numberOfNewParameters != 0) {
if (elimParams != null && elimParams.isEmpty()) {
elimParams = DependentLink.Helper.toList(list.getFirst());
}
DependentLink newParam = new TypedDependentLink(true, "i" + (numberOfNewParameters == 1 ? "" : numberOfNewParameters), Interval(), EmptyDependentLink.getInstance());
newParams.add(newParam);
for (int i = numberOfNewParameters - 1; i >= 1; i--) {
newParam = new UntypedDependentLink("i" + i, newParam);
newParams.add(newParam);
}
list.append(newParam);
constructor.setParameters(list.getFirst());
List<IntervalElim.CasePair> pairs;
ElimBody elimBody;
if (constructor.getBody() instanceof IntervalElim) {
pairs = ((IntervalElim) constructor.getBody()).getCases();
for (int i = 0; i < pairs.size(); i++) {
pairs.set(i, new IntervalElim.CasePair(addAts(pairs.get(i).proj1, newParam, constructorType), addAts(pairs.get(i).proj2, newParam, constructorType)));
}
elimBody = ((IntervalElim) constructor.getBody()).getOtherwise();
} else {
pairs = new ArrayList<>();
elimBody = constructor.getBody() instanceof ElimBody ? (ElimBody) constructor.getBody() : null;
}
int i = 0;
Expression type = constructorType;
while (type instanceof DataCallExpression && ((DataCallExpression) type).getDefinition() == Prelude.PATH) {
List<Expression> pathArgs = ((DataCallExpression) type).getDefCallArguments();
LamExpression lamExpr = (LamExpression) pathArgs.get(0);
type = lamExpr.getBody();
DependentLink param = newParams.get(i++);
pairs.add(new IntervalElim.CasePair(addAts(pathArgs.get(1), param, type.subst(lamExpr.getParameters(), Left())), addAts(pathArgs.get(2), param, type.subst(lamExpr.getParameters(), Right()))));
type = type.subst(lamExpr.getParameters(), new ReferenceExpression(newParam));
newParam = newParam.getNext();
}
constructor.setBody(new IntervalElim(DependentLink.Helper.size(list.getFirst()), pairs, elimBody));
}
}
if (elimParams != null) {
try (var ignored = new Utils.RefContextSaver(typechecker.getContext(), typechecker.getLocalExpressionPrettifier())) {
Expression expectedType = constructorType != null ? constructorType : oldConstructor.getDataTypeExpression(oldConstructor.makeIdLevels());
CountingErrorReporter countingErrorReporter = new CountingErrorReporter(PathEndpointMismatchError.class, errorReporter);
List<DependentLink> finalElimParams = elimParams;
List<ExtElimClause> clauses = typechecker.withErrorReporter(countingErrorReporter, tc -> new PatternTypechecking(PatternTypechecking.Mode.CONSTRUCTOR, typechecker, false, null, finalElimParams).typecheckClauses(def.getClauses(), def.getParameters(), oldConstructor.getParameters(), expectedType, null));
if (clauses != null) {
if (!newParams.isEmpty()) {
for (ExtElimClause clause : clauses) {
Expression expr = clause.getExpression();
if (expr == null) continue;
for (DependentLink param : newParams) {
expr = AtExpression.make(expr.normalize(NormalizationMode.WHNF), new ReferenceExpression(param), true);
}
clause.setExpression(expr);
}
}
for (int i = 0; i < clauses.size(); i++) {
checkConstructorsOnlyOnTop(clauses.get(i).getExpression(), dataDefinition, def.getClauses().get(i).getExpression());
}
}
Body body = clauses == null ? null : new ElimTypechecking(errorReporter, typechecker.getEquations(), expectedType, PatternTypechecking.Mode.CONSTRUCTOR, def.getClauses(), def).typecheckElim(clauses, oldConstructor.getParameters(), elimParams);
if (constructor != null) {
if (body != null) {
if (constructor.getBody() instanceof IntervalElim intervalElim) {
if (body instanceof IntervalElim oldIntervalElim) {
List<IntervalElim.CasePair> cases = new ArrayList<>();
cases.addAll(oldIntervalElim.getCases().subList(0, oldIntervalElim.getCases().size() - intervalElim.getCases().size()));
cases.addAll(intervalElim.getCases());
constructor.setBody(new IntervalElim(intervalElim.getNumberOfParameters(), cases, oldIntervalElim.getOtherwise()));
} else if (body instanceof ElimBody) {
constructor.setBody(new IntervalElim(intervalElim.getNumberOfParameters(), intervalElim.getCases(), (ElimBody) body));
}
} else {
constructor.setBody(body);
}
}
constructor.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
}
boolean dataSortIsProp = dataDefinition.getSort().isProp();
if (dataSortIsProp) {
dataDefinition.setSort(Sort.SET0);
}
if (body != null && countingErrorReporter.getErrorsNumber() == 0) {
new ConditionsChecking(typechecker.getEquations(), errorReporter, def).check(body, clauses, def.getClauses(), oldConstructor);
}
if (dataSortIsProp) {
dataDefinition.setSort(Sort.PROP);
}
}
}
if (constructor != null) {
constructor.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
calculateTypeClassParameters(def, constructor);
calculateGoodThisParameters(constructor);
calculateParametersTypecheckingOrder(constructor);
int recursiveIndex = -1;
int i = 0;
loop:
for (DependentLink link = constructor.getParameters(); link.hasNext(); link = link.getNext(), i++) {
if (link.getTypeExpr() instanceof DataCallExpression && dataDefinitions.contains(((DataCallExpression) link.getTypeExpr()).getDefinition())) {
for (DependentLink link2 = link.getNext(); link2.hasNext(); link2 = link2.getNext()) {
link2 = link2.getNextTyped(null);
if (link2.getTypeExpr().findFreeBinding(link)) {
continue loop;
}
}
if (recursiveIndex != -1) {
recursiveIndex = -1;
break;
} else {
recursiveIndex = i;
}
}
}
if (recursiveIndex != -1) {
constructor.setRecursiveParameter(recursiveIndex);
}
}
return ok;
}