test: move some tests from PatternTyckTest, add tests for allInOneN…

…oElim

base/src/main/java/org/aya/tyck/pat/ClauseTycker.java

@@ -51,7 +51,9 @@ public record TyckResult(
   }
 
   /**
-   * @param unpiedResult the result according to the pattern tycking
+   * @param unpiedResult the result according to the pattern tycking, the
+   *                     {@link DepTypeTerm.Unpi#params} is always empty if the signature result is
+   *                     {@link org.aya.tyck.pat.iter.Pusheenable.Const}
    * @param paramSubst   substitution for parameter, in the same order as parameter.
    *                     See {@link PatternTycker#paramSubst}
    * @param freePats     a free version of the patterns.

base/src/test/java/org/aya/tyck/PatternTyckTest.java

@@ -1,9 +1,8 @@
-// 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.tyck;
 
 import org.aya.prettier.AyaPrettierOptions;
-import org.intellij.lang.annotations.Language;
 import org.junit.jupiter.api.Test;
 
 import static org.aya.tyck.TyckTest.tyck;
@@ -21,133 +20,4 @@ def lind (a b : Nat) : Nat elim a
     result.forEach(def -> assertTrue(
       def.toDoc(AyaPrettierOptions.pretty()).isNotEmpty()));
   }
-
-  @Test public void test1() {
-    var result = tyck("""
-      open inductive Nat | O | S Nat
-      open inductive Vec Nat Type
-      | 0, A => vnil
-      | S n, A => infixr vcons A (Vec n A)
-      
-      def length (A : Type) (n : Nat) (v : Vec n A) : Nat elim v
-      | vnil => 0
-      | _ vcons xs => S (length _ _ xs)
-      
-      def threeTimesAhThreeTimes (A : Type) (a : A) : Vec 3 A =>
-        a vcons a vcons a vcons vnil
-      
-      def head (A : Type) (n : Nat) (v : Vec (S n) A) : A elim v
-      | x vcons _ => x
-      
-      def unwrap (A : Type) (v : Vec 1 A) : A elim v
-      | x vcons vnil => x
-      """).defs();
-
-    assertTrue(result.isNotEmpty());
-  }
-
-  @Test public void test2() {
-    var result = tyck("""
-      open inductive Nat | O | S Nat
-      
-      prim I : ISet
-      prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
-      variable A B : Type
-      def infix = (a b : A) : Type => Path (\\i => A) a b
-      def refl {a : A} : a = a => \\i => a
-      def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b => \\i => f (p i)
-      
-      overlap def infix + (a b: Nat): Nat
-      | 0, b => b
-      | a, 0 => a
-      | S a, b => S (a + b)
-      | a, S b => S (a + b)
-      tighter =
-      
-      overlap def +-comm (a b: Nat): a + b = b + a
-      | 0, _ => refl
-      | _, 0 => refl
-      | S a, b => pmap S (+-comm a b)
-      | a, S b => pmap S (+-comm a b)
-      """).defs();
-    assertTrue(result.isNotEmpty());
-  }
-
-  @Test public void test3() {
-    var result = tyck("""
-      open inductive Nat | O | S Nat
-      
-      prim I : ISet
-      prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
-      variable A B : Type
-      def infix = (a b : A) => Path (\\i => A) a b
-      def refl {a : A} : a = a => \\i => a
-      
-      overlap def infix +' (a b: Nat): Nat
-      | 0, b => b
-      | a, 0 => a
-      | S a, b => S (a +' b)
-      | a, S b => S (a +' b)
-      tighter =
-      
-      open inductive Int
-      | pos Nat | neg Nat
-      | zro : pos 0 = neg 0
-      
-      def succ Int : Int
-      | pos n => pos (S n)
-      | neg 0 => pos 1
-      | neg (S n) => neg n
-      | zro i => pos 1
-      
-      def abs Int : Nat
-      | pos n => n
-      | neg n => n
-      | zro _ => 0
-      """).defs();
-    assertTrue(result.isNotEmpty());
-  }
-
-  @Test public void test4() {
-    assertTrue(tyck("""
-      open inductive Nat | O | S Nat
-      open inductive Fin Nat
-      | 1 => fzero
-      | S n => fsucc (Fin n)
-      
-      def exfalso (A : Type) (x : Fin 0) : A elim x | ()
-      """).defs().isNotEmpty());
-  }
-
-  @Test public void issue630() {
-    assertTrue(tyck("""
-      open inductive Nat | O | S Nat
-      open inductive INat (n : Nat)
-      | O => zero
-      | S n' => +-one
-      | S (S n') => +-two
-      
-      def yes {n : Nat} (a : INat n) (b : INat n) : Nat
-      | +-one, +-two => O
-      | _, _ => S O
-      """).defs().isNotEmpty());
-  }
-
-  @Test public void test5() {
-    @Language("Aya") var code = """
-      open inductive Nat | O | S Nat
-      open inductive Vec Type Nat
-      | A, O => vnil
-      | A, S n => vcons A (Vec A n)
-      
-      open inductive MatchMe (n : Nat) (Vec Nat n)
-      | S n', vcons v xs => matched
-
-      def checkMe {n : Nat} (m : Nat) {v : Vec Nat n} (MatchMe n v) : Nat
-      | O, matched => O
-      | S m, /* {vcons _ _} ,*/ matched => O
-      """;
-
-    var result = tyck(code).defs();
-  }
 }

cli-impl/src/test/resources/success/src/Pattern.aya

@@ -0,0 +1,54 @@
+open import prelude
+import data::vec::base as vec
+
+module Test1 {
+  open vec
+  def unwrap (A : Type) (v : Vec 1 A) : A elim v
+  | x :> [] => x
+
+  def length (A : Type) (n : Nat) (v : Vec n A) : Nat elim v
+  | [] => 0
+  | _ :> xs => S (length _ _ xs)
+
+  def threeTimesAhThreeTimes (A : Type) (a : A) : Vec 3 A =>
+    a :> a :> a :> []
+}
+
+module Test4 {
+  open inductive Fin Nat
+  | 1 => fzero
+  | suc n => fsucc (Fin n)
+
+  def exfalso (A : Type) (x : Fin 0) : A elim x | ()
+}
+
+module Test5 {
+  open vec
+  open inductive MatchMe (n : Nat) (Vec n Nat)
+  | suc n', v :> xs => matched
+
+  def checkMe {n : Nat} (m : Nat) {v : Vec n Nat} (MatchMe n v) : Nat
+  | 0, matched => 0
+  | suc m, /* {vcons _ _} ,*/ matched => 0
+}
+
+module Issue630 {
+  open inductive INat (n : Nat)
+  | 0 => zro
+  | suc n' => +-one
+  | suc (suc n') => +-two
+
+  def yes {n : Nat} (a : INat n) (b : INat n) : Nat
+  | +-one, +-two => 0
+  | _, _ => 1
+}
+
+module PullRequest1268 {
+  def id (A : Type) : A -> A => fn a => a
+
+  def allInOneNoElim {A : Type} (a : A) {B : Type} (b : B) {C : Type} : Fn (D : Type) (d : D) D -> D
+  | a, b, D => fn d => id D
+
+  def elims {A : Type} (a : A) (B : Type) (b : B) {C : Type} : Fn (D : Type) D -> D elim a b
+  | a => fn b D => id D
+}