type nat = Zero | Suc of nat
let zero = Zero
let one = Suc zero
let two = Suc one
let three= Suc two
let four = Suc three
let rec nat_of_int = function
| 0 -> Zero
| n -> Suc (nat_of_int (n-1))
let rec int_of_nat = function
| Zero -> 0
| Suc n -> 1 + (int_of_nat n)
let rec add m n = match m with
| Zero -> n
| Suc m -> Suc (add m n)
let _ = add two two = four
let rec mul m n = match m with
| Zero -> Zero
| Suc m -> add n (mul m n)
let _ = mul two two = four
let rec pow m = function
| Zero -> one
| Suc n -> mul m (pow m n)
let _ = pow two two = four
let rec int_of_nat' m = function
| Zero -> m
| Suc n -> int_of_nat' (m+1) n
let int_of_nat n = int_of_nat' 0 n
let rec nat_of_int' m = function
| 0 -> m
| n -> nat_of_int' (Suc m) (n-1)
let nat_of_int m = nat_of_int' Zero m
let rec add m n = match m with
| Zero -> n
| Suc m -> add m (Suc n)
let rec mul' m n p = match m with
| Zero -> p
| Suc m -> mul' n m (add n p)
let mul m n = mul' m n Zero
let rec pow' m n p = match n with
| Zero -> p
| Suc n ->
pow' m n (mul m p)
let rec pow m n = pow' m n one
let rec sub m n = match m, n with
| Zero, _ -> Zero
| m, Zero -> m
| Suc m, Suc n -> sub m n
let _ = sub three two = one
let rec ul_of_nat = function
| Zero -> []
| Suc n -> () :: (ul_of_nat n)
let rec nat_of_ul = function
| [] -> Zero
| _ :: xs -> Suc (nat_of_ul xs)
let zero' = []
let one' = () :: zero'
let two' = () :: one'
let three' = () :: two'
let four' = () :: three'
let _ = nat_of_ul two' = two
let _ = ul_of_nat three = three'
let add_iso m n =
let xs = ul_of_nat m in
let ys = ul_of_nat n in
let zs = xs @ ys in
nat_of_ul zs
type binary = bool list
let rec int_of_bin = function
| [] -> 0
| true :: bs -> 1 + 2 * (int_of_bin bs)
| false :: bs -> 2 * (int_of_bin bs)
let rec bin_of_int = function
| 0 -> []
| n -> (n mod 2 = 1) :: (bin_of_int (n / 2))
let rec string_of_bin = function
| [] -> ""
| true :: bs -> (string_of_bin bs) ^ "1"
| false :: bs -> (string_of_bin bs) ^ "0"
let rec binadd' bs bs' carry = match bs, bs' with
| [], bs | bs, [] when carry -> binadd' bs [carry] false
| [], bs | bs, [] -> bs
| b :: bs, b' :: bs' when b && b' && carry
-> true :: (binadd' bs bs' true)
| b :: bs, b' :: bs' when b && b' || b' && carry || carry && b
-> false :: (binadd' bs bs' true)
| b :: bs, b' :: bs' when b || b' || carry
-> true :: (binadd' bs bs' false)
| b :: bs, b' :: bs'
-> false :: (binadd' bs bs' false)
let binadd bs bs' = binadd' bs bs' false
let big_nat = nat_of_int 1000000
let big_dig = bin_of_int 1000000
let bench op num =
let t0 = Sys.time () in
let _ = op num num in
let t1 = Sys.time () in
print_float (t1 -. t0); print_newline ()
let t = bench add big_nat
let t' = bench binadd big_dig