diff --git a/pkgs/redex-pkgs/redex-pict-lib/redex/pict.rkt b/pkgs/redex-pkgs/redex-pict-lib/redex/pict.rkt index 35959827a7..548b1ee99c 100644 --- a/pkgs/redex-pkgs/redex-pict-lib/redex/pict.rkt +++ b/pkgs/redex-pkgs/redex-pict-lib/redex/pict.rkt @@ -89,7 +89,7 @@ (parameter/c reduction-rule-style/c)] [arrow-space (parameter/c natural-number/c)] [label-space (parameter/c natural-number/c)] - [metafunction-cases (parameter/c (or/c #f (and/c pair? (listof (or/c exact-nonnegative-integer? string?)))))] + [metafunction-cases (parameter/c (or/c #f (listof (or/c exact-nonnegative-integer? string?))))] [judgment-form-cases (parameter/c (or/c #f (and/c (listof (or/c exact-nonnegative-integer? string?)) pair?)))] [metafunction-pict-style diff --git a/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt b/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt index 6df8cee038..37db7e6bbf 100644 --- a/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt +++ b/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt @@ -6,10 +6,9 @@ racket/pretty racket/set (only-in racket/list drop-right last partition add-between - splitf-at) + splitf-at remove-duplicates) - texpict/mrpict - texpict/utils + pict redex/private/reduction-semantics redex/private/judgment-form @@ -875,7 +874,7 @@ (cond [mf-cases (define i 0) - (define sorted-cases (remove-dups (sort (filter number? mf-cases) <))) + (define sorted-cases (remove-duplicates (sort (filter number? mf-cases) <))) (define named-cases (apply set (filter string? mf-cases))) (apply append @@ -930,17 +929,6 @@ [else (values eqns conclusions eqn-names)])) -;; remove-dups : (listof number)[sorted] -> (listof number)[sorted] -;; removes duplicate numbers from 'l' -(define (remove-dups l) - (let loop ([l l]) - (cond - [(null? (cdr l)) l] - [(= (car l) (cadr l)) - (loop (cdr l))] - [else - (cons (car l) (loop (cdr l)))]))) - (define (metafunctions->pict/proc mfs contract? name) (unless (andmap (λ (mf) (equal? (metafunc-proc-lang (metafunction-proc (car mfs))) (metafunc-proc-lang (metafunction-proc mf)))) @@ -1147,6 +1135,7 @@ ;; two columns of non-spanning rows. (define max-w-before-rhs (apply max + 0 (map (lambda (row) (match row [(list lhs 'fill 'fill) @@ -1173,38 +1162,41 @@ 0))] [else row])) rows))) - (table 3 - (adjust-for-fills - (apply append - (for/list ([lhs/contract (in-list lhs/contracts)] - [sc (in-list scs)] - [rhs (in-list rhss)] - [linebreak? (in-list linebreak-list)]) - (append - (list - (cond - [(equal? rhs 'contract) ;; contract - (list lhs/contract 'fill 'fill)] - [linebreak? - (list lhs/contract 'fill 'fill)] - [(and sc (eq? style 'left-right/beside-side-conditions)) - (list lhs/contract =-pict (htl-append 10 rhs sc))] - [else - (list lhs/contract =-pict rhs)])) - (if linebreak? - (list - (list (htl-append sep =-pict rhs) - 'fill - 'fill)) - null) - (if (or (not sc) - (and (not linebreak?) - (eq? style 'left-right/beside-side-conditions))) - null - (list - (list sc 'fill 'fill))))))) - ltl-superimpose ltl-superimpose - sep sep)] + (define table-elements + (adjust-for-fills + (apply append + (for/list ([lhs/contract (in-list lhs/contracts)] + [sc (in-list scs)] + [rhs (in-list rhss)] + [linebreak? (in-list linebreak-list)]) + (append + (list + (cond + [(equal? rhs 'contract) ;; contract + (list lhs/contract 'fill 'fill)] + [linebreak? + (list lhs/contract 'fill 'fill)] + [(and sc (eq? style 'left-right/beside-side-conditions)) + (list lhs/contract =-pict (htl-append 10 rhs sc))] + [else + (list lhs/contract =-pict rhs)])) + (if linebreak? + (list + (list (htl-append sep =-pict rhs) + 'fill + 'fill)) + null) + (if (or (not sc) + (and (not linebreak?) + (eq? style 'left-right/beside-side-conditions))) + null + (list + (list sc 'fill 'fill)))))))) + (if (null? table-elements) + (blank) + (table 3 table-elements + ltl-superimpose ltl-superimpose + sep sep))] [(vertical) (apply vl-append sep diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/pict-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/pict-test.rkt index 425824d65e..11c2907945 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/pict-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/pict-test.rkt @@ -1,60 +1,100 @@ #lang racket/base (require racket/file) - ;; these tests just make sure that errors don't - ;; happen. These tests are really only last resorts - ;; for testing functions that aren't easily extraced - ;; from the pict.rkt library +;; these tests just make sure that errors don't happen. (module test racket/base) - - (require redex/reduction-semantics - redex/pict) - - (require texpict/mrpict mred/mred mzlib/class) - - (define-language empty-language) - - (define-language var-ab - [var (a - b)]) - (void (render-language var-ab)) - - (define-language var-not-ab - [var (variable-except x - y)]) - (void (render-language var-not-ab)) - - (let () - (define-metafunction empty-language [(zero any_in) 0]) - (void (render-metafunction zero))) - (void - (render-reduction-relation - (reduction-relation - empty-language - (--> number_const - ,(term - (+ number_const 0)))))) - - (void - (render-reduction-relation - (reduction-relation - empty-language - (--> a b - (fresh x) - (fresh y))))) - +(require redex/reduction-semantics + redex/pict + pict + racket/gui/base + racket/class + rackunit) - (define-language x1-9 - (x 1 2 3 4 5 6 7 8 9)) - - (define-extended-language x0-10 x1-9 - (x 0 .... 10)) - - (void (render-language x0-10)) - - (let ([tmp (make-temporary-file "redex-pict-test~a.pdf")]) - (render-language x0-10 tmp) - (delete-file tmp)) - - (printf "pict-test.rkt passed\n") +(define-language empty-language) + +(define-language var-ab + [var (a + b)]) +(void (render-language var-ab)) + +(define-language var-not-ab + [var (variable-except x + y)]) +(void (render-language var-not-ab)) + +(let () + (define-metafunction empty-language [(zero any_in) 0]) + (void (render-metafunction zero))) + +(void + (render-reduction-relation + (reduction-relation + empty-language + (--> number_const + ,(term + (+ number_const 0)))))) + +(void + (render-reduction-relation + (reduction-relation + empty-language + (--> a b + (fresh x) + (fresh y))))) + + +(define-language x1-9 + (x 1 2 3 4 5 6 7 8 9)) + +(define-extended-language x0-10 x1-9 + (x 0 .... 10)) + +(void (render-language x0-10)) + +(let ([tmp (make-temporary-file "redex-pict-test~a.pdf")]) + (render-language x0-10 tmp) + (delete-file tmp)) + +(define-metafunction empty-language + id : any -> any + [(id any) any]) + +(check-equal? + (pict-width + (parameterize ([metafunction-cases '()]) + (render-metafunction id))) + 0) + +(check-equal? + (pict-height + (parameterize ([metafunction-cases '()]) + (render-metafunction id))) + 0) + +(void + (parameterize ([metafunction-cases '()]) + (render-metafunction id #:contract? #t))) + +(define-judgment-form empty-language + #:mode (deep-empty I) + #:contract (deep-empty any) + [----- + (deep-empty ())] + [(deep-empty any) + ---- + (deep-empty (any))]) + +(check-equal? + (pict-width + (parameterize ([metafunction-cases '()]) + (render-judgment-form deep-empty))) + 0) + +(check-equal? + (pict-height + (parameterize ([metafunction-cases '()]) + (render-judgment-form deep-empty))) + 0) + +(printf "pict-test.rkt passed\n")