recursive case types: add test cases from simple recursive programs o…

…n lists and trees

Summary: Also tested in the runtime, and they all work.

Reviewed By: dlreeves

Differential Revision: D62880628

fbshipit-source-id: 863243ee63d671ae7b90657b5169469dd2221904

hphp/hack/test/typecheck/case_type/recursive/forest.php

@@ -0,0 +1,68 @@
+<?hh
+<<file: __EnableUnstableFeatures('case_types')>>
+
+case type Forest<T> = (Tree<T>, Forest<T>) | null;
+case type Tree<T> = shape(
+    'tree' => T,
+    'forest' => Forest<T>,
+  );
+
+function tree_data<T>(Tree<T> $tree): T {
+  if ($tree is shape(...)) {
+    return $tree['tree'];
+  }
+}
+
+case type Lst<T> = (T, Lst<T>) | null;
+
+function make<T>(vec<T> $trees): Forest<T> {
+  $forest = null;
+  foreach ($trees as $tree) {
+    $forest = tuple(shape('tree' => $tree, 'forest' => $forest), $forest);
+  }
+  return $forest;
+}
+
+function make_rec<T>(Lst<T> $trees): Forest<T> {
+  if ($trees is null) {
+    return null;
+  } else {
+    list($tree_data, $trees) = $trees;
+    $forest = make_rec($trees);
+    $tree = shape('tree' => $tree_data, 'forest' => $forest);
+    return tuple($tree, $forest);
+  }
+}
+
+function make_tail_rec<T>(Lst<T> $trees, Forest<T> $forest_acc): Forest<T> {
+  if ($trees is null) {
+    return $forest_acc;
+  } else {
+    list($tree_data, $trees) = $trees;
+    $tree = shape('tree' => $tree_data, 'forest' => $forest_acc);
+    $forest_acc = tuple($tree, $forest_acc);
+    return make_tail_rec($trees, $forest_acc);
+  }
+}
+
+function to_list<T>(Forest<T> $forest): Lst<T> {
+  if ($forest is null) {
+    return null;
+  } else {
+    list($tree, $forest) = $forest;
+    $tree_data = tree_data($tree);
+    $forest = to_list($forest);
+    return tuple($tree_data, $forest);
+  }
+}
+
+function to_list_tail_rec<T>(Forest<T> $forest, Lst<T> $list_acc): Lst<T> {
+  if ($forest is null) {
+    return $list_acc;
+  } else {
+    list($tree, $forest) = $forest;
+    $tree_data = tree_data($tree);
+    $list_acc = tuple($tree_data, $list_acc);
+    return to_list_tail_rec($forest, $list_acc);
+  }
+}

hphp/hack/test/typecheck/case_type/recursive/forest.php.exp

@@ -0,0 +1,20 @@
+ERROR: File "forest.php", line 4, characters 11-16:
+Cyclic type definition (Typing[4014])
+  File "forest.php", line 4, characters 33-41:
+  Cyclic use is here
+ERROR: File "forest.php", line 16, characters 11-13:
+Cyclic type definition (Typing[4014])
+  File "forest.php", line 16, characters 24-29:
+  Cyclic use is here
+ERROR: File "forest.php", line 10, characters 10-18:
+Invalid return type (Typing[4336])
+  File "forest.php", line 10, characters 39-39:
+  Expected `T`
+  File "forest.php", line 10, characters 10-18:
+  But got `void` because this function does not always return a value
+ERROR: File "forest.php", line 10, characters 1-102:
+This function can exit with and without returning a value (Typing[4421])
+  File "forest.php", line 12, characters 5-25:
+  Returning a value here.
+  File "forest.php", line 10, characters 1-102:
+  This function does not always return a value

hphp/hack/test/typecheck/case_type/recursive/forest_w_type_alias.php

@@ -0,0 +1,163 @@
+<?hh
+<<file: __EnableUnstableFeatures('case_types')>>
+
+case type Lst<T> = (T, Lst<T>) | null;
+
+function reverse_list<T>(Lst<T> $list): Lst<T> {
+  $list_acc = null;
+  while ($list is nonnull) {
+    list($v, $list) = $list;
+    $list_acc = tuple($v, $list_acc);
+  }
+  return $list_acc;
+}
+
+function rev_vec_to_list<T>(vec<T> $vec): Lst<T> {
+  $list = null;
+  foreach ($vec as $v) {
+    $list = tuple($v, $list);
+  }
+  return $list;
+}
+
+function list_to_vec<T>(Lst<T> $list): vec<T> {
+  $vec = vec[];
+  while ($list is nonnull) {
+    list($v, $list) = $list;
+    $vec[] = $v;
+  }
+  return $vec;
+}
+
+case type Forest<T> = Tree<T> | null;
+type Tree<T> = shape(
+  'tree' => T,
+  'forest' => Forest<T>,
+);
+
+function rev_make<T>(vec<T> $trees): Forest<T> {
+  $forest = null;
+  foreach ($trees as $tree) {
+    $forest = shape('tree' => $tree, 'forest' => $forest);
+  }
+  return $forest;
+}
+
+function make_rec<T>(Lst<T> $trees): Forest<T> {
+  if ($trees is null) {
+    return null;
+  } else {
+    list($tree_data, $trees) = $trees;
+    $forest = make_rec($trees);
+    $tree = shape('tree' => $tree_data, 'forest' => $forest);
+    return $tree;
+  }
+}
+
+function rev_make_tail_rec<T>(Lst<T> $trees, Forest<T> $forest_acc): Forest<T> {
+  if ($trees is null) {
+    return $forest_acc;
+  } else {
+    list($tree_data, $trees) = $trees;
+    $forest_acc = shape('tree' => $tree_data, 'forest' => $forest_acc);
+    return rev_make_tail_rec($trees, $forest_acc);
+  }
+}
+
+function to_list_rec<T>(Forest<T> $forest): Lst<T> {
+  if ($forest is null) {
+    return null;
+  } else {
+    $tree_data = $forest['tree'];
+    $forest = to_list_rec($forest['forest']);
+    return tuple($tree_data, $forest);
+  }
+}
+
+function rev_to_list_tail_rec<T>(Forest<T> $forest, Lst<T> $list_acc): Lst<T> {
+  if ($forest is null) {
+    return $list_acc;
+  } else {
+    $tree_data = $forest['tree'];
+    $list_acc = tuple($tree_data, $list_acc);
+    return rev_to_list_tail_rec($forest['forest'], $list_acc);
+  }
+}
+
+function reverse_forest_tail_rec<T>(
+  Forest<T> $forest,
+  Forest<T> $forest_acc,
+): Forest<T> {
+  if ($forest is null) {
+    return $forest_acc;
+  } else {
+    $tree = $forest['tree'];
+    $forest = $forest['forest'];
+    $forest_acc = shape('tree' => $tree, 'forest' => $forest_acc);
+    return reverse_forest_tail_rec($forest, $forest_acc);
+  }
+}
+
+function reverse_forest_tail_rec2<T>(
+  Forest<T> $forest,
+  Forest<T> $forest_acc,
+): Forest<T> {
+  if ($forest is shape(...)) {
+    $tree = $forest['tree'];
+    $forest = $forest['forest'];
+    $forest_acc = shape('tree' => $tree, 'forest' => $forest_acc);
+    return reverse_forest_tail_rec2($forest, $forest_acc);
+  } else {
+    return $forest_acc;
+  }
+}
+
+function reverse_forest<T>(Forest<T> $forest): Forest<T> {
+  return reverse_forest_tail_rec2($forest, null);
+}
+
+function vec_length<T>(vec<T> $vec): int {
+  $len = 0;
+  foreach ($vec as $_) {
+    $len += 1;
+  }
+  return $len;
+}
+
+function vec_equal<T>(vec<T> $vec1, vec<T> $vec2): bool {
+  if (vec_length($vec1) !== vec_length($vec2)) {
+    return false;
+  }
+  foreach ($vec1 as $i => $v) {
+    if ($v !== $vec2[$i]) {
+      return false;
+    }
+  }
+  return true;
+}
+
+function test_list_is<T>(Lst<T> $list, vec<T> $expected): void {
+  $vec = list_to_vec($list);
+  if (!vec_equal($expected, $vec)) {
+    echo "FAIL got\n";
+    var_dump($vec);
+  }
+}
+
+function test_to_list<T>(Forest<T> $forest, vec<T> $expected): void {
+  $list = to_list_rec($forest);
+  test_list_is($list, $expected);
+  $list = rev_to_list_tail_rec($forest, null);
+  test_list_is(reverse_list($list), $expected);
+}
+
+<<__EntryPoint>>
+function main(): void {
+  $vec = vec[1, 2, 3];
+  $forest = reverse_forest(rev_make($vec));
+  test_to_list($forest, $vec);
+  $forest = reverse_forest(make_rec(rev_vec_to_list($vec)));
+  test_to_list($forest, $vec);
+  $forest = rev_make_tail_rec(rev_vec_to_list($vec), null);
+  test_to_list($forest, $vec);
+}

hphp/hack/test/typecheck/case_type/recursive/forest_w_type_alias.php.exp

@@ -0,0 +1,8 @@
+ERROR: File "forest_w_type_alias.php", line 4, characters 11-13:
+Cyclic type definition (Typing[4014])
+  File "forest_w_type_alias.php", line 4, characters 24-29:
+  Cyclic use is here
+ERROR: File "forest_w_type_alias.php", line 32, characters 11-16:
+Cyclic type definition (Typing[4014])
+  File "forest_w_type_alias.php", line 35, characters 15-23:
+  Cyclic use is here

hphp/hack/test/typecheck/case_type/recursive/int_tree.php

@@ -0,0 +1,101 @@
+<?hh
+<<file: __EnableUnstableFeatures('case_types')>>
+
+case type A = vec<A> | int;
+
+function make_A_rec(int $depth, int $elt): A {
+  if ($depth === 0) {
+    return $elt;
+  }
+  return vec[make_A_rec($depth - 1, $elt)];
+}
+
+function make_A_rec2(A $a, int $depth): A {
+  if ($depth > 0) {
+    return make_A_rec2(vec[$a], $depth - 1);
+  } else {
+    return $a;
+  }
+}
+
+function make_A(int $depth, int $elt): A {
+  return make_A_rec2($elt, $depth);
+}
+
+function is_empty(A $a): bool {
+  if ($a is vec<_>) {
+    foreach ($a as $_) {
+      return false;
+    }
+    return true;
+  } else {
+    return false;
+  }
+}
+
+function depth(A $a): int {
+  if ($a is vec<_>) {
+    if (is_empty($a)) {
+      return 1;
+    } else {
+      return 1 + depth($a[0]);
+    }
+  } else {
+    return 0;
+  }
+}
+
+function depth_b(A $a): int {
+  if ($a is int) {
+    return 0;
+  } else {
+    if (is_empty($a)) {
+      return 1;
+    } else {
+      return 1 + depth_b($a[0]);
+    }
+  }
+}
+
+function depth2(A $a): int {
+  if ($a is vec<_>) {
+    $depth = 0;
+    foreach ($a as $a1) {
+      $elt_depth = depth2($a1);
+      if ($elt_depth > $depth) {
+        $depth = $elt_depth;
+      }
+    }
+    return 1 + $depth;
+  } else {
+    return 0;
+  }
+}
+
+function depth2_b(A $a): int {
+  if ($a is int) {
+    return 0;
+  } else {
+    $depth = 0;
+    foreach ($a as $a1) {
+      $elt_depth = depth2_b($a1);
+      if ($elt_depth > $depth) {
+        $depth = $elt_depth;
+      }
+    }
+    return 1 + $depth;
+  }
+}
+
+<<__EntryPoint>>
+function main(): void {
+  $a = make_A(10, 0);
+  $depth = depth($a);
+  $depth_b = depth_b($a);
+  $depth2 = depth2($a);
+  $depth2_b = depth2_b($a);
+  echo "depth = $depth\n";
+  echo "depth_b = $depth_b\n";
+  echo "depth2 = $depth2\n";
+  echo "depth2_b = $depth2_b\n";
+}

hphp/hack/test/typecheck/case_type/recursive/int_tree.php.exp

@@ -0,0 +1,4 @@
+ERROR: File "int_tree.php", line 4, characters 11-11:
+Cyclic type definition (Typing[4014])
+  File "int_tree.php", line 4, characters 19-19:
+  Cyclic use is here