<div dir="ltr">I like the 3rd approach you mention. Rather than checking that property within mod_live, I think you could prove it as a syntactic property of source_to_mod. (This puts in the same category of other syntactic properties that are required for later phases and proved to be propagated by earlier ones.) It sounds like a reasonably simple property to deal with.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 26 March 2017 at 13:09, Yong Kiam <span dir="ltr"><<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi dev,<div><br></div><div>I've been stuck on mod_live for awhile, the main problem seems to be that this is a legitimate modLang program:</div><div><br></div><div>val 0 = fn () => Global 1</div><div>val 1 = ...</div><div>val 2 = (Global 0) ()</div><div>... Global 1 never read here ...</div><div><br></div><div>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 read.</div><div><br></div><div>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.</div><div><br></div><div>I have two ways around this:</div><div><br></div><div>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:</div><div><br></div><div>val 0 = ...</div><div>val 1 = Global 0</div><div>val 2 = Global 1</div><div>... (0,1,2 all dead, but only 2 would be removed)</div><div><br></div><div>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).</div><div><br></div><div>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).</div><div><br></div><div>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.</div><div><br></div><div>Does anyone have better suggestions? Or am I missing something important?</div><div><br></div></div>
<br>______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
<br></blockquote></div><br></div>