Skip to content
This repository has been archived by the owner on May 27, 2024. It is now read-only.

Commit

Permalink
test: remove test
Browse files Browse the repository at this point in the history
  • Loading branch information
HoshinoTented committed Jan 20, 2024
1 parent b3f5bdc commit 5dc074e
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 16 deletions.
2 changes: 1 addition & 1 deletion base/src/main/java/org/aya/tyck/tycker/StateBased.java
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ public sealed interface StateBased permits AbstractExprTycker {
default <D extends TeleDef, S extends TeleDecl<? extends Term>> @NotNull Result
defCall(DefVar<D, S> defVar, Callable.Factory<D, S> function) {
var tele = TeleDef.defTele(defVar);
var spine = tele.mapIndexed((i, type) -> type.<Term>map(_ -> new LocalTerm(tele.size() - 1 - i))); // λ. λ. λ. someCtor 2 1 0
var spine = tele.mapIndexed((i, type) -> type.<Term>map(x -> new LocalTerm(tele.size() - 1 - i))); // λ. λ. λ. someCtor 2 1 0
Term body = function.make(defVar, 0, spine);
var type = PiTerm.make(tele, TeleDef.defResult(defVar));
if ((defVar.core instanceof FnDef fn && fn.modifiers.contains(Modifier.Inline)) /*|| defVar.core instanceof PrimDef*/) {
Expand Down
15 changes: 0 additions & 15 deletions base/src/test/java/org/aya/syntax/core/BindTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -29,19 +29,4 @@ public class BindTest {
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;
}
}

0 comments on commit 5dc074e

Please sign in to comment.