merge: Quotient and fmset ++-assoc (#1103)

base/src/main/java/org/aya/tyck/ExprTycker.java

@@ -102,7 +102,7 @@ case PiTerm(var dom, var cod) -> {
         var freshHole = freshMeta(Constants.randomName(hole), expr.sourcePos(), new MetaVar.OfType(type));
         hole.solution().set(freshHole);
         userHoles.append(new WithPos<>(expr.sourcePos(), hole));
-        if (hole.explicit()) fail(new Goal(state, freshHole, hole.accessibleLocal()));
+        if (hole.explicit()) fail(new Goal(state, freshHole, localCtx().clone(), hole.accessibleLocal()));
         yield new Jdg.Default(freshHole, type);
       }
       case Expr.LitInt(var end) -> {
@@ -152,15 +152,15 @@ case PiTerm(var dom, var cod) -> {
         return new Jdg.Default(new LamTerm(closure), eq);
       }
     }
-    unifyTyReported(type, resultType, expr);
-    return result;
+    if (unifyTyReported(type, resultType, expr)) return result;
+    return new Jdg.Default(new ErrorTerm(result.wellTyped()), type);
   }
 
   public @NotNull Term ty(@NotNull WithPos<Expr> expr) {
     return switch (expr.data()) {
       case Expr.Hole hole -> {
         var meta = freshMeta(Constants.randomName(hole), expr.sourcePos(), MetaVar.Misc.IsType);
-        if (hole.explicit()) fail(new Goal(state, meta, hole.accessibleLocal()));
+        if (hole.explicit()) fail(new Goal(state, meta, localCtx().clone(), hole.accessibleLocal()));
         yield meta;
       }
       case Expr.Sort sort -> new SortTerm(sort.kind(), sort.lift());

base/src/main/java/org/aya/tyck/error/Goal.java

@@ -8,6 +8,7 @@
 import org.aya.syntax.core.term.FreeTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.call.MetaCall;
+import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.syntax.ref.MetaVar;
 import org.aya.tyck.TyckState;
@@ -19,7 +20,7 @@
 
 public record Goal(
   @Override @NotNull TyckState state, @NotNull MetaCall hole,
-  @NotNull ImmutableSeq<LocalVar> scope
+  @NotNull LocalCtx ctx, @NotNull ImmutableSeq<LocalVar> scope
 ) implements Problem, Stateful {
   @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
     var meta = hole.ref();
@@ -48,9 +49,11 @@ public record Goal(
   }
   private @NotNull Doc renderScopeVar(@NotNull PrettierOptions options, Term arg) {
     var paramDoc = freezeHoles(arg).toDoc(options);
-    var scopeInfo = arg instanceof FreeTerm(var ref) && scope.contains(ref)
-      ? paramDoc : Doc.sep(paramDoc, Doc.parened(Doc.english("not in scope")));
-    return Doc.par(1, scopeInfo);
+    if (arg instanceof FreeTerm(var ref)) {
+      if (ctx.contains(ref)) paramDoc = Doc.sep(paramDoc, Doc.symbol(":"), ctx.get(ref).toDoc(options));
+      if (!scope.contains(ref)) paramDoc = Doc.sep(paramDoc, Doc.parened(Doc.english("not in scope")));
+    }
+    return Doc.par(1, paramDoc);
   }
 
   @Override public @NotNull SourcePos sourcePos() { return hole.ref().pos(); }

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

@@ -310,24 +310,19 @@ record PushTelescope(@NotNull ImmutableSeq<Pat> wellTyped, @NotNull WithPos<Expr
       foundError(new PatternProblem.TooManyPattern(pattern.term()));
     }
 
-    boolean needGenPat = true;
+    // the telescope may end with implicit parameters
+    // loop invariant: [currentParam] is the next unchecked parameter if not null
+    while (currentParam != null && !currentParam.explicit()) {
+      wellTyped.append(generatePattern());
+      // [currentParam] is checked!
+      moveNext();
+      // [currentParam] is unchecked if not null.
+    }
 
-    if (body != null) {
+    if (currentParam != null && body != null) {
       var result = pushTelescope(body);
       wellTyped.appendAll(result.wellTyped);
       body = result.newBody;
-      needGenPat = result.wellTyped.isEmpty();
-    }
-
-    if (needGenPat) {
-      // the telescope may ends with implicit parameters
-      // loop invariant: [currentParam] is the next unchecked parameter if not null
-      while (currentParam != null && !currentParam.explicit()) {
-        wellTyped.append(generatePattern());
-        // [currentParam] is checked!
-        moveNext();
-        // [currentParam] is unchecked if not null.
-      }
     }
 
     // [currentParam] is the next unchecked parameter if not null

base/src/main/java/org/aya/unify/Synthesizer.java

@@ -48,7 +48,7 @@ public boolean inheritPiDom(@NotNull Term ty, @NotNull SortTerm expected) {
     return switch (tyty.kind()) {
       case Type -> expected.kind() == SortKind.Type && tyty.lift() <= expected.lift();
       case Set -> expected.kind() == SortKind.Set && tyty.lift() <= expected.lift();
-      case ISet -> Panic.unreachable();
+      case ISet -> expected.kind() == SortKind.Type;
     };
   }
 

base/src/main/java/org/aya/unify/TermComparator.java

@@ -160,7 +160,7 @@ private boolean checkApproxResult(@Nullable Term type, Term approxResult) {
    * @return whether they are 'the same' and their types are {@param type}
    */
   private boolean doCompareTyped(@NotNull Term lhs, @NotNull Term rhs, @NotNull Term type) {
-    return switch (type) {
+    return switch (whnf(type)) {
       // TODO: ClassCall
       case LamTerm _, ConCallLike _, TupTerm _ -> Panic.unreachable();
       case ErrorTerm _ -> true;
@@ -206,15 +206,15 @@ case SigmaTerm(var paramSeq) -> {
   private @Nullable Term compareUntyped(@NotNull Term preLhs, @NotNull Term preRhs) {
     {
       var result = compareApprox(preLhs, preRhs);
-      if (result != null) return result;
+      if (result != null) return whnf(result);
       failure = null;
     }
 
     var lhs = whnf(preLhs);
     var rhs = whnf(preRhs);
     if (!(lhs == preLhs && rhs == preRhs)) {
       var result = compareApprox(lhs, rhs);
-      if (result != null) return result;
+      if (result != null) return whnf(result);
     }
 
     Term result;
@@ -337,12 +337,12 @@ private boolean compareLambda(@NotNull LamTerm lambda, @NotNull Term rhs, @NotNu
     for (var i = 0; i < types.telescopeSize(); ++i) {
       var l = list.get(i);
       var r = rist.get(i);
-      var ty = whnf(types.telescope(i, argsCum));
+      var ty = types.telescope(i, argsCum);
       if (!compare(l, r, ty)) return null;
       argsCum[i] = l;
     }
 
-    return whnf(types.result(argsCum));
+    return types.result(argsCum);
   }
 
   /**

cli-impl/src/test/resources/negative/GoalAndMeta.txt

@@ -21,7 +21,7 @@ Goal: Goal of type
         Nat
         (Normalized: Nat)
       Context:
-        a
+        a : Nat
 
 In file $FILE:2:28 ->
 
@@ -146,8 +146,8 @@ In file $FILE:7:41 ->
 Error: Cannot check the expression
          g 0
        of type
-         F (Neg 0)
-         (Normalized: F (0 → Empty))
+         F (Neg <X>)
+         (Normalized: F (<X> → Empty))
        against the type
          Nat
 
@@ -160,7 +160,7 @@ In file $FILE:7:15 ->
 
 Error: Unsolved meta _
        in `^0 (?_ ^0)`
-       in `Fn (y : ^0 (?_ ^0)) → ^1 (Neg y)`
+       in `^0 (?_ ^0) → ^1 (Neg <X>)`
 
 4 error(s), 0 warning(s).
 What are you doing?

cli-impl/src/test/resources/shared/src/algebra/free-group.aya

@@ -0,0 +1,12 @@
+open import prelude
+
+open inductive FreeGroup (A : Type)
+| η A
+| infixl · (a b : FreeGroup A) tighter =
+| ε
+| inv (FreeGroup A)
+| assoc (x y z : FreeGroup A) : x · (y · z) = (x · y) · z
+| idr (x : FreeGroup A) : x = x · ε
+| idl (x : FreeGroup A) : x = ε · x
+| invr (x : FreeGroup A) : x · (inv x) = ε
+| invl (x : FreeGroup A) : (inv x) · x = ε

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

@@ -13,3 +13,8 @@ overlap def infixr ++ (xs ys : FMSet A) : FMSet A
 | x :] xs', _ => x :] xs' ++ ys
 | comm x y xs' i, _ => comm x y (xs' ++ ys) i
 tighter :] =
+
+def ++-assoc {xs ys zs : FMSet A} : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs elim xs
+| [] => refl
+| x :] xs' => pmap (x :]) ++-assoc
+| comm x y xs' i => fn j => comm x y (++-assoc j) i

cli-impl/src/test/resources/shared/src/relation/binary/quotient.aya

@@ -0,0 +1,12 @@
+open import prelude hiding (map)
+
+open inductive infix / (A : Type) (R : Fn (a b : A) → Type) tighter =
+| in~ A
+| eq~ {a b : A} (R a b) : in~ a = in~ b
+
+variable A B : Type
+
+def map {R : ∀ a b → Type} {Q : ∀ a b → Type} (f : A → B)
+        (p : ∀ a a' → R a a' → Q (f a) (f a')) (q : A / R) : B / Q elim q
+| in~ a => in~ (f a)
+| eq~ r i => eq~ (p _ _ r) i

tools-repl/src/main/java/org/aya/repl/Repl.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
+// Copyright (c) 2020-2024 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.repl;
 
@@ -47,7 +47,5 @@ default boolean loop(@NotNull String prompt, @NotNull CommandManager commandMana
     return true;
   }
 
-  default @NotNull String renderDoc(@NotNull Doc doc) {
-    return doc.debugRender();
-  }
+  @NotNull String renderDoc(@NotNull Doc doc);
 }