Struct WIP

base/src/main/java/org/aya/concrete/Expr.java

@@ -179,6 +179,12 @@ public RefExpr(@NotNull SourcePos sourcePos, @NotNull Var resolvedVar) {
 
   }
 
+  record SelfExpr(
+    @NotNull SourcePos sourcePos,
+    @Nullable Var resolvedStruct
+  ) implements Expr {
+  }
+
   record LiftExpr(@NotNull SourcePos sourcePos, @NotNull Expr expr, int lift) implements Expr {}
 
   /**

base/src/main/java/org/aya/concrete/stmt/ClassDecl.java

@@ -2,9 +2,22 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.stmt;
 
+import kala.collection.Map;
+import kala.collection.immutable.ImmutableMap;
+import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableHashMap;
+import kala.collection.mutable.MutableMap;
+import kala.control.Option;
 import org.aya.concrete.Expr;
+import org.aya.concrete.Pattern;
 import org.aya.core.def.ClassDef;
+import org.aya.core.def.Def;
+import org.aya.core.def.FieldDef;
+import org.aya.core.def.StructDef;
+import org.aya.core.term.StructCall;
+import org.aya.ref.DefVar;
 import org.aya.resolve.context.Context;
+import org.aya.util.MutableGraph;
 import org.aya.util.binop.OpDecl;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
@@ -16,7 +29,7 @@
  * @author zaoqi
  * @see Decl
  */
-public non-sealed/*sealed*/ abstract class ClassDecl extends CommonDecl implements Decl.Resulted, Decl.TopLevel {
+public sealed abstract class ClassDecl extends CommonDecl implements Decl.Resulted, Decl.TopLevel {
   private final @NotNull Decl.Personality personality;
   public @Nullable Context ctx = null;
   public @NotNull Expr result;
@@ -58,4 +71,151 @@ protected ClassDecl(
   @Override public String toString() {
     return getClass().getSimpleName() + "[" + ref().name() + "]";
   }
+
+  /**
+   * Concrete structure definition
+   *
+   * @author vont
+   */
+  public static final class StructDecl extends ClassDecl {
+    public final @NotNull DefVar<StructDef, StructDecl> ref;
+    public @NotNull
+    final ImmutableSeq<StructField> fields;
+    // `StructCall`s
+    // This will be desugared so StructDef doesn't need to store this.
+    public final @NotNull ImmutableSeq<Expr> parents;
+    // set in tyck
+    // rootRef -> StructField
+    public @Nullable ImmutableMap<DefVar<FieldDef, StructField>, StructField> fieldMap = null;
+    public int ulift;
+
+    public @NotNull ImmutableMap<DefVar<FieldDef, StructField>, StructField> calculateFieldMap(
+      @NotNull ImmutableSeq<StructCall> parents
+    ) {
+      if (fieldMap == null) fieldMap = collectFields(parents).toImmutableMap();
+      return fieldMap;
+    }
+
+    private @NotNull MutableMap<DefVar<FieldDef, StructField>, StructField> collectFields(@NotNull ImmutableSeq<StructCall> parents) {
+      var fieldMap = MutableMap.create();
+      for (var parent : parents) {
+        // TODO: diamond inheritance
+        var implicitOverrides = parent.params();
+        var implicitFields = implicitOverrides.map(t -> new StructField(t._1.concrete, (Expr) (Object) t._2.term())); // TODO: implement this
+        parent.ref().concrete.fieldMap.forEach((field, structField) -> {
+          var x = fieldMap.put(field.concrete.rootRef, structField);
+          if (x.isDefined()) {
+            throw new IllegalStateException("Duplicate field: " + field); // TODO: better error
+          }
+        });
+        implicitFields.forEach(field -> {
+          var x = fieldMap.put(field.rootRef, field);
+          if (x.isDefined()) {
+            throw new IllegalStateException("Duplicate field: " + field); // TODO: better error
+          }
+        });
+      }
+    }
+
+    public StructDecl(
+      @NotNull SourcePos sourcePos, @NotNull SourcePos entireSourcePos,
+      @NotNull Accessibility accessibility,
+      @Nullable OpInfo opInfo,
+      @NotNull String name,
+      @NotNull Expr result,
+      @NotNull ImmutableSeq<Expr> parents,
+      @NotNull ImmutableSeq<StructField> fields,
+      @NotNull BindBlock bindBlock,
+      @NotNull Decl.Personality personality
+    ) {
+      super(sourcePos, entireSourcePos, opInfo, bindBlock, result, personality, accessibility);
+      this.parents = parents;
+      this.fields = fields;
+      this.ref = DefVar.concrete(this, name);
+      fields.forEach(field -> field.structRef = ref);
+    }
+
+    @Override public @NotNull DefVar<StructDef, StructDecl> ref() {
+      return ref;
+    }
+
+    public static final class StructField extends CommonDecl implements Decl.Telescopic, Decl.Resulted {
+      public final @NotNull DefVar<FieldDef, StructField> rootRef;
+      public final @NotNull Option<DefVar<FieldDef, StructField>> parentRef;
+      public final @NotNull DefVar<FieldDef, StructField> ref;
+      public DefVar<StructDef, StructDecl> structRef;
+      public @NotNull ImmutableSeq<Pattern.Clause> clauses;
+      public @NotNull Expr result;
+      public @NotNull Option<Expr> body;
+      public final boolean coerce;
+
+      // will change after resolve
+      public @NotNull ImmutableSeq<Expr.Param> telescope;
+      public @Nullable Def.Signature signature;
+
+      public StructField(
+        @NotNull SourcePos sourcePos, @NotNull SourcePos entireSourcePos,
+        @Nullable OpInfo opInfo,
+        @NotNull String name,
+        @NotNull ImmutableSeq<Expr.Param> telescope,
+        @NotNull Expr result,
+        @NotNull Option<Expr> body,
+        @NotNull ImmutableSeq<Pattern.Clause> clauses,
+        boolean coerce,
+        @NotNull BindBlock bindBlock
+      ) {
+        super(sourcePos, entireSourcePos, Accessibility.Public, opInfo, bindBlock);
+        this.coerce = coerce;
+        this.result = result;
+        this.clauses = clauses;
+        this.body = body;
+        this.ref = DefVar.concrete(this, name);
+        this.rootRef = this.ref;
+        this.parentRef = Option.none();
+        this.telescope = telescope;
+      }
+
+      public StructField(@NotNull StructField parent, @NotNull Expr result) {
+        super(parent.sourcePos, parent.entireSourcePos, Accessibility.Public, parent.opInfo, parent.bindBlock);
+        if (parent.telescope.isNotEmpty() || parent.body.isDefined() || parent.clauses.isNotEmpty() || parent.coerce)
+          throw new UnsupportedOperationException("TODO");
+        this.coerce = parent.coerce;
+        this.result = result;
+        this.clauses = parent.clauses;
+        this.body = parent.body;
+        this.ref = DefVar.concrete(this, parent.ref.name());
+        this.rootRef = parent.rootRef;
+        this.parentRef = Option.some(parent.ref);
+        this.telescope = parent.telescope;
+      }
+
+      @Override public @NotNull DefVar<FieldDef, StructField> ref() {
+        return ref;
+      }
+
+      @Override public @NotNull ImmutableSeq<Expr.Param> telescope() {
+        return telescope;
+      }
+
+      @Override public void setTelescope(@NotNull ImmutableSeq<Expr.Param> telescope) {
+        this.telescope = telescope;
+      }
+
+      @Override public @Nullable Def.Signature signature() {
+        return signature;
+      }
+
+      @Override public void setSignature(Def.@Nullable Signature signature) {
+        this.signature = signature;
+      }
+
+      @Override public @NotNull Expr result() {
+        return result;
+      }
+
+      @Override public void setResult(@NotNull Expr result) {
+        this.result = result;
+      }
+    }
+  }
 }

base/src/main/java/org/aya/concrete/stmt/CommonDecl.java

@@ -14,7 +14,7 @@
  * @apiNote This class should only be used in extends and permits clause. Use {@link Decl} elsewhere instead.
  * @see Decl
  */
-public sealed abstract class CommonDecl implements Decl permits ClassDecl, TeleDecl, TeleDecl.DataCtor, TeleDecl.StructField {
+public sealed abstract class CommonDecl implements Decl permits ClassDecl, TeleDecl, TeleDecl.DataCtor, ClassDecl.StructDecl.StructField {
   public final @NotNull Accessibility accessibility;
   public final @NotNull SourcePos sourcePos;
   public final @NotNull SourcePos entireSourcePos;

base/src/main/java/org/aya/concrete/stmt/Decl.java

@@ -71,7 +71,7 @@ enum Personality {
    *
    * @author kiva
    */
-  sealed interface Telescopic permits TeleDecl, TeleDecl.DataCtor, TeleDecl.StructField {
+  sealed interface Telescopic permits TeleDecl, TeleDecl.DataCtor, ClassDecl.StructDecl.StructField {
     @NotNull ImmutableSeq<Expr.Param> telescope();
     void setTelescope(@NotNull ImmutableSeq<Expr.Param> telescope);
     @Nullable Def.Signature signature();
@@ -94,7 +94,7 @@ sealed interface TopLevel permits ClassDecl, TeleDecl {
    *
    * @author kiva
    */
-  sealed interface Resulted permits ClassDecl, TeleDecl, TeleDecl.StructField {
+  sealed interface Resulted permits ClassDecl, TeleDecl, ClassDecl.StructDecl.StructField {
     @NotNull Expr result();
     void setResult(@NotNull Expr result);
   }

base/src/main/java/org/aya/concrete/stmt/TeleDecl.java

@@ -5,7 +5,6 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import kala.control.Either;
-import kala.control.Option;
 import org.aya.concrete.Expr;
 import org.aya.concrete.Pattern;
 import org.aya.core.def.*;
@@ -210,101 +209,6 @@ public DataDecl(
     }
   }
 
-  /**
-   * Concrete structure definition
-   *
-   * @author vont
-   */
-  public static final class StructDecl extends TeleDecl {
-    public final @NotNull DefVar<StructDef, StructDecl> ref;
-    public @NotNull
-    final ImmutableSeq<StructField> fields;
-    public int ulift;
-
-    public StructDecl(
-      @NotNull SourcePos sourcePos, @NotNull SourcePos entireSourcePos,
-      @NotNull Accessibility accessibility,
-      @Nullable OpInfo opInfo,
-      @NotNull String name,
-      @NotNull ImmutableSeq<Expr.Param> telescope,
-      @NotNull Expr result,
-      // @NotNull ImmutableSeq<String> superClassNames,
-      @NotNull ImmutableSeq<StructField> fields,
-      @NotNull BindBlock bindBlock,
-      @NotNull Decl.Personality personality
-    ) {
-      super(sourcePos, entireSourcePos, accessibility, opInfo, bindBlock, telescope, result, personality);
-      this.fields = fields;
-      this.ref = DefVar.concrete(this, name);
-      fields.forEach(field -> field.structRef = ref);
-    }
-
-    @Override public @NotNull DefVar<StructDef, StructDecl> ref() {
-      return ref;
-    }
-  }
-
-  public static final class StructField extends CommonDecl implements Decl.Telescopic, Decl.Resulted {
-    public final @NotNull DefVar<FieldDef, TeleDecl.StructField> ref;
-    public DefVar<StructDef, StructDecl> structRef;
-    public @NotNull ImmutableSeq<Pattern.Clause> clauses;
-    public @NotNull Expr result;
-    public @NotNull Option<Expr> body;
-    public final boolean coerce;
-
-    // will change after resolve
-    public @NotNull ImmutableSeq<Expr.Param> telescope;
-    public @Nullable Def.Signature signature;
-
-    public StructField(
-      @NotNull SourcePos sourcePos, @NotNull SourcePos entireSourcePos,
-      @Nullable OpInfo opInfo,
-      @NotNull String name,
-      @NotNull ImmutableSeq<Expr.Param> telescope,
-      @NotNull Expr result,
-      @NotNull Option<Expr> body,
-      @NotNull ImmutableSeq<Pattern.Clause> clauses,
-      boolean coerce,
-      @NotNull BindBlock bindBlock
-    ) {
-      super(sourcePos, entireSourcePos, Accessibility.Public, opInfo, bindBlock);
-      this.coerce = coerce;
-      this.result = result;
-      this.clauses = clauses;
-      this.body = body;
-      this.ref = DefVar.concrete(this, name);
-      this.telescope = telescope;
-    }
-
-    @Override public @NotNull DefVar<FieldDef, StructField> ref() {
-      return ref;
-    }
-
-    @Override public @NotNull ImmutableSeq<Expr.Param> telescope() {
-      return telescope;
-    }
-
-    @Override public void setTelescope(@NotNull ImmutableSeq<Expr.Param> telescope) {
-      this.telescope = telescope;
-    }
-
-    @Override public @Nullable Def.Signature signature() {
-      return signature;
-    }
-
-    @Override public void setSignature(Def.@Nullable Signature signature) {
-      this.signature = signature;
-    }
-
-    @Override public @NotNull Expr result() {
-      return result;
-    }
-
-    @Override public void setResult(@NotNull Expr result) {
-      this.result = result;
-    }
-  }
-
   /**
    * Concrete function definition
    *

base/src/main/java/org/aya/concrete/visitor/ExprView.java

@@ -35,6 +35,7 @@ public interface ExprView {
   private @NotNull Expr traverse(@NotNull Expr expr) {
     return switch (expr) {
       case Expr.RefExpr ref -> ref; // I don't know
+      case Expr.SelfExpr ref -> ref;
       case Expr.UnresolvedExpr unresolved -> unresolved;
       case Expr.LamExpr lam -> {
         var param = commit(lam.param());

base/src/main/java/org/aya/concrete/visitor/StmtOps.java

@@ -53,10 +53,9 @@ default void visitDecl(@NotNull Decl decl, P pp) {
     if (decl instanceof Decl.Telescopic teleDecl) visitTelescopic(decl, teleDecl, pp);
     if (decl instanceof Decl.Resulted resulted) resulted.setResult(visitExpr(resulted.result(), pp));
     switch (decl) {
-      case ClassDecl classDecl -> {}
       case TeleDecl.PrimDecl prim -> {}
       case TeleDecl.DataDecl data -> data.body.forEach(ctor -> traced(ctor, pp, this::visitDecl));
-      case TeleDecl.StructDecl struct -> struct.fields.forEach(field -> traced(field, pp, this::visitDecl));
+      case ClassDecl.StructDecl struct -> struct.fields.forEach(field -> traced(field, pp, this::visitDecl));
       case TeleDecl.FnDecl fn -> fn.body = fn.body.map(
         expr -> visitExpr(expr, pp),
         clauses -> clauses.map(clause -> visitClause(clause, pp))
@@ -65,7 +64,7 @@ default void visitDecl(@NotNull Decl decl, P pp) {
         ctor.patterns = ctor.patterns.map(pat -> visitPattern(pat, pp));
         ctor.clauses = ctor.clauses.map(clause -> visitClause(clause, pp));
       }
-      case TeleDecl.StructField field -> {
+      case ClassDecl.StructDecl.StructField field -> {
         field.clauses = field.clauses.map(clause -> visitClause(clause, pp));
         field.body = field.body.map(expr -> visitExpr(expr, pp));
       }

base/src/main/java/org/aya/core/def/ClassDef.java

@@ -2,18 +2,33 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.core.def;
 
+import kala.collection.immutable.ImmutableSeq;
 import org.aya.concrete.stmt.ClassDecl;
+import org.aya.core.term.FormTerm;
+import org.aya.core.term.Term;
 import org.aya.distill.CoreDistiller;
 import org.aya.generic.AyaDocile;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.DefVar;
 import org.aya.util.distill.DistillerOptions;
 import org.jetbrains.annotations.NotNull;
 
-public non-sealed/*sealed*/ interface ClassDef extends AyaDocile, GenericDef {
+public sealed interface ClassDef extends AyaDocile, GenericDef {
   @Override default @NotNull Doc toDoc(@NotNull DistillerOptions options) {
     return new CoreDistiller(options).def(this);
   }
 
   @Override @NotNull DefVar<? extends ClassDef, ? extends ClassDecl> ref();
+
+  abstract sealed class Type implements ClassDef permits StructDef {
+    public final int resultLevel;
+
+    protected Type(int resultLevel) {
+      super();
+      this.resultLevel = resultLevel;
+    }
+    @Override public @NotNull Term result() {
+      return new FormTerm.Univ(resultLevel);
+    }
+  }
 }