Re: [racket-users] [Redex] test-->>E and trace

[Anton Podkopaev]

Robby,

Thank you very much!

BR,
Anton Podkopaev


BR,
Anton Podkopaev

On Wed, Feb 10, 2016 at 4:34 PM, Anton Podkopaev 
wrote:

> Robby,
>
> Thank you very much!
>
> BR,
> Anton Podkopaev
>
> On Wed, Feb 10, 2016 at 3:50 PM, Robby Findler <
> ro...@eecs.northwestern.edu> wrote:
>
>> Sure. The trick is to use the #:reduce argument and then just ignore
>> the actual reduction relation. A revision of the earlier code
>> demonstrates, as below.
>>
>> Robby
>>
>> #lang racket
>>
>> (require redex)
>>
>> (define-language L (n ::= natural))
>> (define red
>>   (reduction-relation
>>L
>>(--> n ,(max 0 (min 20 (+ (term n) 3
>>(--> n ,(max 0 (min 20 (- (term n) 1))
>>
>> (define (find-path red from to)
>>   (define parents (make-hash))
>>   (let/ec done
>> (let loop ([t from])
>>   (define nexts (apply-reduction-relation red t))
>>   (for ([next (in-list (remove-duplicates nexts))])
>> (cond
>>   [(equal? next to)
>>(hash-set! parents to t)
>>(done)]
>>   [(hash-ref parents next #f)
>>(void)]
>>   [else
>>(hash-set! parents next t)
>>(loop next)]
>>   parents)
>>
>> (define parents (find-path red 0 10))
>> (define children
>>   (for/hash ([(k v) (in-hash parents)]
>>  #:unless (equal? k 0))
>> (values v k)))
>>
>> (traces red 0
>> #:reduce
>> (λ (_ t)
>>   (let/ec k
>> (list (list #f (hash-ref children t (λ () (k '()
>>
>> On Wed, Feb 10, 2016 at 4:08 AM, Anton Podkopaev 
>> wrote:
>> > Robby,
>> >
>> > Thank you, it mostly works for my semantics, and I know how to change
>> the
>> > algorithm for some corner cases.
>> >
>> > Then I have one more question --- then I get terms (a result of
>> > `find-path'), is there a way to show them (and only them) using GUI
>> tools
>> > like `traces' and `stepper'?
>> >
>> >
>> >
>> > BR,
>> > Anton Podkopaev
>> >
>> > On Wed, Feb 10, 2016 at 2:42 AM, Robby Findler <
>> ro...@eecs.northwestern.edu>
>> > wrote:
>> >>
>> >> I'm sorry it took me so long to get back to this. I'm not sure there
>> >> is a good thing to be added to Redex for this problem. Overall, it
>> >> seems like a graph search problem and there are multiple different
>> >> strategies depending on properties of the graph that you're searching.
>> >> It's not too hard to code these up in Racket and then find the best
>> >> one for your task, I would say. And redex's current support is pretty
>> >> simplistic, tailored to models with much less interesting reduction
>> >> graphs than yours has, I think.
>> >>
>> >> If you find what seems to be a particularly useful and general purpose
>> >> search strategy and want it to be included in Redex, I'd be delighted
>> >> if you would make a pull request. In the meantime, I've offered one
>> >> that may or may not work well for your model, below.
>> >>
>> >> hth,
>> >> Robby
>> >>
>> >> #lang racket
>> >> (require redex/reduction-semantics)
>> >> (define-language L (n ::= natural))
>> >> (define red
>> >>   (reduction-relation
>> >>L
>> >>(--> n ,(max 0 (min 20 (+ (term n) 3
>> >>(--> n ,(max 0 (min 20 (- (term n) 1))
>> >>
>> >> (define (find-path red from to)
>> >>   (define parents (make-hash))
>> >>   (let/ec done
>> >> (let loop ([t from])
>> >>   (define nexts (apply-reduction-relation red t))
>> >>   (for ([next (in-list (remove-duplicates nexts))])
>> >> (cond
>> >>   [(equal? next to)
>> >>(hash-set! parents to t)
>> >>(done)]
>> >>   [(hash-ref parents next #f)
>> >>(void)]
>> >>   [else
>> >>(hash-set! parents next t)
>> >>(loop next)]
>> >>   (let loop ([term to])
>> >> (cond
>> >>   [(equal? term from) (list from)]
>> >>   [else (cons term (loop (hash-ref parents term)))])))
>> >>
>> >> (find-path red 0 10)
>> >>
>> >>
>> >> On Sun, Dec 20, 2015 at 6:26 AM, Anton Podkopaev > >
>> >> wrote:
>> >> > Unfortunately, I need something else, because my semantics is highly
>> >> > non-deterministic, and I want to be able to see only paths, which
>> lead
>> >> > to a
>> >> > certain term.
>> >> >
>> >> > BR,
>> >> > Anton Podkopaev
>> >> >
>> >> > 2015-12-18 20:49 GMT+03:00 Robby Findler <
>> ro...@eecs.northwestern.edu>:
>> >> >>
>> >> >> I think you may want to call apply-reduction-relation* with a
>> >> >> #:stop-when argument instead?
>> >> >>
>> >> >> Robby
>> >> >>
>> >> >>
>> >> >> On Fri, Dec 18, 2015 at 5:33 AM, Anton Podkopaev <
>> podkoav...@gmail.com>
>> >> >> wrote:
>> >> >> > Hello, colleagues!
>> >> >> >
>> >> >> > Is there any way to get a term trace from successful test-->>E in
>> >> >> > Redex?
>> >> >> >
>> >> >> > BR,
>> >> >> > Anton Podkopaev, PhD student, SPbSU
>> >> >> >
>> >> >> > --
>> >> >> > You received this message because you are subscribed to the 

Re: [racket-users] [Redex] test-->>E and trace

[Anton Podkopaev]

Robby,

Thank you, it mostly works for my semantics, and I know how to change the
algorithm for some corner cases.

Then I have one more question --- then I get terms (a result of
`find-path'), is there a way to show them (and only them) using GUI tools
like `traces' and `stepper'?



BR,
Anton Podkopaev

On Wed, Feb 10, 2016 at 2:42 AM, Robby Findler 
wrote:

> I'm sorry it took me so long to get back to this. I'm not sure there
> is a good thing to be added to Redex for this problem. Overall, it
> seems like a graph search problem and there are multiple different
> strategies depending on properties of the graph that you're searching.
> It's not too hard to code these up in Racket and then find the best
> one for your task, I would say. And redex's current support is pretty
> simplistic, tailored to models with much less interesting reduction
> graphs than yours has, I think.
>
> If you find what seems to be a particularly useful and general purpose
> search strategy and want it to be included in Redex, I'd be delighted
> if you would make a pull request. In the meantime, I've offered one
> that may or may not work well for your model, below.
>
> hth,
> Robby
>
> #lang racket
> (require redex/reduction-semantics)
> (define-language L (n ::= natural))
> (define red
>   (reduction-relation
>L
>(--> n ,(max 0 (min 20 (+ (term n) 3
>(--> n ,(max 0 (min 20 (- (term n) 1))
>
> (define (find-path red from to)
>   (define parents (make-hash))
>   (let/ec done
> (let loop ([t from])
>   (define nexts (apply-reduction-relation red t))
>   (for ([next (in-list (remove-duplicates nexts))])
> (cond
>   [(equal? next to)
>(hash-set! parents to t)
>(done)]
>   [(hash-ref parents next #f)
>(void)]
>   [else
>(hash-set! parents next t)
>(loop next)]
>   (let loop ([term to])
> (cond
>   [(equal? term from) (list from)]
>   [else (cons term (loop (hash-ref parents term)))])))
>
> (find-path red 0 10)
>
>
> On Sun, Dec 20, 2015 at 6:26 AM, Anton Podkopaev 
> wrote:
> > Unfortunately, I need something else, because my semantics is highly
> > non-deterministic, and I want to be able to see only paths, which lead
> to a
> > certain term.
> >
> > BR,
> > Anton Podkopaev
> >
> > 2015-12-18 20:49 GMT+03:00 Robby Findler :
> >>
> >> I think you may want to call apply-reduction-relation* with a
> >> #:stop-when argument instead?
> >>
> >> Robby
> >>
> >>
> >> On Fri, Dec 18, 2015 at 5:33 AM, Anton Podkopaev 
> >> wrote:
> >> > Hello, colleagues!
> >> >
> >> > Is there any way to get a term trace from successful test-->>E in
> Redex?
> >> >
> >> > BR,
> >> > Anton Podkopaev, PhD student, SPbSU
> >> >
> >> > --
> >> > You received this message because you are subscribed to the Google
> >> > Groups
> >> > "Racket Users" group.
> >> > To unsubscribe from this group and stop receiving emails from it, send
> >> > an
> >> > email to racket-users+unsubscr...@googlegroups.com.
> >> > For more options, visit https://groups.google.com/d/optout.
> >
> >
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] [Redex] test-->>E and trace

[Robby Findler]

Sure. The trick is to use the #:reduce argument and then just ignore
the actual reduction relation. A revision of the earlier code
demonstrates, as below.

Robby

#lang racket

(require redex)

(define-language L (n ::= natural))
(define red
  (reduction-relation
   L
   (--> n ,(max 0 (min 20 (+ (term n) 3
   (--> n ,(max 0 (min 20 (- (term n) 1))

(define (find-path red from to)
  (define parents (make-hash))
  (let/ec done
(let loop ([t from])
  (define nexts (apply-reduction-relation red t))
  (for ([next (in-list (remove-duplicates nexts))])
(cond
  [(equal? next to)
   (hash-set! parents to t)
   (done)]
  [(hash-ref parents next #f)
   (void)]
  [else
   (hash-set! parents next t)
   (loop next)]
  parents)

(define parents (find-path red 0 10))
(define children
  (for/hash ([(k v) (in-hash parents)]
 #:unless (equal? k 0))
(values v k)))

(traces red 0
#:reduce
(λ (_ t)
  (let/ec k
(list (list #f (hash-ref children t (λ () (k '()

On Wed, Feb 10, 2016 at 4:08 AM, Anton Podkopaev  wrote:
> Robby,
>
> Thank you, it mostly works for my semantics, and I know how to change the
> algorithm for some corner cases.
>
> Then I have one more question --- then I get terms (a result of
> `find-path'), is there a way to show them (and only them) using GUI tools
> like `traces' and `stepper'?
>
>
>
> BR,
> Anton Podkopaev
>
> On Wed, Feb 10, 2016 at 2:42 AM, Robby Findler 
> wrote:
>>
>> I'm sorry it took me so long to get back to this. I'm not sure there
>> is a good thing to be added to Redex for this problem. Overall, it
>> seems like a graph search problem and there are multiple different
>> strategies depending on properties of the graph that you're searching.
>> It's not too hard to code these up in Racket and then find the best
>> one for your task, I would say. And redex's current support is pretty
>> simplistic, tailored to models with much less interesting reduction
>> graphs than yours has, I think.
>>
>> If you find what seems to be a particularly useful and general purpose
>> search strategy and want it to be included in Redex, I'd be delighted
>> if you would make a pull request. In the meantime, I've offered one
>> that may or may not work well for your model, below.
>>
>> hth,
>> Robby
>>
>> #lang racket
>> (require redex/reduction-semantics)
>> (define-language L (n ::= natural))
>> (define red
>>   (reduction-relation
>>L
>>(--> n ,(max 0 (min 20 (+ (term n) 3
>>(--> n ,(max 0 (min 20 (- (term n) 1))
>>
>> (define (find-path red from to)
>>   (define parents (make-hash))
>>   (let/ec done
>> (let loop ([t from])
>>   (define nexts (apply-reduction-relation red t))
>>   (for ([next (in-list (remove-duplicates nexts))])
>> (cond
>>   [(equal? next to)
>>(hash-set! parents to t)
>>(done)]
>>   [(hash-ref parents next #f)
>>(void)]
>>   [else
>>(hash-set! parents next t)
>>(loop next)]
>>   (let loop ([term to])
>> (cond
>>   [(equal? term from) (list from)]
>>   [else (cons term (loop (hash-ref parents term)))])))
>>
>> (find-path red 0 10)
>>
>>
>> On Sun, Dec 20, 2015 at 6:26 AM, Anton Podkopaev 
>> wrote:
>> > Unfortunately, I need something else, because my semantics is highly
>> > non-deterministic, and I want to be able to see only paths, which lead
>> > to a
>> > certain term.
>> >
>> > BR,
>> > Anton Podkopaev
>> >
>> > 2015-12-18 20:49 GMT+03:00 Robby Findler :
>> >>
>> >> I think you may want to call apply-reduction-relation* with a
>> >> #:stop-when argument instead?
>> >>
>> >> Robby
>> >>
>> >>
>> >> On Fri, Dec 18, 2015 at 5:33 AM, Anton Podkopaev 
>> >> wrote:
>> >> > Hello, colleagues!
>> >> >
>> >> > Is there any way to get a term trace from successful test-->>E in
>> >> > Redex?
>> >> >
>> >> > BR,
>> >> > Anton Podkopaev, PhD student, SPbSU
>> >> >
>> >> > --
>> >> > You received this message because you are subscribed to the Google
>> >> > Groups
>> >> > "Racket Users" group.
>> >> > To unsubscribe from this group and stop receiving emails from it,
>> >> > send
>> >> > an
>> >> > email to racket-users+unsubscr...@googlegroups.com.
>> >> > For more options, visit https://groups.google.com/d/optout.
>> >
>> >
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] [Redex] test-->>E and trace

[Robby Findler]

I'm sorry it took me so long to get back to this. I'm not sure there
is a good thing to be added to Redex for this problem. Overall, it
seems like a graph search problem and there are multiple different
strategies depending on properties of the graph that you're searching.
It's not too hard to code these up in Racket and then find the best
one for your task, I would say. And redex's current support is pretty
simplistic, tailored to models with much less interesting reduction
graphs than yours has, I think.

If you find what seems to be a particularly useful and general purpose
search strategy and want it to be included in Redex, I'd be delighted
if you would make a pull request. In the meantime, I've offered one
that may or may not work well for your model, below.

hth,
Robby

#lang racket
(require redex/reduction-semantics)
(define-language L (n ::= natural))
(define red
  (reduction-relation
   L
   (--> n ,(max 0 (min 20 (+ (term n) 3
   (--> n ,(max 0 (min 20 (- (term n) 1))

(define (find-path red from to)
  (define parents (make-hash))
  (let/ec done
(let loop ([t from])
  (define nexts (apply-reduction-relation red t))
  (for ([next (in-list (remove-duplicates nexts))])
(cond
  [(equal? next to)
   (hash-set! parents to t)
   (done)]
  [(hash-ref parents next #f)
   (void)]
  [else
   (hash-set! parents next t)
   (loop next)]
  (let loop ([term to])
(cond
  [(equal? term from) (list from)]
  [else (cons term (loop (hash-ref parents term)))])))

(find-path red 0 10)


On Sun, Dec 20, 2015 at 6:26 AM, Anton Podkopaev  wrote:
> Unfortunately, I need something else, because my semantics is highly
> non-deterministic, and I want to be able to see only paths, which lead to a
> certain term.
>
> BR,
> Anton Podkopaev
>
> 2015-12-18 20:49 GMT+03:00 Robby Findler :
>>
>> I think you may want to call apply-reduction-relation* with a
>> #:stop-when argument instead?
>>
>> Robby
>>
>>
>> On Fri, Dec 18, 2015 at 5:33 AM, Anton Podkopaev 
>> wrote:
>> > Hello, colleagues!
>> >
>> > Is there any way to get a term trace from successful test-->>E in Redex?
>> >
>> > BR,
>> > Anton Podkopaev, PhD student, SPbSU
>> >
>> > --
>> > You received this message because you are subscribed to the Google
>> > Groups
>> > "Racket Users" group.
>> > To unsubscribe from this group and stop receiving emails from it, send
>> > an
>> > email to racket-users+unsubscr...@googlegroups.com.
>> > For more options, visit https://groups.google.com/d/optout.
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] [Redex] test-->>E and trace

[Anton Podkopaev]

Unfortunately, I need something else, because my semantics is highly
non-deterministic, and I want to be able to see only paths, which lead to a
certain term.

BR,
Anton Podkopaev

2015-12-18 20:49 GMT+03:00 Robby Findler :

> I think you may want to call apply-reduction-relation* with a
> #:stop-when argument instead?
>
> Robby
>
>
> On Fri, Dec 18, 2015 at 5:33 AM, Anton Podkopaev 
> wrote:
> > Hello, colleagues!
> >
> > Is there any way to get a term trace from successful test-->>E in Redex?
> >
> > BR,
> > Anton Podkopaev, PhD student, SPbSU
> >
> > --
> > You received this message because you are subscribed to the Google Groups
> > "Racket Users" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to racket-users+unsubscr...@googlegroups.com.
> > For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[racket-users] [Redex] test-->>E and trace

[Anton Podkopaev]

Hello, colleagues!

Is there any way to get a term trace from successful test-->>E in Redex?

BR,
Anton Podkopaev, PhD student, SPbSU

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] [Redex] test-->>E and trace

[Matthias Felleisen]

The quickest way is to write a macro that expands to trace plus a test. -- 
Matthias



On Dec 18, 2015, at 6:33 AM, Anton Podkopaev  wrote:

> Hello, colleagues!
> 
> Is there any way to get a term trace from successful test-->>E in Redex?
> 
> BR,
> Anton Podkopaev, PhD student, SPbSU
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] [Redex] test-->>E and trace

[Robby Findler]

I think you may want to call apply-reduction-relation* with a
#:stop-when argument instead?

Robby


On Fri, Dec 18, 2015 at 5:33 AM, Anton Podkopaev  wrote:
> Hello, colleagues!
>
> Is there any way to get a term trace from successful test-->>E in Redex?
>
> BR,
> Anton Podkopaev, PhD student, SPbSU
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.