am I right? @ice1000

aya-prover · Jan 19, 2024 · df59db6 · df59db6 · ice1000 · Jan 19, 2024
1 parent ff50b0c
commit df59db6
Show file tree

Hide file tree

Showing 5 changed files with 80 additions and 12 deletions.
diff --git a/base/src/main/java/org/aya/syntax/core/term/SigmaTerm.java b/base/src/main/java/org/aya/syntax/core/term/SigmaTerm.java
@@ -11,14 +11,14 @@
 /**
  * @author re-xyr
  */
-public record SigmaTerm(@NotNull ImmutableSeq<Arg<Term>> params) implements StableWHNF, Formation {
-  public @NotNull SigmaTerm update(@NotNull ImmutableSeq<Arg<Term>> params) {
+public record SigmaTerm(@NotNull ImmutableSeq<Term> params) implements StableWHNF, Formation {
+  public @NotNull SigmaTerm update(@NotNull ImmutableSeq<Term> params) {
     return params.sameElements(params(), true) ? this : new SigmaTerm(params);
   }
 
   @Override
   public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
-    return update(params.mapIndexed((i, param) -> param.descent(t -> f.apply(i, t))));
+    return update(params.mapIndexed(f));
   }
 
   // @Override public @NotNull SigmaTerm descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g) {

diff --git a/base/src/main/java/org/aya/syntax/core/term/TupTerm.java b/base/src/main/java/org/aya/syntax/core/term/TupTerm.java
@@ -11,18 +11,13 @@
 /**
  * @author re-xyr
  */
-public record TupTerm(@NotNull ImmutableSeq<Arg<Term>> items) implements StableWHNF {
-  private @NotNull TupTerm update(@NotNull ImmutableSeq<Arg<Term>> items) {
+public record TupTerm(@NotNull ImmutableSeq<Term> items) implements StableWHNF {
+  private @NotNull TupTerm update(@NotNull ImmutableSeq<Term> items) {
     return items.sameElements(items(), true) ? this : new TupTerm(items);
   }
 
   @Override
   public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
-    return update(items.map(x -> x.descent(t -> f.apply(0, t))));
-  }
-
-  @Contract("_ -> new") public static @NotNull TupTerm
-  explicits(@NotNull ImmutableSeq<Term> explicits) {
-    return new TupTerm(explicits.map(i -> new Arg<>(i, true)));
+    return update(items.map(x -> f.apply(0, x)));
   }
 }
diff --git a/base/src/main/java/org/aya/syntax/ref/LocalCtx.java b/base/src/main/java/org/aya/syntax/ref/LocalCtx.java
@@ -16,4 +16,25 @@ public record LocalCtx(
   public @NotNull LocalCtx derive() {
     return new LocalCtx(MutableMap.create(), this);
   }
+
+  public @NotNull Term get(@NotNull LocalVar name) {
+    var ctx = this;
+    Term result;
+
+    while (ctx != null) {
+      result = ctx.getLocal(name);
+      if (result != null) return result;
+      ctx = ctx.parent;
+    }
+
+    throw new UnsupportedOperationException("?");
+  }
+
+  public @Nullable Term getLocal(@NotNull LocalVar name) {
+    return binds.getOrNull(name);
+  }
+
+  public void put(@NotNull LocalVar name, @NotNull Term type) {
+    binds.put(name, type);
+  }
 }
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -2,9 +2,11 @@
 // 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 org.aya.syntax.core.term.Term;
+import org.aya.syntax.concrete.Expr;
+import org.aya.syntax.core.term.*;
 import org.aya.syntax.ref.LocalCtx;
 import org.aya.tyck.tycker.AbstractExprTycker;
+import org.aya.util.Arg;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
 
@@ -17,4 +19,52 @@ public ExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Repo
   public @NotNull Term whnf(@NotNull Term term) {
     throw new UnsupportedOperationException("TODO");
   }
+
+  public @NotNull Result synthesize(@NotNull Expr expr) {
+    return doSynthesize(expr);
+  }
+
+  private @NotNull Result doSynthesize(@NotNull Expr expr) {
+    return switch (expr) {
+      case Expr.App app -> throw new UnsupportedOperationException("TODO");
+      case Expr.Array array -> throw new UnsupportedOperationException("TODO");
+      case Expr.Do aDo -> throw new UnsupportedOperationException("TODO");
+      case Expr.Error error -> throw new UnsupportedOperationException("TODO");
+      case Expr.Hole hole -> throw new UnsupportedOperationException("TODO");
+      case Expr.Lambda(var param, var body) -> {
+        var paramResult = synthesize(param.type().data());
+
+        yield subscoped(() -> {
+          localCtx().put(param.ref(), paramResult.wellTyped());
+          var bodyResult = synthesize(body.data());
+          var lamTerm = new LamTerm(param.explicit(), bodyResult.wellTyped().bind(param.ref()));
+          var ty = new PiTerm(
+            new Arg<>(paramResult.type(), param.explicit()),
+            bodyResult.type()   // TODO: do we need to `.bind` on type?
+          );
+          return new Result.Default(lamTerm, ty);
+        });
+      }
+      case Expr.Let let -> throw new UnsupportedOperationException("TODO");
+      case Expr.LitInt litInt -> throw new UnsupportedOperationException("TODO");
+      case Expr.LitString litString -> throw new UnsupportedOperationException("TODO");
+      case Expr.Pi(var param, var body) -> throw new UnsupportedOperationException("TODO");
+      case Expr.RawSort rawSort -> throw new UnsupportedOperationException("TODO");
+      case Expr.Ref ref -> new Result.Default(new FreeTerm(ref.var()), localCtx().get(ref.var()));
+      case Expr.Sigma sigma -> throw new UnsupportedOperationException("TODO");
+      case Expr.Sort sort -> throw new UnsupportedOperationException("TODO");
+      case Expr.Tuple(var items) -> {
+        var results = items.map(i -> synthesize(i.data()));
+        var wellTypeds = results.map(Result::wellTyped);
+        var tys = results.map(Result::type);
+        var wellTyped = new TupTerm(wellTypeds);
+        var ty = new SigmaTerm(tys);
+
+        yield new Result.Default(wellTyped, ty);
+      }
+      case Expr.BinOpSeq _ -> throw new UnsupportedOperationException("deesugared");
+      case Expr.Idiom _ -> throw new UnsupportedOperationException("desugared");
+      case Expr.Unresolved _ -> throw new UnsupportedOperationException("?");
+    };
+  }
 }
diff --git a/base/src/main/java/org/aya/tyck/tycker/ContextBased.java b/base/src/main/java/org/aya/tyck/tycker/ContextBased.java
@@ -3,6 +3,7 @@
 package org.aya.tyck.tycker;
 
 import org.aya.syntax.ref.LocalCtx;
+import org.jetbrains.annotations.ApiStatus;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 
@@ -17,6 +18,7 @@ public sealed interface ContextBased permits AbstractExprTycker {
    * @param ctx new {@link LocalCtx}
    * @return old context
    */
+  @ApiStatus.Internal
   @Contract(mutates = "this")
   @NotNull LocalCtx setLocalCtx(@NotNull LocalCtx ctx);