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

Commit

Permalink
tyck: now pass the test
Browse files Browse the repository at this point in the history
  • Loading branch information
@HoshinoTented
HoshinoTented committed Feb 17, 2024
1 parent 4a4e9ed commit c2fdf3c
Show file tree
Hide file tree
Showing 2 changed files with 62 additions and 10 deletions.
38 changes: 32 additions & 6 deletions base/src/main/java/org/aya/tyck/ExprTycker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 org.aya.generic.SortKind;
import org.aya.syntax.concrete.Expr;
import org.aya.syntax.core.def.TeleDef;
import org.aya.syntax.core.term.*;
Expand Down Expand Up @@ -31,6 +32,25 @@ public ExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Repo
return synthesize(expr);
}

public @NotNull Term ty(@NotNull Expr expr) {
return doTy(expr);
}

private @NotNull Term doTy(@NotNull Expr expr) {
return switch (expr) {
case Expr.Sort sort -> new SortTerm(sort.kind(), sort.lift());
case Expr.Pi(var param, var last) -> {
var wellParam = ty(param.type().data());
yield subscoped(() -> {
localCtx().put(param.ref(), wellParam);
var wellLast = ty(last.data());
return new PiTerm(wellParam, wellLast);
});
}
default -> synthesize(expr).wellTyped();
};
}

public @NotNull Result synthesize(@NotNull Expr expr) {
return doSynthesize(expr);
}
Expand All @@ -53,8 +73,6 @@ public ExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Repo

yield new Result.Default(app, ty);
}
case Expr.Array array -> 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());
Expand All @@ -70,18 +88,22 @@ yield subscoped(() -> {
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 -> switch (ref.var()) {
case LocalVar lVar -> new Result.Default(new FreeTerm(lVar), localCtx().get(lVar));
case DefVar<?, ?> defVar -> ExprTyckerUtils.inferDef(defVar);
default -> throw new UnsupportedOperationException("TODO");
};
case Expr.Sigma sigma -> throw new UnsupportedOperationException("TODO");
case Expr.Sort sort -> 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);
yield new Result.Default(ty, ty); // FIXME: Type in Type
}
case Expr.Tuple(var items) -> {
var results = items.map(i -> synthesize(i.data()));
var wellTypeds = results.map(Result::wellTyped);
Expand All @@ -91,6 +113,10 @@ yield subscoped(() -> {

yield new Result.Default(wellTyped, ty);
}
case Expr.Error error -> throw new UnsupportedOperationException("TODO");
case Expr.Let let -> throw new UnsupportedOperationException("TODO");
case Expr.Array array -> throw new UnsupportedOperationException("TODO");
case Expr.RawSort rawSort -> throw new UnsupportedOperationException("desugared");
case Expr.Do aDo -> throw new UnsupportedOperationException("desugared");
case Expr.BinOpSeq _ -> throw new UnsupportedOperationException("deesugared");
case Expr.Idiom _ -> throw new UnsupportedOperationException("desugared");
Expand Down
34 changes: 30 additions & 4 deletions base/src/test/java/org/aya/syntax/core/BindTest.java
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,19 @@
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.aya.util.reporter.ThrowingReporter;
import org.jetbrains.annotations.NotNull;
import org.junit.jupiter.api.Test;

import static org.junit.jupiter.api.Assertions.assertEquals;
Expand All @@ -16,12 +23,31 @@ public class BindTest {
// λx. λy. x y
var x = new LocalVar("x", SourcePos.NONE);
var y = new LocalVar("y", SourcePos.NONE);
var body = new AppTerm(new FreeTerm(x), Arg.ofExplicitly(new FreeTerm(y)));
var body = new AppTerm(new FreeTerm(x), new FreeTerm(y));
// λy. x y => λ. x 0
var lamYXY = new LamTerm(true, body.bind(y));
var lamYXY = new LamTerm(body.bind(y));
// λx. λ. x 0 => λ. λ. 1 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)))));
var lamXYXY = new LamTerm(lamYXY.bind(x));
var expect = new LamTerm(new LamTerm(new AppTerm(new LocalTerm(1), new LocalTerm(0))));
assertEquals(expect, lamXYXY);
}

@Test public void testTyckLam() {
var x = new LocalVar("x", SourcePos.NONE);
var y = new LocalVar("y", SourcePos.NONE);
var ty = new Expr.Type(0);
var pi = new Expr.Pi(new Expr.Param(SourcePos.NONE, LocalVar.IGNORED, of(ty), true), of(ty)); // Type -> Type
var refX = new Expr.Ref(x);
var refY = new Expr.Ref(y);
var XY = new Expr.App(of(refX), new Expr.NamedArg(SourcePos.NONE, true, null, of(refY)));
var YXY = new Expr.Lambda(new Expr.Param(SourcePos.NONE, y, of(ty), true), of(XY));
var XYXY = new Expr.Lambda(new Expr.Param(SourcePos.NONE, x, of(pi), true), of(YXY));

var tycker = new ExprTycker(null, new LocalCtx(MutableMap.create(), null), null);
var result = tycker.synthesize(XYXY);
}

public static <T> @NotNull WithPos<T> of(T data) {
return new WithPos<>(SourcePos.NONE, data);
}
}

0 comments on commit c2fdf3c

Please sign in to comment.