prop: remove definition of Prop

Author: ice1000

Diff for: base/src/main/java/org/aya/concrete/Expr.java

@@ -332,7 +332,7 @@ record Lift(@NotNull SourcePos sourcePos, @NotNull Expr expr, int lift) implemen
       return expr == expr() ? this : new Lift(sourcePos, expr, lift);
     }
 
-    @Override public @NotNull Expr.Lift descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+    @Override public @NotNull Lift descent(@NotNull UnaryOperator<@NotNull Expr> f) {
       return update(f.apply(expr));
     }
   }
@@ -341,7 +341,7 @@ record Lift(@NotNull SourcePos sourcePos, @NotNull Expr expr, int lift) implemen
    * @author tsao-chi
    */
   record RawSort(@NotNull SourcePos sourcePos, @NotNull SortKind kind) implements Expr {
-    @Override public @NotNull Expr.RawSort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+    @Override public @NotNull RawSort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
       return this;
     }
   }
@@ -351,7 +351,7 @@ sealed interface Sort extends Expr {
 
     SortKind kind();
 
-    @Override default @NotNull Expr.Sort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+    @Override default @NotNull Sort descent(@NotNull UnaryOperator<@NotNull Expr> f) {
       return this;
     }
   }
@@ -368,16 +368,6 @@ record Set(@NotNull SourcePos sourcePos, @Override int lift) implements Sort {
     }
   }
 
-  record Prop(@NotNull SourcePos sourcePos) implements Sort {
-    @Override public int lift() {
-      return 0;
-    }
-
-    @Override public SortKind kind() {
-      return SortKind.Prop;
-    }
-  }
-
   record ISet(@NotNull SourcePos sourcePos) implements Sort {
     @Override public int lift() {
       return 0;
@@ -487,13 +477,13 @@ record Match(
    * @author kiva
    */
   record LitInt(@NotNull SourcePos sourcePos, int integer) implements Expr {
-    @Override public @NotNull Expr.LitInt descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+    @Override public @NotNull LitInt descent(@NotNull UnaryOperator<@NotNull Expr> f) {
       return this;
     }
   }
 
   record LitString(@NotNull SourcePos sourcePos, @NotNull String string) implements Expr {
-    @Override public @NotNull Expr.LitString descent(@NotNull UnaryOperator<@NotNull Expr> f) {
+    @Override public @NotNull LitString descent(@NotNull UnaryOperator<@NotNull Expr> f) {
       return this;
     }
   }

Diff for: base/src/main/java/org/aya/concrete/desugar/Desugarer.java

@@ -54,7 +54,6 @@ public static class DesugarInterruption extends Exception {}
       case Expr.RawSort(var pos, var kind) -> switch (kind) {
         case Type -> new Expr.Type(pos, 0);
         case Set -> new Expr.Set(pos, 0);
-        case Prop -> new Expr.Prop(pos);
         case ISet -> new Expr.ISet(pos);
       };
       case Expr.BinOpSeq(var pos, var seq) -> {

Diff for: base/src/main/java/org/aya/core/term/PiTerm.java

@@ -69,19 +69,14 @@ case PiTerm(var param, var body) when param.explicit() -> {
       case Type -> switch (codomain.kind()) {
         case Type, Set -> new SortTerm(SortKind.Type, Math.max(alift, blift));
         case ISet -> new SortTerm(SortKind.Set, alift);
-        case Prop -> codomain;
       };
       case ISet -> switch (codomain.kind()) {
-        case ISet, Prop -> SortTerm.Set0;
+        case ISet -> SortTerm.Set0;
         case Set, Type -> codomain;
       };
       case Set -> switch (codomain.kind()) {
         case Set, Type -> new SortTerm(SortKind.Set, Math.max(alift, blift));
-        case ISet, Prop -> new SortTerm(SortKind.Set, alift);
-      };
-      case Prop -> switch (codomain.kind()) {
-        case Prop, Type -> codomain;
-        default -> new SortTerm(SortKind.Set, blift);
+        case ISet -> new SortTerm(SortKind.Set, alift);
       };
     };
   }

Diff for: base/src/main/java/org/aya/core/term/SigmaTerm.java

@@ -30,9 +30,7 @@ public record SigmaTerm(@NotNull ImmutableSeq<@NotNull Param> params) implements
 
   public static @NotNull SortTerm lub(@NotNull SortTerm x, @NotNull SortTerm y) {
     int lift = Math.max(x.lift(), y.lift());
-    if (x.kind() == SortKind.Prop || y.kind() == SortKind.Prop) {
-      return SortTerm.Prop;
-    } else if (x.kind() == SortKind.Set || y.kind() == SortKind.Set) {
+    if (x.kind() == SortKind.Set || y.kind() == SortKind.Set) {
       return new SortTerm(SortKind.Set, lift);
     } else if (x.kind() == SortKind.Type || y.kind() == SortKind.Type) {
       return new SortTerm(SortKind.Type, lift);

Diff for: base/src/main/java/org/aya/core/term/SortTerm.java

@@ -26,15 +26,13 @@ public SortTerm(@NotNull SortKind kind, int lift) {
   public static final @NotNull SortTerm Set0 = new SortTerm(SortKind.Set, 0);
   public static final @NotNull SortTerm Set1 = new SortTerm(SortKind.Set, 1);
   public static final @NotNull SortTerm ISet = new SortTerm(SortKind.ISet, 0);
-  public static final @NotNull SortTerm Prop = new SortTerm(SortKind.Prop, 0);
 
   /**
    * <a href="https://github.com/agda/agda/blob/6a92d584c70a615fdc3f364975814d75a0e31bf7/src/full/Agda/TypeChecking/Substitute.hs#L1541-L1558">Agda</a>
    */
   public @NotNull SortTerm succ() {
     return switch (kind) {
       case Type, Set -> new SortTerm(kind, lift + 1);
-      case Prop -> Type0;
       case ISet -> Set1;
     };
   }

Diff for: base/src/main/java/org/aya/generic/SortKind.java

@@ -1,9 +1,9 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// 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, Prop, ISet;
+  Type, Set, ISet;
 
   public boolean hasLevel() {
     return this == Type || this == Set;

Diff for: base/src/main/java/org/aya/tyck/pat/PatternProblem.java

@@ -64,16 +64,6 @@ record UnavailableCtor(
     }
   }
 
-  record IllegalPropPat(
-    @Override @NotNull Pattern pattern
-  ) implements PatternProblem {
-    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
-      return Doc.vcat(
-        Doc.english("Prop pattern is disallowed in this context:"),
-        Doc.par(1, pattern.toDoc(options)));
-    }
-  }
-
   record UnknownCtor(@Override @NotNull Pattern pattern) implements PatternProblem {
     @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
       return Doc.vcat(

Diff for: base/src/main/java/org/aya/tyck/unify/Synthesizer.java

@@ -46,10 +46,6 @@ public boolean inheritPiDom(@NotNull Term type, @NotNull SortTerm expected) {
     }
     if (!(tryPress(type) instanceof SortTerm actual)) return false;
     return switch (expected.kind()) {
-      case Prop -> switch (actual.kind()) {
-        case Prop, Type -> true;
-        case Set, ISet -> false;
-      };
       case Type -> actual.kind() != SortKind.Set && actual.lift() <= expected.lift();
       case Set -> actual.lift() <= expected.lift();
       case ISet -> unreachable(type);

Diff for: base/src/main/java/org/aya/tyck/unify/TermComparator.java

@@ -95,7 +95,6 @@ private static boolean sortLt(SortTerm l, SortTerm r) {
         case ISet, Set -> true;
         default -> false;
       };
-      case Prop -> r.kind() == SortKind.Prop;
       case Set -> r.kind() == SortKind.Set && lift <= rift;
     };
   }
@@ -253,6 +252,7 @@ private boolean doCompareTyped(@NotNull Term type, @NotNull Term lhs, @NotNull T
     // Note that it looks tempting to apply some unification here, but it is not correct:
     // If ?x =_A y where A : Prop, then it may not be the case that ?x is y!
     // I think Arend has probably made such a mistake before, but they removed this feature anyway.
+    // TODO: revise the above, because `Prop` is now removed
     traceEntrance(new Trace.UnifyT(lhs.freezeHoles(state), rhs.freezeHoles(state),
       pos, type.freezeHoles(state)));
     var ret = switch (type) {

Diff for: base/src/test/java/org/aya/repr/ShapeMatcherTest.java

@@ -41,7 +41,6 @@ open data Fin (n : Nat) | suc n => fzero | suc n => fsuc (Fin n)
 
   @Test
   public void matchList() {
-    match(true, AyaShape.LIST_SHAPE, "data List (A : Prop) | nil | cons A (List A)");
     match(true, AyaShape.LIST_SHAPE, "data List (A : Type) | nil | cons A (List A)");
     match(true, AyaShape.LIST_SHAPE, "data List (A : Type) | cons A (List A) | nil");
     match(true, AyaShape.LIST_SHAPE, "data List (A : Type) | nil | infixr :< A (List A)");

Diff for: base/src/test/resources/failure/projection/issues2/issue879.aya

@@ -6,23 +6,7 @@ def c: Set 1 => ISet
 def e: Set 2 => Unit -> Set 1
 def d: e => \u => ISet
 
-def f: Prop => Sig (A : Prop) ** A
-
 open data Rua : Set | rua
 open import Paths
 def II : ISet => Sig I ** I
 def test : II => (0 , 0)
-
-open data Disj (A B : Prop) : Prop
-| inl (a : A)
-| inr (b : B)
-
-variable A : Type
-
-// Leibniz equality using impredicative universe of propositions
-def Leibniz (x y : A) : Prop
-  => Fn (P : A → Prop) → P x → P y
-
-def refl (a : A) : Leibniz a a => \p x => x
-def symm {x y : A} (p : Leibniz x y)
-  : Leibniz y x => p (\ y' => Leibniz y' x) (refl _)

Diff for: base/src/test/resources/failure/projection/issues2/issue879.aya.txt

@@ -37,7 +37,7 @@ public class ReplCompilerTest {
   }
 
   @Test public void simpleExpr() {
-    compile("Prop");
+    compile("Set");
   }
 
   @Test public void issue382() {