merge: Renamer (#1096)

.github/README.md

@@ -1,28 +1,27 @@
 [![actions]](https://github.com/aya-prover/aya-dev/actions/workflows/gradle-check.yaml)
 [![maven]][maven-repo]
-[![gitter]](https://gitter.im/aya-prover/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge)
 [![codecov]](https://codecov.io/gh/aya-prover/aya-dev)
 
 [**Website**](https://www.aya-prover.org) contains:
 
 + Development blogs which are written for general audience
 + [Installation](https://www.aya-prover.org/guide/install.html)
   instructions (basically telling you what to download in [GitHub Releases])
-+ [Tutorial for Haskellers](https://www.aya-prover.org/guide/haskeller-tutorial.html)
-+ [Tutorial of extension types](https://www.aya-prover.org/guide/ext-types.html)
++ [Tutorial for functional programming features](https://www.aya-prover.org/guide/haskeller-tutorial.html)
++ [Tutorial for theorem proving features](https://www.aya-prover.org/guide/prover-tutorial.html)
 
 Aya is under active development, so please expect bugs, usability or performance issues
 (please file issues or create threads in discussions!).
 
 ## What to expect?
 
-+ Dependent types, including pi-types, sigma types, indexed families, etc.
++ Dependent types, including Π-types, Σ-types, indexed families, etc.
   You could write a [sized-vector type][gadt].
 + Set-level cubical type theory (XTT).
   + Demonstration of [quotient-inductive-inductive types][hiir],
     no forward declaration or mutual block needed!
     We infer the type checking order by how definitions use each other.
-  + Proof of `funExt` in [Paths.aya][funExt].
+  + Proof of `funExt` in [paths.aya][funExt].
 + Pattern matching with first-match semantics.
   Checkout the [red-black tree][rbtree] (without deletion yet).
 + A JIT-compiler that translates Aya code to higher-order abstract syntax in Java.
@@ -32,11 +31,10 @@ Aya is under active development, so please expect bugs, usability or performance
   You may preview the features (in Chinese)
   [here](https://blog.imkiva.org/posts/intro-literate-aya.html).
 + Binary operators, with precedence specified by a partial ordering
-  (instead of a number like in Haskell or Agda)
-  which is useful for [equation reasoning][assoc].
+  (instead of a number like in Haskell or Agda).
 + A fairly good termination checker.
-  We adapted some code from Agda's implementation to accept
-  [more definitions][foetus] (which are rejected by, e.g. Arend).
+  We adapted some code from Agda's implementation to accept more definitions such as the
+  `testSwapAdd` example in [this file][foetus] (which are rejected by, e.g. Arend).
 
 See also [use as a library](#use-as-a-library).
 
@@ -54,9 +52,9 @@ of IDE is IntelliJ IDEA, version 2023.3 or higher is required.
 + We welcome nitpicks on error reporting! Please let us know anything not perfect.
   We have already implemented several user-suggested error messages.
 + Before contributing in any form, please read
-  [the contribution guideline](https://github.com/aya-prover/aya-dev/blob/master/.github/CONTRIBUTING.md) thoroughly
+  [the contribution guideline](CONTRIBUTING.md) thoroughly
   and make sure you understand your responsibilities.
-+ Please follow [the Code of Conduct](https://github.com/aya-prover/aya-dev/blob/master/.github/CODE_OF_CONDUCT.md) to
++ Please follow [the Code of Conduct](CODE_OF_CONDUCT.md) to
   ensure an inclusive and welcoming community atmosphere.
 + Ask [@ice1000] or simply create a ticket in the discussion to become an organization member.
   + If you want to contribute, ask before doing anything.
@@ -66,17 +64,15 @@ of IDE is IntelliJ IDEA, version 2023.3 or higher is required.
 [@ice1000]: https://github.com/ice1000
 [actions]: https://github.com/aya-prover/aya-dev/actions/workflows/gradle-check.yaml/badge.svg
 [codecov]: https://img.shields.io/codecov/c/github/aya-prover/aya-dev?logo=codecov&logoColor=white
-[gitter]: https://img.shields.io/gitter/room/aya-prover/community?color=cyan&logo=gitter
 [maven]: https://img.shields.io/maven-central/v/org.aya-prover/base?logo=gradle
-[oop]: ../cli-impl/src/test/resources/shared/src/arith/Nat.aya
-[gadt]: ../cli-impl/src/test/resources/shared/src/data/Vec.aya
-[regularity]: ../cli-impl/src/test/resources/shared/src/Paths.aya
-[funExt]: ../cli-impl/src/test/resources/shared/src/Paths.aya
+[oop]: ../cli-impl/src/test/resources/shared/src/arith/nat/base.aya
+[gadt]: ../cli-impl/src/test/resources/shared/src/data/vec/base.aya
+[regularity]: ../cli-impl/src/test/resources/shared/src/paths.aya
+[funExt]: ../cli-impl/src/test/resources/shared/src/paths.aya
 [rbtree]: ../jit-compiler/src/test/resources/TreeSort.aya
 [tbtree-bench]: ../jit-compiler/src/test/java/RedBlackTreeTest.java
-[hiir]: ../cli-impl/src/test/resources/shared/src/type-theory/Thorsten.aya
-[assoc]: ../base/src/test/resources/success/src/Assoc.aya
-[foetus]: ../base/src/test/resources/success/src/FoetusLimitation.aya
+[hiir]: https://www.aya-prover.org/blog/tt-in-tt-qiit.html
+[foetus]: ../cli-impl/src/test/java/org/aya/test/fixtures/TerckError.java
 [maven-repo]: https://repo1.maven.org/maven2/org/aya-prover
 
 ## Use as a library
@@ -101,7 +97,8 @@ implementation group: 'org.aya-prover', name: '[project name]', version: '[lates
 + `[project name]` specifies the subproject of Aya you want to use,
   and the options are `pretty`, `base`, `cli-impl`, `parser`, etc.
   + The syntax definitions live in `syntax`.
-  + The parser lives in `parser` and `producer`.
+  + The parser lives in `parser` (the generated parsing code) and `producer`
+    (transformer from parse tree to concrete syntax tree).
   + The type checker lives in `base`.
   + The JIT compiler lives in `jit-compiler`.
   + The generalized pretty printing framework is in `pretty`.

base/src/main/java/org/aya/tyck/ExprTycker.java

@@ -68,7 +68,7 @@ public ExprTycker(
   }
 
   public ExprTycker(@NotNull TyckState state, @NotNull Reporter reporter) {
-    this(state, new LocalCtx(), new LocalLet(), reporter);
+    this(state, new MapLocalCtx(), new LocalLet(), reporter);
   }
 
   public void solveMetas() {
@@ -85,17 +85,13 @@ public void solveMetas() {
       case Expr.Lambda(var ref, var body) -> switch (whnf(type)) {
         case PiTerm(var dom, var cod) -> {
           // unifyTyReported(param, dom, expr);
-          var core = subscoped(() -> {
-            localCtx().put(ref, dom);
-            return inherit(body, cod.apply(new FreeTerm(ref))).wellTyped();
-          }).bind(ref);
+          var core = subscoped(ref, dom, () ->
+            inherit(body, cod.apply(new FreeTerm(ref))).wellTyped()).bind(ref);
           yield new Jdg.Default(new LamTerm(core), type);
         }
         case EqTerm eq -> {
-          var core = subscoped(() -> {
-            localCtx().put(ref, DimTyTerm.INSTANCE);
-            return inherit(body, eq.appA(new FreeTerm(ref))).wellTyped();
-          }).bind(ref);
+          var core = subscoped(ref, DimTyTerm.INSTANCE, () ->
+            inherit(body, eq.appA(new FreeTerm(ref))).wellTyped()).bind(ref);
           checkBoundaries(eq, core, body.sourcePos(), msg ->
             new CubicalError.BoundaryDisagree(expr, msg, new UnifyInfo(state)));
           yield new Jdg.Default(new LamTerm(core), eq);
@@ -142,11 +138,9 @@ case PiTerm(var dom, var cod) -> {
     if (type instanceof EqTerm eq) {
       resultType = whnf(resultType);
       if (resultType instanceof PiTerm(var dom, var cod) && dom == DimTyTerm.INSTANCE) {
-        var wellTyped = subscoped(() -> {
-          var ref = new FreeTerm(new LocalVar("i"));
-          localCtx().put(ref.name(), DimTyTerm.INSTANCE);
-          return unifyTyReported(eq.appA(ref), cod.apply(ref), expr);
-        });
+        var ref = new FreeTerm(new LocalVar("i"));
+        var wellTyped = subscoped(ref.name(), DimTyTerm.INSTANCE, () ->
+          unifyTyReported(eq.appA(ref), cod.apply(ref), expr));
         if (!wellTyped) return result;
         var closure = result.wellTyped() instanceof LamTerm(var clo) ? clo
           // This is kinda unsafe but it should be fine
@@ -173,11 +167,8 @@ case PiTerm(var dom, var cod) -> {
       case Expr.Pi(var param, var last) -> {
         var wellParam = ty(param.typeExpr());
         addWithTerm(param, param.sourcePos(), wellParam);
-        yield subscoped(() -> {
-          localCtx().put(param.ref(), wellParam);
-          var wellLast = ty(last).bind(param.ref());
-          return new PiTerm(wellParam, wellLast);
-        });
+        yield subscoped(param.ref(), wellParam, () ->
+          new PiTerm(wellParam, ty(last).bind(param.ref())));
       }
       case Expr.Sigma(var elems) -> subscoped(() -> {
         var tele = MutableList.<LocalVar>create();

base/src/main/java/org/aya/tyck/StmtTycker.java

@@ -22,7 +22,7 @@
 import org.aya.syntax.core.term.call.DataCall;
 import org.aya.syntax.core.term.xtt.DimTyTerm;
 import org.aya.syntax.core.term.xtt.EqTerm;
-import org.aya.syntax.ref.LocalCtx;
+import org.aya.syntax.ref.MapLocalCtx;
 import org.aya.syntax.telescope.Signature;
 import org.aya.tyck.ctx.LocalLet;
 import org.aya.tyck.error.*;
@@ -46,7 +46,8 @@ public record StmtTycker(
   @NotNull PrimFactory primFactory
 ) implements Problematic {
   private @NotNull ExprTycker mkTycker() {
-    return new ExprTycker(new TyckState(shapeFactory, primFactory), new LocalCtx(), new LocalLet(), reporter);
+    return new ExprTycker(new TyckState(shapeFactory, primFactory),
+      new MapLocalCtx(), new LocalLet(), reporter);
   }
   public @NotNull TyckDef check(Decl predecl) {
     ExprTycker tycker = null;
@@ -272,6 +273,6 @@ private void checkPrim(@NotNull ExprTycker tycker, PrimDecl prim) {
       msg -> new PrimError.BadSignature(prim, msg, new UnifyInfo(tycker.state)));
     primRef.signature = tele.descent(tycker::zonk);
     tycker.solveMetas();
-    tycker.setLocalCtx(new LocalCtx());
+    tycker.setLocalCtx(new MapLocalCtx());
   }
 }

base/src/main/java/org/aya/tyck/pat/ClauseTycker.java

@@ -6,7 +6,7 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.primitive.ImmutableIntSeq;
 import kala.value.primitive.MutableBooleanValue;
-import org.aya.generic.NameGenerator;
+import org.aya.generic.Renamer;
 import org.aya.prettier.AyaPrettierOptions;
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
@@ -138,7 +138,7 @@ public record Worker(
       : telescope;
 
     return new PatternTycker(exprTycker, telescope, new LocalLet(), indices == null,
-      new NameGenerator());
+      new Renamer());
   }
 
   public @NotNull LhsResult checkLhs(

base/src/main/java/org/aya/tyck/pat/IApplyConfl.java

@@ -9,7 +9,7 @@
 import org.aya.syntax.core.pat.PatToTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.call.FnCall;
-import org.aya.syntax.ref.LocalCtx;
+import org.aya.syntax.ref.MapLocalCtx;
 import org.aya.tyck.ExprTycker;
 import org.aya.tyck.error.ClausesProblem;
 import org.aya.tyck.error.UnifyInfo;
@@ -53,7 +53,7 @@ public void check() {
 
   private void apply(int i, PatMatcher chillMatcher) {
     var matching = matchings.get(i);
-    var ctx = new LocalCtx();
+    var ctx = new MapLocalCtx();
     var cases = new PatToTerm.Monadic(ctx).list(matching.patterns().view());
     if (cases.sizeEquals(1)) return;
     if (cases.isEmpty()) Panic.unreachable();

base/src/main/java/org/aya/tyck/pat/PatternTycker.java

@@ -8,7 +8,7 @@
 import kala.control.Result;
 import kala.value.MutableValue;
 import org.aya.generic.Constants;
-import org.aya.generic.NameGenerator;
+import org.aya.generic.Renamer;
 import org.aya.generic.State;
 import org.aya.normalize.Normalizer;
 import org.aya.normalize.PatMatcher;
@@ -69,7 +69,7 @@ public class PatternTycker implements Problematic, Stateful {
 
   private @UnknownNullability Param currentParam = null;
   private boolean hasError = false;
-  private final @NotNull NameGenerator nameGen;
+  private final @NotNull Renamer nameGen;
 
   /**
    * @see #tyckInner(SeqView, SeqView, WithPos)
@@ -78,7 +78,7 @@ private PatternTycker(
     @NotNull ExprTycker tycker,
     @NotNull SeqView<Param> tele,
     @NotNull LocalLet sub,
-    @NotNull NameGenerator nameGen
+    @NotNull Renamer nameGen
   ) {
     this(tycker, tele, sub, true, nameGen);
   }
@@ -88,14 +88,15 @@ public PatternTycker(
     @NotNull SeqView<Param> telescope,
     @NotNull LocalLet asSubst,
     boolean allowImplicit,
-    @NotNull NameGenerator nameGen
+    @NotNull Renamer nameGen
   ) {
     this.exprTycker = exprTycker;
     this.telescope = telescope;
     this.paramSubst = MutableList.create();
     this.asSubst = asSubst;
     this.allowImplicit = allowImplicit;
     this.nameGen = nameGen;
+    nameGen.store(exprTycker.localCtx());
   }
 
   public record TyckResult(
@@ -373,13 +374,12 @@ private <T> T onTyck(@NotNull Supplier<T> block) {
     return onTyck(() -> {
       var type = currentParam.type();
       Pat pat;
-      var freshName = currentParam.name();
+      var freshVar = nameGen.bindName(currentParam.name());
       if (exprTycker.whnf(type) instanceof DataCall dataCall) {
         // this pattern would be a Con, it can be inferred
         // TODO: I NEED A SOURCE POS!!
-        pat = new Pat.Meta(MutableValue.create(), freshName, dataCall, SourcePos.NONE);
+        pat = new Pat.Meta(MutableValue.create(), freshVar.name(), dataCall, SourcePos.NONE);
       } else {
-        var freshVar = LocalVar.generate(freshName);
         // If the type is not a DataCall, then the only available pattern is Pat.Bind
         pat = new Pat.Bind(freshVar, type);
         exprTycker.localCtx().put(freshVar, type);
@@ -412,14 +412,7 @@ private void addAsSubst(@NotNull LocalVar as, @NotNull Pat pattern, @NotNull Ter
 
   private @NotNull TyckResult done(@NotNull MutableList<Pat> wellTyped, @Nullable WithPos<Expr> newBody) {
     var paramSubst = this.paramSubst.toImmutableSeq();
-
-    return new TyckResult(
-      wellTyped.toImmutableSeq(),
-      paramSubst,
-      asSubst,
-      newBody,
-      hasError
-    );
+    return new TyckResult(wellTyped.toImmutableSeq(), paramSubst, asSubst, newBody, hasError);
   }
 
   private record Selection(
@@ -497,15 +490,15 @@ private record Selection(
 
   /// region Helper
   private @NotNull Pat randomPat(Term param) {
-    return new Pat.Bind(LocalVar.generate("?"), param);
+    return new Pat.Bind(nameGen.bindName(param), param);
   }
 
   /**
    * Generate names for core telescope
    */
   private @NotNull SeqView<Param> generateNames(@NotNull ImmutableSeq<Term> telescope) {
     return telescope.view().mapIndexed((_, t) ->
-      new Param(nameGen.next(exprTycker.whnf(t)), t, true));
+      new Param(nameGen.bindName(exprTycker.whnf(t)).name(), t, true));
   }
 
   /// endregion Helper

base/src/main/java/org/aya/tyck/tycker/AbstractTycker.java

@@ -4,11 +4,12 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.value.LazyValue;
-import org.aya.generic.NameGenerator;
+import org.aya.generic.Renamer;
 import org.aya.normalize.Finalizer;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.LocalCtx;
+import org.aya.syntax.ref.LocalCtx1;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.tyck.ExprTycker;
 import org.aya.tyck.Jdg;
@@ -19,6 +20,8 @@
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
 
+import java.util.function.Function;
+
 public sealed abstract class AbstractTycker implements Stateful, Contextful, Problematic permits ExprTycker, TermComparator {
   public final @NotNull TyckState state;
   private @NotNull LocalCtx localCtx;
@@ -44,11 +47,13 @@ protected AbstractTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNu
     return new Jdg.Lazy(wellTyped, LazyValue.of(() ->
       new Synthesizer(this).synthDontNormalize(wellTyped)));
   }
-
-  public @NotNull LocalVar putIndex(@NotNull NameGenerator nameGen, @NotNull Term type) {
-    var var = nameGen.nextVar(whnf(type));
-    localCtx.put(var, type);
-    return var;
+  public <R> R subscoped(@NotNull Term type, @NotNull Function<LocalVar, R> action, @NotNull Renamer nameGen) {
+    var var = nameGen.bindName(type);
+    var parentCtx = setLocalCtx(new LocalCtx1(type, var, localCtx()));
+    var result = action.apply(var);
+    setLocalCtx(parentCtx);
+    nameGen.unbindName(var);
+    return result;
   }
 
   public @NotNull Term zonk(Term t) {
@@ -57,5 +62,4 @@ protected AbstractTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNu
   public ImmutableSeq<WithPos<Param>> zonk(ImmutableSeq<WithPos<Param>> tele) {
     return tele.map(wp -> wp.map(p -> p.descent(this::zonk)));
   }
-  public @NotNull Jdg zonk(@NotNull Jdg result) { return result.map(this::zonk); }
 }

base/src/main/java/org/aya/tyck/tycker/Contextful.java

@@ -11,6 +11,7 @@
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.call.MetaCall;
 import org.aya.syntax.ref.LocalCtx;
+import org.aya.syntax.ref.LocalCtx1;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.syntax.ref.MetaVar;
 import org.aya.util.error.SourcePos;
@@ -51,11 +52,11 @@ default <R> R subscoped(@NotNull Supplier<R> action) {
   }
 
   @Contract(mutates = "this")
-  default <R> R with(@NotNull LocalVar var, @NotNull Term type, @NotNull Supplier<R> action) {
-    return subscoped(() -> {
-      localCtx().put(var, type);
-      return action.get();
-    });
+  default <R> R subscoped(@NotNull LocalVar var, @NotNull Term type, @NotNull Supplier<R> action) {
+    var parentCtx = setLocalCtx(new LocalCtx1(type, var, localCtx()));
+    var result = action.get();
+    setLocalCtx(parentCtx);
+    return result;
   }
 
   /**