open Batteries

class virtual number = object(self : 'a)
  method virtual succ : 'a
  method virtual pred : 'a option
end



type lazy_number_data =
  | Number of number
  | Zero
  | Succ of lazy_number_data
  | Sum of lazy_number_data * lazy_number_data

class lazy_number data0 = object
  inherit number
  val data = data0
  method succ = {< data = Succ data >}
  method pred =
    let rec aux = function
      | Number x -> x#pred |> Option.map (fun t -> Number t)
      | Zero -> None
      | Succ x -> Some x
      | Sum (x1, x2) -> begin
          match aux x1 with
          | None -> aux x2
          | Some x1' -> Some (Sum (x1', x2))
        end
    in
    match aux data with
    | None -> None
    | Some data' -> Some {< data = data' >}
end

let lazy_sum x y =
  let lazy_x = Number x in (* This could be x#data is x is an instance of lazy_number *)
  let lazy_y = Number y in
  new lazy_number (Sum (lazy_x, lazy_y))



type unary_number_data =
  | O
  | S of unary_number_data

class unary_number data0 = object
  inherit number
  val data = data0
  method succ = {< data = S data >}
  method pred =
    match data with
    | O -> None
    | S data' -> Some {< data = data' >}
end

let rec unary_number_of_number x =
  match x#pred with
  | None -> O
  | Some x' -> S (unary_number_of_number x')

let unazy_sum x0 y0 =
  let unary_x = unary_number_of_number x0 in (* This could be x0#data if x0 is an instance of unary_number *)
  let rec aux y =
    match y#pred with
    | None -> unary_x
    | Some y' -> S (aux y')
  in
  aux y0