merge: Add elim for Simpl Indexed Type (#1263)

Fix #1261

base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java

@@ -108,7 +108,7 @@ public ImmutableSeq<ResolvingStmt> resolveStmt(@NotNull ImmutableSeq<Stmt> stmts
     return switch (predecl) {
       case DataDecl decl -> {
         var ctx = resolveTopLevelDecl(decl, context);
-        var innerCtx = resolveChildren(decl, ctx, d -> d.body.view(), (con, mCtx) -> {
+        var innerCtx = resolveChildren(decl, ctx, d -> d.body.clauses.view(), (con, mCtx) -> {
           setupModule(mCtx, con.ref);
           mCtx.defineSymbol(con.ref(), Stmt.Accessibility.Public, con.sourcePos());
         });

base/src/main/java/org/aya/resolve/visitor/StmtResolver.java

@@ -57,23 +57,14 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
         // Generalized works for simple bodies and signatures
         var resolver = resolveDeclSignature(info, new ExprResolver(ctx, true), decl, where);
         switch (decl.body) {
-          case FnBody.BlockBody(var cls, var elims, var rawElims) -> {
-            assert elims == null;
+          case FnBody.BlockBody body -> {
+            assert body.elims() == null;
             // introducing generalized variable is not allowed in clauses, hence we insert them before body resolving
             insertGeneralizedVars(decl, resolver);
-            var finalElims = rawElims.map(elim -> {
-              var result = resolver.resolve(new QualifiedID(elim.sourcePos(), elim.data()));
-              if (!(result instanceof LocalVar localVar)) {
-                return resolver.ctx().reportAndThrow(new NameProblem.UnqualifiedNameNotFoundError(resolver.ctx(),
-                  elim.data(), elim.sourcePos()));
-              }
-              // result is LocalVar -> result in telescope
-              return localVar;
-            });
-
+            resolveElim(resolver, body.inner());
             var clausesResolver = resolver.deriveRestrictive();
             clausesResolver.reference().append(new TyckOrder.Head(decl));
-            decl.body = new FnBody.BlockBody(cls.map(clausesResolver::clause), finalElims, rawElims);
+            decl.body = body.map(clausesResolver::clause);
             addReferences(info, new TyckOrder.Body(decl), clausesResolver);
           }
           case FnBody.ExprBody(var expr) -> {
@@ -87,6 +78,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
       case ResolvingStmt.TopDecl(DataDecl data, var ctx) -> {
         var resolver = resolveDeclSignature(info, new ExprResolver(ctx, true), data, Where.Head);
         insertGeneralizedVars(data, resolver);
+        resolveElim(resolver, data.body);
         data.body.forEach(con -> {
           var bodyResolver = resolver.deriveRestrictive();
           var mCtx = MutableValue.create(resolver.ctx());
@@ -98,8 +90,9 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
           addReferences(info, new TyckOrder.Head(con), bodyResolver);
           // No body no body but you!
         });
+
         addReferences(info, new TyckOrder.Body(data), resolver.reference().view()
-          .concat(data.body.map(TyckOrder.Body::new)));
+          .concat(data.body.clauses.map(TyckOrder.Body::new)));
       }
       case ResolvingStmt.TopDecl(ClassDecl decl, var ctx) -> {
         var resolver = new ExprResolver(ctx, false);
@@ -172,4 +165,23 @@ private static void addReferences(@NotNull ResolveInfo info, TyckOrder decl, Exp
   private static void insertGeneralizedVars(@NotNull TeleDecl decl, @NotNull ExprResolver resolver) {
     decl.telescope = decl.telescope.prependedAll(resolver.allowedGeneralizes().valuesView());
   }
+
+  private static <Cls> void resolveElim(@NotNull ExprResolver resolver, @NotNull MatchBody<Cls> body) {
+    if (body.elims() != null) {
+      // TODO: panic or just return?
+      return;
+    }
+
+    var resolved = body.rawElims.map(elim -> {
+      var result = resolver.resolve(new QualifiedID(elim.sourcePos(), elim.data()));
+      if (!(result instanceof LocalVar localVar)) {
+        return resolver.ctx().reportAndThrow(new NameProblem.UnqualifiedNameNotFoundError(resolver.ctx(),
+          elim.data(), elim.sourcePos()));
+      }
+      // result is LocalVar -> result in telescope
+      return localVar;
+    });
+
+    body.resolve(resolved);
+  }
 }

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

@@ -98,8 +98,11 @@ yield switch (fnDecl.body) {
             fnRef.signature = fnRef.signature.descent(zonker::zonk);
             yield factory.apply(Either.left(resultTerm));
           }
-          case FnBody.BlockBody(var clauses, var elims, _) -> {
+          case FnBody.BlockBody body -> {
+            var clauses = body.clauses();
+            var elims = body.elims();
             assert elims != null;
+
             var signature = fnRef.signature;
             // we do not load signature here, so we need a fresh ExprTycker
             var clauseTycker = new ClauseTycker.Worker(new ClauseTycker(tycker = mkTycker()),
@@ -137,8 +140,8 @@ yield switch (fnDecl.body) {
       }
       case DataDecl data -> {
         assert data.ref.signature != null;
-        for (var kon : data.body) checkHeader(kon);
-        yield new DataDef(data.ref, data.body.map(kon -> kon.ref.core));
+        for (var kon : data.body.clauses) checkHeader(kon);
+        yield new DataDef(data.ref, data.body.clauses.map(kon -> kon.ref.core));
       }
     };
     reporter.clearSuppress();
@@ -174,11 +177,11 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(),
         fnRef.signature = teleTycker.checkSignature(fn.telescope, result);
 
         // For ExprBody, they will be zonked later
-        if (fn.body instanceof FnBody.BlockBody(var cls, _, _)) {
+        if (fn.body instanceof FnBody.BlockBody body) {
           tycker.solveMetas();
           var zonker = new Finalizer.Zonk<>(tycker);
           fnRef.signature = fnRef.signature.pusheen(tycker::whnf).descent(zonker::zonk);
-          if (fnRef.signature.params().isEmpty() && cls.isEmpty())
+          if (fnRef.signature.params().isEmpty() && body.clauses().isEmpty())
             fail(new NobodyError(decl.sourcePos(), fn.ref));
         }
       }
@@ -239,8 +242,11 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
 
     var wellPats = ImmutableSeq.<Pat>empty();
     if (con.patterns.isNotEmpty()) {
+      var resolvedElim = dataRef.concrete.body.elims();
+      assert resolvedElim != null;
+      var indicies = ClauseTycker.Worker.computeIndices(ownerBinds, resolvedElim);
       // do not do coverage check
-      var lhsResult = new ClauseTycker(tycker = mkTycker()).checkLhs(dataSig, null,
+      var lhsResult = new ClauseTycker(tycker = mkTycker()).checkLhs(dataSig, indicies,
         new Pattern.Clause(con.entireSourcePos(), con.patterns, Option.none()), false);
       if (lhsResult.hasError()) {
         return;

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

@@ -101,15 +101,29 @@ public record Worker(
         cl.paramSubst, cl.asSubst, cl.clause, cl.hasError));
       return parent.checkAllRhs(teleVars, lhsResult);
     }
+
     private @Nullable ImmutableIntSeq computeIndices() {
-      return elims.isEmpty() ? null : elims.mapToInt(ImmutableIntSeq.factory(),
-        teleVars::indexOf);
+      return computeIndices(teleVars, elims);
     }
+
     public @NotNull TyckResult checkNoClassify() {
       return parent.checkAllRhs(teleVars, parent.checkAllLhs(computeIndices(), signature, clauses.view(), isFn));
     }
+
+    public static @Nullable ImmutableIntSeq computeIndices(
+      @NotNull ImmutableSeq<LocalVar> teleVars,
+      @NotNull ImmutableSeq<LocalVar> elims
+    ) {
+      return elims.isEmpty() ? null : elims.mapToInt(ImmutableIntSeq.factory(),
+        teleVars::indexOf);
+    }
   }
 
+  @Override public @NotNull Reporter reporter() { return exprTycker.reporter; }
+  @Override public @NotNull TyckState state() { return exprTycker.state; }
+
+  // region tycking
+
   public @NotNull ImmutableSeq<LhsResult> checkAllLhs(
     @Nullable ImmutableIntSeq indices, @NotNull Signature signature,
     @NotNull SeqView<Pattern.Clause> clauses, boolean isFn
@@ -134,20 +148,6 @@ public record Worker(
     return new TyckResult(rhsResult, lhsError);
   }
 
-  @Override public @NotNull Reporter reporter() { return exprTycker.reporter; }
-  @Override public @NotNull TyckState state() { return exprTycker.state; }
-  private @NotNull PatternTycker newPatternTycker(
-    @Nullable ImmutableIntSeq indices,
-    @NotNull SeqView<Param> telescope
-  ) {
-    telescope = indices != null
-      ? telescope.mapIndexed((idx, p) -> indices.contains(idx) ? p.explicitize() : p.implicitize())
-      : telescope;
-
-    return new PatternTycker(exprTycker, telescope, new LocalLet(), indices == null,
-      new Renamer());
-  }
-
   public @NotNull LhsResult checkLhs(
     @NotNull Signature signature,
     @Nullable ImmutableIntSeq indices,
@@ -226,6 +226,36 @@ else if (result.hasError) {
     }
   }
 
+  // endregion tycking
+
+  // region util
+
+  private @NotNull PatternTycker newPatternTycker(
+    @Nullable ImmutableIntSeq indices,
+    @NotNull SeqView<Param> telescope
+  ) {
+    telescope = indices != null
+      ? telescope.mapIndexed((idx, p) -> indices.contains(idx) ? p.explicitize() : p.implicitize())
+      : telescope;
+
+    return new PatternTycker(exprTycker, telescope, new LocalLet(), indices == null,
+      new Renamer());
+  }
+
+  private static boolean hasAbsurdity(@NotNull Pattern term) {
+    return hasAbsurdity(term, MutableBooleanValue.create());
+  }
+
+  private static boolean hasAbsurdity(@NotNull Pattern term, @NotNull MutableBooleanValue b) {
+    if (term == Pattern.Absurd.INSTANCE) b.set(true);
+    else term.forEach((_, p) -> b.set(b.get() || hasAbsurdity(p, b)));
+    return b.get();
+  }
+
+  // endregion util
+
+  // region post tycking
+
   private static final class TermInline implements UnaryOperator<Term> {
     @Override public @NotNull Term apply(@NotNull Term term) {
       if (term instanceof MetaPatTerm metaPat) {
@@ -239,14 +269,6 @@ private static final class TermInline implements UnaryOperator<Term> {
     }
   }
 
-  private static boolean hasAbsurdity(@NotNull Pattern term) {
-    return hasAbsurdity(term, MutableBooleanValue.create());
-  }
-  private static boolean hasAbsurdity(@NotNull Pattern term, @NotNull MutableBooleanValue b) {
-    if (term == Pattern.Absurd.INSTANCE) b.set(true);
-    else term.forEach((_, p) -> b.set(b.get() || hasAbsurdity(p, b)));
-    return b.get();
-  }
 
   /**
    * Inline terms which in pattern
@@ -285,4 +307,6 @@ public static void apply(@NotNull Pattern pat) {
 
     return new PatternTycker.TyckResult(wellTyped, paramSubst, result.asSubst(), result.newBody(), result.hasError());
   }
+
+  // endregion post tycking
 }

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

@@ -487,7 +487,7 @@ private record Selection(
       case DataDef.Delegate delegate -> {
         // the core may be unchecked!
         var concrete = (DataDecl) delegate.ref.concrete;
-        yield concrete.body.view()
+        yield concrete.body.clauses.view()
           .filter(it -> it.telescope.isEmpty())
           .map(it -> it.ref.name());
       }

base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java

@@ -25,6 +25,9 @@ def bar (A : Type 0) : A -> A => fn x => {? x ?}
       open inductive Fin Nat
       | S n => FZ
       | S n => FS (Fin n)
+      open inductive Vec (A : Type) (n : Nat) elim n
+      | O => vnil
+      | S m => vcons A (Vec A m)
       def infixl + Nat Nat : Nat
       | 0, a => a
       | S a, b as b' => S (a + b')

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

@@ -1,8 +1,9 @@
 open import prelude hiding (++)
 
-open inductive Vec Nat Type
-| 0, A => []
-| suc n, A => infixr :> A (Vec n A)
+@suppress(Shadowing)
+open inductive Vec (n : Nat) (A : Type) elim n
+| 0 => []
+| suc n => infixr :> A (Vec n A)
 
 variable A B : Type
 variable n m o : Nat

ide/src/main/java/org/aya/ide/Resolver.java

@@ -73,7 +73,7 @@ public interface Resolver {
 
   static @NotNull SeqView<DefVar<?, ?>> withChildren(@NotNull Decl def) {
     return switch (def) {
-      case DataDecl data -> SeqView.<DefVar<?, ?>>of(data.ref).appendedAll(data.body.map(DataCon::ref));
+      case DataDecl data -> SeqView.<DefVar<?, ?>>of(data.ref).appendedAll(data.body.clauses.map(DataCon::ref));
       // case ClassDecl struct ->
       //   SeqView.<DefVar<?, ?>>of(struct.ref).appendedAll(struct.members.map(TeleDecl.ClassMember::ref));
       default -> SeqView.of(def.ref());

parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java

@@ -41,6 +41,7 @@ public interface AyaPsiElementTypes {
   IElementType DO_BINDING = new AyaPsiElementType("DO_BINDING");
   IElementType DO_BLOCK_CONTENT = new AyaPsiElementType("DO_BLOCK_CONTENT");
   IElementType DO_EXPR = new AyaPsiElementType("DO_EXPR");
+  IElementType ELIM_DATA_BODY = new AyaPsiElementType("ELIM_DATA_BODY");
   IElementType EXPR = new AyaPsiElementType("EXPR");
   IElementType FN_BODY = new AyaPsiElementType("FN_BODY");
   IElementType FN_DECL = new AyaPsiElementType("FN_DECL");

parser/src/main/gen/org/aya/parser/AyaPsiParser.java

@@ -693,7 +693,7 @@ public static boolean dataConClause(PsiBuilder b, int l) {
   /* ********************************************************** */
   // pragma* declModifier*
   //  KW_DATA declNameOrInfix?
-  //  tele* type? bindBlock? dataBody*
+  //  tele* type? bindBlock? elimDataBody
   public static boolean dataDecl(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "dataDecl")) return false;
     boolean r, p;
@@ -706,7 +706,7 @@ public static boolean dataDecl(PsiBuilder b, int l) {
     r = p && report_error_(b, dataDecl_4(b, l + 1)) && r;
     r = p && report_error_(b, dataDecl_5(b, l + 1)) && r;
     r = p && report_error_(b, dataDecl_6(b, l + 1)) && r;
-    r = p && dataDecl_7(b, l + 1) && r;
+    r = p && elimDataBody(b, l + 1) && r;
     exit_section_(b, l, m, r, p, null);
     return r || p;
   }
@@ -765,17 +765,6 @@ private static boolean dataDecl_6(PsiBuilder b, int l) {
     return true;
   }
 
-  // dataBody*
-  private static boolean dataDecl_7(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "dataDecl_7")) return false;
-    while (true) {
-      int c = current_position_(b);
-      if (!dataBody(b, l + 1)) break;
-      if (!empty_element_parsed_guard_(b, "dataDecl_7", c)) break;
-    }
-    return true;
-  }
-
   /* ********************************************************** */
   // fnDecl | primDecl | classDecl | dataDecl
   public static boolean decl(PsiBuilder b, int l) {
@@ -862,6 +851,36 @@ public static boolean doBlockContent(PsiBuilder b, int l) {
     return r;
   }
 
+  /* ********************************************************** */
+  // elims? dataBody*
+  public static boolean elimDataBody(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "elimDataBody")) return false;
+    boolean r;
+    Marker m = enter_section_(b, l, _NONE_, ELIM_DATA_BODY, "<elim data body>");
+    r = elimDataBody_0(b, l + 1);
+    r = r && elimDataBody_1(b, l + 1);
+    exit_section_(b, l, m, r, false, null);
+    return r;
+  }
+
+  // elims?
+  private static boolean elimDataBody_0(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "elimDataBody_0")) return false;
+    elims(b, l + 1);
+    return true;
+  }
+
+  // dataBody*
+  private static boolean elimDataBody_1(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "elimDataBody_1")) return false;
+    while (true) {
+      int c = current_position_(b);
+      if (!dataBody(b, l + 1)) break;
+      if (!empty_element_parsed_guard_(b, "elimDataBody_1", c)) break;
+    }
+    return true;
+  }
+
   /* ********************************************************** */
   // KW_ELIM weakId+
   static boolean elims(PsiBuilder b, int l) {

parser/src/main/grammar/AyaPsiParser.bnf

@@ -239,7 +239,9 @@ classMember
 
 dataDecl ::= pragma* declModifier*
  KW_DATA declNameOrInfix?
- tele* type? bindBlock? dataBody* { pin=3 }
+ tele* type? bindBlock? elimDataBody { pin=3 }
+
+elimDataBody ::= elims? dataBody*
 
 dataBody ::= BAR (dataConClause | dataCon) {
   mixin="org.aya.intellij.psi.impl.AyaPsiGenericDeclImpl"