From 49c0d6c13e0ba6c868b6151756695124ba5d77ab Mon Sep 17 00:00:00 2001 From: Oscar Boykin Date: Fri, 15 Mar 2024 13:51:20 -0700 Subject: [PATCH] Add a Bosatsu/Queue property check --- .../org/bykn/bosatsu/PathModuleTest.scala | 4 +- test_workspace/BinNat.bosatsu | 8 ++- test_workspace/Nat.bosatsu | 22 +++++++- test_workspace/Queue.bosatsu | 32 ++++++++++++ test_workspace/Rand.bosatsu | 52 ++++++++++++++++--- 5 files changed, 109 insertions(+), 9 deletions(-) diff --git a/cli/src/test/scala/org/bykn/bosatsu/PathModuleTest.scala b/cli/src/test/scala/org/bykn/bosatsu/PathModuleTest.scala index 9366a67a1..53972ba9a 100644 --- a/cli/src/test/scala/org/bykn/bosatsu/PathModuleTest.scala +++ b/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: _* ) diff --git a/test_workspace/BinNat.bosatsu b/test_workspace/BinNat.bosatsu index fe217229f..33b71bef6 100644 --- a/test_workspace/BinNat.bosatsu +++ b/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: diff --git a/test_workspace/Nat.bosatsu b/test_workspace/Nat.bosatsu index 5b12ed46a..4db783296 100644 --- a/test_workspace/Nat.bosatsu +++ b/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") ]) diff --git a/test_workspace/Queue.bosatsu b/test_workspace/Queue.bosatsu index e94297668..ff78b0399 100644 --- a/test_workspace/Queue.bosatsu +++ b/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), ]) diff --git a/test_workspace/Rand.bosatsu b/test_workspace/Rand.bosatsu index 58076e4ae..25a7b1c3d 100644 --- a/test_workspace/Rand.bosatsu +++ b/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) \ No newline at end of file