concrete: more Expr

aya-prover · Jan 4, 2024 · c5d8ff2 · c5d8ff2
1 parent 6dc6a71
commit c5d8ff2
Show file tree

Hide file tree

Showing 3 changed files with 103 additions and 31 deletions.
diff --git a/base/src/main/java/module-info.java b/base/src/main/java/module-info.java
@@ -16,5 +16,6 @@
   exports org.aya.syntax.core.def;
   exports org.aya.syntax.core.term;
   exports org.aya.syntax.ref;
-  exports org.aya.syntax.concrete.expr;
+  exports org.aya.generic;
+  exports org.aya.syntax.concrete;
 }
diff --git a/base/src/main/java/org/aya/generic/SortKind.java b/base/src/main/java/org/aya/generic/SortKind.java
@@ -0,0 +1,11 @@
+// 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;
+
+public enum SortKind {
+  Type, Set, ISet;
+
+  public boolean hasLevel() {
+    return this == Type || this == Set;
+  }
+}
diff --git a/...va/org/aya/syntax/concrete/expr/Expr.java → ...in/java/org/aya/syntax/concrete/Expr.java b/...va/org/aya/syntax/concrete/expr/Expr.java → ...in/java/org/aya/syntax/concrete/Expr.java
@@ -1,11 +1,14 @@
-package org.aya.syntax.concrete.expr;
+// Copyright (c) 2020-2024 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.syntax.concrete;
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.value.MutableValue;
+import org.aya.generic.SortKind;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.util.BinOpElem;
-import org.aya.util.error.SourceNode;
 import org.aya.util.error.SourcePos;
+import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -14,30 +17,23 @@
 public sealed interface Expr {
   @NotNull Expr descent(@NotNull UnaryOperator<@NotNull Expr> f);
 
-  record Node(@NotNull SourcePos sourcePos, @NotNull Expr expr) implements SourceNode {
-    public @NotNull Node map(@NotNull UnaryOperator<Expr> mapper) {
-      var result = mapper.apply(expr);
-      return result == expr ? this : new Node(sourcePos, result);
-    }
-  }
-
   record Param(
     @NotNull SourcePos sourcePos,
     @NotNull LocalVar ref,
-    @NotNull Node type,
+    @NotNull WithPos<Expr> type,
     boolean explicit
     // @ForLSP MutableValue<Result> theCore
   ) {
     public Param(@NotNull SourcePos sourcePos, @NotNull LocalVar var, boolean explicit) {
-      this(sourcePos, var, new Node(sourcePos, new Hole(false, null)), explicit);
+      this(sourcePos, var, new WithPos<>(sourcePos, new Hole(false, null)), explicit);
     }
 
-    public @NotNull Param update(@NotNull Node type) {
+    public @NotNull Param update(@NotNull WithPos<Expr> type) {
       return type == type() ? this : new Param(sourcePos, ref, type, explicit);
     }
 
     public @NotNull Param descent(@NotNull UnaryOperator<Expr> f) {
-      return update(type.map(f));
+      return update(type.descent(f));
     }
   }
 
@@ -48,7 +44,7 @@ public Param(@NotNull SourcePos sourcePos, @NotNull LocalVar var, boolean explic
    */
   record Hole(
     boolean explicit,
-    @Nullable Expr filling,
+    @Nullable Expr filling, // TODO
     MutableValue<ImmutableSeq<LocalVar>> accessibleLocal
   ) implements Expr {
     public Hole(boolean explicit, @Nullable Expr filling) {
@@ -79,68 +75,68 @@ record Ref(@NotNull LocalVar var) implements Expr {
     }
   }
 
-  record Lam(@NotNull Param param, @NotNull Node body) implements Expr {
-    public @NotNull Lam update(@NotNull Param param, @NotNull Node body) {
+  record Lam(@NotNull Param param, @NotNull WithPos<Expr> body) implements Expr {
+    public @NotNull Lam update(@NotNull Param param, @NotNull WithPos<Expr> body) {
       return param == param() && body == body() ? this : new Lam(param, body);
     }
 
     @Override public @NotNull Lam descent(@NotNull UnaryOperator<@NotNull Expr> f) {
-      return update(param.descent(f), body.map(f));
+      return update(param.descent(f), body.descent(f));
     }
   }
 
   record Tuple(
-    @NotNull ImmutableSeq<@NotNull Node> items
+    @NotNull ImmutableSeq<@NotNull WithPos<Expr>> items
   ) implements Expr {
-    public @NotNull Expr.Tuple update(@NotNull ImmutableSeq<@NotNull Node> items) {
+    public @NotNull Expr.Tuple update(@NotNull ImmutableSeq<@NotNull WithPos<Expr>> items) {
       return items.sameElements(items(), true) ? this : new Tuple(items);
     }
 
     @Override public @NotNull Expr.Tuple descent(@NotNull UnaryOperator<@NotNull Expr> f) {
-      return update(items.map(x -> x.map(f)));
+      return update(items.map(x -> x.descent(f)));
     }
   }
 
-  record App(@NotNull Node function, @NotNull NamedArg argument) implements Expr {
-    public @NotNull App update(@NotNull Node function, @NotNull NamedArg argument) {
+  record App(@NotNull WithPos<Expr> function, @NotNull NamedArg argument) implements Expr {
+    public @NotNull App update(@NotNull WithPos<Expr> function, @NotNull NamedArg argument) {
       return function == function() && argument == argument() ? this : new App(function, argument);
     }
 
     @Override public @NotNull App descent(@NotNull UnaryOperator<@NotNull Expr> f) {
-      return update(function.map(f), argument.descent(f));
+      return update(function.descent(f), argument.descent(f));
     }
   }
 
   record NamedArg(
     @NotNull SourcePos sourcePos,
     @Override boolean explicit,
     @Nullable String name,
-    @NotNull Node arg
+    @NotNull WithPos<Expr> arg
   ) implements BinOpElem<Expr> {
     @Override
     public @NotNull Expr term() {
-      return arg.expr();
+      return arg.data();
     }
 
-    public @NotNull NamedArg update(@NotNull Node expr) {
+    public @NotNull NamedArg update(@NotNull WithPos<Expr> expr) {
       return expr == arg ? this : new NamedArg(sourcePos, explicit, name, expr);
     }
 
     public @NotNull NamedArg descent(@NotNull UnaryOperator<@NotNull Expr> f) {
-      return update(arg.map(f));
+      return update(arg.descent(f));
     }
   }
 
   record Pi(
     @NotNull Param param,
-    @NotNull Node last
+    @NotNull WithPos<Expr> last
   ) implements Expr {
-    public @NotNull Pi update(@NotNull Param param, @NotNull Node last) {
+    public @NotNull Pi update(@NotNull Param param, @NotNull WithPos<Expr> last) {
       return param == param() && last == last() ? this : new Pi(param, last);
     }
 
     @Override public @NotNull Pi descent(@NotNull UnaryOperator<@NotNull Expr> f) {
-      return update(param.descent(f), last.map(f));
+      return update(param.descent(f), last.descent(f));
     }
   }
 
@@ -155,4 +151,68 @@ record Sigma(
       return update(params.map(param -> param.descent(f)));
     }
   }
+
+  record RawSort(@NotNull SourcePos sourcePos, @NotNull SortKind kind) implements Expr {
+    @Override public @NotNull RawSort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+      return this;
+    }
+  }
+
+  sealed interface Sort extends Expr {
+    int lift();
+
+    SortKind kind();
+
+    @Override default @NotNull Sort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+      return this;
+    }
+  }
+
+  record Type(@Override int lift) implements Sort {
+    @Override public SortKind kind() {
+      return SortKind.Type;
+    }
+  }
+
+  record Set(@Override int lift) implements Sort {
+    @Override public SortKind kind() {
+      return SortKind.Set;
+    }
+  }
+
+  enum ISet implements Sort {
+    INSTANCE;
+
+    @Override public int lift() {
+      return 0;
+    }
+
+    @Override public SortKind kind() {
+      return SortKind.ISet;
+    }
+  }
+
+  record LitInt(int integer) implements Expr {
+    @Override public @NotNull LitInt descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+      return this;
+    }
+  }
+
+  record LitString(@NotNull String string) implements Expr {
+    @Override public @NotNull LitString descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+      return this;
+    }
+  }
+
+  record BinOpSeq(
+    @NotNull ImmutableSeq<NamedArg> seq
+  ) implements Expr {
+    public @NotNull BinOpSeq update(@NotNull ImmutableSeq<NamedArg> seq) {
+      return seq.sameElements(seq(), true) ? this : new BinOpSeq(seq);
+    }
+
+    @Override public @NotNull BinOpSeq descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+      return update(seq.map(arg -> arg.descent(f)));
+    }
+  }
 }