let diff a1 a2 =
let n1 = Array.length a1 in
let n2 = Array.length a2 in
let i1 = ref 0 in
let i2 = ref 0 in
let cpt = ref 0 in
let d = Array.copy a1 in
while !i1 < n1 && !i2 < n2 do
let ai1 = a1.(!i1) in
let c = Atom.compare ai1 a2.(!i2) in
if c = 0 then (incr i1; incr i2)
else if c < 0 then begin
d.(!cpt) <- ai1;
incr cpt;
incr i1
end
else incr i2
done;
while !i1 < n1 do
d.(!cpt) <- a1.(!i1);
incr cpt;
incr i1
done;
Array.sub d 0 !cpt