From 6fb5542f933248b47c19ea88bef82e29218df79d Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 12 Dec 2023 18:52:05 -0500 Subject: [PATCH] misc: more code review Co-authored-by: Hoshino Tented --- .../java/org/aya/core/serde/CompiledAya.java | 5 +--- .../main/java/org/aya/core/serde/SerTerm.java | 2 +- .../java/org/aya/core/serde/Serializer.java | 24 ++++++++++++------- .../src/test/java/org/aya/core/SuedeTest.java | 4 ++-- .../test/java/org/aya/tyck/TyckDeclTest.java | 5 ++-- 5 files changed, 22 insertions(+), 18 deletions(-) diff --git a/base/src/main/java/org/aya/core/serde/CompiledAya.java b/base/src/main/java/org/aya/core/serde/CompiledAya.java index ecbe3baa2..c41b86ed3 100644 --- a/base/src/main/java/org/aya/core/serde/CompiledAya.java +++ b/base/src/main/java/org/aya/core/serde/CompiledAya.java @@ -145,10 +145,7 @@ private void ser(@NotNull ImmutableSeq defs) { } private void serDef(@NotNull AyaShape.Factory factory, @NotNull GenericDef def) { - var shapeResultMaybe = factory.find(def) - .map(x -> SerDef.SerShapeResult.serialize(state, x)) - .getOrNull(); - var serDef = new Serializer(state).serialize(def, shapeResultMaybe); + var serDef = new Serializer(state, factory).serialize(def); serDefs.append(serDef); serOp(serDef, def); switch (serDef) { diff --git a/base/src/main/java/org/aya/core/serde/SerTerm.java b/base/src/main/java/org/aya/core/serde/SerTerm.java index 12d21359b..4af88d9bd 100644 --- a/base/src/main/java/org/aya/core/serde/SerTerm.java +++ b/base/src/main/java/org/aya/core/serde/SerTerm.java @@ -359,7 +359,7 @@ sealed interface SerShapedApplicable extends Serializable permits SerIntegerOps record ConInfo( SerDef.SerShapeResult result, SerTerm.Data data - ) {} + ) implements Serializable {} record SerIntegerOps( @NotNull SerDef.QName ref, diff --git a/base/src/main/java/org/aya/core/serde/Serializer.java b/base/src/main/java/org/aya/core/serde/Serializer.java index 0e86b9cf1..d7f8a62e5 100644 --- a/base/src/main/java/org/aya/core/serde/Serializer.java +++ b/base/src/main/java/org/aya/core/serde/Serializer.java @@ -9,6 +9,7 @@ import kala.tuple.Tuple; import org.aya.core.def.*; import org.aya.core.pat.Pat; +import org.aya.core.repr.AyaShape; import org.aya.core.term.*; import org.aya.generic.Shaped; import org.aya.guest0x0.cubical.Partial; @@ -18,13 +19,15 @@ import org.aya.util.error.InternalException; import org.jetbrains.annotations.Contract; import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; /** * @author ice1000 */ -public record Serializer(@NotNull Serializer.State state) { - public @NotNull SerDef serialize(@NotNull GenericDef def, @Nullable SerDef.SerShapeResult shapeResult) { +public record Serializer( + @NotNull Serializer.State state, + @NotNull AyaShape.Factory factory +) { + public @NotNull SerDef serialize(@NotNull GenericDef def) { return switch (def) { case FnDef fn -> new SerDef.Fn( state.def(fn.ref), @@ -32,7 +35,9 @@ public record Serializer(@NotNull Serializer.State state) { fn.body.map(this::serialize, matchings -> matchings.map(this::serialize)), fn.modifiers, serialize(fn.result), - shapeResult + factory.find(def) + .map(x -> SerDef.SerShapeResult.serialize(state, x)) + .getOrNull() ); case MemberDef field -> new SerDef.Field( state.def(field.classRef), @@ -43,13 +48,13 @@ public record Serializer(@NotNull Serializer.State state) { ); case ClassDef clazz -> new SerDef.Clazz( state.def(clazz.ref()), - clazz.members.map(field -> (SerDef.Field) serialize(field, null)) + clazz.members.map(field -> (SerDef.Field) serialize(field)) ); case DataDef data -> new SerDef.Data( state.def(data.ref), serializeParams(data.telescope), serialize(data.result), - data.body.map(ctor -> (SerDef.Ctor) serialize(ctor, null)) + data.body.map(ctor -> (SerDef.Ctor) serialize(ctor)) ); case PrimDef prim -> { assert prim.ref.module != null; @@ -185,9 +190,10 @@ case PAppTerm(var of, var args, var cube) -> new SerTerm.PathApp(serialize(of), private @NotNull SerTerm.SerShapedApplicable serializeShapedApplicable(@NotNull Shaped.Applicable shapedApplicable) { return switch (shapedApplicable) { - case IntegerOps.ConRule conRule -> new SerTerm.SerIntegerOps(state.def(conRule.ref()), Either.left(new SerTerm.ConInfo( - SerDef.SerShapeResult.serialize(state, conRule.paramRecognition()), (SerTerm.Data) serialize(conRule.paramType()) - ))); + case IntegerOps.ConRule conRule -> + new SerTerm.SerIntegerOps(state.def(conRule.ref()), Either.left(new SerTerm.ConInfo( + SerDef.SerShapeResult.serialize(state, conRule.paramRecognition()), (SerTerm.Data) serialize(conRule.paramType()) + ))); case IntegerOps.FnRule fnRule -> new SerTerm.SerIntegerOps(state.def(fnRule.ref()), Either.right(fnRule.kind())); default -> throw new IllegalStateException("Unexpected value: " + shapedApplicable); }; diff --git a/base/src/test/java/org/aya/core/SuedeTest.java b/base/src/test/java/org/aya/core/SuedeTest.java index cacde7227..ddd79c812 100644 --- a/base/src/test/java/org/aya/core/SuedeTest.java +++ b/base/src/test/java/org/aya/core/SuedeTest.java @@ -74,9 +74,9 @@ prim strcat (str1 str2: String) : String private void suedeAll(@Language("Aya") @NotNull String code) { var res = TyckDeclTest.successTyckDecls(code); var state = new SerTerm.DeState(res.component1()); - var serializer = new Serializer(new Serializer.State()); + var serializer = new Serializer(new Serializer.State(), res.component3()); res.component2().view() - .map(x -> serializer.serialize(x, null)) + .map(serializer::serialize) .map(ser -> ser.de(state)) .forEach(Assertions::assertNotNull); } diff --git a/base/src/test/java/org/aya/tyck/TyckDeclTest.java b/base/src/test/java/org/aya/tyck/TyckDeclTest.java index 09cef499b..a509e833a 100644 --- a/base/src/test/java/org/aya/tyck/TyckDeclTest.java +++ b/base/src/test/java/org/aya/tyck/TyckDeclTest.java @@ -5,6 +5,7 @@ import kala.collection.immutable.ImmutableSeq; import kala.tuple.Tuple; import kala.tuple.Tuple2; +import kala.tuple.Tuple3; import org.aya.concrete.ParseTest; import org.aya.concrete.stmt.Stmt; import org.aya.concrete.stmt.decl.TeleDecl; @@ -54,13 +55,13 @@ public static void header(@NotNull PrimDef.Factory factory, @NotNull TeleDecl return primFactory; } - public static @NotNull Tuple2> + public static @NotNull Tuple3, AyaShape.Factory> successTyckDecls(@Language("Aya") @NonNls @NotNull String text) { var res = successDesugarDecls(text); var shapes = new AyaShape.Factory(); return Tuple.of(res.component1(), res.component2().view() .map(i -> i instanceof TeleDecl s ? tyck(res.component1(), s, null, shapes) : null) - .filter(Objects::nonNull).toImmutableSeq()); + .filter(Objects::nonNull).toImmutableSeq(), shapes); } public static @NotNull Tuple2>