Add Danvy's mystery list function

[mkeoliya]

Example of a function that requires a non-list invariant (i.e non-trivial structure for pre-condition).

type 'a tree =
  | Leaf
  | Node of 'a * 'a tree * 'a tree

let rec reduce f base t =
  match t with
  | Leaf -> base
  | Node (vl, t1, t2) ->
    let t1 = reduce f base t1 in
    let t2 = reduce f base t2 in

    f t1 vl t2

let hd_or ls vl =
  match ls with
  | [] -> vl
  | hd :: _ -> hd

let tl_safe ls  =
  match ls with
  | [] -> []
  | _ :: tl -> tl

let count_and_copy t =
  let s = ref [] in
  let f = (fun t1 vl t2 ->
      let count = 1 + t1 + t2 in
      let t2 = hd_or !s Leaf in
      s := tl_safe !s;
      let t1 = hd_or !s Leaf in
      s := tl_safe !s;
      s := (Node (vl, t1, t2)) :: !s;
      count
    ) in
  let count = reduce f 0 t in
  (count, List.hd !s)