For derivations it could even go the other way, ie. starting with just the final deduction steps, and then manually expanding the parts that matter.
-- É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" <matth...@ccs.neu.edu> > To: "Eric Tanter" <etan...@dcc.uchile.cl> > Cc: users@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 > ____________________ Racket Users list: http://lists.racket-lang.org/users
