fn-shape: don't use NAT

aya-prover · Oct 21, 2023 · 6e92f62 · 6e92f62
1 parent d548fed
commit 6e92f62
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/base/src/main/java/org/aya/tyck/repr/ShapeFactory.java b/base/src/main/java/org/aya/tyck/repr/ShapeFactory.java
@@ -51,17 +51,17 @@ public final class ShapeFactory {
     @NotNull ShapeRecognition recog,
     @NotNull AyaShape.Factory factory
   ) {
+    var core = ref.core;
+    if (core == null) return null;
+
     if (recog.shape() == AyaShape.PLUS_LEFT_SHAPE || recog.shape() == AyaShape.PLUS_RIGHT_SHAPE) {
-      var dataRef = (DefVar<DataDef, TeleDecl.DataDecl>) recog.captures().get(CodeShape.GlobalId.NAT);
-      var dataDef = dataRef.core;
+      if (!(core.result instanceof DataCall paramType)) return null;
+      var dataDef = paramType.ref().core;
       assert dataDef != null : "How?";
 
       var paramRecog = factory.find(dataDef).getOrNull();
       if (paramRecog == null) throw new InternalException("How?");
 
-      // TODO[h]: Can I use ref.core.result directly?
-      var paramType = new DataCall(dataRef, 0, ImmutableSeq.empty());
-
       return new IntegerOpsTerm.FnRule(ref, paramRecog, paramType, IntegerOpsTerm.FnRule.Kind.Add);
     }