This repository has been archived by the owner on May 27, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
4622634
commit 3895187
Showing
1 changed file
with
16 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,18 +1,31 @@ | ||
package org.aya.syntax.core.term; | ||
|
||
import kala.collection.SeqLike; | ||
import kala.function.BooleanConsumer; | ||
import kala.function.IndexedFunction; | ||
import org.aya.syntax.ref.LocalVar; | ||
import org.jetbrains.annotations.NotNull; | ||
|
||
public record LamTerm(Term body) implements StableWHNF { | ||
public record LamTerm(boolean explicit, Term body) implements StableWHNF { | ||
public @NotNull LamTerm update(@NotNull Term body) { | ||
return body == this.body | ||
? this | ||
: new LamTerm(body); | ||
: new LamTerm(explicit, body); | ||
} | ||
|
||
@Override | ||
public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) { | ||
return update(f.apply(1, body)); | ||
} | ||
|
||
public static @NotNull Term unwrap(@NotNull Term term, @NotNull BooleanConsumer params) { | ||
while (term instanceof LamTerm lambda) { | ||
params.accept(lambda.explicit); | ||
term = lambda.body; | ||
} | ||
return term; | ||
} | ||
|
||
public static @NotNull Term make(@NotNull SeqLike<Boolean> telescope, @NotNull Term body) { | ||
return telescope.view().foldRight(body, LamTerm::new); | ||
} | ||
} |