[racket] [redex] traces for derivation trees

Well, somehow traces already deals with that in some way, with scrolling/zooming (although there are refresh/repaint issues when using zooming). It is indeed overwhelming to use traces with large programs/executions, but it's better than nothing.

I guess I'm saying that the machinery that is already in place for traces would be quite helpful as it is. Then, any HCI improvement will actually benefit both traces and derivations.

-- Éric


On Mar 8, 2012, at 12:27 PM, J. Ian Johnson wrote:

> I am suddenly reminded of Shriram's demo of the stepper with ... to hide steps.
> 
> -Ian
> ----- Original Message -----
> From: "Matthias Felleisen" <matthias at ccs.neu.edu>
> To: "Eric Tanter" <etanter at dcc.uchile.cl>
> Cc: users at racket-lang.org
> Sent: Thursday, March 8, 2012 9:18:38 AM GMT -05:00 US/Canada Eastern
> Subject: Re: [racket] [redex] traces for derivation trees
> 
> 
> 
> Even for small terms, trees will get very large. Whoever tackles this problem needs to think thru the HCI issues of presenting large trees and zooming in and out of pieces -- Matthias
> 
> 
> 
> 
> On Mar 8, 2012, at 8:14 AM, Eric Tanter wrote:
> 
>> Hi Burke,
>> 
>> That's great to hear that you're considering something like that. Like Neil, I'm in the "easy" position of stating a wish.
>> 
>> Neil's description is pretty much what I have in mind. (maybe drawing the derivation tree bottom-up instead of left-to-right, but that's a detail)
>> 
>> -- Éric
>> 
>> 
>> On Mar 7, 2012, at 7:37 PM, Neil Toronto wrote:
>> 
>>> I'd like this, myself. I wouldn't be creating it, so that's easy to say.
>>> 
>>> I imagine something that behaves like `traces' but shows derivation trees instead of expressions, and creates multiple nodes only when a judgment rule is nondeterministic.
>>> 
>>> Neil
>>> 
>>> On 03/07/2012 02:15 PM, Burke Fetscher wrote:
>>>> Hi Eric -
>>>> 
>>>> Unfortunately there isn't a 'traces' equivalent for 'define-judgment-form' right now.  However, as someone who is working on related things in Redex I have had similar thoughts and think it's a great idea, so hopefully we will add it at some point in the future.  And if you have any further ideas about what you would want something like this to look like please send them my way.
>>>> 
>>>> Burke
>>>> 
>>>> On Mar 7, 2012, at 1:16 PM, Eric Tanter wrote:
>>>> 
>>>>> Hi,
>>>>> 
>>>>> As I'm enjoying the new `define-judgment-form' in Redex, I started to dream about an equivalent of `traces' for `judgment-holds'.
>>>>> 
>>>>> I'm going to try to use Redex in a course based on Pierce's TAPL, and once students see `traces' for reduction relations, they will be a bit disappointed by the text-based output for typing derivations that one can obtain by using `current-traced-metafunctions'.
>>>>> 
>>>>> Is there something like that already? if not, does it sound feasible?
>>>>> 
>>>>> Thanks,
>>>>> 
>>>>> -- Éric
>>>>> 
>>>>> ____________________
>>>>> Racket Users list:
>>>>> http://lists.racket-lang.org/users
>>>> 
>>>> 
>>>> ____________________
>>>> Racket Users list:
>>>> http://lists.racket-lang.org/users
>>> 
>>> ____________________
>>> Racket Users list:
>>> http://lists.racket-lang.org/users
>>> 
>> 
>> 
>> ____________________
>> Racket Users list:
>> http://lists.racket-lang.org/users
> 
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users
>