Fix tests

src/test/java/org/arend/term/expr/visitor/PrettyPrintingTest.java

@@ -336,7 +336,9 @@ public void revealing2() {
 
   @Test
   public void revealing3() {
-    testRevealing("\\class A { | f {n : Nat} : n = 1 } \\func e (q : A) : q.f = idp => Path.inProp _ _",
+    testRevealing(
+      "\\class A { | f {n : Nat} : n = 1 }\n" +
+      "\\func e (q : A) (p : q.f = idp) : q.f = idp => p",
             (group) -> ((FunctionDefinition) getDefinition(group, "e")).getResultType(),
             "q.f {1} = idp",
             (result) -> result.cast(FunCallExpression.class).getDefCallArguments().get(1).cast(AppExpression.class).getFunction());

src/test/java/org/arend/typechecking/StrictPropTest.java

@@ -11,11 +11,6 @@ public void parametersError() {
     assertThatErrorsAre(Matchers.typecheckingError(NotEqualExpressionsError.class));
   }
 
-  @Test
-  public void parametersTest() {
-    typeCheckDef("\\func f {A : \\Prop} (x y : A) : x = y => Path.inProp _ _");
-  }
-
   @Test
   public void setError() {
     typeCheckDef("\\func f {A : \\Set0} (x y : A) : x = y => idp", 1);
@@ -27,22 +22,12 @@ public void setPathError() {
     assertThatErrorsAre(Matchers.typecheckingError(NotEqualExpressionsError.class));
   }
 
-  @Test
-  public void setPathTest() {
-    typeCheckDef("\\func f {A : \\Set} (x y : A) (p q : x = y) : p = q => Path.inProp _ _");
-  }
-
   @Test
   public void setPiError() {
     typeCheckDef("\\func f {A : \\Set} (x y : A) : \\Pi (p q : = \\levels \\lp 0 x y) -> p = q => \\lam p q => idp", 1);
     assertThatErrorsAre(Matchers.typecheckingError(NotEqualExpressionsError.class));
   }
 
-  @Test
-  public void setPiTest() {
-    typeCheckDef("\\lemma f {A : \\Set} (x y : A) : \\Pi (p q : x = y) -> p = q => Path.inProp");
-  }
-
   @Test
   public void classTest() {
     typeCheckModule(
@@ -52,19 +37,21 @@ public void classTest() {
 
   @Test
   public void classUseLevelError() {
-    typeCheckModule(
-      "\\record B (X : \\Type) (p : \\Pi (x x' : X) -> x = x') (x0 : X)\n" +
-      " \\where \\use \\level levelProp {X : \\Type} {p : \\Pi (x x' : X) -> x = x'} (b b' : B X p) : b = b' => path (\\lam i => \\new B X p (p b.x0 b'.x0 @ i))\n" +
-      "\\func f {X : \\Type} {p : \\Pi (x x' : X) -> x = x'} (b b' : B X p) : b = {B X p} b' => idp", 1);
+    typeCheckModule("""
+      \\record B (X : \\Type) (p : \\Pi (x x' : X) -> x = x') (x0 : X)
+        \\where \\use \\level levelProp {X : \\Type} {p : \\Pi (x x' : X) -> x = x'} (b b' : B X p) : b = b' => path (\\lam i => \\new B X p (p b.x0 b'.x0 @ i))
+      \\func f {X : \\Type} {p : \\Pi (x x' : X) -> x = x'} (b b' : B X p) : b = {B X p} b' => idp
+      """, 1);
     assertThatErrorsAre(Matchers.typecheckingError(NotEqualExpressionsError.class));
   }
 
   @Test
   public void classUseLevelTest() {
-    typeCheckModule(
-      "\\record B (X : \\Type) (p : \\Pi (x x' : X) -> x = x') (x0 : X)\n" +
-      " \\where \\use \\level levelProp {X : \\Type} {p : \\Pi (x x' : X) -> x = x'} (b b' : B X p) : b = b' => path (\\lam i => \\new B X p (p b.x0 b'.x0 @ i))\n" +
-      "\\func f {X : \\Type} {p : \\Pi (x x' : X) -> x = x'} (b b' : B X p) : b = {B X p} b' => Path.inProp b b'");
+    typeCheckModule("""
+      \\record B (X : \\Type) (p : \\Pi (x x' : X) -> x = x') (x0 : X)
+        \\where \\use \\level levelProp {X : \\Type} {p : \\Pi (x x' : X) -> x = x'} (b b' : B X p) : b = b' => path (\\lam i => \\new B X p (p b.x0 b'.x0 @ i))
+      \\func f {X : \\Type} {p : \\Pi (x x' : X) -> x = x'} (b b' : B X p) : \\Prop => b = {B X p} b'
+      """);
   }
 
   @Test

src/test/java/org/arend/typechecking/TruncationsTest.java

@@ -0,0 +1,101 @@
+package org.arend.typechecking;
+
+import org.arend.core.definition.DataDefinition;
+import org.junit.Test;
+
+import static org.junit.Assert.assertTrue;
+
+public class TruncationsTest extends TypeCheckingTestCase {
+  @Test
+  public void elimInProp() {
+    typeCheckModule(
+      "\\truncated \\data TrP (A : \\Type) : \\Prop | inP A\n" +
+      "\\func inP-inv (P : \\Prop) (p : TrP P) : P \\elim p | inP p => p");
+  }
+
+  @Test
+  public void elimInSet1() {
+    typeCheckModule(
+      "\\truncated \\data TrS (A : \\Type) : \\Set | inS A\n" +
+      "\\func inS-inv (A : \\Set) (x : TrS A) : A \\elim x | inS x => x");
+  }
+
+  @Test
+  public void elimInSet2() {
+    typeCheckModule(
+      "\\truncated \\data TrS (A : \\Type) : \\Set | inS A\n" +
+      "\\func trSToNat (A : \\Type) (x : TrS A) : Nat \\elim x | inS x => 0");
+  }
+
+  @Test
+  public void truncPEval() {
+    typeCheckModule("""
+      \\truncated \\data TrP (A : \\Type) : \\Prop | inP A
+      \\func inP-inv (P : \\Prop) (p : TrP P) : P \\elim p | inP p => p
+      \\func trunc-eval (P : \\Prop) (p : TrP P) : \\Prop => inP {P} (inP-inv P p) = {TrP P} p
+      """);
+  }
+
+  @Test
+  public void setTruncationTests() {
+    typeCheckModule("""
+      \\data TrS' (A : \\Type0)
+        | inS' A
+        | truncS' (a a' : TrS' A) (p q : a = a') (i j : I) \\elim i, j {
+          | left, _ => a
+          | right, _ => a'
+          | i, left => p @ i
+          | i, right => q @ i
+        }
+      \\func set-trunc-test (A : \\Type0) (a a' : TrS' A) (p q : a = a') : TrS' A => truncS' a a' p q left left
+      \\func set-trunc-test' (A : \\Type0) (a a' : TrS' A) (p q : a = a') : p = q => path (\\lam i => path (\\lam j => truncS' a a' p q j i))
+      """);
+  }
+
+  @Test
+  public void dynamicSetTruncationTests() {
+    typeCheckClass("""
+      \\data TrS' (A : \\Type0)
+        | inS' A
+        | truncS' (a a' : TrS' A) (p q : a = a') (i j : I) \\elim i, j {
+          | left, _ => a
+          | right, _ => a'
+          | i, left => p @ i
+          | i, right => q @ i
+        }
+      \\func set-trunc-test (A : \\Type0) (a a' : TrS' A) (p q : a = a') : TrS' A => truncS' a a' p q left left
+      \\func set-trunc-test' (A : \\Type0) (a a' : TrS' A) (p q : a = a') : p = q => path (\\lam i => path (\\lam j => truncS' a a' p q j i))
+      """, "");
+  }
+
+  @Test
+  public void S1Level() {
+    DataDefinition definition = (DataDefinition) typeCheckDef("""
+      \\data S1
+        | base
+        | loop I {
+          | left => base
+          | right => base
+        }
+      """);
+    assertTrue(definition.getSort().getPLevel().isClosed() && definition.getSort().getPLevel().getConstant() == 0);
+    assertTrue(definition.getSort().getHLevel().isInfinity());
+  }
+
+  @Test
+  public void useLevel() {
+    typeCheckModule("""
+      \\truncated \\data D (A : \\Type) : \\Set
+        | con A
+        | pathCon (a a' : A) (i : I) \\elim i {
+          | left => con a
+          | right => con a'
+        }
+        \\where \\use \\level proof {A : \\Type} (d1 d2 : D A) : d1 = d2
+          | con a, con a' => path (pathCon a a')
+      \\sfunc f (d : D Nat) : Nat
+        | con _ => 0
+        | pathCon _ _ _ => 0
+      """);
+  }
+}