private void findLevelsParents()

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);
      }
    }
  }