(* Unary (Peano) numbers *)

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

(* tail rec version *)
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

(* other operations *)
    
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

(* nat is "isomorphic" to unit list *)

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


(* LECTURE 2 : NUMBERS

 * Lecture 1 recap : 
   * Numbers are just a data type ("Peano" numbers)
   * Definitions `up to iso'
   * The built-in `int' is not (finite, wrap-around arithmetic)
   * The defn of numbers is the mathematical defn
   * The defn of operations is the mathematical defn
   * `Obviously correct', reference implementation
   * May be slow or otherwise inefficient
 *) 






(* Numbers as lists of digits *)

(* Most significant digit to the right *)
    
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)

(* b0 b1 b2 ... bn-1 bn  = bn * 2^0 + bn-1 * 2^1 + ... b1 * 2^(n-1) + b0 * 2^n *) 

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"

(*
    1
1001010
  10010
-------
1011100
*)

(* OCaml new sytax:
 *   match EXP with 
 *   | PATT when COND  -> EXP
 *   | PATT when COND' -> EXP'
 *   | ...
 *   | PATT            -> EXP"
 *   is the same as
 *   match EXP with 
 *   | PATT -> if COND then EXP else if COND' then EXP' else if ... else EXP"
 *)


(* addition *)
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

(* Testing and benchmarks *)

let big_nat = nat_of_int 1000000
let big_dig = bin_of_int 1000000

(* Less conclusive than profiling but more convenient, 
 * It only makes sense on the same machine, under same conditions. 
 * Ideally it must be run repeatedly and average. *)
    
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


(* WARM-UP QUESTIONS *)

(* Q1 : determine whether a bin is odd or even *)

(* Q1 : tail-recursive implementation of ... *)

(* Q1/Q2 : implement Integers, Rationals *)

(* Q2 : binary subtraction *)

(* Q3 : binary multiplication 
   https://en.wikipedia.org/wiki/Ancient_Egyptian_multiplication *)

(* Q3 : efficient representation isomorphic to nat *)

(* Q3 : efficient representations that respect equality *)

(* Q1/Q3 : Sum a list of floats ... while minimising errors *)