Add Nat::divmod (#1192)

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, sub_Nat, mult, exp, to_Int, to_Nat, is_even, div2, cmp_Nat
+export Nat(), times2, add, sub_Nat, mult, exp, to_Int, to_Nat, is_even, div2, cmp_Nat, divmod
 
 # This is the traditional encoding of natural numbers
 # it is useful when you are iterating on all values
@@ -85,6 +85,19 @@ def div2(n: Nat) -> Nat:
                 else: loop(n, acc, True)
     loop(n, Zero, is_even(n))
 
+def divmod(numerator: Nat, divisor: Nat) -> (Nat, Nat):
+  def loop(numerator: Nat, d: Nat, m: Nat) -> (Nat, Nat):
+    recur numerator:
+      case Zero: (d, m)
+      case Succ(n):
+        m1 = Succ(m)
+        if cmp_Nat(m1, divisor) matches EQ: loop(n, Succ(d), Zero)
+        else: loop(n, d, m1)
+
+  match divisor:
+    case Zero: (Zero, numerator)
+    case _: loop(numerator, Zero, Zero)
+
 one = Succ(Zero)
 
 def exp(base: Nat, power: Nat) -> Nat:

test_workspace/NumberProps.bosatsu

@@ -7,7 +7,7 @@ from Bosatsu/BinNat import (BinNat, toBinNat as int_to_BinNat, is_even as is_eve
   )
 from Bosatsu/Nat import (Nat, Zero as NZero, Succ as NSucc, to_Nat as int_to_Nat, is_even as is_even_Nat,
   times2 as times2_Nat, div2 as div2_Nat, cmp_Nat, to_Int as nat_to_Int, add as add_Nat,
-  mult as mult_Nat, exp as exp_Nat, sub_Nat)
+  mult as mult_Nat, exp as exp_Nat, sub_Nat, divmod as divmod_Nat)
 from Bosatsu/Properties import (Prop, suite_Prop, forall_Prop, run_Prop)
 from Bosatsu/Rand import (Rand, from_pair, geometric_Int, int_range, map_Rand, prod_Rand)
 
@@ -103,6 +103,15 @@ nat_props = suite_Prop(
       t2_2 = mult_Nat(n, NSucc(NSucc(NZero)))
       Assertion(cmp_Nat(t2, t2_2) matches EQ, "times2 == mult(2, _)")
     )),
+    forall_Prop(prod_Rand(rand_Nat, rand_Nat), "divmod homomorphism", ((n1, n2)) -> (
+      (dn, mn) = divmod_Nat(n1, n2)
+      di = div(n1.nat_to_Int(), n2.nat_to_Int())
+      mi = mod_Int(n1.nat_to_Int(), n2.nat_to_Int())
+      Assertion(
+        (eq_Int(dn.nat_to_Int(), di), eq_Int(mn.nat_to_Int(), mi)) matches (True, True),
+        "div Nat")
+    )),
+
   ]
 )