From 94a146c942934932fbc0fda3a396781a51e28c84 Mon Sep 17 00:00:00 2001
From: Spencer Florence <spencer@florence.io>
Date: Tue, 1 Oct 2019 12:07:00 -0500
Subject: [PATCH 1/2] add redex-rackunit-adapter-lib

---
 redex-rackunit-adapter-lib/info.rkt           |   9 ++
 .../redex/rackunit-adapter.rkt                | 149 ++++++++++++++++++
 2 files changed, 158 insertions(+)
 create mode 100644 redex-rackunit-adapter-lib/info.rkt
 create mode 100644 redex-rackunit-adapter-lib/redex/rackunit-adapter.rkt

diff --git a/redex-rackunit-adapter-lib/info.rkt b/redex-rackunit-adapter-lib/info.rkt
new file mode 100644
index 00000000..71fa3642
--- /dev/null
+++ b/redex-rackunit-adapter-lib/info.rkt
@@ -0,0 +1,9 @@
+#lang setup/infotab
+
+(define collection 'multi)
+
+(define deps '("redex-lib" "rackunit"))
+
+(define pkg-desc "PLT Redex libraries for practical semantics engineering")
+
+(define pkg-authors '(florence))
diff --git a/redex-rackunit-adapter-lib/redex/rackunit-adapter.rkt b/redex-rackunit-adapter-lib/redex/rackunit-adapter.rkt
new file mode 100644
index 00000000..e57b8ff4
--- /dev/null
+++ b/redex-rackunit-adapter-lib/redex/rackunit-adapter.rkt
@@ -0,0 +1,149 @@
+#lang racket
+(provide
+ (rename-out
+  [in:test-->* test-->]
+  [in:test-->>* test-->>]
+  [in:test-judgment-holds test-judgment-holds]
+  [in:test-equal test-equal])
+ test-judgment-does-not-hold
+ test-->>∃
+ test--/>
+ test--?>
+ test-->>P
+ test-->>P*)
+(require redex/reduction-semantics
+         rackunit
+         (for-syntax syntax/parse)
+         syntax/parse/define
+         (for-syntax rackunit-abbrevs/error-reporting))
+
+(define-syntax in:test-->*
+  (syntax-parser
+    [(_ R term results ...)
+     (syntax/loc this-syntax
+       (test--> R term (list results ...)))]))
+
+(define-syntax in:test-->>*
+  (syntax-parser
+    [(_ R term results ...)
+     (syntax/loc this-syntax
+       (test-->> R term (list results ...)))]))
+
+(define-check (test--> R term expected)
+  (define res (apply-reduction-relation R term))
+  (unless (equal? (list->set res)
+                  (list->set expected))
+    (with-check-info
+     (['results res]
+      ['expected expected])
+     (fail-check "Did not match reductions in one step"))))
+
+(define-check (test-->> R term results ...)
+  (define res (apply-reduction-relation* R term))
+  (define expected (list results ...))
+  (unless (equal? (list->set res)
+                  (list->set expected))
+    (with-check-info
+     (['results res]
+      ['expected expected])
+     (fail-check "Did not match reductions in many"))))
+
+(define-check (test-->>∃ R term expected)
+  (define res (apply-reduction-relation* R term #:all? #t))
+  (unless (memf (curry (default-equiv) expected) res)
+    (with-check-info
+     (['results res]
+      ['expected expected])
+     (fail-check "could not find term not match reductions in many steps"))))
+
+(define-check (test--/> R term)
+  (define res (apply-reduction-relation R term))
+  (unless (empty? res)
+    (with-check-info
+     (['results res])
+     (fail-check "could not find term not match reductions in many steps"))))
+
+(define-check (test--?> R term t)
+  (define res (apply-reduction-relation R term))
+  (if t
+      (when (empty? res)
+        (fail-check "had no reductions when it should have"))
+      (unless (empty? res)
+        (with-check-info
+         (['results res])
+         (fail-check "could not find term not match reductions in many steps")))))
+
+(define-check (test-->>P R term P)
+  (define res (apply-reduction-relation* R term))
+  (define failed
+    (for/list ([r (in-list res)]
+               #:unless (P r))
+      r))
+  (unless (empty? failed)
+    (with-check-info
+     (['all-results res]
+      ['failed failed])
+     (fail-check "Some terminal reductions failed property"))))
+
+(define-check (test-->>P* R term P)
+  (define res (apply-reduction-relation* R term))
+  (define failed (P res))
+  (unless failed
+    (with-check-info
+     (['all-results res])
+     (fail-check "Some terminal reductions failed property"))))
+
+(define-syntax in:test-equal
+  (syntax-parser
+    [(test-equal a b)
+     (syntax/loc this-syntax
+       (test-equal a b #:equiv (default-equiv)))]
+    [(test-equal a b #:equiv eq)
+     #`(with-default-check-info*
+        (list (make-check-name 'test-equial)
+              (make-check-location '#,(syntax->location this-syntax))
+              (make-check-expression
+               '(test-equal a b #:equiv eq)))
+        (lambda ()
+          ((current-check-around)
+           (lambda ()
+             (define a* a)
+             (define b* b)
+             (unless (eq a* b*)
+               (with-check-info
+                (['expected a*]
+                 ['actual b*])
+                (fail-check)))))))]))
+
+(define-syntax test-judgment-does-not-hold
+  (syntax-parser
+    [(test-judgment-does-not-hold (judgment body ...))
+     #`(with-default-check-info*
+        (list (make-check-name 'test-judgment-does-not-hold)
+              (make-check-location '#,(syntax->location this-syntax))
+              (make-check-expression
+               '(test-judgment-doesnt-hold (judgment body ...))))
+        (lambda ()
+          ((current-check-around)
+           (lambda ()
+             (define r (judgment-holds (judgment body ...) (body ...)))
+             (with-check-info
+              (['|held at| (map (lambda (x) (cons 'judgment x)) r)])
+              (unless (empty? r)
+                (fail-check "judgment, in fact, held")))))))]))
+
+(define-syntax in:test-judgment-holds
+  (syntax-parser
+    [(test-judgment-doesnt-hold (judgment body ...))
+     #`(with-default-check-info*
+        (list (make-check-name 'test-judgment-doesnt-hold)
+              (make-check-location '#,(syntax->location this-syntax))
+              (make-check-expression
+               '(test-judgment-doesnt-hold (judgment body ...))))
+        (lambda ()
+          ((current-check-around)
+           (lambda ()
+             (define r (judgment-holds (judgment body ...)))
+             (when (not r)
+               (fail-check "judgment didn't hold"))))))]))
+

From e83b948308a3fd12b0f5edccc16da7887306625f Mon Sep 17 00:00:00 2001
From: Spencer Florence <spencer@florence.io>
Date: Tue, 1 Oct 2019 12:44:38 -0500
Subject: [PATCH 2/2] fix some typos

---
 .../redex/rackunit-adapter.rkt                | 21 +++++--------------
 1 file changed, 5 insertions(+), 16 deletions(-)

diff --git a/redex-rackunit-adapter-lib/redex/rackunit-adapter.rkt b/redex-rackunit-adapter-lib/redex/rackunit-adapter.rkt
index e57b8ff4..07039a46 100644
--- a/redex-rackunit-adapter-lib/redex/rackunit-adapter.rkt
+++ b/redex-rackunit-adapter-lib/redex/rackunit-adapter.rkt
@@ -8,7 +8,6 @@
  test-judgment-does-not-hold
  test-->>∃
  test--/>
- test--?>
  test-->>P
  test-->>P*)
 (require redex/reduction-semantics
@@ -54,24 +53,14 @@
     (with-check-info
      (['results res]
       ['expected expected])
-     (fail-check "could not find term not match reductions in many steps"))))
+     (fail-check "expected term was not reachable"))))
 
 (define-check (test--/> R term)
   (define res (apply-reduction-relation R term))
   (unless (empty? res)
     (with-check-info
      (['results res])
-     (fail-check "could not find term not match reductions in many steps"))))
-
-(define-check (test--?> R term t)
-  (define res (apply-reduction-relation R term))
-  (if t
-      (when (empty? res)
-        (fail-check "had no reductions when it should have"))
-      (unless (empty? res)
-        (with-check-info
-         (['results res])
-         (fail-check "could not find term not match reductions in many steps")))))
+     (fail-check "term reduced"))))
 
 (define-check (test-->>P R term P)
   (define res (apply-reduction-relation* R term))
@@ -91,7 +80,7 @@
   (unless failed
     (with-check-info
      (['all-results res])
-     (fail-check "Some terminal reductions failed property"))))
+     (fail-check "reductions failed property"))))
 
 (define-syntax in:test-equal
   (syntax-parser
@@ -100,7 +89,7 @@
        (test-equal a b #:equiv (default-equiv)))]
     [(test-equal a b #:equiv eq)
      #`(with-default-check-info*
-        (list (make-check-name 'test-equial)
+        (list (make-check-name 'test-equal)
               (make-check-location '#,(syntax->location this-syntax))
               (make-check-expression
                '(test-equal a b #:equiv eq)))
@@ -130,7 +119,7 @@
              (with-check-info
               (['|held at| (map (lambda (x) (cons 'judgment x)) r)])
               (unless (empty? r)
-                (fail-check "judgment, in fact, held")))))))]))
+                (fail-check)))))))]))
 
 (define-syntax in:test-judgment-holds
   (syntax-parser