tycker: start working on checking of applications

aya-prover · Mar 8, 2024 · 132125a · 132125a
1 parent 16f1281
commit 132125a
Show file tree

Hide file tree

Showing 7 changed files with 52 additions and 86 deletions.
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -2,21 +2,19 @@
 // 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.ImmutableSeq;
 import org.aya.generic.SortKind;
 import org.aya.syntax.concrete.Expr;
-import org.aya.syntax.core.def.TeleDef;
 import org.aya.syntax.core.term.*;
-import org.aya.syntax.core.term.call.Callable;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.tyck.tycker.AbstractExprTycker;
-import org.aya.tyck.tycker.ExprTyckerUtils;
+import org.aya.tyck.tycker.AppTycker;
+import org.aya.util.error.WithPos;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
 
-import java.util.Objects;
-
 public final class ExprTycker extends AbstractExprTycker {
   public ExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Reporter reporter) {
     super(state, ctx, reporter);
@@ -28,58 +26,43 @@ public ExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Repo
     return term;
   }
 
-  public @NotNull Result inherit(@NotNull Expr expr, @NotNull Term type) {
+  public @NotNull Result inherit(@NotNull WithPos<Expr> expr, @NotNull Term type) {
     return synthesize(expr);
   }
 
-  public @NotNull Term ty(@NotNull Expr expr) {
+  public @NotNull Term ty(@NotNull WithPos<Expr> expr) {
     return doTy(expr);
   }
 
-  private @NotNull Term doTy(@NotNull Expr expr) {
-    return switch (expr) {
+  private @NotNull Term doTy(@NotNull WithPos<Expr> expr) {
+    return switch (expr.data()) {
       case Expr.Sort sort -> new SortTerm(sort.kind(), sort.lift());
       case Expr.Pi(var param, var last) -> {
-        var wellParam = ty(param.type().data());
+        var wellParam = ty(param.type());
         yield subscoped(() -> {
           localCtx().put(param.ref(), wellParam);
-          var wellLast = ty(last.data());
+          var wellLast = ty(last);
           return new PiTerm(wellParam, wellLast);
         });
       }
       default -> synthesize(expr).wellTyped();
     };
   }
 
-  public @NotNull Result synthesize(@NotNull Expr expr) {
+  public @NotNull Result synthesize(@NotNull WithPos<Expr> expr) {
     return doSynthesize(expr);
   }
 
-  private @NotNull Result doSynthesize(@NotNull Expr expr) {
-    return switch (expr) {
-      case Expr.App(var f, var a) -> {
-        var resultF = synthesize(f.data());
-        if (!(whnf(resultF.type()) instanceof PiTerm fTy)) throw new UnsupportedOperationException("TODO");
-
-        var wellF = whnf(resultF.wellTyped());
-        if (wellF instanceof Callable.Tele callF) {
-          yield checkAppOnCall(callF, fTy, a);
-        }
-
-        var param = fTy.param();
-        var wellArg = inherit(a.term(), param).wellTyped();
-        var app = AppTerm.make(wellF, wellArg);
-        var ty = fTy.body().instantiate(wellArg);
-
-        yield new Result.Default(app, ty);
-      }
+  private @NotNull Result doSynthesize(@NotNull WithPos<Expr> expr) {
+    return switch (expr.data()) {
+      case Expr.App(var f, var a) -> checkApplication(f, a);
       case Expr.Hole hole -> throw new UnsupportedOperationException("TODO");
       case Expr.Lambda(var param, var body) -> {
-        var paramResult = synthesize(param.type().data());
+        var paramResult = synthesize(param.type());
 
         yield subscoped(() -> {
           localCtx().put(param.ref(), paramResult.wellTyped());
-          var bodyResult = synthesize(body.data());
+          var bodyResult = synthesize(body);
           var lamTerm = new LamTerm(bodyResult.wellTyped().bind(param.ref()));
           var ty = new PiTerm(
             paramResult.type(),
@@ -92,20 +75,20 @@ yield subscoped(() -> {
       case Expr.LitString litString -> throw new UnsupportedOperationException("TODO");
       case Expr.Ref ref -> switch (ref.var()) {
         case LocalVar lVar -> new Result.Default(new FreeTerm(lVar), localCtx().get(lVar));
-        case DefVar<?, ?> defVar -> ExprTyckerUtils.inferDef(defVar);
+        case DefVar<?, ?> defVar -> AppTycker.checkDefApplication(defVar, _ -> ImmutableSeq.empty());
         default -> throw new UnsupportedOperationException("TODO");
       };
       case Expr.Sigma sigma -> throw new UnsupportedOperationException("TODO");
       case Expr.Pi(var param, var body) -> {
         var ty = ty(expr);
         yield new Result.Default(ty, new SortTerm(SortKind.Type, 0));
       }
-      case Expr.Sort sort -> {
-        var ty = ty(sort);
+      case Expr.Sort _ -> {
+        var ty = ty(expr);
         yield new Result.Default(ty, ty);       // FIXME: Type in Type
       }
       case Expr.Tuple(var items) -> {
-        var results = items.map(i -> synthesize(i.data()));
+        var results = items.map(this::synthesize);
         var wellTypeds = results.map(Result::wellTyped);
         var tys = results.map(Result::type);
         var wellTyped = new TupTerm(wellTypeds);
@@ -124,41 +107,13 @@ yield subscoped(() -> {
     };
   }
 
+  private @NotNull Result checkApplication(WithPos<Expr> f, ImmutableSeq<Expr.NamedArg> a) {
+    throw new UnsupportedOperationException("TODO");
+  }
+
   private @NotNull PiTerm ensurePi(Term term) {
     if (term instanceof PiTerm pi) return pi;
     // TODO
     throw new UnsupportedOperationException("TODO: report NotPi");
   }
-
-  private @NotNull Result checkAppOnCall(@NotNull Callable.Tele f, @NotNull PiTerm fTy, @NotNull Expr.NamedArg arg) {
-    var argLicit = arg.explicit();
-    var tele = TeleDef.defTele(f.ref());
-    var param = tele.get(f.args().size());    // always success
-
-    while (param.explicit() != argLicit
-      || (arg.name() != null && Objects.equals(param.name(), arg.name()))) {
-      if (argLicit || arg.name() != null) {
-        // We need to insert hole if:
-        // * the parameter is implicit but the argument is explicit
-        // * the parameter and the argument is both implicit but the argument is an named argument,
-        //   and the parameter is not the one.
-
-        // do insert hole
-        var hole = mockTerm(param, arg.sourcePos());
-        f = f.applyTo(hole);
-        var newTy = fTy.body().instantiate(hole);
-        fTy = ensurePi(newTy);
-        param = tele.get(f.args().size());
-      } else {
-        // the parameter is explicit but the argument is implicit
-        // which is TODO not cool.
-        throw new UnsupportedOperationException("TODO: report not cool");
-      }
-    }
-
-    // for now, we can safely apply {arg} to {f}
-
-    var wellArg = inherit(arg.term(), fTy.param()).wellTyped();
-    return new Result.Default(f.applyTo(wellArg), fTy.body().instantiate(wellArg));
-  }
 }
diff --git a/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java b/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java
@@ -32,11 +32,11 @@ protected AbstractExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @N
 
   @Override
   public @NotNull TyckState state() {
-    return this.state;
+    return state;
   }
 
   @Override
   public @NotNull Reporter reporter() {
-    return this.reporter;
+    return reporter;
   }
 }
diff --git a/.../org/aya/tyck/tycker/ExprTyckerUtils.java → ...n/java/org/aya/tyck/tycker/AppTycker.java b/.../org/aya/tyck/tycker/ExprTyckerUtils.java → ...n/java/org/aya/tyck/tycker/AppTycker.java
@@ -6,24 +6,31 @@
 import org.aya.syntax.concrete.stmt.decl.Decl;
 import org.aya.syntax.concrete.stmt.decl.TeleDecl;
 import org.aya.syntax.core.def.*;
+import org.aya.syntax.core.term.Param;
+import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.call.DataCall;
 import org.aya.syntax.core.term.call.FnCall;
 import org.aya.syntax.ref.DefVar;
 import org.aya.tyck.Result;
 import org.jetbrains.annotations.NotNull;
 
-public final class ExprTyckerUtils {
-  private ExprTyckerUtils() {}
+import java.util.function.Function;
+
+public final class AppTycker {
+  private AppTycker() {}
 
   @SuppressWarnings("unchecked")
-  public static @NotNull Result inferDef(@NotNull DefVar<? extends Def, ? extends Decl> defVar) {
+  public static @NotNull Result checkDefApplication(
+    @NotNull DefVar<? extends Def, ? extends Decl> defVar,
+    Function<ImmutableSeq<Param>, ImmutableSeq<Term>> makeArgs
+  ) {
     var core = defVar.core;
     var concrete = defVar.concrete;
 
     if (core instanceof FnDef || concrete instanceof TeleDecl.FnDecl) {
       var fnVar = (DefVar<FnDef, TeleDecl.FnDecl>) defVar;
       new Result.Default(
-        new FnCall(fnVar, 0, ImmutableSeq.empty()),
+        new FnCall(fnVar, 0, makeArgs.apply(TeleDef.defTele(fnVar))),
         TeleDef.defType(fnVar)
       );
     } else if (core instanceof DataDef || concrete instanceof TeleDecl.DataDecl) {

diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -134,13 +134,14 @@ record Tuple(
     }
   }
 
-  record App(@NotNull WithPos<Expr> function, @NotNull NamedArg argument) implements Expr {
-    public @NotNull App update(@NotNull WithPos<Expr> function, @NotNull NamedArg argument) {
-      return function == function() && argument == argument() ? this : new App(function, argument);
+  record App(@NotNull WithPos<Expr> function, @NotNull ImmutableSeq<NamedArg> argument) implements Expr {
+    public @NotNull App update(@NotNull WithPos<Expr> function, @NotNull ImmutableSeq<NamedArg> argument) {
+      return function == function() && argument.sameElements(argument(), true)
+        ? this : new App(function, argument);
     }
 
     @Override public @NotNull App descent(@NotNull UnaryOperator<@NotNull Expr> f) {
-      return update(function.descent(f), argument.descent(f));
+      return update(function.descent(f), argument.map(arg -> arg.descent(f)));
     }
   }
 

diff --git a/syntax/src/main/java/org/aya/syntax/core/def/CtorDef.java b/syntax/src/main/java/org/aya/syntax/core/def/CtorDef.java
@@ -22,10 +22,10 @@ public final class CtorDef extends SubLevelDef {
    */
   public CtorDef(
     @NotNull DefVar<DataDef, TeleDecl.DataDecl> dataRef, @NotNull DefVar<CtorDef, TeleDecl.DataCtor> ref,
-    @NotNull ImmutableSeq<Param> selfTele,
+    @NotNull ImmutableSeq<Param> ownerTele, @NotNull ImmutableSeq<Param> selfTele,
     @NotNull Term result, boolean coerce
   ) {
-    super(selfTele, result, coerce);
+    super(ownerTele, selfTele, result, coerce);
     ref.core = this;
     this.dataRef = dataRef;
     this.ref = ref;

diff --git a/syntax/src/main/java/org/aya/syntax/core/def/SubLevelDef.java b/syntax/src/main/java/org/aya/syntax/core/def/SubLevelDef.java
@@ -14,21 +14,24 @@
  * @author ice1000
  */
 public sealed abstract class SubLevelDef implements TeleDef permits CtorDef {
+  public final @NotNull ImmutableSeq<Param> ownerTele;
   public final @NotNull ImmutableSeq<Param> selfTele;
   public final @NotNull Term result;
   public final boolean coerce;
 
   protected SubLevelDef(
+    @NotNull ImmutableSeq<Param> ownerTele,
     @NotNull ImmutableSeq<Param> selfTele,
     @NotNull Term result, boolean coerce
   ) {
+    this.ownerTele = ownerTele;
     this.selfTele = selfTele;
     this.result = result;
     this.coerce = coerce;
   }
 
   public @NotNull SeqView<Param> fullTelescope() {
-    return selfTele.view();
+    return ownerTele.view().concat(selfTele);
   }
 
   @Override public @NotNull Term result() {

diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Param.java b/syntax/src/main/java/org/aya/syntax/core/term/Param.java
@@ -6,16 +6,16 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-public record Param(
-  @Nullable String name,
-  @NotNull Term type,
-  boolean explicit
-) {
+public record Param(@Nullable String name, @NotNull Term type, boolean explicit) {
   public Param(@NotNull Term type, boolean explicit) {
     this(null, type, explicit);
   }
 
   public @NotNull Arg<Term> toArg() {
     return new Arg<>(type, explicit);
   }
+
+  public @NotNull Param implicitize() {
+    return new Param(name, type, false);
+  }
 }