pat-lam: fix potential bug

aya-prover · Jan 15, 2025 · 7e18116 · 7e18116
1 parent 71a9d4b
commit 7e18116
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 17 deletions.
diff --git a/base/src/main/java/org/aya/resolve/salt/Desalt.java b/base/src/main/java/org/aya/resolve/salt/Desalt.java
@@ -10,13 +10,16 @@
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
 import org.aya.syntax.ref.LocalVar;
+import org.aya.util.Arg;
 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.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.util.Objects;
+
 /** Desugar, but the sugars are not sweet enough, therefore called salt. */
 public final class Desalt implements PosedUnaryOperator<Expr> {
   private final @NotNull ResolveInfo info;
@@ -75,25 +78,29 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
       case Expr.RawSort(var kind) -> new Expr.Sort(kind, 0);
       case Expr.LetOpen letOpen -> apply(letOpen.body());
       case Expr.IrrefutableLam lam -> {
-        MutableBooleanValue isVanilla = MutableBooleanValue.create(true);
-        var lamTele = lam.patterns().mapIndexed((idx, pat) -> {
-          var name = switch (pat.term().data()) {
-            case Pattern.Bind(var bind, var _) -> bind.name();
-            case Pattern.CalmFace _ -> Constants.ANONYMOUS_PREFIX;
-            default -> {
-              isVanilla.set(false);
-              yield "IrrefutableLam" + idx;
-            }
-          };
-
-          return LocalVar.generate(name, pat.term().sourcePos());
-        });
+        var isVanilla = lam.patterns().allMatch(x -> x.term().data() instanceof Pattern.Refutable);
 
+        ImmutableSeq<LocalVar> lamTele;
         WithPos<Expr> realBody;
 
-        if (isVanilla.get()) {
+        if (isVanilla) {
+          // fn a _ c => ...
+          lamTele = lam.patterns().map(x -> ((Pattern.Refutable) x.term().data()).toLocalVar(x.term().sourcePos()));
           realBody = lam.body();
         } else {
+          lamTele = lam.patterns().mapIndexed((idx, pat) -> {
+            if (pat.term().data() instanceof Pattern.Refutable refutable) {
+              var bind = refutable.toLocalVar(pat.term().sourcePos());
+              // we need fresh bind, since [bind] may be used in the body.
+              return LocalVar.generate(bind.name(), bind.definition());
+            } else {
+              return LocalVar.generate("IrrefutableLam" + idx, pat.term().sourcePos());
+            }
+          });
+
+          // fn a' _ c' => match a', _, c' { a, _, (con c) => ... }
+          // the var with prime are renamed vars
+
           realBody = new WithPos<>(sourcePos, new Expr.Match(
             lamTele.map(x -> new WithPos<>(x.definition(), new Expr.Ref(x))),
             ImmutableSeq.of(lam.clause()),

diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.concrete;
 
@@ -30,6 +30,9 @@
 public sealed interface Pattern extends AyaDocile {
   void forEach(@NotNull PosedConsumer<@NotNull Pattern> f);
   interface Salt { }
+  interface Refutable {
+    @NotNull LocalVar toLocalVar(@NotNull SourcePos pos);
+  }
 
   @NotNull Pattern descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f);
 
@@ -63,11 +66,14 @@ enum Absurd implements Pattern {
     @Override public @NotNull Pattern descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f) { return this; }
   }
 
-  enum CalmFace implements Pattern {
+  enum CalmFace implements Pattern, Refutable {
     INSTANCE;
 
     @Override public void forEach(@NotNull PosedConsumer<@NotNull Pattern> f) { }
     @Override public @NotNull Pattern descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f) { return this; }
+    @Override public @NotNull LocalVar toLocalVar(@NotNull SourcePos pos) {
+      return LocalVar.generate(pos);
+    }
   }
 
   /**
@@ -76,10 +82,13 @@ enum CalmFace implements Pattern {
   record Bind(
     @NotNull LocalVar bind,
     @ForLSP @NotNull MutableValue<@Nullable Term> type
-  ) implements Pattern {
+  ) implements Pattern, Refutable {
     public Bind(@NotNull LocalVar bind) { this(bind, MutableValue.create()); }
     @Override public void forEach(@NotNull PosedConsumer<@NotNull Pattern> f) { }
     @Override public @NotNull Bind descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f) { return this; }
+    @Override public @NotNull LocalVar toLocalVar(@NotNull SourcePos pos) {
+      return bind;
+    }
   }
 
   record Con(