end else begin (* top resize *)
(* preventively allocate the space for the following elements *)
let nlen = ((i - offset + 1) lsl 1) + 1 in
end else begin (* top resize *)
(* preventively allocate the space for the following elements *)
let nlen = ((i - offset + 1) lsl 1) + 1 in