source: etc/campbell/dev-notes/2011-10-24-freshness.txt

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 739 bytes
Line 
1I've reached the point where I need to use the freshness of names in anger.
2The reason is that I need to generate extra temporary variables and registers
3during stages, but I also need to know that they are paired with the correct
4type in the resulting function.  A failure of fresh name generation would mean
5that all such assertions would become conditional on whether the generator has
6overflowed.
7
8Worse, it may become difficult to use dependent types at all for variables
9whose type ought to depend upon something that may be invalidated by a clash.
10I don't think this happens just now, but it's easy to imagine that adding a
11temporary to a Cminor function might cause the t in an "expr t" to change, and
12the whole thing falls apart.
Note: See TracBrowser for help on using the repository browser.