merge: Jit class cp 2 (#1139)

More

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

@@ -37,7 +37,7 @@ public class TyckTest {
     var result = tyck("""
       inductive Nat | O | S Nat
       inductive FreeMonoid (A : Type) | e | cons A (FreeMonoid A)
-            
+      
       def id {A : Type} (a : A) => a
       def lam (A : Type) : Fn (a : A) -> Type => fn a => A
       def tup (A : Type) (B : A -> Type) (a : A) (b : Fn (a : A) -> B a)
@@ -66,7 +66,7 @@ def letExample (A : Type) (B : A -> Type) (f : Fn (a : A) -> B a) (a : A) : B a
       prim I : ISet
       prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
       prim coe (r s : I) (A : I -> Type) : A r -> A s
-            
+      
       def transp (A : I -> Type) (a : A 0) : A 1 => coe 0 1 A a
       def transpInv (A : I -> Type) (a : A 1) : A 0 => coe 1 0 A a
       def coeFill0 (A : I -> Type) (u : A 0) : Path A u (transp A u) => \\i => coe 0 i A u
@@ -152,7 +152,7 @@ open inductive Phantom Nat Nat (A : Type) | mk A
       prim I prim Path prim coe
       variable A : Type
       def infix = (a b : A) => Path (\\i => A) a b
-            
+      
       class Monoid
       | classifying carrier : Type
       | unit : carrier

syntax/src/main/java/org/aya/syntax/compile/JitClass.java

@@ -7,7 +7,6 @@
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.core.def.ClassDefLike;
 import org.aya.syntax.core.def.MemberDefLike;
-import org.aya.syntax.core.term.SortTerm;
 import org.aya.syntax.core.term.Term;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -21,8 +20,7 @@ protected JitClass() {
 
   public abstract @NotNull JitMember[] membars();
 
-  @Override
-  public final @NotNull ImmutableSeq<MemberDefLike> members() {
+  @Override public final @NotNull ImmutableSeq<MemberDefLike> members() {
     return ImmutableArray.Unsafe.wrap(membars());
   }
 
@@ -31,8 +29,7 @@ protected JitClass() {
     return ClassDefLike.super.telescope(i, teleArgs);
   }
 
-  @Override
-  public final @NotNull Term result(Seq<Term> teleArgs) {
+  @Override public final @NotNull Term result(Seq<Term> teleArgs) {
     return result(teleArgs.size());
   }
 }

syntax/src/main/java/org/aya/syntax/compile/JitMember.java

@@ -25,15 +25,7 @@ protected JitMember(
     this.type = type;
   }
 
-  @Override
-  public @NotNull ClassDefLike classRef() {
-    return classRef;
-  }
-
-  @Override
-  public @NotNull SortTerm type() { return type; }
-  @Override
-  public int index() {
-    return index;
-  }
+  @Override public @NotNull ClassDefLike classRef() { return classRef; }
+  @Override public @NotNull SortTerm type() { return type; }
+  @Override public int index() { return index; }
 }

syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java

@@ -21,7 +21,7 @@
  *     v                    v                   v                  v
  *   ConDef  <- - -  ConDef.Delegate <----- ConDefLike ----->    JitCon
  * </pre>
- * where the arrows indicate mean "is superclass of".<br/>
+ * where the arrows mean "is superclass of".<br/>
  * <ul>
  *   <li>The first chain is "core def" chain, which are well-typed definition</li>
  *   <li>The second chain is "local def" chain, which may refer to a not yet tycked definition, i.e. tyck a recursive function</li>

syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java

@@ -15,7 +15,7 @@ public sealed interface ClassDefLike extends AnyDef permits JitClass, ClassDef.D
 
   default @NotNull Term telescope(int i, @NotNull Seq<Term> restriction) {
     var member = members().get(i);
-    // Our code should not refer the subterm of self, the only meaningful part is [self.forget()]
+    // Our code should not refer the subterm of [self], the only meaningful part is [self.forget()]
     // Also, we don't use NewTerm, cause the type of the self-parameter is a class call without any restriction.
     var self = new ClassCastTerm(this, ErrorTerm.DUMMY, ImmutableSeq.empty(),
       restriction.map(Closure::mkConst)

syntax/src/main/java/org/aya/syntax/core/def/MemberDefLike.java

@@ -8,6 +8,10 @@
 
 public sealed interface MemberDefLike extends AnyDef permits JitMember, MemberDef.Delegate {
   @NotNull ClassDefLike classRef();
+
+  /**
+   * The type of the type of this member, not include self-parameter
+   */
   @NotNull SortTerm type();
 
   int index();