where/error doesn't report errors sometimes about redex HOT 8 CLOSED

I think I get what you're saying, but do you think you could make a standalone example just to make sure I'm getting it right?

from redex.

Yes. I was just too lazy and wanted to file the issue before I forgot the problem. I'll circle back to it.

from redex.

Standalone example:

#lang racket
(require redex/reduction-semantics)

(define-language issue-254
  (Id ::= variable-not-otherwise-mentioned)
  )

(define-metafunction issue-254
  test-function : Id Id -> boolean

  [(test-function Id_1 Id)
   #t
   (where/error Id Id_1)
   ]
  )

(pretty-print (term (test-function Foo Bar)))

Running this yields:

> racket -l errortrace -l racket/base -e '(require "src/issue254.rkt")' 
test-function: no clauses matched for (test-function Foo Bar)
  errortrace...:
   /home/nmatsakis/versioned/mir-formality/src/issue254.rkt:17:20: (test-function Foo Bar)
   /home/nmatsakis/versioned/mir-formality/src/issue254.rkt:17:14: (term (test-function Foo Bar))
   /home/nmatsakis/versioned/mir-formality/src/issue254.rkt:17:0: (pretty-print (term (test-function Foo Bar)))
  context...:
   /home/nmatsakis/stow/racket/share/pkgs/redex-lib/redex/private/error.rkt:10:0: redex-error
   /home/nmatsakis/versioned/mir-formality/src/issue254.rkt:17:0
   body of "/home/nmatsakis/versioned/mir-formality/src/issue254.rkt"
   body of top-level

but I expect to see "define-metafunction: where/error did not match"

from redex.

@shhyou it looks like there is an explicit test case checking for something very close to this situation that disagrees with this issue.

Here's the commit and here's the relevant test case.

I am currently disagreeing with the existing test case and have put a candidate commit on a branch. There are a bunch of details in the commit because #f can come out for a lack of a match and also because the clause returns #f so that's why the extra thunk was introduced.

Anyway, what do you think?

from redex.

I don't really get the fix, so let me ask this instead. Does the fix distinguish between these three situations?

1. Match failure in where/error because the shape of the pattern doesn't match
2. Match failure in where/error because repeated names are assigned non-equal values
3. Match failure in other where clauses that come after where/error in the same metafunction case

It looks like the existing code conflated case 2 and 3, which I suppose is wrong.

from redex.

I think it does!

I think the third case is separated from the second case because it goes through a different code path; a where/error ends up in the helper function combine-where/error-results and a where (no /error) ends up in combine-where-results/flatten. (I had to change that path, but only because I changed the shape of the code that the macro generates that's in common to the two paths.)

Do you have an idea for a new test case maybe?

from redex.

Here is an attempt of case 2. I am not sure if this will take a different path from the test case at line 708--716.

(define-metafunction empty-language
  [(f integer)
   0
   (where/error integer 3)
   (where #t #t)]
  [(f _) 1])

(with-handlers ([exn:fail? exn-message])
  (term (f 4))) ;; => #rx"where/error"

Here is an attempt of case 3:

(define-metafunction empty-language
  [(h integer)
   0
   (where/error integer 3)
   (where integer 4)]
  [(h _) 1])

(term (h 3)) ;; => should be 1
(with-handlers ([exn:fail? exn-message])
  (term (h 4))) ;; => #rx"where/error"

from redex.

Thanks! I think the test case probably should be changed. If you think there is more to worry about or I'm missing something, then please let me know!

from redex.