fix test-->, test-->>, and test-->>∃ so they accept IO judgment forms.

closes #162

Author: rfindler

redex-doc/redex/scribblings/ref/testing.scrbl

@@ -58,7 +58,7 @@ the comparison. It defaults to @racket[(default-equiv)].
               ([option (code:line #:cycles-ok)
                        (code:line #:equiv pred-expr)
                        (code:line #:pred pred-expr)])
-              #:contracts ([rel-expr reduction-relation?]
+              #:contracts ([rel-expr (or/c reduction-relation? IO-judgment-form?)]
                            [pred-expr (-> any/c any)]
                            [e1-expr any/c]
                            [e2-expr any/c])]{
@@ -91,7 +91,7 @@ isn't supplied, then @racket[(default-equiv)] is used.
 
 @defform/subs[(test--> rel-expr option ... e1-expr e2-expr ...)
               ([option (code:line #:equiv pred-expr)])
-              #:contracts ([rel-expr reduction-relation?]
+              #:contracts ([rel-expr (or/c reduction-relation? IO-judgment-form?)]
                            [pred-expr (-> any/c any/c any/c)]
                            [e1-expr any/c]
                            [e2-expr any/c])]{
@@ -124,7 +124,7 @@ step, using @racket[pred-expr] to determine equivalence (or
 
 @defform/subs[(test-->>∃ option ... rel-expr start-expr goal-expr)
               ([option (code:line #:steps steps-expr)])
-              #:contracts ([rel-expr reduction-relation?]
+              #:contracts ([rel-expr (or/c reduction-relation? IO-judgment-form?)]
                            [start-expr any/c]
                            [goal-expr (or/c (-> any/c any/c)
                                             (not/c procedure?))]

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

@@ -2944,15 +2944,16 @@
   (values (apply-reduction-relation red arg) #f))
 
 (define (test-->>/procs name red arg-thnk expected-thnk apply-red cycles-ok? equiv? pred srcinfo)
-  (unless (reduction-relation? red)
-    (error name "expected a reduction relation as first argument, got ~e" red))
+  (unless (or (reduction-relation? red)
+              (IO-judgment-form? red))
+    (error name "expected a reduction relation or an IO-judgment-form as first argument, got ~e" red))
   (when pred
     (unless (and (procedure? pred)
                  (procedure-arity-includes? pred 1))
       (error 'test-->> "expected a procedure that accepted one argument for the #:pred, got ~e"
              pred)))
   (define-values (arg expected)
-    (parameterize ([default-language (reduction-relation-lang red)])
+    (parameterize ([default-language (reduction-relation/IO-jf-lang red)])
       (values (arg-thnk) (expected-thnk))))
   (define test-failed? #f)
   (define (fail) (inc-failures) (set! test-failed? #t))
@@ -2999,7 +3000,7 @@
            relation
            start:expr
            goal)
-     #:declare relation (expr/c #'reduction-relation? 
+     #:declare relation (expr/c #'(or/c reduction-relation? IO-judgment-form?)
                                 #:name "reduction relation expression")
      #:declare goal (expr/c #'(or/c (-> any/c any/c) (not/c procedure?)) 
                             #:name "goal expression")

redex-test/redex/tests/tl-test.rkt

@@ -29,6 +29,13 @@
   (test (capture-output (test-->> red 2 3) (test-results))
         #rx"FAILED .*tl-test.(?:.+):[0-9.]+\nexpected: 3\n  actual: 2\n1 test failed \\(out of 1 total\\).\n"))
 
+(let ()
+  (define-judgment-form empty-language #:mode (J I O) [(J 1 2)])
+  (test (capture-output (test-->> J 1 2) (test-results))
+        "One test passed.\n")
+  (test (capture-output (test-->> J 2 3) (test-results))
+        #rx"FAILED .*tl-test.(?:.+):[0-9.]+\nexpected: 3\n  actual: 2\n1 test failed \\(out of 1 total\\).\n"))
+
 (let ()
   (define red-share (reduction-relation 
                      empty-language
@@ -208,6 +215,11 @@
   (test (capture-output (test--> red (term (1 2 3)) (term ((1 2 3)))) (test-results))
         "One test passed.\n"))
 
+(let ()
+  (define-judgment-form empty-language #:mode (J I O) [(J any (any))])
+  (test (capture-output (test--> J (term (1 2 3)) (term ((1 2 3)))) (test-results))
+        "One test passed.\n"))
+
 (let ()
   (define red (reduction-relation empty-language 
                                   (--> any (any))
@@ -274,7 +286,16 @@
   (test (capture-output (test-->>E 1+ 0 7)) "")
   (test (capture-output (test-->>∃ #:steps +inf.0 1+ 0 7)) "")
   (test (capture-output (test-->>∃ 1+ 0 equal-to-7)) "")
+
+  (define-judgment-form L
+    #:mode (1+/J I O)
+    [(1+/J number ,(add1 (term number)))])
 
+  (test (capture-output (test-->>∃ 1+/J 0 7)) "")
+  (test (capture-output (test-->>E 1+/J 0 7)) "")
+  (test (capture-output (test-->>∃ #:steps +inf.0 1+/J 0 7)) "")
+  (test (capture-output (test-->>∃ 1+/J 0 equal-to-7)) "")
+
   (define identity
     (reduction-relation
      L
@@ -283,7 +304,7 @@
   (test (capture-output (test-->>∃ identity 0 1))
         #rx"^FAILED .*\nterm 1 not reachable from 0\n$")
 
-  (test (capture-output (test-results)) "2 tests failed (out of 6 total).\n")
+  (test (capture-output (test-results)) "2 tests failed (out of 10 total).\n")
 
   (test-contract-violation
    (test-->>∃ 1+ 0 (λ (x y) x))