[isabelle-dev] eq_list

[Christian Sternagel]

Dear all,

browsing through the Isabelle sources (as one does once in a while) I 
noticed that 'eq_list' could be implemented slightly more efficient. As 
suggested on this mailing-list I also consulted the history tomes and 
found that in

 
http://isabelle.in.tum.de/repos/isabelle/diff/d59364649bcc/src/Pure/library.ML

where 'eq_list' and 'equal_lists' where unified, the old 'eq_list' 
avoided to separately go through the input lists to compute their 
lengths (as I would have suggested).

1) Why not get rid of the length computations again?

2) The alternating (un)wrapping of pairs in the auxiliary local function 
of 'eq_list' seems unnecessary. (I'm not sure whether the compiler does 
optimize this away anyway or not.)

Those are just peephole optimizations, but they seem easy enough.

What about the following? (As always, I'm interested in historical lore 
as well as your opinions.)

fun eq_list eq (list1, list2) =
   pointer_eq (list1, list2) orelse
     let
       fun eq_lst (x :: xs) (y :: ys) = eq (x, y) andalso eq_lst xs ys
         | eq_lst [] [] = true
         | eq_lst _ _ = false;
     in eq_lst list1 list2 end;

This partly avoids the repeated (un)wrapping of pairs (I guess curried 
infix operators are a historical SML accident, but I digress ...) and 
does not separately compute the length of the given lists.

cheers

chris