Tests define-judgment-form and metafunction renaming

Closes PR 11469
This commit is contained in:
Casey Klein 2011-08-16 13:02:33 -05:00
parent 9e2e11e9c4
commit e485e9f348

View File

@ -12,11 +12,34 @@
(syntax-line stx)
(syntax-column stx)))
(define arrow-collector%
(define (expected-arrows bindings)
(for/fold ([arrs (set)]) ([binding bindings])
(for/fold ([arrs arrs]) ([bound (cdr binding)])
(set-add arrs
(list (source (car binding))
(source bound))))))
(define (expected-rename-class binding)
(apply set (map source binding)))
(define collector%
(class (annotations-mixin object%)
(super-new)
(define/override (syncheck:find-source-object stx)
stx)
(define/override (syncheck:add-rename-menu id
all-ids
new-name-interferes?)
(match all-ids
[(list (list ids _ _) ...)
(set! renames (cons ids renames))]))
(define renames '())
(define/public (collected-rename-class stx)
(for/fold ([class (set)]) ([ids renames])
(if (for/or ([id ids])
(equal? (source stx) (source id)))
(set-union class (apply set (map source ids)))
class)))
(define/override (syncheck:add-arrow start-source-obj
start-left
start-right
@ -37,7 +60,7 @@
(namespace-anchor->namespace module-anchor))
;; judgment forms
(let ([annotations (new arrow-collector%)])
(let ([annotations (new collector%)])
(define-values (add-syntax done)
(make-traversal module-namespace #f))
@ -51,6 +74,11 @@
(define render-name #'J)
(define holds-name #'J)
(define language-binding
(list language-def-name language-use-name))
(define judgment-form-binding
(list mode-name contract-name conclusion-name premise-name render-name holds-name))
(parameterize ([current-annotations annotations]
[current-namespace module-namespace])
(add-syntax
@ -66,15 +94,15 @@
(done))
(test (send annotations collected-arrows)
(set (list (source language-def-name) (source language-use-name))
(list (source mode-name) (source contract-name))
(list (source mode-name) (source conclusion-name))
(list (source mode-name) (source premise-name))
(list (source mode-name) (source render-name))
(list (source mode-name) (source holds-name)))))
(expected-arrows
(list language-binding judgment-form-binding)))
(test (send annotations collected-rename-class language-def-name)
(expected-rename-class language-binding))
(test (send annotations collected-rename-class mode-name)
(expected-rename-class judgment-form-binding)))
;; metafunctions
(let ([annotations (new arrow-collector%)])
(let ([annotations (new collector%)])
(define-values (add-syntax done)
(make-traversal module-namespace #f))
@ -87,6 +115,11 @@
(define render-name #'f)
(define term-name #'f)
(define language-binding
(list language-def-name language-use-name))
(define metafunction-binding
(list contract-name lhs-name rhs-name render-name term-name))
(parameterize ([current-annotations annotations]
[current-namespace module-namespace])
(add-syntax
@ -100,10 +133,11 @@
(done))
(test (send annotations collected-arrows)
(set (list (source language-def-name) (source language-use-name))
(list (source contract-name) (source lhs-name))
(list (source contract-name) (source rhs-name))
(list (source contract-name) (source render-name))
(list (source contract-name) (source term-name)))))
(expected-arrows
(list language-binding metafunction-binding)))
(test (send annotations collected-rename-class language-def-name)
(expected-rename-class language-binding))
(test (send annotations collected-rename-class contract-name)
(expected-rename-class metafunction-binding)))
(print-tests-passed 'check-syntax-test.rkt)