producer: reimplement og lambda

base/src/main/java/org/aya/resolve/salt/Desalt.java

@@ -3,23 +3,18 @@
 package org.aya.resolve.salt;
 
 import kala.collection.immutable.ImmutableSeq;
-import kala.value.primitive.MutableBooleanValue;
-import org.aya.generic.Constants;
 import org.aya.generic.term.SortKind;
 import org.aya.resolve.ResolveInfo;
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
 import org.aya.syntax.ref.LocalVar;
-import org.aya.util.Arg;
 import org.aya.util.error.Panic;
 import org.aya.util.error.PosedUnaryOperator;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.Objects;
-
 /** Desugar, but the sugars are not sweet enough, therefore called salt. */
 public final class Desalt implements PosedUnaryOperator<Expr> {
   private final @NotNull ResolveInfo info;
@@ -77,7 +72,7 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
       case Expr.Idiom idiom -> throw new UnsupportedOperationException("TODO");
       case Expr.RawSort(var kind) -> new Expr.Sort(kind, 0);
       case Expr.LetOpen letOpen -> apply(letOpen.body());
-      case Expr.IrrefutableLam lam -> {
+      case Expr.RawLam lam -> {
         var isVanilla = lam.patterns().allMatch(x -> x.term().data() instanceof Pattern.Refutable);
 
         ImmutableSeq<LocalVar> lamTele;

base/src/main/java/org/aya/resolve/visitor/ExprResolver.java

@@ -115,7 +115,7 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
     return switch (pre(expr)) {
       case Expr.Do doExpr ->
         doExpr.update(apply(SourcePos.NONE, doExpr.bindName()), bind(doExpr.binds(), MutableValue.create(ctx)));
-      case Expr.IrrefutableLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
+      case Expr.RawLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
       case Expr.DepType depType -> {
         var mCtx = MutableValue.create(ctx);
         var param = bind(depType.param(), mCtx);

producer/src/main/java/org/aya/producer/AyaProducer.java

@@ -664,19 +664,22 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
         result = new WithPos<>(bodyHolePos, new Expr.Hole(false, null));
       } else result = expr(bodyExpr);
       var tele = teleBinderUntyped(node.child(TELE_BINDER_UNTYPED)).view()
-        .map(LocalVar::from);
-      return Expr.buildLam(pos, tele, result);
+        .map(LocalVar::from)
+        .map(v -> new WithPos<Pattern>(v.definition(), new Pattern.Bind(v)))
+        .map(Arg::ofExplicitly)
+        .toImmutableSeq();
+      return new WithPos<>(pos, new Expr.RawLam(new Pattern.Clause(pos, tele, Option.some(result))));
     }
     if (node.is(LAMBDA_1_EXPR)) {
       var result = expr(node.child(EXPR));
       var tele = patterns(node.child(PATTERNS).child(COMMA_SEP));
-      return new WithPos<>(pos, new Expr.IrrefutableLam(new Pattern.Clause(pos, tele, Option.some(result))));
+      return new WithPos<>(pos, new Expr.RawLam(new Pattern.Clause(pos, tele, Option.some(result))));
     }
     if (node.is(LAMBDA_2_EXPR)) {
       var bodyExpr = node.peekChild(EXPR);
       Option<WithPos<Expr>> result = bodyExpr == null ? Option.none() : Option.some(expr(bodyExpr));
       var tele = unitPattern(node.child(UNIT_PATTERN));
-      return new WithPos<>(pos, new Expr.IrrefutableLam(new Pattern.Clause(pos, ImmutableSeq.of(tele), result)));
+      return new WithPos<>(pos, new Expr.RawLam(new Pattern.Clause(pos, ImmutableSeq.of(tele), result)));
     }
     if (node.is(IDIOM_ATOM)) {
       var block = node.peekChild(IDIOM_BLOCK);

syntax/src/main/java/org/aya/prettier/ConcretePrettier.java

@@ -116,7 +116,7 @@ yield visitConcreteCalls(assoc,
         }
         yield checkParen(outer, Doc.sep(prelude), Outer.BinOp);
       }
-      case Expr.IrrefutableLam(var cls) -> checkParen(outer, visitLambda(cls), Outer.BinOp);
+      case Expr.RawLam(var cls) -> checkParen(outer, visitLambda(cls), Outer.BinOp);
       case Expr.Hole expr -> {
         if (!expr.explicit()) yield Doc.symbol(Constants.ANONYMOUS_PREFIX);
         var filling = expr.filling();

syntax/src/main/java/org/aya/syntax/concrete/Expr.java

@@ -2,10 +2,13 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.concrete;
 
+import java.util.function.BiFunction;
+import java.util.function.Consumer;
+import java.util.function.Function;
+
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Either;
-import kala.control.Option;
 import kala.value.MutableValue;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.Nested;
@@ -27,11 +30,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.Objects;
-import java.util.function.BiFunction;
-import java.util.function.Consumer;
-import java.util.function.Function;
-
 public sealed interface Expr extends AyaDocile {
   @NotNull Expr descent(@NotNull PosedUnaryOperator<@NotNull Expr> f);
   void forEach(@NotNull PosedConsumer<@NotNull Expr> f);
@@ -137,18 +135,18 @@ public Ref(@NotNull AnyVar var) {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  record IrrefutableLam(@NotNull Pattern.Clause clause) implements Expr, Sugar {
+  record RawLam(@NotNull Pattern.Clause clause) implements Expr, Sugar {
     public static boolean canBeBind(@NotNull Arg<WithPos<Pattern>> pat) {
       var thePat = pat.term().data();
       return thePat instanceof Pattern.Bind || thePat == Pattern.CalmFace.INSTANCE;
     }
 
-    public IrrefutableLam {
+    public RawLam {
       assert clause.patterns.isNotEmpty();
     }
 
-    public @NotNull IrrefutableLam update(@NotNull Pattern.Clause clause) {
-      return clause == this.clause ? this : new IrrefutableLam(clause);
+    public @NotNull Expr.RawLam update(@NotNull Pattern.Clause clause) {
+      return clause == this.clause ? this : new RawLam(clause);
     }
 
     public @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns() {
@@ -159,11 +157,11 @@ public static boolean canBeBind(@NotNull Arg<WithPos<Pattern>> pat) {
       return clause.expr.get();
     }
 
-    @Override public @NotNull IrrefutableLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
+    @Override public @NotNull Expr.RawLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
       return descent(f, PosedUnaryOperator.identity());
     }
 
-    public @NotNull IrrefutableLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
+    public @NotNull Expr.RawLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
       return update(clause.descent(f, g));
     }
 

syntax/src/main/java/org/aya/syntax/concrete/Pattern.java

@@ -31,7 +31,7 @@ public sealed interface Pattern extends AyaDocile {
   void forEach(@NotNull PosedConsumer<@NotNull Pattern> f);
   interface Salt { }
 
-  /// Whether a [Pattern] can be a [Pattern.Bind], this is used by [Expr.IrrefutableLam] in desugarer.
+  /// Whether a [Pattern] can be a [Pattern.Bind], this is used by [Expr.RawLam] in desugarer.
   ///
   /// @see Pattern.Bind
   /// @see Pattern.CalmFace

tools/src/main/java/org/aya/util/IterableUtil.java

@@ -2,11 +2,11 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.util;
 
-import org.jetbrains.annotations.NotNull;
-
 import java.util.function.BiConsumer;
 import java.util.function.Consumer;
 
+import org.jetbrains.annotations.NotNull;
+
 public interface IterableUtil {
   static <T> void forEach(@NotNull Iterable<T> it, @NotNull BiConsumer<T, T> separator, @NotNull Consumer<T> run) {
     var iter = it.iterator();