Metafunctions in O position of Judgment Not Working

[maxsnew]

Small repro:

#lang racket/base

(require redex)

(define-language Simple
  (e unit)
  (t top))

(define-judgment-form Simple
  #:mode (types I O)
  [------------
   (types unit top)])
(define-metafunction Simple
  [(unit2) unit])

(define-metafunction Simple
  [(top2) top])

Everything works fine if there's no metafunction or if a metafunction is used in an I position:

> (judgment-holds (types unit top))
#t
> (judgment-holds (types (unit2) top))
#t

But it fails if you use the metafunction in the O position:

> (judgment-holds (types unit (top2)))
#f

Even though

> (equal? (term (top2)) (car (judgment-holds (types unit t) t)))
#t

[rfindler]

The O positions are syntactically restricted to be patterns (inside judgment forms anyway) and metafunctions can go in patterns. Are you suggesting a different rule? (Can you say what the rule would be?)

[jeapostrophe]

I believe he's saying it is broken

Jay

On Friday, September 25, 2015, Robby Findler notifications@github.com
wrote:

The O positions are syntactically restricted to be patterns (inside
judgment forms anyway) and metafunctions can go in patterns. Are you
suggesting a different rule? (Can you say what the rule would be?)

—
Reply to this email directly or view it on GitHub
#13 (comment).

Jay McCarthy
http://jeapostrophe.github.io

       "Wherefore, be not weary in well-doing,
  for ye are laying the foundation of a great work.

And out of small things proceedeth that which is great."
- D&C 64:33

[maxsnew]

The metafunction top2 should evaluate to top which in the 2nd to last example above, but it doesn't.

[rfindler]

On Fri, Sep 25, 2015 at 3:20 PM, Max S. New notifications@github.com
wrote:

The metafunction top2 should evaluate to top which in the 2nd to last
example above, but it doesn't.

I don't see why you think that. Metafunctions aren't allowed to be used in
patterns. Maybe you're missing the syntax error message? Or maybe you're
thinking of some change to the semantics of Redex that makes it make sense
to put metafunctions in patterns somehow?

Robby

[maxsnew]

Oh above you said metafunctions "can" go into patterns but I see now you meant "can't".

So I guess I'm proposing that in a pattern a metafunction is just evaluated and its output used as a pattern.

[rfindler]

That's a pretty radical change and it would prohibit things like compiling patterns to racket/match, which seems bad. And what scoping rules would you give for that?

[rfindler]

Well, this seems to be a big semantics discussion we could have and so probably best not to do that in a github issue, so I'm closing this. If it seems wrong to you, please reopen.