in base/src/main/java/org/arend/typechecking/visitor/WhereVarsFixVisitor.java [48:245]
public static void fixDefinition(Collection<? extends Concrete.Definition> definitions, ErrorReporter errorReporter) {
var whereVars = WhereVarsCollector.findWhereVars(definitions);
Map<TCDefReferable, List<Referable>> selfArgsMap = new HashMap<>();
Map<TCDefReferable, Pair<List<Concrete.Parameter>, List<Pair<TCDefReferable, Integer>>>> paramsMap = new HashMap<>();
for (Concrete.Definition definition : definitions) {
List<Concrete.Parameter> newParams = Collections.emptyList();
List<Pair<TCDefReferable, Integer>> parametersOriginalDefinitions = Collections.emptyList();
if (!whereVars.proj1.isEmpty() || !whereVars.proj2.isEmpty()) {
Set<Pair<TCDefReferable, Integer>> wherePairs = new HashSet<>();
Map<TCDefReferable, Set<Referable>> refMap = new HashMap<>();
for (ParameterReferable whereRef : whereVars.proj1) {
if (definition.getExternalParameters().containsKey(whereRef.getDefinition())) {
wherePairs.add(new Pair<>(whereRef.getDefinition(), whereRef.getIndex()));
refMap.computeIfAbsent(whereRef.getDefinition(), k -> new HashSet<>()).add(getReferable(definition, whereRef));
}
}
record ParamData(TCDefReferable definition, Concrete.Parameter parameter, int index) {}
loop:
for (Map.Entry<TCDefReferable, Set<Referable>> entry : refMap.entrySet()) {
Map<Referable, ParamData> parameterMap = new HashMap<>();
for (Map.Entry<TCDefReferable, Concrete.ExternalParameters> entry1 : definition.getExternalParameters().entrySet()) {
int index = 0;
for (Concrete.Parameter parameter : entry1.getValue().parameters) {
for (Referable referable : parameter.getReferableList()) {
if (referable != null) {
ParamData data = new ParamData(entry1.getKey(), parameter, index);
parameterMap.put(referable, data);
parameterMap.put(referable.getUnderlyingReferable(), data);
}
index++;
}
}
}
Set<Referable> found = entry.getValue();
for (Referable referable : found) {
if (!parameterMap.containsKey(referable)) {
continue loop;
}
}
while (!found.isEmpty()) {
Set<Referable> foundRefs = new HashSet<>();
for (Referable referable : found) {
Concrete.Expression type = parameterMap.get(referable).parameter.getType();
if (type != null) {
type.accept(new FreeVariableCollectorConcrete(foundRefs), null);
}
}
found.clear();
for (Referable foundRef : foundRefs) {
while (foundRef instanceof ParameterReferable paramRef) {
foundRef = paramRef.getUnderlyingReferable();
}
ParamData paramData = parameterMap.get(foundRef);
if (paramData != null && wherePairs.add(new Pair<>(paramData.definition, paramData.index))) {
found.add(foundRef);
}
}
}
}
int myLevel = getReferableLevel(definition.getData());
for (Definition def : whereVars.proj2) {
for (Pair<TCDefReferable, Integer> pair : def.getParametersOriginalDefinitions()) {
if (definition.getExternalParameters().containsKey(pair.proj1) && pair.proj1 != definition.getData() && !wherePairs.contains(pair) && getReferableLevel(pair.proj1) < myLevel && !(definition instanceof Concrete.CoClauseFunctionDefinition && ((Concrete.CoClauseFunctionDefinition) definition).getUseParent() == pair.proj1)) {
wherePairs.add(pair);
}
}
}
parametersOriginalDefinitions = new ArrayList<>(wherePairs);
parametersOriginalDefinitions.sort(Comparator.comparingInt((Pair<TCDefReferable, Integer> data) -> getReferableLevel(data.proj1)).thenComparingInt(data -> data.proj2));
newParams = new ArrayList<>();
for (var data : parametersOriginalDefinitions) {
Concrete.ExternalParameters params = definition.getExternalParameters().get(data.proj1);
if (params != null) {
Pair<Concrete.Parameter, Referable> param = Concrete.getParameter(params.parameters, data.proj2);
if (param != null) {
newParams.add(new Concrete.TelescopeParameter(definition.getData(), false, Collections.singletonList(param.proj2), param.proj1.getType() == null ? null : param.proj1.getType(), param.proj1.isProperty()));
}
}
}
List<Concrete.Parameter> newNewParams = new ArrayList<>();
for (int i = 0; i < newParams.size(); i++) {
Concrete.Parameter param = newParams.get(i);
if (i + 1 < newParams.size() && param.getType() != null && param.getType() == newParams.get(i + 1).getType() && param.isExplicit() == newParams.get(i + 1).isExplicit()) {
List<Referable> referables = new ArrayList<>(param.getReferableList());
while (i + 1 < newParams.size() && param.getType() == newParams.get(i + 1).getType() && param.isExplicit() == newParams.get(i + 1).isExplicit()) {
i++;
referables.addAll(newParams.get(i).getReferableList());
}
newNewParams.add(new Concrete.TelescopeParameter(definition.getData(), param.isExplicit(), referables, param.getType() == null ? null : param.getType().accept(new ReplaceDataVisitor(definition.getData()), null), param.isProperty()));
} else {
newNewParams.add(new Concrete.TelescopeParameter(definition.getData(), param.isExplicit(), param.getReferableList(), param.getType() == null ? null : param.getType().accept(new ReplaceDataVisitor(definition.getData()), null), param.isProperty()));
}
}
newParams = newNewParams;
List<Referable> selfArgs = new ArrayList<>();
for (Concrete.Parameter param : newParams) {
selfArgs.addAll(param.getReferableList());
}
if (!selfArgs.isEmpty()) {
selfArgsMap.put(definition.getData(), selfArgs);
}
Set<Referable> levelRefs = new HashSet<>();
for (Concrete.Parameter param : newParams) {
if (param.getType() != null) {
param.getType().accept(new FindLevelVariablesVisitor(levelRefs), null);
}
}
levelRefs.removeIf(ref -> ref instanceof TCLevelReferable);
if (!levelRefs.isEmpty()) {
Concrete.LevelParameters pLevels = null;
Concrete.LevelParameters hLevels = null;
Set<TCDefReferable> pLevelsDefs = new HashSet<>();
Set<TCDefReferable> hLevelsDefs = new HashSet<>();
for (var varData : parametersOriginalDefinitions) {
Concrete.ExternalParameters params = definition.getExternalParameters().get(varData.proj1);
if (params != null) {
if (params.pLevelParameters != null) {
pLevelsDefs.add(varData.proj1);
if (pLevels == null) pLevels = params.pLevelParameters;
}
if (params.hLevelParameters != null) {
hLevelsDefs.add(varData.proj1);
if (hLevels == null) hLevels = params.hLevelParameters;
}
}
}
checkLevels(pLevelsDefs, definition.getPLevelParameters(), errorReporter, "p", definition);
checkLevels(hLevelsDefs, definition.getHLevelParameters(), errorReporter, "h", definition);
if (pLevels != null && definition.getPLevelParameters() == null) {
definition.setPLevelParameters(pLevels);
}
if (hLevels != null && definition.getHLevelParameters() == null) {
definition.setHLevelParameters(hLevels);
}
}
}
if (!parametersOriginalDefinitions.isEmpty()) {
paramsMap.put(definition.getData(), new Pair<>(newParams, parametersOriginalDefinitions));
}
}
for (Concrete.Definition definition : definitions) {
WhereVarsFixVisitor varsFixVisitor = new WhereVarsFixVisitor(definition, selfArgsMap);
definition.accept(varsFixVisitor, null);
var pair = paramsMap.get(definition.getData());
if (pair != null) {
if (definition instanceof Concrete.ClassDefinition) {
SubstConcreteVisitor visitor = new SubstConcreteVisitor(null);
for (int i = 0; i < pair.proj1.size(); i++) {
Concrete.Parameter param = pair.proj1.get(i);
List<Referable> newRefs = new ArrayList<>(param.getRefList().size());
pair.proj1.set(i, new Concrete.TelescopeParameter(param.getData(), param.isExplicit(), newRefs, param.getType() == null ? null : param.getType().accept(visitor, null), param.isProperty()));
for (Referable referable : param.getRefList()) {
FieldReferableImpl newRef = new FieldReferableImpl(AccessModifier.PUBLIC, Precedence.DEFAULT, referable.getRefName(), param.isExplicit(), true, true, definition.getData());
newRefs.add(newRef);
visitor.bind(referable, newRef);
}
}
definition.accept(visitor, null);
}
varsFixVisitor.visitParameters(pair.proj1, null);
definition.addParameters(pair.proj1, pair.proj2);
if (definition instanceof Concrete.BaseFunctionDefinition) {
Concrete.FunctionBody body = ((Concrete.BaseFunctionDefinition) definition).getBody();
if (body instanceof Concrete.ElimFunctionBody && body.getEliminatedReferences().isEmpty()) {
for (Concrete.FunctionClause clause : body.getClauses()) {
addParametersToClause(pair.proj1, clause);
}
}
}
if (definition instanceof Concrete.DataDefinition dataDef && dataDef.getEliminatedReferences() != null && dataDef.getEliminatedReferences().isEmpty()) {
for (Concrete.ConstructorClause clause : dataDef.getConstructorClauses()) {
addParametersToClause(pair.proj1, clause);
}
}
if (definition instanceof Concrete.CoClauseFunctionDefinition coClauseDef) {
int n = coClauseDef.getNumberOfExternalParameters();
for (Concrete.Parameter parameter : pair.proj1) {
parameter.setExplicit(false);
n += parameter.getNumberOfParameters();
}
coClauseDef.setNumberOfExternalParameters(n);
}
}
}
}