[WIP] add redex-rackunit-adapter-lib

[florence]

This PR adds a new redex library that integrates better with rackunit. It's still very much a WIPthe purpose of this PR 1) get feedback on other ways to integration rackunit, 2) to decide if any of the features here should be moved into redex proper, 3) to decide if this should be added here or as a stand alone package.

The changes this makes are as follows

All test-* forms have been updated to:

1. integrate with the control-flow properties of test-begin, test-case, and test-suite.
2. invoke the (error-display-handler) to get a clickable button that will jump to the failed test (this is called indirectly via rackunit).
3. Test failures use rackunit style prints. For example:

> (redex:test-equal 1 2 #:equiv equal?)
FAILED :5.2
  actual: 1
expected: 2
> (racknit:test-equal 1 2 #:equiv equal?)
--------------------
. FAILURE
name:       test-equal
location:   interactions from an unsaved editor:9:2
expected:   1
actual:     2
--------------------

and

> (define-language L)
> (define-judgment-form L
    #:mode (nat? I)
    [--------
     (nat? natural)])
> (redex:test-judgment-holds (nat? "a"))
FAILED :24.2
  judgment of nat? does not hold
> (rackunit:test-judgment-holds (nat? "a"))
--------------------
. FAILURE
name:       rackunit:test-judgment-holds
location:   interactions from an unsaved editor:27:2

judgment didn't hold
--------------------

In addition the following test forms are added:

• test-judgment-does-not-hold : tests that a judgment does not hold
• test--/> : tests that a term does not reduce
• test-->>P : a combination of test-->> and test-predicate, which tests if all reachable terms hold for some property P
• test-->>P*: like test-->>P, but the predicate is give the list of all terms

Examples of test failures for new forms: test-judgment-does-not-hold

> (define-judgment-form L
    #:mode (buggy-rest I O)
    [----
     (buggy-rest () nil)]
    [----
     (buggy-rest (any any_1 ...) (any_1 ...))])
> (test-judgment-does-not-hold (buggy-rest () any))
--------------------
. FAILURE
name:       test-judgment-does-not-hold
location:   interactions from an unsaved editor:22:2
held at:    ((buggy-rest () nil))
--------------------

test--/>

> (define R (reduction-relation L (--> any any)))
> (test--/> R 1)
--------------------
. FAILURE
name:       test--/>
location:   interactions from an unsaved editor:5:2
params:     '(#<reduction-relation> 1)
results:    (1)

term reduced
--------------------

test-->>P

> (define R1 (reduction-relation L (--> natural ,(~a (term natural)))))
> (test-->>P R1 1 natural?)
--------------------
. FAILURE
name:         test-->>P
location:     interactions from an unsaved editor:16:2
params:       '(#<reduction-relation> 1 #<procedure:natural?>)
all-results:  ("1")
failed:       ("1")

Some terminal reductions failed property
--------------------

test-->>P*

> (define R2
    (reduction-relation
     L
     (--> natural natural)))
> (test-->>P*
   R2 1
   (lambda (x) (= (length x) 1)))
--------------------
. FAILURE
name:         test-->>P*
location:     interactions from an unsaved editor:78:2
params:       '(#<reduction-relation> 1 #<procedure>)
all-results:  ()

Some terminal reductions failed property
--------------------

A TODO list:

[ ] Write docs [ ] write tests [ ] use internal test-judgment-holds that redex uses to improve error messages [ ] extend test-judgment-holds to have the same interface as redex proper [ ] extend test-judgment-does-not-hold to have the same interface as redex proper [ ] extend test--> to have the same interface as redex proper [ ] extend test-->> to have the same interface as redex proper [ ] extend test-->>∃ to have the same interface as redex proper [ ] add test-->>E [ ] add test-predicate [ ] add redex-check [ ] change test-equal to no show the #:equiv when non is provided [ ] add test-->P and test-->P* [ ] update error message to instead of giving stuff like (#<reduction-relation> 1 #<procedure:natural?>), to give (R1 1 natural?)

[wilbowma]

You're a beautiful person for this.

[florence]

From a prior discussion with robby, it sounds like we would at least like to move the invoking of the error-display-handler and test-judgment-does-not-hold over to redex proper. I would guess test--/> and test-->>P should be moved to. (the usefulness of test-->>P* is more up in the air to me: I've basically only used it for the test example test I gave, which basically says "the reduction is acyclic, terminating, and confluent". @wilbowma, @rfindler does test-->>P* sound useful to you?).

Moving the integration of the control-flow properties of test-begin and friends would be nice, but I don't see currently how to do that without also copying the error message style of rackunit, which IIUC @rfindler was iffy about.

[wilbowma]

Since Redex already ships with testing stuff, it makes sense to me that all of this eventually ends up in Redex. (Ideally replacing anything that doesn't integrated with rackunit.)

test-->>P* looks useful to me; most of my calls to reduction relations are through apply-reduction-relation*.

[rfindler]

Yeah, I don't find the printing style of rackunit very beautiful. If that's really important, lets put it into a different library; I definitely don't want to replace the redex-style printing with the stuff with the hyphens.

I do think that the larger zoo of test- forms is an improvement; I agree that test->P* is somewhat iffy. But if it would be useful in someone's real model, lets add it.