Skip to content

Commit 8b7d721

Browse files
ice1000ice1000
committed
merge: branch 'main' into 1128
# Conflicts: # syntax/src/main/java/org/aya/prettier/CorePrettier.java
2 parents d358e0a + 0830357 commit 8b7d721

File tree

29 files changed

+430
-216
lines changed

29 files changed

+430
-216
lines changed

Diff for: ‎base/src/main/java/org/aya/normalize/Normalizer.java

+8-9
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,12 @@
1-
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
1+
// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
22
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
33
package org.aya.normalize;
44

5+
import java.util.function.BiFunction;
6+
import java.util.function.UnaryOperator;
7+
8+
import static org.aya.generic.State.Stuck;
9+
510
import kala.collection.SeqView;
611
import kala.collection.immutable.ImmutableSeq;
712
import kala.collection.immutable.ImmutableSet;
@@ -25,15 +30,9 @@
2530
import org.aya.syntax.ref.LocalVar;
2631
import org.aya.tyck.TyckState;
2732
import org.aya.tyck.tycker.Stateful;
28-
import org.aya.util.error.WithPos;
2933
import org.jetbrains.annotations.NotNull;
3034
import org.jetbrains.annotations.Nullable;
3135

32-
import java.util.function.BiFunction;
33-
import java.util.function.UnaryOperator;
34-
35-
import static org.aya.generic.State.Stuck;
36-
3736
/**
3837
* Unlike in pre-v0.30 Aya, we use only one normalizer, only doing head reduction,
3938
* and we merge conservative normalizer and the whnf normalizer.
@@ -92,8 +91,8 @@ case FnCall(FnDef.Delegate delegate, int ulift, var args) -> {
9291
term = body.instTele(args.view());
9392
continue;
9493
}
95-
case Either.Right(var clauses): {
96-
var result = tryUnfoldClauses(clauses.view().map(WithPos::data),
94+
case Either.Right(var body): {
95+
var result = tryUnfoldClauses(body.matchingsView(),
9796
args, core.is(Modifier.Overlap), ulift);
9897
// we may get stuck
9998
if (result == null) return defaultValue;

Diff for: ‎base/src/main/java/org/aya/primitive/ShapeMatcher.java

+8-9
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,12 @@
1-
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
1+
// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
22
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
33
package org.aya.primitive;
44

5+
import java.util.Objects;
6+
import java.util.function.BiPredicate;
7+
import java.util.function.BooleanSupplier;
8+
import java.util.function.Function;
9+
510
import kala.collection.SeqLike;
611
import kala.collection.immutable.ImmutableMap;
712
import kala.collection.immutable.ImmutableSeq;
@@ -24,15 +29,9 @@
2429
import org.aya.util.Pair;
2530
import org.aya.util.RepoLike;
2631
import org.aya.util.error.Panic;
27-
import org.aya.util.error.WithPos;
2832
import org.jetbrains.annotations.NotNull;
2933
import org.jetbrains.annotations.Nullable;
3034

31-
import java.util.Objects;
32-
import java.util.function.BiPredicate;
33-
import java.util.function.BooleanSupplier;
34-
import java.util.function.Function;
35-
3635
/**
3736
* @author kiva
3837
*/
@@ -123,10 +122,10 @@ private boolean matchFn(@NotNull FnShape shape, @NotNull FnDef def) {
123122
return switch (new Pair<>(shape.body(), def.body())) {
124123
case Pair(Either.Left(var termShape), Either.Left(var term)) ->
125124
matchInside(() -> captures.put(shape.name(), def.ref()), () -> matchTerm(termShape, term));
126-
case Pair(Either.Right(var clauseShapes), Either.Right(var clauses)) -> {
125+
case Pair(Either.Right(var clauseShapes), Either.Right(var body)) -> {
127126
var mode = def.is(Modifier.Overlap) ? MatchMode.Sub : MatchMode.Eq;
128127
yield matchInside(() -> captures.put(shape.name(), def.ref()), () ->
129-
matchMany(mode, clauseShapes, clauses.view().map(WithPos::data), this::matchClause));
128+
matchMany(mode, clauseShapes, body.matchingsView(), this::matchClause));
130129
}
131130
default -> false;
132131
};

Diff for: ‎base/src/main/java/org/aya/resolve/salt/Desalt.java

+38-1
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
1-
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
1+
// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
22
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
33
package org.aya.resolve.salt;
44

5+
import kala.collection.immutable.ImmutableSeq;
56
import org.aya.generic.term.SortKind;
67
import org.aya.resolve.ResolveInfo;
78
import org.aya.syntax.concrete.Expr;
89
import org.aya.syntax.concrete.Pattern;
10+
import org.aya.syntax.ref.LocalVar;
911
import org.aya.util.error.Panic;
1012
import org.aya.util.error.PosedUnaryOperator;
1113
import org.aya.util.error.SourcePos;
@@ -70,6 +72,41 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
7072
case Expr.Idiom idiom -> throw new UnsupportedOperationException("TODO");
7173
case Expr.RawSort(var kind) -> new Expr.Sort(kind, 0);
7274
case Expr.LetOpen letOpen -> apply(letOpen.body());
75+
case Expr.ClauseLam lam -> {
76+
var isVanilla = lam.patterns().allMatch(x -> x.term().data() instanceof Pattern.BindLike);
77+
78+
ImmutableSeq<LocalVar> lamTele;
79+
WithPos<Expr> realBody;
80+
81+
if (isVanilla) {
82+
// fn a _ c => ...
83+
lamTele = lam.patterns().map(x -> ((Pattern.BindLike) x.term().data()).toLocalVar(x.term().sourcePos()));
84+
realBody = lam.body();
85+
} else {
86+
lamTele = lam.patterns().mapIndexed((idx, pat) -> {
87+
if (pat.term().data() instanceof Pattern.BindLike bindLike) {
88+
var bind = bindLike.toLocalVar(pat.term().sourcePos());
89+
// we need fresh bind, since [bind] may be used in the body.
90+
return LocalVar.generate(bind.name(), SourcePos.NONE);
91+
} else {
92+
return LocalVar.generate("IrrefutableLam" + idx, SourcePos.NONE);
93+
}
94+
});
95+
96+
// fn a' _ c' => match a', _, c' { a, _, (con c) => ... }
97+
// the var with prime are renamed vars
98+
99+
realBody = new WithPos<>(sourcePos, new Expr.Match(
100+
lamTele.map(x -> new WithPos<>(x.definition(), new Expr.Ref(x))),
101+
ImmutableSeq.of(lam.clause()),
102+
ImmutableSeq.empty(),
103+
true,
104+
null
105+
));
106+
}
107+
108+
yield apply(Expr.buildLam(sourcePos, lamTele.view(), realBody));
109+
}
73110
};
74111
}
75112
public @NotNull PosedUnaryOperator<Pattern> pattern = new Pat();

Diff for: ‎base/src/main/java/org/aya/resolve/visitor/ExprResolver.java

+7-7
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
1+
// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
22
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
33
package org.aya.resolve.visitor;
44

@@ -30,7 +30,6 @@
3030
import org.aya.util.error.WithPos;
3131
import org.jetbrains.annotations.Contract;
3232
import org.jetbrains.annotations.NotNull;
33-
import org.jetbrains.annotations.Nullable;
3433

3534
/**
3635
* Resolves bindings.
@@ -116,11 +115,7 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
116115
return switch (pre(expr)) {
117116
case Expr.Do doExpr ->
118117
doExpr.update(apply(SourcePos.NONE, doExpr.bindName()), bind(doExpr.binds(), MutableValue.create(ctx)));
119-
case Expr.Lambda lam -> {
120-
var mCtx = MutableValue.create(ctx);
121-
mCtx.update(ctx -> ctx.bind(lam.ref()));
122-
yield lam.update(lam.body().descent(enter(mCtx.get())));
123-
}
118+
case Expr.ClauseLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
124119
case Expr.DepType depType -> {
125120
var mCtx = MutableValue.create(ctx);
126121
var param = bind(depType.param(), mCtx);
@@ -202,6 +197,8 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
202197
yield match.update(discriminant, clauses, returns);
203198
}
204199

200+
// Expr.Lambda is a desugar target, which is produced after resolving.
201+
case Expr.Lambda _ -> Panic.unreachable();
205202
case Expr newExpr -> newExpr.descent(this);
206203
};
207204
}
@@ -235,6 +232,9 @@ private void addReference(@NotNull DefVar<?, ?> defVar) {
235232
return clause.update(pats, body);
236233
}
237234

235+
/// Resolve a [Pattern]
236+
///
237+
/// @param telescope the telescope of the clause which the {@param pattern} lives, can be [ImmutableSeq#empty()].
238238
public @NotNull WithPos<Pattern> resolvePattern(@NotNull WithPos<Pattern> pattern, @NotNull ImmutableSeq<LocalVar> telescope, MutableValue<Context> ctx) {
239239
var resolver = new PatternResolver(ctx.get(), telescope, this::addReference);
240240
var result = pattern.descent(resolver);

Diff for: ‎base/src/main/java/org/aya/terck/CallResolver.java

+5-6
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
1-
// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
1+
// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
22
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
33
package org.aya.terck;
44

5+
import java.util.function.Consumer;
6+
57
import kala.collection.Set;
68
import kala.collection.immutable.ImmutableSeq;
79
import kala.collection.immutable.ImmutableSet;
@@ -22,14 +24,11 @@
2224
import org.aya.syntax.core.term.xtt.PAppTerm;
2325
import org.aya.tyck.TyckState;
2426
import org.aya.tyck.tycker.Stateful;
25-
import org.aya.util.error.WithPos;
2627
import org.aya.util.terck.CallGraph;
2728
import org.aya.util.terck.CallMatrix;
2829
import org.aya.util.terck.Relation;
2930
import org.jetbrains.annotations.NotNull;
3031

31-
import java.util.function.Consumer;
32-
3332
/**
3433
* Resolve calls and build call graph of recursive functions,
3534
* after {@link org.aya.tyck.StmtTycker}.
@@ -139,8 +138,8 @@ private Relation compareConArgs(@NotNull ImmutableSeq<Term> conArgs, @NotNull Pa
139138
}
140139

141140
public void check() {
142-
var clauses = caller.body().getRightValue();
143-
clauses.view().map(WithPos::data).forEach(this);
141+
var clauses = caller.body().getRightValue().matchingsView();
142+
clauses.forEach(this);
144143
}
145144

146145
@Override public void accept(@NotNull Term.Matching matching) {

Diff for: ‎base/src/main/java/org/aya/tyck/ExprTycker.java

+7-8
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,10 @@
22
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
33
package org.aya.tyck;
44

5+
import java.util.Comparator;
6+
import java.util.function.BiFunction;
7+
import java.util.function.Function;
8+
59
import kala.collection.immutable.ImmutableSeq;
610
import kala.collection.immutable.ImmutableTreeSeq;
711
import kala.collection.mutable.MutableList;
@@ -50,10 +54,6 @@
5054
import org.jetbrains.annotations.NotNull;
5155
import org.jetbrains.annotations.Nullable;
5256

53-
import java.util.Comparator;
54-
import java.util.function.BiFunction;
55-
import java.util.function.Function;
56-
5757
public final class ExprTycker extends AbstractTycker implements Unifiable {
5858
public final @NotNull MutableTreeSet<WithPos<Expr.WithTerm>> withTerms =
5959
MutableTreeSet.create(Comparator.comparing(SourceNode::sourcePos));
@@ -191,9 +191,7 @@ && whnf(type) instanceof DataCall dataCall
191191
ImmutableSeq.fill(discriminant.size(), i ->
192192
new LocalVar("match" + i, discriminant.get(i).sourcePos(), GenerateKind.Basic.Tyck)),
193193
ImmutableSeq.empty(), clauses);
194-
var wellClauses = clauseTycker.check(exprPos)
195-
.wellTyped()
196-
.map(WithPos::data);
194+
var wellClauses = clauseTycker.check(exprPos).wellTyped().matchingsView();
197195

198196
// Find free occurrences
199197
var usages = new FreeCollector();
@@ -204,7 +202,8 @@ && whnf(type) instanceof DataCall dataCall
204202
var captures = usages.collected();
205203
var lifted = new Matchy(type.bindTele(wellArgs.size(), captures.view()),
206204
new QName(QPath.fileLevel(fileModule), "match-" + exprPos.lineColumnString()),
207-
wellClauses.map(clause -> clause.update(clause.body().bindTele(clause.bindCount(), captures.view()))));
205+
wellClauses.map(clause -> clause.update(clause.body().bindTele(clause.bindCount(), captures.view())))
206+
.toImmutableSeq());
208207

209208
var wellTerms = wellArgs.map(Jdg::wellTyped);
210209
return new MatchCall(lifted, wellTerms, captures.map(FreeTerm::new));

Diff for: ‎base/src/main/java/org/aya/tyck/StmtTycker.java

+23-14
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
33
package org.aya.tyck;
44

5+
import static org.aya.tyck.tycker.TeleTycker.loadTele;
6+
57
import kala.collection.immutable.ImmutableSeq;
68
import kala.control.Either;
79
import kala.control.Option;
@@ -44,8 +46,6 @@
4446
import org.jetbrains.annotations.NotNull;
4547
import org.jetbrains.annotations.Nullable;
4648

47-
import static org.aya.tyck.tycker.TeleTycker.loadTele;
48-
4949
public record StmtTycker(
5050
@NotNull SuppressingReporter reporter, @NotNull ModulePath fileModule,
5151
@NotNull ShapeFactory shapeFactory, @NotNull PrimFactory primFactory
@@ -85,8 +85,6 @@ public void suppress(@NotNull Decl decl) {
8585
case FnDecl fnDecl -> {
8686
var fnRef = fnDecl.ref;
8787
assert fnRef.signature != null;
88-
89-
var factory = FnDef.factory(body -> new FnDef(fnRef, fnDecl.modifiers, body));
9088
var teleVars = fnDecl.telescope.map(Expr.Param::ref);
9189

9290
yield switch (fnDecl.body) {
@@ -100,7 +98,7 @@ yield switch (fnDecl.body) {
10098
var zonker = new Finalizer.Zonk<>(tycker);
10199
var resultTerm = zonker.zonk(result).bindTele(teleVars.view());
102100
fnRef.signature = fnRef.signature.descent(zonker::zonk);
103-
yield factory.apply(Either.left(resultTerm));
101+
yield new FnDef(fnRef, fnDecl.modifiers, Either.left(resultTerm));
104102
}
105103
case FnBody.BlockBody body -> {
106104
var clauses = body.clauses();
@@ -119,22 +117,33 @@ yield switch (fnDecl.body) {
119117

120118
var orderIndependent = fnDecl.modifiers.contains(Modifier.Overlap);
121119
FnDef def;
122-
ClauseTycker.TyckResult patResult;
120+
boolean hasLhsError;
121+
FnClauseBody coreBody;
123122
if (orderIndependent) {
124123
// Order-independent.
125-
patResult = clauseTycker.checkNoClassify();
126-
def = factory.apply(Either.right(patResult.wellTyped()));
127-
if (!patResult.hasLhsError()) {
124+
var patResult = clauseTycker.checkNoClassify();
125+
coreBody = new FnClauseBody(patResult.wellTyped());
126+
def = new FnDef(fnRef, fnDecl.modifiers, Either.right(coreBody));
127+
hasLhsError = patResult.hasLhsError();
128+
if (!hasLhsError) {
128129
var rawParams = signature.params();
129130
var confluence = new YouTrack(rawParams, tycker, fnDecl.sourcePos());
130-
confluence.check(patResult, signature.result(),
131-
PatClassifier.classify(patResult.clauses().view(), rawParams.view(), tycker, fnDecl.sourcePos()));
131+
var classes = PatClassifier.classify(patResult.clauses().view(),
132+
rawParams.view(), tycker, fnDecl.sourcePos());
133+
var absurds = patResult.absurdPrefixCount();
134+
coreBody.classes = classes.map(cls -> cls.ignoreAbsurd(absurds));
135+
confluence.check(coreBody, signature.result());
132136
}
133137
} else {
134-
patResult = clauseTycker.check(fnDecl.entireSourcePos());
135-
def = factory.apply(Either.right(patResult.wellTyped()));
138+
var patResult = clauseTycker.check(fnDecl.entireSourcePos());
139+
coreBody = patResult.wellTyped();
140+
hasLhsError = patResult.hasLhsError();
141+
def = new FnDef(fnRef, fnDecl.modifiers, Either.right(coreBody));
142+
}
143+
if (!hasLhsError) {
144+
var hitConflChecker = new IApplyConfl(def, tycker, fnDecl.sourcePos());
145+
hitConflChecker.check();
136146
}
137-
if (!patResult.hasLhsError()) new IApplyConfl(def, tycker, fnDecl.sourcePos()).check();
138147
yield def;
139148
}
140149
};

0 commit comments

Comments
 (0)