Hi all,
I use the code export of Isabelle and this will generate (poly)ML source code of the following form:
... fun mem l (x :: xs) = (if ((x : IntInf.int) = l) then xs else let val v = mem l xs; in (x :: v) end) | mem l [] = raise (Fail "Cannot find literal"); ...
The function (as many others of that form) can easily be transformed into a tail recursive function.
Does PolyML figure out that it is possible to make this function tail-recursive (automatically) by "unfolding the let"?
Thanks in advance.
Lukas Bulwahn
Lukas Bulwahn wrote:
fun mem l (x :: xs) = (if ((x : IntInf.int) = l) then xs else let val v = mem l xs; in (x :: v) end) | mem l [] = raise (Fail "Cannot find literal");
The function (as many others of that form) can easily be transformed into a tail recursive function.
Can you explain this and preferably give a translation using a while-loop and refs? The function returns the original list with one item removed. In order to be able to rebuild the list it must stack up each item on the list until it either reaches the end or the matching item. It then unwinds the recursion to build the list. I don't see how it can be tail recursive.
David