[CakeML-dev] Pathological modLang programs
tanyongkiam at gmail.com
Sun Mar 26 02:09:55 UTC 2017
I've been stuck on mod_live for awhile, the main problem seems to be that
this is a legitimate modLang program:
val 0 = fn () => Global 1
val 1 = ...
val 2 = (Global 0) ()
... Global 1 never read here ...
In my current set up, I pass a set of live globals from back to front
through the list of decs, tracking all the globals that could have been
In the above fragment, this approach would delete the val 1 = ... line
because it was never read from back to front. I think only focusing on
deleting Dletrecs does not solve the problem either.
I have two ways around this:
1) fallback to a more naive analysis, i.e. walk through all the
declarations and keep every global that is ever read. This would not be
able to catch chains of dead globals:
val 0 = ...
val 1 = Global 0
val 2 = Global 1
... (0,1,2 all dead, but only 2 would be removed)
2) go to a more complicated one. Not only do I go back to front, but I also
go front to back and track for each global, the set of globals that it can
transitively reference. When a global gets added, this analysis would have
to add all the globals that can be transitively read via that global. (so
when 0 gets added above, it transitively adds 1).
I didn't particularly like 1 or 2 because 1) seems too naive and 2) seems
to difficult (having to deal with termination of the transitive addition).
A potential 3rd approach is to essentially type check the entire program
and only apply the removal [ass if all the globals happen to point in the
right way. i.e. any dec at position n must only mention globals < n. I
think that still works in modLang before any complicated knot tying is done.
Does anyone have better suggestions? Or am I missing something important?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Developers