concrete: rename

aya-prover · Jan 20, 2025 · 0b48848 · 0b48848
1 parent 17f69e1
commit 0b48848
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 22 deletions.
diff --git a/base/src/main/java/org/aya/resolve/salt/Desalt.java b/base/src/main/java/org/aya/resolve/salt/Desalt.java
@@ -72,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.RawLam lam -> {
+      case Expr.ClauseLam lam -> {
         var isVanilla = lam.patterns().allMatch(x -> x.term().data() instanceof Pattern.Refutable);
 
         ImmutableSeq<LocalVar> lamTele;

diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/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.RawLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
+      case Expr.ClauseLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
       case Expr.DepType depType -> {
         var mCtx = MutableValue.create(ctx);
         var param = bind(depType.param(), mCtx);

diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
@@ -668,18 +668,18 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
         .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))));
+      return new WithPos<>(pos, new Expr.ClauseLam(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.RawLam(new Pattern.Clause(pos, tele, Option.some(result))));
+      return new WithPos<>(pos, new Expr.ClauseLam(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.RawLam(new Pattern.Clause(pos, ImmutableSeq.of(tele), result)));
+      return new WithPos<>(pos, new Expr.ClauseLam(new Pattern.Clause(pos, ImmutableSeq.of(tele), result)));
     }
     if (node.is(IDIOM_ATOM)) {
       var block = node.peekChild(IDIOM_BLOCK);

diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/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.RawLam(var cls) -> checkParen(outer, visitLambda(cls), Outer.BinOp);
+      case Expr.ClauseLam(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();

diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -74,7 +74,7 @@ public Param(@NotNull SourcePos sourcePos, @NotNull LocalVar ref, @NotNull WithP
 
   /// @param filling  the inner expr of goal
   /// @param explicit whether the hole is a type-directed programming goal or
-  ///                 a to-be-solved by tycking hole.
+  ///                                 a to-be-solved by tycking hole.
   record Hole(
     boolean explicit,
     @Nullable WithPos<Expr> filling,
@@ -135,33 +135,28 @@ public Ref(@NotNull AnyVar var) {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  record RawLam(@NotNull Pattern.Clause clause) implements Expr, Sugar {
+  record ClauseLam(@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 RawLam {
+    public ClauseLam {
       assert clause.patterns.isNotEmpty();
     }
 
-    public @NotNull Expr.RawLam update(@NotNull Pattern.Clause clause) {
-      return clause == this.clause ? this : new RawLam(clause);
+    public @NotNull Expr.ClauseLam update(@NotNull Pattern.Clause clause) {
+      return clause == this.clause ? this : new ClauseLam(clause);
     }
 
-    public @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns() {
-      return clause.patterns;
-    }
-
-    public @NotNull WithPos<Expr> body() {
-      return clause.expr.get();
-    }
+    public @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns() { return clause.patterns; }
+    public @NotNull WithPos<Expr> body() { return clause.expr.get(); }
 
-    @Override public @NotNull Expr.RawLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
+    @Override public @NotNull Expr.ClauseLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
       return descent(f, PosedUnaryOperator.identity());
     }
 
-    public @NotNull Expr.RawLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
+    public @NotNull Expr.ClauseLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
       return update(clause.descent(f, g));
     }
 
@@ -456,7 +451,7 @@ public void forEach(@NotNull Consumer<Expr> f) {
     /// @param generator `x * y` part above
     /// @param binds     `x <- [1, 2, 3], y <- [4, 5, 6]` part above
     /// @param names     the bind (`>>=`) function, it is [#monadBind] in default,
-    ///                  the pure (`return`) function, it is [#functorPure] in default
+    ///                                   the pure (`return`) function, it is [#functorPure] in default
     /// @apiNote a ArrayCompBlock will be desugar to a do-block. For the example above,
     /// it will be desugared to `do x <- [1, 2, 3], y <- [4, 5, 6], return x * y`
     public record CompBlock(

diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java b/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.RawLam] in desugarer.
+  /// Whether a [Pattern] can be a [Pattern.Bind], this is used by [Expr.ClauseLam] in desugarer.
   ///
   /// @see Pattern.Bind
   /// @see Pattern.CalmFace