diff --git a/.github/README.md b/.github/README.md index 53270ee38a..bb83d0f825 100644 --- a/.github/README.md +++ b/.github/README.md @@ -1,6 +1,5 @@ [![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: @@ -8,21 +7,21 @@ + 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`. diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java index b92b3e06b1..bc0f6e8936 100644 --- a/base/src/main/java/org/aya/tyck/ExprTycker.java +++ b/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.create(); diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index f516e5883e..de793ed534 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/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()); } } diff --git a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java index 50a209f3a5..494952f523 100644 --- a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java +++ b/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( diff --git a/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java b/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java index 0afc1c4a1e..e7e06f6388 100644 --- a/base/src/main/java/org/aya/tyck/pat/IApplyConfl.java +++ b/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(); diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java index d1c37ff1e6..74a3a8d82c 100644 --- a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java +++ b/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 tele, @NotNull LocalLet sub, - @NotNull NameGenerator nameGen + @NotNull Renamer nameGen ) { this(tycker, tele, sub, true, nameGen); } @@ -88,7 +88,7 @@ public PatternTycker( @NotNull SeqView telescope, @NotNull LocalLet asSubst, boolean allowImplicit, - @NotNull NameGenerator nameGen + @NotNull Renamer nameGen ) { this.exprTycker = exprTycker; this.telescope = telescope; @@ -96,6 +96,7 @@ public PatternTycker( this.asSubst = asSubst; this.allowImplicit = allowImplicit; this.nameGen = nameGen; + nameGen.store(exprTycker.localCtx()); } public record TyckResult( @@ -373,13 +374,12 @@ private T onTyck(@NotNull Supplier 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 wellTyped, @Nullable WithPos 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,7 +490,7 @@ 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); } /** @@ -505,7 +498,7 @@ private record Selection( */ private @NotNull SeqView generateNames(@NotNull ImmutableSeq 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 diff --git a/base/src/main/java/org/aya/tyck/tycker/AbstractTycker.java b/base/src/main/java/org/aya/tyck/tycker/AbstractTycker.java index 24e024f340..116ffa6cd4 100644 --- a/base/src/main/java/org/aya/tyck/tycker/AbstractTycker.java +++ b/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 subscoped(@NotNull Term type, @NotNull Function 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> zonk(ImmutableSeq> tele) { return tele.map(wp -> wp.map(p -> p.descent(this::zonk))); } - public @NotNull Jdg zonk(@NotNull Jdg result) { return result.map(this::zonk); } } diff --git a/base/src/main/java/org/aya/tyck/tycker/Contextful.java b/base/src/main/java/org/aya/tyck/tycker/Contextful.java index dfc7347360..4a0e7f3bed 100644 --- a/base/src/main/java/org/aya/tyck/tycker/Contextful.java +++ b/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 subscoped(@NotNull Supplier action) { } @Contract(mutates = "this") - default R with(@NotNull LocalVar var, @NotNull Term type, @NotNull Supplier action) { - return subscoped(() -> { - localCtx().put(var, type); - return action.get(); - }); + default R subscoped(@NotNull LocalVar var, @NotNull Term type, @NotNull Supplier action) { + var parentCtx = setLocalCtx(new LocalCtx1(type, var, localCtx())); + var result = action.get(); + setLocalCtx(parentCtx); + return result; } /** diff --git a/base/src/main/java/org/aya/unify/DoubleChecker.java b/base/src/main/java/org/aya/unify/DoubleChecker.java index 5b28eeac4d..92d0dad9e4 100644 --- a/base/src/main/java/org/aya/unify/DoubleChecker.java +++ b/base/src/main/java/org/aya/unify/DoubleChecker.java @@ -17,6 +17,8 @@ import org.aya.util.reporter.Reporter; import org.jetbrains.annotations.NotNull; +import java.util.function.Function; + /** * @apiNote {@link Unifier#localCtx()} should be the same object as {@link Synthesizer#localCtx()} */ @@ -24,21 +26,20 @@ public record DoubleChecker( @NotNull Unifier unifier, @NotNull Synthesizer synthesizer ) implements Stateful, Contextful, Problematic { - public DoubleChecker(@NotNull Unifier unifier) { this(unifier, new Synthesizer(unifier)); } + public DoubleChecker(@NotNull Unifier unifier) { this(unifier, new Synthesizer(unifier.nameGen, unifier)); } public boolean inherit(@NotNull Term preterm, @NotNull Term expected) { return switch (preterm) { case ErrorTerm _ -> true; case PiTerm(var pParam, var pBody) -> { if (!(whnf(expected) instanceof SortTerm expectedTy)) yield Panic.unreachable(); - yield synthesizer.inheritPiDom(pParam, expectedTy) && subscoped(() -> { - var param = putIndex(pParam); - return inherit(pBody.apply(param), expectedTy); - }); + yield synthesizer.inheritPiDom(pParam, expectedTy) && subscoped(pParam, param -> + inherit(pBody.apply(param), expectedTy)); } case SigmaTerm sigma -> { if (!(whnf(expected) instanceof SortTerm expectedTy)) yield Panic.unreachable(); - yield subscoped(() -> sigma.view(i -> new FreeTerm(putIndex(i))) + yield subscoped(() -> sigma + .view(synthesizer::mkFree) .allMatch(param -> inherit(param, expectedTy))); } case TupTerm(var elems) when whnf(expected) instanceof SigmaTerm sigmaTy -> { @@ -50,18 +51,15 @@ case TupTerm(var elems) when whnf(expected) instanceof SigmaTerm sigmaTy -> { return null; }).isOk(); } - case LamTerm(var body) -> subscoped(() -> switch (whnf(expected)) { - case PiTerm(var dom, var cod) -> { - var param = putIndex(dom); - yield inherit(body.apply(param), cod.apply(param)); - } - case EqTerm eq -> { - var param = putIndex(DimTyTerm.INSTANCE); + case LamTerm(var body) -> switch (whnf(expected)) { + case PiTerm(var dom, var cod) -> subscoped(dom, param -> + inherit(body.apply(param), cod.apply(param))); + case EqTerm eq -> subscoped(DimTyTerm.INSTANCE, param -> { // TODO: check boundaries - yield inherit(body.apply(param), eq.A().apply(param)); - } + return inherit(body.apply(param), eq.A().apply(param)); + }); default -> failF(new BadExprError(preterm, unifier.pos, expected)); - }); + }; case TupTerm _ -> failF(new BadExprError(preterm, unifier.pos, expected)); default -> unifier.compare(synthesizer.synthDontNormalize(preterm), expected, null); }; @@ -75,5 +73,7 @@ private boolean failF(@NotNull Problem problem) { @Override public @NotNull LocalCtx setLocalCtx(@NotNull LocalCtx ctx) { return unifier.setLocalCtx(ctx); } @Override public @NotNull TyckState state() { return unifier.state(); } @Override public @NotNull Reporter reporter() { return unifier.reporter(); } - public @NotNull LocalVar putIndex(@NotNull Term type) { return unifier.putIndex(type); } + public R subscoped(@NotNull Term type, @NotNull Function action) { + return unifier.subscoped(type, action); + } } diff --git a/base/src/main/java/org/aya/unify/Synthesizer.java b/base/src/main/java/org/aya/unify/Synthesizer.java index 4145e648cc..4246bc9f2a 100644 --- a/base/src/main/java/org/aya/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/unify/Synthesizer.java @@ -3,7 +3,7 @@ package org.aya.unify; import kala.collection.mutable.MutableList; -import org.aya.generic.NameGenerator; +import org.aya.generic.Renamer; import org.aya.generic.term.SortKind; import org.aya.syntax.core.def.PrimDef; import org.aya.syntax.core.term.*; @@ -27,11 +27,12 @@ import org.jetbrains.annotations.Nullable; public record Synthesizer( - @NotNull NameGenerator nameGen, + @NotNull Renamer renamer, @NotNull AbstractTycker tycker ) implements Stateful, Contextful { public Synthesizer(@NotNull AbstractTycker tycker) { - this(new NameGenerator(), tycker); + this(new Renamer(), tycker); + renamer.store(tycker.localCtx()); } public boolean inheritPiDom(@NotNull Term ty, @NotNull SortTerm expected) { @@ -77,10 +78,8 @@ public boolean inheritPiDom(@NotNull Term ty, @NotNull SortTerm expected) { case AppTerm(var f, var a) -> trySynth(f) instanceof PiTerm pi ? pi.body().apply(a) : null; case PiTerm pi -> { if (!(trySynth(pi.param()) instanceof SortTerm pSort)) yield null; - var bTy = subscoped(() -> { - var param = putIndex(pi.param()); - return trySynth(pi.body().apply(param)); - }); + var bTy = tycker.subscoped(pi.param(), param -> + trySynth(pi.body().apply(param)), renamer); if (!(bTy instanceof SortTerm bSort)) yield null; yield PiTerm.lub(pSort, bSort); @@ -88,7 +87,7 @@ public boolean inheritPiDom(@NotNull Term ty, @NotNull SortTerm expected) { case SigmaTerm sigma -> { var pTys = MutableList.create(); boolean succ = subscoped(() -> { - for (var p : sigma.view(i -> new FreeTerm(putIndex(i)))) { + for (var p : sigma.view(this::mkFree)) { if (!(trySynth(p) instanceof SortTerm pSort)) return false; pTys.append(pSort); } @@ -138,8 +137,10 @@ case MetaCall(var ref, var args) when ref.req() instanceof MetaVar.OfType(var ty }; } - public @NotNull LocalVar putIndex(@NotNull Term type) { - return tycker.putIndex(nameGen, type); + public @NotNull Term mkFree(@NotNull Term type) { + var param = LocalVar.generate(Renamer.nameOf(type)); + localCtx().put(param, type); + return new FreeTerm(param); } @Override public @NotNull TyckState state() { return tycker.state; } @Override public @NotNull LocalCtx localCtx() { return tycker.localCtx(); } diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java index 840355de39..05f9e2cf5b 100644 --- a/base/src/main/java/org/aya/unify/TermComparator.java +++ b/base/src/main/java/org/aya/unify/TermComparator.java @@ -4,7 +4,7 @@ import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; -import org.aya.generic.NameGenerator; +import org.aya.generic.Renamer; import org.aya.generic.stmt.Shaped; import org.aya.generic.term.SortKind; import org.aya.prettier.AyaPrettierOptions; @@ -43,13 +43,14 @@ public abstract sealed class TermComparator extends AbstractTycker permits Unifi // If false, we refrain from solving meta, and return false if we encounter a non-identical meta. private boolean solveMeta = true; private @Nullable FailureData failure = null; - private final @NotNull NameGenerator nameGen = new NameGenerator(); + final @NotNull Renamer nameGen = new Renamer(); public TermComparator( @NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Reporter reporter, @NotNull SourcePos pos, @NotNull Ordering cmp ) { super(state, ctx, reporter); + nameGen.store(ctx); this.pos = pos; this.cmp = cmp; } @@ -164,27 +165,23 @@ private boolean doCompareTyped(@NotNull Term lhs, @NotNull Term rhs, @NotNull Te case LamTerm _, ConCallLike _, TupTerm _ -> Panic.unreachable(); case ErrorTerm _ -> true; case PiTerm pi -> switch (new Pair<>(lhs, rhs)) { - case Pair(LamTerm(var lbody), LamTerm(var rbody)) -> subscoped(() -> { - var var = putIndex(pi.param()); - return compare( + case Pair(LamTerm(var lbody), LamTerm(var rbody)) -> subscoped(pi.param(), var -> + compare( lbody.apply(var), rbody.apply(var), pi.body().apply(var) - ); - }); + )); case Pair(LamTerm lambda, _) -> compareLambda(lambda, rhs, pi); case Pair(_, LamTerm rambda) -> compareLambda(rambda, lhs, pi); default -> compare(lhs, rhs, null); }; case EqTerm eq -> switch (new Pair<>(lhs, rhs)) { - case Pair(LamTerm(var lbody), LamTerm(var rbody)) -> subscoped(() -> { - var var = putIndex(DimTyTerm.INSTANCE); - return compare( + case Pair(LamTerm(var lbody), LamTerm(var rbody)) -> subscoped(DimTyTerm.INSTANCE, var -> + compare( lbody.apply(var), rbody.apply(var), eq.appA(new FreeTerm(var)) - ); - }); + )); case Pair(LamTerm lambda, _) -> compareLambda(lambda, rhs, eq); case Pair(_, LamTerm rambda) -> compareLambda(rambda, lhs, eq); default -> compare(lhs, rhs, null); @@ -253,10 +250,8 @@ case PAppTerm(var f, var a, _, _) -> { if (!(rhs instanceof CoeTerm(var rType, var rR, var rS))) yield null; if (!compare(coe.r(), rR, DimTyTerm.INSTANCE)) yield null; if (!compare(coe.s(), rS, DimTyTerm.INSTANCE)) yield null; - if (!subscoped(() -> { - var var = putIndex(DimTyTerm.INSTANCE); - return compare(coe.type().apply(var), rType.apply(var), null); - })) yield null; + if (!subscoped(DimTyTerm.INSTANCE, var -> + compare(coe.type().apply(var), rType.apply(var), null))) yield null; yield coe.family(); } case ProjTerm(var lof, var ldx) -> { @@ -314,8 +309,7 @@ case ProjTerm(var lof, var ldx) -> { /** Compare {@param lambda} and {@param rhs} with {@param type} */ private boolean compareLambda(@NotNull LamTerm lambda, @NotNull Term rhs, @NotNull PiTerm type) { - return subscoped(() -> { - var var = putIndex(type.param()); + return subscoped(type.param(), var -> { var lhsBody = lambda.body().apply(var); var rhsBody = AppTerm.make(rhs, new FreeTerm(var)); return compare(lhsBody, rhsBody, type.body().apply(var)); @@ -323,8 +317,7 @@ private boolean compareLambda(@NotNull LamTerm lambda, @NotNull Term rhs, @NotNu } private boolean compareLambda(@NotNull LamTerm lambda, @NotNull Term rhs, @NotNull EqTerm type) { - return subscoped(() -> { - var var = putIndex(DimTyTerm.INSTANCE); + return subscoped(DimTyTerm.INSTANCE, var -> { var lhsBody = lambda.body().apply(var); var free = new FreeTerm(var); var rhsBody = AppTerm.make(rhs, free); @@ -364,10 +357,7 @@ private R compareTypeWith( @NotNull Function continuation ) { if (!compare(lTy, rTy, null)) return onFailed.get(); - return subscoped(() -> { - var name = putParam(new Param(nameGen.next(whnf(lTy)), lTy, true)); - return continuation.apply(name); - }); + return subscoped(lTy, continuation); } private R compareTypesWithAux( @@ -451,10 +441,8 @@ case Pair(SigmaTerm(var lParams), SigmaTerm(var rParams)) -> compareTypesWith(lParams, rParams, () -> false, _ -> true); case Pair(SortTerm lhs, SortTerm rhs) -> compareSort(lhs, rhs); case Pair(EqTerm(var A, var a0, var a1), EqTerm(var B, var b0, var b1)) -> { - var tyResult = subscoped(() -> { - var var = putIndex(DimTyTerm.INSTANCE); - return compare(A.apply(var), B.apply(var), null); - }); + var tyResult = subscoped(DimTyTerm.INSTANCE, var -> + compare(A.apply(var), B.apply(var), null)); if (!tyResult) yield false; yield compare(a0, b0, A.apply(DimTerm.I0)) && compare(a1, b1, A.apply(DimTerm.I1)); } @@ -467,9 +455,8 @@ case Pair(EqTerm(var A, var a0, var a1), EqTerm(var B, var b0, var b1)) -> { localCtx().put(var, param.type()); return var; } - - public @NotNull LocalVar putIndex(@NotNull Term term) { - return super.putIndex(nameGen, term); + public R subscoped(@NotNull Term type, @NotNull Function action) { + return super.subscoped(type, action, nameGen); } public @NotNull FailureData getFailure() { diff --git a/cli-impl/src/test/resources/negative/ExprTyckError.txt b/cli-impl/src/test/resources/negative/ExprTyckError.txt index 839c82e6fc..5f87127956 100644 --- a/cli-impl/src/test/resources/negative/ExprTyckError.txt +++ b/cli-impl/src/test/resources/negative/ExprTyckError.txt @@ -78,8 +78,8 @@ Error: Cannot check the expression of type Type 1 against the type - \ _0 ⇒ 1 - (Normalized: \ _0 ⇒ 1) + \ 0 ⇒ 0 + (Normalized: \ 0 ⇒ 0) 2 error(s), 0 warning(s). What are you doing? diff --git a/cli-impl/src/test/resources/negative/GoalAndMeta.txt b/cli-impl/src/test/resources/negative/GoalAndMeta.txt index c335459337..5a5858c1f9 100644 --- a/cli-impl/src/test/resources/negative/GoalAndMeta.txt +++ b/cli-impl/src/test/resources/negative/GoalAndMeta.txt @@ -160,7 +160,7 @@ In file $FILE:7:15 -> Error: Unsolved meta _ in `^0 (?_ ^0)` - in `Fn (_0 : ^0 (?_ ^0)) → ^1 (Neg _0)` + in `Fn (y : ^0 (?_ ^0)) → ^1 (Neg y)` 4 error(s), 0 warning(s). What are you doing? diff --git a/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java index 2ccc581fa6..eecbd5ae6a 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/FnSerializer.java @@ -86,7 +86,7 @@ private void buildInvoke(FnDef unit, @NotNull String onStuckTerm, @NotNull Strin var argsTerm = "args"; var onStuckTerm = "onStuck"; var onStuckParam = new JitParam(onStuckTerm, CLASS_TERM); - var names = ImmutableSeq.fill(unit.telescope().size(), () -> nameGen().nextName(null)); + var names = ImmutableSeq.fill(unit.telescope().size(), () -> nameGen().nextName()); var fixedParams = MutableList.create(); fixedParams.append(onStuckParam); fixedParams.appendAll(names.view().map(x -> new JitParam(x, CLASS_TERM))); diff --git a/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java index 40b0f217f7..076a8c96ed 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java @@ -96,7 +96,7 @@ private void doSerialize(@NotNull Pat pat, @NotNull String term, @NotNull Once c buildIfElse(STR."\{ExprializeUtils.getCallInstance(mmTerm)} == \{ExprializeUtils.getInstance(NameSerializer.getClassReference(con.ref()))}", State.Mismatch, () -> { var conArgsTerm = buildLocalVar(TYPE_IMMTERMSEQ, - nameGen().nextName(null), STR."\{mmTerm}.conArgs()"); + nameGen().nextName(), STR."\{mmTerm}.conArgs()"); doSerialize(con.args().view(), SourceBuilder.fromSeq(conArgsTerm, con.args().size()).view(), Once.of(() -> buildUpdate(VARIABLE_SUBSTATE, "true"))); })) @@ -137,7 +137,7 @@ private void multiStage( @NotNull ImmutableSeq> preContinuation, @NotNull Once continuation ) { - var tmpName = nameGen().nextName(null); + var tmpName = nameGen().nextName(); buildUpdate(VARIABLE_SUBSTATE, "false"); buildLocalVar(CLASS_TERM, tmpName, term); diff --git a/jit-compiler/src/main/java/org/aya/compiler/SourceBuilder.java b/jit-compiler/src/main/java/org/aya/compiler/SourceBuilder.java index e5b7e07b32..a5437f0774 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/SourceBuilder.java +++ b/jit-compiler/src/main/java/org/aya/compiler/SourceBuilder.java @@ -87,7 +87,7 @@ default void buildIfInstanceElse( @NotNull Consumer onSucc, @Nullable Runnable onFailed ) { - String name = nameGen().nextName(null); + String name = nameGen().nextName(); buildIfElse(STR."\{term} instanceof \{type} \{name}", () -> onSucc.accept(name), onFailed); @@ -126,7 +126,7 @@ default void buildClass( default @NotNull ImmutableSeq buildGenLocalVarsFromSeq(@NotNull String type, @NotNull String seqTerm, int size) { String[] names = new String[size]; for (int i = 0; i < size; ++i) { - var name = nameGen().nextName(null); + var name = nameGen().nextName(); names[i] = name; buildLocalVar(type, name, STR."\{seqTerm}.get(\{i})"); } diff --git a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java index e9665a825f..007c0360d6 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java @@ -235,7 +235,7 @@ case ListTerm(var repr, var nil, var cons, var type) -> ExprializeUtils.makeNew( } private @NotNull String serializeClosure(@NotNull Closure body) { - return serializeClosure(nameGen.nextName(null), body); + return serializeClosure(nameGen.nextName(), body); } private @NotNull String serializeClosure(@NotNull String param, @NotNull Closure body) { diff --git a/syntax/src/main/java/org/aya/generic/NameGenerator.java b/syntax/src/main/java/org/aya/generic/NameGenerator.java index cf798b5523..b7a622796e 100644 --- a/syntax/src/main/java/org/aya/generic/NameGenerator.java +++ b/syntax/src/main/java/org/aya/generic/NameGenerator.java @@ -2,17 +2,7 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.generic; -import org.aya.syntax.core.pat.PatToTerm; -import org.aya.syntax.core.term.*; -import org.aya.syntax.core.term.xtt.CoeTerm; -import org.aya.syntax.core.term.xtt.DimTyTerm; -import org.aya.syntax.core.term.xtt.EqTerm; -import org.aya.syntax.core.term.xtt.PAppTerm; -import org.aya.syntax.ref.GenerateKind; -import org.aya.syntax.ref.LocalVar; -import org.aya.util.error.SourcePos; import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; /** * Thread-unsafe name generator @@ -24,36 +14,7 @@ public int nextId() { return id++; } - public @NotNull String next(@Nullable Term whty) { - return whty == null ? nextName(null) : nextName(nameOf(whty)); - } - - public @NotNull LocalVar nextVar(@Nullable Term whty) { - return new LocalVar(next(whty), SourcePos.SER, GenerateKind.Basic.Tyck); - } - - public @NotNull String nextName(@Nullable String typeName) { - return (typeName == null ? "" : Constants.ANONYMOUS_PREFIX + typeName) - + Constants.ANONYMOUS_PREFIX + nextId(); - } - - public @Nullable String nameOf(@NotNull Term ty) { - return switch (ty) { - case FreeTerm freeTerm -> freeTerm.name().name(); - case MetaPatTerm(var meta) -> { - var solution = meta.solution().get(); - if (solution == null) yield null; - yield nameOf(PatToTerm.visit(solution)); - } - case PiTerm _ -> "Pi"; - case SigmaTerm _ -> "Sigma"; - case DimTyTerm _ -> "Dim"; - case ProjTerm p -> nameOf(p.of()); - case AppTerm a -> nameOf(a.fun()); - case PAppTerm a -> nameOf(a.fun()); - case EqTerm _ -> "Eq"; - case CoeTerm _ -> "coe"; - default -> null; - }; + public @NotNull String nextName() { + return Constants.ANONYMOUS_PREFIX + nextId(); } } diff --git a/syntax/src/main/java/org/aya/generic/Renamer.java b/syntax/src/main/java/org/aya/generic/Renamer.java new file mode 100644 index 0000000000..c05c929c9a --- /dev/null +++ b/syntax/src/main/java/org/aya/generic/Renamer.java @@ -0,0 +1,98 @@ +// Copyright (c) 2020-2024 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.generic; + +import kala.collection.mutable.MutableMap; +import org.aya.syntax.core.pat.PatToTerm; +import org.aya.syntax.core.term.*; +import org.aya.syntax.core.term.call.Callable; +import org.aya.syntax.core.term.xtt.CoeTerm; +import org.aya.syntax.core.term.xtt.DimTyTerm; +import org.aya.syntax.core.term.xtt.EqTerm; +import org.aya.syntax.core.term.xtt.PAppTerm; +import org.aya.syntax.ref.LocalCtx; +import org.aya.syntax.ref.LocalVar; +import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; + +public record Renamer(MutableMap scope) { + public Renamer() { + this(MutableMap.create()); + } + + public void store(@NotNull LocalCtx ctx) { + ctx.extract().forEach(lv -> scope.put(lv.name(), lv)); + } + + public static @NotNull String nameOf(@Nullable Term ty) { + return switch (ty) { + case FreeTerm(var name) -> name.name(); + case MetaPatTerm(var meta) -> { + var solution = meta.solution().get(); + if (solution == null) yield "p"; + yield nameOf(PatToTerm.visit(solution)); + } + case Callable.Tele c -> Character.toString(Character.toLowerCase( + c.ref().name().codePointAt(0))); + case PiTerm _ -> "f"; + case SigmaTerm _ -> "t"; + case DimTyTerm _ -> "i"; + case ProjTerm p -> nameOf(p.of()); + case AppTerm a -> nameOf(a.fun()); + case PAppTerm a -> nameOf(a.fun()); + case EqTerm _, CoeTerm _ -> "p"; + case null, default -> "x"; + }; + } + + public @NotNull LocalVar bindName(@Nullable Term name) { + return bindName(nameOf(name)); + } + public @NotNull LocalVar bindName(@NotNull String name) { + if (scope.containsKey(name)) { + var newGame = sanitizeName(name); + var uid = LocalVar.generate(newGame); + scope.put(newGame, uid); + return uid; + } else { + var uid = LocalVar.generate(name); + scope.put(name, uid); + return uid; + } + } + + private String sanitizeName(String name) { + if (name.length() == 1) { + var c = name.codePointAt(0); + if (c >= 'a' && c <= 'z') { + var ideal = conflictAlphabetic(c, 'a'); + if (ideal != null) return ideal; + } + if (c >= 'A' && c <= 'Z') { + var ideal = conflictAlphabetic(c, 'A'); + if (ideal != null) return ideal; + } + } + return conflictSuffix(name); + } + + private String conflictAlphabetic(int c, int base) { + int initial = c - base; + int i = initial + 1; + while (scope.containsKey(Character.toString(i + base))) { + if (i == initial) return null; + i = (i + 1) % 26; + } + return Character.toString(i + base); + } + + private String conflictSuffix(String name) { + int i = 0; + while (scope.containsKey(name + i)) i++; + return name + i; + } + + public void unbindName(@NotNull LocalVar uid) { + scope.remove(uid.name()); + } +} diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java index c4d64f50cb..79edadbae9 100644 --- a/syntax/src/main/java/org/aya/prettier/CorePrettier.java +++ b/syntax/src/main/java/org/aya/prettier/CorePrettier.java @@ -8,7 +8,7 @@ import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableList; import org.aya.generic.AyaDocile; -import org.aya.generic.NameGenerator; +import org.aya.generic.Renamer; import org.aya.generic.term.ParamLike; import org.aya.pretty.doc.Doc; import org.aya.syntax.concrete.stmt.decl.DataCon; @@ -44,7 +44,7 @@ * @see ConcretePrettier */ public class CorePrettier extends BasePrettier { - private final NameGenerator nameGen = new NameGenerator(); + private final Renamer nameGen = new Renamer(); public CorePrettier(@NotNull PrettierOptions options) { super(options); @@ -96,10 +96,10 @@ case SigmaTerm(var params) -> { yield checkParen(outer, doc, Outer.BinOp); } case LamTerm lam -> { - var pair = LamTerm.unwrap(lam); - var params = generateNames(pair.component1()).view(); - var paramRef = params.map(FreeTerm::new); - var body = pair.component2().instantiateTele(paramRef); + var pair = LamTerm.unlam(lam, nameGen); + var params = pair.params(); + var paramRef = params.view().map(FreeTerm::new); + var body = pair.body().instantiateTele(paramRef); Doc bodyDoc; // Syntactic eta-contraction if (body instanceof Callable.Tele call) { @@ -121,7 +121,10 @@ case SigmaTerm(var params) -> { if (params.isEmpty()) yield bodyDoc; var list = MutableList.of(LAMBDA); - params.forEach(param -> list.append(Doc.bracedUnless(linkDef(param), true))); + params.forEach(param -> { + nameGen.unbindName(param); + list.append(Doc.bracedUnless(linkDef(param), true)); + }); list.append(FN_DEFINED_AS); list.append(bodyDoc); var doc = Doc.sep(list); @@ -175,25 +178,23 @@ case ErrorTerm(var desc, var isReallyError) -> { case PiTerm piTerm -> { // Try to omit the Pi keyword { - var var = nameGen.nextVar(piTerm.param()); + var var = nameGen.bindName(piTerm.param()); var codomain = piTerm.body().apply(var); if (FindUsage.free(codomain, var) == 0) { - yield checkParen(outer, Doc.sep( - justType(Arg.ofExplicitly(piTerm.param()), Outer.BinOp), - ARROW, - term(Outer.Codomain, codomain) - ), Outer.BinOp); + var param = justType(Arg.ofExplicitly(piTerm.param()), Outer.BinOp); + var cod = term(Outer.Codomain, codomain); + nameGen.unbindName(var); + yield checkParen(outer, Doc.sep(param, ARROW, cod), Outer.BinOp); } } - var pair = PiTerm.unpi(piTerm, UnaryOperator.identity()); - var params = pair.names().zip(pair.params(), CoreParam::new); + var pair = PiTerm.unpi(piTerm, UnaryOperator.identity(), nameGen); + var params = pair.names().zip(pair.params(), CoreParam::new) + .toImmutableSeq(); var body = pair.body().instantiateTeleVar(params.view().map(ParamLike::ref)); - var doc = Doc.sep( - KW_PI, - visitTele(params, body, FindUsage::free), - ARROW, - term(Outer.Codomain, body) - ); + var teleDoc = visitTele(params, body, FindUsage::free); + var cod = term(Outer.Codomain, body); + var doc = Doc.sep(KW_PI, teleDoc, ARROW, cod); + pair.names().forEach(nameGen::unbindName); // Add paren when it's not free or a codomain yield checkParen(outer, doc, Outer.BinOp); } @@ -401,13 +402,8 @@ private record CoreParam( return richTele.toImmutableSeq(); } - // used for lambda - private @NotNull ImmutableSeq generateNames(int count) { - return ImmutableSeq.fill(count, () -> generateName(null)); - } - private @NotNull LocalVar generateName(@Nullable Term whty) { - return LocalVar.generate(nameGen.next(whty), SourcePos.SER); + return nameGen.bindName(whty); } /// endregion Name Generating } diff --git a/syntax/src/main/java/org/aya/syntax/core/term/LamTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/LamTerm.java index c1266893be..1c024eaf6f 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/LamTerm.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/LamTerm.java @@ -2,8 +2,10 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.syntax.core.term; +import kala.collection.Seq; +import kala.collection.mutable.MutableList; import kala.function.IndexedFunction; -import kala.tuple.primitive.IntObjTuple2; +import org.aya.generic.Renamer; import org.aya.syntax.core.Closure; import org.aya.syntax.core.term.marker.StableWHNF; import org.aya.syntax.ref.LocalVar; @@ -24,21 +26,24 @@ public LamTerm(Term indexedBody) { return body; } + public record Unlam(@NotNull Seq params, @NotNull Term body) { } + /** * Unwrap a {@link LamTerm} as much as possible * * @return an integer indicates how many bindings are introduced * and a most inner term that is not a {@link LamTerm}. */ - public static @NotNull IntObjTuple2 unwrap(@NotNull Term term) { - int params = 0; + public static @NotNull Unlam unlam(@NotNull Term term, @NotNull Renamer nameGen) { + var params = MutableList.create(); var it = term; while (it instanceof LamTerm lamTerm) { - params = params + 1; - it = lamTerm.body.apply(new FreeTerm(LocalVar.generate(String.valueOf(params)))); + var name = nameGen.bindName(String.valueOf(params.size())); + params.append(name); + it = lamTerm.body.apply(new FreeTerm(name)); } - return IntObjTuple2.of(params, it); + return new Unlam(params, it); } } diff --git a/syntax/src/main/java/org/aya/syntax/core/term/PiTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/PiTerm.java index ae07099c7d..68f53a86a1 100644 --- a/syntax/src/main/java/org/aya/syntax/core/term/PiTerm.java +++ b/syntax/src/main/java/org/aya/syntax/core/term/PiTerm.java @@ -2,11 +2,12 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.syntax.core.term; +import kala.collection.Seq; import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableList; import kala.function.IndexedFunction; -import org.aya.generic.NameGenerator; +import org.aya.generic.Renamer; import org.aya.generic.term.SortKind; import org.aya.syntax.core.Closure; import org.aya.syntax.core.term.marker.Formation; @@ -31,22 +32,25 @@ public record PiTerm(@NotNull Term param, @NotNull Closure body) implements Stab } public record Unpi( - @NotNull ImmutableSeq params, - @NotNull ImmutableSeq names, + @NotNull Seq params, + @NotNull Seq names, @NotNull Term body ) { } - @ForLSP public static @NotNull Unpi unpi(@NotNull Term term, @NotNull UnaryOperator pre) { + public static @NotNull Unpi unpi(@NotNull Term term, @NotNull UnaryOperator pre) { + return unpi(term, pre, new Renamer()); + } + @ForLSP public static @NotNull Unpi + unpi(@NotNull Term term, @NotNull UnaryOperator pre, @NotNull Renamer nameGen) { var params = MutableList.create(); var names = MutableList.create(); - var nameGen = new NameGenerator(); while (pre.apply(term) instanceof PiTerm(var param, var body)) { params.append(param); - var var = LocalVar.generate(nameGen.next(param)); + var var = nameGen.bindName(param); names.append(var); term = body.apply(var); } - return new Unpi(params.toImmutableSeq(), names.toImmutableSeq(), term); + return new Unpi(params, names, term); } public record UnpiRaw( @NotNull ImmutableSeq params, diff --git a/syntax/src/main/java/org/aya/syntax/ref/LocalCtx.java b/syntax/src/main/java/org/aya/syntax/ref/LocalCtx.java index 21cdc43259..875bd273b8 100644 --- a/syntax/src/main/java/org/aya/syntax/ref/LocalCtx.java +++ b/syntax/src/main/java/org/aya/syntax/ref/LocalCtx.java @@ -5,66 +5,23 @@ import kala.collection.SeqView; import kala.collection.mutable.MutableLinkedHashMap; import kala.collection.mutable.MutableList; -import kala.control.Option; import org.aya.syntax.core.term.Term; import org.aya.util.Scoped; import org.jetbrains.annotations.Contract; import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; import java.util.function.UnaryOperator; -public record LocalCtx( - @NotNull MutableLinkedHashMap binds, - @NotNull MutableList vars, - @Override @Nullable LocalCtx parent -) implements Scoped { - public LocalCtx() { - this(MutableLinkedHashMap.of(), MutableList.create(), null); - } - - public boolean isEmpty() { - return binds.isEmpty() && (parent == null || parent.isEmpty()); - } - - @Override public @NotNull LocalCtx self() { return this; } - - @Override @Contract("-> new") - public @NotNull LocalCtx derive() { - return new LocalCtx(MutableLinkedHashMap.of(), MutableList.create(), this); - } - - public int size() { - return binds.size() + (parent == null ? 0 : parent.size()); - } - - public @NotNull Option getLocal(@NotNull LocalVar name) { - return binds.getOption(name); - } - - @Override public void putLocal(@NotNull LocalVar key, @NotNull Term value) { - binds.put(key, value); - vars.append(key); - } - +public interface LocalCtx extends Scoped { + boolean isEmpty(); + int size(); @Contract(value = "_ -> new", pure = true) - public @NotNull LocalCtx map(UnaryOperator mapper) { - var newBinds = binds.view() - .mapValues((_, t) -> mapper.apply(t)); - - return new LocalCtx(MutableLinkedHashMap.from(newBinds), vars, parent == null ? null : parent.map(mapper)); - } - - /** - * Collect free variables of this context, usually used for {@link MetaVar} - */ - public @NotNull SeqView extract() { - SeqView parentView = parent == null ? SeqView.empty() : parent.extract(); - return parentView.concat(vars); - } + @NotNull LocalCtx map(UnaryOperator mapper); + @NotNull SeqView extract(); + @NotNull LocalCtx clone(); + @Override default @NotNull LocalCtx self() { return this; } - @SuppressWarnings("MethodDoesntCallSuperMethod") - @Override public @NotNull LocalCtx clone() { - return new LocalCtx(binds.clone(), vars.clone(), parent != null ? parent.clone() : null); + @Override @Contract("-> new") default @NotNull LocalCtx derive() { + return new MapLocalCtx(MutableLinkedHashMap.of(), MutableList.create(), this); } } diff --git a/syntax/src/main/java/org/aya/syntax/ref/LocalCtx1.java b/syntax/src/main/java/org/aya/syntax/ref/LocalCtx1.java new file mode 100644 index 0000000000..7cd6bef7cd --- /dev/null +++ b/syntax/src/main/java/org/aya/syntax/ref/LocalCtx1.java @@ -0,0 +1,39 @@ +// Copyright (c) 2020-2024 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.syntax.ref; + +import kala.collection.SeqView; +import kala.control.Option; +import org.aya.syntax.core.term.Term; +import org.aya.util.error.Panic; +import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; + +import java.util.function.UnaryOperator; + +public record LocalCtx1( + @NotNull Term type, + @NotNull LocalVar var, + @Override @Nullable LocalCtx parent +) implements LocalCtx { + @Override public boolean isEmpty() { return false; } + @Override public int size() { + return 1 + (parent == null ? 0 : parent.size()); + } + @Override public @NotNull LocalCtx map(UnaryOperator mapper) { + return new LocalCtx1(mapper.apply(type), var, parent == null ? null : parent.map(mapper)); + } + @Override public @NotNull SeqView extract() { + SeqView parentView = parent == null ? SeqView.empty() : parent.extract(); + return parentView.concat(SeqView.of(var)); + } + @Override public @NotNull LocalCtx clone() { + return new LocalCtx1(type, var, parent == null ? null : parent.clone()); + } + @Override public @NotNull Option getLocal(@NotNull LocalVar key) { + return key.equals(var) ? Option.some(type) : parent == null ? Option.none() : parent.getLocal(key); + } + @Override public void putLocal(@NotNull LocalVar key, @NotNull Term value) { + throw new Panic("LocalCtx1 is immutable"); + } +} diff --git a/syntax/src/main/java/org/aya/syntax/ref/MapLocalCtx.java b/syntax/src/main/java/org/aya/syntax/ref/MapLocalCtx.java new file mode 100644 index 0000000000..a65aee1886 --- /dev/null +++ b/syntax/src/main/java/org/aya/syntax/ref/MapLocalCtx.java @@ -0,0 +1,62 @@ +// Copyright (c) 2020-2024 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.syntax.ref; + +import kala.collection.SeqView; +import kala.collection.mutable.MutableLinkedHashMap; +import kala.collection.mutable.MutableList; +import kala.control.Option; +import org.aya.syntax.core.term.Term; +import org.jetbrains.annotations.Contract; +import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; + +import java.util.function.UnaryOperator; + +public record MapLocalCtx( + @NotNull MutableLinkedHashMap binds, + @NotNull MutableList vars, + @Override @Nullable LocalCtx parent +) implements LocalCtx { + public MapLocalCtx() { + this(MutableLinkedHashMap.of(), MutableList.create(), null); + } + + @Override public boolean isEmpty() { + return binds.isEmpty() && (parent == null || parent.isEmpty()); + } + + @Override public int size() { + return binds.size() + (parent == null ? 0 : parent.size()); + } + + public @NotNull Option getLocal(@NotNull LocalVar name) { + return binds.getOption(name); + } + + @Override public void putLocal(@NotNull LocalVar key, @NotNull Term value) { + binds.put(key, value); + vars.append(key); + } + + @Override @Contract(value = "_ -> new", pure = true) + public @NotNull LocalCtx map(UnaryOperator mapper) { + var newBinds = binds.view() + .mapValues((_, t) -> mapper.apply(t)); + + return new MapLocalCtx(MutableLinkedHashMap.from(newBinds), vars, parent == null ? null : parent.map(mapper)); + } + + /** + * Collect free variables of this context, usually used for {@link MetaVar} + */ + @Override public @NotNull SeqView extract() { + SeqView parentView = parent == null ? SeqView.empty() : parent.extract(); + return parentView.concat(vars); + } + + @SuppressWarnings("MethodDoesntCallSuperMethod") + @Override public @NotNull MapLocalCtx clone() { + return new MapLocalCtx(binds.clone(), vars.clone(), parent != null ? parent.clone() : null); + } +}