define-extended-judgment-form should replace rules with same name

[dvanhorn]

I was surprised to discover that define-extended-judgment-form does not do something similar to extend-reduction-relation when an extension names a rule the same as the underlying relation, i.e. replace that rule with the new one.

Here is a concrete example:

#lang racket
(require redex/reduction-semantics)

(define-language A
  (v ::= integer))

(define-extended-language B A
  (v ::= .... boolean))

(define-judgment-form A
  #:mode (valA I)
  #:contract (valA v)
  [---- id
   (valA v)])

(define-extended-judgment-form B valA
  #:mode (valB I)
  #:contract (valB v)
  [---- id
   (valB boolean)])

(judgment-holds (valB 4))  ;; should produce #f, id rule replaced
(judgment-holds (valB #t)) ;; should produce #t

Being able to do this is critical when you want to extend "helper" judgments by replacing the original rule with a similar rule that use the helper for the extended language.

For example:

#lang racket
(require redex/reduction-semantics)

(define-language A
  (v ::= integer))

(define-extended-language B A
  (v ::= .... boolean))

(define-judgment-form A
  #:mode (valA I)
  #:contract (valA v)
  [(helpA v)
   ---- id
   (valA v)])

(define-judgment-form A
  #:mode (helpA I)
  #:contract (helpA v)
  [-----
   (helpA v)])

(define-extended-judgment-form B valA
  #:mode (valB I)
  #:contract (valB v)  
  [(helpB boolean)
    ---- id
   (valB boolean)])

;; reinterpret helpA over B
(define-extended-judgment-form B helpA
  #:mode (helpB I)
  #:contract (helpB v))

(judgment-holds (helpB #t)) ;; #t, as expected

;; should produce #t, results in a contract violation
;; because helpA is still being used
(judgment-holds (valB #t)) 

It's also conceptually confusing since using define-extended-judgment-form lets you create two distinct rules with the same name, which is not allowed when you to write out the same judgment form without using extension.

[rfindler]

Yeah sounds like a bug to me too. Hope it won't break too many models .... :(

On Sun, Aug 25, 2019 at 10:29 AM David Van Horn notifications@github.com wrote:

I was surprised to discover that define-extended-judgment-form does not do something similar to extend-reduction-relation when an extension names a rule the same as the underlying relation, i.e. replace that rule with the new one.

Here is a concrete example:

lang racket

(require redex/reduction-semantics)

(define-language A (v ::= integer))

(define-extended-language B A (v ::= .... boolean))

(define-judgment-form A

:mode (valA I)

:contract (valA v)

[---- id (valA v)])

(define-extended-judgment-form B valA

:mode (valB I)

:contract (valB v)

[---- id (valB boolean)])

(judgment-holds (valB 4)) ;; should produce #f, id rule replaced (judgment-holds (valB #t)) ;; should produce #t

Being able to do this is critical when you want to extend "helper" judgments by replacing the original rule with a similar rule that use the helper for the extended language.

For example:

lang racket

(require redex/reduction-semantics)

(define-language A (v ::= integer))

(define-extended-language B A (v ::= .... boolean))

(define-judgment-form A

:mode (valA I)

:contract (valA v)

[(helpA v) ---- id (valA v)])

(define-judgment-form A

:mode (helpA I)

:contract (helpA v)

[----- (helpA v)])

(define-extended-judgment-form B valA

:mode (valB I)

:contract (valB v)

[(helpB boolean) ---- id (valB boolean)]) ;; reinterpret helpA over B (define-extended-judgment-form B helpA

:mode (helpB I)

:contract (helpB v))

(judgment-holds (helpB #t)) ;; #t, as expected ;; should produce #t, results in a contract violation;; because helpA is still being used (judgment-holds (valB #t))

It's also conceptually confusing since using define-extended-judgment-form lets you create two distinct rules with the same name, which is not allowed when you to write out the same judgment form without using extension.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/racket/redex/issues/192?email_source=notifications&email_token=AADBNMCPASPRKB7QAVM3TVLQGKQPJA5CNFSM4IPJMK72YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HHHVABQ, or mute the thread https://github.com/notifications/unsubscribe-auth/AADBNMCRSEATMJY4EGDARXLQGKQPJANCNFSM4IPJMK7Q .