add complete queue property checks (#1171)

* add complete queue property checks

* make Nat::div2 O(N)

cli/src/test/scala/org/bykn/bosatsu/PathModuleTest.scala

@@ -116,7 +116,7 @@ class PathModuleTest extends AnyFunSuite {
     }
 
   test("test direct run of a file") {
-    val deps = List("Nat", "List", "Bool", "Rand", "Properties")
+    val deps = List("Nat", "List", "Bool", "Rand", "Properties", "BinNat")
     val inputs = deps.map { n => s"--input test_workspace/${n}.bosatsu"}.mkString(" ")
     val out = run(
       s"test $inputs --test_file test_workspace/Queue.bosatsu"

test_workspace/BinNat.bosatsu

@@ -2,7 +2,7 @@ package Bosatsu/BinNat
 
 from Bosatsu/Nat import Nat, Zero as NatZero, Succ as NatSucc, times2 as times2_Nat
 
-export BinNat(), toInt, toNat, toBinNat, next, add_BinNat, times2, div2
+export BinNat(), toInt, toNat, toBinNat, next, add_BinNat, times2, div2, prev
 # a natural number with three variants:
 # Zero = 0
 # Odd(n) = 2n + 1

test_workspace/Nat.bosatsu

@@ -1,7 +1,7 @@
 package Bosatsu/Nat
 
 from Bosatsu/Predef import add as operator +, times as operator *
-export Nat(), times2, add, mult, exp, to_Int, to_Nat
+export Nat(), times2, add, mult, exp, to_Int, to_Nat, is_even, div2
 
 # This is the traditional encoding of natural numbers
 # it is useful when you are iterating on all values
@@ -33,6 +33,23 @@ def mult(n1: Nat, n2: Nat) -> Nat:
         Succ(n2):
           Succ(mult(n1, n2).add(add(n1, n2)))
 
+def is_even(n: Nat) -> Bool:
+    def loop(n: Nat, res: Bool) -> Bool:
+        recur n:
+            case Zero: res
+            case Succ(n): loop(n, False if res else True)
+    loop(n, True)
+
+def div2(n: Nat) -> Nat:
+    def loop(n: Nat, acc: Nat, is_even):
+        recur n:
+            case Zero: acc
+            case Succ(n):
+                # (n + 1) / 2 = n/2 if n is even, else n/2 + 1
+                if is_even: loop(n, Succ(acc), False)
+                else: loop(n, acc, True)
+    loop(n, Zero, is_even(n))
+
 one = Succ(Zero)
 
 def exp(base: Nat, power: Nat) -> Nat:
@@ -104,5 +121,9 @@ tests = TestSuite("Nat tests",
     multLaw(n1, n2, "1 * 2"),
     multLaw(n2, n1, "2 * 1"),
     from_to_suite,
-    Assertion(exp(n2, n5).to_Int() matches 32, "exp(2, 5) == 32")
+    Assertion(exp(n2, n5).to_Int() matches 32, "exp(2, 5) == 32"),
+    Assertion(n1.div2().to_Int() matches 0, "1 div2 == 0"),
+    Assertion(n2.div2().to_Int() matches 1, "2 div2 == 1"),
+    Assertion(n3.div2().to_Int() matches 1, "3 div2 == 1"),
+    Assertion(n4.div2().to_Int() matches 2, "4 div2 == 2"),
   ])

test_workspace/Queue.bosatsu

@@ -2,7 +2,9 @@ package Queue
 
 from Bosatsu/List import eq_List
 from Bosatsu/Rand import (Rand, sequence_Rand, map_Rand, flat_map_Rand,
-  int_range as int_range_Rand, geometric_Int)
+  int_range as int_range_Rand, geometric_Int, one_of, prod_Rand)
+
+from Bosatsu/Nat import (Nat, Zero, Succ, to_Nat as int_to_Nat)
 
 from Bosatsu/Properties import Prop, forall_Prop, suite_Prop, run_Prop
 
@@ -48,7 +50,7 @@ def fold_Queue(Queue(f, b): Queue[a], init: b, fold_fn: (b, a) -> b) -> b:
   b.reverse().foldLeft(front, fold_fn)
 
 def reverse_Queue(Queue(f, b): Queue[a]) -> Queue[a]:
-  Queue(b.reverse(), f.reverse())
+  Queue(b, f)
 
 def eq_Queue(eq_fn: (a, a) -> Bool)(left: Queue[a], right: Queue[a]) -> Bool:
   res = left.fold_Queue((True, right), \(g, right), al ->
@@ -85,14 +87,46 @@ q12 = empty.push(1).push(2)
 
 def samp(r)(fn): flat_map_Rand(r, fn)
 
+rand_int = int_range_Rand(128)
+
 rand_geo_List_Int: Rand[List[Int]] = (
-  rand_int = int_range_Rand(128)
   len <- geometric_Int.samp()
   lst = replicate_List(rand_int, len)
   sequence_Rand(lst)
 )
 
-rand_Queue_Int: Rand[Queue[Int]] = rand_geo_List_Int.map_Rand(from_List)
+queue_from_list = rand_geo_List_Int.map_Rand(from_List)
+
+def rand_Queue_depth(depth: Nat) -> Rand[Queue[Int]]:
+    recur depth:
+        case Zero: queue_from_list
+        case Succ(n):
+          smaller = rand_Queue_depth(n)
+          pop_rand = smaller.map_Rand(pop)
+          push_rand = prod_Rand(rand_int, smaller).map_Rand(((h, q)) -> push(q, h))
+          rev_rand = smaller.map_Rand(reverse_Queue)
+          one_of(pop_rand, [push_rand, rev_rand])
+
+rand_Queue_Int: Rand[Queue[Int]] = rand_Queue_depth(int_to_Nat(50))
+
+def show_List[a](lst: List[a], showa: a -> String) -> String:
+  def inner(lst):
+    recur lst:
+      case []: ""
+      case [a]: showa(a)
+      case [a, *t]:
+        tstr = inner(t)
+        astr = showa(a)
+        "${astr}, ${tstr}"
+
+  middle = inner(lst)
+  "[${middle}]"
+
+def show_Queue[a](q: Queue[a], showa: a -> String) -> String:
+  Queue(f, b) = q
+  frontStr = show_List(f, showa)
+  backStr = show_List(b, showa)
+  "Queue(${frontStr}, ${backStr})"
 
 queue_laws = suite_Prop(
   "queue properties",
@@ -105,7 +139,32 @@ queue_laws = suite_Prop(
                 case [h, *_]: eq_Int(h, i)
                 case _: False
       Assertion(res, "check head")
-    ))
+    )),
+    forall_Prop(rand_Queue_Int, "reverse isomorphism", q -> (
+      rev_tl = q.reverse_Queue().to_List()
+      rev_tl_str = show_List(rev_tl, int_to_String)
+      tl_rev = q.to_List().reverse()
+      tl_rev_str = show_List(tl_rev, int_to_String)
+      res = eq_li(rev_tl, tl_rev)
+      q_str = show_Queue(q, int_to_String)
+      Assertion(res, "rev_tl = ${rev_tl_str} tl_rev = ${tl_rev_str}: ${q_str}")
+    )),
+    forall_Prop(rand_int.prod_Rand(rand_Queue_Int),
+      "push is the same as reverse prepend reverse", ((h, q)) -> (
+      q1 = q.push(h).to_List()
+      q2 = [h, *q.to_List().reverse()].reverse()
+      res = eq_li(q1, q2)
+      Assertion(res, "push isomorphism")
+    )),
+    forall_Prop(rand_Queue_Int, "pop isomorphism", q -> (
+      match q.unpush():
+        case Some((h, t)):
+          list1 = [h, *(t.to_List())]
+          list2 = q.to_List()
+          Assertion(eq_li(list1, list2), "pop non-empty")
+        case None:
+          Assertion(q.to_List() matches [], "empty is only unpush")
+    )),
   ]
 )
 

test_workspace/Rand.bosatsu

@@ -1,9 +1,13 @@
 package Bosatsu/Rand
 
-from Bosatsu/Nat import Nat, Zero, Succ, exp as exp_Nat, to_Int as nat_to_Int, to_Nat as int_to_Nat
+from Bosatsu/Nat import (Nat, Zero, Succ, exp as exp_Nat,
+  to_Int as nat_to_Int, to_Nat as int_to_Nat)
+
+from Bosatsu/BinNat import (BinNat, Zero as BZero, Odd, Even,
+  next as next_BinNat, prev as prev_BinNat, toInt as binNat_to_Int)
 
 export (Rand, run_Rand, prod_Rand, map_Rand, flat_map_Rand, const_Rand,
-  int_range, sequence_Rand, bool_Rand, geometric_Int)
+  int_range, sequence_Rand, bool_Rand, geometric_Int, from_pair, one_of)
 
 struct State(s0: Int, s1: Int, s2: Int, s3: Int)
 struct UInt64(toInt: Int)
@@ -178,4 +182,89 @@ def geometric(depth: Nat, acc: Int) -> Rand[Int]:
                   case False: geometric(prev, acc + 1)
           ))
 
-geometric_Int: Rand[Int] = geometric(nat30, 0)
+geometric_Int: Rand[Int] = geometric(nat30, 0)
+
+def len[a](list: List[a]) -> BinNat:
+    def loop(list, acc):
+        recur list:
+            case []: acc
+            case [_, *t]: loop(t, acc.next_BinNat())
+    loop(list, BZero)
+
+def split_at[a](list: List[a], idx: BinNat) -> (List[a], List[a]):
+  recur list:
+    case []: ([], [])
+    case [h, *t]:
+      match idx:
+        case BZero: ([], list)
+        case _:
+          (left, right) = split_at(t, idx.prev_BinNat())
+          ([h, *left], right)
+
+def from_pair(left: Rand[a], right: Rand[a]) -> Rand[a]:
+    bool_Rand.flat_map_Rand(b -> (
+      match b:
+        case True: left
+        case False: right
+    ))
+
+def one_of[a](head: Rand[a], tail: List[Rand[a]]) -> Rand[a]:
+    unreachable_case = head
+    # invariant: items_len == len(items), and items_len > 0
+    def loop(items_len: BinNat, items: List[Rand[a]]) -> Rand[a]:
+        recur items_len:
+            case BZero:
+                # unreachable, just return head to typecheck
+                unreachable_case
+            case Odd(BZero):
+                # 2 * 0 + 1, just choose the head of the list
+                match items:
+                    case [h, *_]: h
+                    case _:
+                      # unreacheable len > 0, so can't match
+                      unreachable_case
+            case Odd(n):
+                # llen = 2n + 1
+                # split into 1 + n + n 
+                # with weight (n + 1) choose left, and with weight n choose right
+                match items:
+                    case [front, *tail]:
+                        (left, right) = split_at(tail, n)
+                        lrand = loop(n, left)
+                        rrand = loop(n, right)
+                        # equal chance left and right
+                        back = from_pair(lrand, rrand)
+                        int_range(binNat_to_Int(items_len)) \
+                          .flat_map_Rand(idx -> (
+                            match idx:
+                              case 0: front
+                              case _: back
+                          ))
+                    case []: unreachable_case
+            case Even(BZero):
+              # exactly two, choose each equally likely
+              match items:
+                  case [left, right, *_]:
+                    # equal chance left and right
+                    from_pair(left, right)
+                  case _:
+                    unreachable_case
+            case Even(n):
+              # 2n + 2, pull two off, choose them equally likely,
+              match items:
+                  case [f1, f2, *tail]:
+                    front = from_pair(f1, f2)
+                    back = loop(n, tail)
+                    # with prob 1/(n + 1) choose front
+                    int_range(binNat_to_Int(items_len).div(2)) \
+                      .flat_map_Rand(idx -> (
+                        match idx:
+                          case 0: front
+                          case _: back
+                      ))
+                  case _:
+                    unreachable_case
+
+    items = [head, *tail]
+    loop(len(items), items)
+