merge: Fix two issues related to arrays and meta lit terms, implement…

… `debug-show-shapes` (#1147) As title
aya-prover · Nov 18, 2024 · 038fdba · 038fdba
2 parents 55cdeb6 + 66cb8a2
commit 038fdba
Show file tree

Hide file tree

Showing 13 changed files with 91 additions and 10 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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<RenderOptions.StyleFamilyName, Path> 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -29,7 +29,10 @@ public record MetaLitTerm(
   }
 
   @SuppressWarnings("unchecked") public @NotNull Term inline(UnaryOperator<Term> 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();