Skip to content

Commit

Permalink
merge: Jit class cp (#1138)
Browse files Browse the repository at this point in the history
Cherry picked from #1134
  • Loading branch information
ice1000 authored Nov 15, 2024
2 parents 7606a47 + 26555c7 commit a79dc34
Show file tree
Hide file tree
Showing 23 changed files with 381 additions and 126 deletions.
13 changes: 11 additions & 2 deletions base/src/main/java/org/aya/tyck/StmtTycker.java
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,8 @@
import org.aya.tyck.pat.YouTrack;
import org.aya.tyck.tycker.Problematic;
import org.aya.tyck.tycker.TeleTycker;
import org.aya.unify.Synthesizer;
import org.aya.util.error.Panic;
import org.aya.util.error.WithPos;
import org.aya.util.reporter.Reporter;
import org.jetbrains.annotations.NotNull;
Expand Down Expand Up @@ -173,8 +175,15 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker
new Param("self", classCall, false),
classRef.concrete.sourcePos()
);
new MemberDef(classRef, member.ref, classRef.concrete.members.indexOf(member), signature.params(), signature.result());
member.ref.signature = signature;

// self is still in the context
var type = new Synthesizer(tycker).synth(signature.telescope().inst(ImmutableSeq.of(new FreeTerm(self))).makePi());
if (!(type instanceof SortTerm sortType)) {
Panic.unreachable();
} else {
new MemberDef(classRef, member.ref, classRef.concrete.members.indexOf(member), signature.params(), signature.result(), sortType);
member.ref.signature = signature;
}
}

/**
Expand Down
36 changes: 9 additions & 27 deletions base/src/main/java/org/aya/tyck/tycker/AppTycker.java
Original file line number Diff line number Diff line change
Expand Up @@ -5,25 +5,22 @@
import kala.collection.Seq;
import kala.collection.SeqView;
import kala.collection.immutable.ImmutableArray;
import kala.collection.immutable.ImmutableSeq;
import kala.function.CheckedBiFunction;
import org.aya.generic.stmt.Shaped;
import org.aya.syntax.compile.JitCon;
import org.aya.syntax.compile.JitData;
import org.aya.syntax.compile.JitFn;
import org.aya.syntax.compile.JitPrim;
import org.aya.syntax.concrete.stmt.decl.*;
import org.aya.syntax.core.Closure;
import org.aya.syntax.core.def.*;
import org.aya.syntax.core.repr.AyaShape;
import org.aya.syntax.core.term.*;
import org.aya.syntax.core.term.Term;
import org.aya.syntax.core.term.call.*;
import org.aya.syntax.ref.DefVar;
import org.aya.syntax.ref.LocalVar;
import org.aya.syntax.telescope.AbstractTele;
import org.aya.tyck.Jdg;
import org.aya.tyck.TyckState;
import org.aya.unify.Synthesizer;
import org.aya.util.error.Panic;
import org.aya.util.error.SourcePos;
import org.jetbrains.annotations.NotNull;
Expand Down Expand Up @@ -150,7 +147,7 @@ public AppTycker(

private @NotNull Jdg checkClassCall(@NotNull ClassDefLike clazz) throws Ex {
var self = LocalVar.generate("self");
var appliedParams = ofClassMembers(self, clazz, argsCount).lift(lift);
var appliedParams = ofClassMembers(clazz, argsCount).lift(lift);
state.classThis.push(self);
var result = makeArgs.applyChecked(appliedParams, (args, _) -> new Jdg.Default(
new ClassCall(clazz, 0, ImmutableArray.from(args).map(x -> x.bind(self))),
Expand All @@ -174,21 +171,15 @@ public AppTycker(
});
}

private @NotNull AbstractTele ofClassMembers(@NotNull LocalVar self, @NotNull ClassDefLike def, int memberCount) {
var synthesizer = new Synthesizer(tycker);
return switch (def) {
case ClassDef.Delegate delegate -> new TakeMembers(self, delegate.core(), memberCount, synthesizer);
};
private @NotNull AbstractTele ofClassMembers(@NotNull ClassDefLike def, int memberCount) {
return new TakeMembers(def, memberCount);
}

record TakeMembers(
@NotNull LocalVar self, @NotNull ClassDef clazz,
@Override int telescopeSize, @NotNull Synthesizer synthesizer
) implements AbstractTele {
record TakeMembers(@NotNull ClassDefLike clazz, @Override int telescopeSize) implements AbstractTele {
@Override public boolean telescopeLicit(int i) { return true; }
@Override public @NotNull String telescopeName(int i) {
assert i < telescopeSize;
return clazz.members().get(i).ref().name();
return clazz.members().get(i).name();
}

// class Foo
Expand All @@ -199,23 +190,14 @@ record TakeMembers(
@Override public @NotNull Term telescope(int i, Seq<Term> teleArgs) {
// teleArgs are former members
assert i < telescopeSize;
var member = clazz.members().get(i);
return TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new NewTerm(
new ClassCall(new ClassDef.Delegate(clazz.ref()), 0,
ImmutableSeq.fill(clazz.members().size(), idx -> Closure.mkConst(idx < i ? teleArgs.get(idx) : ErrorTerm.DUMMY))
)
))).makePi(Seq.empty());
return clazz.telescope(i, teleArgs);
}

@Override public @NotNull Term result(Seq<Term> teleArgs) {
return clazz.members().view()
.drop(telescopeSize)
.map(member -> TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new FreeTerm(self))).makePi(Seq.empty()))
.map(ty -> (SortTerm) synthesizer.synth(ty))
.foldLeft(SortTerm.Type0, SigmaTerm::lub);
return clazz.result(telescopeSize);
}
@Override public @NotNull SeqView<String> namesView() {
return clazz.members().sliceView(0, telescopeSize).map(i -> i.ref().name());
return clazz.members().sliceView(0, telescopeSize).map(AnyDef::name);
}
}
}
15 changes: 12 additions & 3 deletions base/src/test/java/org/aya/tyck/TyckTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ public class TyckTest {
var result = tyck("""
inductive Nat | O | S Nat
inductive FreeMonoid (A : Type) | e | cons A (FreeMonoid A)
def id {A : Type} (a : A) => a
def lam (A : Type) : Fn (a : A) -> Type => fn a => A
def tup (A : Type) (B : A -> Type) (a : A) (b : Fn (a : A) -> B a)
Expand Down Expand Up @@ -66,7 +66,7 @@ def letExample (A : Type) (B : A -> Type) (f : Fn (a : A) -> B a) (a : A) : B a
prim I : ISet
prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
prim coe (r s : I) (A : I -> Type) : A r -> A s
def transp (A : I -> Type) (a : A 0) : A 1 => coe 0 1 A a
def transpInv (A : I -> Type) (a : A 1) : A 0 => coe 1 0 A a
def coeFill0 (A : I -> Type) (u : A 0) : Path A u (transp A u) => \\i => coe 0 i A u
Expand Down Expand Up @@ -152,7 +152,7 @@ open inductive Phantom Nat Nat (A : Type) | mk A
prim I prim Path prim coe
variable A : Type
def infix = (a b : A) => Path (\\i => A) a b
class Monoid
| classifying carrier : Type
| unit : carrier
Expand All @@ -162,6 +162,15 @@ class Monoid
""").defs.isNotEmpty());
}

@Test
public void what() {
assertTrue(tyck("""
class Kontainer
| Taipe : Type
| walue : Taipe
""").defs.isNotEmpty());
}

@SuppressWarnings("unchecked") private static <T extends AnyDef> T
getDef(@NotNull ImmutableSeq<TyckDef> defs, @NotNull String name) {
return (T) TyckAnyDef.make(defs.find(x -> x.ref().name().equals(name)).get());
Expand Down
8 changes: 8 additions & 0 deletions cli-impl/src/test/java/org/aya/test/LibraryTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,13 @@

import static org.junit.jupiter.api.Assertions.assertEquals;

/**
* LibraryTest testing the compilation of a library and its dependencies
*
* @see #testOnDisk
* @see #testLiterate
* @see #testInMemoryAndPrim
*/
public class LibraryTest {
public static final ThrowingReporter REPORTER = new ThrowingReporter(AyaPrettierOptions.pretty());
@ParameterizedTest
Expand All @@ -51,6 +58,7 @@ public void testOnDisk(@NotNull String libName) throws IOException {
assertEquals(0, compile(libRoot));
}

// Use this test for additional compilation
@Test public void fastTestOnDisk() throws IOException {
FileUtil.deleteRecursively(DIR.resolve("build"));
assertEquals(0, compile(DIR));
Expand Down
11 changes: 10 additions & 1 deletion cli-impl/src/test/resources/success/src/Classes.aya
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,13 @@ class Kontainer

def tyck0 : Nat => Kontainer::walue {new Kontainer Nat 0}

def norm0 : Kontainer::walue {new Kontainer Nat 0} = 0 => refl
def norm0 : Kontainer::walue {new Kontainer Nat 0} = 0 => refl

def subtype : Kontainer Nat => new Kontainer Nat 0
// In core:
// def subtype : Kontainer Nat => cast [Taipe := Nat] [walue := 0] (new Kontainer Nat 0)

def norm1 : Kontainer::walue {subtype} = 0 => refl
// In core:
// (cast [Taipe := Nat] [walue := 0] (new Kontainer Nat 0)) .walue
// -> 0 (it is recorded in the ClassCastTerm!)
6 changes: 3 additions & 3 deletions gradle/libs.versions.toml
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ kala = "0.74.0"
picocli = "4.7.6"
build-util = "0.0.28"
# https://github.com/jline/jline3
jline = "3.26.3"
jline = "3.27.1"
# https://github.com/commonmark/commonmark-java
commonmark = "0.24.0"
# https://junit.org/junit5
Expand All @@ -23,11 +23,11 @@ hamcrest = "2.2"
# https://github.com/google/gson
gson = "2.11.0"
# https://github.com/beryx/badass-jlink-plugin
jlink = "3.0.1"
jlink = "3.1.0-rc-1"
# https://github.com/jacoco/jacoco
jacoco = "0.8.12"
# https://github.com/manifold-systems/manifold/tree/master/manifold-deps-parent/manifold-delegation
manifold = "2024.1.39"
manifold = "2024.1.41"

[plugins]
jlink = { id = "org.beryx.jlink", version.ref = "jlink" }
Expand Down
7 changes: 3 additions & 4 deletions ide-lsp/build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -57,16 +57,15 @@ jlink {
requires("java.logging")
}
launcher {
mainClass.set(Constants.mainClassQName)
mainClass = Constants.mainClassQName
name = "aya-lsp"
jvmArgs = mutableListOf("--enable-preview")
}
secondaryLauncher {
moduleName = "aya.cli.console"
mainClass = "org.aya.cli.console.Main"
name = "aya"
jvmArgs = mutableListOf("--enable-preview")
this as org.beryx.jlink.data.SecondaryLauncherData
mainClass = "org.aya.cli.console.Main"
moduleName = "aya.cli.console"
}
supportedPlatforms.forEach { platform ->
targetPlatform(platform) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -40,4 +40,8 @@ protected AbstractSerializer(@NotNull SourceBuilder builder) {
return new TermExprializer(sourceBuilder.nameGen(), argTerms)
.serialize(term);
}

protected @NotNull String serializeTerm(@NotNull Term term) {
return serializeTermUnderTele(term, ImmutableSeq.empty());
}
}
47 changes: 47 additions & 0 deletions jit-compiler/src/main/java/org/aya/compiler/ClassSerializer.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
package org.aya.compiler;

import kala.collection.immutable.ImmutableSeq;
import org.aya.syntax.compile.JitClass;
import org.aya.syntax.compile.JitMember;
import org.aya.syntax.core.def.ClassDef;
import org.aya.syntax.core.term.call.ClassCall;
import org.jetbrains.annotations.NotNull;

import static org.aya.compiler.AyaSerializer.CLASS_IMMSEQ;
import static org.aya.compiler.ExprializeUtils.getJavaReference;
import static org.aya.compiler.NameSerializer.getClassReference;

public final class ClassSerializer extends JitDefSerializer<ClassDef> {
public static final String CLASS_JITMEMBERS = getJavaReference(JitMember.class);
public static final String CLASS_CLASSCALL = getJavaReference(ClassCall.class);
public static final String FIELD_MEMBERS = "members";
public static final String METHOD_MEMBARS = "membars";

public ClassSerializer(@NotNull SourceBuilder builder) { super(builder, JitClass.class); }
@Override protected @NotNull String callClass() { return CLASS_CLASSCALL; }
@Override protected void buildConstructor(ClassDef unit) { buildSuperCall(ImmutableSeq.empty()); }

@Override
protected boolean shouldBuildEmptyCall(@NotNull ClassDef unit) {
return true;
}

private void buildMembers(ClassDef unit) {
buildIf(STR."\{FIELD_MEMBERS} == null", () ->
buildUpdate(FIELD_MEMBERS, ExprializeUtils.makeArrayFrom(CLASS_JITMEMBERS, unit.members().map(mem ->
ExprializeUtils.getInstance(getClassReference(mem.ref())))
)));

buildReturn(FIELD_MEMBERS);
}

@Override public AbstractSerializer<ClassDef> serialize(ClassDef unit) {
buildFramework(unit, () ->
buildMethod(METHOD_MEMBARS, ImmutableSeq.empty(), STR."\{CLASS_IMMSEQ}<\{CLASS_JITMEMBERS}>", true,
() -> buildMembers(unit)));

return this;
}
}
88 changes: 88 additions & 0 deletions jit-compiler/src/main/java/org/aya/compiler/JitDefSerializer.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
package org.aya.compiler;

import kala.collection.immutable.ImmutableSeq;
import org.aya.syntax.compile.CompiledAya;
import org.aya.syntax.core.def.TyckDef;
import org.jetbrains.annotations.NotNull;

import static org.aya.compiler.AyaSerializer.*;
import static org.aya.compiler.NameSerializer.javifyClassName;

public abstract class JitDefSerializer<T extends TyckDef> extends AbstractSerializer<T> {
public static final String CLASS_METADATA = ExprializeUtils.getJavaReference(CompiledAya.class);

protected final @NotNull Class<?> superClass;

protected JitDefSerializer(@NotNull SourceBuilder builder, @NotNull Class<?> superClass) {
super(builder);
this.superClass = superClass;
}

/**
* @see CompiledAya
*/
protected void buildMetadata(@NotNull T unit) {
var ref = unit.ref();
var module = ref.module;
var assoc = ref.assoc();
var assocIdx = assoc == null ? -1 : assoc.ordinal();
assert module != null;
appendLine(STR."@\{CLASS_METADATA}(");
var modPath = module.module().module();
appendMetadataRecord("module", ExprializeUtils.makeHalfArrayFrom(modPath.view().map(ExprializeUtils::makeString)), true);
// Assumption: module.take(fileModule.size).equals(fileModule)
appendMetadataRecord("fileModuleSize", Integer.toString(module.fileModuleSize()), false);
appendMetadataRecord("name", ExprializeUtils.makeString(ref.name()), false);
appendMetadataRecord("assoc", Integer.toString(assocIdx), false);
buildShape(unit);

appendLine(")");
}

protected void buildShape(T unit) {
appendMetadataRecord("shape", "-1", false);
appendMetadataRecord("recognition", ExprializeUtils.makeHalfArrayFrom(ImmutableSeq.empty()), false);
}

protected void appendMetadataRecord(@NotNull String name, @NotNull String value, boolean isFirst) {
var prepend = isFirst ? "" : ", ";
appendLine(STR."\{prepend}\{name} = \{value}");
}

public void buildInstance(@NotNull String className) {
buildConstantField(className, STATIC_FIELD_INSTANCE, ExprializeUtils.makeNew(className));
}

public void buildSuperCall(@NotNull ImmutableSeq<String> args) {
appendLine(STR."super(\{args.joinToString(", ")});");
}

protected abstract boolean shouldBuildEmptyCall(@NotNull T unit);

protected void buildFramework(@NotNull T unit, @NotNull Runnable continuation) {
var className = javifyClassName(unit.ref());
buildMetadata(unit);
buildInnerClass(className, superClass, () -> {
buildInstance(className);
appendLine();
// empty return type for constructor
buildMethod(className, ImmutableSeq.empty(), "/*constructor*/", false, () -> buildConstructor(unit));
appendLine();
if (shouldBuildEmptyCall(unit)) {
buildConstantField(callClass(), FIELD_EMPTYCALL, ExprializeUtils.makeNew(
callClass(), ExprializeUtils.getInstance(className)));
}
appendLine();
continuation.run();
});
}

protected abstract @NotNull String callClass();

/**
* @see org.aya.syntax.compile.JitDef
*/
protected abstract void buildConstructor(T unit);
}
Loading

0 comments on commit a79dc34

Please sign in to comment.