diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java index 2f5e5e872c..44a2c1ce79 100644 --- a/base/src/main/java/org/aya/normalize/Normalizer.java +++ b/base/src/main/java/org/aya/normalize/Normalizer.java @@ -15,6 +15,7 @@ import org.aya.syntax.core.term.call.*; import org.aya.syntax.core.term.marker.BetaRedex; import org.aya.syntax.core.term.marker.StableWHNF; +import org.aya.syntax.core.term.repr.MetaLitTerm; import org.aya.syntax.core.term.xtt.CoeTerm; import org.aya.syntax.core.term.xtt.DimTerm; import org.aya.syntax.literate.CodeOptions.NormalizeMode; @@ -88,8 +89,9 @@ yield switch (reduceRule) { case ConCall call when call.conArgs().getLast() instanceof DimTerm dim -> call.head().ref().equality(call.args(), dim == DimTerm.I0); case PrimCall prim -> state.primFactory.unfold(prim, state); - case MetaPatTerm metaTerm -> metaTerm.inline(this); + case MetaPatTerm meta -> meta.inline(this); case MetaCall meta -> state.computeSolution(meta, this); + case MetaLitTerm meta -> meta.inline(this); case CoeTerm(var type, var r, var s) -> { if (r instanceof DimTerm || r instanceof FreeTerm) { if (r.equals(s)) yield new LamTerm(new LocalTerm(0)); diff --git a/base/src/main/java/org/aya/normalize/error/UnsolvedLit.java b/base/src/main/java/org/aya/normalize/error/UnsolvedLit.java index e53ee93801..0c84acee87 100644 --- a/base/src/main/java/org/aya/normalize/error/UnsolvedLit.java +++ b/base/src/main/java/org/aya/normalize/error/UnsolvedLit.java @@ -9,9 +9,7 @@ import org.aya.util.reporter.Problem; import org.jetbrains.annotations.NotNull; -public record UnsolvedLit( - @NotNull MetaLitTerm lit -) implements Problem { +public record UnsolvedLit(@NotNull MetaLitTerm lit) implements Problem { @Override public @NotNull SourcePos sourcePos() { return lit.sourcePos(); } @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { return Doc.vcat( diff --git a/base/src/main/java/org/aya/resolve/module/ModuleLoader.java b/base/src/main/java/org/aya/resolve/module/ModuleLoader.java index be3a32843b..2dd903e086 100644 --- a/base/src/main/java/org/aya/resolve/module/ModuleLoader.java +++ b/base/src/main/java/org/aya/resolve/module/ModuleLoader.java @@ -70,7 +70,7 @@ public interface ModuleLoader extends Problematic { /** * Resolve a certain module. * - * @param context the context of the module + * @param resolveInfo the context of the module * @param program the statements of the module * @param recurseLoader the module loader that used to resolve */ diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java index 1f0761515b..9fe4a60e54 100644 --- a/base/src/main/java/org/aya/tyck/ExprTycker.java +++ b/base/src/main/java/org/aya/tyck/ExprTycker.java @@ -15,6 +15,7 @@ import org.aya.syntax.core.def.DataDefLike; import org.aya.syntax.core.def.PrimDef; import org.aya.syntax.core.repr.AyaShape; +import org.aya.syntax.core.repr.ShapeRecognition; import org.aya.syntax.core.term.*; import org.aya.syntax.core.term.call.ClassCall; import org.aya.syntax.core.term.call.DataCall; @@ -130,6 +131,16 @@ case PiTerm(var dom, var cod) -> { }; yield new Jdg.Default(wellTyped, sigmaTerm); } + case Expr.Array arr when arr.arrayBlock().isRight() + && whnf(type) instanceof DataCall dataCall + && state.shapeFactory.find(dataCall.ref()).getOrNull() instanceof ShapeRecognition recog + && recog.shape() == AyaShape.LIST_SHAPE -> { + var arrayBlock = arr.arrayBlock().getRightValue(); + var elementTy = dataCall.args().get(0); + var results = ImmutableTreeSeq.from(arrayBlock.exprList().map( + element -> inherit(element, elementTy).wellTyped())); + yield new Jdg.Default(new ListTerm(results, recog, dataCall), type); + } case Expr.Let let -> checkLet(let, e -> inherit(e, type)); default -> inheritFallbackUnify(type, synthesize(expr), expr); }; @@ -320,8 +331,9 @@ yield subscoped(param.ref(), wellParam, () -> var defs = state.shapeFactory.findImpl(AyaShape.LIST_SHAPE); if (defs.isEmpty()) yield fail(arr, new NoRuleError(expr, null)); if (defs.sizeGreaterThan(1)) { + var elMeta = freshMeta("el_ty", expr.sourcePos(), MetaVar.Misc.IsType, false); var tyMeta = freshMeta("arr_ty", expr.sourcePos(), MetaVar.Misc.IsType, false); - var results = elements.map(element -> inherit(element, tyMeta).wellTyped()); + var results = elements.map(element -> inherit(element, elMeta).wellTyped()); yield new Jdg.Default(new MetaLitTerm(expr.sourcePos(), results, defs, tyMeta), tyMeta); } var match = defs.getFirst(); diff --git a/base/src/main/java/org/aya/tyck/tycker/AbstractTycker.java b/base/src/main/java/org/aya/tyck/tycker/AbstractTycker.java index 49b6aa29f7..db3a8c5d1e 100644 --- a/base/src/main/java/org/aya/tyck/tycker/AbstractTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/AbstractTycker.java @@ -15,7 +15,6 @@ import org.aya.tyck.TyckState; import org.aya.unify.Synthesizer; import org.aya.unify.TermComparator; -import org.aya.util.error.WithPos; import org.aya.util.reporter.Reporter; import org.jetbrains.annotations.NotNull; diff --git a/cli-console/src/main/java/org/aya/cli/repl/AyaRepl.java b/cli-console/src/main/java/org/aya/cli/repl/AyaRepl.java index 4db15e20a8..9b2b218c44 100644 --- a/cli-console/src/main/java/org/aya/cli/repl/AyaRepl.java +++ b/cli-console/src/main/java/org/aya/cli/repl/AyaRepl.java @@ -79,6 +79,7 @@ public CommandManager makeCommand() { ReplCommands.SHOW_CWD, ReplCommands.SHOW_PROPERTY, ReplCommands.SHOW_MODULE_PATHS, + ReplCommands.SHOW_SHAPES, ReplCommands.LOAD, ReplCommands.COLOR, ReplCommands.STYLE diff --git a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java index 1308585a44..f5ae0c289e 100644 --- a/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java +++ b/cli-console/src/main/java/org/aya/cli/repl/ReplCommands.java @@ -3,9 +3,12 @@ package org.aya.cli.repl; import kala.collection.immutable.ImmutableSeq; +import kala.collection.mutable.MutableList; import kala.control.Either; import org.aya.cli.render.RenderOptions; import org.aya.prettier.AyaPrettierOptions; +import org.aya.prettier.BasePrettier; +import org.aya.pretty.doc.Doc; import org.aya.producer.AyaParserImpl; import org.aya.repl.Command; import org.aya.repl.CommandArg; @@ -76,6 +79,17 @@ record StyleParam(@NotNull Either value) } }; + @NotNull Command SHOW_SHAPES = new Command(ImmutableSeq.of("debug-show-shapes"), "Show recognized shapes") { + @Entry public @NotNull Command.Result execute(@NotNull AyaRepl repl) { + var discovered = repl.replCompiler.getShapeFactory().discovered; + return Result.ok(repl.renderDoc(Doc.vcat(discovered.mapTo(MutableList.create(), + (def, recog) -> + Doc.sep(BasePrettier.refVar(def), + Doc.symbol("=>"), + Doc.plain(recog.shape().name()))))), true); + } + }; + @NotNull Command LOAD = new Command(ImmutableSeq.of("load"), "Load a file or library into REPL") { @Entry public @NotNull Command.Result execute(@NotNull AyaRepl repl, @NotNull Path path) { try { diff --git a/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java b/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java index 839c828d4f..9ec4d076e9 100644 --- a/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java +++ b/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java @@ -16,6 +16,7 @@ import org.aya.generic.InterruptException; import org.aya.normalize.Normalizer; import org.aya.primitive.PrimFactory; +import org.aya.primitive.ShapeFactory; import org.aya.producer.AyaParserImpl; import org.aya.resolve.ResolveInfo; import org.aya.resolve.context.EmptyContext; @@ -206,6 +207,7 @@ private void loadFile(@NotNull Path file) { } public @NotNull ReplContext getContext() { return context; } + public @NotNull ShapeFactory getShapeFactory() { return shapeFactory; } public void loadPreludeIfPossible() { if (loader.existsFileLevelModule(ModulePath.of("prelude"))) { compileToContext("open import prelude", NormalizeMode.NULL); diff --git a/cli-impl/src/test/resources/negative/GoalAndMeta.txt b/cli-impl/src/test/resources/negative/GoalAndMeta.txt index de68efcb89..7b35bf2ab1 100644 --- a/cli-impl/src/test/resources/negative/GoalAndMeta.txt +++ b/cli-impl/src/test/resources/negative/GoalAndMeta.txt @@ -192,6 +192,36 @@ Error: Unsolved meta _ Let's learn from that. LiteralAmbiguous3: +In file $FILE:6:4 -> + + 4 │ + 5 │ def good : List Unit => [ ] + 6 │ def bad => [ unit ] + │ ╰─╯ + +Error: Unsolved meta _ + +In file $FILE:6:4 -> + + 4 │ + 5 │ def good : List Unit => [ ] + 6 │ def bad => [ unit ] + │ ╰─╯ + +Error: Unsolved meta _ + in `?_` + in `[unit]` + +In file $FILE:6:4 -> + + 4 │ + 5 │ def good : List Unit => [ ] + 6 │ def bad => [ unit ] + │ ╰─╯ + +Error: Unsolved meta _ + in `[unit]` + In file $FILE:6:11 -> 4 │ @@ -204,7 +234,7 @@ Error: Unable to solve the type of this literal: I'm confused about the following candidates: `List`, `List2` -1 error(s), 0 warning(s). +4 error(s), 0 warning(s). Let's learn from that. NonPattern: diff --git a/cli-impl/src/test/resources/success/src/Test.aya b/cli-impl/src/test/resources/success/src/Test.aya index 37af8bb485..68b5a0b546 100644 --- a/cli-impl/src/test/resources/success/src/Test.aya +++ b/cli-impl/src/test/resources/success/src/Test.aya @@ -19,3 +19,20 @@ module Issue1130 { def f (p : I -> Nat) => 0 def test => f (refl {a := 1}) } + +module Issue1144 { + open inductive NewList (A : Type) + | newNil + | newCons A (NewList A) + + private def test : NewList Nat => [ 0 ] +} + +module Issue1145 { + open Issue1144 + open inductive NewNat : Type + | newZero + | newSucc (pred : NewNat) + + def test : NewList Nat => [ 0 ] +} diff --git a/cli-impl/src/test/resources/success/src/TestNoExtraLists.aya b/cli-impl/src/test/resources/success/src/TestNoExtraLists.aya new file mode 100644 index 0000000000..cabd8c847c --- /dev/null +++ b/cli-impl/src/test/resources/success/src/TestNoExtraLists.aya @@ -0,0 +1,3 @@ +open import prelude + +def canonicalList => [ 114514 ] diff --git a/jit-compiler/src/test/resources/TreeSort.aya b/jit-compiler/src/test/resources/TreeSort.aya index a640bd5832..2f660bef32 100644 --- a/jit-compiler/src/test/resources/TreeSort.aya +++ b/jit-compiler/src/test/resources/TreeSort.aya @@ -54,7 +54,7 @@ def insert (a : A) (node : RBTree A) (dec_le : Decider A) : RBTree A elim node | rbLeaf => rbNode red rbLeaf a rbLeaf | rbNode c l1 a1 l2 => insert_lemma dec_le a a1 c l1 l2 (dec_le a1 a) -private def aux (l : List A) (r : RBTree A) (dec_le : Decider A) : RBTree A elim l +private def aux (ls : List A) (r : RBTree A) (dec_le : Decider A) : RBTree A elim ls | [] => r | a :> l => aux l (repaint (insert a r dec_le)) dec_le def tree_sort (dec_le : Decider A) (l : List A) => rbTreeToList (aux l rbLeaf dec_le) [] diff --git a/syntax/src/main/java/org/aya/syntax/core/term/repr/MetaLitTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/repr/MetaLitTerm.java index 44934ab8e0..58f95e0a2e 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/repr/MetaLitTerm.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/repr/MetaLitTerm.java @@ -29,7 +29,10 @@ public record MetaLitTerm( } @SuppressWarnings("unchecked") public @NotNull Term inline(UnaryOperator pre) { - if (!(pre.apply(type) instanceof DataCall dataCall)) return this; + var normalizedType = pre.apply(type); + // really? + // if (normalizedType == DimTyTerm.INSTANCE) return (int) repr == 0 ? DimTerm.I0 : DimTerm.I1; + if (!(normalizedType instanceof DataCall dataCall)) return this; return candidates.find(t -> t.def().equals(dataCall.ref())).flatMap(t -> { var recog = t.recog(); var shape = recog.shape();