16 Oct
2007
16 Oct
'07
5:21 p.m.
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