search

racket / redex

Other
93 stars 36 forks source link

Pattern matcher infinitely loops on extended union language #224

Closed wilbowma closed 4 years ago

wilbowma commented 4 years ago

This is the smallest example I've come up with

#lang racket/base

(require
 redex/reduction-semantics)

(define-language L1
  [w ::= number]
  [p ::= e]
  [e ::= (pop w)])

(define-language L2
  [e ::= (push w)])

(define-union-language mergeL L1 L2)
(define-extended-language LL mergeL
  [e ::= .... p])

#|
meow.rkt> (redex-match? L1 e (term (push 5)))
#t
meow.rkt> (redex-match? L2 e (term (push 5)))
#t
meow.rkt> (redex-match? mergeL e (term (push 5)))
#t
meow.rkt> (redex-match? LL e (term (push 5)))
|#

The final call, (redex-match? LL e (term (push 5))), seems to loop forever. Each line seems to be necessary, as far as I can tell.

rfindler commented 4 years ago

It looks like you've cleverly defeated Redex's detection of languages that would cause the pattern matcher to loop. Here's a language that's just like LL, except without the extensions and unions and it is a syntax error:

(define-language L
  [w ::= number]
  [p ::= e]
  [e ::= (pop w) (push w) p])
wilbowma commented 4 years ago

Ah. I got there by following a design pattern for generating multi-language semantics. I'll have to be more careful.

rfindler commented 4 years ago

Hopefully redex will be more helpful in that process next time! Thanks for finding the bug.

Robby