in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [961:1043]
private void findLevelsParents(TopLevelDefinition typedDef, Concrete.Definition cdef, List<? extends Concrete.ReferenceExpression> refs, int setLevelsParentsUpTo) {
boolean hadPLevels = cdef.getPLevelParameters() != null;
boolean hadHLevels = cdef.getHLevelParameters() != null;
boolean searchPLevels = !hadPLevels;
boolean searchHLevels = !hadHLevels;
TCReferable pLevelsParent = getFirstLevelParameter(cdef.getPLevelParameters());
TCReferable hLevelsParent = getFirstLevelParameter(cdef.getHLevelParameters());
boolean pLevelsNotDerived = false;
boolean hLevelsNotDerived = false;
boolean allPLevelsDerived = true;
boolean allHLevelsDerived = true;
if (searchPLevels || searchHLevels) {
for (int i = 0; i < refs.size(); i++) {
Concrete.ReferenceExpression ref = refs.get(i);
Definition def = ((TCDefReferable) ref.getReferent()).getTypechecked();
if (searchPLevels && def.getPLevelsParent() != null && (i < setLevelsParentsUpTo || !def.arePLevelsDerived()) && ref.getPLevels() == null) {
if (pLevelsParent == null) {
pLevelsParent = def.getPLevelsParent();
if (i < setLevelsParentsUpTo) {
pLevelsNotDerived = true;
}
if (!def.arePLevelsDerived()) {
allPLevelsDerived = false;
}
} else if (pLevelsParent != def.getPLevelsParent()) {
pLevelsParent = null;
searchPLevels = false;
}
}
if (searchHLevels && def.getHLevelsParent() != null && (i < setLevelsParentsUpTo || !def.areHLevelsDerived()) && ref.getHLevels() == null) {
if (hLevelsParent == null) {
hLevelsParent = def.getHLevelsParent();
if (i < setLevelsParentsUpTo) {
hLevelsNotDerived = true;
}
if (!def.areHLevelsDerived()) {
allHLevelsDerived = false;
}
} else if (hLevelsParent != def.getHLevelsParent()) {
hLevelsParent = null;
searchHLevels = false;
}
}
}
}
if (pLevelsParent == null && hLevelsParent == null) {
return;
}
List<Concrete.LevelExpression> pLevelExprs = null;
if (pLevelsParent != null) {
if (cdef.getPLevelParameters() == null) {
cdef.setPLevelParameters(referableToLevelParameters(pLevelsParent, cdef.getData(), true));
}
if (cdef.getPLevelParameters() != null) {
typedDef.setPLevelsParent(pLevelsParent);
typedDef.setPLevelsDerived(!hadPLevels && (!pLevelsNotDerived || allPLevelsDerived));
pLevelExprs = levelParametersToExpressions(null, cdef.getPLevelParameters(), LevelVariable.LvlType.PLVL);
}
}
List<Concrete.LevelExpression> hLevelExprs = null;
if (hLevelsParent != null) {
if (cdef.getHLevelParameters() == null) {
cdef.setHLevelParameters(referableToLevelParameters(hLevelsParent, cdef.getData(), false));
}
if (cdef.getHLevelParameters() != null) {
typedDef.setHLevelsParent(hLevelsParent);
typedDef.setHLevelsDerived(!hadHLevels && (!hLevelsNotDerived || allHLevelsDerived));
hLevelExprs = levelParametersToExpressions(null, cdef.getHLevelParameters(), LevelVariable.LvlType.HLVL);
}
}
for (Concrete.ReferenceExpression ref : refs) {
Definition def = ((TCDefReferable) ref.getReferent()).getTypechecked();
if (pLevelsParent != null && def.getPLevelsParent() == pLevelsParent && ref.getPLevels() == null) {
ref.setPLevels(pLevelExprs);
}
if (hLevelsParent != null && def.getHLevelsParent() == hLevelsParent && ref.getHLevels() == null) {
ref.setHLevels(hLevelExprs);
}
}
}