Code review: distillation of Set :>: Mu ... and Set :>: Nu ...

[GoogleCodeExporter]

The code in question is in Features.Desc and Features.Nu. I'll focus on:

distill es (SET :>: tm@(C (Mu ltm@(Just _ :?=: _))))

in Features.Desc but the problem is the same for:

distill es (SET :>: tm@(C (Nu ltm@(Just _ :?=: _))))

The documentation of these code was saying:

"If a label is not in scope, we remove it, so the definition appears at the
appropriate place when the proof state is printed."

And then, the code was doing some complex name search. I don't understand the 
documentation nor the purpose of the name search (which was not used). 
Moreover, it prevented me from proper distillation, so I scratched it. 

Did I damaged anything? I wonder if 
[http://code.google.com/p/epigram/issues/detail?id=63] is not a consequence of 
my violence.

Original issue reported on code.google.com by pedag...@gmail.com on 29 Aug 2010 at 1:43

[GoogleCodeExporter]

Issue 63 has been merged into this issue.

Original comment by adamgundry on 31 Aug 2010 at 8:28

[GoogleCodeExporter]

The previous code was extracting the reference from the label, checking whether 
the set was in scope, and if not, distilling the definition of the set rather 
than the label. This meant, for example, that we would get

Nat := Mu NatDesc : Set

rather than

Nat := Nat : Set

appearing in the printed output. As I understand it, this behaviour doesn't 
really make sense with anchors, as they live in a different namespace. I 
suggest we leave the code as-is for the time being, and update the 
documentation and test results for NatDev.pig. Problems like this should be 
dealt with when implementing the source language.

Original comment by adamgundry on 31 Aug 2010 at 8:37