allow metafunction-cases to be the empty list
and thus allow metafunctions contracts to be typeset, without showing any of the cases of the metafunction
This commit is contained in:
Robby Findler
parent
735881831b
commit
251b8e283f
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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")
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user