(* Natural numbers in unary *)

datatype nat = Zero | Succ of nat

fun add (m, Zero) = m
  | add (m, Succ n) = Succ (add (m, n))

fun mul (m, Zero) = Zero
  | mul (m, Succ n) = add (mul (m, n), m)

fun double Zero = Zero
  | double (Succ m) = Succ (Succ (double m))

fun exp Zero = Succ Zero
  | exp (Succ m) = double (exp m)


(* Lists *)

(* datatype 'a list = nil | :: of 'a * 'a list *)

fun reverse nil = nil
  | reverse (h::t) = t @ [h]

(* Two-three trees *)

datatype 'a two_three_tree =
    Empty
  | Binary of 'a * 'a two_three_tree * 'a two_three_tree
  | Ternary of 'a * 'a two_three_tree * 'a two_three_tree * 'a two_three_tree

fun size Empty = 0
  | size (Binary (_, t1, t2)) = 1 + size t1 + size t2
  | size (Ternary (_, t1, t2, t3)) = 1 + size t1 + size t2 + size t3

(* Recursion patterns *)

fun nat_recursion base step =
    let
	fun loop Zero = base
	  | loop (Succ m) = step (m, loop m)
    in
	loop
    end

val double = nat_recursion (Zero) (fn (_, result) => Succ (Succ result))
val exp = nat_recursion (Succ Zero) (fn (_, result) => double result)

fun list_recursion base step =
    let
	fun loop nil = base
	  | loop (h::t) = step (h, loop t)
    in
	loop
    end

fun reverse l = list_recursion nil (fn (h, t) => t @ [h]) l

fun two_three_recursion base step2 step3 =
    let
	fun loop Empty = base
	  | loop (Binary (v, t1, t2)) =
	    step2 (v, loop t1, loop t2)
	  | loop (Ternary (v, t1, t2, t3)) =
	    step3 (v, loop t1, loop t2, loop t3)
    in
	loop
    end

fun size t =
    two_three_recursion
    0
    (fn (_, s1, s2) => 1+s1+s2)
    (fn (_, s1, s2, s3) => 1+s1+s2+s3)
    t