From c5d8ff280d7d3adb24087cff4dd4134596a58b87 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Thu, 4 Jan 2024 21:26:41 +0800 Subject: [PATCH] concrete: more Expr --- base/src/main/java/module-info.java | 3 +- .../main/java/org/aya/generic/SortKind.java | 11 ++ .../aya/syntax/concrete/{expr => }/Expr.java | 120 +++++++++++++----- 3 files changed, 103 insertions(+), 31 deletions(-) create mode 100644 base/src/main/java/org/aya/generic/SortKind.java rename base/src/main/java/org/aya/syntax/concrete/{expr => }/Expr.java (54%) diff --git a/base/src/main/java/module-info.java b/base/src/main/java/module-info.java index 3cbc5238..a8c982ae 100644 --- a/base/src/main/java/module-info.java +++ b/base/src/main/java/module-info.java @@ -16,5 +16,6 @@ exports org.aya.syntax.core.def; exports org.aya.syntax.core.term; exports org.aya.syntax.ref; - exports org.aya.syntax.concrete.expr; + exports org.aya.generic; + exports org.aya.syntax.concrete; } diff --git a/base/src/main/java/org/aya/generic/SortKind.java b/base/src/main/java/org/aya/generic/SortKind.java new file mode 100644 index 00000000..7e4f408a --- /dev/null +++ b/base/src/main/java/org/aya/generic/SortKind.java @@ -0,0 +1,11 @@ +// Copyright (c) 2020-2023 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.generic; + +public enum SortKind { + Type, Set, ISet; + + public boolean hasLevel() { + return this == Type || this == Set; + } +} diff --git a/base/src/main/java/org/aya/syntax/concrete/expr/Expr.java b/base/src/main/java/org/aya/syntax/concrete/Expr.java similarity index 54% rename from base/src/main/java/org/aya/syntax/concrete/expr/Expr.java rename to base/src/main/java/org/aya/syntax/concrete/Expr.java index 3fe5ed1e..664e6cee 100644 --- a/base/src/main/java/org/aya/syntax/concrete/expr/Expr.java +++ b/base/src/main/java/org/aya/syntax/concrete/Expr.java @@ -1,11 +1,14 @@ -package org.aya.syntax.concrete.expr; +// 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.syntax.concrete; import kala.collection.immutable.ImmutableSeq; import kala.value.MutableValue; +import org.aya.generic.SortKind; import org.aya.syntax.ref.LocalVar; import org.aya.util.BinOpElem; -import org.aya.util.error.SourceNode; import org.aya.util.error.SourcePos; +import org.aya.util.error.WithPos; import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; @@ -14,30 +17,23 @@ public sealed interface Expr { @NotNull Expr descent(@NotNull UnaryOperator<@NotNull Expr> f); - record Node(@NotNull SourcePos sourcePos, @NotNull Expr expr) implements SourceNode { - public @NotNull Node map(@NotNull UnaryOperator mapper) { - var result = mapper.apply(expr); - return result == expr ? this : new Node(sourcePos, result); - } - } - record Param( @NotNull SourcePos sourcePos, @NotNull LocalVar ref, - @NotNull Node type, + @NotNull WithPos type, boolean explicit // @ForLSP MutableValue theCore ) { public Param(@NotNull SourcePos sourcePos, @NotNull LocalVar var, boolean explicit) { - this(sourcePos, var, new Node(sourcePos, new Hole(false, null)), explicit); + this(sourcePos, var, new WithPos<>(sourcePos, new Hole(false, null)), explicit); } - public @NotNull Param update(@NotNull Node type) { + public @NotNull Param update(@NotNull WithPos type) { return type == type() ? this : new Param(sourcePos, ref, type, explicit); } public @NotNull Param descent(@NotNull UnaryOperator f) { - return update(type.map(f)); + return update(type.descent(f)); } } @@ -48,7 +44,7 @@ public Param(@NotNull SourcePos sourcePos, @NotNull LocalVar var, boolean explic */ record Hole( boolean explicit, - @Nullable Expr filling, + @Nullable Expr filling, // TODO MutableValue> accessibleLocal ) implements Expr { public Hole(boolean explicit, @Nullable Expr filling) { @@ -79,35 +75,35 @@ record Ref(@NotNull LocalVar var) implements Expr { } } - record Lam(@NotNull Param param, @NotNull Node body) implements Expr { - public @NotNull Lam update(@NotNull Param param, @NotNull Node body) { + record Lam(@NotNull Param param, @NotNull WithPos body) implements Expr { + public @NotNull Lam update(@NotNull Param param, @NotNull WithPos body) { return param == param() && body == body() ? this : new Lam(param, body); } @Override public @NotNull Lam descent(@NotNull UnaryOperator<@NotNull Expr> f) { - return update(param.descent(f), body.map(f)); + return update(param.descent(f), body.descent(f)); } } record Tuple( - @NotNull ImmutableSeq<@NotNull Node> items + @NotNull ImmutableSeq<@NotNull WithPos> items ) implements Expr { - public @NotNull Expr.Tuple update(@NotNull ImmutableSeq<@NotNull Node> items) { + public @NotNull Expr.Tuple update(@NotNull ImmutableSeq<@NotNull WithPos> items) { return items.sameElements(items(), true) ? this : new Tuple(items); } @Override public @NotNull Expr.Tuple descent(@NotNull UnaryOperator<@NotNull Expr> f) { - return update(items.map(x -> x.map(f))); + return update(items.map(x -> x.descent(f))); } } - record App(@NotNull Node function, @NotNull NamedArg argument) implements Expr { - public @NotNull App update(@NotNull Node function, @NotNull NamedArg argument) { + record App(@NotNull WithPos function, @NotNull NamedArg argument) implements Expr { + public @NotNull App update(@NotNull WithPos function, @NotNull NamedArg argument) { return function == function() && argument == argument() ? this : new App(function, argument); } @Override public @NotNull App descent(@NotNull UnaryOperator<@NotNull Expr> f) { - return update(function.map(f), argument.descent(f)); + return update(function.descent(f), argument.descent(f)); } } @@ -115,32 +111,32 @@ record NamedArg( @NotNull SourcePos sourcePos, @Override boolean explicit, @Nullable String name, - @NotNull Node arg + @NotNull WithPos arg ) implements BinOpElem { @Override public @NotNull Expr term() { - return arg.expr(); + return arg.data(); } - public @NotNull NamedArg update(@NotNull Node expr) { + public @NotNull NamedArg update(@NotNull WithPos expr) { return expr == arg ? this : new NamedArg(sourcePos, explicit, name, expr); } public @NotNull NamedArg descent(@NotNull UnaryOperator<@NotNull Expr> f) { - return update(arg.map(f)); + return update(arg.descent(f)); } } record Pi( @NotNull Param param, - @NotNull Node last + @NotNull WithPos last ) implements Expr { - public @NotNull Pi update(@NotNull Param param, @NotNull Node last) { + public @NotNull Pi update(@NotNull Param param, @NotNull WithPos last) { return param == param() && last == last() ? this : new Pi(param, last); } @Override public @NotNull Pi descent(@NotNull UnaryOperator<@NotNull Expr> f) { - return update(param.descent(f), last.map(f)); + return update(param.descent(f), last.descent(f)); } } @@ -155,4 +151,68 @@ record Sigma( return update(params.map(param -> param.descent(f))); } } + + record RawSort(@NotNull SourcePos sourcePos, @NotNull SortKind kind) implements Expr { + @Override public @NotNull RawSort descent(@NotNull UnaryOperator<@NotNull Expr> f) { + return this; + } + } + + sealed interface Sort extends Expr { + int lift(); + + SortKind kind(); + + @Override default @NotNull Sort descent(@NotNull UnaryOperator<@NotNull Expr> f) { + return this; + } + } + + record Type(@Override int lift) implements Sort { + @Override public SortKind kind() { + return SortKind.Type; + } + } + + record Set(@Override int lift) implements Sort { + @Override public SortKind kind() { + return SortKind.Set; + } + } + + enum ISet implements Sort { + INSTANCE; + + @Override public int lift() { + return 0; + } + + @Override public SortKind kind() { + return SortKind.ISet; + } + } + + record LitInt(int integer) implements Expr { + @Override public @NotNull LitInt descent(@NotNull UnaryOperator<@NotNull Expr> f) { + return this; + } + } + + record LitString(@NotNull String string) implements Expr { + @Override public @NotNull LitString descent(@NotNull UnaryOperator<@NotNull Expr> f) { + return this; + } + } + + record BinOpSeq( + @NotNull ImmutableSeq seq + ) implements Expr { + public @NotNull BinOpSeq update(@NotNull ImmutableSeq seq) { + return seq.sameElements(seq(), true) ? this : new BinOpSeq(seq); + } + + @Override public @NotNull BinOpSeq descent(@NotNull UnaryOperator<@NotNull Expr> f) { + return update(seq.map(arg -> arg.descent(f))); + } + } }