search

braibant / articheck

14 stars 2 forks source link

Keep names of functions so as to provide concrete counter-exampels #17

Open protz opened 10 years ago

protz commented 10 years ago

@gasche already mentioned it in another issue and I also though about. I think our GADT should also contain the name of the functions, so that one can build a description of one (among potentially many) sequences of functions that led to a particular element, so that when the element fails to satisfy the predicate, the user can see how we created this element.

gasche commented 10 years ago

I made a first try at this in a private stlc-witnesses branch, and it does not work very well. I hoped to be able to reconstruct the function argument values (and not just their string representation), but it's hard to type statically.

braibant commented 10 years ago

Yup, indeed. However, I do not think that this information should belong to the ('a,'b) fn part. I think it is a matter of the client code that implements the staturation to keep track of this.