internal error via judgment form

[mfelleisen]

Racket Version

6.12.0.3--2018-02-07(-/f) [3m].

Program

(define-language Flow
  (p ::= ((node x e) ... (solve x x e)))
  (e ::= x integer (edge x e))
  (x ::= (variable-except node edge solve))
  #:binding-forms
  ((node x_n e_n) #:refers-to (shadow x_n ...) ...
   (solve x_from x_to e #:refers-to (shadow x_n ...))))

(define-judgment-form Flow
  #:mode (⊢p I)
  [------------------------------------------------- p
   (⊢p ((node x_n e_n) ... (solve x_from x_to e)))])

(judgment-holds (⊢p ((node b (edge d 30)) (solve a d argmax))))

Expected

a Boolean

Got

  expected: list?
  given: 'b«0»

Hints

1. Removing integer makes the problem disappear.
2. (judgment-holds (⊢p ((node b (edge d 30)) (node d) (solve a d argmax)))) also makes the problem disappear.

The above is distilled down from about 5 pages. I tried to make it smaller and couldn't.

[wilbowma]

Does this do what you want:

#lang racket/base
(require redex/reduction-semantics)

(define-language Flow
  (p ::= ((node x e) ... (solve x x e)))
  (e ::= x integer (edge x e))
  (x ::= (variable-except node edge solve))
  #:binding-forms
  ((node x_n e_n) ... #:...bind (clauses x (shadow clauses x))
   (solve x_from x_to e #:refers-to clauses)))

(define-judgment-form Flow
  #:mode (⊢p I)
  [------------------------------------------------- p
   (⊢p ((node x_n e_n) ... (solve x_from x_to e)))])

(judgment-holds (⊢p ((node b (edge d 30)) (solve a d argmax))))

If so, there's a bug in your binding specification (in addition to the bug in the redex error reporting).

[mfelleisen]

I don't want to fix the program, I want Redex to be fixed so that mistakes such as these don't raise uninformative internal error messages.

[rfindler]

Here's a slightly simpler program with the same bad behavior:

#lang racket
(require redex/reduction-semantics)
(define-language Flow
  (p ::= ((node x e) ...))
  (e ::= x (e e))
  (x ::= variable-not-otherwise-mentioned)
  #:binding-forms
  ((node x_n e_n) #:refers-to (shadow x_n ...) ...))

(define-metafunction Flow
  [(f ((node x_n e_n) ...)) (x_n ...)])

(term (f ((node x x))))

[rfindler]

I spent a little time looking at this a little while ago and thank you very much @wilbowma -- last time I looked at this I thought the original example that @mfelleisen put was supposed to work, as opposed to be a syntax error!

Still, tho, I don't know what the precise condition is that should make this an error. At first I thought it should be a #:refers-to inside an ellipsis, but I see this case in the code that suggests that, at least in some situations, that's supposed to work.

I don't suppose anyone can confirm that this shoud be a syntax error and maybe say what the syntax error should actually be?

[wilbowma]

I'm surprised to see #:refers-to used inside an ellipses; I don't think I've ever used that pattern. My assumption was that It couldn't be used, and instead a #:...bind had to be used.

[rfindler]

Okay! I'll try making that an error and see how it goes.

[rfindler]

I'm thinking that maybe the real error with the simplified example above should be that the x_n inside shadow is inside two ellipses and the x_n that's in the argument to node is inside only one.

[rfindler]

Ah, well it isn't so simple, as I found this in the test suites (thanks for that!)

   (va-vb-lambda (x ...) expr #:refers-to (shadow x ...) ...)

and, judging from how it is used, the intent seems to be that this is an implicit begin the body of a lambda, where each of the exprs can have all of the xs appear free inside (and they'd get bound by the lambda).

This intent seems to be pretty similar to what Matthias wanted in the language at the start of this PR:

(node x_n e_n) #:refers-to (shadow x_n ...) ...

where, I think, the idea was that each e_n can refer to any of the x_ns. There is a missing overall keyword wrapper, tho, which might make a difference somehow.