Triage examples that we want to show to newcomers (#392)

app/tests/integration_test.rs

@@ -16,23 +16,24 @@ fn version_command() {
 #[test]
 fn check_command() {
     let mut cmd = Command::cargo_bin(BINARY).unwrap();
-    let assert = cmd.args(vec!["check", "../examples/absurd.pol"]).assert();
-    assert.success().stdout("../examples/absurd.pol typechecked successfully!\n");
+    let assert = cmd.args(vec!["check", "../examples/encoding_scott.pol"]).assert();
+    assert.success().stdout("../examples/encoding_scott.pol typechecked successfully!\n");
 }
 
 /// Check that "pol check" works correctly
 #[test]
 fn check_command_2() {
     let mut cmd = Command::cargo_bin(BINARY).unwrap();
-    let assert = cmd.args(vec!["check", "../examples/imports.pol"]).assert();
-    assert.success().stdout("../examples/imports.pol typechecked successfully!\n");
+    let assert = cmd.args(vec!["check", "../examples/encoding_church.pol"]).assert();
+    assert.success().stdout("../examples/encoding_church.pol typechecked successfully!\n");
 }
 
 /// Check that "pol run" works correctly
 #[test]
 fn run_command() {
     let mut cmd = Command::cargo_bin(BINARY).unwrap();
-    let assert = cmd.env("NO_COLOR", "1").args(vec!["run", "../examples/vect.pol"]).assert();
+    let assert =
+        cmd.env("NO_COLOR", "1").args(vec!["run", "../test/suites/success/037-vect.pol"]).assert();
     assert
         .success()
         .stdout("Cons(S(S(S(Z))), Z, Cons(S(S(Z)), Z, Cons(S(Z), Z, Cons(Z, Z, Nil))))\n");

examples/covect.pol

@@ -1,29 +0,0 @@
-data Nat { Z, S(n: Nat) }
-
-def Nat.add(y: Nat): Nat {
-    Z => y,
-    S(x') => S(x'.add(y))
-}
-
-codata Vec(n: Nat) {
-    Vec(S(n)).tail(n: Nat): Vec(n),
-    Vec(n).append(n m: Nat, ys: Vec(m)): Vec(n.add(m))
-}
-
-codef Nil: Vec(Z) {
-    .append(n, m, ys) => ys,
-    .tail(n) absurd
-}
-
-codef Cons(n' x: Nat, xs: Vec(n')): Vec(S(n')) {
-    .tail(n) => xs,
-    .append(n, m, ys) => Cons(n'.add(m), x, xs.append(n', m, ys))
-}
-
-data Top { Unit }
-
-def Top.example1: Vec(2) { Unit => Cons(1, 0, Cons(0, 0, Nil)) }
-
-def Top.example2: Vec(4) {
-    Unit => Unit.example1.append(2, 2, Unit.example1)
-}

examples/example.pol

@@ -1,17 +0,0 @@
-data Nat { Z, S(n: Nat) }
-
-def Nat.add(y: Nat): Nat {
-    Z => y,
-    S(x') => S(x'.add(y))
-}
-
-data Vec(n: Nat) {
-    Nil: Vec(Z),
-    Cons(n x: Nat, xs: Vec(n)): Vec(S(n))
-}
-
-codata Stream { .head: Nat, .tail: Stream }
-
-codata NatToNat { .ap(x: Nat): Nat }
-
-let main: Nat { 2.add(3) }

examples/neg_inverse.pol

@@ -1,17 +0,0 @@
-data Eq(a: Type, x y: a) {
-    Refl(a: Type, x: a): Eq(a, x, x)
-}
-
-codata Bool { (x: Bool).neg_inverse: Eq(Bool, x, x.not.not), .and(other: Bool): Bool, .not: Bool }
-
-codef True: Bool {
-    .neg_inverse => Refl(Bool, True),
-    .and(other) => other,
-    .not => False
-}
-
-codef False: Bool {
-    .neg_inverse => Refl(Bool, False),
-    .and(other) => False,
-    .not => True
-}

examples/simple.pol

@@ -1,16 +0,0 @@
-data Nat { Z, S(n: Nat) }
-
-data Option(a: Type) {
-    None(a: Type): Option(a),
-    Some(a: Type, x: a): Option(a)
-}
-
-data List(a: Type) {
-    Nil(a: Type): List(a),
-    Cons(a: Type, x: a, xs: List(a)): List(a)
-}
-
-def List(a).head(a: Type): Option(a) {
-    Nil(a) => None(a),
-    Cons(a, x, xs) => Some(a, x)
-}

examples/stream.pol

@@ -1,30 +0,0 @@
-data Nat { Z, S(n: Nat) }
-
-data Bool { T, F }
-
-def Bool.not: Bool {
-    T => F,
-    F => T
-}
-
-def Bool.if_then_else(a: Type, then else: a): a {
-    T => then,
-    F => else
-}
-
-codata Stream { .head: Nat, .tail: Stream }
-
-codef Zeroes: Stream {
-    .head => Z,
-    .tail => Zeroes
-}
-
-codef Ones: Stream {
-    .head => S(Z),
-    .tail => Ones
-}
-
-codef Alternate(choose: Bool): Stream {
-    .head => choose.if_then_else(Nat, S(Z), Z),
-    .tail => Alternate(choose.not)
-}

examples/tutorial.pol

@@ -0,0 +1,60 @@
+data Bool { T, F }
+
+def Bool.not: Bool {
+    T => F,
+    F => T
+}
+
+def Bool.if_then_else(a: Type, then else: a): a {
+    T => then,
+    F => else
+}
+
+data Nat { Z, S(n: Nat) }
+
+def Nat.add(y: Nat): Nat {
+    Z => y,
+    S(x') => S(x'.add(y))
+}
+
+data Vec(n: Nat) {
+    VNil: Vec(Z),
+    VCons(n x: Nat, xs: Vec(n)): Vec(S(n))
+}
+
+codata Stream { .head: Nat, .tail: Stream }
+
+codata NatToNat { .ap(x: Nat): Nat }
+
+let main: Nat { 2.add(3) }
+
+
+data Option(a: Type) {
+    None(a: Type): Option(a),
+    Some(a: Type, x: a): Option(a)
+}
+
+data List(a: Type) {
+    Nil(a: Type): List(a),
+    Cons(a: Type, x: a, xs: List(a)): List(a)
+}
+
+def List(a).hd(a: Type): Option(a) {
+    Nil(a) => None(a),
+    Cons(a, x, xs) => Some(a, x)
+}
+
+codef Zeroes: Stream {
+    .head => Z,
+    .tail => Zeroes
+}
+
+codef Ones: Stream {
+    .head => S(Z),
+    .tail => Ones
+}
+
+codef Alternate(choose: Bool): Stream {
+    .head => choose.if_then_else(Nat, S(Z), Z),
+    .tail => Alternate(choose.not)
+}

test/suites/success/025-imports.pol

@@ -1,5 +1,5 @@
-use "../std/data/nat.pol"
-use "../std/data/bool.pol"
+use "../../../std/data/nat.pol"
+use "../../../std/data/bool.pol"
 
 let one: Nat { 1 }
 

test/suites/success/028-boolrep.pol

@@ -1,4 +1,4 @@
-use "../std/data/bool.pol"
+use "../../../std/data/bool.pol"
 
 data BoolRep(x: Bool) {
     TrueRep: BoolRep(T),
@@ -21,4 +21,4 @@ def Top.flipRep(x: Bool, rep: BoolRep(x)): BoolRep(x.neg) {
 
 def Top.example: Bool {
     Unit => Unit.flipRep(T, TrueRep).extract(F)
-}
+}

test/test-runner/src/phases.rs

@@ -350,8 +350,8 @@ impl Phase for Xfunc {
     async fn run(db: &mut Database, uri: &Url) -> Result<Self::Out, driver::Error> {
         // xfunc tests for these examples are currently disabled due to
         // https://github.com/polarity-lang/polarity/issues/317
-        if uri.as_str().ends_with("examples/comatches.pol")
-            || uri.as_str().ends_with("examples/Webserver.pol")
+        if uri.as_str().ends_with("suites/success/023-comatches.pol")
+            || uri.as_str().ends_with("suites/success/036-webserver.pol")
         {
             return Ok(());
         }