resolve: test passed for variable rules

aya-prover · Jan 7, 2025 · 3522916 · 3522916
1 parent ea8793a
commit 3522916
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 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
@@ -280,10 +280,13 @@ private void introduceDependencies(@NotNull GeneralizedVar var) {
   public @NotNull AnyVar resolve(@NotNull QualifiedID name) {
     var result = ctx.get(name);
     if (result instanceof GeneralizedVar gvar) {
-      // Ensure all dependencies are introduced
-      introduceDependencies(gvar);
       var gened = allowedGeneralizes.getOrNull(gvar);
       if (gened != null) return gened.ref();
+      if (!allowGeneralizing) {
+        ctx.reporter().report(new GeneralizedNotAvailableError(name.sourcePos(), gvar));
+        throw new Context.ResolvingInterruptedException();
+      }
+      introduceDependencies(gvar);
     }
     return result;
   }

diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java
@@ -38,7 +38,8 @@ static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info)
       case ResolvingStmt.ResolvingDecl decl -> resolveDecl(decl, info);
       case ResolvingStmt.ModStmt(var stmts) -> resolveStmt(stmts, info);
       case ResolvingStmt.GenStmt(var variables) -> {
-        var resolver = new ExprResolver(info.thisModule(), false);
+        // Create resolver with allowGeneralizing=true for variable declarations
+        var resolver = new ExprResolver(info.thisModule(), true);
         resolver.enter(Where.Head);
 
         // First pass: register all variables to detect cycles