elim-shadow: intro

aya-prover · Dec 29, 2024 · 300148e · 300148e
1 parent 50413bd
commit 300148e
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 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
@@ -22,13 +22,15 @@
 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;
 import org.aya.util.error.SourcePos;
 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,19 +223,20 @@ 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<LocalVar> 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())));
     exit();
     return clause.update(pats, body);
   }
 
-  public @NotNull WithPos<Pattern> resolvePattern(@NotNull WithPos<Pattern> pattern, MutableValue<Context> ctx) {
-    var resolver = new PatternResolver(ctx.get(), this::addReference);
+  public @NotNull WithPos<Pattern> resolvePattern(@NotNull WithPos<Pattern> pattern, @NotNull ImmutableSeq<LocalVar> telescope, MutableValue<Context> 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
@@ -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<Pattern> {
   // DIRTY!!
   private @NotNull Context context;
+  private final @NotNull ImmutableSeq<LocalVar> mercy;
   private final @NotNull Consumer<TyckUnit> parentAdd;
 
-  public PatternResolver(@NotNull Context context, @NotNull Consumer<TyckUnit> parentAdd) {
+  public PatternResolver(@NotNull Context context, @NotNull ImmutableSeq<LocalVar> mercy, @NotNull Consumer<TyckUnit> parentAdd) {
     this.context = context;
+    this.mercy = mercy;
     this.parentAdd = parentAdd;
   }
 
@@ -47,7 +47,7 @@ public PatternResolver(@NotNull Context context, @NotNull Consumer<TyckUnit> 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<TyckUnit> 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
@@ -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);