Skip to content

Commit

Permalink
make tests pass, but expose bug
Browse files Browse the repository at this point in the history
  • Loading branch information
johnynek committed Mar 22, 2024
1 parent fb3e341 commit d32020f
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 11 deletions.
19 changes: 10 additions & 9 deletions test_workspace/BinNat.bosatsu
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,10 @@ def toBinNat(n: Int) -> BinNat:

def cmp_BinNat(a: BinNat, b: BinNat) -> Comparison:
recur a:
case Zero:
match b:
case Odd(_) | Even(_): LT
case Zero: EQ
case Odd(a1):
match b:
case Odd(b1): cmp_BinNat(a1, b1)
Expand All @@ -67,16 +71,13 @@ def cmp_BinNat(a: BinNat, b: BinNat) -> Comparison:
case GT | EQ: GT
case LT: LT
case Zero: GT
case Zero:
match b:
case Odd(_) | Even(_): LT
case Zero: EQ

# this is more efficient potentially than cmp_BinNat
# because at the first difference we can stop. In the worst
# case of equality, the cost is the same.
def eq_BinNat(a: BinNat, b: BinNat) -> Bool:
recur a:
case Zero: b matches Zero
case Odd(n):
match b:
case Odd(m): eq_BinNat(n, m)
Expand All @@ -85,7 +86,6 @@ def eq_BinNat(a: BinNat, b: BinNat) -> Bool:
match b:
case Even(m): eq_BinNat(n, m)
case _: False
case Zero: b matches Zero

# Return the next number
def next(b: BinNat) -> BinNat:
Expand Down Expand Up @@ -155,6 +155,10 @@ def doub_prev(b: BinNat) -> Option[BinNat]:

def sub_Option(left: BinNat, right: BinNat) -> Option[BinNat]:
recur left:
case Zero:
match right:
case Zero: Some(Zero)
case _: None
case Odd(left) as odd:
match right:
case Zero: Some(odd)
Expand Down Expand Up @@ -184,10 +188,6 @@ def sub_Option(left: BinNat, right: BinNat) -> Option[BinNat]:
match sub_Option(left, right):
case Some(n_m): Some(times2(n_m))
case None: None
case Zero:
match right:
case Zero: Some(Zero)
case _: None

def sub_BinNat(left: BinNat, right: BinNat) -> BinNat:
match sub_Option(left, right):
Expand Down Expand Up @@ -325,4 +325,5 @@ test = TestSuite(
Assertion(fib(two).toInt().eq_Int(2), "fib(2) == 2"),
Assertion(fib(three).toInt().eq_Int(3), "fib(3) == 3"),
Assertion(fib(four).toInt().eq_Int(5), "fib(4) == 5"),
Assertion(cmp_BinNat(54.toBinNat(), 54.toBinNat()) matches EQ, "54 == 54"),
])
8 changes: 6 additions & 2 deletions test_workspace/NumberProps.bosatsu
Original file line number Diff line number Diff line change
Expand Up @@ -112,11 +112,15 @@ binnat_props = suite_Prop(
forall_Prop(rand_BinNat, "if is_even(n) then times2(div2(n)) == n", n -> (
if is_even_BinNat(n):
n1 = times2_BinNat(div2_BinNat(n))
Assertion(cmp_BinNat(n1, n) matches EQ, "times2/div2")
n_str = binNat_to_Int(n).int_to_String()
n1_str = binNat_to_Int(n1).int_to_String()
Assertion(cmp_BinNat(n1, n) matches EQ, "even, times2/div2: n = ${n_str}, n1 = ${n1_str}")
else:
# we return the previous number
n1 = times2_BinNat(div2_BinNat(n))
Assertion(cmp_BinNat(n1.next_BinNat(), n) matches EQ, "times2/div2")
n_str = binNat_to_Int(n).int_to_String()
n1_str = binNat_to_Int(n1).int_to_String()
Assertion(cmp_BinNat(n1.next_BinNat(), n) matches EQ, "times2/div2: n = ${n_str}, n1 = ${n1_str}")
)),
forall_Prop(prod_Rand(rand_BinNat, rand_BinNat), "cmp_BinNat matches cmp_Int", ((n1, n2)) -> (
cmp_n = cmp_BinNat(n1, n2)
Expand Down

0 comments on commit d32020f

Please sign in to comment.