test: java.lang.ClassFormatError

aya-prover · Jan 20, 2024 · b3f5bdc · b3f5bdc
1 parent 0128511
commit b3f5bdc
Show file tree

Hide file tree

Showing 6 changed files with 30 additions and 12 deletions.
diff --git a/base/src/main/java/module-info.java b/base/src/main/java/module-info.java
@@ -13,12 +13,14 @@
 
   exports org.aya.generic;
   exports org.aya.prelude;
-  exports org.aya.syntax.concrete.stmt;
+  exports org.aya.resolve.context;
   exports org.aya.syntax.concrete.stmt.decl;
+  exports org.aya.syntax.concrete.stmt;
   exports org.aya.syntax.concrete;
   exports org.aya.syntax.core.def;
+  exports org.aya.syntax.core.term.call;
   exports org.aya.syntax.core.term;
   exports org.aya.syntax.ref;
-  exports org.aya.resolve.context;
-  exports org.aya.syntax.core.term.call;
+  exports org.aya.tyck.tycker;
+  exports org.aya.tyck;
 }
diff --git a/base/src/main/java/org/aya/syntax/core/Signature.java b/base/src/main/java/org/aya/syntax/core/Signature.java
@@ -21,5 +21,6 @@ public record Signature<T extends Term>(
 ) implements AyaDocile {
   @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
     // return Doc.sep(Doc.sep(param.view().map(p -> p.toDoc(options))), Doc.symbol("->"), result.toDoc(options));
+    throw new UnsupportedOperationException("TODO");
   }
 }
diff --git a/base/src/main/java/org/aya/syntax/core/pat/Pat.java b/base/src/main/java/org/aya/syntax/core/pat/Pat.java
@@ -11,5 +11,5 @@
  * @author kiva, ice1000, HoshinoTented
  */
 @Debug.Renderer(text = "toTerm().toDoc(AyaPrettierOptions.debug()).debugRender()")
-public sealed interface Pat extends AyaDocile {
+public interface Pat extends AyaDocile {
 }
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
@@ -23,10 +23,6 @@ public record SigmaTerm(@NotNull ImmutableSeq<Term> params) implements StableWHN
     return update(params.mapIndexed(f));
   }
 
-  // @Override public @NotNull SigmaTerm descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g) {
-  //   return update(params.map(p -> p.descent(f)));
-  // }
-
   // public static @NotNull SortTerm lub(@NotNull SortTerm x, @NotNull SortTerm y) {
   //   int lift = Math.max(x.lift(), y.lift());
   //   if (x.kind() == SortKind.Set || y.kind() == SortKind.Set) {

diff --git a/base/src/main/java/org/aya/tyck/tycker/StateBased.java b/base/src/main/java/org/aya/tyck/tycker/StateBased.java
@@ -46,5 +46,4 @@ public sealed interface StateBased permits AbstractExprTycker {
 
     return new Result.Default(LamTerm.make(spine.map(Arg::explicit), body), type);
   }
-
 }
diff --git a/base/src/test/java/org/aya/syntax/core/BindTest.java b/base/src/test/java/org/aya/syntax/core/BindTest.java
@@ -1,12 +1,17 @@
 package org.aya.syntax.core;
 
+import kala.collection.mutable.MutableMap;
+import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.core.term.AppTerm;
 import org.aya.syntax.core.term.FreeTerm;
 import org.aya.syntax.core.term.LamTerm;
 import org.aya.syntax.core.term.LocalTerm;
+import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
+import org.aya.tyck.ExprTycker;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
+import org.aya.util.error.WithPos;
 import org.junit.jupiter.api.Test;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
@@ -18,10 +23,25 @@ public class BindTest {
     var y = new LocalVar("y", SourcePos.NONE);
     var body = new AppTerm(new FreeTerm(x), Arg.ofExplicitly(new FreeTerm(y)));
     // λy. x y => λ. x 0
-    var lamYXY = new LamTerm(body.bind(y));
+    var lamYXY = new LamTerm(true, body.bind(y));
     // λx. λ. x 0 => λ. λ. 1 0
-    var lamXYXY = new LamTerm(lamYXY.bind(x));
-    var expect = new LamTerm(new LamTerm(new AppTerm(new LocalTerm(1), Arg.ofExplicitly(new LocalTerm(0)))));
+    var lamXYXY = new LamTerm(true, lamYXY.bind(x));
+    var expect = new LamTerm(true, new LamTerm(true, new AppTerm(new LocalTerm(1), Arg.ofExplicitly(new LocalTerm(0)))));
     assertEquals(expect, lamXYXY);
   }
+
+
+  @Test
+  public void tyckLam() {
+    var x = new LocalVar("x", SourcePos.NONE);
+    var y = new LocalVar("y", SourcePos.NONE);
+    // x y
+    var body = new Expr.App(new WithPos<>(SourcePos.NONE, new Expr.Ref(x)), new Expr.NamedArg(SourcePos.NONE, true, null, new WithPos<>(SourcePos.NONE, new Expr.Ref(y))));
+    // λ y. x y
+    var lamYXY = new Expr.Lambda(new Expr.Param(SourcePos.NONE, y, true), new WithPos<>(SourcePos.NONE, body));
+    var lamXYXY = new Expr.Lambda(new Expr.Param(SourcePos.NONE, x, true), new WithPos<>(SourcePos.NONE, lamYXY));
+    var tycker = new ExprTycker(null, new LocalCtx(MutableMap.create(), null), null);
+    var result = tycker.synthesize(lamXYXY);
+    return;
+  }
 }
Original file line number	Diff line number	Diff line change
Expand Up		@@ -46,5 +46,4 @@ public sealed interface StateBased permits AbstractExprTycker {

		return new Result.Default(LamTerm.make(spine.map(Arg::explicit), body), type);
		}

		}