From 300148e29f25e1c5db03336cbe6128aa8362a311 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sun, 29 Dec 2024 23:48:15 +0800 Subject: [PATCH] elim-shadow: intro --- .../org/aya/resolve/visitor/ExprResolver.java | 13 ++++++++----- .../aya/resolve/visitor/PatternResolver.java | 18 +++++++++++------- .../org/aya/resolve/visitor/StmtResolver.java | 6 ++++-- 3 files changed, 23 insertions(+), 14 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java index 2157d16211..7cb0f378ae 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -22,6 +22,7 @@ import org.aya.syntax.ref.AnyVar; import org.aya.syntax.ref.DefVar; import org.aya.syntax.ref.GeneralizedVar; +import org.aya.syntax.ref.LocalVar; import org.aya.tyck.error.ClassError; import org.aya.util.error.Panic; import org.aya.util.error.PosedUnaryOperator; @@ -29,6 +30,7 @@ import org.aya.util.error.WithPos; import org.jetbrains.annotations.Contract; import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; /** * Resolves bindings. @@ -194,7 +196,7 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { // Requires exhaustiveness check, therefore must need the full data body enter(Where.FnPattern); - var clauses = match.clauses().map(this::clause); + var clauses = match.clauses().map(x -> clause(ImmutableSeq.empty(), x)); exit(); yield match.update(discriminant, clauses, returns); @@ -221,10 +223,11 @@ private void addReference(@NotNull DefVar defVar) { addReference(defVar.concrete); } - public @NotNull Pattern.Clause clause(@NotNull Pattern.Clause clause) { + public @NotNull Pattern.Clause clause(@NotNull ImmutableSeq telescope, @NotNull Pattern.Clause clause) { var mCtx = MutableValue.create(ctx); enter(Where.FnPattern); - var pats = clause.patterns.map(pa -> pa.descent(pat -> resolvePattern(pat, mCtx))); + var pats = clause.patterns.map(pa -> + pa.descent(pat -> resolvePattern(pat, telescope, mCtx))); exit(); enter(Where.FnBody); var body = clause.expr.map(x -> x.descent(enter(mCtx.get()))); @@ -232,8 +235,8 @@ private void addReference(@NotNull DefVar defVar) { return clause.update(pats, body); } - public @NotNull WithPos resolvePattern(@NotNull WithPos pattern, MutableValue ctx) { - var resolver = new PatternResolver(ctx.get(), this::addReference); + public @NotNull WithPos resolvePattern(@NotNull WithPos pattern, @NotNull ImmutableSeq telescope, MutableValue ctx) { + var resolver = new PatternResolver(ctx.get(), telescope, this::addReference); var result = pattern.descent(resolver); ctx.set(resolver.context()); return result; diff --git a/base/src/main/java/org/aya/resolve/visitor/PatternResolver.java b/base/src/main/java/org/aya/resolve/visitor/PatternResolver.java index a8cc94e215..5fd929bf1c 100644 --- a/base/src/main/java/org/aya/resolve/visitor/PatternResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/PatternResolver.java @@ -2,6 +2,7 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.resolve.visitor; +import kala.collection.immutable.ImmutableSeq; import org.aya.generic.stmt.TyckUnit; import org.aya.resolve.context.Context; import org.aya.resolve.error.NameProblem; @@ -10,10 +11,7 @@ import org.aya.syntax.concrete.stmt.ModuleName; import org.aya.syntax.concrete.stmt.decl.DataCon; import org.aya.syntax.core.def.ConDefLike; -import org.aya.syntax.ref.AnyDefVar; -import org.aya.syntax.ref.AnyVar; -import org.aya.syntax.ref.CompiledVar; -import org.aya.syntax.ref.DefVar; +import org.aya.syntax.ref.*; import org.aya.util.error.Panic; import org.aya.util.error.PosedUnaryOperator; import org.aya.util.error.SourcePos; @@ -25,10 +23,12 @@ public class PatternResolver implements PosedUnaryOperator { // DIRTY!! private @NotNull Context context; + private final @NotNull ImmutableSeq mercy; private final @NotNull Consumer parentAdd; - public PatternResolver(@NotNull Context context, @NotNull Consumer parentAdd) { + public PatternResolver(@NotNull Context context, @NotNull ImmutableSeq mercy, @NotNull Consumer parentAdd) { this.context = context; + this.mercy = mercy; this.parentAdd = parentAdd; } @@ -47,7 +47,7 @@ public PatternResolver(@NotNull Context context, @NotNull Consumer par } // It is not a constructor, it is a bind - context = context.bind(bind.bind()); + context = context.bind(bind.bind(), this::toWarn); yield bind; } case Pattern.QualifiedRef qref -> { @@ -64,13 +64,17 @@ public PatternResolver(@NotNull Context context, @NotNull Consumer par yield context.reportAndThrow(new NameProblem.QualifiedNameNotFoundError(qid.component(), qid.name(), pos)); } case Pattern.As as -> { - context = context.bind(as.as()); + context = context.bind(as.as(), this::toWarn); yield as; } default -> pat; }; } + private boolean toWarn(@Nullable AnyVar var) { + return var instanceof LocalVar && !mercy.contains(var); + } + private void addReference(@NotNull AnyDefVar defVar) { if (defVar instanceof DefVar fr) parentAdd.accept(fr.concrete); } diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index d9741b22ce..4c58dea905 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -64,7 +64,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N resolveElim(resolver, body.inner()); var clausesResolver = resolver.deriveRestrictive(); clausesResolver.reference().append(new TyckOrder.Head(decl)); - decl.body = body.map(clausesResolver::clause); + decl.body = body.map(x -> clausesResolver.clause(decl.teleVars().toImmutableSeq(), x)); addReferences(info, new TyckOrder.Body(decl), clausesResolver); } case FnBody.ExprBody(var expr) -> { @@ -84,7 +84,9 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N var mCtx = MutableValue.create(resolver.ctx()); bodyResolver.reference().append(new TyckOrder.Head(data)); bodyResolver.enter(Where.ConPattern); - con.patterns = con.patterns.map(pat -> pat.descent(pattern -> bodyResolver.resolvePattern(pattern, mCtx))); + con.patterns = con.patterns.map(pat -> + pat.descent(pattern -> + bodyResolver.resolvePattern(pattern, data.teleVars().toImmutableSeq(), mCtx))); bodyResolver.exit(); resolveMemberSignature(con, bodyResolver, mCtx); addReferences(info, new TyckOrder.Head(con), bodyResolver);