elim-data: done

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

@@ -172,10 +172,6 @@ private static <Cls> void resolveElim(@NotNull ExprResolver resolver, @NotNull M
       return;
     }
 
-    if (body.rawElims.isEmpty()) {
-      return;
-    }
-
     var resolved = body.rawElims.map(elim -> {
       var result = resolver.resolve(new QualifiedID(elim.sourcePos(), elim.data()));
       if (!(result instanceof LocalVar localVar)) {

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/negative/GoalAndMeta.txt

@@ -190,6 +190,15 @@ Error: Unable to solve the type of this literal:
 Let's learn from that.
 
 NonPattern:
+In file C:\Users\hoshino\Documents\Projects\project-aya\aya-dev\cli-impl\src\test\resources\shared\src\data\vec\base.aya:5:6 ->
+
+  3 │   open inductive Vec (n : Nat) (A : Type) elim n
+  4 │   | 0 => []
+  5 │   | suc n => infixr :> A (Vec n A)
+    │         ╰╯
+
+Warning: The name `n` shadows a previous local definition from outer scope
+
 In file $FILE:9:3 ->
 
   6 │       def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)

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

@@ -13,6 +13,15 @@ Error: Unknown constructor
 Let's learn from that.
 
 SelectionFailed:
+In file C:\Users\hoshino\Documents\Projects\project-aya\aya-dev\cli-impl\src\test\resources\shared\src\data\vec\base.aya:5:6 ->
+
+  3 │   open inductive Vec (n : Nat) (A : Type) elim n
+  4 │   | 0 => []
+  5 │   | suc n => infixr :> A (Vec n A)
+    │         ╰╯
+
+Warning: The name `n` shadows a previous local definition from outer scope
+
 In file $FILE:4:2 ->
 
   2 │   open import data::vec::base
@@ -37,7 +46,7 @@ Error: I'm unsure if there should be a case for
        as index unification is blocked for type
          Vec (<n> + <n>) A
 
-2 error(s), 0 warning(s).
+2 error(s), 1 warning(s).
 Let's learn from that.
 
 SelectionBlocked:

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

@@ -1,8 +1,8 @@
 open import prelude hiding (++)
 
-open inductive Vec Nat Type
-| 0, A => []
-| suc n, A => infixr :> A (Vec n A)
+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

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"

producer/src/main/java/org/aya/producer/AyaProducer.java

@@ -353,20 +353,28 @@ private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl
   }
 
   public @Nullable DataDecl dataDecl(GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
-    var body = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq();
+    var body = node.peekChild(ELIM_DATA_BODY);
+    if (body == null) return error(body, "Expect data body");
     var tele = telescope(node.childrenOfType(TELE));
     var info = declInfo(node, ModifierParser.DECL_FILTER);
     var name = info.checkName(this);
     if (name == null) return null;
     var ty = typeOrNull(node.peekChild(TYPE));
-    // FIXME: parse elims
-    var decl = new DataDecl(info.info, name, tele, ty, ImmutableSeq.empty(), body);
+    var decl = new DataDecl(info.info, name, tele, ty, elimDataBody(body));
     if (info.modifier.isExample()) decl.isExample = true;
     giveMeOpen(info.modifier, decl, additional);
     pragma(node, decl);
     return decl;
   }
 
+  public @NotNull MatchBody<DataCon> elimDataBody(@NotNull GenericNode<?> node) {
+    var elims = node.childrenOfType(WEAK_ID)
+      .map(this::weakId)
+      .toImmutableSeq();
+    var bodies = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq();
+    return new MatchBody<>(bodies, elims);
+  }
+
   public @Nullable DataCon dataBody(@NotNull GenericNode<?> node) {
     var dataConClause = node.peekChild(DATA_CON_CLAUSE);
     if (dataConClause != null) return dataCon(

syntax/src/main/java/org/aya/prettier/ConcretePrettier.java

@@ -434,11 +434,11 @@ else if (tighters.isEmpty()) return Doc.cat(Doc.line(), Doc.hang(2, Doc.sep(
       var elimList = elim == null
         ? body.rawElims.map(x -> Doc.plain(x.data()))
         : elim.map(BasePrettier::varDoc);
-      elimLine = Doc.sep(KW_ELIM, Doc.sep(elimList));
+      elimLine = Doc.cat(Doc.spaced(KW_ELIM), Doc.sep(elimList));
     }
 
     var clauses = Doc.emptyIf(body.clauses.isEmpty(), () -> prettier.apply(body.clauses));
-    return Doc.vcatNonEmpty(elimLine, clauses);
+    return Doc.vcat(elimLine, clauses);
   }
 
   private @NotNull Doc visitLetBind(@NotNull Expr.LetBind letBind) {

syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/DataDecl.java

@@ -27,11 +27,10 @@ public DataDecl(
     @NotNull String name,
     @NotNull ImmutableSeq<Expr.Param> telescope,
     @Nullable WithPos<Expr> result,
-    @NotNull ImmutableSeq<WithPos<String>> elims,
-    @NotNull ImmutableSeq<DataCon> body
+    @NotNull MatchBody<DataCon> body
   ) {
     super(info, telescope, result);
-    this.body = new MatchBody<>(body, elims);
+    this.body = body;
     this.ref = DefVar.concrete(this, name);
     body.forEach(con -> con.dataRef = ref);
   }

syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/MatchBody.java

@@ -41,7 +41,7 @@ public MatchBody(@NotNull ImmutableSeq<Clause> clauses, @NotNull ImmutableSeq<Wi
   }
 
   public void resolve(@NotNull ImmutableSeq<LocalVar> elims) {
-    assert this.elims != null;
+    assert this.elims == null;
     this.elims = elims;
   }