STRUCT: roughly implement ExprTycker synth for Expr.NewExpr

aya-prover · Jul 26, 2022 · 240a161 · 240a161
1 parent fbcb7dd
commit 240a161
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 9 deletions.
diff --git a/base/src/main/java/org/aya/core/term/StructCall.java b/base/src/main/java/org/aya/core/term/StructCall.java
@@ -3,6 +3,7 @@
 package org.aya.core.term;
 
 import kala.collection.Map;
+import kala.collection.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableHashMap;
 import kala.collection.mutable.MutableMap;
@@ -45,4 +46,10 @@ public boolean finished() {
   public @NotNull StructCall apply(@NotNull FieldDef field, @NotNull Arg<Term> arg) {
     return new StructCall(ref, ulift, params.appended(Tuple2.of(field.rootRef(), arg)));
   }
+
+  public @NotNull StructCall apply(@NotNull ImmutableMap<DefVar<FieldDef, ClassDecl.StructDecl.StructField>, Term> map) {
+    final StructCall[] result = {this};
+    map.forEach((key, value) -> result[0] = result[0].apply(key.core, new Arg(value, true)));
+    return result[0];
+  }
 }
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck;
 
+import kala.collection.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.MutableMap;
@@ -25,6 +26,7 @@
 import org.aya.generic.util.NormalizeMode;
 import org.aya.ref.DefVar;
 import org.aya.ref.LocalVar;
+import org.aya.ref.Var;
 import org.aya.tyck.env.LocalCtx;
 import org.aya.tyck.env.MapLocalCtx;
 import org.aya.tyck.error.*;
@@ -101,19 +103,15 @@ private void tracing(@NotNull Consumer<Trace.@NotNull Builder> consumer) {
         yield new Result(result.wellTyped.lift(levels), result.type.lift(levels));
       }
       case Expr.NewExpr newExpr -> {
-        throw new UnsupportedOperationException("TODO");
-        /*
         var structExpr = newExpr.struct();
         var struct = instImplicits(synthesize(structExpr).wellTyped, structExpr.sourcePos());
-        if (!(struct instanceof CallTerm.Struct structCall))
+        if (!(struct instanceof StructCall structCall))
           yield fail(structExpr, struct, BadTypeError.structCon(state, newExpr, struct));
         var structRef = structCall.ref();
 
-        var subst = new Subst(MutableMap.from(
-          Def.defTele(structRef).view().zip(structCall.args())
-            .map(t -> Tuple.of(t._1.ref(), t._2.term()))));
+        var subst = new Subst(MutableMap.create());
 
-        var fields = MutableList.<Tuple2<DefVar<FieldDef, TeleDecl.StructField>, Term>>create();
+        var fields = MutableList.<Tuple2<DefVar<FieldDef, ClassDecl.StructDecl.StructField>, Term>>create();
         var missing = MutableList.<Var>create();
         var conFields = newExpr.fields();
 
@@ -152,8 +150,7 @@ private void tracing(@NotNull Consumer<Trace.@NotNull Builder> consumer) {
           yield fail(newExpr, structCall, new FieldProblem.MissingFieldError(newExpr.sourcePos(), missing.toImmutableSeq()));
         if (conFields.isNotEmpty())
           yield fail(newExpr, structCall, new FieldProblem.NoSuchFieldError(newExpr.sourcePos(), conFields.map(f -> f.name().data())));
-        yield new Result(new IntroTerm.New(structCall, ImmutableMap.from(fields)), structCall);
-        */
+        yield new Result(new IntroTerm.New(structCall.apply(ImmutableMap.from(fields))), structCall);
       }
       case Expr.ProjExpr proj -> {
         var struct = proj.tup();