search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
48 stars 7 forks source link

Infinite? loop when elaborating data in type with non-standard description #10

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
See ./test/BugDescLoop.pig for example. Presumably this is a bug in the
elaboration case for tags with arguments.

Original issue reported on code.google.com by adamgundry on 13 May 2010 at 11:56

GoogleCodeExporter commented 9 years ago 
The tag with args code is broken with this example, but the flat spin is a 
deeper 
issue, since (with or wi'out the special distill rule active):

elab con ['node (con ['leaf]) (con ['leaf])] : Mu TreeD

Loops, while

con ['node (con ['leaf]) , con ['leaf]] : Mu TreeD

elaborates correctly. The 1st line is type incorrect. Odd.

Original comment by morris...@gmail.com on 25 May 2010 at 10:15

GoogleCodeExporter commented 9 years ago 
Should say, 'node 'leaf 'leaf elaborates into the first line, and so should 
also give 
a type error.

Original comment by morris...@gmail.com on 25 May 2010 at 10:36

GoogleCodeExporter commented 9 years ago 
It looks like the loop is caused by the elaboration cases for treating lists as
inductive data. Removing those cases (and updating TreeD appropriately) gives 
the
expected type error instead of a loop. We only really use these cases for 
writing
enumerations, so we could perhaps get rid of them entirely, or restrict them to 
only
apply for constructing values in EnumU. I will do the latter for the time being,
since it requires fewer updates to test cases, and I think the description of
enumerations is not vulnerable to the problem.

The tag with args code is broken because it expects descriptions to be in a 
certain
format (that generated by the data tactic). Perhaps we can make it more generic.

Original comment by adamgundry on 25 May 2010 at 11:06

GoogleCodeExporter commented 9 years ago 
It would certainly be possible to use the code of the data type to work out how 
to 
pack and unpack the args to tagged data-types. The data tactic does something 
of the 
sort when it creates the smart constructors. For the moment I suggest filing 
another 
issue about it.

Original comment by morris...@gmail.com on 25 May 2010 at 11:57

GoogleCodeExporter commented 9 years ago 
Fixed in trunk (at least as far as the infinite loop is concerned). I will open
another issue for the tag args question.

Original comment by adamgundry on 25 May 2010 at 12:02