confluence: prepare for unify pat to produce a subst

aya-prover · Jan 6, 2023 · 5dfa3a0 · 5dfa3a0
1 parent 94b2f8b
commit 5dfa3a0
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 8 deletions.
diff --git a/base/src/main/java/org/aya/core/pat/PatUnify.java b/base/src/main/java/org/aya/core/pat/PatUnify.java
@@ -1,13 +1,14 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 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.core.pat;
 
-import kala.collection.SeqLike;
+import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.core.term.RefTerm;
+import org.aya.core.term.Term;
 import org.aya.core.visitor.Subst;
-import org.aya.prettier.AyaPrettierOptions;
 import org.aya.generic.util.InternalException;
+import org.aya.prettier.AyaPrettierOptions;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.LocalVar;
 import org.aya.tyck.env.LocalCtx;
@@ -18,7 +19,7 @@
  * The unification of patterns. This is <strong>not</strong> pattern unification.
  *
  * @author ice1000
- * @see PatUnify#unifyPat(SeqLike, SeqLike, Subst, Subst, LocalCtx)
+ * @see PatUnify#unifyPat(ImmutableSeq, SeqView, SeqView, Subst, Subst, LocalCtx)
  */
 public record PatUnify(@NotNull Subst lhsSubst, @NotNull Subst rhsSubst, @NotNull LocalCtx ctx) {
   private void unify(@NotNull Pat lhs, @NotNull Pat rhs) {
@@ -108,8 +109,9 @@ private static void unifyPat(Pat lhs, Pat rhs, Subst lhsSubst, Subst rhsSubst, L
    * @see PatUnify#visitAs(LocalVar, org.aya.core.pat.Pat)
    */
   public static @NotNull LocalCtx unifyPat(
-    @NotNull SeqLike<Pat> lpats,
-    @NotNull SeqLike<Pat> rpats,
+    @NotNull ImmutableSeq<Term.Param> telescope,
+    @NotNull SeqView<Pat> lpats,
+    @NotNull SeqView<Pat> rpats,
     @NotNull Subst lhsSubst,
     @NotNull Subst rhsSubst,
     @NotNull LocalCtx ctx

diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -89,7 +89,7 @@ public StmtTycker(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuild
               def = factory.apply(result.result(), Either.right(result.matchings()));
               if (!result.hasLhsError()) {
                 tracing(builder -> builder.shift(new Trace.LabelT(pos, "confluence check")));
-                PatClassifier.confluence(result, tycker, pos,
+                PatClassifier.confluence(signature.param(), result, tycker, pos,
                   PatClassifier.classify(result.clauses(), signature.param(), tycker, pos));
                 tracing(TreeBuilder::reduce);
               }

diff --git a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java b/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
@@ -90,6 +90,7 @@ public static int[] firstMatchDomination(
   }
 
   public static void confluence(
+    @NotNull ImmutableSeq<Term.Param> telescope,
     @NotNull ClauseTycker.PatResult clauses,
     @NotNull ExprTycker tycker, @NotNull SourcePos pos,
     @NotNull MCT<Term, PatErr> mct
@@ -104,7 +105,9 @@ public static void confluence(
         var rhsInfo = contents.get(i);
         var lhsSubst = new Subst();
         var rhsSubst = new Subst();
-        var ctx = PatUnify.unifyPat(lhsInfo.component2().patterns().map(Arg::term), rhsInfo.component2().patterns().map(Arg::term),
+        var ctx = PatUnify.unifyPat(telescope,
+          lhsInfo.component2().patterns().view().map(Arg::term),
+          rhsInfo.component2().patterns().view().map(Arg::term),
           lhsSubst, rhsSubst, tycker.ctx.deriveMap());
         domination(ctx, rhsSubst, tycker.reporter, lhsInfo.component1(), rhsInfo.component1(), rhsInfo.component2());
         domination(ctx, lhsSubst, tycker.reporter, rhsInfo.component1(), lhsInfo.component1(), lhsInfo.component2());