search

racket / redex

Other
93 stars 36 forks source link

enumerator fails to terminate #186

Closed rfindler closed 5 years ago

rfindler commented 5 years ago

In the program below, the call to generate-term never seems to return.

#lang racket
(require redex/reduction-semantics)
(define-language L
  (m ::= (e))
  (e ::= (f) 1)
  (f ::= e (e ...)))

(printf "starting\n")
(generate-term L m #:i-th 0)
maxsnew commented 5 years ago

I don't have time to look at this right now (POPL deadline looming). But it's probably because of the ordering in an infinitary or/e in the implementation which is making it always produce an inductive case. In particular if you swap the order of the cases in e or f it will work.

There is some code that was supposed to re-order them automatically so that's likely the source of the bug. I can look into it next week.

rfindler commented 5 years ago

Oh, right. Bad timing with the POPL deadline! Thanks.

Robby

On Mon, Jul 8, 2019 at 12:30 PM Max S. New notifications@github.com wrote:

I don't have time to look at this right now (POPL deadline looming). But it's probably because of the ordering in an infinitary or/e in the implementation which is making it always produce an inductive case. In particular if you swap the order of the cases in e or f it will work.

There is some code that was supposed to re-order them automatically so that's likely the source of the bug. I can look into it next week.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/racket/redex/issues/186?email_source=notifications&email_token=AADBNMCNAWNBSKRDHP6U7FTP6OBUVA5CNFSM4H66JDM2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZN6UNA#issuecomment-509340212, or mute the thread https://github.com/notifications/unsubscribe-auth/AADBNMHRX256NNZRXWE2WJ3P6OBUVANCNFSM4H66JDMQ .