Skip to content

Commit

Permalink
prop: remove some unnecessary qualification
Browse files Browse the repository at this point in the history
  • Loading branch information
@ice1000
ice1000 committed Nov 11, 2023
1 parent 8d1b637 commit 40e1859
Showing 1 changed file with 21 additions and 21 deletions.
42 changes: 21 additions & 21 deletions base/src/main/java/org/aya/concrete/Expr.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ default Expr resolveLax(@NotNull ModuleContext context) {
resolver.enterBody();
var inner = resolver.apply(this);
var view = resolver.allowedGeneralizes().valuesView().toImmutableSeq().view();
return Expr.buildLam(sourcePos(), view, inner);
return buildLam(sourcePos(), view, inner);
}

@Override default @NotNull Doc toDoc(@NotNull PrettierOptions options) {
Expand All @@ -85,7 +85,7 @@ public Unresolved(@NotNull SourcePos sourcePos, @NotNull String name) {
this(sourcePos, new QualifiedID(sourcePos, name));
}

@Override public @NotNull Expr.Unresolved descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Unresolved descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return this;
}
}
Expand Down Expand Up @@ -115,11 +115,11 @@ public Hole(@NotNull SourcePos sourcePos, boolean explicit, @Nullable Expr filli
this(sourcePos, explicit, filling, MutableValue.create());
}

public @NotNull Expr.Hole update(@Nullable Expr filling) {
public @NotNull Hole update(@Nullable Expr filling) {
return filling == filling() ? this : new Hole(sourcePos, explicit, filling);
}

@Override public @NotNull Expr.Hole descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Hole descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(filling == null ? null : f.apply(filling));
}
}
Expand All @@ -132,11 +132,11 @@ record App(
@NotNull Expr function,
@NotNull NamedArg argument
) implements Expr {
public @NotNull Expr.App update(@NotNull Expr function, @NotNull NamedArg argument) {
public @NotNull App update(@NotNull Expr function, @NotNull NamedArg argument) {
return function == function() && argument == argument() ? this : new App(sourcePos, function, argument);
}

@Override public @NotNull Expr.App descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull App descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(f.apply(function), argument.descent(f));
}
}
Expand Down Expand Up @@ -197,11 +197,11 @@ record Pi(
return last;
}

public @NotNull Expr.Pi update(@NotNull Param param, @NotNull Expr last) {
public @NotNull Pi update(@NotNull Param param, @NotNull Expr last) {
return param == param() && last == last() ? this : new Pi(sourcePos, param, last);
}

@Override public @NotNull Expr.Pi descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Pi descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(param.descent(f), f.apply(last));
}
}
Expand Down Expand Up @@ -280,11 +280,11 @@ record Lambda(
@NotNull Param param,
@NotNull Expr body
) implements Expr, Nested<Param, Expr, Lambda> {
public @NotNull Expr.Lambda update(@NotNull Param param, @NotNull Expr body) {
public @NotNull Lambda update(@NotNull Param param, @NotNull Expr body) {
return param == param() && body == body() ? this : new Lambda(sourcePos, param, body);
}

@Override public @NotNull Expr.Lambda descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Lambda descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(param.descent(f), f.apply(body));
}
}
Expand All @@ -296,11 +296,11 @@ record Sigma(
@NotNull SourcePos sourcePos,
@NotNull ImmutableSeq<@NotNull Param> params
) implements Expr {
public @NotNull Expr.Sigma update(@NotNull ImmutableSeq<@NotNull Param> params) {
public @NotNull Sigma update(@NotNull ImmutableSeq<@NotNull Param> params) {
return params.sameElements(params(), true) ? this : new Sigma(sourcePos, params);
}

@Override public @NotNull Expr.Sigma descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Sigma descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(params.map(param -> param.descent(f)));
}
}
Expand All @@ -322,13 +322,13 @@ public Ref(@NotNull SourcePos sourcePos, @NotNull AnyVar resolvedVar) {
this(sourcePos, resolvedVar, MutableValue.create());
}

@Override public @NotNull Expr.Ref descent(@NotNull UnaryOperator<@NotNull Expr> f) {
@Override public @NotNull Ref descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return this;
}
}

record Lift(@NotNull SourcePos sourcePos, @NotNull Expr expr, int lift) implements Expr {
public @NotNull Expr.Lift update(@NotNull Expr expr) {
public @NotNull Lift update(@NotNull Expr expr) {
return expr == expr() ? this : new Lift(sourcePos, expr, lift);
}

Expand Down Expand Up @@ -685,15 +685,15 @@ public static Expr.Array newGenerator(
*/
record Let(
@NotNull SourcePos sourcePos,
@NotNull Expr.LetBind bind,
@NotNull LetBind bind,
@NotNull Expr body
) implements Expr, Nested<LetBind, Expr, Let> {
@Override
public @NotNull LetBind param() {
return bind;
}

public @NotNull Let update(@NotNull Expr.LetBind bind, @NotNull Expr body) {
public @NotNull Let update(@NotNull LetBind bind, @NotNull Expr body) {
return bind() == bind && body() == body
? this
: new Let(sourcePos(), bind, body);
Expand All @@ -712,13 +712,13 @@ record LetBind(
@NotNull Expr result,
@NotNull Expr definedAs
) implements SourceNode {
public @NotNull Expr.LetBind update(@NotNull ImmutableSeq<Expr.Param> telescope, @NotNull Expr result, @NotNull Expr definedAs) {
public @NotNull LetBind update(@NotNull ImmutableSeq<Expr.Param> telescope, @NotNull Expr result, @NotNull Expr definedAs) {
return telescope().sameElements(telescope, true) && result() == result && definedAs() == definedAs
? this
: new LetBind(sourcePos, bindName, telescope, result, definedAs);
}

public @NotNull Expr.LetBind descent(@NotNull UnaryOperator<@NotNull Expr> f) {
public @NotNull LetBind descent(@NotNull UnaryOperator<@NotNull Expr> f) {
return update(telescope().map(x -> x.descent(f)), f.apply(result()), f.apply(definedAs()));
}
}
Expand Down Expand Up @@ -754,15 +754,15 @@ record LetOpen(
}

static @NotNull Expr buildPi(@NotNull SourcePos sourcePos, @NotNull SeqView<Param> params, @NotNull Expr body) {
return buildNested(sourcePos, params, body, Expr.Pi::new);
return buildNested(sourcePos, params, body, Pi::new);
}

static @NotNull Expr buildLam(@NotNull SourcePos sourcePos, @NotNull SeqView<Param> params, @NotNull Expr body) {
return buildNested(sourcePos, params, body, Expr.Lambda::new);
return buildNested(sourcePos, params, body, Lambda::new);
}

static @NotNull Expr buildLet(@NotNull SourcePos sourcePos, @NotNull SeqView<LetBind> binds, @NotNull Expr body) {
return buildNested(sourcePos, binds, body, Expr.Let::new);
return buildNested(sourcePos, binds, body, Let::new);
}

/** convert flattened terms into nested right-associate terms */
Expand Down

0 comments on commit 40e1859

Please sign in to comment.