From db96adf4a856d72ad961a539dc9912745ca825c9 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 19:19:10 -0500 Subject: [PATCH 01/28] misc: move file --- base/src/main/java/org/aya/core/term/Term.java | 2 +- base/src/main/java/org/aya/tyck/tycker/PropTycker.java | 4 ++-- base/src/main/java/org/aya/tyck/unify/DoubleChecker.java | 3 +-- base/src/main/java/org/aya/tyck/{ => unify}/Synthesizer.java | 2 +- 4 files changed, 5 insertions(+), 6 deletions(-) rename base/src/main/java/org/aya/tyck/{ => unify}/Synthesizer.java (99%) diff --git a/base/src/main/java/org/aya/core/term/Term.java b/base/src/main/java/org/aya/core/term/Term.java index dbe77e6301..c1587ae0cd 100644 --- a/base/src/main/java/org/aya/core/term/Term.java +++ b/base/src/main/java/org/aya/core/term/Term.java @@ -19,9 +19,9 @@ import org.aya.pretty.doc.Doc; import org.aya.ref.AnyVar; import org.aya.ref.LocalVar; -import org.aya.tyck.Synthesizer; import org.aya.tyck.env.LocalCtx; import org.aya.tyck.tycker.TyckState; +import org.aya.tyck.unify.Synthesizer; import org.aya.util.Arg; import org.aya.util.error.SourcePos; import org.aya.util.prettier.PrettierOptions; diff --git a/base/src/main/java/org/aya/tyck/tycker/PropTycker.java b/base/src/main/java/org/aya/tyck/tycker/PropTycker.java index ec9e846a5d..3f883fbb3c 100644 --- a/base/src/main/java/org/aya/tyck/tycker/PropTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/PropTycker.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.tyck.tycker; @@ -9,8 +9,8 @@ import org.aya.generic.util.InternalException; import org.aya.prettier.AyaPrettierOptions; import org.aya.tyck.ExprTycker; -import org.aya.tyck.Synthesizer; import org.aya.tyck.trace.Trace; +import org.aya.tyck.unify.Synthesizer; import org.aya.util.reporter.Reporter; import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; diff --git a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java index 2df380ff18..a868eadc55 100644 --- a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java +++ b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java @@ -1,10 +1,9 @@ -// 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.tyck.unify; import org.aya.core.term.*; import org.aya.generic.util.NormalizeMode; -import org.aya.tyck.Synthesizer; import org.aya.tyck.error.BadExprError; import org.aya.tyck.error.TupleError; import org.aya.tyck.unify.TermComparator.Sub; diff --git a/base/src/main/java/org/aya/tyck/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java similarity index 99% rename from base/src/main/java/org/aya/tyck/Synthesizer.java rename to base/src/main/java/org/aya/tyck/unify/Synthesizer.java index e0650b9568..1a51c324ec 100644 --- a/base/src/main/java/org/aya/tyck/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -1,6 +1,6 @@ // 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.tyck; +package org.aya.tyck.unify; import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableList; From 5cb4030e689a2d0bb805982b3e85aaf604b7a969 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 20:50:42 -0500 Subject: [PATCH 02/28] sort: RTFM --- note/sort-system.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 note/sort-system.md diff --git a/note/sort-system.md b/note/sort-system.md new file mode 100644 index 0000000000..c5000e5875 --- /dev/null +++ b/note/sort-system.md @@ -0,0 +1,28 @@ +# Agda's sort system + +Comments: + ++ `ISet` behaves like `Set`, but functions into `Type` land in `Type`. ++ Supports `Inf`, `LockUniv`, and `SizeUniv`. ++ `Prop` is predicative because of the termination checker. ++ Reference: https://github.com/agda/agda/issues/5667 + +Related rules: + +| Input | Output | Sort | +|--------------|--------------|------------------| +| `Prop` a | `Type` b | `Type` a ∨ b | +| `Type` a | `Prop` b | `Prop` a ∨ b | +| `? a` | `? b` (same) | `?` a ∨ b (same) | +| not `Prop` a | not `Prop` b | `Set` a ∨ b | + +# Regarding impredicativity + +Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. _Definitional Proof-Irrelevance withouth K_. [PDF](https://hal.inria.fr/hal-01859964v2/document) + +Page 1:10 mentions: + +> _An impredicative variant_. +> We will see in section 4 that we can also allow +> an impredicative version of `sProp`, which amounts +> to just ignoring the indices on `sProp` throughout. From 88433a7722c4f115cef6995df04381fb41673f56 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 21:23:23 -0500 Subject: [PATCH 03/28] meta: move --- base/src/main/java/module-info.java | 1 + .../java/org/aya/core/{ => meta}/Meta.java | 41 +++++++++++-------- .../main/java/org/aya/core/meta/MetaInfo.java | 25 +++++++++++ .../main/java/org/aya/tyck/env/LocalCtx.java | 2 +- .../java/org/aya/tyck/tycker/TyckState.java | 6 +-- .../main/java/org/aya/tyck/unify/Unifier.java | 4 +- note/sort-system.md | 23 +++++++---- 7 files changed, 70 insertions(+), 32 deletions(-) rename base/src/main/java/org/aya/core/{ => meta}/Meta.java (74%) create mode 100644 base/src/main/java/org/aya/core/meta/MetaInfo.java diff --git a/base/src/main/java/module-info.java b/base/src/main/java/module-info.java index a7ee70128c..c155bc4f38 100644 --- a/base/src/main/java/module-info.java +++ b/base/src/main/java/module-info.java @@ -42,4 +42,5 @@ exports org.aya.tyck.trace; exports org.aya.tyck.unify; exports org.aya.tyck; + exports org.aya.core.meta; } diff --git a/base/src/main/java/org/aya/core/Meta.java b/base/src/main/java/org/aya/core/meta/Meta.java similarity index 74% rename from base/src/main/java/org/aya/core/Meta.java rename to base/src/main/java/org/aya/core/meta/Meta.java index 09396ee70c..eb5e945025 100644 --- a/base/src/main/java/org/aya/core/Meta.java +++ b/base/src/main/java/org/aya/core/meta/Meta.java @@ -1,6 +1,6 @@ // 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; +package org.aya.core.meta; import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; @@ -15,7 +15,6 @@ import org.aya.util.Arg; import org.aya.util.error.SourcePos; import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; /** * @author ice1000, re-xyr @@ -26,13 +25,8 @@ public final class Meta implements AnyVar { public final @NotNull ImmutableSeq contextTele; public final @NotNull ImmutableSeq telescope; public final @NotNull String name; - public final @Nullable Term result; + public final @NotNull MetaInfo info; public final @NotNull SourcePos sourcePos; - /** - * Usually implies {@link Meta#result} == null, - * asserts that the current meta is a type meta. - */ - public final boolean isType; public final @NotNull MutableList> conditions = MutableList.create(); public SeqView fullTelescope() { @@ -42,14 +36,13 @@ public SeqView fullTelescope() { private Meta( @NotNull ImmutableSeq contextTele, @NotNull ImmutableSeq telescope, - @NotNull String name, @Nullable Term result, - boolean isType, @NotNull SourcePos sourcePos + @NotNull String name, @NotNull MetaInfo info, + @NotNull SourcePos sourcePos ) { this.contextTele = contextTele; this.telescope = telescope; this.name = name; - this.result = result; - this.isType = isType; + this.info = info; this.sourcePos = sourcePos; } @@ -57,7 +50,7 @@ private Meta( @NotNull ImmutableSeq contextTele, @NotNull String name, @NotNull SourcePos sourcePos ) { - return new Meta(contextTele, ImmutableSeq.empty(), name, null, true, sourcePos); + return new Meta(contextTele, ImmutableSeq.empty(), name, new MetaInfo.AnyType(), sourcePos); } public static @NotNull Meta from( @@ -66,9 +59,9 @@ private Meta( ) { if (result instanceof PiTerm pi) { var buf = MutableList.create(); - var r = pi.parameters(buf); - return new Meta(contextTele, buf.toImmutableSeq(), name, r, false, sourcePos); - } else return new Meta(contextTele, ImmutableSeq.empty(), name, result, false, sourcePos); + var r = new MetaInfo.Result(pi.parameters(buf)); + return new Meta(contextTele, buf.toImmutableSeq(), name, r, sourcePos); + } else return new Meta(contextTele, ImmutableSeq.empty(), name, new MetaInfo.Result(result), sourcePos); } public @NotNull PiTerm asPi( @@ -76,14 +69,26 @@ private Meta( @NotNull ImmutableSeq> contextArgs ) { assert telescope.isEmpty(); - var domVar = new Meta(contextTele, ImmutableSeq.empty(), domName, result, isType, sourcePos); - var codVar = new Meta(contextTele, ImmutableSeq.empty(), codName, result, isType, sourcePos); + // TODO[isType]: this one should be piDom + var domVar = new Meta(contextTele, ImmutableSeq.empty(), domName, info, sourcePos); + // TODO[isType]: this one should be piCod + var codVar = new Meta(contextTele, ImmutableSeq.empty(), codName, info, sourcePos); var dom = new MetaTerm(domVar, contextArgs, ImmutableSeq.empty()); var cod = new MetaTerm(codVar, contextArgs, ImmutableSeq.empty()); var domParam = new Term.Param(Constants.randomlyNamed(sourcePos), dom, explicit); return new PiTerm(domParam, cod); } + public @NotNull MetaTerm asPiDom( + @NotNull Term resultNew, @NotNull ImmutableSeq> contextArgs + ) { + assert telescope.isEmpty(); + assert info instanceof MetaInfo.AnyType; + // TODO[isType]: this one should be piDom + var typed = new Meta(contextTele, ImmutableSeq.empty(), name, info, sourcePos); + return new MetaTerm(typed, contextArgs, ImmutableSeq.empty()); + } + @Override public @NotNull String name() { return name; } diff --git a/base/src/main/java/org/aya/core/meta/MetaInfo.java b/base/src/main/java/org/aya/core/meta/MetaInfo.java new file mode 100644 index 0000000000..f16a75577d --- /dev/null +++ b/base/src/main/java/org/aya/core/meta/MetaInfo.java @@ -0,0 +1,25 @@ +// 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.meta; + +import org.aya.core.term.Term; +import org.jetbrains.annotations.NotNull; + +/** + * Constraints on a meta variable. + * + * @author ice1000 + */ +public sealed interface MetaInfo { + /** + * The type of the meta is known. + * We shall check the solution against this type. + */ + record Result(@NotNull Term result) implements MetaInfo {} + + /** + * The meta variable is a type. + * It should be able to appear on the RHS of a judgment. + */ + record AnyType() implements MetaInfo {} +} diff --git a/base/src/main/java/org/aya/tyck/env/LocalCtx.java b/base/src/main/java/org/aya/tyck/env/LocalCtx.java index 774fc86661..7cd53294b5 100644 --- a/base/src/main/java/org/aya/tyck/env/LocalCtx.java +++ b/base/src/main/java/org/aya/tyck/env/LocalCtx.java @@ -9,8 +9,8 @@ import kala.collection.mutable.MutableList; import kala.tuple.Tuple; import kala.tuple.Tuple2; -import org.aya.core.Meta; import org.aya.core.UntypedParam; +import org.aya.core.meta.Meta; import org.aya.core.term.IntervalTerm; import org.aya.core.term.LamTerm; import org.aya.core.term.MetaTerm; diff --git a/base/src/main/java/org/aya/tyck/tycker/TyckState.java b/base/src/main/java/org/aya/tyck/tycker/TyckState.java index 9a5e1468c0..6c4872caf0 100644 --- a/base/src/main/java/org/aya/tyck/tycker/TyckState.java +++ b/base/src/main/java/org/aya/tyck/tycker/TyckState.java @@ -1,12 +1,12 @@ -// 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.tyck.tycker; import kala.collection.mutable.MutableList; import kala.collection.mutable.MutableMap; import kala.collection.mutable.MutableSet; -import org.aya.core.Meta; import org.aya.core.def.PrimDef; +import org.aya.core.meta.Meta; import org.aya.core.term.ErrorTerm; import org.aya.core.term.MetaTerm; import org.aya.core.term.SortTerm; @@ -21,9 +21,9 @@ import org.aya.tyck.trace.Trace; import org.aya.tyck.unify.Unifier; import org.aya.util.Ordering; -import org.aya.util.prettier.PrettierOptions; import org.aya.util.error.SourcePos; import org.aya.util.error.WithPos; +import org.aya.util.prettier.PrettierOptions; import org.aya.util.reporter.Reporter; import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index e5fd10e8d6..df04844108 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -1,11 +1,11 @@ -// 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.tyck.unify; import kala.collection.Seq; import kala.collection.mutable.MutableArrayList; import kala.control.Option; -import org.aya.core.Meta; +import org.aya.core.meta.Meta; import org.aya.core.ops.Eta; import org.aya.core.term.*; import org.aya.core.visitor.DeltaExpander; diff --git a/note/sort-system.md b/note/sort-system.md index c5000e5875..4cc36772b0 100644 --- a/note/sort-system.md +++ b/note/sort-system.md @@ -6,19 +6,26 @@ Comments: + Supports `Inf`, `LockUniv`, and `SizeUniv`. + `Prop` is predicative because of the termination checker. + Reference: https://github.com/agda/agda/issues/5667 ++ `SSet` is paraphrased as `Set` below to be consistent with Aya. -Related rules: +Related rules on the $\Pi$-type: -| Input | Output | Sort | -|--------------|--------------|------------------| -| `Prop` a | `Type` b | `Type` a ∨ b | -| `Type` a | `Prop` b | `Prop` a ∨ b | -| `? a` | `? b` (same) | `?` a ∨ b (same) | -| not `Prop` a | not `Prop` b | `Set` a ∨ b | +| Input sort | Output sort | Sort | +|------------|--------------|------------------| +| `Prop` a | `Type` b | `Type` a ∨ b | +| `Type` a | `Prop` b | `Prop` a ∨ b | +| `?` a | `?` b (same) | `?` a ∨ b (same) | +| `?` a | `¿` b | `Set` a ∨ b | + +# Notes + ++ If sort is not `Set`, then cod's sort is just `<=` the result sort and should have the same kind. ++ If sort is `Set`, then cod's sort is `<=` the result sort and can be any kind. # Regarding impredicativity -Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. _Definitional Proof-Irrelevance withouth K_. [PDF](https://hal.inria.fr/hal-01859964v2/document) +Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. _Definitional Proof-Irrelevance without +K_. [PDF](https://hal.inria.fr/hal-01859964v2/document) Page 1:10 mentions: From d54864327d364bb74897d72f4d65faf976d8ea11 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 21:23:56 -0500 Subject: [PATCH 04/28] sort: more on piDom --- base/src/main/java/org/aya/core/term/MetaTerm.java | 8 ++++++-- base/src/main/java/org/aya/tyck/unify/DoubleChecker.java | 6 +++--- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/base/src/main/java/org/aya/core/term/MetaTerm.java b/base/src/main/java/org/aya/core/term/MetaTerm.java index 4174e3404d..9a1474e72a 100644 --- a/base/src/main/java/org/aya/core/term/MetaTerm.java +++ b/base/src/main/java/org/aya/core/term/MetaTerm.java @@ -1,10 +1,10 @@ -// 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.term; import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; -import org.aya.core.Meta; +import org.aya.core.meta.Meta; import org.aya.util.Arg; import org.jetbrains.annotations.NotNull; @@ -31,6 +31,10 @@ public record MetaTerm( return ref.asPi(ref.name() + "dom", ref.name() + "cod", explicit, contextArgs); } + public @NotNull MetaTerm asPiDom(@NotNull Term result) { + return ref.asPiDom(result, contextArgs); + } + public @NotNull SeqView<@NotNull Arg> fullArgs() { return contextArgs.view().concat(args); } diff --git a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java index a868eadc55..1a83bfb831 100644 --- a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java +++ b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java @@ -61,9 +61,9 @@ case TupTerm(var items)when whnf(expected) instanceof SigmaTerm sigma -> { yield res != null && res.items().allMatch(i -> !(i.term() instanceof ErrorTerm)); } case PiTerm(var dom, var cod) -> { - var domSort = synthesizer.press(dom.type()); - // TODO[isType]: make sure the above is a type. Need an extra "isType" - yield unifier.ctx.with(dom, () -> inherit(cod, expected)); + if (!(expected instanceof SortTerm sort)) yield Synthesizer.unreachable(expected); + if (!synthesizer.inheritPiDom(dom.type(), sort)) yield false; + yield unifier.ctx.with(dom, () -> inherit(cod, sort)); } case default -> compare(synthesizer.press(preterm), expected, null); }; From ab4806f10921bf35650c24e2ace42fb20846a0af Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 22:27:05 -0500 Subject: [PATCH 05/28] sort: adapt some changes on `info` --- .../main/java/org/aya/core/meta/MetaInfo.java | 8 ++++++- .../main/java/org/aya/core/term/SortTerm.java | 5 ++++- .../main/java/org/aya/tyck/unify/Unifier.java | 7 ++++--- note/sort-system.md | 21 ++++++++++++------- 4 files changed, 28 insertions(+), 13 deletions(-) diff --git a/base/src/main/java/org/aya/core/meta/MetaInfo.java b/base/src/main/java/org/aya/core/meta/MetaInfo.java index f16a75577d..908a3bed36 100644 --- a/base/src/main/java/org/aya/core/meta/MetaInfo.java +++ b/base/src/main/java/org/aya/core/meta/MetaInfo.java @@ -4,6 +4,7 @@ import org.aya.core.term.Term; import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; /** * Constraints on a meta variable. @@ -11,6 +12,7 @@ * @author ice1000 */ public sealed interface MetaInfo { + @Nullable Term result(); /** * The type of the meta is known. * We shall check the solution against this type. @@ -21,5 +23,9 @@ record Result(@NotNull Term result) implements MetaInfo {} * The meta variable is a type. * It should be able to appear on the RHS of a judgment. */ - record AnyType() implements MetaInfo {} + record AnyType() implements MetaInfo { + @Override public @Nullable Term result() { + return null; + } + } } diff --git a/base/src/main/java/org/aya/core/term/SortTerm.java b/base/src/main/java/org/aya/core/term/SortTerm.java index 4c79fd4c81..e3c4cd9adc 100644 --- a/base/src/main/java/org/aya/core/term/SortTerm.java +++ b/base/src/main/java/org/aya/core/term/SortTerm.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.term; @@ -27,6 +27,9 @@ public SortTerm(@NotNull SortKind kind, int lift) { public static final @NotNull SortTerm ISet = new SortTerm(SortKind.ISet, 0); public static final @NotNull SortTerm Prop = new SortTerm(SortKind.Prop, 0); + /** + * Agda + */ public @NotNull SortTerm succ() { return switch (kind) { case Type, Set -> new SortTerm(kind, lift + 1); diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index df04844108..8746f14cb5 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -6,6 +6,7 @@ import kala.collection.mutable.MutableArrayList; import kala.control.Option; import org.aya.core.meta.Meta; +import org.aya.core.meta.MetaInfo; import org.aya.core.ops.Eta; import org.aya.core.term.*; import org.aya.core.visitor.DeltaExpander; @@ -88,7 +89,7 @@ protected Term solveMeta(@NotNull MetaTerm lhs, @NotNull Term preRhs, Sub lr, Su // Update: this is still needed, see #327 last task (`coe'`) var checker = new DoubleChecker(new Unifier(Ordering.Lt, reporter, false, false, traceBuilder, state, pos, ctx.deriveMap()), lr, rl); - var expectedType = meta.result; + var expectedType = meta.info.result(); if (expectedType == null) expectedType = providedType; else if (providedType != null) { // The provided type from the context, hence neither from LHS nor RHS, @@ -171,8 +172,8 @@ else if (providedType != null) { private @NotNull Option<@Nullable Term> sameMeta(Sub lr, Sub rl, @NotNull MetaTerm lhs, Meta meta, Term preRhs) { if (!(preRhs instanceof MetaTerm rcall && meta == rcall.ref())) return Option.none(); // If we do not know the type, then we do not perform the comparison - if (meta.result == null) return Option.some(null); - var holeTy = PiTerm.make(meta.telescope, meta.result); + if (!(meta.info instanceof MetaInfo.Result(var result))) return Option.some(null); + var holeTy = PiTerm.make(meta.telescope, result); for (var arg : lhs.args().zipView(rcall.args())) { if (!(holeTy instanceof PiTerm holePi)) throw new InternalException("meta arg size larger than param size. this should not happen"); diff --git a/note/sort-system.md b/note/sort-system.md index 4cc36772b0..9f7fe225ab 100644 --- a/note/sort-system.md +++ b/note/sort-system.md @@ -10,17 +10,22 @@ Comments: Related rules on the $\Pi$-type: -| Input sort | Output sort | Sort | -|------------|--------------|------------------| -| `Prop` a | `Type` b | `Type` a ∨ b | -| `Type` a | `Prop` b | `Prop` a ∨ b | -| `?` a | `?` b (same) | `?` a ∨ b (same) | -| `?` a | `¿` b | `Set` a ∨ b | +| Input sort | Output sort | Result | +|-----------------|--------------|------------------| +| `Prop`/`Type` a | `Type` b | `Type` a ∨ b | +| `Prop`/`Type` a | `Prop` b | `Prop` a ∨ b | +| `?` a | `?` b (same) | `?` a ∨ b (same) | +| `?` a | `¿` b | `Set` a ∨ b | # Notes -+ If sort is not `Set`, then cod's sort is just `<=` the result sort and should have the same kind. -+ If sort is `Set`, then cod's sort is `<=` the result sort and can be any kind. ++ Codomain's sort: + + If result is not `Set`: just `<=` the result sort and should have the same kind. + + If result is `Set`, then can be any kind with suitable levels. ++ Domain's sort: + + If result is `Prop`/`Type`, then can be `Prop`/`Type` with suitable levels. + + If result is `Set`, then can be anything. + + If result is `Type`, then can be anything except `Set`/`ISet`. # Regarding impredicativity From d276146870c866fc8c82d41132fdc5a15490d89a Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 22:28:25 -0500 Subject: [PATCH 06/28] sort: adapt more changes on `info` --- base/src/main/java/org/aya/tyck/error/Goal.java | 7 ++++--- base/src/main/java/org/aya/tyck/unify/TermComparator.java | 4 ++-- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/error/Goal.java b/base/src/main/java/org/aya/tyck/error/Goal.java index 1aacd61679..965fc5016b 100644 --- a/base/src/main/java/org/aya/tyck/error/Goal.java +++ b/base/src/main/java/org/aya/tyck/error/Goal.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.tyck.error; @@ -9,8 +9,8 @@ import org.aya.pretty.doc.Doc; import org.aya.ref.LocalVar; import org.aya.tyck.tycker.TyckState; -import org.aya.util.prettier.PrettierOptions; import org.aya.util.error.SourcePos; +import org.aya.util.prettier.PrettierOptions; import org.aya.util.reporter.Problem; import org.jetbrains.annotations.NotNull; @@ -21,7 +21,8 @@ public record Goal( ) implements Problem { @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { var meta = hole.ref(); - var result = meta.result != null ? meta.result.freezeHoles(state) + var nullableResult = meta.info.result(); + var result = nullableResult != null ? nullableResult.freezeHoles(state) : new ErrorTerm(Doc.plain("???"), false); var doc = Doc.vcatNonEmpty( Doc.english("Goal of type"), diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java index cf2b4a88d2..d68a7447c5 100644 --- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java +++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.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.tyck.unify; @@ -131,7 +131,7 @@ protected final boolean compare(Term lhs, Term rhs, Sub lr, Sub rl, @Nullable Te if (rhs instanceof MetaTerm rMeta) { // In case we're comparing two metas with one isType and the other has a type, // prefer solving the isType one to the typed one. - if (lhs instanceof MetaTerm lMeta && lMeta.ref().result == null) + if (lhs instanceof MetaTerm lMeta && lMeta.ref().info.result() == null) return solveMeta(lMeta, rMeta, lr, rl, type) != null; return solveMeta(rMeta, lhs, rl, lr, type) != null; } From 49a0b83186a3823d275f5a046eb07fecffe60ecd Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 23:24:35 -0500 Subject: [PATCH 07/28] sort: `inheritPiDom` --- .../main/java/org/aya/core/term/PiTerm.java | 13 ++++----- .../java/org/aya/tyck/unify/Synthesizer.java | 29 ++++++++++++++++--- .../org/aya/tyck/unify/TermComparator.java | 1 + note/sort-system.md | 3 +- 4 files changed, 32 insertions(+), 14 deletions(-) diff --git a/base/src/main/java/org/aya/core/term/PiTerm.java b/base/src/main/java/org/aya/core/term/PiTerm.java index e1934707c1..e2cbd582ba 100644 --- a/base/src/main/java/org/aya/core/term/PiTerm.java +++ b/base/src/main/java/org/aya/core/term/PiTerm.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.term; @@ -11,7 +11,6 @@ import org.aya.tyck.Result; import org.aya.util.Arg; import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; import java.util.function.UnaryOperator; @@ -62,7 +61,7 @@ case PiTerm(var param, var body)when param.explicit() -> { }; } - public static @Nullable SortTerm max(@NotNull SortTerm domain, @NotNull SortTerm codomain) { + public static @NotNull SortTerm max(@NotNull SortTerm domain, @NotNull SortTerm codomain) { var alift = domain.lift(); var blift = codomain.lift(); return switch (domain.kind()) { @@ -72,18 +71,16 @@ case PiTerm(var param, var body)when param.explicit() -> { case Prop -> codomain; }; case ISet -> switch (codomain.kind()) { - case ISet -> SortTerm.Set0; + case ISet, Prop -> SortTerm.Set0; case Set, Type -> codomain; - default -> null; }; case Set -> switch (codomain.kind()) { case Set, Type -> new SortTerm(SortKind.Set, Math.max(alift, blift)); - case ISet -> new SortTerm(SortKind.Set, alift); - default -> null; + case ISet, Prop -> new SortTerm(SortKind.Set, alift); }; case Prop -> switch (codomain.kind()) { case Prop, Type -> codomain; - default -> null; + default -> new SortTerm(SortKind.Set, blift); }; }; } diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java index 1a51c324ec..aa1e6fa289 100644 --- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -6,6 +6,7 @@ import kala.collection.mutable.MutableList; import org.aya.core.def.Def; import org.aya.core.def.PrimDef; +import org.aya.core.meta.MetaInfo; import org.aya.core.term.*; import org.aya.core.visitor.DeltaExpander; import org.aya.core.visitor.Subst; @@ -32,6 +33,27 @@ public record Synthesizer(@NotNull TyckState state, @NotNull LocalCtx ctx) { return whnf(synthesize); } + public boolean inheritPiDom(Term type, SortTerm expected) { + if (type instanceof MetaTerm meta && meta.ref().info instanceof MetaInfo.AnyType) { + var typed = meta.asPiDom(expected); + state.solve(meta.ref(), typed); + return false; + } + if (!(synthesize(type) instanceof SortTerm actual)) return false; + return switch (expected.kind()) { + case Prop -> switch (actual.kind()) { + case Prop, Type -> true; + case Set, ISet -> false; + }; + case Type -> switch (actual.kind()) { + case Prop, Type -> actual.lift() <= expected.lift(); + case Set, ISet -> false; + }; + case Set -> actual.lift() <= expected.lift(); + case ISet -> unreachable(type); + }; + } + public @Nullable Term synthesize(@NotNull Term preterm) { return switch (preterm) { case RefTerm term -> ctx.get(term.var()); @@ -41,8 +63,8 @@ public record Synthesizer(@NotNull TyckState state, @NotNull LocalCtx ctx) { .lift(call.ulift()); // TODO[isType]: deal with type-only metas case MetaTerm hole -> { - var result = hole.ref().result; - if (result != null) yield result; + var info = hole.ref().info; + if (info instanceof MetaInfo.Result(var result)) yield result; var simpl = whnf(hole); if (simpl instanceof MetaTerm again) { throw new UnsupportedOperationException("TODO"); @@ -134,12 +156,11 @@ case InTerm(var phi, var u) -> { }; } - private static T unreachable(@NotNull Term preterm) { + static T unreachable(@NotNull Term preterm) { throw new AssertionError("Unexpected term: " + preterm); } private @NotNull Term whnf(Term x) { return x.normalize(state, NormalizeMode.WHNF); } - } diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java index d68a7447c5..9cd2534e2a 100644 --- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java +++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java @@ -249,6 +249,7 @@ private boolean visitLists(SeqView l, SeqView r, Sub lr, Sub rl, @No else return null; } + /** TODO: Revise when JDK 20 is released. */ private record Pair(Term lhs, Term rhs) {} private @NotNull Term getType(@NotNull Callable lhs, @NotNull DefVar> lhsRef) { diff --git a/note/sort-system.md b/note/sort-system.md index 9f7fe225ab..6d8f99cdfe 100644 --- a/note/sort-system.md +++ b/note/sort-system.md @@ -24,8 +24,7 @@ Related rules on the $\Pi$-type: + If result is `Set`, then can be any kind with suitable levels. + Domain's sort: + If result is `Prop`/`Type`, then can be `Prop`/`Type` with suitable levels. - + If result is `Set`, then can be anything. - + If result is `Type`, then can be anything except `Set`/`ISet`. + + If result is `Set`, then can be anything with suitable levels. # Regarding impredicativity From 57c3949858d3bd963e80dc22acca3810b4a2fa05 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 23:31:45 -0500 Subject: [PATCH 08/28] sort: recover piDom check --- base/src/main/java/org/aya/tyck/StmtTycker.java | 8 +++----- .../java/org/aya/tyck/error/UnifyError.java | 17 ++++++++++++++++- .../java/org/aya/tyck/tycker/MockedTycker.java | 7 ++++++- 3 files changed, 25 insertions(+), 7 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index dcdbce9f74..c30690ded2 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.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.tyck; @@ -28,7 +28,6 @@ import org.aya.tyck.trace.Trace; import org.aya.tyck.tycker.TracedTycker; import org.aya.util.Arg; -import org.aya.util.Ordering; import org.aya.util.TreeBuilder; import org.aya.util.error.SourcePos; import org.aya.util.reporter.Reporter; @@ -337,9 +336,8 @@ private record TeleResult(@NotNull Term.Param param, @NotNull SourcePos pos) {} */ private @NotNull Term checkTele(@NotNull ExprTycker exprTycker, @NotNull Expr tele, @NotNull SortTerm sort) { var result = exprTycker.ty(tele); - var unifier = exprTycker.unifier(tele.sourcePos(), Ordering.Lt); - // TODO[isType]: there is no restriction on constructor telescope now - // new DoubleChecker(unifier).inherit(result, sort); + if (!exprTycker.synthesizer().inheritPiDom(result, sort)) + reporter.report(new UnifyError.PiDom(tele, result, sort)); return result; } diff --git a/base/src/main/java/org/aya/tyck/error/UnifyError.java b/base/src/main/java/org/aya/tyck/error/UnifyError.java index 550b1bb2ec..3d7f61642b 100644 --- a/base/src/main/java/org/aya/tyck/error/UnifyError.java +++ b/base/src/main/java/org/aya/tyck/error/UnifyError.java @@ -1,9 +1,11 @@ -// 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.tyck.error; import org.aya.concrete.Expr; import org.aya.concrete.stmt.TeleDecl; +import org.aya.core.term.SortTerm; +import org.aya.core.term.Term; import org.aya.generic.ExprProblem; import org.aya.pretty.doc.Doc; import org.aya.util.error.SourcePos; @@ -42,4 +44,17 @@ record ConReturn( return info.describeUnify(options, comparison, prologue, Doc.english("while it should return")); } } + + record PiDom( + @Override @NotNull Expr expr, + Term result, SortTerm sort + ) implements UnifyError, ExprProblem { + @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { + return Doc.vcat( + Doc.english("The type"), + Doc.par(1, result.toDoc(options)), + Doc.english("is in the domain of a function whose type is"), + Doc.par(1, sort.toDoc(options))); + } + } } diff --git a/base/src/main/java/org/aya/tyck/tycker/MockedTycker.java b/base/src/main/java/org/aya/tyck/tycker/MockedTycker.java index 0bd3bc43d3..e079f2e0b6 100644 --- a/base/src/main/java/org/aya/tyck/tycker/MockedTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/MockedTycker.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.tyck.tycker; @@ -13,6 +13,7 @@ import org.aya.tyck.env.MapLocalCtx; import org.aya.tyck.pat.TypedSubst; import org.aya.tyck.trace.Trace; +import org.aya.tyck.unify.Synthesizer; import org.aya.tyck.unify.Unifier; import org.aya.util.Arg; import org.aya.util.Ordering; @@ -46,6 +47,10 @@ protected MockedTycker(@NotNull Reporter reporter, Trace.@Nullable Builder trace return unifier(pos, ord, localCtx); } + public @NotNull Synthesizer synthesizer() { + return new Synthesizer(state, localCtx); + } + protected final @NotNull Term mockTerm(Term.Param param, SourcePos pos) { // TODO: maybe we should create a concrete hole and check it against the type // in case we can synthesize this term via its type only From 0f90e620119c46e3566d10cdf839856021f4b15c Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 23:39:18 -0500 Subject: [PATCH 09/28] sort: allow `ISet` --- base/src/main/java/org/aya/tyck/unify/DoubleChecker.java | 2 +- base/src/main/java/org/aya/tyck/unify/Synthesizer.java | 6 ++---- note/sort-system.md | 2 ++ 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java index 1a83bfb831..44e2c0ca63 100644 --- a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java +++ b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java @@ -61,7 +61,7 @@ case TupTerm(var items)when whnf(expected) instanceof SigmaTerm sigma -> { yield res != null && res.items().allMatch(i -> !(i.term() instanceof ErrorTerm)); } case PiTerm(var dom, var cod) -> { - if (!(expected instanceof SortTerm sort)) yield Synthesizer.unreachable(expected); + if (!(whnf(expected) instanceof SortTerm sort)) yield Synthesizer.unreachable(expected); if (!synthesizer.inheritPiDom(dom.type(), sort)) yield false; yield unifier.ctx.with(dom, () -> inherit(cod, sort)); } diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java index aa1e6fa289..bcc8236ecf 100644 --- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -10,6 +10,7 @@ import org.aya.core.term.*; import org.aya.core.visitor.DeltaExpander; import org.aya.core.visitor.Subst; +import org.aya.generic.SortKind; import org.aya.generic.util.InternalException; import org.aya.generic.util.NormalizeMode; import org.aya.guest0x0.cubical.Partial; @@ -45,10 +46,7 @@ public boolean inheritPiDom(Term type, SortTerm expected) { case Prop, Type -> true; case Set, ISet -> false; }; - case Type -> switch (actual.kind()) { - case Prop, Type -> actual.lift() <= expected.lift(); - case Set, ISet -> false; - }; + case Type -> actual.kind() != SortKind.Set && actual.lift() <= expected.lift(); case Set -> actual.lift() <= expected.lift(); case ISet -> unreachable(type); }; diff --git a/note/sort-system.md b/note/sort-system.md index 6d8f99cdfe..f47a21b823 100644 --- a/note/sort-system.md +++ b/note/sort-system.md @@ -13,6 +13,7 @@ Related rules on the $\Pi$-type: | Input sort | Output sort | Result | |-----------------|--------------|------------------| | `Prop`/`Type` a | `Type` b | `Type` a ∨ b | +| `ISet` | `Type` b | `Type` b | | `Prop`/`Type` a | `Prop` b | `Prop` a ∨ b | | `?` a | `?` b (same) | `?` a ∨ b (same) | | `?` a | `¿` b | `Set` a ∨ b | @@ -24,6 +25,7 @@ Related rules on the $\Pi$-type: + If result is `Set`, then can be any kind with suitable levels. + Domain's sort: + If result is `Prop`/`Type`, then can be `Prop`/`Type` with suitable levels. + + If result is `Type`, then can be `ISet`. + If result is `Set`, then can be anything with suitable levels. # Regarding impredicativity From 2ddedeb27748554cdf8399ca8954570ce4ea84df Mon Sep 17 00:00:00 2001 From: ice1000 Date: Thu, 5 Jan 2023 23:53:20 -0500 Subject: [PATCH 10/28] sort: allow `ISet` --- base/src/main/java/org/aya/tyck/unify/DoubleChecker.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java index 44e2c0ca63..cba5bd900a 100644 --- a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java +++ b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java @@ -32,6 +32,14 @@ public DoubleChecker(@NotNull Unifier unifier, @NotNull Sub lr, @NotNull Sub rl) } public boolean inherit(@NotNull Term preterm, @NotNull Term expected) { + if (expected instanceof MetaTerm) { + var lhs = synthesizer().synthesize(preterm); + if (lhs == null) { + assert false : "No rules -- unsure if reachable"; + return false; + } + return compare(lhs, expected, null); + } return switch (preterm) { case ErrorTerm term -> true; case SigmaTerm sigma -> sigma.params().view() From a5b4c09088590760ba0a9cf84672974b6bde1bf0 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 04:54:57 +0000 Subject: [PATCH 11/28] tests: update fixture (finally\!) --- .../resources/failure/levels/too-high.aya.txt | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/base/src/test/resources/failure/levels/too-high.aya.txt b/base/src/test/resources/failure/levels/too-high.aya.txt index 2a2a95b701..5a7b64cdd3 100644 --- a/base/src/test/resources/failure/levels/too-high.aya.txt +++ b/base/src/test/resources/failure/levels/too-high.aya.txt @@ -1 +1,14 @@ -That looks right! +In file $FILE:3:8 -> + + 1 │ data List (A : Type 1) : Type 0 + 2 │ | nil + 3 │ | cons A (List A) + │ ╰╯ + +Error: The type + A + is in the domain of a function whose type is + Type 0 + +1 error(s), 0 warning(s). +What are you doing? From 238e14c2faba31db4eea435ea1a48fc4266fa9ff Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 00:19:03 -0500 Subject: [PATCH 12/28] tycker: rename `localCtx` to `ctx` --- .../main/java/org/aya/tyck/ExprTycker.java | 32 +++++++++---------- .../main/java/org/aya/tyck/StmtTycker.java | 12 +++---- .../java/org/aya/tyck/pat/ClauseTycker.java | 10 +++--- .../java/org/aya/tyck/pat/PatClassifier.java | 4 +-- .../java/org/aya/tyck/pat/PatternTycker.java | 4 +-- .../org/aya/tyck/tycker/MockedTycker.java | 18 +++++------ .../java/org/aya/tyck/tycker/PropTycker.java | 2 +- .../org/aya/tyck/tycker/UnifiedTycker.java | 4 +-- 8 files changed, 43 insertions(+), 43 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java index c01d7f7297..2813004590 100644 --- a/base/src/main/java/org/aya/tyck/ExprTycker.java +++ b/base/src/main/java/org/aya/tyck/ExprTycker.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.tyck; @@ -61,7 +61,7 @@ public final class ExprTycker extends PropTycker { case Expr.Lambda lam when lam.param().type() instanceof Expr.Hole -> inherit(lam, generatePi(lam)); case Expr.Lambda lam -> { var paramTy = ty(lam.param().type()); - yield localCtx.with(lam.param().ref(), paramTy, () -> { + yield ctx.with(lam.param().ref(), paramTy, () -> { var body = synthesize(lam.body()); var param = new Term.Param(lam.param(), paramTy); var pi = new PiTerm(param, body.type()).freezeHoles(state).rename(); @@ -77,7 +77,7 @@ public final class ExprTycker extends PropTycker { .getOption(loc) // automatically unfold .getOrElse(() -> { // not defined in definitionEqualities, search localCtx - var ty = localCtx.get(loc); + var ty = ctx.get(loc); return new Result.Default(new RefTerm(loc), ty); }); case DefVar defVar -> inferRef(defVar); @@ -85,11 +85,11 @@ public final class ExprTycker extends PropTycker { }; case Expr.Pi pi -> { var corePi = ty(pi); - yield new Result.Default(corePi, corePi.computeType(state, localCtx)); + yield new Result.Default(corePi, corePi.computeType(state, ctx)); } case Expr.Sigma sigma -> { var coreSigma = ty(sigma); - yield new Result.Default(coreSigma, coreSigma.computeType(state, localCtx)); + yield new Result.Default(coreSigma, coreSigma.computeType(state, ctx)); } case Expr.Lift lift -> { var result = synthesize(lift.expr()); @@ -276,7 +276,7 @@ public final class ExprTycker extends PropTycker { // Anyway, the `Term.descent` will recurse into the `Cube` for `PathApp` and substitute the partial element. yield new Result.Default(newApp, pi.body().subst(subst)); } - case Expr.Hole hole -> inherit(hole, localCtx.freshTyHole(Constants.randomName(hole), hole.sourcePos()).component2()); + case Expr.Hole hole -> inherit(hole, ctx.freshTyHole(Constants.randomName(hole), hole.sourcePos()).component2()); case Expr.Error err -> Result.Default.error(err.description()); case Expr.LitInt lit -> { int integer = lit.integer(); @@ -284,7 +284,7 @@ public final class ExprTycker extends PropTycker { var defs = shapeFactory.findImpl(AyaShape.NAT_SHAPE); if (defs.isEmpty()) yield fail(expr, new NoRuleError(expr, null)); if (defs.sizeGreaterThan(1)) { - var type = localCtx.freshTyHole("_ty" + lit.integer() + "'", lit.sourcePos()); + var type = ctx.freshTyHole("_ty" + lit.integer() + "'", lit.sourcePos()); yield new Result.Default(new MetaLitTerm(lit.sourcePos(), lit.integer(), defs, type.component1()), type.component1()); } var match = defs.first(); @@ -297,7 +297,7 @@ public final class ExprTycker extends PropTycker { yield new Result.Default(new StringTerm(litStr.string()), state.primFactory().getCall(PrimDef.ID.STRING)); } - case Expr.Path path -> localCtx.withIntervals(path.params().view(), () -> { + case Expr.Path path -> ctx.withIntervals(path.params().view(), () -> { var type = synthesize(path.type()); var partial = elaboratePartial(path.partial(), type.wellTyped()); var cube = new PathTerm(path.params(), type.wellTyped(), partial); @@ -320,7 +320,7 @@ public final class ExprTycker extends PropTycker { // preparing var dataParam = Def.defTele(def.ref).first(); var sort = dataParam.type(); // the sort of type below. - var hole = localCtx.freshHole(sort, arr.sourcePos()); + var hole = ctx.freshHole(sort, arr.sourcePos()); var type = new DataCall(def.ref(), 0, ImmutableSeq.of( new Arg<>(hole.component1(), dataParam.explicit()))); @@ -447,7 +447,7 @@ public NotPi(@NotNull Term what) { } case Expr.Hole hole -> { // TODO[ice]: deal with unit type - var freshHole = localCtx.freshHole(term, Constants.randomName(hole), hole.sourcePos()); + var freshHole = ctx.freshHole(term, Constants.randomName(hole), hole.sourcePos()); if (hole.explicit()) reporter.report(new Goal(state, freshHole.component1(), hole.accessibleLocal().get())); yield new Result.Default(freshHole.component2(), term); } @@ -473,7 +473,7 @@ yield switch (whnf(term)) { addWithTerm(param, type); var resultParam = new Term.Param(var, type, param.explicit()); var body = dt.substBody(resultParam.toTerm()); - yield localCtx.with(resultParam, () -> { + yield ctx.with(resultParam, () -> { var rec = check(lam.body(), body); return new Result.Default(new LamTerm(LamTerm.param(resultParam), rec.wellTyped()), dt); }); @@ -515,7 +515,7 @@ yield switch (whnf(term)) { private @NotNull Term doTy(@NotNull Expr expr) { return switch (expr) { case Expr.Hole hole -> { - var freshHole = localCtx.freshTyHole(Constants.randomName(hole), hole.sourcePos()); + var freshHole = ctx.freshTyHole(Constants.randomName(hole), hole.sourcePos()); if (hole.explicit()) reporter.report(new Goal(state, freshHole.component1(), hole.accessibleLocal().get())); yield freshHole.component2(); } @@ -526,7 +526,7 @@ yield switch (whnf(term)) { var domRes = ty(param.type()); addWithTerm(param, domRes); var resultParam = new Term.Param(var, domRes, param.explicit()); - yield localCtx.with(resultParam, () -> new PiTerm(resultParam, ty(pi.last()))); + yield ctx.with(resultParam, () -> new PiTerm(resultParam, ty(pi.last()))); } case Expr.Sigma sigma -> { var resultTele = MutableList.>create(); @@ -534,10 +534,10 @@ yield switch (whnf(term)) { var result = ty(tuple.type()); addWithTerm(tuple, result); var ref = tuple.ref(); - localCtx.put(ref, result); + ctx.put(ref, result); resultTele.append(Tuple.of(ref, tuple.explicit(), result)); } - localCtx.remove(sigma.params().view().map(Expr.Param::ref)); + ctx.remove(sigma.params().view().map(Expr.Param::ref)); yield new SigmaTerm(Term.Param.fromBuffer(resultTele)); } default -> synthesize(expr).wellTyped(); @@ -571,7 +571,7 @@ public ExprTycker(@NotNull PrimDef.Factory primFactory, @NotNull AyaShape.Factor return traced(() -> new Trace.ExprT(expr, type.freezeHoles(state)), expr, e -> { if (type instanceof PiTerm pi && !pi.param().explicit() && needImplicitParamIns(e)) { var implicitParam = new Term.Param(new LocalVar(Constants.ANONYMOUS_PREFIX), pi.param().type(), false); - var body = localCtx.with(implicitParam, () -> inherit(e, pi.substBody(implicitParam.toTerm()))).wellTyped(); + var body = ctx.with(implicitParam, () -> inherit(e, pi.substBody(implicitParam.toTerm()))).wellTyped(); return new Result.Default(new LamTerm(LamTerm.param(implicitParam), body), pi); } else return doInherit(e, type); }); diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index c30690ded2..97e091bd5a 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.java @@ -198,7 +198,7 @@ public void tyckHeader(@NotNull Decl decl, @NotNull ExprTycker tycker) { case TeleDecl.PrimDecl prim -> { // This directly corresponds to the tycker.localCtx = new LocalCtx(); // at the end of this case clause. - assert tycker.localCtx.isEmpty(); + assert tycker.ctx.isEmpty(); var core = prim.ref.core; var tele = tele(tycker, prim.telescope, null); if (tele.isNotEmpty()) { @@ -219,7 +219,7 @@ public void tyckHeader(@NotNull Decl decl, @NotNull ExprTycker tycker) { tycker.unifyTyReported(result, core.result, prim.result); } else prim.signature = new Def.Signature<>(core.telescope, core.result); tycker.solveMetas(); - tycker.localCtx = new SeqLocalCtx(); + tycker.ctx = new SeqLocalCtx(); } case TeleDecl.DataCtor ctor -> checkCtor(tycker, ctor); case TeleDecl.StructField field -> { @@ -255,7 +255,7 @@ private void checkCtor(@NotNull ExprTycker tycker, TeleDecl.DataCtor ctor) { new Pattern.Clause(ctor.sourcePos, ctor.patterns, Option.none()), sig, false, false); pat = lhs.preclause().patterns(); // Revert to the "after patterns" state - tycker.localCtx = lhs.gamma(); + tycker.ctx = lhs.gamma(); tycker.definitionEqualities = lhs.bodySubst(); predataCall = (DataCall) predataCall.subst(new Subst( dataSig.param().view().map(Term.Param::ref), @@ -307,7 +307,7 @@ private void checkCtor(@NotNull ExprTycker tycker, TeleDecl.DataCtor ctor) { } private static void loadTele(@NotNull ExprTycker tycker, Def.Signature dataSig) { - dataSig.param().forEach(tycker.localCtx::put); + dataSig.param().forEach(tycker.ctx::put); } private SortTerm resultTy(@NotNull ExprTycker tycker, TeleDecl data) { @@ -352,7 +352,7 @@ private record TeleResult(@NotNull Term.Param param, @NotNull SourcePos pos) {} : exprTycker.ty(param.type()) ); var newParam = new Term.Param(param, paramTyped); - exprTycker.localCtx.put(newParam); + exprTycker.ctx.put(newParam); exprTycker.addWithTerm(param, paramTyped); return new TeleResult(newParam, param.sourcePos()); }); @@ -364,7 +364,7 @@ private record TeleResult(@NotNull Term.Param param, @NotNull SourcePos pos) {} return okTele.map(tt -> { var rawParam = tt.param; var param = new Term.Param(rawParam, zonker.apply(rawParam.type())); - exprTycker.localCtx.put(param); + exprTycker.ctx.put(param); return param; }); } 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 a76c3bb310..2bc39a2b5c 100644 --- a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java +++ b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java @@ -74,7 +74,7 @@ public record PatResult( ) { // TODO[isType]: revise this // https://github.com/agda/agda/blob/66d22577abe9ac67649c6e662c91d8593d1bf86c/src/full/Agda/TypeChecking/Rules/LHS.hs#L2099-L2136 - var inProp = exprTycker.localCtx.with(() -> + var inProp = exprTycker.ctx.with(() -> exprTycker.isPropType(signature.result()), signature.param().view()); return new AllLhsResult(clauses.mapIndexed((index, clause) -> exprTycker.traced( () -> new Trace.LabelT(clause.sourcePos, "lhs of clause " + (1 + index)), @@ -142,11 +142,11 @@ public record LhsResult( match.hasError |= patTycker.hasError(); - var patterns = step0.wellTyped().map(p -> p.descent(x -> x.inline(exprTycker.localCtx))); + var patterns = step0.wellTyped().map(p -> p.descent(x -> x.inline(exprTycker.ctx))); // inline after inline patterns inlineTypedSubst(patTycker.bodySubst); var type = inlineTerm(step0.codomain()); - exprTycker.localCtx.modifyMyTerms(META_PAT_INLINER); + exprTycker.ctx.modifyMyTerms(META_PAT_INLINER); var consumer = new PatternConsumer() { @Override public void pre(@NotNull Pattern pat) { var typeRef = switch (pat) { @@ -162,14 +162,14 @@ public record LhsResult( }; match.patterns.view().map(Arg::term).forEach(consumer::accept); - return new LhsResult(exprTycker.localCtx, type, patTycker.bodySubst, patTycker.hasError(), + return new LhsResult(exprTycker.ctx, type, patTycker.bodySubst, patTycker.hasError(), new Pat.Preclause<>(match.sourcePos, patterns, Option.ofNullable(step0.newBody()))); }); } private static Pat.Preclause checkRhs(@NotNull ExprTycker exprTycker, @NotNull LhsResult lhsResult) { return exprTycker.subscoped(() -> { - exprTycker.localCtx = lhsResult.gamma; + exprTycker.ctx = lhsResult.gamma; var term = exprTycker.subscoped(() -> { // We `addDirectly` to `definitionEqualities`. // This means terms in `definitionEqualities` won't be substituted by `lhsResult.bodySubst` diff --git a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java b/base/src/main/java/org/aya/tyck/pat/PatClassifier.java index a1a410f732..6c0af32ff9 100644 --- a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java +++ b/base/src/main/java/org/aya/tyck/pat/PatClassifier.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.tyck.pat; @@ -106,7 +106,7 @@ public static void confluence( var lhsSubst = new Subst(MutableMap.create()); var rhsSubst = new Subst(MutableMap.create()); var ctx = PatUnify.unifyPat(lhsInfo.component2().patterns().map(Arg::term), rhsInfo.component2().patterns().map(Arg::term), - lhsSubst, rhsSubst, tycker.localCtx.deriveMap()); + lhsSubst, rhsSubst, tycker.ctx.deriveMap()); domination(ctx, rhsSubst, tycker.reporter, lhsInfo.component1(), rhsInfo.component1(), rhsInfo.component2()); domination(ctx, lhsSubst, tycker.reporter, rhsInfo.component1(), lhsInfo.component1(), lhsInfo.component2()); var lhsTerm = lhsInfo.component2().body().subst(lhsSubst); 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 e7ef7c6cd0..453e322aa3 100644 --- a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java +++ b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java @@ -106,7 +106,7 @@ public PatternTycker(@NotNull ExprTycker exprTycker, yield new Pat.Ctor(realCtor.component3().ref(), patterns, dataCall); } case Pattern.Bind(var pos, var bind, var tyExpr, var tyRef) -> { - exprTycker.localCtx.put(bind, term); + exprTycker.ctx.put(bind, term); if (tyExpr != null) exprTycker.subscoped(() -> { exprTycker.definitionEqualities.addDirectly(bodySubst); var syn = exprTycker.synthesize(tyExpr); @@ -289,7 +289,7 @@ private void generatePat() { bind = new Pat.Meta(MutableValue.create(), freshVar, dataCall); } else { bind = new Pat.Bind(freshVar, currParam.type()); - exprTycker.localCtx.put(freshVar, currParam.type()); + exprTycker.ctx.put(freshVar, currParam.type()); } wellTyped.append(new Arg<>(bind, false)); addSigSubst(currParam, bind); diff --git a/base/src/main/java/org/aya/tyck/tycker/MockedTycker.java b/base/src/main/java/org/aya/tyck/tycker/MockedTycker.java index e079f2e0b6..843647b172 100644 --- a/base/src/main/java/org/aya/tyck/tycker/MockedTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/MockedTycker.java @@ -36,7 +36,7 @@ * @see #subscoped(Supplier) */ public abstract sealed class MockedTycker extends ConcreteAwareTycker permits UnifiedTycker { - public @NotNull LocalCtx localCtx = new MapLocalCtx(); + public @NotNull LocalCtx ctx = new MapLocalCtx(); public @NotNull TypedSubst definitionEqualities = new TypedSubst(); protected MockedTycker(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuilder, @NotNull TyckState state) { @@ -44,18 +44,18 @@ protected MockedTycker(@NotNull Reporter reporter, Trace.@Nullable Builder trace } public @NotNull Unifier unifier(@NotNull SourcePos pos, @NotNull Ordering ord) { - return unifier(pos, ord, localCtx); + return unifier(pos, ord, ctx); } public @NotNull Synthesizer synthesizer() { - return new Synthesizer(state, localCtx); + return new Synthesizer(state, ctx); } protected final @NotNull Term mockTerm(Term.Param param, SourcePos pos) { // TODO: maybe we should create a concrete hole and check it against the type // in case we can synthesize this term via its type only var genName = param.ref().name().concat(Constants.GENERATED_POSTFIX); - return localCtx.freshHole(param.type(), genName, pos).component2(); + return ctx.freshHole(param.type(), genName, pos).component2(); } protected final @NotNull Arg mockArg(Term.Param param, SourcePos pos) { @@ -70,8 +70,8 @@ protected MockedTycker(@NotNull Reporter reporter, Trace.@Nullable Builder trace private @NotNull Term generatePi(@NotNull SourcePos pos, @NotNull String name, boolean explicit) { var genName = name + Constants.GENERATED_POSTFIX; // [ice]: unsure if ZERO is good enough - var domain = localCtx.freshTyHole(genName + "ty", pos).component2(); - var codomain = localCtx.freshTyHole(genName + "ret", pos).component2(); + var domain = ctx.freshTyHole(genName + "ty", pos).component2(); + var codomain = ctx.freshTyHole(genName + "ret", pos).component2(); return new PiTerm(new Term.Param(new LocalVar(genName, pos), domain, explicit), codomain); } @@ -87,16 +87,16 @@ protected final Result instImplicits(@NotNull Result result, @NotNull SourcePos } public R subscoped(@NotNull Supplier action) { - var parentCtx = this.localCtx; + var parentCtx = this.ctx; var parentSubst = this.definitionEqualities; - this.localCtx = parentCtx.deriveMap(); + this.ctx = parentCtx.deriveMap(); this.definitionEqualities = parentSubst.derive(); var result = action.get(); this.definitionEqualities = parentSubst; - this.localCtx = parentCtx; + this.ctx = parentCtx; return result; } diff --git a/base/src/main/java/org/aya/tyck/tycker/PropTycker.java b/base/src/main/java/org/aya/tyck/tycker/PropTycker.java index 3f883fbb3c..14dabb730f 100644 --- a/base/src/main/java/org/aya/tyck/tycker/PropTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/PropTycker.java @@ -43,7 +43,7 @@ protected final T withInProp(boolean inProp, @NotNull Supplier supplier) } public boolean isPropType(@NotNull Term type) { - var sort = new Synthesizer(state, localCtx).synthesize(type); + var sort = new Synthesizer(state, ctx).synthesize(type); if (sort == null) throw new UnsupportedOperationException("Zaoqi"); sort = whnf(sort); if (sort instanceof MetaTerm meta) { diff --git a/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java b/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java index d60d7a49ce..d14ea52686 100644 --- a/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java @@ -137,7 +137,7 @@ public boolean unifyReported( @NotNull Term lhs, @NotNull Term rhs, @NotNull Term ty, Expr loc, Function p ) { - return unifyReported(lhs, rhs, ty, loc.sourcePos(), localCtx, p); + return unifyReported(lhs, rhs, ty, loc.sourcePos(), ctx, p); } protected final void confluence(@NotNull ImmutableSeq> clauses, @NotNull Expr loc, @NotNull Term type) { @@ -152,7 +152,7 @@ protected final void confluence(@NotNull ImmutableSeq> clauses, protected final Result.Default checkBoundaries(Expr expr, PathTerm path, Subst subst, Term lambda) { var applied = path.applyDimsTo(lambda); - return localCtx.withIntervals(path.params().view(), () -> { + return ctx.withIntervals(path.params().view(), () -> { var happy = switch (path.partial()) { case Partial.Const sad -> boundary(expr, applied, sad.u(), path.type(), subst); case Partial.Split hap -> hap.clauses().allMatch(c -> From 8c563d5795227564b0d0721db482bdb30d40f815 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 00:31:39 -0500 Subject: [PATCH 13/28] tycker: split `MockTycker` with `LetListTycker` --- .../aya/tyck/tycker/ConcreteAwareTycker.java | 7 ++-- .../org/aya/tyck/tycker/LetListTycker.java | 41 +++++++++++++++++++ .../{MockedTycker.java => MockTycker.java} | 32 +++------------ .../org/aya/tyck/tycker/StatedTycker.java | 5 +-- .../org/aya/tyck/tycker/UnifiedTycker.java | 2 +- .../org/aya/tyck/unify/TermComparator.java | 8 ++-- 6 files changed, 57 insertions(+), 38 deletions(-) create mode 100644 base/src/main/java/org/aya/tyck/tycker/LetListTycker.java rename base/src/main/java/org/aya/tyck/tycker/{MockedTycker.java => MockTycker.java} (74%) diff --git a/base/src/main/java/org/aya/tyck/tycker/ConcreteAwareTycker.java b/base/src/main/java/org/aya/tyck/tycker/ConcreteAwareTycker.java index 3dfb6b99f8..1c1e5fb8e9 100644 --- a/base/src/main/java/org/aya/tyck/tycker/ConcreteAwareTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/ConcreteAwareTycker.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.tyck.tycker; @@ -10,6 +10,7 @@ import org.aya.core.visitor.Zonker; import org.aya.guest0x0.cubical.Partial; import org.aya.tyck.Result; +import org.aya.tyck.env.MapLocalCtx; import org.aya.tyck.trace.Trace; import org.aya.util.error.SourceNode; import org.aya.util.reporter.Reporter; @@ -28,12 +29,12 @@ * @see #solveMetas() * @see #traceExit */ -public sealed abstract class ConcreteAwareTycker extends StatedTycker permits MockedTycker { +public sealed abstract class ConcreteAwareTycker extends MockTycker permits LetListTycker { public final @NotNull MutableTreeSet withTerms = MutableTreeSet.create(Comparator.comparing(SourceNode::sourcePos)); protected ConcreteAwareTycker(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuilder, @NotNull TyckState state) { - super(reporter, traceBuilder, state); + super(reporter, traceBuilder, state, new MapLocalCtx()); } //region Zonk + solveMetas diff --git a/base/src/main/java/org/aya/tyck/tycker/LetListTycker.java b/base/src/main/java/org/aya/tyck/tycker/LetListTycker.java new file mode 100644 index 0000000000..7159cfbc3e --- /dev/null +++ b/base/src/main/java/org/aya/tyck/tycker/LetListTycker.java @@ -0,0 +1,41 @@ +// 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.tyck.tycker; + +import org.aya.tyck.pat.TypedSubst; +import org.aya.tyck.trace.Trace; +import org.aya.util.reporter.Reporter; +import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; + +import java.util.function.Supplier; + +/** + * This is the third base-base class of a tycker. + * It has a localCtx and supports some term mocking functions. + * + * @author ice1000 + * @see #subscoped(Supplier) + */ +public abstract sealed class LetListTycker extends ConcreteAwareTycker permits UnifiedTycker { + public @NotNull TypedSubst definitionEqualities = new TypedSubst(); + + protected LetListTycker(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuilder, @NotNull TyckState state) { + super(reporter, traceBuilder, state); + } + + public R subscoped(@NotNull Supplier action) { + var parentCtx = this.ctx; + var parentSubst = this.definitionEqualities; + + this.ctx = parentCtx.deriveMap(); + this.definitionEqualities = parentSubst.derive(); + + var result = action.get(); + + this.definitionEqualities = parentSubst; + this.ctx = parentCtx; + + return result; + } +} diff --git a/base/src/main/java/org/aya/tyck/tycker/MockedTycker.java b/base/src/main/java/org/aya/tyck/tycker/MockTycker.java similarity index 74% rename from base/src/main/java/org/aya/tyck/tycker/MockedTycker.java rename to base/src/main/java/org/aya/tyck/tycker/MockTycker.java index 843647b172..6351e090ef 100644 --- a/base/src/main/java/org/aya/tyck/tycker/MockedTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/MockTycker.java @@ -10,10 +10,9 @@ import org.aya.ref.LocalVar; import org.aya.tyck.Result; import org.aya.tyck.env.LocalCtx; -import org.aya.tyck.env.MapLocalCtx; -import org.aya.tyck.pat.TypedSubst; import org.aya.tyck.trace.Trace; import org.aya.tyck.unify.Synthesizer; +import org.aya.tyck.unify.TermComparator; import org.aya.tyck.unify.Unifier; import org.aya.util.Arg; import org.aya.util.Ordering; @@ -22,25 +21,21 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; -import java.util.function.Supplier; - /** - * This is the third base-base class of a tycker. - * It has a localCtx and supports some term mocking functions. + * This is the 2.25-th base class of a tycker. * * @author ice1000 * @see #generatePi * @see #instImplicits(Result, SourcePos) * @see #mockArg * @see #mockTerm - * @see #subscoped(Supplier) */ -public abstract sealed class MockedTycker extends ConcreteAwareTycker permits UnifiedTycker { - public @NotNull LocalCtx ctx = new MapLocalCtx(); - public @NotNull TypedSubst definitionEqualities = new TypedSubst(); +public abstract sealed class MockTycker extends StatedTycker permits ConcreteAwareTycker, TermComparator { + public @NotNull LocalCtx ctx; - protected MockedTycker(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuilder, @NotNull TyckState state) { + protected MockTycker(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuilder, @NotNull TyckState state, @NotNull LocalCtx ctx) { super(reporter, traceBuilder, state); + this.ctx = ctx; } public @NotNull Unifier unifier(@NotNull SourcePos pos, @NotNull Ordering ord) { @@ -85,19 +80,4 @@ protected final Result instImplicits(@NotNull Result result, @NotNull SourcePos } return new Result.Default(term, type); } - - public R subscoped(@NotNull Supplier action) { - var parentCtx = this.ctx; - var parentSubst = this.definitionEqualities; - - this.ctx = parentCtx.deriveMap(); - this.definitionEqualities = parentSubst.derive(); - - var result = action.get(); - - this.definitionEqualities = parentSubst; - this.ctx = parentCtx; - - return result; - } } diff --git a/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java b/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java index b4801a31ef..357d1629ec 100644 --- a/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/StatedTycker.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.tyck.tycker; @@ -14,7 +14,6 @@ import org.aya.tyck.Result; import org.aya.tyck.env.LocalCtx; import org.aya.tyck.trace.Trace; -import org.aya.tyck.unify.TermComparator; import org.aya.tyck.unify.Unifier; import org.aya.util.Ordering; import org.aya.util.error.SourcePos; @@ -32,7 +31,7 @@ * @see #defCall * @see #inferRef(DefVar) */ -public abstract sealed class StatedTycker extends TracedTycker permits ConcreteAwareTycker, TermComparator { +public abstract sealed class StatedTycker extends TracedTycker permits MockTycker { public final @NotNull TyckState state; protected StatedTycker(@NotNull Reporter reporter, @Nullable Trace.Builder traceBuilder, @NotNull TyckState state) { diff --git a/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java b/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java index d14ea52686..0ffe8ff0ef 100644 --- a/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java @@ -44,7 +44,7 @@ * @see #checkBoundaries * @see #inheritFallbackUnify */ -public sealed abstract class UnifiedTycker extends MockedTycker permits PropTycker { +public sealed abstract class UnifiedTycker extends LetListTycker permits PropTycker { protected UnifiedTycker(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuilder, @NotNull TyckState state) { super(reporter, traceBuilder, state); } diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java index 9cd2534e2a..74de53d53d 100644 --- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java +++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java @@ -28,7 +28,7 @@ import org.aya.tyck.env.LocalCtx; import org.aya.tyck.error.LevelError; import org.aya.tyck.trace.Trace; -import org.aya.tyck.tycker.StatedTycker; +import org.aya.tyck.tycker.MockTycker; import org.aya.tyck.tycker.TyckState; import org.aya.util.Arg; import org.aya.util.Ordering; @@ -51,17 +51,15 @@ * @see #compareUntyped(Term, Term, Sub, Sub) the "synthesize" direction * @see #compare(Term, Term, Sub, Sub, Term) the "inherit" direction */ -public sealed abstract class TermComparator extends StatedTycker permits Unifier { +public sealed abstract class TermComparator extends MockTycker permits Unifier { protected final @NotNull SourcePos pos; protected final @NotNull Ordering cmp; - protected final @NotNull LocalCtx ctx; private FailureData failure; public TermComparator(@Nullable Trace.Builder traceBuilder, @NotNull TyckState state, @NotNull Reporter reporter, @NotNull SourcePos pos, @NotNull Ordering cmp, @NotNull LocalCtx ctx) { - super(reporter, traceBuilder, state); + super(reporter, traceBuilder, state, ctx); this.pos = pos; this.cmp = cmp; - this.ctx = ctx; } private static boolean isCall(@NotNull Term term) { From 54fb8dedd92c556d0d16cc69a6bdc7943c4e0bc3 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 00:35:47 -0500 Subject: [PATCH 14/28] unifier: refactor --- .../org/aya/tyck/unify/DoubleChecker.java | 2 +- .../main/java/org/aya/tyck/unify/Unifier.java | 33 +++++++++++-------- 2 files changed, 20 insertions(+), 15 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java index cba5bd900a..6aa4d4ef32 100644 --- a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java +++ b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java @@ -24,7 +24,7 @@ public DoubleChecker(@NotNull Unifier unifier) { } public DoubleChecker(@NotNull Unifier unifier, @NotNull Sub lr, @NotNull Sub rl) { - this(unifier, new Synthesizer(unifier.state, unifier.ctx), lr, rl); + this(unifier, unifier.synthesizer(), lr, rl); } private @NotNull Term whnf(Term x) { diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index 8746f14cb5..ac88428278 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -89,21 +89,26 @@ protected Term solveMeta(@NotNull MetaTerm lhs, @NotNull Term preRhs, Sub lr, Su // Update: this is still needed, see #327 last task (`coe'`) var checker = new DoubleChecker(new Unifier(Ordering.Lt, reporter, false, false, traceBuilder, state, pos, ctx.deriveMap()), lr, rl); - var expectedType = meta.info.result(); - if (expectedType == null) expectedType = providedType; - else if (providedType != null) { - // The provided type from the context, hence neither from LHS nor RHS, - // so we don't substitute it backwards, hence the empty `Sub`. - compareUntyped(expectedType, providedType, lr, new Sub()); - expectedType = expectedType.freezeHoles(state); + // Check the expected type. + switch (meta.info) { + case MetaInfo.AnyType() -> {} + case MetaInfo.Result(var expectedType) -> { + if (providedType != null) { + // The provided type from the context, hence neither from LHS nor RHS, + // so we don't substitute it backwards, hence the empty `Sub`. + compareUntyped(expectedType, providedType, lr, new Sub()); + providedType = expectedType.freezeHoles(state); + } else providedType = expectedType; + } } - if (expectedType != null) { + // Check the solution. + if (providedType != null) { // resultTy might be an ErrorTerm, what to do? - if (!checker.inherit(preRhs, expectedType)) - reporter.report(new HoleProblem.IllTypedError(lhs, expectedType, preRhs)); + if (!checker.inherit(preRhs, providedType)) + reporter.report(new HoleProblem.IllTypedError(lhs, providedType, preRhs)); } else { - expectedType = checker.synthesizer().synthesize(preRhs); - if (expectedType == null) { + providedType = checker.synthesizer().synthesize(preRhs); + if (providedType == null) { throw new UnsupportedOperationException("TODO: add an error report for this"); } } @@ -119,7 +124,7 @@ else if (providedType != null) { if (!allowVague && overlap.anyMatch(var -> preRhs.findUsages(var) > 0)) { state.addEqn(createEqn(lhs, preRhs, lr, rl)); // Skip the unification and scope check - return expectedType; + return providedType; } // Now we are sure that the variables in overlap are all unused. @@ -163,7 +168,7 @@ else if (providedType != null) { return new ErrorTerm(solved); } tracing(builder -> builder.append(new Trace.LabelT(pos, "Hole solved!"))); - return expectedType; + return providedType; } /** From 8f8740c71b8f47173985d6e89d5ec49f41b5c581 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 00:40:12 -0500 Subject: [PATCH 15/28] meta: add `PiDom` --- base/src/main/java/org/aya/core/meta/MetaInfo.java | 12 ++++++++++++ base/src/main/java/org/aya/tyck/unify/Unifier.java | 1 + 2 files changed, 13 insertions(+) diff --git a/base/src/main/java/org/aya/core/meta/MetaInfo.java b/base/src/main/java/org/aya/core/meta/MetaInfo.java index 908a3bed36..ba41d60482 100644 --- a/base/src/main/java/org/aya/core/meta/MetaInfo.java +++ b/base/src/main/java/org/aya/core/meta/MetaInfo.java @@ -2,6 +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.core.meta; +import org.aya.core.term.SortTerm; import org.aya.core.term.Term; import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; @@ -28,4 +29,15 @@ record AnyType() implements MetaInfo { return null; } } + + /** + * The meta variable is the domain of a pi type which is of a known type. + *

+ * See: notes/sort-system.md + */ + record PiDom(@NotNull SortTerm sort) implements MetaInfo { + @Override public @Nullable Term result() { + return null; + } + } } diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index ac88428278..37b21d4453 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -100,6 +100,7 @@ protected Term solveMeta(@NotNull MetaTerm lhs, @NotNull Term preRhs, Sub lr, Su providedType = expectedType.freezeHoles(state); } else providedType = expectedType; } + case MetaInfo.PiDom(var sort) -> checker.synthesizer().inheritPiDom(preRhs, sort); } // Check the solution. if (providedType != null) { From ef1d0f8b74c62a6222e0d5891a8020f795c3249f Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 00:44:39 -0500 Subject: [PATCH 16/28] meta: use `PiDom` --- .../src/main/java/org/aya/core/meta/Meta.java | 21 +++++++++++-------- .../main/java/org/aya/core/term/MetaTerm.java | 2 +- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/base/src/main/java/org/aya/core/meta/Meta.java b/base/src/main/java/org/aya/core/meta/Meta.java index eb5e945025..734e852726 100644 --- a/base/src/main/java/org/aya/core/meta/Meta.java +++ b/base/src/main/java/org/aya/core/meta/Meta.java @@ -8,6 +8,7 @@ import kala.tuple.Tuple2; import org.aya.core.term.MetaTerm; import org.aya.core.term.PiTerm; +import org.aya.core.term.SortTerm; import org.aya.core.term.Term; import org.aya.core.visitor.Subst; import org.aya.generic.Constants; @@ -69,23 +70,25 @@ private Meta( @NotNull ImmutableSeq> contextArgs ) { assert telescope.isEmpty(); - // TODO[isType]: this one should be piDom - var domVar = new Meta(contextTele, ImmutableSeq.empty(), domName, info, sourcePos); - // TODO[isType]: this one should be piCod - var codVar = new Meta(contextTele, ImmutableSeq.empty(), codName, info, sourcePos); + var knownDomInfo = info; + // TODO[isType]: deal with piCod + var knownCodInfo = info; + if (knownDomInfo instanceof MetaInfo.Result(var result)) { + if (!(result instanceof SortTerm sort)) throw new AssertionError("This should be unreachable"); + knownDomInfo = new MetaInfo.PiDom(sort); + } + var domVar = new Meta(contextTele, ImmutableSeq.empty(), domName, knownDomInfo, sourcePos); + var codVar = new Meta(contextTele, ImmutableSeq.empty(), codName, knownCodInfo, sourcePos); var dom = new MetaTerm(domVar, contextArgs, ImmutableSeq.empty()); var cod = new MetaTerm(codVar, contextArgs, ImmutableSeq.empty()); var domParam = new Term.Param(Constants.randomlyNamed(sourcePos), dom, explicit); return new PiTerm(domParam, cod); } - public @NotNull MetaTerm asPiDom( - @NotNull Term resultNew, @NotNull ImmutableSeq> contextArgs - ) { + public @NotNull MetaTerm asPiDom(@NotNull SortTerm sort, @NotNull ImmutableSeq> contextArgs) { assert telescope.isEmpty(); assert info instanceof MetaInfo.AnyType; - // TODO[isType]: this one should be piDom - var typed = new Meta(contextTele, ImmutableSeq.empty(), name, info, sourcePos); + var typed = new Meta(contextTele, ImmutableSeq.empty(), name, new MetaInfo.PiDom(sort), sourcePos); return new MetaTerm(typed, contextArgs, ImmutableSeq.empty()); } diff --git a/base/src/main/java/org/aya/core/term/MetaTerm.java b/base/src/main/java/org/aya/core/term/MetaTerm.java index 9a1474e72a..eee1c8c69b 100644 --- a/base/src/main/java/org/aya/core/term/MetaTerm.java +++ b/base/src/main/java/org/aya/core/term/MetaTerm.java @@ -31,7 +31,7 @@ public record MetaTerm( return ref.asPi(ref.name() + "dom", ref.name() + "cod", explicit, contextArgs); } - public @NotNull MetaTerm asPiDom(@NotNull Term result) { + public @NotNull MetaTerm asPiDom(@NotNull SortTerm result) { return ref.asPiDom(result, contextArgs); } From 5d015cb1190fea2f2b055c10dd2dcd948b7dbcfe Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 00:48:14 -0500 Subject: [PATCH 17/28] synthesize: allow some `null` returning --- .../java/org/aya/tyck/unify/Synthesizer.java | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java index bcc8236ecf..2261ffa355 100644 --- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -80,9 +80,8 @@ public boolean inheritPiDom(Term type, SortTerm expected) { case SigmaTerm sigma -> { var univ = MutableList.create(); for (var param : sigma.params()) { - var pressed = press(param.type()); - // TODO[isType]: There can be metas in the sigma's parameters - if (!(pressed instanceof SortTerm sort)) yield unreachable(pressed); + var pressed = synthesize(param.type()); + if (!(pressed instanceof SortTerm sort)) yield null; univ.append(sort); ctx.put(param); } @@ -90,19 +89,20 @@ public boolean inheritPiDom(Term type, SortTerm expected) { yield univ.reduce(SigmaTerm::max); } case PiTerm pi -> { - var paramTyRaw = press(pi.param().type()); + var paramTyRaw = synthesize(pi.param().type()); + if (!(paramTyRaw instanceof SortTerm paramTy)) yield null; var t = new Synthesizer(state, ctx.deriveSeq()); yield t.ctx.with(pi.param(), () -> { - if (paramTyRaw instanceof SortTerm paramTy && t.press(pi.body()) instanceof SortTerm retTy) { + if (t.press(pi.body()) instanceof SortTerm retTy) { return PiTerm.max(paramTy, retTy); - } else return unreachable(pi); + } else return null; }); } case NewTerm neu -> neu.struct(); case ErrorTerm term -> ErrorTerm.typeOf(term.description()); case ProjTerm proj -> { - var sigmaRaw = press(proj.of()); - if (!(sigmaRaw instanceof SigmaTerm sigma)) yield ErrorTerm.typeOf(proj); + var sigmaRaw = synthesize(proj.of()); + if (!(sigmaRaw instanceof SigmaTerm sigma)) yield null; var index = proj.ix() - 1; var telescope = sigma.params(); yield telescope.get(index).type().subst(ProjTerm.projSubst(proj.of(), index, telescope)); From 91309877dc2db44bc16c9bcf796b5f92771388dc Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 01:00:01 -0500 Subject: [PATCH 18/28] synthesize: deal with `null`s smartly --- .../org/aya/tyck/unify/DoubleChecker.java | 11 +++--- .../java/org/aya/tyck/unify/Synthesizer.java | 36 ++++++++++++------- 2 files changed, 28 insertions(+), 19 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java index 6aa4d4ef32..8e8c44e51d 100644 --- a/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java +++ b/base/src/main/java/org/aya/tyck/unify/DoubleChecker.java @@ -9,7 +9,6 @@ import org.aya.tyck.unify.TermComparator.Sub; import org.aya.util.Ordering; import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; public record DoubleChecker( @NotNull Unifier unifier, @NotNull Synthesizer synthesizer, @@ -38,7 +37,7 @@ public boolean inherit(@NotNull Term preterm, @NotNull Term expected) { assert false : "No rules -- unsure if reachable"; return false; } - return compare(lhs, expected, null); + return compare(lhs, expected); } return switch (preterm) { case ErrorTerm term -> true; @@ -57,7 +56,7 @@ case PLamTerm(var params, var body)when whnf(expected) instanceof PathTerm path inherit(body, path.substBody(params))); case PartialTerm(var par, var rhsTy)when whnf(expected) instanceof PartialTyTerm(var ty, var phi) -> { if (!PartialTerm.impliesCof(phi, par.restr(), unifier.state)) yield false; - yield compare(rhsTy, ty, null); + yield compare(rhsTy, ty); } case TupTerm(var items)when whnf(expected) instanceof SigmaTerm sigma -> { var res = sigma.check(items, (e, t) -> { @@ -73,11 +72,11 @@ case PiTerm(var dom, var cod) -> { if (!synthesizer.inheritPiDom(dom.type(), sort)) yield false; yield unifier.ctx.with(dom, () -> inherit(cod, sort)); } - case default -> compare(synthesizer.press(preterm), expected, null); + case default -> compare(synthesizer.press(preterm), expected); }; } - private boolean compare(@NotNull Term lhs, @NotNull Term expected, @Nullable Term type) { - return unifier.compare(lhs, expected, lr, rl, type); + private boolean compare(@NotNull Term lhs, @NotNull Term expected) { + return unifier.compare(lhs, expected, lr, rl, null); } } diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java index 2261ffa355..719b362eb5 100644 --- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -28,10 +28,15 @@ * @see org.aya.tyck.unify.DoubleChecker */ public record Synthesizer(@NotNull TyckState state, @NotNull LocalCtx ctx) { - public @NotNull Term press(@NotNull Term preterm) { + public @Nullable Term tryPress(@NotNull Term preterm) { var synthesize = synthesize(preterm); + return synthesize != null ? whnf(synthesize) : null; + } + + public @NotNull Term press(@NotNull Term preterm) { + var synthesize = tryPress(preterm); assert synthesize != null : preterm.toDoc(AyaPrettierOptions.pretty()).debugRender(); - return whnf(synthesize); + return synthesize; } public boolean inheritPiDom(Term type, SortTerm expected) { @@ -52,6 +57,10 @@ public boolean inheritPiDom(Term type, SortTerm expected) { }; } + /** + * @param preterm expected to be whnf + * @return null if failed to synthesize + */ public @Nullable Term synthesize(@NotNull Term preterm) { return switch (preterm) { case RefTerm term -> ctx.get(term.var()); @@ -70,7 +79,7 @@ public boolean inheritPiDom(Term type, SortTerm expected) { } case RefTerm.Field field -> Def.defType(field.ref()); case FieldTerm access -> { - var callRaw = press(access.of()); + var callRaw = tryPress(access.of()); if (!(callRaw instanceof StructCall call)) yield unreachable(callRaw); var field = access.ref(); var subst = DeltaExpander.buildSubst(Def.defTele(field), access.fieldArgs()) @@ -89,7 +98,7 @@ public boolean inheritPiDom(Term type, SortTerm expected) { yield univ.reduce(SigmaTerm::max); } case PiTerm pi -> { - var paramTyRaw = synthesize(pi.param().type()); + var paramTyRaw = tryPress(pi.param().type()); if (!(paramTyRaw instanceof SortTerm paramTy)) yield null; var t = new Synthesizer(state, ctx.deriveSeq()); yield t.ctx.with(pi.param(), () -> { @@ -101,7 +110,7 @@ public boolean inheritPiDom(Term type, SortTerm expected) { case NewTerm neu -> neu.struct(); case ErrorTerm term -> ErrorTerm.typeOf(term.description()); case ProjTerm proj -> { - var sigmaRaw = synthesize(proj.of()); + var sigmaRaw = tryPress(proj.of()); if (!(sigmaRaw instanceof SigmaTerm sigma)) yield null; var index = proj.ix() - 1; var telescope = sigma.params(); @@ -132,9 +141,9 @@ case InTerm(var phi, var u) -> { .map(t -> new Arg<>(t, true))); } case OutTerm outS -> { - var ty = press(outS.of()); + var ty = tryPress(outS.of()); if (ty instanceof PrimCall sub) yield sub.args().first().term(); - yield unreachable(outS); + yield null; } case PAppTerm app -> { // v @ ui : A[ui/xi] @@ -142,13 +151,14 @@ case InTerm(var phi, var u) -> { var ui = app.args().map(Arg::term); yield app.cube().type().subst(new Subst(xi, ui)); } - case PLamTerm lam -> { - var bud = press(lam.body()); - yield new PathTerm(lam.params(), bud, new Partial.Const<>(bud)); + case PLamTerm(var params, var body) -> { + var bud = tryPress(body); + if (bud == null) yield null; + yield new PathTerm(params, bud, new Partial.Const<>(body)); } - case AppTerm app -> { - var piRaw = press(app.of()); - yield piRaw instanceof PiTerm pi ? pi.substBody(app.arg().term()) : null; + case AppTerm(var of, var arg) -> { + var piRaw = tryPress(of); + yield piRaw instanceof PiTerm pi ? pi.substBody(arg.term()) : null; } case default -> null; }; From 94b4b09278d807a6c7719c2496778536e27af270 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 01:06:56 -0500 Subject: [PATCH 19/28] synthesize: return true --- .../src/main/java/org/aya/tyck/unify/Synthesizer.java | 3 +-- base/src/test/resources/success/src/Issues/874.aya | 11 +++++++++++ 2 files changed, 12 insertions(+), 2 deletions(-) create mode 100644 base/src/test/resources/success/src/Issues/874.aya diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java index 719b362eb5..93b8671e55 100644 --- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -42,8 +42,7 @@ public record Synthesizer(@NotNull TyckState state, @NotNull LocalCtx ctx) { public boolean inheritPiDom(Term type, SortTerm expected) { if (type instanceof MetaTerm meta && meta.ref().info instanceof MetaInfo.AnyType) { var typed = meta.asPiDom(expected); - state.solve(meta.ref(), typed); - return false; + return state.solve(meta.ref(), typed); } if (!(synthesize(type) instanceof SortTerm actual)) return false; return switch (expected.kind()) { diff --git a/base/src/test/resources/success/src/Issues/874.aya b/base/src/test/resources/success/src/Issues/874.aya new file mode 100644 index 0000000000..0e992bf104 --- /dev/null +++ b/base/src/test/resources/success/src/Issues/874.aya @@ -0,0 +1,11 @@ +open import Paths +open import Arith::Nat::Core + +data Test : Prop +| con Nat + +data TestPiDomMeta : Prop +| con (x : _) (x = 1) + +data TestPiDomMeta2 : Type +| con (x : _) (x = 1) From 7eb1621b6bb042754e2ebe3593f258d2ae67231b Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 01:12:02 -0500 Subject: [PATCH 20/28] synthesize: refine code --- .../java/org/aya/tyck/tycker/PropTycker.java | 3 +-- .../java/org/aya/tyck/unify/Synthesizer.java | 16 ++++------------ .../test/resources/success/src/Issues/874.aya | 2 +- 3 files changed, 6 insertions(+), 15 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/tycker/PropTycker.java b/base/src/main/java/org/aya/tyck/tycker/PropTycker.java index 14dabb730f..dcd10a1086 100644 --- a/base/src/main/java/org/aya/tyck/tycker/PropTycker.java +++ b/base/src/main/java/org/aya/tyck/tycker/PropTycker.java @@ -43,9 +43,8 @@ protected final T withInProp(boolean inProp, @NotNull Supplier supplier) } public boolean isPropType(@NotNull Term type) { - var sort = new Synthesizer(state, ctx).synthesize(type); + var sort = new Synthesizer(state, ctx).tryPress(type); if (sort == null) throw new UnsupportedOperationException("Zaoqi"); - sort = whnf(sort); if (sort instanceof MetaTerm meta) { // TODO[isType]: refactor non-Prop assertions state.notInPropMetas().add(meta.ref()); // assert not Prop diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java index 93b8671e55..63ded8f594 100644 --- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -44,7 +44,7 @@ public boolean inheritPiDom(Term type, SortTerm expected) { var typed = meta.asPiDom(expected); return state.solve(meta.ref(), typed); } - if (!(synthesize(type) instanceof SortTerm actual)) return false; + if (!(tryPress(type) instanceof SortTerm actual)) return false; return switch (expected.kind()) { case Prop -> switch (actual.kind()) { case Prop, Type -> true; @@ -67,19 +67,11 @@ public boolean inheritPiDom(Term type, SortTerm expected) { case Callable.DefCall call -> Def.defResult(call.ref()) .subst(DeltaExpander.buildSubst(Def.defTele(call.ref()), call.args())) .lift(call.ulift()); - // TODO[isType]: deal with type-only metas - case MetaTerm hole -> { - var info = hole.ref().info; - if (info instanceof MetaInfo.Result(var result)) yield result; - var simpl = whnf(hole); - if (simpl instanceof MetaTerm again) { - throw new UnsupportedOperationException("TODO"); - } else yield synthesize(simpl); - } + case MetaTerm hole -> hole.ref().info.result(); case RefTerm.Field field -> Def.defType(field.ref()); case FieldTerm access -> { var callRaw = tryPress(access.of()); - if (!(callRaw instanceof StructCall call)) yield unreachable(callRaw); + if (!(callRaw instanceof StructCall call)) yield unreachable(access); var field = access.ref(); var subst = DeltaExpander.buildSubst(Def.defTele(field), access.fieldArgs()) .add(DeltaExpander.buildSubst(Def.defTele(call.ref()), access.structArgs())); @@ -88,7 +80,7 @@ public boolean inheritPiDom(Term type, SortTerm expected) { case SigmaTerm sigma -> { var univ = MutableList.create(); for (var param : sigma.params()) { - var pressed = synthesize(param.type()); + var pressed = tryPress(param.type()); if (!(pressed instanceof SortTerm sort)) yield null; univ.append(sort); ctx.put(param); diff --git a/base/src/test/resources/success/src/Issues/874.aya b/base/src/test/resources/success/src/Issues/874.aya index 0e992bf104..d2f34fff5d 100644 --- a/base/src/test/resources/success/src/Issues/874.aya +++ b/base/src/test/resources/success/src/Issues/874.aya @@ -8,4 +8,4 @@ data TestPiDomMeta : Prop | con (x : _) (x = 1) data TestPiDomMeta2 : Type -| con (x : _) (x = 1) +| con : ∀ x -> (x = 1) -> _ From 2cb8c8f5156abfc3e75e834548b7b105f7487695 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 01:26:11 -0500 Subject: [PATCH 21/28] meta: pretty print info --- base/src/main/java/module-info.java | 2 +- .../main/java/org/aya/core/meta/MetaInfo.java | 19 +++++++++++++++++-- .../java/org/aya/tyck/error/HoleProblem.java | 7 ++++--- .../java/org/aya/tyck/unify/Synthesizer.java | 2 +- .../main/java/org/aya/tyck/unify/Unifier.java | 12 +++++++++--- .../pretty/backend/latex/DocTeXPrinter.java | 3 ++- .../src/main/java/org/aya/pretty/doc/Doc.java | 14 +++++++++----- 7 files changed, 43 insertions(+), 16 deletions(-) diff --git a/base/src/main/java/module-info.java b/base/src/main/java/module-info.java index c155bc4f38..31dae88492 100644 --- a/base/src/main/java/module-info.java +++ b/base/src/main/java/module-info.java @@ -17,6 +17,7 @@ exports org.aya.concrete.visitor; exports org.aya.concrete; exports org.aya.core.def; + exports org.aya.core.meta; exports org.aya.core.ops; exports org.aya.core.pat; exports org.aya.core.repr; @@ -42,5 +43,4 @@ exports org.aya.tyck.trace; exports org.aya.tyck.unify; exports org.aya.tyck; - exports org.aya.core.meta; } diff --git a/base/src/main/java/org/aya/core/meta/MetaInfo.java b/base/src/main/java/org/aya/core/meta/MetaInfo.java index ba41d60482..0ee33c3f16 100644 --- a/base/src/main/java/org/aya/core/meta/MetaInfo.java +++ b/base/src/main/java/org/aya/core/meta/MetaInfo.java @@ -4,6 +4,9 @@ import org.aya.core.term.SortTerm; import org.aya.core.term.Term; +import org.aya.generic.AyaDocile; +import org.aya.pretty.doc.Doc; +import org.aya.util.prettier.PrettierOptions; import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; @@ -12,13 +15,17 @@ * * @author ice1000 */ -public sealed interface MetaInfo { +public sealed interface MetaInfo extends AyaDocile { @Nullable Term result(); /** * The type of the meta is known. * We shall check the solution against this type. */ - record Result(@NotNull Term result) implements MetaInfo {} + record Result(@NotNull Term result) implements MetaInfo { + @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) { + return Doc.sep(Doc.symbol("?"), Doc.symbol(":"), result.toDoc(options)); + } + } /** * The meta variable is a type. @@ -28,6 +35,10 @@ record AnyType() implements MetaInfo { @Override public @Nullable Term result() { return null; } + + @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) { + return Doc.sep(Doc.plain("_"), Doc.symbols(":", "?")); + } } /** @@ -39,5 +50,9 @@ record PiDom(@NotNull SortTerm sort) implements MetaInfo { @Override public @Nullable Term result() { return null; } + + @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) { + return Doc.sep(Doc.symbols("?", "->", "_", ":"), sort.toDoc(options)); + } } } diff --git a/base/src/main/java/org/aya/tyck/error/HoleProblem.java b/base/src/main/java/org/aya/tyck/error/HoleProblem.java index fff18362bb..dba18077ec 100644 --- a/base/src/main/java/org/aya/tyck/error/HoleProblem.java +++ b/base/src/main/java/org/aya/tyck/error/HoleProblem.java @@ -1,10 +1,11 @@ -// 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.tyck.error; import kala.collection.Seq; import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; +import org.aya.core.meta.MetaInfo; import org.aya.core.term.MetaTerm; import org.aya.core.term.Term; import org.aya.prettier.BasePrettier; @@ -43,12 +44,12 @@ record BadSpineError( record IllTypedError( @Override @NotNull MetaTerm term, - @NotNull Term result, + @NotNull MetaInfo result, @Override @NotNull Term solution ) implements HoleProblem { @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { return Doc.vcat( - Doc.english("The meta is supposed to have type"), + Doc.english("The meta (denoted ?) is supposed to satisfy"), Doc.par(1, result.toDoc(options)), Doc.english("However, the solution below does not have the same type:"), Doc.par(1, solution.toDoc(options)) diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java index 63ded8f594..7672fb493e 100644 --- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -39,7 +39,7 @@ public record Synthesizer(@NotNull TyckState state, @NotNull LocalCtx ctx) { return synthesize; } - public boolean inheritPiDom(Term type, SortTerm expected) { + public boolean inheritPiDom(@NotNull Term type, @NotNull SortTerm expected) { if (type instanceof MetaTerm meta && meta.ref().info instanceof MetaInfo.AnyType) { var typed = meta.asPiDom(expected); return state.solve(meta.ref(), typed); diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index 37b21d4453..47a52d2664 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -91,7 +91,9 @@ protected Term solveMeta(@NotNull MetaTerm lhs, @NotNull Term preRhs, Sub lr, Su reporter, false, false, traceBuilder, state, pos, ctx.deriveMap()), lr, rl); // Check the expected type. switch (meta.info) { - case MetaInfo.AnyType() -> {} + case MetaInfo.AnyType() -> { + + } case MetaInfo.Result(var expectedType) -> { if (providedType != null) { // The provided type from the context, hence neither from LHS nor RHS, @@ -100,13 +102,17 @@ protected Term solveMeta(@NotNull MetaTerm lhs, @NotNull Term preRhs, Sub lr, Su providedType = expectedType.freezeHoles(state); } else providedType = expectedType; } - case MetaInfo.PiDom(var sort) -> checker.synthesizer().inheritPiDom(preRhs, sort); + case MetaInfo.PiDom(var sort) -> { + if (!checker.synthesizer().inheritPiDom(preRhs, sort)) { + reporter.report(new HoleProblem.IllTypedError(lhs, meta.info, preRhs)); + } + } } // Check the solution. if (providedType != null) { // resultTy might be an ErrorTerm, what to do? if (!checker.inherit(preRhs, providedType)) - reporter.report(new HoleProblem.IllTypedError(lhs, providedType, preRhs)); + reporter.report(new HoleProblem.IllTypedError(lhs, new MetaInfo.Result(providedType), preRhs)); } else { providedType = checker.synthesizer().synthesize(preRhs); if (providedType == null) { diff --git a/pretty/src/main/java/org/aya/pretty/backend/latex/DocTeXPrinter.java b/pretty/src/main/java/org/aya/pretty/backend/latex/DocTeXPrinter.java index 7ba843b6c0..4b5a307896 100644 --- a/pretty/src/main/java/org/aya/pretty/backend/latex/DocTeXPrinter.java +++ b/pretty/src/main/java/org/aya/pretty/backend/latex/DocTeXPrinter.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.pretty.backend.latex; @@ -40,6 +40,7 @@ public class DocTeXPrinter extends StringPrinter { Tuple.of("=>", "\\Rightarrow"), Tuple.of("->", "\\to"), Tuple.of("_|_", "\\bot"), + Tuple.of("_", "\\textunderscore"), Tuple.of("~", "\\neg"), Tuple.of("**", "\\times"), id(":"), id("."), diff --git a/pretty/src/main/java/org/aya/pretty/doc/Doc.java b/pretty/src/main/java/org/aya/pretty/doc/Doc.java index 759d634971..8c15d54fd9 100644 --- a/pretty/src/main/java/org/aya/pretty/doc/Doc.java +++ b/pretty/src/main/java/org/aya/pretty/doc/Doc.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.pretty.doc; @@ -605,12 +605,16 @@ record PageWidth(@NotNull IntFunction docBuilder) implements Doc { } /** - * @param text '\n' not allowed! + * @param symbol '\n' not allowed! * @return special symbol */ - @Contract("_ -> new") static @NotNull Doc symbol(String text) { - assert !text.contains("\n"); - return new SpecialSymbol(text); + @Contract("_ -> new") static @NotNull Doc symbol(String symbol) { + assert !symbol.contains("\n"); + return new SpecialSymbol(symbol); + } + + @Contract("_ -> new") static @NotNull Doc symbols(String... symbols) { + return sep(Seq.of(symbols).map(Doc::symbol)); } /** From 8d6c9a9b8646c83047da13194591d3507ab083fe Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 01:32:47 -0500 Subject: [PATCH 22/28] unify: report error --- .../main/java/org/aya/tyck/unify/Unifier.java | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index 47a52d2664..73d186ce9a 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -78,8 +78,13 @@ public Unifier( return overlap; } - @Override @Nullable - protected Term solveMeta(@NotNull MetaTerm lhs, @NotNull Term preRhs, Sub lr, Sub rl, @Nullable Term providedType) { + @Override protected @Nullable Term + solveMeta(@NotNull MetaTerm lhs, @NotNull Term preRhs, Sub lr, Sub rl, @Nullable Term providedType) { + return solveMetaWHNF(lhs, whnf(preRhs), lr, rl, providedType); + } + + private @Nullable Term + solveMetaWHNF(@NotNull MetaTerm lhs, @NotNull Term preRhs, Sub lr, Sub rl, @Nullable Term providedType) { var meta = lhs.ref(); var sameMeta = sameMeta(lr, rl, lhs, meta, preRhs); if (sameMeta.isDefined()) return sameMeta.get(); @@ -92,7 +97,13 @@ protected Term solveMeta(@NotNull MetaTerm lhs, @NotNull Term preRhs, Sub lr, Su // Check the expected type. switch (meta.info) { case MetaInfo.AnyType() -> { - + if (!(preRhs instanceof Formation)) { + providedType = checker.synthesizer().synthesize(preRhs); + if (!(providedType instanceof SortTerm)) { + reporter.report(new HoleProblem.IllTypedError(lhs, meta.info, preRhs)); + return null; + } + } } case MetaInfo.Result(var expectedType) -> { if (providedType != null) { From 6a6b8d94d38922eb1d54c278a292aeacb18dcd1b Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 01:40:05 -0500 Subject: [PATCH 23/28] unify: properly handle `isType` --- .../main/java/org/aya/core/meta/MetaInfo.java | 14 ++++++++++++++ .../main/java/org/aya/tyck/unify/Unifier.java | 18 ++++++++++++------ 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/base/src/main/java/org/aya/core/meta/MetaInfo.java b/base/src/main/java/org/aya/core/meta/MetaInfo.java index 0ee33c3f16..7476358e5c 100644 --- a/base/src/main/java/org/aya/core/meta/MetaInfo.java +++ b/base/src/main/java/org/aya/core/meta/MetaInfo.java @@ -6,6 +6,7 @@ import org.aya.core.term.Term; import org.aya.generic.AyaDocile; import org.aya.pretty.doc.Doc; +import org.aya.tyck.unify.Synthesizer; import org.aya.util.prettier.PrettierOptions; import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; @@ -17,6 +18,7 @@ */ public sealed interface MetaInfo extends AyaDocile { @Nullable Term result(); + boolean isType(@NotNull Synthesizer synthesizer); /** * The type of the meta is known. * We shall check the solution against this type. @@ -25,6 +27,10 @@ record Result(@NotNull Term result) implements MetaInfo { @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) { return Doc.sep(Doc.symbol("?"), Doc.symbol(":"), result.toDoc(options)); } + + @Override public boolean isType(@NotNull Synthesizer synthesizer) { + return synthesizer.tryPress(result) instanceof SortTerm; + } } /** @@ -36,6 +42,10 @@ record AnyType() implements MetaInfo { return null; } + @Override public boolean isType(@NotNull Synthesizer synthesizer) { + return true; + } + @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) { return Doc.sep(Doc.plain("_"), Doc.symbols(":", "?")); } @@ -51,6 +61,10 @@ record PiDom(@NotNull SortTerm sort) implements MetaInfo { return null; } + @Override public boolean isType(@NotNull Synthesizer synthesizer) { + return true; + } + @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) { return Doc.sep(Doc.symbols("?", "->", "_", ":"), sort.toDoc(options)); } diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index 73d186ce9a..cf4fc2c737 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -96,14 +96,20 @@ public Unifier( reporter, false, false, traceBuilder, state, pos, ctx.deriveMap()), lr, rl); // Check the expected type. switch (meta.info) { + case MetaInfo.AnyType()when preRhs instanceof Formation -> {} + case MetaInfo.AnyType()when preRhs instanceof MetaTerm rhsMeta -> { + if (!rhsMeta.ref().info.isType(checker.synthesizer())) { + reporter.report(new HoleProblem.IllTypedError(lhs, meta.info, preRhs)); + return null; + } + } case MetaInfo.AnyType() -> { - if (!(preRhs instanceof Formation)) { - providedType = checker.synthesizer().synthesize(preRhs); - if (!(providedType instanceof SortTerm)) { - reporter.report(new HoleProblem.IllTypedError(lhs, meta.info, preRhs)); - return null; - } + var synthesize = checker.synthesizer().synthesize(preRhs); + if (!(synthesize instanceof SortTerm)) { + reporter.report(new HoleProblem.IllTypedError(lhs, meta.info, preRhs)); + return null; } + if (providedType == null) providedType = synthesize; } case MetaInfo.Result(var expectedType) -> { if (providedType != null) { From f62f7803c3c27845b53cbfa974634ccc5192c902 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 01:50:51 -0500 Subject: [PATCH 24/28] synth: call `whnf` back --- .../src/main/java/org/aya/tyck/unify/Synthesizer.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java index 7672fb493e..71c18531df 100644 --- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -57,7 +57,7 @@ public boolean inheritPiDom(@NotNull Term type, @NotNull SortTerm expected) { } /** - * @param preterm expected to be whnf + * @param preterm expected to be beta-normalized * @return null if failed to synthesize */ public @Nullable Term synthesize(@NotNull Term preterm) { @@ -67,7 +67,14 @@ public boolean inheritPiDom(@NotNull Term type, @NotNull SortTerm expected) { case Callable.DefCall call -> Def.defResult(call.ref()) .subst(DeltaExpander.buildSubst(Def.defTele(call.ref()), call.args())) .lift(call.ulift()); - case MetaTerm hole -> hole.ref().info.result(); + case MetaTerm hole -> { + var result = hole.ref().info.result(); + if (result == null) { + preterm = whnf(preterm); + yield preterm instanceof MetaTerm ? null : synthesize(preterm); + } + else yield result; + } case RefTerm.Field field -> Def.defType(field.ref()); case FieldTerm access -> { var callRaw = tryPress(access.of()); From b0ae9945edfddcef628c0b5c7fcae5a11678a372 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 02:06:00 -0500 Subject: [PATCH 25/28] synth: unify conditionally --- .../main/java/org/aya/tyck/ExprTycker.java | 2 +- .../main/java/org/aya/tyck/unify/Unifier.java | 26 ++++++++++++------- .../src/test/java/org/aya/core/SuedeTest.java | 3 +-- 3 files changed, 18 insertions(+), 13 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java index 2813004590..1f167b85ae 100644 --- a/base/src/main/java/org/aya/tyck/ExprTycker.java +++ b/base/src/main/java/org/aya/tyck/ExprTycker.java @@ -466,7 +466,7 @@ yield switch (whnf(term)) { var var = param.ref(); var lamParam = param.type(); var type = dt.param().type(); - var result = synthesize(lamParam).wellTyped(); + var result = ty(lamParam); if (unifyTyReported(result, type, lamParam)) type = result; else yield error(lam, dt); diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index cf4fc2c737..1160bffb7c 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -95,13 +95,15 @@ public Unifier( var checker = new DoubleChecker(new Unifier(Ordering.Lt, reporter, false, false, traceBuilder, state, pos, ctx.deriveMap()), lr, rl); // Check the expected type. + var needUnify = true; switch (meta.info) { - case MetaInfo.AnyType()when preRhs instanceof Formation -> {} + case MetaInfo.AnyType()when preRhs instanceof Formation -> needUnify = false; case MetaInfo.AnyType()when preRhs instanceof MetaTerm rhsMeta -> { if (!rhsMeta.ref().info.isType(checker.synthesizer())) { reporter.report(new HoleProblem.IllTypedError(lhs, meta.info, preRhs)); return null; } + needUnify = false; } case MetaInfo.AnyType() -> { var synthesize = checker.synthesizer().synthesize(preRhs); @@ -109,6 +111,7 @@ public Unifier( reporter.report(new HoleProblem.IllTypedError(lhs, meta.info, preRhs)); return null; } + needUnify = false; if (providedType == null) providedType = synthesize; } case MetaInfo.Result(var expectedType) -> { @@ -125,17 +128,20 @@ public Unifier( } } } - // Check the solution. - if (providedType != null) { - // resultTy might be an ErrorTerm, what to do? - if (!checker.inherit(preRhs, providedType)) - reporter.report(new HoleProblem.IllTypedError(lhs, new MetaInfo.Result(providedType), preRhs)); - } else { - providedType = checker.synthesizer().synthesize(preRhs); - if (providedType == null) { - throw new UnsupportedOperationException("TODO: add an error report for this"); + if (needUnify) { + // Check the solution. + if (providedType != null) { + // resultTy might be an ErrorTerm, what to do? + if (!checker.inherit(preRhs, providedType)) + reporter.report(new HoleProblem.IllTypedError(lhs, new MetaInfo.Result(providedType), preRhs)); + } else { + providedType = checker.synthesizer().synthesize(preRhs); + if (providedType == null) { + throw new UnsupportedOperationException("TODO: add an error report for this"); + } } } + if (!needUnify) providedType = SortTerm.Type0; // Pattern unification: buildSubst(lhs.args.invert(), meta.telescope) var subst = DeltaExpander.buildSubst(meta.contextTele, lhs.contextArgs()); var overlap = invertSpine(subst, lhs, meta); diff --git a/base/src/test/java/org/aya/core/SuedeTest.java b/base/src/test/java/org/aya/core/SuedeTest.java index ce83e71927..838155b404 100644 --- a/base/src/test/java/org/aya/core/SuedeTest.java +++ b/base/src/test/java/org/aya/core/SuedeTest.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; @@ -10,7 +10,6 @@ import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Test; -@SuppressWarnings("UnknownLanguage") public class SuedeTest { @Test public void nat() { suedeAll(""" From 0a999f8757e0016376a733a0c0553be6a1c7117f Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 02:16:36 -0500 Subject: [PATCH 26/28] synth: whnf more --- base/src/main/java/org/aya/tyck/error/HoleProblem.java | 4 ++-- base/src/main/java/org/aya/tyck/unify/Unifier.java | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/error/HoleProblem.java b/base/src/main/java/org/aya/tyck/error/HoleProblem.java index dba18077ec..e346300cd8 100644 --- a/base/src/main/java/org/aya/tyck/error/HoleProblem.java +++ b/base/src/main/java/org/aya/tyck/error/HoleProblem.java @@ -49,9 +49,9 @@ record IllTypedError( ) implements HoleProblem { @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { return Doc.vcat( - Doc.english("The meta (denoted ?) is supposed to satisfy"), + Doc.english("The meta (denoted ? below) is supposed to satisfy:"), Doc.par(1, result.toDoc(options)), - Doc.english("However, the solution below does not have the same type:"), + Doc.english("However, the solution below does not seem so:"), Doc.par(1, solution.toDoc(options)) ); } diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index 1160bffb7c..c353c86d77 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -106,7 +106,7 @@ public Unifier( needUnify = false; } case MetaInfo.AnyType() -> { - var synthesize = checker.synthesizer().synthesize(preRhs); + var synthesize = checker.synthesizer().tryPress(preRhs); if (!(synthesize instanceof SortTerm)) { reporter.report(new HoleProblem.IllTypedError(lhs, meta.info, preRhs)); return null; From e20b911c1b74d29e96410cbb49800209e18390cb Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 02:20:11 -0500 Subject: [PATCH 27/28] unify: guard error terms --- base/src/main/java/org/aya/tyck/unify/Unifier.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java index c353c86d77..1fa29c5463 100644 --- a/base/src/main/java/org/aya/tyck/unify/Unifier.java +++ b/base/src/main/java/org/aya/tyck/unify/Unifier.java @@ -96,7 +96,8 @@ public Unifier( reporter, false, false, traceBuilder, state, pos, ctx.deriveMap()), lr, rl); // Check the expected type. var needUnify = true; - switch (meta.info) { + if (preRhs instanceof ErrorTerm) needUnify = false; + else switch (meta.info) { case MetaInfo.AnyType()when preRhs instanceof Formation -> needUnify = false; case MetaInfo.AnyType()when preRhs instanceof MetaTerm rhsMeta -> { if (!rhsMeta.ref().info.isType(checker.synthesizer())) { @@ -141,7 +142,7 @@ public Unifier( } } } - if (!needUnify) providedType = SortTerm.Type0; + if (!needUnify && providedType == null) providedType = SortTerm.Type0; // Pattern unification: buildSubst(lhs.args.invert(), meta.telescope) var subst = DeltaExpander.buildSubst(meta.contextTele, lhs.contextArgs()); var overlap = invertSpine(subst, lhs, meta); From 1ecad86cd5dc4cb9fc80157464922632006c4b2d Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 07:26:51 +0000 Subject: [PATCH 28/28] tests: add negative fixtures --- .../resources/failure/holes/pi-dom-meta.aya | 5 +++ .../failure/holes/pi-dom-meta.aya.txt | 38 +++++++++++++++++++ .../test/resources/failure/holes/pi-dom.aya | 4 ++ .../resources/failure/holes/pi-dom.aya.txt | 14 +++++++ 4 files changed, 61 insertions(+) create mode 100644 base/src/test/resources/failure/holes/pi-dom-meta.aya create mode 100644 base/src/test/resources/failure/holes/pi-dom-meta.aya.txt create mode 100644 base/src/test/resources/failure/holes/pi-dom.aya create mode 100644 base/src/test/resources/failure/holes/pi-dom.aya.txt diff --git a/base/src/test/resources/failure/holes/pi-dom-meta.aya b/base/src/test/resources/failure/holes/pi-dom-meta.aya new file mode 100644 index 0000000000..bf0d608de6 --- /dev/null +++ b/base/src/test/resources/failure/holes/pi-dom-meta.aya @@ -0,0 +1,5 @@ +data X : Set +data infix = (a b : X) : Set + +data Test : Type +| con (x : _) (y : X) (x = y) diff --git a/base/src/test/resources/failure/holes/pi-dom-meta.aya.txt b/base/src/test/resources/failure/holes/pi-dom-meta.aya.txt new file mode 100644 index 0000000000..71fd4af59a --- /dev/null +++ b/base/src/test/resources/failure/holes/pi-dom-meta.aya.txt @@ -0,0 +1,38 @@ +In file $FILE:5:19 -> + + 3 │ + 4 │ data Test : Type + 5 │ | con (x : _) (y : X) (x = y) + │ ╰╯ + +Error: The type + X + is in the domain of a function whose type is + Type 0 + +In file $FILE:5:11 -> + + 3 │ + 4 │ data Test : Type + 5 │ | con (x : _) (y : X) (x = y) + │ ╰╯ + +Error: The meta (denoted ? below) is supposed to satisfy: + ? → _ : Type 0 + However, the solution below does not seem so: + X + +In file $FILE:5:23 -> + + 3 │ + 4 │ data Test : Type + 5 │ | con (x : _) (y : X) (x = y) + │ ╰───╯ + +Error: The type + x = y + is in the domain of a function whose type is + Type 0 + +3 error(s), 0 warning(s). +What are you doing? diff --git a/base/src/test/resources/failure/holes/pi-dom.aya b/base/src/test/resources/failure/holes/pi-dom.aya new file mode 100644 index 0000000000..b8e825fb99 --- /dev/null +++ b/base/src/test/resources/failure/holes/pi-dom.aya @@ -0,0 +1,4 @@ +data X : Set + +data Test : Type +| con X diff --git a/base/src/test/resources/failure/holes/pi-dom.aya.txt b/base/src/test/resources/failure/holes/pi-dom.aya.txt new file mode 100644 index 0000000000..36f7ef888b --- /dev/null +++ b/base/src/test/resources/failure/holes/pi-dom.aya.txt @@ -0,0 +1,14 @@ +In file $FILE:4:6 -> + + 2 │ + 3 │ data Test : Type + 4 │ | con X + │ ╰╯ + +Error: The type + X + is in the domain of a function whose type is + Type 0 + +1 error(s), 0 warning(s). +What are you doing?