Let Term

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

@@ -14,6 +14,7 @@
 import org.aya.concrete.stmt.Stmt;
 import org.aya.concrete.stmt.UseHide;
 import org.aya.generic.AyaDocile;
+import org.aya.generic.Nested;
 import org.aya.generic.ParamLike;
 import org.aya.generic.SortKind;
 import org.aya.guest0x0.cubical.Restr;
@@ -44,6 +45,7 @@
  * @author re-xyr
  */
 public sealed interface Expr extends AyaDocile, SourceNode, Restr.TermLike<Expr> {
+
   @NotNull Expr descent(@NotNull UnaryOperator<@NotNull Expr> f);
   /**
    * Do !!!NOT!!! use in the type checker.
@@ -190,7 +192,12 @@ record Pi(
     @NotNull SourcePos sourcePos,
     @NotNull Param param,
     @NotNull Expr last
-  ) implements Expr {
+  ) implements Expr, Nested<Param, Expr, Pi> {
+    @Override
+    public @NotNull Expr body() {
+      return last;
+    }
+
     public @NotNull Expr.Pi update(@NotNull Param param, @NotNull Expr last) {
       return param == param() && last == last() ? this : new Pi(sourcePos, param, last);
     }
@@ -273,7 +280,7 @@ record Lambda(
     @NotNull SourcePos sourcePos,
     @NotNull Param param,
     @NotNull Expr body
-  ) implements Expr {
+  ) implements Expr, Nested<Param, Expr, Lambda> {
     public @NotNull Expr.Lambda update(@NotNull Param param, @NotNull Expr body) {
       return param == param() && body == body() ? this : new Lambda(sourcePos, param, body);
     }
@@ -691,7 +698,12 @@ record Let(
     @NotNull SourcePos sourcePos,
     @NotNull Expr.LetBind bind,
     @NotNull Expr body
-  ) implements Expr {
+  ) implements Expr, Nested<Expr.LetBind, Expr, Let> {
+    @Override
+    public @NotNull Expr.LetBind param() {
+      return bind;
+    }
+
     public @NotNull Let update(@NotNull Expr.LetBind bind, @NotNull Expr body) {
       return bind() == bind && body() == body
         ? this
@@ -778,4 +790,21 @@ record LetOpen(
     return constructor.apply(sourcePos, params.first(),
       buildNested(subPos, drop, body, constructor));
   }
+
+  @SuppressWarnings("unchecked")
+  static <Param, Term, This extends Nested<Param, Term, This>>
+  @NotNull Tuple2<ImmutableSeq<Param>, Term>
+  destructNested(@NotNull This nested) {
+    var telescope = MutableList.<Param>create();
+    This nestedBody = nested;
+    Term body = (Term) nested;
+
+    while (nestedBody != null) {
+      telescope.append(nestedBody.param());
+      body = nestedBody.body();
+      nestedBody = nestedBody.tryNested();
+    }
+
+    return kala.tuple.Tuple.of(telescope.toImmutableSeq(), body);
+  }
 }

base/src/main/java/org/aya/core/serde/SerTerm.java

@@ -320,4 +320,11 @@ record OutS(@NotNull SerTerm phi, @NotNull SerTerm par, @NotNull SerTerm u) impl
       return new OutTerm(phi.de(state), par.de(state), u.de(state));
     }
   }
+
+  record Let(@NotNull SimpVar bind, @NotNull SerTerm definedAs, @NotNull SerTerm body) implements SerTerm {
+    @Override
+    public @NotNull Term de(@NotNull DeState state) {
+      return new LetTerm(bind.de(state), definedAs.de(state), body.de(state));
+    }
+  }
 }

base/src/main/java/org/aya/core/serde/Serializer.java

@@ -125,6 +125,8 @@ case PAppTerm(var of, var args, var cube) -> new SerTerm.PathApp(serialize(of),
       case HCompTerm hComp -> throw new InternalException("TODO");
       case InTerm(var phi, var u) -> new SerTerm.InS(serialize(phi), serialize(u));
       case OutTerm(var phi, var par, var u) -> new SerTerm.OutS(serialize(phi), serialize(par), serialize(u));
+      case LetTerm(var bind, var definedAs, var body) ->
+        new SerTerm.Let(serialize(bind), serialize(definedAs), serialize(body));
     };
   }
 

base/src/main/java/org/aya/core/term/LetTerm.java

@@ -0,0 +1,42 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.core.term;
+
+import kala.tuple.Tuple;
+import kala.tuple.Tuple2;
+import org.aya.core.pat.Pat;
+import org.aya.generic.Nested;
+import org.aya.ref.LocalVar;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.function.UnaryOperator;
+
+public record LetTerm(
+  @NotNull LocalVar bind,
+  @NotNull Term definedAs,
+  @NotNull Term body
+) implements Term, Nested<Tuple2<LocalVar, Term>, Term, LetTerm> {
+  /**
+   * Substitute {@link LetTerm#bind} in {@link LetTerm#body} with {@link LetTerm#definedAs}.
+   * In order to avoid normalizing {@code big} multiple times in {@code (\ x => (x, ..., x)) big}
+   */
+  public @NotNull Term inline(@NotNull UnaryOperator<Term> inliner) {
+    return body.subst(bind, inliner.apply(definedAs));
+  }
+
+  public @NotNull LetTerm update(@NotNull Term definedAs, @NotNull Term body) {
+    return this.definedAs == definedAs && this.body == body
+      ? this
+      : new LetTerm(bind, definedAs, body);
+  }
+
+  @Override
+  public @NotNull Term descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g) {
+    return update(f.apply(definedAs), f.apply(body));
+  }
+
+  @Override
+  public @NotNull Tuple2<LocalVar, Term> param() {
+    return Tuple.of(bind, definedAs);
+  }
+}

base/src/main/java/org/aya/core/term/Term.java

@@ -38,7 +38,7 @@
  * @author ice1000
  */
 public sealed interface Term extends AyaDocile, Restr.TermLike<Term>
-  permits Callable, CoeTerm, Elimination, Formation, FormulaTerm, HCompTerm, InTerm, MatchTerm, MetaLitTerm, MetaPatTerm, PartialTerm, RefTerm, RefTerm.Field, StableWHNF {
+  permits Callable, CoeTerm, Elimination, Formation, FormulaTerm, HCompTerm, InTerm, MatchTerm, LetTerm, MetaLitTerm, MetaPatTerm, PartialTerm, RefTerm, RefTerm.Field, StableWHNF {
   // Descending an operation to the term AST
   // NOTE: Currently we require the operation `f` to preserve StructCall, DataCall, and SortTerm.
   @NotNull Term descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g);

base/src/main/java/org/aya/core/visitor/BetaExpander.java

@@ -77,6 +77,7 @@ yield switch (codom) {
           default -> term;
         };
       }
+      case LetTerm let -> apply(let.inline(this));
       default -> term;
     };
   }

base/src/main/java/org/aya/generic/Nested.java

@@ -0,0 +1,44 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.generic;
+
+import org.aya.concrete.Expr;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+/**
+ * A Nested structure is something consists of a head and a body, for example:
+ * <ul>
+ *   <li>{@link Expr.Lambda} is a nested structure, it has a {@link Expr.Param} as a head and a {@link Expr} as a body</li>
+ *   <li>{@link Expr.Let} is a nested structure, it has a {@link Expr.LetBind} as a head and a {@link Expr} as a body</li>
+ *   <li>If you wish, {@link Expr.App} is also a nested structure in some way</li>
+ * </ul>
+ * <p>
+ * A Nested class is supposed to also be a {@link Term}
+ */
+public interface Nested<Param, Term, This extends Nested<Param, Term, This>> {
+  /**
+   * The head of a nested structure.
+   * It looks like a parameter of a lambda expression, so I call it "param".
+   */
+  @NotNull Param param();
+
+  /**
+   * The body of a nested structure
+   */
+  @NotNull Term body();
+
+  /**
+   * The nested body of a nested structure
+   *
+   * @return null if the body is not {@link This}
+   * @implSpec {@code tryNested == null || tryNested == body}
+   */
+  @SuppressWarnings("unchecked")
+  default @Nullable This tryNested() {
+    var body = body();
+    var clazz = getClass();
+
+    return clazz.isInstance(body) ? (This) clazz.cast(body) : null;
+  }
+}

base/src/main/java/org/aya/prettier/AbstractLetPrettier.java

@@ -0,0 +1,37 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.prettier;
+
+import org.aya.generic.AyaDocile;
+import org.aya.generic.Nested;
+import org.aya.pretty.doc.Doc;
+import org.jetbrains.annotations.NotNull;
+
+public abstract class AbstractLetPrettier<Bind, Term extends AyaDocile, LetTerm extends Nested<Bind, Term, LetTerm>>
+  implements LetPrettier<Bind, Term, LetTerm> {
+  private final @NotNull BasePrettier<Term> basePrettier;
+
+  public AbstractLetPrettier(@NotNull BasePrettier<Term> basePrettier, LetTerm helper) {
+    this.basePrettier = basePrettier;
+  }
+
+  @Override
+  public @NotNull Doc kwLet() {
+    return Doc.styled(BasePrettier.KEYWORD, "let");
+  }
+
+  @Override
+  public @NotNull Doc kwIn() {
+    return Doc.styled(BasePrettier.KEYWORD, "in");
+  }
+
+  @Override
+  public @NotNull Doc bar() {
+    return Doc.symbol("|");
+  }
+
+  @Override
+  public @NotNull Doc term(@NotNull Term term) {
+    return basePrettier.term(BasePrettier.Outer.Free, term);
+  }
+}

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

@@ -191,40 +191,12 @@ yield visitCalls(null, fn, (nc, l) -> l.toDoc(options), outer,
           Doc.symbol("]")
         )
       );
-      case Expr.Let let -> {
-        var letsAndBody = sugarLet(let);
-        var lets = letsAndBody.component1();
-        var body = letsAndBody.component2();
-        var oneLine = lets.sizeEquals(1);
-        var letSeq = oneLine
-          ? visitLetBind(lets.first())
-          : Doc.vcat(lets.view()
-            .map(this::visitLetBind)
-            // | f := g
-            .map(x -> Doc.sep(Doc.symbol("|"), x)));
-
-        var docs = ImmutableSeq.of(
-          Doc.styled(KEYWORD, "let"),
-          letSeq,
-          Doc.styled(KEYWORD, "in")
-        );
-
-        // ```
-        // let a := b in
-        // ```
-        //
-        // or
-        //
-        // ```
-        // let
-        // | a := b
-        // | c := d
-        // in
-        // ```
-        var halfLet = oneLine ? Doc.sep(docs) : Doc.vcat(docs);
-
-        yield Doc.sep(halfLet, term(Outer.Free, body));
-      }
+      case Expr.Let let -> new AbstractLetPrettier<>(this, let) {
+        @Override
+        public @NotNull Doc visitBind(Expr.@NotNull LetBind letBind) {
+          return visitLetBind(letBind);
+        }
+      }.visitLet(let);
       // let open Foo using (bar) in
       //   body
       case Expr.LetOpen letOpen -> Doc.vcat(

base/src/main/java/org/aya/prettier/CorePrettier.java

@@ -7,19 +7,20 @@
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
+import kala.tuple.Tuple2;
 import org.aya.core.def.*;
 import org.aya.core.pat.Pat;
 import org.aya.core.repr.CodeShape;
 import org.aya.core.term.*;
 import org.aya.core.visitor.TermFolder;
 import org.aya.generic.AyaDocile;
-import org.aya.util.error.InternalException;
 import org.aya.guest0x0.cubical.Partial;
 import org.aya.guest0x0.cubical.Restr;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.DefVar;
 import org.aya.ref.LocalVar;
 import org.aya.util.Arg;
+import org.aya.util.error.InternalException;
 import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -238,6 +239,15 @@ case CoeTerm(var ty, var r, var s) -> visitCalls(null,
       case HCompTerm hComp -> throw new InternalException("TODO");
       case InTerm(var phi, var u) -> insideOut(outer, phi, u, "inS");
       case OutTerm(var phi, var par, var u) -> insideOut(outer, phi, u, "outS");
+      case LetTerm let -> new AbstractLetPrettier<>(this, let) {
+        @Override
+        public @NotNull Doc visitBind(@NotNull Tuple2<LocalVar, Term> letBind) {
+          var bind = letBind.component1();
+          Doc type = null;      // TODO: type
+          var definedAs = letBind.component2();
+          return Doc.sep(varDoc(bind), Doc.symbol(":="), term(definedAs));
+        }
+      }.visitLet(let);
     };
   }
 

base/src/main/java/org/aya/prettier/LetPrettier.java

@@ -0,0 +1,43 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.prettier;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.concrete.Expr;
+import org.aya.generic.Nested;
+import org.aya.pretty.doc.Doc;
+import org.jetbrains.annotations.NotNull;
+
+public interface LetPrettier<Bind, Term, LetTerm extends Nested<Bind, Term, LetTerm>> {
+  @NotNull Doc bar();
+  @NotNull Doc kwLet();
+  @NotNull Doc kwIn();
+
+  @NotNull Doc visitBind(@NotNull Bind bind);
+  @NotNull Doc term(@NotNull Term term);
+
+  default @NotNull Doc visitLet(@NotNull LetTerm term) {
+    var pair = Expr.destructNested(term);
+    var binds = pair.component1();
+    var body = pair.component2();
+    var oneLine = binds.sizeEquals(1);
+    var docBinds = visitBinds(binds);
+    var docs = ImmutableSeq.of(kwLet(), docBinds, kwIn());
+    var head = oneLine ? Doc.sep(docs) : Doc.vcat(docs);
+
+    return Doc.sep(head, term(body));
+  }
+
+  default @NotNull Doc visitBinds(@NotNull ImmutableSeq<Bind> binds) {
+    assert binds.isNotEmpty() : "???";
+    if (binds.sizeEquals(1)) {
+      return visitBind(binds.first());
+    } else {
+      return Doc.vcat(
+        binds.view()
+          .map(this::visitBind)
+          .map(x -> Doc.sep(bar(), x))
+      );
+    }
+  }
+}

base/src/main/java/org/aya/ref/GenerateKind.java

@@ -11,10 +11,20 @@ public sealed interface GenerateKind {
    */
   enum None implements GenerateKind {
     INSTANCE;
+
+    @Override
+    public String toString() {
+      return "None";
+    }
   }
 
   enum Anonymous implements GenerateKind {
     INSTANCE;
+
+    @Override
+    public String toString() {
+      return "Anonymous";
+    }
   }
 
   record Generalized(@NotNull GeneralizedVar origin) implements GenerateKind {