Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] add redex-rackunit-adapter-lib #199

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

florence
Copy link
Contributor

@florence florence commented Oct 1, 2019

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
Copy link
Collaborator

wilbowma commented Oct 1, 2019

You're a beautiful person for this.

@florence
Copy link
Contributor Author

florence commented Oct 1, 2019

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
Copy link
Collaborator

wilbowma commented Oct 1, 2019

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
Copy link
Member

rfindler commented Oct 5, 2019

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants