They do not currently --- all the tests are expanding into simple rackunit
forms such as 'check-equal?', 'check-false', 'check-true', etc with redex's
'term' wrapped around the original syntax.
However, you could mimic `default-equiv` by defining a redex
metafunction/relation/judgment that captures the notion of equivalence you
want.
For example, you could test for some language-specific notion of `α=`
instead of Racket's `equal?` like this:
(redex-relation-chk
α=
[(subst (λ (x) (f x)) [g / f])
(λ (y) (g y))]
...)
On Thu, Nov 5, 2015 at 10:42 PM William J. Bowman <[email protected]>
wrote:
> Thanks, I've been meaning to do something about this for months!
>
> Do they make use of `default-equiv`?
>
> --
> William J. Bowman
>
> On Wed, Nov 04, 2015 at 05:50:01AM -0800, Andrew Kent wrote:
> > Dear other PLT Redex users,
> >
> > Do you have any clever tricks/tools to make testing in PLT Redex
> > more palletable? I was finding some of my tests had a lot more
> > boiler-plate text than actual test-relevant code. I would love to
> > hear your thoughts/experiences on this issue... and share
> > something I threw together that I've found helpful:
> >
> > I basically hijacked and rewrote Jay's lovely rackunit/chk
> > pkg (thanks Jay!) to cater to redex tests. It's now the
> > 'redex-chk' pkg (on http://pkgs.racket-lang.org/).
> >
> > It allows verbose tests like these:
> >
> > (module+ test
> > ;; restrict tests
> > (test-equal (term (restrict mt-Γ Any Int)) (term Int))
> > (test-equal (term (restrict mt-Γ Int Any)) (term Int))
> > (test-equal (term (restrict mt-Γ Int Bool)) (term (U)))
> > (test-equal (term (restrict mt-Γ (U Bool Int) Int)) (term Int))
> >
> > ;; subtyping tests
> > (test-equal (judgment-holds (subtype mt-Γ Int Int)) #t)
> > (test-equal (judgment-holds (subtype mt-Γ Int Any)) #t)
> > (test-equal (judgment-holds (subtype mt-Γ Any Int)) #f))
> >
> > to be written like this:
> >
> > (module+ test
> > ;; restrict tests
> > (redex-chk
> > (restrict mt-Γ Any Int) Int
> > (restrict mt-Γ Int Any) Int
> > #:= (restrict mt-Γ Int Bool) (U)
> > [(restrict mt-Γ (U Bool Int) Int) Int])
> >
> > ;; subtyping tests
> > (redex-relation-chk
> > subtype
> > [mt-Γ Int Int]
> > [mt-Γ Int Any]
> > [#:f mt-Γ Any Int]))
> >
> > (Note -- each of the restrict tests is checking for 'equal?',
> > there's just several equivalent ways to write that,
> > like in Jay's rackunit/chk lib)
> >
> > Anyway - throwing this together was a fun macro-learning experience for
> > me and I think has helped me write more and better tests for my
> > redex model (now that it's easier). I figured it might be useful for
> > others, and wondered if anyone else had done anything in the same
> > department.
> >
> > Best,
> > Andrew
> >
> > --
> > You received this message because you are subscribed to the Google
> Groups "Racket Users" group.
> > To unsubscribe from this group and stop receiving emails from it, send
> an email to [email protected].
> > For more options, visit https://groups.google.com/d/optout.
>
>
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
For more options, visit https://groups.google.com/d/optout.
