From 3895187f8905a98d0a7b471f9063d7b7e0875a1b Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sat, 13 Jan 2024 18:45:34 +0800
Subject: [PATCH] term: lambda with implicit argument

---
 .../org/aya/syntax/core/term/LamTerm.java     | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/base/src/main/java/org/aya/syntax/core/term/LamTerm.java b/base/src/main/java/org/aya/syntax/core/term/LamTerm.java
index 24913d11..4c6a6c0d 100644
--- a/base/src/main/java/org/aya/syntax/core/term/LamTerm.java
+++ b/base/src/main/java/org/aya/syntax/core/term/LamTerm.java
@@ -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);
+  }
 }