c-sterna at jaist.ac.jp
Wed Oct 24 08:55:37 CEST 2012
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
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
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.
More information about the isabelle-dev