At present, we convert a tag with arguments into a value in Mu D or IMu I D
i without looking at the description, just by folding over the list of
arguments. This works for the particular descriptions produced by the data
tactic, but tends to break for other descriptions. For example,
make NatD := 'sumD ['zero 'suc] [('constD (Sig ())) 'idD] : Desc ;
elab 'suc 'zero : Mu NatD ;
fails because 'suc 'zero expands to con ['suc 'zero] instead of con ['suc ,
'zero]. Distillation is overly optimistic, and produces tags with arguments
that do not elaborate back into the corresponding value.
We should make the elaboration rules use the description to work out how to
represent arguments appropriately. There will need to be some restrictions
on the description (e.g. for Desc, it must be a 'sumD or a 'sigmaD of an
enumeration), but we should also be able to generate better error messages
when these restrictions are not met.
Original issue reported on code.google.com by adamgundry on 25 May 2010 at 12:17
Original issue reported on code.google.com by
adamgundryon 25 May 2010 at 12:17