fix rendering of metafunctions that use ∪, ∨, etc in the range contract

pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt

@@ -444,7 +444,9 @@
      (begin
        (unless (identifier? #'lang)
          (raise-syntax-error #f "expected an identifier in the language position" stx #'lang))
-       (define-values (contract-name dom-ctcs pre-condition codom-contracts post-condition pats)
+       (define-values (contract-name dom-ctcs pre-condition 
+                                     codom-contracts codom-seps post-condition
+                                     pats)
          (split-out-contract stx (syntax-e #'def-form-id) #'body #t))
        (with-syntax* ([((name trms ...) rest ...) (car pats)]
                       [(mode-stx ...) #`(#:mode (name I))]
@@ -462,7 +464,8 @@
   ;; initial test determines if a contract is specified or not
   (cond
     [(pair? (syntax-e (car (syntax->list rest))))
-     (values #f #f #f (list #'any) #f (check-clauses stx syn-error-name (syntax->list rest) relation?))]
+     (values #f #f #f (list #'any) '() #f 
+             (check-clauses stx syn-error-name (syntax->list rest) relation?))]
     [else
      (syntax-case rest ()
        [(id separator more ...)
@@ -475,7 +478,8 @@
                (raise-syntax-error syn-error-name 
                                    "expected clause definitions to follow domain contract"
                                    stx))
-             (values #'id contract #f (list #'any) #f (check-clauses stx syn-error-name clauses #t)))]
+             (values #'id contract #f (list #'any) '() #f
+                     (check-clauses stx syn-error-name clauses #t)))]
           [else
            (unless (eq? ': (syntax-e #'separator))
              (raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator))
@@ -485,10 +489,12 @@
                [(null? more)
                 (raise-syntax-error syn-error-name "expected an ->" stx)]
                [(eq? (syntax-e (car more)) '->)
-                (define-values (raw-clauses rev-codomains pre-condition post-condition)
+                (define-values (raw-clauses rev-codomains rev-codomain-separators
+                                            pre-condition post-condition)
                   (let loop ([prev (car more)]
                              [more (cdr more)]
-                             [codomains '()])
+                             [codomains '()]
+                             [codomain-separators '()])
                     (cond
                       [(null? more)
                        (raise-syntax-error syn-error-name
@@ -497,14 +503,15 @@
                        (define after-this-one (cdr more))
                        (cond
                          [(null? after-this-one)
-                          (values null (cons (car more) codomains) #t #t)]
+                          (values null (cons (car more) codomains) codomain-separators #t #t)]
                          [else
                           (define kwd (cadr more))
                           (cond
                             [(member (syntax-e kwd) '(or ∨ ∪))
                              (loop kwd 
                                    (cddr more)
-                                   (cons (car more) codomains))]
+                                   (cons (car more) codomains)
+                                   (cons (syntax-e kwd) codomain-separators))]
                             [(and (not relation?) 
                                   (or (equal? (syntax-e kwd) '#:pre)
                                       (equal? (syntax-e kwd) '#:post)))
@@ -534,11 +541,13 @@
                                 (set! post (caddr more))])
                              (values remainder
                                      (cons (car more) codomains)
+                                     codomain-separators
                                      pre 
                                      post)]
                             [else
                              (values (cdr more)
                                      (cons (car more) codomains)
+                                     codomain-separators
                                      #t
                                      #t)])])])))
                 (let ([doms (reverse dom-pats)]
@@ -547,6 +556,7 @@
                           doms
                           (if relation? #f pre-condition)
                           (reverse rev-codomains)
+                          (reverse rev-codomain-separators)
                           (if relation? #f post-condition)
                           clauses))]
                [else

pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt

@@ -1192,7 +1192,9 @@
             (raise-syntax-error 
              syn-error-name 
              "expected a previously defined metafunction" orig-stx prev-metafunction))))
-       (let*-values ([(contract-name dom-ctcs pre-condition codom-contracts post-condition pats)
+       (let*-values ([(contract-name dom-ctcs pre-condition 
+                                     codom-contracts codomain-separators post-condition
+                                     pats)
                       (split-out-contract orig-stx syn-error-name #'rest #f)]
                      [(name _) (defined-name (list contract-name) pats orig-stx)])
          (when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
@@ -1217,6 +1219,7 @@
                                                                     (list pre-condition)
                                                                     #f)
                                                               #,codom-contracts
+                                                              '#,codomain-separators
                                                               #,(if post-condition
                                                                     (list post-condition)
                                                                     #f)
@@ -1265,7 +1268,7 @@
     [(_ orig-stx lang prev-metafunction-stx
         name name-predicate
         dom-ctcs-stx pre-condition-stx
-        codom-contracts-stx post-condition-stx
+        codom-contracts-stx codomain-separators-stx post-condition-stx
         pats-stx syn-error-name)
      (let ()
        (define (condition-or-false s)
@@ -1279,6 +1282,7 @@
        (define dom-ctcs (syntax-e #'dom-ctcs-stx))
        (define pre-condition (condition-or-false #'pre-condition-stx))
        (define codom-contracts (syntax-e #'codom-contracts-stx))
+       (define codomain-separators (syntax-e #'codomain-separators-stx))
        (define post-condition (condition-or-false #'post-condition-stx))
        (define pats (syntax-e #'pats-stx))
        (define syn-error-name (syntax-e #'syn-error-name))
@@ -1417,7 +1421,8 @@
                                          #,(with-syntax ([(dom-ctc ...) dom-ctcs])
                                              #`(list (to-lw dom-ctc) ...))
                                          #,(with-syntax ([(codom-ctc ...) codom-contracts])
-                                             #`(list (to-lw codom-ctc) ...)))
+                                             #`(list (to-lw codom-ctc) ...))
+                                         #,codomain-separators)
                                       #'#f)
                                 
                                 ;; body of mf

pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt

@@ -953,11 +953,13 @@
                         [(and contract? lws)
                          (define doms (list-ref lws 0))
                          (define rngs (list-ref lws 1))
+                         (define separators (list-ref lws 2))
                          (render-metafunction-contract
                           (metafunc-proc-lang (metafunction-proc mf))
                           (metafunc-proc-name (metafunction-proc mf))
                           doms
-                          rngs)]
+                          rngs
+                          separators)]
                         [else #f])))
   (define all-eqns (map (λ (mf) (list-ref (metafunc-proc-pict-info (metafunction-proc mf)) 1)) mfs))
   (define all-lhss 
@@ -1141,14 +1143,25 @@
                              null
                              (list sc)))]))))]))
 
-(define (render-metafunction-contract lang name doms rngs)
+(define (render-metafunction-contract lang name doms rngs separators)
   (hbl-append (basic-text (format "~a" name) (metafunction-style))
               (basic-text " : " (default-style))
               (apply hbl-append (add-between (map (λ (x) (lw->pict lang x)) doms) 
                                              (basic-text " " (default-style))))
               (basic-text " → " (default-style))
-              (apply hbl-append (add-between (map (λ (x) (lw->pict lang x)) rngs)
-                                             (basic-text " " (default-style))))))
+              (apply hbl-append 
+                     (add-between (interleave-ctc-separators
+                                   (map (λ (x) (lw->pict lang x)) rngs)
+                                   (map (λ (x) (basic-text (format "~a" x) (default-style)))
+                                        separators))
+                                  (basic-text " " (default-style))))))
+
+(define (interleave-ctc-separators eles betweens)
+  (cond
+    [(null? betweens) eles]
+    [else (list* (car eles)
+                 (car betweens)
+                 (interleave-ctc-separators (cdr eles) (cdr betweens)))]))
 
 (define (metafunction-call name an-lw)
   (struct-copy lw an-lw

pkgs/redex-pkgs/redex-test/redex/tests/bitmap-test.rkt

@@ -148,6 +148,7 @@
          "metafunction-judgment-holds.png"))
 
 (define-metafunction lang
+  T : any any -> 1 ∪ (2 2) ∨ 1234
   [(T x y)
    1
    (side-condition (not (eq? (term x) (term y))))