merge: Tycking enhancements, more testing (#1068)

plctlab · May 30, 2024 · 49d5e4a · 49d5e4a
2 parents a6484cc + 9f8c8f6
commit 49d5e4a
Show file tree

Hide file tree

Showing 9 changed files with 112 additions and 92 deletions.
diff --git a/.github/workflows/nightly-build.yaml b/.github/workflows/nightly-build.yaml
@@ -89,14 +89,18 @@ jobs:
           cp ./ide-lsp/build/libs/*-fat.jar ./lsp-fatjar.jar
           cp ./cli-console/build/libs/*-fat.jar ./cli-fatjar.jar
 
+      - name: Get current date
+        id: date
+        run: echo "MY_DATE=$(date +%Y/%m/%d-%H:%M)" >> $GITHUB_ENV
+
       - name: Update Release (jlink zips and jars)
         uses: Xotl/cool-github-releases@v1
         if: matrix.os == 'ubuntu-latest'
         with:
           mode: update
           isPrerelease: false
           tag_name: nightly-build
-          release_name: "Nightly builds"
+          release_name: "${{ env.MY_DATE }} nightly build"
           body_mrkdwn: |
             _These are latest builds, but the date on GitHub is frozen due to stupid limitations.
             Corresponding commit: <https://github.com/aya-prover/aya-dev/commit/${{ github.sha }}>_

diff --git a/base/src/main/java/org/aya/resolve/context/ModuleContext.java b/base/src/main/java/org/aya/resolve/context/ModuleContext.java
@@ -199,7 +199,7 @@ default void importSymbol(
     } else {
       var uniqueCandidates = candidates.uniqueCandidates();
       if (uniqueCandidates.size() != 1 || uniqueCandidates.iterator().next() != ref) {
-        reporter().report(new NameProblem.AmbiguousNameWarn(name, sourcePos));
+        fail(new NameProblem.AmbiguousNameWarn(name, sourcePos));
 
         if (candidates.map().containsKey(ModuleName.This)) {
           // H : modName instance ModulePath.Qualified
@@ -222,8 +222,8 @@ default void importSymbol(
     var result = symbols.add(modName, name, ref);
     assert result.isEmpty() : "Sanity check"; // should already be reported as an error
 
-    // Only `DefVar`s can be exported.
-    if (ref instanceof DefVar<?, ?> defVar && acc == Stmt.Accessibility.Public) {
+    // Only `AnyDefVar`s can be exported.
+    if (ref instanceof AnyDefVar defVar && acc == Stmt.Accessibility.Public) {
       var success = exportSymbol(modName, name, defVar);
       if (!success) {
         reportAndThrow(new NameProblem.DuplicateExportError(name, sourcePos));

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -198,8 +198,18 @@ yield subscoped(() -> {
       case Expr.Sugar s ->
         throw new IllegalArgumentException(STR."\{s.getClass()} is desugared, should be unreachable");
       case Expr.App(var f, var a) -> {
-        if (!(f.data() instanceof Expr.Ref ref)) throw new IllegalStateException("function must be Expr.Ref");
-        yield checkApplication(ref, expr.sourcePos(), a);
+        int lift;
+        if (f.data() instanceof Expr.Lift(var inner, var level)) {
+          lift = level;
+          f = inner;
+        } else lift = 0;
+        if (f.data() instanceof Expr.Ref ref) {
+          yield checkApplication(ref, lift, expr.sourcePos(), a);
+        } else try {
+          yield generateApplication(a, synthesize(f)).lift(lift);
+        } catch (NotPi e) {
+          yield fail(expr.data(), BadTypeError.pi(state, expr, e.actual));
+        }
       }
       case Expr.Hole hole -> throw new UnsupportedOperationException("TODO");
       case Expr.Lambda lam -> inherit(expr, generatePi(lam, expr.sourcePos()));
@@ -215,12 +225,13 @@ yield subscoped(() -> {
         var type = new DataCall((DataDefLike) match.def(), 0, ImmutableSeq.empty());
         yield new Jdg.Default(new IntegerTerm(integer, match.recog(), type), type);
       }
+      case Expr.Lift(var inner, var level) -> synthesize(inner).map(x -> x.elevate(level));
       case Expr.LitString litStr -> {
         if (!state.primFactory().have(PrimDef.ID.STRING))
           yield fail(litStr, new NoRuleError(expr, null));
         yield new Jdg.Default(new StringTerm(litStr.string()), state.primFactory().getCall(PrimDef.ID.STRING));
       }
-      case Expr.Ref ref -> checkApplication(ref, expr.sourcePos(), ImmutableSeq.empty());
+      case Expr.Ref ref -> checkApplication(ref, 0, expr.sourcePos(), ImmutableSeq.empty());
       case Expr.Sigma _, Expr.Pi _ -> lazyJdg(ty(expr));
       case Expr.Sort _ -> sort(expr);
       case Expr.Tuple(var items) -> {
@@ -265,11 +276,11 @@ yield subscoped(() -> {
   }
 
   private @NotNull Jdg checkApplication(
-    @NotNull Expr.Ref f, @NotNull SourcePos sourcePos,
+    @NotNull Expr.Ref f, int lift, @NotNull SourcePos sourcePos,
     @NotNull ImmutableSeq<Expr.NamedArg> args
   ) {
     try {
-      var result = doCheckApplication(f.var(), args);
+      var result = doCheckApplication(f.var(), lift, args);
       addWithTerm(f, sourcePos, result.type());
       return result;
     } catch (NotPi notPi) {
@@ -279,17 +290,16 @@ yield subscoped(() -> {
   }
 
   private @NotNull Jdg doCheckApplication(
-    @NotNull AnyVar f, @NotNull ImmutableSeq<Expr.NamedArg> args
+    @NotNull AnyVar f, int lift, @NotNull ImmutableSeq<Expr.NamedArg> args
   ) throws NotPi {
     return switch (f) {
-      case LocalVar ref when localLet.contains(ref) ->
-        generateApplication(args, localLet.get(ref));
+      case LocalVar ref when localLet.contains(ref) -> generateApplication(args, localLet.get(ref)).lift(lift);
       case LocalVar lVar -> generateApplication(args,
-        new Jdg.Default(new FreeTerm(lVar), localCtx().get(lVar)));
+        new Jdg.Default(new FreeTerm(lVar), localCtx().get(lVar))).lift(lift);
       case CompiledVar(var content) -> AppTycker.checkCompiledApplication(content,
-        (params, k) -> computeArgs(args, params, k));
-      case DefVar<?, ?> defVar -> AppTycker.checkDefApplication(defVar, state,
-        (params, k) -> computeArgs(args, params, k));
+        new AppTycker.CheckAppData<>(state, lift, (params, k) -> computeArgs(args, params, k)));
+      case DefVar<?, ?> defVar -> AppTycker.checkDefApplication(defVar,
+        new AppTycker.CheckAppData<>(state, lift, (params, k) -> computeArgs(args, params, k)));
       default -> throw new UnsupportedOperationException("TODO");
     };
   }

diff --git a/base/src/main/java/org/aya/tyck/Jdg.java b/base/src/main/java/org/aya/tyck/Jdg.java
@@ -17,6 +17,7 @@ public sealed interface Jdg {
 
   default @NotNull Jdg bindTele(@NotNull SeqView<LocalVar> vars) { return map(t -> t.bindTele(vars)); }
   @NotNull Jdg map(@NotNull UnaryOperator<Term> f);
+  default Jdg lift(int lift) { return map(t -> t.elevate(lift)); }
 
   /**
    * {@link Default#type} is the type of {@link Default#wellTyped}.

diff --git a/base/src/main/java/org/aya/tyck/tycker/AppTycker.java b/base/src/main/java/org/aya/tyck/tycker/AppTycker.java
@@ -4,9 +4,8 @@
 
 import kala.collection.immutable.ImmutableArray;
 import kala.function.CheckedBiFunction;
-import org.aya.syntax.compile.JitData;
-import org.aya.syntax.compile.JitFn;
-import org.aya.syntax.compile.JitTele;
+import org.aya.generic.stmt.Shaped;
+import org.aya.syntax.compile.*;
 import org.aya.syntax.concrete.stmt.decl.DataCon;
 import org.aya.syntax.concrete.stmt.decl.DataDecl;
 import org.aya.syntax.concrete.stmt.decl.FnDecl;
@@ -28,89 +27,95 @@ public interface AppTycker {
   interface Factory<Ex extends Exception> extends
     CheckedBiFunction<JitTele, Function<Term[], Jdg>, Jdg, Ex> {
   }
+  record CheckAppData<Ex extends Exception>(
+    @NotNull TyckState state, int lift, @NotNull Factory<Ex> makeArgs
+  ) { }
 
-  static <Ex extends Exception> @NotNull Jdg checkCompiledApplication(
-    JitTele def, @NotNull Factory<Ex> makeArgs
-  ) throws Ex {
+  static <Ex extends Exception> @NotNull Jdg
+  checkCompiledApplication(@NotNull JitTele def, CheckAppData<Ex> input) throws Ex {
     return switch (def) {
-      case JitFn fn -> makeArgs.applyChecked(fn, args -> {
+      case JitFn fn -> {
         int shape = fn.metadata().shape();
-        if (shape != -1) {
-          var operator = AyaShape.ofFn(fn, AyaShape.values()[shape]);
-          if (operator != null) return new Jdg.Default(
-            new RuleReducer.Fn(operator, 0, ImmutableArray.from(args)), fn.result(args));
-        }
-        return new Jdg.Default(new FnCall(fn, 0, ImmutableArray.from(args)), fn.result(args));
-      });
-      case JitData data -> makeArgs.applyChecked(data, args ->
-        new Jdg.Default(new DataCall(data, 0, ImmutableArray.from(args)), data.result(args)));
-      default -> Panic.unreachable();
+        var operator = shape != -1 ? AyaShape.ofFn(fn, AyaShape.values()[shape]) : null;
+        yield checkFnCall(input.makeArgs, input.lift, fn, operator);
+      }
+      case JitData data -> checkDataCall(input.makeArgs, input.lift, data);
+      case JitPrim prim -> checkPrimCall(input.state, input.makeArgs, input.lift, prim);
+      case JitCon con -> checkConCall(input.state, input.makeArgs, input.lift, con);
+      default -> throw new Panic(def.getClass().getCanonicalName());
     };
   }
 
   @SuppressWarnings("unchecked")
   static <Ex extends Exception> @NotNull Jdg checkDefApplication(
-    @NotNull DefVar<?, ?> defVar,
-    @NotNull TyckState state, @NotNull Factory<Ex> makeArgs
+    @NotNull DefVar<?, ?> defVar, @NotNull CheckAppData<Ex> input
   ) throws Ex {
     return switch (defVar.concrete) {
       case FnDecl _ -> {
-        var fnVar = (DefVar<FnDef, FnDecl>) defVar;
-        var signature = TyckDef.defSignature(fnVar);
-        yield makeArgs.applyChecked(signature, args -> {
-          var shape = state.shapeFactory().find(new FnDef.Delegate(fnVar));
-          var argsSeq = ImmutableArray.from(args);
-          var result = signature.result(args);
-          if (shape.isDefined()) {
-            var operator = AyaShape.ofFn(new FnDef.Delegate(fnVar), shape.get().shape());
-            if (operator != null) {
-              return new Jdg.Default(new RuleReducer.Fn(operator, 0, argsSeq), result);
-            }
-          }
-          return new Jdg.Default(new FnCall(fnVar, 0, argsSeq), result);
-        });
-      }
-      case DataDecl _ -> {
-        var dataVar = (DefVar<DataDef, DataDecl>) defVar;
-        var signature = TyckDef.defSignature(dataVar);
-        yield makeArgs.applyChecked(signature, args -> new Jdg.Default(
-          new DataCall(dataVar, 0, ImmutableArray.from(args)),
-          signature.result(args)
-        ));
+        var fnDef = new FnDef.Delegate((DefVar<FnDef, FnDecl>) defVar);
+        var op = input.state.shapeFactory().find(fnDef).map(recog -> AyaShape.ofFn(fnDef, recog.shape())).getOrNull();
+        yield checkFnCall(input.makeArgs, input.lift, fnDef, op);
       }
-      case PrimDecl _ -> {
-        var primVar = (DefVar<PrimDef, PrimDecl>) defVar;
-        var signature = TyckDef.defSignature(primVar);
-        yield makeArgs.applyChecked(signature, args -> new Jdg.Default(
-          state.primFactory().unfold(new PrimCall(primVar, 0, ImmutableArray.from(args)), state),
-          signature.result(args)
-        ));
-      }
-      case DataCon _ -> {
-        var conVar = (DefVar<ConDef, DataCon>) defVar;
-        var conCore = conVar.core;
-        assert conCore != null;
-        var dataVar = conCore.dataRef;
+      // Extracted to prevent pervasive influence of suppression of unchecked warning.
+      case DataDecl _ -> checkDataCall(input.makeArgs, input.lift,
+        new DataDef.Delegate((DefVar<DataDef, DataDecl>) defVar));
+      case PrimDecl _ -> checkPrimCall(input.state, input.makeArgs, input.lift,
+        new PrimDef.Delegate((DefVar<PrimDef, PrimDecl>) defVar));
+      case DataCon _ -> checkConCall(input.state, input.makeArgs, input.lift,
+        new ConDef.Delegate((DefVar<ConDef, DataCon>) defVar));
+      default -> Panic.unreachable();
+    };
+  }
 
-        // ownerTele + selfTele
-        var fullSignature = TyckDef.defSignature(conVar);
-        var ownerTele = conCore.ownerTele;
+  private static <Ex extends Exception> Jdg
+  checkConCall(@NotNull TyckState state, @NotNull Factory<Ex> makeArgs, int lift, ConDefLike conVar) throws Ex {
+    var dataVar = conVar.dataRef();
 
-        yield makeArgs.applyChecked(fullSignature, args -> {
-          var realArgs = ImmutableArray.from(args);
-          var ownerArgs = realArgs.take(ownerTele.size());
-          var conArgs = realArgs.drop(ownerTele.size());
+    // ownerTele + selfTele
+    var fullSignature = conVar.signature();
 
-          var type = (DataCall) fullSignature.result(realArgs);
-          var shape = state.shapeFactory().find(new DataDef.Delegate(dataVar))
-            .mapNotNull(recog -> AyaShape.ofCon(new ConDef.Delegate(conVar), recog, type))
-            .getOrNull();
-          if (shape != null) return new Jdg.Default(new RuleReducer.Con(shape, 0, ownerArgs, conArgs), type);
-          var wellTyped = new ConCall(conVar, 0, ownerArgs, conArgs);
-          return new Jdg.Default(wellTyped, type);
-        });
+    return makeArgs.applyChecked(fullSignature, args -> {
+      var realArgs = ImmutableArray.from(args);
+      var ownerArgs = realArgs.take(conVar.ownerTeleSize());
+      var conArgs = realArgs.drop(conVar.ownerTeleSize());
+
+      var type = (DataCall) fullSignature.result(realArgs);
+      var shape = state.shapeFactory().find(dataVar)
+        .mapNotNull(recog -> AyaShape.ofCon(conVar, recog, type))
+        .getOrNull();
+      if (shape != null) return new Jdg.Default(new RuleReducer.Con(shape, lift, ownerArgs, conArgs), type);
+      var wellTyped = new ConCall(conVar, ownerArgs, lift, conArgs);
+      return new Jdg.Default(wellTyped, type);
+    });
+  }
+  private static <Ex extends Exception> Jdg
+  checkPrimCall(@NotNull TyckState state, @NotNull Factory<Ex> makeArgs, int lift, PrimDefLike primVar) throws Ex {
+    var signature = primVar.signature();
+    return makeArgs.applyChecked(signature, args -> new Jdg.Default(
+      state.primFactory().unfold(new PrimCall(primVar, lift, ImmutableArray.from(args)), state),
+      signature.result(args)
+    ));
+  }
+  private static <Ex extends Exception> Jdg
+  checkDataCall(@NotNull Factory<Ex> makeArgs, int lift, DataDefLike data) throws Ex {
+    var signature = data.signature();
+    return makeArgs.applyChecked(signature, args -> new Jdg.Default(
+      new DataCall(data, lift, ImmutableArray.from(args)),
+      signature.result(args)
+    ));
+  }
+  private static <Ex extends Exception> @NotNull Jdg checkFnCall(
+    @NotNull Factory<Ex> makeArgs, int lift, FnDefLike fnDef,
+    Shaped.Applicable<FnDefLike> operator
+  ) throws Ex {
+    var signature = fnDef.signature();
+    return makeArgs.applyChecked(signature, args -> {
+      var argsSeq = ImmutableArray.from(args);
+      var result = signature.result(args);
+      if (operator != null) {
+        return new Jdg.Default(new RuleReducer.Fn(operator, lift, argsSeq), result);
       }
-      default -> Panic.unreachable();
-    };
+      return new Jdg.Default(new FnCall(fnDef, lift, argsSeq), result);
+    });
   }
 }
diff --git a/base/src/main/java/org/aya/unify/Synthesizer.java b/base/src/main/java/org/aya/unify/Synthesizer.java
@@ -5,8 +5,6 @@
 import kala.collection.mutable.MutableList;
 import org.aya.generic.NameGenerator;
 import org.aya.generic.term.SortKind;
-import org.aya.prettier.AyaPrettierOptions;
-import org.aya.syntax.core.def.AnyDef;
 import org.aya.syntax.core.def.PrimDef;
 import org.aya.syntax.core.term.*;
 import org.aya.syntax.core.term.call.Callable;
@@ -60,13 +58,13 @@ public boolean inheritPiDom(@NotNull Term ty, @NotNull SortTerm expected) {
 
   public @NotNull Term synth(@NotNull Term term) {
     var result = trySynth(term);
-    assert result != null : term.toDoc(AyaPrettierOptions.debug()).debugRender();
+    assert result != null : term.debuggerOnlyToString() + " : " + term.getClass();
     return result;
   }
 
   public @NotNull Term synthDontNormalize(@NotNull Term term) {
     var result = synthesize(term);
-    assert result != null : term.toDoc(AyaPrettierOptions.debug()).debugRender();
+    assert result != null : term.debuggerOnlyToString() + " : " + term.getClass();
     return result;
   }
 

diff --git a/cli-impl/src/test/java/org/aya/test/LibraryTest.java b/cli-impl/src/test/java/org/aya/test/LibraryTest.java
@@ -52,6 +52,7 @@ public void testOnDisk(@NotNull String libName) throws IOException {
   }
 
   @Test public void fastTestOnDisk() throws IOException {
+    FileUtil.deleteRecursively(DIR.resolve("build"));
     assertEquals(0, compile(DIR));
   }
 

diff --git a/cli-impl/src/test/resources/success/src/Test.aya b/cli-impl/src/test/resources/success/src/Test.aya
@@ -5,4 +5,4 @@ def something (a : Nat)
  : a + 1 + a = 1 + a + a => refl
 
 def issue1061 : Nat -> Nat
-| n => n
+| n => Nat::suc n
diff --git a/parser/src/main/java/org/aya/parser/AyaParserDefinitionBase.java b/parser/src/main/java/org/aya/parser/AyaParserDefinitionBase.java
@@ -48,6 +48,7 @@ public AyaParserDefinitionBase(@NotNull IFileElementType file) {
   /** text keywords */
   public static final @NotNull TokenSet KEYWORDS = TokenSet.create(
     AyaPsiElementTypes.KW_AS,
+    AyaPsiElementTypes.KW_ELIM,
     AyaPsiElementTypes.KW_CODATA,
     AyaPsiElementTypes.KW_COERCE,
     AyaPsiElementTypes.KW_COMPLETED,