Skip to content

Commit

Permalink
pat: improve iterators
Browse files Browse the repository at this point in the history 
no more nullable
stage(s)
  • Loading branch information
@HoshinoTented @ice1000
HoshinoTented authored and ice1000 committed Jan 4, 2025
1 parent 6b9ab24 commit 148a827
Show file tree
Hide file tree
Showing 11 changed files with 185 additions and 171 deletions.
14 changes: 6 additions & 8 deletions base/src/main/java/org/aya/tyck/ExprTycker.java
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
// Copyright (c) 2020-2025 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;

Expand Down Expand Up @@ -33,7 +33,6 @@
import org.aya.syntax.core.term.xtt.PAppTerm;
import org.aya.syntax.ref.*;
import org.aya.syntax.telescope.AbstractTele;
import org.aya.syntax.telescope.Signature;
import org.aya.tyck.ctx.LocalLet;
import org.aya.tyck.error.*;
import org.aya.tyck.pat.ClauseTycker;
Expand Down Expand Up @@ -184,15 +183,14 @@ && whnf(type) instanceof DataCall dataCall
ImmutableSeq<WithPos<Expr>> discriminant, @NotNull SourcePos exprPos,
ImmutableSeq<Pattern.Clause> clauses, ImmutableSeq<Jdg> wellArgs, Term type
) {
var telescope = new AbstractTele.Locns(
wellArgs.map(x -> new Param(Constants.ANONYMOUS_PREFIX, x.type(), true)),
type);
var signature = new Signature(telescope, discriminant.map(WithPos::sourcePos));
var telescope = wellArgs.map(x -> new Param(Constants.ANONYMOUS_PREFIX, x.type(), true));
var clauseTycker = new ClauseTycker.Worker(
new ClauseTycker(this),
// always nameless
telescope,
new DepTypeTerm.UnpiRaw(ImmutableSeq.empty(), type),
ImmutableSeq.fill(discriminant.size(), i -> new LocalVar("match" + i)),
signature, clauses, ImmutableSeq.empty(), true);
ImmutableSeq.empty(),
clauses, true);
var wellClauses = clauseTycker.check(exprPos)
.wellTyped()
.map(WithPos::data);
Expand Down
16 changes: 10 additions & 6 deletions base/src/main/java/org/aya/tyck/StmtTycker.java
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
// Copyright (c) 2020-2025 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;

Expand Down Expand Up @@ -33,6 +33,7 @@
import org.aya.tyck.pat.IApplyConfl;
import org.aya.tyck.pat.PatClassifier;
import org.aya.tyck.pat.YouTrack;
import org.aya.tyck.pat.iter.SignatureIterator;
import org.aya.tyck.tycker.Problematic;
import org.aya.tyck.tycker.TeleTycker;
import org.aya.unify.Synthesizer;
Expand Down Expand Up @@ -105,8 +106,11 @@ yield switch (fnDecl.body) {

var signature = fnRef.signature;
// we do not load signature here, so we need a fresh ExprTycker
var clauseTycker = new ClauseTycker.Worker(new ClauseTycker(tycker = mkTycker()),
teleVars, signature, clauses, elims, true);
tycker = mkTycker();
var unpi = DepTypeTerm.unpiDBI(signature.result(), tycker::whnf);
var clauseTycker = new ClauseTycker.Worker(new ClauseTycker(tycker),
signature.params(), unpi,
teleVars, elims, clauses, true);

var orderIndependent = fnDecl.modifiers.contains(Modifier.Overlap);
FnDef def;
Expand Down Expand Up @@ -180,7 +184,7 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(),
if (fn.body instanceof FnBody.BlockBody body) {
tycker.solveMetas();
var zonker = new Finalizer.Zonk<>(tycker);
fnRef.signature = fnRef.signature.pusheen(tycker::whnf).descent(zonker::zonk);
fnRef.signature = fnRef.signature.descent(zonker::zonk);
if (fnRef.signature.params().isEmpty() && body.clauses().isEmpty())
fail(new NobodyError(decl.sourcePos(), fn.ref));
}
Expand Down Expand Up @@ -244,9 +248,9 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
if (con.patterns.isNotEmpty()) {
var resolvedElim = dataRef.concrete.body.elims();
assert resolvedElim != null;
var indicies = ClauseTycker.Worker.computeIndices(ownerBinds, resolvedElim);
// do not do coverage check
var lhsResult = new ClauseTycker(tycker = mkTycker()).checkLhs(dataSig, indicies,
var lhsResult = new ClauseTycker(tycker = mkTycker()).checkLhs(
SignatureIterator.make(dataSig.params(), new DepTypeTerm.UnpiRaw(dataSig.result()), ownerBinds, resolvedElim),
new Pattern.Clause(con.entireSourcePos(), con.patterns, Option.none()), false);
if (lhsResult.hasError()) {
return;
Expand Down
82 changes: 37 additions & 45 deletions base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,9 @@
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
// Copyright (c) 2020-2025 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;

import kala.collection.SeqView;
import kala.collection.immutable.ImmutableSeq;
import kala.collection.immutable.primitive.ImmutableIntSeq;
import kala.value.primitive.MutableBooleanValue;
import org.aya.generic.Renamer;
import org.aya.normalize.Finalizer;
Expand All @@ -14,17 +13,17 @@
import org.aya.syntax.core.Jdg;
import org.aya.syntax.core.pat.Pat;
import org.aya.syntax.core.pat.TypeEraser;
import org.aya.syntax.core.term.ErrorTerm;
import org.aya.syntax.core.term.MetaPatTerm;
import org.aya.syntax.core.term.Param;
import org.aya.syntax.core.term.Term;
import org.aya.syntax.core.term.*;
import org.aya.syntax.ref.LocalCtx;
import org.aya.syntax.ref.LocalVar;
import org.aya.syntax.telescope.Signature;
import org.aya.syntax.telescope.AbstractTele;
import org.aya.tyck.ExprTycker;
import org.aya.tyck.TyckState;
import org.aya.tyck.ctx.LocalLet;
import org.aya.tyck.error.PatternProblem;
import org.aya.tyck.pat.iter.LambdaPusheen;
import org.aya.tyck.pat.iter.PatternIterator;
import org.aya.tyck.pat.iter.SignatureIterator;
import org.aya.tyck.tycker.Problematic;
import org.aya.tyck.tycker.Stateful;
import org.aya.util.error.Panic;
Expand All @@ -33,8 +32,8 @@
import org.aya.util.reporter.Reporter;
import org.jetbrains.annotations.Contract;
import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;

import java.util.function.Supplier;
import java.util.function.UnaryOperator;

public final class ClauseTycker implements Problematic, Stateful {
Expand All @@ -61,14 +60,19 @@ public record TyckResult(
*/
public record LhsResult(
@NotNull LocalCtx localCtx,
@NotNull Term type,
@NotNull AbstractTele.Locns newSignature,
@NotNull ImmutableSeq<LocalVar> allBinds,
@NotNull ImmutableSeq<Pat> freePats,
@NotNull ImmutableSeq<Jdg> paramSubst,
@NotNull LocalLet asSubst,
@NotNull Pat.Preclause<Expr> clause,
boolean hasError
) {
public @NotNull Term instType() {
// I guess we need not to inline this term even we did before. The [paramSubst] is already inlined.
return newSignature.result().instTele(paramSubst.view().map(Jdg::wellTyped));
}

@Contract(mutates = "param2")
public void addLocalLet(@NotNull ImmutableSeq<LocalVar> teleBinds, @NotNull ExprTycker exprTycker) {
teleBinds.forEachWith(paramSubst, exprTycker.localLet()::put);
Expand All @@ -78,44 +82,40 @@ public void addLocalLet(@NotNull ImmutableSeq<LocalVar> teleBinds, @NotNull Expr

public record Worker(
@NotNull ClauseTycker parent,
@NotNull ImmutableSeq<Param> telescope,
@NotNull DepTypeTerm.UnpiRaw unpi,
@NotNull ImmutableSeq<LocalVar> teleVars,
@NotNull Signature signature,
@NotNull ImmutableSeq<Pattern.Clause> clauses,
@NotNull ImmutableSeq<LocalVar> elims,
@NotNull ImmutableSeq<Pattern.Clause> clauses,
boolean isFn
) {
public @NotNull TyckResult check(@NotNull SourcePos overallPos) {
var lhsResult = parent.checkAllLhs(computeIndices(), signature, clauses.view(), isFn);
var lhsResult = checkAllLhs();

if (lhsResult.noneMatch(r -> r.hasError)) {
var classes = PatClassifier.classify(lhsResult.view().map(LhsResult::clause),
signature.params().view(), parent.exprTycker, overallPos);
// TODO: max(lhsResult.signature.telescope by size)
telescope.view().concat(unpi.params()), parent.exprTycker, overallPos);
if (clauses.isNotEmpty()) {
var usages = PatClassifier.firstMatchDomination(clauses, parent, classes);
// refinePatterns(lhsResults, usages, classes);
}
}

lhsResult = lhsResult.map(cl -> new LhsResult(cl.localCtx, cl.type, cl.allBinds,
lhsResult = lhsResult.map(cl -> new LhsResult(cl.localCtx, cl.newSignature, cl.allBinds,
cl.freePats.map(TypeEraser::erase),
cl.paramSubst, cl.asSubst, cl.clause, cl.hasError));
return parent.checkAllRhs(teleVars, lhsResult);
}

private @Nullable ImmutableIntSeq computeIndices() {
return computeIndices(teleVars, elims);
public @NotNull ImmutableSeq<LhsResult> checkAllLhs() {
return parent.checkAllLhs(() ->
SignatureIterator.make(telescope, unpi, teleVars, elims),
clauses.view(), isFn);
}

public @NotNull TyckResult checkNoClassify() {
return parent.checkAllRhs(teleVars, parent.checkAllLhs(computeIndices(), signature, clauses.view(), isFn));
}

public static @Nullable ImmutableIntSeq computeIndices(
@NotNull ImmutableSeq<LocalVar> teleVars,
@NotNull ImmutableSeq<LocalVar> elims
) {
return elims.isEmpty() ? null : elims.mapToInt(ImmutableIntSeq.factory(),
teleVars::indexOf);
return parent.checkAllRhs(teleVars, checkAllLhs());
}
}

Expand All @@ -125,10 +125,10 @@ public record Worker(
// region tycking

public @NotNull ImmutableSeq<LhsResult> checkAllLhs(
@Nullable ImmutableIntSeq indices, @NotNull Signature signature,
@NotNull Supplier<SignatureIterator> sigIter,
@NotNull SeqView<Pattern.Clause> clauses, boolean isFn
) {
return clauses.map(c -> checkLhs(signature, indices, c, isFn)).toImmutableSeq();
return clauses.map(c -> checkLhs(sigIter.get(), c, isFn)).toImmutableSeq();
}

public @NotNull TyckResult checkAllRhs(
Expand All @@ -149,12 +149,11 @@ public record Worker(
}

public @NotNull LhsResult checkLhs(
@NotNull Signature signature,
@Nullable ImmutableIntSeq indices,
@NotNull SignatureIterator sigIter,
@NotNull Pattern.Clause clause,
boolean isFn
) {
var tycker = newPatternTycker(indices, signature.params().view());
var tycker = newPatternTycker(sigIter, sigIter.elims != null);
try (var _ = exprTycker.subscope()) {
// If a pattern occurs in elimination environment, then we check if it contains absurd pattern.
// If it is not the case, the pattern must be accompanied by a body.
Expand All @@ -163,12 +162,12 @@ public record Worker(
exprTycker.fail(new PatternProblem.InvalidEmptyBody(clause));
}

var patResult = tycker.tyck(clause.patterns.view(), null, clause.expr.getOrNull());
var patIter = new PatternIterator(clause.patterns, clause.expr.isDefined() ? new LambdaPusheen(clause.expr.get()) : PatternIterator.DUMMY);
var patResult = tycker.tyck(patIter, null);
var ctx = exprTycker.localCtx(); // No need to copy the context here

clause.hasError |= patResult.hasError();
patResult = inline(patResult, ctx);
var resultTerm = signature.result().instTele(patResult.paramSubstObj()).descent(new TermInline());
clause.patterns.view().map(it -> it.term().data()).forEach(TermInPatInline::apply);

// It is safe to replace ctx:
Expand All @@ -179,8 +178,8 @@ public record Worker(

var allBinds = patWithTypeBound.component1().toImmutableSeq();
var newClause = new Pat.Preclause<>(clause.sourcePos, patWithTypeBound.component2(),
allBinds.size(), patResult.newBody());
return new LhsResult(ctx, resultTerm, allBinds,
allBinds.size(), patIter.exprBody());
return new LhsResult(ctx, sigIter.signature(), allBinds,
patResult.wellTyped(), patResult.paramSubst(), patResult.asSubst(), newClause, patResult.hasError());
}
}
Expand Down Expand Up @@ -211,7 +210,7 @@ else if (result.hasError) {
exprTycker.setLocalCtx(result.localCtx);
result.addLocalLet(teleBinds, exprTycker);
// now exprTycker has all substitutions that PatternTycker introduced.
wellBody = exprTycker.inherit(bodyExpr, result.type).wellTyped();
wellBody = exprTycker.inherit(bodyExpr, result.instType()).wellTyped();
exprTycker.solveMetas();
wellBody = zonker.zonk(wellBody);

Expand All @@ -230,15 +229,8 @@ else if (result.hasError) {

// region util

private @NotNull PatternTycker newPatternTycker(
@Nullable ImmutableIntSeq indices,
@NotNull SeqView<Param> telescope
) {
telescope = indices != null
? telescope.mapIndexed((idx, p) -> indices.contains(idx) ? p.explicitize() : p.implicitize())
: telescope;

return new PatternTycker(exprTycker, telescope, new LocalLet(), indices == null,
private @NotNull PatternTycker newPatternTycker(@NotNull SignatureIterator sigIter, boolean hasElim) {
return new PatternTycker(exprTycker, sigIter, new LocalLet(), !hasElim,
new Renamer());
}

Expand Down Expand Up @@ -305,7 +297,7 @@ public static void apply(@NotNull Pattern pat) {
// map in place 😱😱😱😱
result.asSubst().subst().replaceAll((_, t) -> inlineTerm(t));

return new PatternTycker.TyckResult(wellTyped, paramSubst, result.asSubst(), result.newBody(), result.hasError());
return new PatternTycker.TyckResult(wellTyped, paramSubst, result.asSubst(), result.hasError());
}

// endregion post tycking
Expand Down
38 changes: 18 additions & 20 deletions base/src/main/java/org/aya/tyck/pat/IApplyConfl.java
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
// Copyright (c) 2020-2025 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;

Expand All @@ -20,25 +20,23 @@

import java.util.function.UnaryOperator;

/**
* This is XTT-specific confluence check, very simple: we check for all combinations.
* So, if we do
* <pre>
* def infix + (a b : Int) : Int
* | zro i, zro j => u
* </pre>
* This thing will check the following:
* <ul>
* <li><code>zro 0, zro 0</code></li>
* <li><code>zro 0, zro 1</code></li>
* <li><code>zro 1, zro 1</code></li>
* <li><code>zro 1, zro 0</code></li>
* </ul>
* In proper cubical type theory, we need to check <code>zro 0, zro j</code> and <code>zro i, zro 0</code>.
* The latter looks like smaller number of checks, but honestly I don't know how to do it in terms of
* pure patterns. The old version of Aya used a hack based on object identity, and I don't like it.
* This one is translatable to a purely functional programming language.
*/
/// This is XTT-specific confluence check, very simple: we check for all combinations.
/// So, if we do
/// ```
/// def infix + (a b : Int) : Int
/// | zro i, zro j => u
///```
/// This thing will check the following:
///
/// - `zro 0, zro 0`
/// - `zro 0, zro 1`
/// - `zro 1, zro 1`
/// - `zro 1, zro 0`
///
/// In proper cubical type theory, we need to check `zro 0, zro j` and `zro i, zro 0`.
/// The latter looks like smaller number of checks, but honestly I don't know how to do it in terms of
/// pure patterns. The old version of Aya used a hack based on object identity, and I don't like it.
/// This one is translatable to a purely functional programming language.
public record IApplyConfl(
@NotNull FnDef def, @NotNull ImmutableSeq<WithPos<Term.Matching>> matchings,
boolean orderIndep, @NotNull SourcePos sourcePos, @NotNull ExprTycker tycker
Expand Down
Loading

0 comments on commit 148a827

Please sign in to comment.