The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Fri, Dec 16, 2005 at 07:38:20AM -0500, 
roconnor AT theorem.ca
 wrote:

> Does anyone know of a nice way of converting a list into a complete
> binary tree using structural recursion such that the order is
> preserved?

Theoretically, here's how I'd do it. There are several practical
problems whose solution is left as exercise for the reader. I'm
confusing natural numbers and sequences (lists) of bits. argument i of
aux is a numbers of length p, but argument i of aux2 is a number of
length p-1. If we are working on lists of A's then let inhabitant be
an inhabitant of A. (This can be avoided through the use of an "'a
tree option" instead of "'a tree" throughout.)

Maybe you can massage this into something nice. Maybe it completely
doesn't work and it is just fever-induced delirium.

For practical use, the test "i = 2*m" would be replaced by something
faster but equivalent, obviously. And numbers would be sequences one
can efficiently approach from both sides (not lispy lists).

Compilers should read top-level statements in inverse order.

let go l = 
 let n = length l in let p = length n and m = (match n with 1::t -> t) in
 let rec aux tree i =
  if i = 2*m
  then aux2 tree m
  else function
  | h :: t -> aux (place tree i h) (succ i) t
 and aux2 tree i = function
  | []     -> tree
  | h :: t -> aux2 (place tree i h) (succ i) t
 in aux (Leaf inhabitant) 0 l

let place tree i h =
 let rec aux = function
  | (Leaf _) as filler , 0::t -> Node (aux filler t) filler
  | (Leaf _) as filler , 1::t -> Node filler (aux filler t)
  | Node l r, 0::t -> Node (aux l t) r
  | Node l r, 1::t -> Node l (aux r t)
  | Leaf _, [] -> Leaf h
  (* yes, this match is incomplete *)
 in aux tree i

-- 
Lionel