shape: fix @ice1000

aya-prover · Oct 20, 2023 · 43008ff · 43008ff
1 parent 21e771d
commit 43008ff
Show file tree

Hide file tree

Showing 10 changed files with 40 additions and 43 deletions.
diff --git a/base/src/main/java/org/aya/core/repr/AyaShape.java b/base/src/main/java/org/aya/core/repr/AyaShape.java
@@ -11,13 +11,15 @@
 import kala.tuple.Tuple2;
 import org.aya.core.def.Def;
 import org.aya.core.def.GenericDef;
+import org.aya.util.Arg;
 import org.jetbrains.annotations.NotNull;
 
 import static org.aya.core.repr.CodeShape.*;
 import static org.aya.core.repr.CodeShape.GlobalId.*;
 import static org.aya.core.repr.CodeShape.LocalId.LHS;
 import static org.aya.core.repr.CodeShape.LocalId.RHS;
 import static org.aya.core.repr.ParamShape.anyLicit;
+import static org.aya.core.repr.ParamShape.explicit;
 
 /**
  * @author kiva
@@ -53,12 +55,12 @@ enum AyaListShape implements AyaShape {
 
     public static final @NotNull CodeShape DATA_LIST = new DataShape(
       LIST,
-      ImmutableSeq.of(anyLicit(A, new TermShape.Sort(null, 0))),
+      ImmutableSeq.of(explicit(A, new TermShape.Sort(null, 0))),
       ImmutableSeq.of(
         new CtorShape(GlobalId.NIL, ImmutableSeq.empty()),
         new CtorShape(GlobalId.CONS, ImmutableSeq.of(
-          anyLicit(TermShape.NameCall.of(A)),
-          anyLicit(new TermShape.NameCall(LIST, ImmutableSeq.of(TermShape.NameCall.of(A))))
+          explicit(TermShape.NameCall.of(A)),
+          explicit(new TermShape.NameCall(LIST, ImmutableSeq.of(new Arg<>(TermShape.NameCall.of(A), true))))
         )) // List A
       ));
 
@@ -74,8 +76,8 @@ enum AyaPlusFnShape implements AyaShape {
       NAT_ADD,
       // _ : Nat -> Nat -> Nat
       ImmutableSeq.of(
-        anyLicit(new TermShape.ShapeCall(NAT, AyaIntShape.DATA_NAT, ImmutableSeq.empty())),
-        anyLicit(TermShape.NameCall.of(NAT))
+        explicit(new TermShape.ShapeCall(NAT, AyaIntShape.DATA_NAT, ImmutableSeq.empty())),
+        explicit(TermShape.NameCall.of(NAT))
       ),
       TermShape.NameCall.of(NAT),
       Either.right(ImmutableSeq.of(
@@ -86,10 +88,10 @@ enum AyaPlusFnShape implements AyaShape {
         // | a, suc b => suc (_ a b)
         new ClauseShape(ImmutableSeq.of(
           new PatShape.Bind(LHS), new PatShape.ShapedCtor(NAT, SUC, ImmutableSeq.of(new PatShape.Bind(RHS)))
-        ), new TermShape.CtorCall(NAT, SUC, ImmutableSeq.of(new TermShape.NameCall(NAT_ADD, ImmutableSeq.of(
-          TermShape.NameCall.of(LHS),
-          TermShape.NameCall.of(RHS)
-        )))))
+        ), new TermShape.CtorCall(NAT, SUC, ImmutableSeq.of(new Arg<>(new TermShape.NameCall(NAT_ADD, ImmutableSeq.of(
+          new Arg<>(TermShape.NameCall.of(LHS), true),    // TODO: licit
+          new Arg<>(TermShape.NameCall.of(RHS), true)
+        )), true))))
       ))
     );
 
@@ -106,8 +108,8 @@ enum AyaPlusFnLeftShape implements AyaShape {
       NAT_ADD,
       // _ : Nat -> Nat -> Nat
       ImmutableSeq.of(
-        anyLicit(new TermShape.ShapeCall(GlobalId.NAT, AyaIntShape.DATA_NAT, ImmutableSeq.empty())),
-        anyLicit(TermShape.NameCall.of(NAT))
+        explicit(new TermShape.ShapeCall(GlobalId.NAT, AyaIntShape.DATA_NAT, ImmutableSeq.empty())),
+        explicit(TermShape.NameCall.of(NAT))
       ),
       TermShape.NameCall.of(NAT),
       Either.right(ImmutableSeq.of(
@@ -118,10 +120,10 @@ enum AyaPlusFnLeftShape implements AyaShape {
         // | suc a, b => _ a (suc b)
         new ClauseShape(ImmutableSeq.of(
           new PatShape.ShapedCtor(NAT, SUC, ImmutableSeq.of(new PatShape.Bind(LHS))), new PatShape.Bind(RHS)
-        ), new TermShape.CtorCall(NAT, SUC, ImmutableSeq.of(new TermShape.NameCall(NAT_ADD, ImmutableSeq.of(
-          TermShape.NameCall.of(LHS),
-          TermShape.NameCall.of(RHS)
-        )))))
+        ), new TermShape.CtorCall(NAT, SUC, ImmutableSeq.of(new Arg<>(new TermShape.NameCall(NAT_ADD, ImmutableSeq.of(
+          new Arg<>(TermShape.NameCall.of(LHS), true),
+          new Arg<>(TermShape.NameCall.of(RHS), true)
+        )), true))))
       ))
     );
 

diff --git a/base/src/main/java/org/aya/core/repr/CodeShape.java b/base/src/main/java/org/aya/core/repr/CodeShape.java
@@ -50,7 +50,7 @@ record DataShape(
   ) implements CodeShape, Moment {}
 
   record CtorShape(
-    @NotNull MomentId name,
+    @NotNull GlobalId name,
     @NotNull ImmutableSeq<ParamShape> tele
   ) implements CodeShape, Moment {}
 }
diff --git a/base/src/main/java/org/aya/core/repr/ParamShape.java b/base/src/main/java/org/aya/core/repr/ParamShape.java
@@ -23,7 +23,11 @@ enum Kind {
   }
 
   static @NotNull ParamShape explicit(@NotNull TermShape type) {
-    return new Licit(CodeShape.LocalId.IGNORED, type, Licit.Kind.Ex);
+    return explicit(CodeShape.LocalId.IGNORED, type);
+  }
+
+  static @NotNull ParamShape explicit(@NotNull CodeShape.LocalId name, @NotNull TermShape type) {
+    return new Licit(name, type, Licit.Kind.Ex);
   }
 
   static @NotNull ParamShape implicit(@NotNull TermShape type) {

diff --git a/base/src/main/java/org/aya/core/repr/PatShape.java b/base/src/main/java/org/aya/core/repr/PatShape.java
@@ -31,9 +31,9 @@ record Ctor(@NotNull ImmutableSeq<PatShape> innerPats) implements CtorLike {
    * @param dataId a reference to a {@link CodeShape.DataShape}d term
    * @param ctorId the {@link CodeShape.MomentId} to the ctor
    */
-  record ShapedCtor(@NotNull CodeShape.MomentId dataId, @NotNull CodeShape.MomentId ctorId,
+  record ShapedCtor(@NotNull CodeShape.MomentId dataId, @NotNull CodeShape.GlobalId ctorId,
                     @NotNull ImmutableSeq<PatShape> innerPats) implements CtorLike {
-    public static @NotNull ShapedCtor of(@NotNull CodeShape.MomentId name, @NotNull CodeShape.MomentId id) {
+    public static @NotNull ShapedCtor of(@NotNull CodeShape.MomentId name, @NotNull CodeShape.GlobalId id) {
       return new ShapedCtor(name, id, ImmutableSeq.empty());
     }
   }

diff --git a/base/src/main/java/org/aya/core/repr/ShapeMatcher.java b/base/src/main/java/org/aya/core/repr/ShapeMatcher.java
@@ -53,7 +53,7 @@ public record Captures(
       return new Captures(MutableMap.create(), MutableValue.create());
     }
 
-    public @NotNull ImmutableMap<MomentId, DefVar<?, ?>> extractGlobal() {
+    public @NotNull ImmutableMap<GlobalId, DefVar<?, ?>> extractGlobal() {
       return ImmutableMap.from(map.toImmutableSeq().view()
         .mapNotNull(x -> switch (new Pair<>(x.component1(), x.component2())) {
           case Pair(GlobalId gid, DefVar<?, ?> dv) -> Tuple.of(gid, dv);
@@ -217,8 +217,8 @@ yield captureIfMatches(shapeCall.name(), defVar, () ->
         };
 
         if (!success) yield false;
-        yield matchMany(MatchMode.OrderedEq, call.args(), callable.args(),
-          (l, r) -> matchTerm(l, r.term()));
+        yield matchMany(MatchMode.OrderedEq, call.args(), callable.args(), (s, c) ->
+          s.explicit() == c.explicit() && matchTerm(s.term(), c.term()));
       }
       case TermShape.Sort sort when term instanceof SortTerm sortTerm -> {
         // kind is null -> any sort
@@ -315,7 +315,7 @@ private static <S, C> boolean matchMany(
     return remainingShapes.isEmpty() || mode == MatchMode.Sup;
   }
 
-  private @NotNull DefVar<?, ?> resolveCtor(@NotNull MomentId data, @NotNull CodeShape.MomentId ctorId) {
+  private @NotNull DefVar<?, ?> resolveCtor(@NotNull MomentId data, @NotNull CodeShape.GlobalId ctorId) {
     if (!(captures.resolve(data) instanceof DefVar<?, ?> defVar)) {
       throw new InternalException("Not a data");
     }

diff --git a/base/src/main/java/org/aya/core/repr/ShapeRecognition.java b/base/src/main/java/org/aya/core/repr/ShapeRecognition.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// 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.core.repr;
 
@@ -8,5 +8,5 @@
 
 public record ShapeRecognition(
   @NotNull AyaShape shape,
-  @NotNull ImmutableMap<CodeShape.MomentId, DefVar<?, ?>> captures
+  @NotNull ImmutableMap<CodeShape.GlobalId, DefVar<?, ?>> captures
 ) {}
diff --git a/base/src/main/java/org/aya/core/repr/TermShape.java b/base/src/main/java/org/aya/core/repr/TermShape.java
@@ -5,6 +5,7 @@
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.core.term.Term;
 import org.aya.generic.SortKind;
+import org.aya.util.Arg;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -26,18 +27,19 @@ enum Any implements TermShape {
   record Sort(@Nullable SortKind kind, int ulift) implements TermShape {}
 
   sealed interface Callable extends TermShape {
-    @NotNull ImmutableSeq<TermShape> args();
+    @NotNull ImmutableSeq<Arg<TermShape>> args();
   }
 
-  record NameCall(@NotNull CodeShape.MomentId name, @Override @NotNull ImmutableSeq<TermShape> args) implements Callable {
+  record NameCall(@NotNull CodeShape.MomentId name,
+                  @Override @NotNull ImmutableSeq<Arg<TermShape>> args) implements Callable {
     public static @NotNull NameCall of(@NotNull CodeShape.MomentId name) {
       return new NameCall(name, ImmutableSeq.empty());
     }
   }
 
   record ShapeCall(@NotNull CodeShape.MomentId name, @NotNull CodeShape shape,
-                   @Override @NotNull ImmutableSeq<TermShape> args) implements Callable, CodeShape.Moment {}
+                   @Override @NotNull ImmutableSeq<Arg<TermShape>> args) implements Callable, CodeShape.Moment {}
 
-  record CtorCall(@NotNull CodeShape.MomentId dataId, @NotNull CodeShape.MomentId ctorId,
-                  @Override @NotNull ImmutableSeq<TermShape> args) implements Callable {}
+  record CtorCall(@NotNull CodeShape.MomentId dataId, @NotNull CodeShape.GlobalId ctorId,
+                  @Override @NotNull ImmutableSeq<Arg<TermShape>> args) implements Callable {}
 }
diff --git a/base/src/main/java/org/aya/core/serde/SerDef.java b/base/src/main/java/org/aya/core/serde/SerDef.java
@@ -142,7 +142,7 @@ record SerBind(@NotNull ImmutableSeq<QName> loosers, @NotNull ImmutableSeq<QName
   /** serialized {@link ShapeRecognition} */
   record SerShapeResult(
     @NotNull SerAyaShape shape,
-    @NotNull ImmutableMap<CodeShape.MomentId, QName> captures
+    @NotNull ImmutableMap<CodeShape.GlobalId, QName> captures
   ) implements Serializable {
     public @NotNull ShapeRecognition de(@NotNull SerTerm.DeState state) {
       return new ShapeRecognition(shape.de(), ImmutableMap.from(captures.view()

diff --git a/base/src/main/java/org/aya/generic/Shaped.java b/base/src/main/java/org/aya/generic/Shaped.java
@@ -37,7 +37,7 @@ sealed interface Inductive<T> extends Shaped<T> {
     @NotNull ShapeRecognition recognition();
     @NotNull T constructorForm();
 
-    @SuppressWarnings("unchecked") default @NotNull DefVar<CtorDef, ?> ctorRef(@NotNull CodeShape.MomentId id) {
+    @SuppressWarnings("unchecked") default @NotNull DefVar<CtorDef, ?> ctorRef(@NotNull CodeShape.GlobalId id) {
       return (DefVar<CtorDef, ?>) recognition().captures().get(id);
     }
 

diff --git a/base/src/test/java/org/aya/repr/ShapeMatcherTest.java b/base/src/test/java/org/aya/repr/ShapeMatcherTest.java
@@ -91,17 +91,6 @@ public void capture() {
     return def.core.toDoc(AyaPrettierOptions.pretty()).debugRender();
   }
 
-  @Test
-  public void matchWeirdList() {
-    match(true, AyaShape.LIST_SHAPE, "data List {A : Type} | nil | cons A (List {A})");
-    match(true, AyaShape.LIST_SHAPE, "data List (A : Type) | nil | cons {A} (List A)");
-    match(true, AyaShape.LIST_SHAPE, "data List (A : Type) | nil | cons A {List A}");
-    match(true, AyaShape.LIST_SHAPE, "data List {A : Type} | nil | cons {A} (List {A})");
-    match(true, AyaShape.LIST_SHAPE, "data List {A : Type} | nil | cons A {List {A}}");
-    match(true, AyaShape.LIST_SHAPE, "data List (A : Type) | nil | cons {A} {List A}");
-    match(true, AyaShape.LIST_SHAPE, "data List {A : Type} | nil | cons {A} {List {A}}");
-  }
-
   @Test
   public void matchPlus() {
     match(ImmutableSeq.of(