in base/src/main/java/org/arend/naming/resolving/visitor/DefinitionResolveNameVisitor.java [326:467]
public Void visitFunction(Concrete.BaseFunctionDefinition def, Scope scope) {
if (def.getStage().ordinal() >= Concrete.Stage.RESOLVED.ordinal()) {
return null;
}
scope = new PrivateFilteredScope(scope);
ExpressionResolveNameVisitor exprVisitor = resolveFunctionHeader(def, scope);
if (myResolveTypeClassReferences) return null;
if (exprVisitor == null) exprVisitor = new ExpressionResolveNameVisitor(myReferableConverter, scope, new ArrayList<>(), myLocalErrorReporter, myResolverListener, visitLevelParameters(def.getPLevelParameters()), visitLevelParameters(def.getHLevelParameters()));
List<Referable> context = exprVisitor.getContext();
checkNameAndPrecedence(def);
Concrete.FunctionBody body = def.getBody();
if (def.getResultType() != null) {
def.setResultType(def.getResultType().accept(exprVisitor, null));
}
if (def.getResultTypeLevel() != null) {
def.setResultTypeLevel(def.getResultTypeLevel().accept(exprVisitor, null));
}
if (body instanceof Concrete.TermFunctionBody) {
((Concrete.TermFunctionBody) body).setTerm(((Concrete.TermFunctionBody) body).getTerm().accept(exprVisitor, null));
}
if (body instanceof Concrete.CoelimFunctionBody) {
ClassReferable typeRef = def.getResultType() == null ? null : new TypeClassReferenceExtractVisitor().getTypeClassReference(def.getResultType());
if (typeRef != null) {
if (def.getKind() == FunctionKind.INSTANCE && typeRef.isRecord()) {
myLocalErrorReporter.report(new NameResolverError("Expected a class, got a record", def));
body.getCoClauseElements().clear();
} else {
for (Concrete.CoClauseElement element : body.getCoClauseElements()) {
if (element instanceof Concrete.ClassFieldImpl) {
exprVisitor.visitClassFieldImpl((Concrete.ClassFieldImpl) element, typeRef);
}
}
}
} else {
myLocalErrorReporter.report(def.getResultType() != null ? new NameResolverError("Expected a class", def.getResultType()) : new NameResolverError("The type of a function defined by copattern matching must be specified explicitly", def));
body.getCoClauseElements().clear();
}
}
if (body instanceof Concrete.ElimFunctionBody) {
if (def.getResultType() == null && !(def instanceof Concrete.CoClauseFunctionDefinition)) {
myLocalErrorReporter.report(new NameResolverError("The type of a function defined by pattern matching must be specified explicitly", def));
}
visitEliminatedReferences(exprVisitor, body.getEliminatedReferences());
context.clear();
if (def instanceof Concrete.CoClauseFunctionDefinition && body.getEliminatedReferences().isEmpty() && ((Concrete.CoClauseFunctionDefinition) def).getNumberOfExternalParameters() > 0) {
List<Boolean> explicitness = new ArrayList<>();
for (int i = ((Concrete.CoClauseFunctionDefinition) def).getNumberOfExternalParameters(); i < def.getParameters().size(); i++) {
for (Referable referable : def.getParameters().get(i).getReferableList()) {
((Concrete.ElimFunctionBody) body).getEliminatedReferences().add(new Concrete.ReferenceExpression(def.getData(), referable));
explicitness.add(def.getParameters().get(i).isExplicit());
}
}
for (Concrete.FunctionClause clause : body.getClauses()) {
int i = 0;
for (int j = 0; j < clause.getPatterns().size(); j++) {
Concrete.Pattern pattern = clause.getPatterns().get(j);
if (i >= explicitness.size()) break;
if (explicitness.get(i) && !pattern.isExplicit()) {
myLocalErrorReporter.report(new NameResolverError("Expected an explicit pattern", pattern));
} else {
if (!explicitness.get(i) && pattern.isExplicit()) {
clause.getPatterns().add(j, new Concrete.NamePattern(pattern.getData(), true, null, null));
}
if (!pattern.isExplicit()) {
pattern.setExplicit(true);
}
i++;
}
}
}
}
addNotEliminatedParameters(def.getParameters(), body.getEliminatedReferences(), context);
exprVisitor.visitClauses(body.getClauses(), null);
}
if (def.getKind().isUse()) {
TCReferable useParent = def.getUseParent();
boolean isFunc = useParent.getKind() == GlobalReferable.Kind.FUNCTION || useParent.getKind() == GlobalReferable.Kind.INSTANCE;
if (isFunc || useParent.getKind() == GlobalReferable.Kind.CLASS || useParent.getKind() == GlobalReferable.Kind.DATA) {
if (def.getKind() == FunctionKind.COERCE) {
if (isFunc) {
myLocalErrorReporter.report(new ParsingError(ParsingError.Kind.MISPLACED_COERCE, def));
}
if (def.getParameters().isEmpty() && def.enclosingClass == null) {
myLocalErrorReporter.report(new ParsingError(ParsingError.Kind.COERCE_WITHOUT_PARAMETERS, def));
}
}
} else {
myLocalErrorReporter.report(new ParsingError(ParsingError.Kind.MISPLACED_USE, def));
}
}
SyntacticDesugarVisitor.desugar(def, myLocalErrorReporter);
if (def instanceof Concrete.CoClauseFunctionDefinition function && def.getKind() == FunctionKind.FUNC_COCLAUSE && function.getNumberOfExternalParameters() > 0) {
BaseConcreteExpressionVisitor<Void> visitor = new BaseConcreteExpressionVisitor<>() {
@Override
public Concrete.Expression visitReference(Concrete.ReferenceExpression expr, Void params) {
if (expr.getReferent() instanceof TCReferable && ((TCReferable) expr.getReferent()).getKind() == GlobalReferable.Kind.COCLAUSE_FUNCTION) {
Concrete.GeneralDefinition definition = myConcreteProvider.getConcrete((TCReferable) expr.getReferent());
if (definition instanceof Concrete.CoClauseFunctionDefinition && ((Concrete.CoClauseFunctionDefinition) definition).getUseParent() == function.getUseParent()) {
List<Concrete.Argument> args = new ArrayList<>();
int i = 0;
loop:
for (Concrete.Parameter parameter : def.getParameters()) {
for (Referable referable : parameter.getReferableList()) {
args.add(new Concrete.Argument(new Concrete.ReferenceExpression(expr.getData(), referable), false));
if (++i >= function.getNumberOfExternalParameters()) {
break loop;
}
}
}
return Concrete.AppExpression.make(expr.getData(), expr, args);
}
}
return expr;
}
@Override
public Concrete.Expression visitApp(Concrete.AppExpression expr, Void params) {
if (expr.getArguments().get(0).isExplicit() || !(expr.getFunction() instanceof Concrete.ReferenceExpression)) {
return super.visitApp(expr, params);
}
for (Concrete.Argument argument : expr.getArguments()) {
argument.expression = argument.expression.accept(this, params);
}
return expr;
}
};
visitor.visitFunctionHeader(function, null);
}
def.setResolved();
if (myResolverListener != null) {
myResolverListener.definitionResolved(def);
}
return null;
}