Changes syntax for define-judgment-form mode and contract specs

collects/redex/private/reduction-semantics.rkt

@@ -1345,7 +1345,7 @@
          (let ()
            (let*-values ([(contract-name dom-ctcs codom-contracts pats)
                           (split-out-contract orig-stx syn-error-name #'rest relation?)]
-                         [(name _) (defined-name contract-name pats orig-stx)])
+                         [(name _) (defined-name (list contract-name) pats orig-stx)])
              (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
                            [(lhs-for-lw ...) (lhs-lws pats)])
                (with-syntax ([((rhs stuff ...) ...) (if relation?
@@ -1494,7 +1494,7 @@
              [syn-err-name (syntax-e #'def-form-id)])
          (define nts (definition-nts lang stx syn-err-name))
          (define-values (judgment-form-name dup-form-names mode position-contracts clauses)
-           (parse-define-judgment-form-body #'body syn-err-name stx))
+           (parse-judgment-form-body #'body syn-err-name stx))
          (define definitions
            #`(begin
                (define-syntax #,judgment-form-name 
@@ -1528,48 +1528,50 @@
           'disappeared-use
           (map syntax-local-introduce dup-form-names)))]))
   
-  (define (parse-define-judgment-form-body body syn-err-name full-stx)
-    (define-values (mode rest-body)
-      (parse-mode-spec body full-stx))
-    (define-values (declared-form-name contracts clauses)
-      (syntax-case rest-body ()
-        [(form-name . rest-contract+clauses)
-         (identifier? #'form-name)
-         (let-values ([(contracts clauses)
-                       (parse-relation-contract #'rest-contract+clauses syn-err-name full-stx)])
-           (values #'form-name contracts clauses))]
-        [_ (values #f #f (syntax->list rest-body))]))
-    (check-clauses full-stx syn-err-name clauses #t)
-    (check-arity-consistency mode contracts clauses full-stx)
+  (define (parse-judgment-form-body body syn-err-name full-stx)
+    (define-syntax-class pos-mode
+      #:literals (I O)
+      (pattern I)
+      (pattern O))
+    (define-syntax-class mode-spec
+      #:description "mode specification"
+      (pattern (_:id _:pos-mode ...)))
+    (define-syntax-class contract-spec
+      #:description "contract specification"
+      (pattern (_:id _:expr ...)))
+    (define-values (name/mode mode name/contract contract rules)
+      (syntax-parse body #:context full-stx
+        [((~or (~seq #:mode ~! mode:mode-spec)
+               (~seq #:contract ~! contract:contract-spec))
+          ... . rules:expr)
+         (let-values ([(name/mode mode)
+                       (syntax-parse #'(mode ...)
+                         [((name . mode)) (values #'name (syntax->list #'mode))]
+                         [_ (raise-syntax-error 
+                             #f "expected definition to include a mode specification"
+                             full-stx)])]
+                      [(name/ctc ctc)
+                       (syntax-parse #'(contract ...)
+                         [() (values #f #f)]
+                         [((name . contract)) (values #'name (syntax->list #'contract))]
+                         [(_ . dups)
+                          (raise-syntax-error 
+                           syn-err-name "expected at most one contract specification"
+                           #f #f (syntax->list #'dups))])])
+           (values name/mode mode name/ctc ctc #'rules))]))
+    (check-clauses full-stx syn-err-name rules #t)
+    (check-arity-consistency mode contract full-stx)
     (define-values (form-name dup-names)
-      (syntax-case clauses ()
-        [() (raise-syntax-error #f "expected at least one clause after mode" full-stx)]
-        [_ (defined-name declared-form-name clauses full-stx)]))
-    (values form-name dup-names mode contracts clauses))
+      (syntax-case rules ()
+        [() (raise-syntax-error #f "expected at least one rule" full-stx)]
+        [_ (defined-name (list name/mode name/contract) rules full-stx)]))
+    (values form-name dup-names mode contract rules))
   
-  (define (check-arity-consistency mode contracts clauses full-def)
+  (define (check-arity-consistency mode contracts full-def)
     (when (and contracts (not (= (length mode) (length contracts))))
       (raise-syntax-error 
        #f "mode and contract specify different numbers of positions" full-def)))
   
-  (define (parse-mode-spec body full-stx)
-    (syntax-case body (mode :)
-      [(mode : . rest-body)
-       (let loop ([rest-body #'rest-body]
-                  [pos-modes '()]
-                  [idx 1])
-         (syntax-case rest-body (I O)
-           [(I . more) 
-            (loop #'more (cons 'I pos-modes) (+ 1 idx))]
-           [(O . more)
-            (loop #'more (cons 'O pos-modes) (+ 1 idx))]
-           [_ (values (reverse pos-modes) rest-body)]))]
-      [_ (raise-syntax-error 
-          #f "expected a mode specification after the language declaration"
-          (if (pair? (syntax-e body))
-              (car (syntax-e body))
-              full-stx))]))
-  
   (define (lhss-bound-names lhss nts syn-error-name)
     (let loop ([lhss lhss])
       (if (null? lhss)
@@ -1581,14 +1583,15 @@
             (values (cons names namess)
                     (cons names/ellipses namess/ellipsess))))))
   
-  (define (defined-name declared-name clauses orig-stx)
+  (define (defined-name declared-names clauses orig-stx)
     (with-syntax ([(((used-names _ ...) _ ...) ...) clauses])
       (define-values (the-name other-names)
-        (if declared-name
-            (values declared-name 
-                    (syntax->list #'(used-names ...)))
-            (values (car (syntax->list #'(used-names ...)))
-                    (cdr (syntax->list #'(used-names ...))))))
+        (let ([present (filter values declared-names)])
+          (if (null? present)
+              (values (car (syntax->list #'(used-names ...)))
+                      (cdr (syntax->list #'(used-names ...))))
+              (values (car present) 
+                      (append (cdr present) (syntax->list #'(used-names ...)))))))
       (let loop ([others other-names])
         (cond
           [(null? others) (values the-name other-names)]
@@ -1596,9 +1599,7 @@
            (unless (eq? (syntax-e the-name) (syntax-e (car others)))
              (raise-syntax-error 
               #f
-              (if declared-name
-                  "expected each clause and the contract to use the same name"
-                  "expected each clause to use the same name")
+              "expected the same name in both positions"
               orig-stx
               the-name (list (car others))))
            (loop (cdr others))]))))
@@ -2127,6 +2128,11 @@
             stx
             #'id)))]))
 
+(define-for-syntax (mode-keyword stx)
+  (raise-syntax-error #f "keyword invalid outside of mode specification" stx))
+(define-syntax I mode-keyword)
+(define-syntax O mode-keyword)
+
 (define-syntax (::= stx)
   (raise-syntax-error #f "cannot be used outside a language definition" stx))
 
@@ -2720,7 +2726,7 @@
                [else #f]))))
 
 (provide (rename-out [-reduction-relation reduction-relation])
-         --> fresh with ::= ;; macro keywords
+         --> fresh with ::= I O ;; macro keywords
          reduction-relation->rule-names
          extend-reduction-relation
          reduction-relation?

collects/redex/redex.scrbl

@@ -1069,17 +1069,17 @@ legtimate inputs according to @racket[metafunction-name]'s contract,
 and @racket[#f] otherwise.
 }
 
-@defform/subs[#:literals (mode : I O ⊂ ⊆ × x where)
+@defform/subs[#:literals (I O where)
              (define-judgment-form language
-               mode-spec
-               maybe-contract
-               [conclusion premise ...] ...)
-             ([mode-spec (code:line mode : use ...)]
-              [use I
-                   O]
-              [maybe-contract (code:line)
-                              (code:line form-id ⊂ @#,ttpattern x ... x @#,ttpattern)
-                              (code:line form-id ⊆ @#,ttpattern × ... × @#,ttpattern)]
+               option ...
+               rule ...)
+             ([option mode-spec
+                      contract-spec]
+              [mode-spec (code:line #:mode (form-id pos-use ...))]
+              [contract-spec (code:line #:contract (form-id @#,ttpattern ...))]
+              [pos-use I
+                       O]
+              [rule [conclusion premise ...]]
               [conclusion (form-id pat/term ...)]
               [premise (judgment-form-id pat/term ...)
                        (where @#,ttpattern @#,tttterm)]
@@ -1088,11 +1088,11 @@ and @racket[#f] otherwise.
 Defines @racket[form-id] as a relation on terms via a set of inference rules.
 Each rule must be such that its premises can be evaluated left-to-right
 without ``guessing'' values for any of their pattern variables. Redex checks this
-property using the @racket[mode-spec] declaration, which partitions positions
+property using the mandatory @racket[mode-spec] declaration, which partitions positions
 into inputs @racket[I] and outputs @racket[O]. Output positions in conclusions
 and input positions in premises must be @|tttterm|s with no uses of 
 @racket[unquote]; input positions in conclusions and output positions in 
-premises must be @|ttpattern|s. When the optional @racket[relation-contract] 
+premises must be @|ttpattern|s. When the optional @racket[contract-spec] 
 declaration is present, Redex dynamically checks that the terms flowing through
 these positions match the provided patterns, raising an exception recognized by 
 @racket[exn:fail:redex] if not.
@@ -1103,8 +1103,8 @@ For example, the following defines addition on natural numbers:
        (define-language nats
          (n z (s n)))
        (define-judgment-form nats
-         mode : I I O
-         sum ⊆ n × n × n
+         #:mode (sum I I O)
+         #:contract (sum n n n)
          [(sum z n n)]
          [(sum (s n_1) n_2 (s n_3))
           (sum n_1 n_2 n_3)])]
@@ -1130,8 +1130,8 @@ to compute all pairs with a given sum.
 @interaction[
 #:eval redex-eval
        (define-judgment-form nats
-         mode : O O I
-         sumr ⊆ n × n × n
+         #:mode (sumr O O I)
+         #:contract (sumr n n n)
          [(sumr z n n)]
          [(sumr (s n_1) n_2 (s n_3))
           (sumr n_1 n_2 n_3)])
@@ -1142,8 +1142,8 @@ and @racket[define-metafunction].
 @interaction[
 #:eval redex-eval
        (define-judgment-form nats
-         mode : I I
-         le ⊆ n × n
+         #:mode (le I I)
+         #:contract (le n n)
          [(le z n)]
          [(le (s n_1) (s n_2))
           (le n_1 n_2)])
@@ -1152,8 +1152,8 @@ and @racket[define-metafunction].
          [(pred z) #f]
          [(pred (s n)) n])
        (define-judgment-form nats
-         mode : I I
-         gt ⊆ n × n
+         #:mode (gt I I)
+         #:contract (gt n n)
          [(gt n_1 n_2)
           (where n_3 (pred n_1))
           (le n_2 n_3)])
@@ -1167,13 +1167,13 @@ non-termination. For example, consider the following definitions:
        (define-language vertices
          (v a b c))
        (define-judgment-form vertices
-         mode : I O
-         edge ⊆ v × v
+         #:mode (edge I O)
+         #:contract (edge v v)
          [(edge a b)]
          [(edge b c)])
        (define-judgment-form vertices
-         mode : I I
-         path ⊆ v × v
+         #:mode (path I I)
+         #:contract (path v v)
          [(path v v)]
          [(path v_1 v_2)
           (path v_2 v_1)]
@@ -1193,10 +1193,23 @@ form, produces a list of terms by instantiating the supplied term template with
 each satisfying assignment of pattern variables. 
 See @racket[define-judgment-form] for examples.
 }                                     
-                                     
-@defform[(define-relation language
-          relation-contract
-          [(name @#,ttpattern ...) @#,tttterm ...] ...)]{
+
+@defidform[I]{
+Recognized specially within @racket[define-judgment-form], the @racket[I] keyword
+is an error elsewhere.
+} 
+@defidform[O]{
+Recognized specially within @racket[define-judgment-form], the @racket[O] keyword
+is an error elsewhere.
+}
+
+@defform/subs[#:literals (⊂ ⊆ × x)
+              (define-relation language
+                relation-contract
+                [(name @#,ttpattern ...) @#,tttterm ...] ...)
+              ([relation-contract (code:line)
+                                  (code:line form-id ⊂ @#,ttpattern x ... x @#,ttpattern)
+                                  (code:line form-id ⊆ @#,ttpattern × ... × @#,ttpattern)])]{
 Similar to @racket[define-judgment-form] but suitable only when every position
 is an input. There is no associated form corresponding to 
 @racket[judgment-holds]; querying the result uses the same syntax as 

collects/redex/reduction-semantics.rkt

@@ -13,6 +13,7 @@
          --> fresh with ;; keywords for reduction-relation
          hole in-hole ;; keywords for term
          ::= ;; keywords for language definition
+         I O ;; keyword for define-judgment-form
          extend-reduction-relation
          reduction-relation?
          

collects/redex/tests/bitmap-test.rkt

@@ -81,7 +81,7 @@
 
 (let ()
   (define-judgment-form lang
-    mode : I O
+    #:mode (id I O)
     [(id e e)])
   (test (render-reduction-relation
          (reduction-relation
@@ -276,7 +276,7 @@
     (n z (s n)))
   
   (define-judgment-form nats
-    mode : I I O
+    #:mode (sum I I O)
     [(sum z n n)]
     [(sum (s n_1) n_2 (s n_3))
      (sum n_1 n_2 n_3)])
@@ -290,7 +290,7 @@
         "judgment-form-rewritten.png")
   
   (define-judgment-form nats
-    mode : I O
+    #:mode (mfw I O)
     [(mfw n_1 n_2)
      (where n_2 (f n_1))])
   
@@ -300,7 +300,7 @@
   (test (render-judgment-form mfw) "judgment-form-metafunction-where.png")
   
   (define-judgment-form nats
-    mode : I O
+    #:mode (nps I O)
     [(nps (name a (s n_1)) n_2)
      (nps z (name n_1 (s (s n_1))))
      (where (name b n_2) z)])
@@ -318,8 +318,8 @@
     (Γ ([x τ] ...)))
   
   (define-judgment-form STLC
-    mode : I I O
-    typeof ⊆ Γ × e × τ
+    #:mode (typeof I I O)
+    #:contract (typeof Γ e τ)
     [(typeof Γ (e_1 e_2) τ)
      (typeof Γ e_1 (τ_2 → τ))
      (typeof Γ e_2 τ_2)]

collects/redex/tests/run-err-tests/judgment-form-undefined.rktd

@@ -4,6 +4,6 @@
    (judgment-holds (use 1))
    (define-language L)
    (define-judgment-form L 
-     mode : I
+     #:mode (def I)
      [(def 1)])
    #f))

collects/redex/tests/syn-err-tests/judgment-form-definition.rktd

@@ -1,40 +1,75 @@
-(#rx"expected a mode"
- ([bad-def (define-judgment-form syn-err-lang)])
+(#rx"expected an identifier defined by define-language"
+ ([not-lang q])
+ (define-judgment-form not-lang))
+
+(#rx"expected.*I.*or.*O"
+ ([bad-mode q])
+ (define-judgment-form syn-err-lang
+   #:mode (sum I bad-mode O)))
+
+(#rx"expected mode specification"
+ ([bad-spec q])
+ (define-judgment-form syn-err-lang
+   #:mode bad-spec))
+
+(#rx"expected contract specification"
+ ([bad-spec q])
+ (define-judgment-form syn-err-lang
+   #:mode (sum I I O)
+   #:contract bad-spec))
+
+(#rx"expected definition to include a mode specification"
+ ([bad-def (define-judgment-form syn-err-lang
+             #:contract (J)
+             [(J)])])
  bad-def)
-(#rx"expected a mode"
- ([mode-kw mode])
- (define-judgment-form syn-err-lang mode-kw))
-(#rx"expected a clause"
- ([junk 1])
+
+(#rx"expected at most one contract specification"
+ ([dup-spec (J)])
  (define-judgment-form syn-err-lang
-   mode : junk
-   [(q 1)]))
-(#rx"expected at least one clause"
- ([bad-def (define-judgment-form syn-err-lang mode :)])
+  #:mode (J)
+  #:contract (J)
+  #:contract dup-spec))
+
+(#rx"expected at most one contract specification"
+ ([dup-spec1 (J)] [dup-spec2 (J)])
+ (define-judgment-form syn-err-lang
+   #:contract (J)
+   #:mode (J)
+   #:contract dup-spec1
+   #:contract dup-spec2))
+
+(#rx"expected the same name"
+ ([name1 J] [name2 K]) ([name3 J])
+ (define-judgment-form syn-err-lang
+   #:mode (name1)
+   #:contract (name2)
+   [(name3)]))
+
+(#rx"expected the same name"
+ ([name1 J] [name2 K]) ([name3 J])
+ (define-judgment-form syn-err-lang
+   #:mode (name1)
+   #:contract (name3)
+   [(name2)]))
+
+(#rx"expected at least one rule"
+ ([bad-def (define-judgment-form syn-err-lang
+             #:mode (J I)
+             #:contract (J n))])
  bad-def)
-(#rx"expected a pattern to follow"
- ([cross ×])
- (define-judgment-form syn-err-lang
-   mode : I
-   J ⊆ number cross))
-(#rx"use the same name"
- ([name1 J] [name2 K])
- (define-judgment-form syn-err-lang
-   mode : I
-   name1 ⊆ number
-   [(name2 number)]))
 (#rx"malformed premise"
  ([bad-prem (q)])
  (let ()
    (define-judgment-form syn-err-lang
-     mode : I
+     #:mode (J I)
      [(J number)
       bad-prem])
    (void)))
 (#rx"different numbers of positions"
  ([bad-def (define-judgment-form syn-err-lang
-             mode : I
-             J ⊆ number × number
+             #:mode (J I)
+             #:contract (J n n)
              [(J number)])])
  bad-def)
 
@@ -42,7 +77,7 @@
  ([unbound number_2])
  (let ()
    (define-judgment-form syn-err-lang
-     mode : I O
+     #:mode (J I O)
      [(J number_1 unbound)
       (J number_1 number_1)])
    (void)))
@@ -50,7 +85,7 @@
  ([unbound number_2])
  (let ()
    (define-judgment-form syn-err-lang
-     mode : I O
+     #:mode (J I O)
      [(J number_1 number_2)
       (J unbound number_1)])
    (void)))
@@ -58,7 +93,7 @@
  ([unbound number_3])
  (let ()
    (define-judgment-form syn-err-lang
-     mode : I O
+     #:mode (J I O)
      [(J number_1 number_2)
       (where number_2 unbound)])
    (void)))
@@ -66,23 +101,23 @@
  ([unbound q])
  (let ()
    (define-judgment-form syn-err-lang
-     mode : I O
+     #:mode (J I O)
      [(J number_1 number_2)
       (where number_2 unbound)
       (where (name q number) number_1)])
    (void)))
 (#rx"arity"
- ([bad-conc (J)])
+ ([bad-conc (J)]) ([name J])
  (let ()
    (define-judgment-form syn-err-lang
-     mode : I
+     #:mode (name I)
      [bad-conc])
    (void)))
 (#rx"arity"
  ([bad-prem (J)]) ([name J])
  (let ()
    (define-judgment-form syn-err-lang
-     mode : I
+     #:mode (name I)
      [(name number)
       bad-prem])
    (void)))
@@ -90,7 +125,7 @@
  ([unq ,(+ 1)])
  (let ()
    (define-judgment-form syn-err-lang
-     mode : I
+     #:mode (uses-unquote I)
      [(uses-unquote n)
       (where n unq)])
    (void)))
@@ -98,6 +133,6 @@
  ([unq ,'z])
  (let ()
    (define-judgment-form syn-err-lang
-     mode : I O
+     #:mode (uses-unquote I O)
      [(uses-unquote n unq)])
    (void)))

collects/redex/tests/tl-test.rkt

@@ -1808,7 +1808,7 @@
     
     (let ()
       (define-judgment-form empty-language
-        mode : I O
+        #:mode (R I O)
         [(R a a)]
         [(R a b)])
       (test (apply-reduction-relation
@@ -1893,8 +1893,8 @@
         (n z (s n)))
       
       (define-judgment-form nats
-        mode : I I O
-        sumi ⊆ n × n × n
+        #:mode (sumi I I O)
+        #:contract (sumi n n n)
         [(sumi z n n)]
         [(sumi (s n_1) n_2 (s n_3))
          (sumi n_1 n_2 n_3)])
@@ -1905,8 +1905,8 @@
       (test (judgment-holds (sumi ,'z (s z) (s z))) #t)
       
       (define-judgment-form nats
-        mode : O O I
-        sumo ⊆ n × n × n
+        #:mode (sumo O O I)
+        #:contract (sumo n n n)
         [(sumo z n n)]
         [(sumo (s n_1) n_2 (s n_3))
          (sumo n_1 n_2 n_3)])
@@ -1917,7 +1917,7 @@
                   (term ([n_1 z] [n_2 (s z)]))))
       
       (define-judgment-form nats
-        mode : O O I
+        #:mode (sumo-ls O O I)
         [(sumo-ls (s n_1) n_2 n_3)
          (sumo (s n_1) n_2 n_3)])
       (test (judgment-holds (sumo-ls n_1 n_2 (s z)) ([,'n_1 n_1] [,'n_2 n_2]))
@@ -1927,33 +1927,33 @@
       (test (judgment-holds (sumo-ls z n_2 (s z)) whatever) (list))
       
       (define-judgment-form nats
-        mode : O O I
+        #:mode (sumo-lz O O I)
         [(sumo-lz z n_2 n_3)
          (sumo z n_2 n_3)])
       (test (judgment-holds (sumo-lz n_1 n_2 (s z)) ([,'n_1 n_1] [,'n_2 n_2]))
             (list (term ([n_1 z] [n_2 (s z)]))))
       
       (define-judgment-form nats
-        mode : O I
+        #:mode (member O I)
         [(member n_i (n_0 ... n_i n_i+1 ...))])
       
       (test (judgment-holds (member n (z (s z) z (s (s z)))) n)
             (list (term (s (s z))) (term z) (term (s z)) (term z)))
       
       (define-judgment-form nats
-        mode : I
+        #:mode (has-zero I)
         [(has-zero (n ...))
          (member z (n ...))])
       
       (test (judgment-holds (has-zero ((s z) z (s (s z))))) #t)
       
       (define-judgment-form nats
-        mode : I
+        #:mode (le2 I)
         [(le2 n)
          (le (add2 n) (s (s (s (s z)))))])
       
       (define-judgment-form nats
-        mode : I I
+        #:mode (le I I)
         [(le z n)]
         [(le (s n_1) (s n_2))
          (le n_1 n_2)])
@@ -1966,8 +1966,8 @@
       (test (judgment-holds (le2 (s (s (s z))))) #f)
       
       (define-judgment-form nats
-        mode : I O
-        uses-add2 ⊆ n × n
+        #:mode (uses-add2 I O)
+        #:contract (uses-add2 n n)
         [(uses-add2 n_1 n_2)
          (sumo n_2 n_3 n_1)
          (where n_2 (add2 n_3))])
@@ -2006,7 +2006,7 @@
                                   ['z #t]
                                   [`(s ,n) (f n)])])
                       (define-judgment-form nats
-                        mode : I I
+                        #:mode (ext-trace I I)
                         [(ext-trace z (side-condition n (f (term n))))]
                         [(ext-trace (s n_1) n_2)
                          (ext-trace n_1 n_2)])
@@ -2029,7 +2029,7 @@
       (eval '(require redex/reduction-semantics))
       (eval '(define-language L))
       (eval '(define-judgment-form L
-               mode : I
+               #:mode (J I)
                [(J a)
                 (J b)]
                [(J b)]))
@@ -2040,8 +2040,8 @@
       (eval '(define-language L
                (s a b c)))
       (eval '(define-judgment-form L
-               mode : I O
-               ctc-fail ⊆ s × s
+               #:mode (ctc-fail I O)
+               #:contract (ctc-fail s s)
                [(ctc-fail a q)]
                [(ctc-fail b s)
                 (ctc-fail q s)]