pretty: explicitize when signature is null

aya-prover · Jul 12, 2024 · 8f52aab · 8f52aab
1 parent 309bc3f
commit 8f52aab
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 28 deletions.
diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -202,7 +202,7 @@ record TakeMembers(
       var member = clazz.members().get(i);
       return TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new NewTerm(
         new ClassCall(new ClassDef.Delegate(clazz.ref()), 0,
-          ImmutableSeq.fill(clazz.members().size(), idx -> Closure.mkConst(idx < teleArgs.size() ? teleArgs.get(idx) : ErrorTerm.DUMMY))
+          ImmutableSeq.fill(clazz.members().size(), idx -> Closure.mkConst(idx < i ? teleArgs.get(idx) : ErrorTerm.DUMMY))
         )
       ))).makePi(Seq.empty());
     }

diff --git a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
@@ -22,14 +22,7 @@
 import org.aya.syntax.concrete.stmt.ModuleName;
 import org.aya.syntax.concrete.stmt.Stmt;
 import org.aya.syntax.concrete.stmt.StmtVisitor;
-import org.aya.syntax.concrete.stmt.decl.DataCon;
-import org.aya.syntax.concrete.stmt.decl.DataDecl;
-import org.aya.syntax.concrete.stmt.decl.FnDecl;
-import org.aya.syntax.concrete.stmt.decl.PrimDecl;
-import org.aya.syntax.core.def.ConDef;
-import org.aya.syntax.core.def.DataDef;
-import org.aya.syntax.core.def.FnDef;
-import org.aya.syntax.core.def.PrimDef;
+import org.aya.syntax.concrete.stmt.decl.*;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.*;
 import org.aya.util.error.Panic;
@@ -144,21 +137,15 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
   public static @NotNull DefKind kindOf(@NotNull AnyVar var) {
     return switch (var) {
       case GeneralizedVar _ -> DefKind.Generalized;
-      case DefVar<?, ?> defVar -> {
-        if (defVar.concrete instanceof FnDecl || defVar.core instanceof FnDef)
-          yield DefKind.Fn;
-//        else if (defVar.concrete instanceof TeleDecl.ClassMember || defVar.core instanceof MemberDef)
-//          yield DefKind.Member;
-        else if (defVar.concrete instanceof DataDecl || defVar.core instanceof DataDef)
-          yield DefKind.Data;
-        else if (defVar.concrete instanceof DataCon || defVar.core instanceof ConDef)
-          yield DefKind.Con;
-        else if (defVar.concrete instanceof PrimDecl || defVar.core instanceof PrimDef)
-          yield DefKind.Prim;
-//        else if (defVar.concrete instanceof ClassDecl || defVar.core instanceof ClassDef)
-//          yield DefKind.Clazz;
-        else throw new Panic(STR."unknown def type: \{defVar}");
-      }
+      case DefVar<?, ?> defVar -> switch (defVar.concrete) {
+        case FnDecl _ -> DefKind.Fn;
+        case ClassMember _ -> DefKind.Member;
+        case DataDecl _ -> DefKind.Data;
+        case DataCon _ -> DefKind.Con;
+        case PrimDecl _ -> DefKind.Prim;
+        case ClassDecl _ -> DefKind.Clazz;
+        default -> throw new Panic(STR."unknown def type: \{defVar}");
+      };
       case LocalVar(_, _, GenerateKind.Generalized(_)) -> DefKind.Generalized;
       case LocalVar _ -> DefKind.LocalVar;
       default -> DefKind.Unknown;

diff --git a/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java
@@ -7,6 +7,7 @@
 import kala.collection.SeqView;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.primitive.MutableBooleanList;
+import kala.collection.primitive.BooleanSeq;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.term.ParamLike;
 import org.aya.pretty.doc.Doc;
@@ -98,10 +99,11 @@ protected BasePrettier(@NotNull PrettierOptions options) {
 
     // Because the signature of DataCon is selfTele, so we only need to deal with core con
     var licit = switch (var) {
-      case TyckAnyDef<?> inner -> inner.core() instanceof SubLevelDef sub ?
-        sub.selfTele.mapToBoolean(MutableBooleanList.factory(), Param::explicit) :
-        Objects.requireNonNull(inner.ref.signature).params()
-          .mapToBooleanTo(MutableBooleanList.create(), Param::explicit);
+      case TyckAnyDef<?> inner -> inner.core() instanceof SubLevelDef sub
+        ? sub.selfTele.mapToBoolean(MutableBooleanList.factory(), Param::explicit)
+        : inner.ref.signature == null
+          ? BooleanSeq.fill(preArgs.size(), true)
+          : inner.ref.signature.params().mapToBooleanTo(MutableBooleanList.create(), Param::explicit);
       case JitDef jit -> MutableBooleanList.from(jit.telescopeLicit);
       default -> throw new UnsupportedOperationException("TODO");
     };