private void fillInClassDefinition()

in base/src/main/java/org/arend/module/serialization/DefinitionDeserialization.java [109:251]


  private void fillInClassDefinition(ExpressionDeserialization defDeserializer, DefinitionProtos.Definition.ClassData classProto, ClassDefinition classDef) throws DeserializationException {
    classDef.setBaseUniverseKind(defDeserializer.readUniverseKind(classProto.getBaseUniverseKind()));

    Map<Integer, LevelProtos.Levels> superLevelsProto = classProto.getSuperLevelsMap();
    if (!superLevelsProto.isEmpty()) {
      Map<ClassDefinition, Levels> superLevels = new HashMap<>();
      for (Map.Entry<Integer, LevelProtos.Levels> entry : superLevelsProto.entrySet()) {
        ClassDefinition superClass = myCallTargetProvider.getCallTarget(entry.getKey(), ClassDefinition.class);
        superLevels.put(superClass, defDeserializer.readLevels(entry.getValue()));
      }
      classDef.setSuperLevels(superLevels);
    }

    for (DefinitionProtos.Definition.ClassData.Field fieldProto : classProto.getPersonalFieldList()) {
      ClassField field = myCallTargetProvider.getCallTarget(fieldProto.getReferable().getIndex(), ClassField.class);
      if (!fieldProto.hasType()) {
        throw new DeserializationException("Missing class field type");
      }
      PiExpression fieldType = checkFieldType(defDeserializer.readPi(fieldProto.getType()), classDef);
      if (fieldProto.getIsProperty()) {
        field.setIsProperty();
      }
      field.setType(fieldType);
      if (fieldProto.hasTypeLevel()) {
        field.setTypeLevel(defDeserializer.readExpr(fieldProto.getTypeLevel()), fieldProto.getResultTypeLevel());
      }
      field.setNumberOfParameters(fieldProto.getNumberOfParameters());
      // setTypeClassReference(field.getReferable(), EmptyDependentLink.getInstance(), fieldType.getCodomain());
      field.setHideable(fieldProto.getIsHideable());
      field.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
      field.setUniverseKind(defDeserializer.readUniverseKind(fieldProto.getUniverseKind()));
      loadKeys(fieldProto.getUserDataMap(), field);
    }

    for (int classFieldRef : classProto.getFieldRefList()) {
      classDef.addField(myCallTargetProvider.getCallTarget(classFieldRef, ClassField.class));
    }
    for (int classFieldRef : classProto.getFieldRefList()) {
      classDef.addField(myCallTargetProvider.getCallTarget(classFieldRef, ClassField.class));
    }
    for (Map.Entry<Integer, ExpressionProtos.Expression.Abs> entry : classProto.getImplementationsMap().entrySet()) {
      classDef.implementField(myCallTargetProvider.getCallTarget(entry.getKey(), ClassField.class), defDeserializer.readAbsExpr(entry.getValue()));
    }
    for (Map.Entry<Integer, DefinitionProtos.Definition.DefaultData> entry : classProto.getDefaultsMap().entrySet()) {
      classDef.addDefault(myCallTargetProvider.getCallTarget(entry.getKey(), ClassField.class), defDeserializer.readAbsExpr(entry.getValue().getExpr()), entry.getValue().getIsFunc());
    }
    for (Map.Entry<Integer, DefinitionProtos.Definition.RefList> entry : classProto.getDefaultDependenciesMap().entrySet()) {
      classDef.addDefaultDependencies(myCallTargetProvider.getCallTarget(entry.getKey(), ClassField.class), readDefinitions(entry.getValue().getRefList(), ClassField.class));
    }
    for (Map.Entry<Integer, DefinitionProtos.Definition.RefList> entry : classProto.getDefaultImplDependenciesMap().entrySet()) {
      classDef.addDefaultImplDependencies(myCallTargetProvider.getCallTarget(entry.getKey(), ClassField.class), readDefinitions(entry.getValue().getRefList(), ClassField.class));
    }
    for (var entry : classProto.getOverriddenFieldMap().entrySet()) {
      classDef.overrideField(myCallTargetProvider.getCallTarget(entry.getKey(), ClassField.class), checkFieldType(defDeserializer.readPi(entry.getValue().getType()), classDef), myCallTargetProvider.getCallTarget(entry.getValue().getOriginalClass(), ClassDefinition.class));
    }
    for (Integer fieldRef : classProto.getCovariantFieldList()) {
      classDef.addCovariantField(myCallTargetProvider.getCallTarget(fieldRef, ClassField.class));
    }
    for (Integer fieldRef : classProto.getOmegaFieldList()) {
      classDef.addOmegaField(myCallTargetProvider.getCallTarget(fieldRef, ClassField.class));
    }
    classDef.setSort(defDeserializer.readSort(classProto.getSort()));

    for (int superClassRef : classProto.getSuperClassRefList()) {
      ClassDefinition superClass = myCallTargetProvider.getCallTarget(superClassRef, ClassDefinition.class);
      classDef.addSuperClass(superClass);
      myDependencyListener.dependsOn(classDef.getReferable(), superClass.getReferable());

      for (Map.Entry<ClassField, AbsExpression> entry : superClass.getImplemented()) {
        classDef.implementField(entry.getKey(), entry.getValue());
      }
    }

    if (classDef.getReferable() instanceof ClassReferableImpl classRef) {
      for (ClassDefinition superClass : classDef.getSuperClasses()) {
        Referable superRef = superClass.getReferable().getUnderlyingReferable();
        if (superRef instanceof ClassReferable) {
          classRef.getSuperClassReferences().add((ClassReferable) superRef);
        }
        if (!classDef.getSuperLevels().isEmpty()) {
          classRef.addSuperLevels(classDef.getSuperLevels().get(superClass) != null);
        }
      }
    }

    if (classProto.getCoercingFieldRef() != -1) {
      classDef.setClassifyingField(myCallTargetProvider.getCallTarget(classProto.getCoercingFieldRef(), ClassField.class));
    }
    if (classProto.getIsRecord()) {
      classDef.setRecord();
    }

    int squasher = classProto.getSquasher();
    if (squasher != 0) {
      classDef.setSquasher(myCallTargetProvider.getCallTarget(squasher, FunctionDefinition.class));
    }

    readCoerceData(classProto.getCoerceData(), classDef.getCoerceData());

    for (DefinitionProtos.Definition.ClassParametersLevel classParametersLevelProto : classProto.getParametersLevelList()) {
      List<ClassField> fields = new ArrayList<>();
      for (Integer fieldRef : classParametersLevelProto.getFieldList()) {
        fields.add(myCallTargetProvider.getCallTarget(fieldRef, ClassField.class));
      }
      DefinitionProtos.Definition.ParametersLevel parametersLevelProto = classParametersLevelProto.getParametersLevel();
      List<Pair<ClassDefinition, Set<ClassField>>> strictList;
      if (classParametersLevelProto.getIsStrict()) {
        strictList = new ArrayList<>();
        for (DefinitionProtos.Definition.ClassParametersLevel.ClassExtSig sig : classParametersLevelProto.getClassExtSigList()) {
          if (sig.getClassDef() == 0) {
            strictList.add(null);
          } else {
            Set<ClassField> sigFields = new HashSet<>();
            for (Integer fieldRef : sig.getFieldList()) {
              sigFields.add(myCallTargetProvider.getCallTarget(fieldRef, ClassField.class));
            }
            strictList.add(new Pair<>(myCallTargetProvider.getCallTarget(sig.getClassDef(), ClassDefinition.class), sigFields));
          }
        }
      } else {
        strictList = null;
      }
      classDef.addParametersLevel(new ClassDefinition.ParametersLevel(parametersLevelProto.getHasParameters() ? defDeserializer.readParameters(parametersLevelProto.getParameterList()) : null, parametersLevelProto.getLevel(), fields, strictList));
    }

    List<Integer> goodFieldIndices = classProto.getGoodFieldList();
    if (!goodFieldIndices.isEmpty()) {
      Set<ClassField> goodFields = new HashSet<>();
      for (Integer goodFieldIndex : goodFieldIndices) {
        goodFields.add(myCallTargetProvider.getCallTarget(goodFieldIndex, ClassField.class));
      }
      classDef.setGoodThisFields(goodFields);
    }

    List<Integer> typeClassFieldIndices = classProto.getTypeClassFieldList();
    if (!typeClassFieldIndices.isEmpty()) {
      Set<ClassField> typeClassFields = new HashSet<>();
      for (Integer typeClassFieldIndex : typeClassFieldIndices) {
        typeClassFields.add(myCallTargetProvider.getCallTarget(typeClassFieldIndex, ClassField.class));
      }
      classDef.setTypeClassFields(typeClassFields);
    }
  }