merge: More things in the lib, handle empty patterns (#1095)

cli-impl/src/test/resources/shared/src/arith/nat.aya

@@ -0,0 +1,2 @@
+public open import arith::nat::base
+public open import arith::nat::properties

cli-impl/src/test/resources/shared/src/arith/nat/base.aya

@@ -2,23 +2,31 @@ open import paths
 
 open inductive Nat | zero | suc Nat
 
+variable a b c : Nat
+
 overlap def infixl + Nat Nat : Nat
 | 0, b => b
 | a, 0 => a
 | suc a, b => suc (a + b)
 | a, suc b => suc (a + b)
 tighter =
 
-overlap def +-comm {a b : Nat} : a + b = b + a elim a b
+overlap def +-comm : a + b = b + a elim a b
 | 0, _ => refl
 | suc _, _ => pmap suc +-comm
 | _, 0 => refl
 | _, suc _ => pmap suc +-comm
 
-overlap def +-assoc {a b c : Nat} : a + (b + c) = (a + b) + c elim a b c
+overlap def +-assoc : a + (b + c) = (a + b) + c elim a b c
 | 0, _, _ => refl
 | _, 0, _ => refl
 | _, _, 0 => refl
 | suc _, _, _ => pmap suc +-assoc
 | _, suc _, _ => pmap suc +-assoc
 | _, _, suc _ => pmap suc +-assoc
+
+overlap def infixl * Nat Nat : Nat
+| 0, n => 0
+| m, 0 => 0
+| suc m, n => n + m * n
+tighter +

cli-impl/src/test/resources/shared/src/arith/nat/properties.aya

@@ -0,0 +1,16 @@
+open import arith::nat::base
+open import data::empty
+open import paths
+
+private def diag Nat : Type
+| 0 => Nat
+| suc a => Empty
+
+def z≠s {a : Nat} (p : 0 = suc a) : Empty => coe 0 1 (\i => diag (p i)) a
+
+private def suc-inj Nat : Nat
+| 0 => 114514
+| suc m => m
+
+def s=s {m n : Nat} (p : suc m = suc n) : m = n => (\i => suc-inj (p i))
+

cli-impl/src/test/resources/shared/src/data/empty.aya

@@ -0,0 +1,4 @@
+inductive Empty
+variable A : Type
+
+def exfalso Empty : A | ()

cli-impl/src/test/resources/shared/src/data/list/base.aya

@@ -5,7 +5,7 @@ open inductive List (A : Type)
 | nil
 | infixr :< A (List A) tighter =
 
-variable A B : Type
+variable A B C : Type
 
 def length (List A) : Nat
 | [ ] => 0
@@ -19,3 +19,19 @@ def infixr ++ (xs ys : List A) : List A
 def map (f : A -> B) (xs : List A) : List B elim xs
 | [ ] => [ ]
 | x :< xs' => f x :< map f xs'
+
+def length-map (f : A -> B) (l : List A) : length (map f l) = length l elim l
+| [ ] => refl
+| x :< xs => pmap suc (length-map f xs)
+
+def map-comp (g : B -> C) (f : A -> B) (l : List A) : map (\x => g (f x)) l = map g (map f l) elim l
+| [ ] => refl
+| x :< xs => pmap (g (f x) :<) (map-comp g f xs)
+
+def map-id (l : List A) : map (\x => x) l = l
+| [ ] => refl
+| x :< xs => pmap (x :<) (map-id xs)
+
+def head-def (x : A) (xs : List A) : A elim xs
+| [ ] => x
+| a :< _ => a

jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java

@@ -7,9 +7,8 @@
 import kala.collection.immutable.primitive.ImmutableIntSeq;
 import kala.range.primitive.IntRange;
 import kala.value.primitive.MutableIntValue;
-import org.aya.generic.NameGenerator;
-import org.aya.normalize.PatMatcher;
 import org.aya.generic.State;
+import org.aya.normalize.PatMatcher;
 import org.aya.syntax.core.pat.Pat;
 import org.aya.syntax.core.term.MetaPatTerm;
 import org.aya.util.error.Panic;
@@ -230,8 +229,11 @@ private int bindAmount(@NotNull ImmutableSeq<Pat> pats) {
 
   /// endregion Java Source Code Generate API
 
-  @Override
-  public PatternSerializer serialize(@NotNull ImmutableSeq<Matching> unit) {
+  @Override public PatternSerializer serialize(@NotNull ImmutableSeq<Matching> unit) {
+    if (unit.isEmpty()) {
+      onMismatch.accept(this);
+      return this;
+    }
     var bindSize = unit.mapToInt(ImmutableIntSeq.factory(), x -> bindAmount(x.patterns));
     int maxBindSize = bindSize.max();