in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [2076:2329]
private boolean typecheckDataBody(DataDefinition dataDefinition, Concrete.DataDefinition def, Set<DataDefinition> dataDefinitions) {
UniverseKind universeKind = dataDefinition.getUniverseKind();
if (myNewDef) {
dataDefinition.setUniverseKind(UniverseKind.WITH_UNIVERSES);
dataDefinition.getConstructors().clear();
}
Sort userSort = dataDefinition.getSort();
Sort inferredSort = def.getConstructorClauses().isEmpty() ? Sort.PROP : Sort.generateInferVars(typechecker.getEquations(), false, def);
if (myNewDef) {
dataDefinition.setSort(inferredSort);
}
boolean dataOk = true;
List<DependentLink> elimParams = Collections.emptyList();
if (def.getEliminatedReferences() != null) {
elimParams = ElimTypechecking.getEliminatedParameters(def.getEliminatedReferences(), def.getConstructorClauses(), dataDefinition.getParameters(), typechecker);
if (elimParams == null) {
dataOk = false;
}
}
ErrorReporter originalErrorReporter = errorReporter;
ErrorReporterCounter countingErrorReporter = new ErrorReporterCounter(GeneralError.Level.ERROR, originalErrorReporter);
errorReporter = countingErrorReporter;
if (!def.getConstructorClauses().isEmpty()) {
Map<Referable, Binding> context = typechecker.getContext();
PatternTypechecking dataPatternTypechecking = elimParams == null ? null : new PatternTypechecking(PatternTypechecking.Mode.DATA, typechecker, true, null, elimParams);
Set<TCReferable> notAllowedConstructors = new HashSet<>();
for (Concrete.ConstructorClause clause : def.getConstructorClauses()) {
for (Concrete.Constructor constructor : clause.getConstructors()) {
notAllowedConstructors.add(constructor.getData());
}
}
boolean noHITs = true;
LocalInstancePool instancePool = typechecker.getInstancePool().getLocalInstancePool();
for (Concrete.ConstructorClause clause : def.getConstructorClauses()) {
typechecker.copyContextFrom(context);
// Typecheck patterns and compute free bindings
boolean patternsOK = true;
PatternTypechecking.Result result = null;
if (clause.getPatterns() != null) {
if (def.getEliminatedReferences() == null) {
originalErrorReporter.report(new TypecheckingError("Expected a constructor without patterns", clause));
dataOk = false;
}
if (dataPatternTypechecking != null) {
ExprSubstitution substitution = new ExprSubstitution();
result = dataPatternTypechecking.typecheckPatterns(clause.getPatterns(), def.getParameters(), dataDefinition.getParameters(), substitution, null, def);
if (instancePool != null) {
typechecker.getInstancePool().setInstancePool(instancePool.subst(substitution));
}
if (result != null && noHITs) {
for (ExpressionPattern pattern : result.getPatterns()) {
if (!checkNoHITs(pattern, clause)) {
result = null;
noHITs = false;
break;
}
}
}
if (result != null && result.hasEmptyPattern()) {
originalErrorReporter.report(new RedundantClauseError(clause));
result = null;
}
if (result == null) {
typechecker.copyContextFrom(context);
patternsOK = false;
}
}
} else {
if (def.getEliminatedReferences() != null) {
originalErrorReporter.report(new TypecheckingError("Expected constructors with patterns", clause));
dataOk = false;
}
}
// Process constructors
for (Concrete.Constructor constructor : clause.getConstructors()) {
// Check that constructors do not refer to constructors defined later
FreeReferablesVisitor visitor = new FreeReferablesVisitor(notAllowedConstructors);
if (constructor.getResultType() != null) {
if (constructor.getResultType().accept(visitor, null) != null) {
errorReporter.report(new ConstructorReferenceError(constructor.getResultType()));
constructor.setResultType(null);
}
}
Iterator<Concrete.FunctionClause> it = constructor.getClauses().iterator();
while (it.hasNext()) {
Concrete.FunctionClause conClause = it.next();
if (visitor.visitClause(conClause, null) != null) {
errorReporter.report(new ConstructorReferenceError(conClause));
it.remove();
}
}
boolean constructorOK = patternsOK;
if (visitor.visitParameters(constructor.getParameters(), null) != null) {
errorReporter.report(new ConstructorReferenceError(constructor));
constructorOK = false;
}
if (!constructorOK) {
constructor.getParameters().clear();
constructor.getEliminatedReferences().clear();
constructor.getClauses().clear();
constructor.setResultType(null);
}
notAllowedConstructors.remove(constructor.getData());
// Typecheck constructors
List<ExpressionPattern> patterns = result == null ? null : result.getPatterns();
if (!typecheckConstructor(constructor, patterns, dataDefinition, dataDefinitions)) {
dataOk = false;
}
}
}
typechecker.getInstancePool().setInstancePool(instancePool);
if (inferredSort.isProp() || inferredSort.getHLevel().isVarOnly()) {
boolean ok = true;
for (int i = 0; i < dataDefinition.getConstructors().size(); i++) {
List<ExpressionPattern> patterns1 = dataDefinition.getConstructors().get(i).getPatterns();
for (int j = i + 1; j < dataDefinition.getConstructors().size(); j++) {
List<ExpressionPattern> patterns2 = dataDefinition.getConstructors().get(j).getPatterns();
if (patterns1 == null || patterns2 == null || ExpressionPattern.unify(patterns1, patterns2, null, null, null, errorReporter, def)) {
ok = false;
break;
}
}
if (!ok) {
break;
}
}
if (!ok) {
Sort.compare(Sort.SET0, inferredSort, CMP.LE, typechecker.getEquations(), def);
}
}
// Check if constructors pattern match on the interval
for (Constructor constructor : dataDefinition.getConstructors()) {
if (constructor.getBody() instanceof IntervalElim && !inferredSort.getHLevel().isInfinity()) {
Sort.compare(new Sort(inferredSort.getPLevel(), Level.INFINITY), inferredSort, CMP.LE, typechecker.getEquations(), def);
break;
}
}
typechecker.invokeDeferredMetas(null, null, false);
LevelEquationsSolver levelSolver = typechecker.getEquations().makeLevelEquationsSolver();
LevelSubstitution levelSubstitution = levelSolver.solveLevels();
typechecker.getEquations().finalizeEquations(levelSubstitution, def);
InPlaceLevelSubstVisitor substVisitor = new InPlaceLevelSubstVisitor(levelSubstitution);
InferenceVariableSolveVisitor solveVisitor = new InferenceVariableSolveVisitor(typechecker);
StripVisitor stripVisitor = new StripVisitor(errorReporter);
typechecker.invokeDeferredMetas(substVisitor, stripVisitor, true);
for (Constructor constructor : dataDefinition.getConstructors()) {
if (!substVisitor.isEmpty()) {
substVisitor.visitParameters(constructor.getParameters(), null);
substVisitor.visitBody(constructor.getBody(), null);
}
solveVisitor.visitParameters(constructor.getParameters(), null);
stripVisitor.visitParameters(constructor.getParameters());
stripVisitor.visitBody(constructor.getBody());
}
if (!substVisitor.isEmpty()) {
inferredSort = inferredSort.subst(substVisitor.getLevelSubstitution());
dataDefinition.setSort(inferredSort);
}
}
if (myNewDef && !dataOk) {
dataDefinition.addStatus(Definition.TypeCheckingStatus.HAS_ERRORS);
}
errorReporter = originalErrorReporter;
// Find covariant parameters
if (myNewDef && dataDefinition.getParameters().hasNext()) {
int index = 0;
Set<DependentLink> parameters = new HashSet<>();
for (DependentLink link = dataDefinition.getParameters(); link.hasNext(); link = link.getNext(), index++) {
dataDefinition.setCovariant(index, true);
parameters.add(link);
}
int size;
do {
size = parameters.size();
getCovariantParameters(dataDefinition, parameters);
index = 0;
for (DependentLink link = dataDefinition.getParameters(); link.hasNext(); link = link.getNext(), index++) {
dataDefinition.setCovariant(index, parameters.contains(link));
}
} while (!parameters.isEmpty() && parameters.size() != size);
}
// Check truncatedness
if (def.isTruncated()) {
if (userSort == null) {
originalErrorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.TRUNCATED_WITHOUT_UNIVERSE, def));
} else {
if (inferredSort.isLessOrEquals(userSort)) {
originalErrorReporter.report(new CertainTypecheckingError(CertainTypecheckingError.Kind.DATA_WONT_BE_TRUNCATED, def.getUniverse() == null ? def : def.getUniverse()));
} else if (myNewDef) {
dataDefinition.setTruncatedLevel(userSort.getHLevel().getConstant());
dataDefinition.setSquashed(true);
}
}
if (countingErrorReporter.getErrorsNumber() == 0 && userSort != null && !userSort.isProp() && !Level.compare(inferredSort.getPLevel(), userSort.getPLevel(), CMP.LE, DummyEquations.getInstance(), null)) {
if (!def.isRecursive() && def.getUniverse() != null && def.getUniverse().getPLevel() == null) {
userSort = new Sort(inferredSort.getPLevel(), userSort.getHLevel());
} else {
countingErrorReporter.report(new DataUniverseError(new Sort(inferredSort.getPLevel(), userSort.getHLevel()), userSort, def.getUniverse() == null ? def : def.getUniverse()));
}
}
} else if (countingErrorReporter.getErrorsNumber() == 0 && userSort != null && !inferredSort.isLessOrEquals(userSort)) {
countingErrorReporter.report(new DataUniverseError(inferredSort, userSort, def.getUniverse() == null ? def : def.getUniverse()));
}
if (myNewDef) {
dataDefinition.setSort(countingErrorReporter.getErrorsNumber() == 0 && userSort != null ? userSort : inferredSort);
typechecker.setStatus(def.getStatus().getTypecheckingStatus());
dataDefinition.addStatus(typechecker.getStatus());
if (universeKind != UniverseKind.WITH_UNIVERSES) {
dataDefinition.setUniverseKind(universeKind);
loop:
for (Constructor constructor : dataDefinition.getConstructors()) {
for (DependentLink link = constructor.getParameters(); link.hasNext(); link = link.getNext()) {
link = link.getNextTyped(null);
universeKind = universeKind.max(new UniverseKindChecker(def.getRecursiveDefinitions()).getUniverseKind(link.getTypeExpr()));
if (universeKind == UniverseKind.WITH_UNIVERSES) {
break loop;
}
}
}
dataDefinition.setUniverseKind(universeKind);
}
}
if (myNewDef) {
GoodThisParametersVisitor goodThisParametersVisitor = new GoodThisParametersVisitor(dataDefinition.getGoodThisParameters(), dataDefinition.getParameters());
for (Constructor constructor : dataDefinition.getConstructors()) {
goodThisParametersVisitor.visitParameters(constructor.getParameters(), null);
goodThisParametersVisitor.visitBody(constructor.getBody(), null);
}
dataDefinition.setGoodThisParameters(goodThisParametersVisitor.getGoodParameters());
def.setTypechecked();
}
return countingErrorReporter.getErrorsNumber() == 0;
}