Add a Bosatsu/Queue property check (#1169)

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

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

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
+export BinNat(), toInt, toNat, toBinNat, next, add_BinNat, times2, div2
 # a natural number with three variants:
 # Zero = 0
 # Odd(n) = 2n + 1
@@ -97,6 +97,12 @@ def times2(b: BinNat) -> BinNat:
       #2(2(n + 1)) = 2((2n + 1) + 1)
       Even(Odd(n))
 
+def div2(b: BinNat) -> BinNat:
+    match b:
+        case Zero: Zero
+        case Odd(n): n
+        case Even(n): prev(n)
+
 # multiply two BinNat together
 def times_BinNat(left: BinNat, right: BinNat) -> BinNat:
   recur left:

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, to_Int, to_Nat
+export Nat(), times2, add, mult, exp, to_Int, to_Nat
 
 # This is the traditional encoding of natural numbers
 # it is useful when you are iterating on all values
@@ -33,6 +33,22 @@ def mult(n1: Nat, n2: Nat) -> Nat:
         Succ(n2):
           Succ(mult(n1, n2).add(add(n1, n2)))
 
+one = Succ(Zero)
+
+def exp(base: Nat, power: Nat) -> Nat:
+    match base:
+        case Zero: one if power matches Zero else Zero
+        case Succ(Zero): one
+        case two_or_more:
+          def loop(power, acc):
+              recur power:
+                  case Zero: acc
+                  case Succ(prev):
+                      # b^(n + 1) = (b^n) * b
+                      loop(prev, acc.mult(two_or_more))
+
+          loop(power, one)
+
 def to_Int(n: Nat) -> Int:
     def loop(acc: Int, n: Nat):
       recur n:
@@ -49,6 +65,9 @@ def to_Nat(i: Int) -> Nat:
 
 n1 = Succ(Zero)
 n2 = Succ(n1)
+n3 = Succ(n2)
+n4 = Succ(n3)
+n5 = Succ(n4)
 
 def operator ==(i0: Int, i1: Int):
     cmp_Int(i0, i1) matches EQ
@@ -85,4 +104,5 @@ 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")
   ])

test_workspace/Queue.bosatsu

@@ -1,6 +1,11 @@
 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)
+
+from Bosatsu/Properties import Prop, forall_Prop, suite_Prop, run_Prop
+
 export (Queue,
   empty_Queue, fold_Queue, push, unpush, pop_value, pop, reverse_Queue, eq_Queue,
   to_List, from_List
@@ -78,6 +83,32 @@ eq_li = eq_List(eq_Int)
 
 q12 = empty.push(1).push(2)
 
+def samp(r)(fn): flat_map_Rand(r, fn)
+
+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_laws = suite_Prop(
+  "queue properties",
+  [
+    forall_Prop(rand_Queue_Int, "pop-law/toList", q -> (
+      res = match q.pop_value():
+          case None: to_List(q) matches []
+          case Some(i):
+            match to_List(q):
+                case [h, *_]: eq_Int(h, i)
+                case _: False
+      Assertion(res, "check head")
+    ))
+  ]
+)
+
 tests = TestSuite("queue tests", [
   Assertion(eq_oi(q12.pop_value(), Some(1)), "1"),
   Assertion(q12.fold_Queue(0,add).eq_Int(3), "fold_Queue add"),
@@ -91,4 +122,5 @@ tests = TestSuite("queue tests", [
   Assertion(from_List([1, 2, 3]).pop().pop().pop().eq_qi(empty), "pop to empty"),
   Assertion(empty.pop().eq_qi(empty), "pop empty is okay"),
   Assertion(to_List(from_List([1, 1, 2, 2, 3, 3])).eq_li([1, 1, 2, 2, 3, 3]), "to/from List"),
+  run_Prop(queue_laws, 100, 4242),
 ])

test_workspace/Rand.bosatsu

@@ -1,7 +1,9 @@
 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
+
 export (Rand, run_Rand, prod_Rand, map_Rand, flat_map_Rand, const_Rand,
-  int_range, sequence_Rand)
+  int_range, sequence_Rand, bool_Rand, geometric_Int)
 
 struct State(s0: Int, s1: Int, s2: Int, s3: Int)
 struct UInt64(toInt: Int)
@@ -77,6 +79,33 @@ def prod_Rand[a, b](ra: Rand[a], rb: Rand[b]) -> Rand[(a, b)]:
 
 def const_Rand[a](a: a) -> Rand[a]: Rand(s -> (s, a))
 
+def xor(a, b):
+    match a:
+        case True: False if b else True
+        case False: b
+
+nat_2 = Succ(Succ(Zero))
+
+def parity(n: Nat, i: Int) -> Bool:
+    recur n:
+        case Zero: (i & 1) matches 1
+        case Succ(p):
+            half_bits = exp_Nat(nat_2, n).nat_to_Int()
+            left_half = i >> half_bits
+            bl = parity(p, left_half)
+            br = parity(p, i)
+            xor(bl, br)
+
+# 2^6 = 64
+zero = Zero
+succ = Succ
+six = zero.succ().succ().succ().succ().succ().succ()
+
+bool_Rand: Rand[Bool] = Rand(s -> (
+  (s, UInt64(i)) = next(s)
+  (s, parity(six, i))
+))
+
 def run_Rand[a](rand: Rand[a], seed: Int) -> a:
   Rand(fn) = rand
   (_, a) = fn(state_from_Int(seed))
@@ -103,17 +132,15 @@ def to_big_Int(us: List[UInt64], acc: Int) -> Int:
     case []: acc
     case [UInt64(h), *t]: to_big_Int(t, (acc << 64) | h)
 
-enum Nat: ZN, SN(n: Nat)
-
-nat30 = int_loop(30, ZN, (i, n) -> (i - 1, SN(n)))
+nat30 = int_to_Nat(30)
 
 def resample(rand_Int: Rand[Int], high: Int, uints: Int) -> Rand[Int]:
   Rand(fn) = rand_Int
   boundary = (1 << (uints * 64)).div(high) * high
   def next(s: State, fuel: Nat) -> (State, Int):
     recur fuel:
-        case ZN: (s, (high - 1).div(2))
-        case SN(n):
+        case Zero: (s, (high - 1).div(2))
+        case Succ(n):
           (s1, i) = fn(s)
           if i.cmp_Int(boundary) matches LT:
             # this sample worked
@@ -139,3 +166,16 @@ def int_range(high: Int) -> Rand[Int]:
       # now we know the integer we get out is >= high
       resample(rand_Int, high, uint_count)
   else: const0
+
+def geometric(depth: Nat, acc: Int) -> Rand[Int]:
+    recur depth:
+        case Zero: const_Rand(acc)
+        case Succ(prev):
+          # prob 1/2 0, prob 1/2 geometric + 1
+          bool_Rand.flat_map_Rand(b -> (
+              match b:
+                  case True: const_Rand(acc)
+                  case False: geometric(prev, acc + 1)
+          ))
+
+geometric_Int: Rand[Int] = geometric(nat30, 0)