Fixing certification tests

svn: r6294
This commit is contained in:
Jay McCarthy 2007-05-25 15:36:49 +00:00
parent 0b74eca282
commit ec228f9092
11 changed files with 1036 additions and 973 deletions

View File

@ -1,5 +1,6 @@
(module lang mzscheme
(require-for-syntax (lib "etc.ss")
(lib "list.ss")
"labels.ss"
"lang/util.ss"
"lang/elim-letrec.ss"

View File

@ -34,6 +34,8 @@
(anormal id stx))
(define (anormal ctxt stx)
(recertify
stx
(kernel-syntax-case
stx #f
[(begin)
@ -160,7 +162,7 @@
[id (identifier? #'id)
(ctxt #'id)]
[_
(raise-syntax-error 'anormal "Dropped through:" stx)]))
(raise-syntax-error 'anormal "Dropped through:" stx)])))
;; anormal*: ((listof w) -> target-expr) (listof source-expr) -> target-expr
;; normalize an expression given as a context and list of sub-expressions

View File

@ -15,6 +15,9 @@
; defun : syntax[1] -> (values syntax?[2] (listof syntax?)[3])
; defunctionalizes the first syntax, returning the second and the lifted lambdas [3]
(define (defun stx)
(recertify/new-defs
stx
(lambda ()
(kernel-syntax-case
stx #f
[(begin be ...)
@ -131,7 +134,7 @@
(values stx
empty)]
[_
(raise-syntax-error 'defun "Dropped through:" stx)]))
(raise-syntax-error 'defun "Dropped through:" stx)]))))
; lift defun to list of syntaxes
(define (lift-defun defun)

View File

@ -10,6 +10,8 @@
;; mark-lambda-as-safe: w -> w
;; If w is a lambda-expression then add #t to the safety mark, otherwise no mark
(define (mark-lambda-as-safe w)
(recertify
w
(syntax-case w (lambda case-lambda)
[(lambda formals be ...)
(syntax/loc w
@ -21,12 +23,14 @@
(case-lambda [formals
(with-continuation-mark safe-call? '(#t (case-lambda formals ...))
be ...)] ...))]
[_else w]))
[_else w])))
(define (elim-callcc stx)
(elim-callcc/mark id stx))
(define (elim-callcc/mark markit stx)
(recertify
stx
(kernel-syntax-case*
stx #f (call/cc call-with-values)
[(begin be ...)
@ -167,4 +171,4 @@
[id (identifier? #'id)
stx]
[_
(raise-syntax-error 'elim-callcc "Dropped through:" stx)])))
(raise-syntax-error 'elim-callcc "Dropped through:" stx)]))))

View File

@ -11,6 +11,8 @@
; Eliminates letrec-values from syntax[2] and correctly handles references to
; letrec-bound variables [3] therein.
(define ((elim-letrec ids) stx)
(recertify
stx
(kernel-syntax-case
stx #f
[(begin be ...)
@ -132,6 +134,6 @@
(syntax/loc stx (#%app unbox id))
#'id)]
[_
(raise-syntax-error 'elim-letrec "Dropped through:" stx)]))
(raise-syntax-error 'elim-letrec "Dropped through:" stx)])))
(define elim-letrec-term (elim-letrec empty)))

View File

@ -4,6 +4,21 @@
(lib "list.ss"))
(provide (all-defined))
(define (recertify old-expr expr)
(syntax-recertify expr old-expr (current-code-inspector) #f))
(define (recertify* old-expr exprs)
(map (lambda (expr)
(syntax-recertify expr old-expr (current-code-inspector) #f))
exprs))
(define (recertify/new-defs old-expr thunk)
(call-with-values
thunk
(lambda (expr new-defs)
(values (recertify old-expr expr)
(recertify* old-expr new-defs)))))
(define current-code-labeling
(make-parameter
(lambda (stx)
@ -27,6 +42,8 @@
(list* #'rv (syntax->list #'(v ...)))]))
(define ((make-define-case inner) stx)
(recertify
stx
(syntax-case stx (define-values define-syntaxes define-values-for-syntax)
[(define-values (v ...) ve)
(with-syntax ([ve (inner #'ve)])
@ -41,13 +58,15 @@
(syntax/loc stx
(define-values-for-syntax (v ...) ve)))]
[_
(raise-syntax-error 'define-case "Dropped through:" stx)]))
(raise-syntax-error 'define-case "Dropped through:" stx)])))
(define ((make-define-case/new-defs inner) stx)
(let-values ([(nstx defs) (inner stx)])
(append defs (list nstx))))
(define ((make-module-case/new-defs inner) stx)
(recertify*
stx
(syntax-case* stx (require provide require-for-syntax require-for-template) module-identifier=?
[(require spec ...)
(list stx)]
@ -58,9 +77,11 @@
[(require-for-template spec ...)
(list stx)]
[_
(inner stx)]))
(inner stx)])))
(define ((make-module-case inner) stx)
(recertify
stx
(syntax-case* stx (require provide require-for-syntax require-for-template) module-identifier=?
[(require spec ...)
stx]
@ -71,9 +92,11 @@
[(require-for-template spec ...)
stx]
[_
(inner stx)]))
(inner stx)])))
(define ((make-lang-module-begin make-labeling transform) stx)
(recertify
stx
(syntax-case stx ()
((mb forms ...)
(with-syntax ([(pmb rfs body ...)
@ -90,7 +113,7 @@
(let ([new-defs (apply append (map transform (syntax->list #'(body ...))))])
(quasisyntax/loc stx
(pmb rfs
#,@new-defs)))))))))
#,@new-defs))))))))))
(define (bound-identifier-member? id ids)
(ormap
@ -100,6 +123,8 @@
;; Kernel Case Template
(define (template stx)
(recertify
stx
(kernel-syntax-case
stx #f
[(begin be ...)
@ -187,4 +212,4 @@
[id (identifier? #'id)
stx]
[_
(raise-syntax-error 'kerncase "Dropped through:" stx)])))
(raise-syntax-error 'kerncase "Dropped through:" stx)]))))

View File

@ -0,0 +1,58 @@
(module certify-tests mzscheme
(require (planet "test.ss" ("schematics" "schemeunit.plt" 1 1))
"language-tester.ss")
(provide certify-suite)
(define certify-suite
(make-test-suite
"Test the certification process"
(make-test-suite
"Splicing tests"
(make-test-case
"quasi-quote with splicing: need to recertify context for qq-append"
(let-values ([(go test-m01.1)
(make-module-eval
(module m01.1 "../lang.ss"
(provide start)
(define (start initial)
`(,@(list 1 2 initial)))))])
(go)
(assert equal? (list 1 2 3) (test-m01.1 '(dispatch-start 3)))
(assert equal? (list 1 2 'foo) (test-m01.1 '(dispatch-start 'foo)))))
(make-test-case
"recertify context test (1)"
(let-values ([(go test-m01.2)
(make-module-eval
(module m01.1 "../lang.ss"
(provide start)
(define (start initial)
`(foo ,@(list 1 2 3)))))])
(go)
(assert-true #t)))
(make-test-case
"recertify context test (2)"
(let-values ([(go test-m01.3)
(make-module-eval
(module m01.3 "../lang.ss"
(provide start)
(define (start n)
`(n ,@(list 1 2 3)))))])
(go)
(assert-true #t)))
(make-test-case
"recertify context test (3)"
(let-values ([(go test-m01.4)
(make-module-eval
(module m1 "../lang.ss"
(provide start)
(define (start initial)
(define (bar n)
`(n ,@(list 1 2 3)))
(bar 7))))])
(go)
(assert-true #t)))))))

View File

@ -96,48 +96,6 @@
(assert = 14 (test-m01 '(dispatch-start 0)))
(assert = 20 (test-m01 '(dispatch-start 6)))))
(make-test-case
"quasi-quote with splicing: need to recertify context for qq-append"
(let-values ([(go test-m01.1)
(make-module-eval
(module m01.1 "../lang.ss"
(provide start)
(define (start initial)
`(,@(list 1 2 initial)))))])
(go)
(assert equal? (list 1 2 3) (test-m01.1 '(dispatch-start 3)))
(assert equal? (list 1 2 'foo) (test-m01.1 '(dispatch-start 'foo)))))
(make-test-case
"recertify context test (1)"
(let-values ([(go test-m01.2)
(make-module-eval
(module m01.1 "../lang.ss"
`(foo ,@(list 1 2 3))))])
(go)
(assert-true #t)))
(make-test-case
"recertify context test (2)"
(let-values ([(go test-m01.3)
(make-module-eval
(module m01.3 "../lang.ss"
(lambda (n)
`(n ,@(list 1 2 3)))))])
(go)
(assert-true #t)))
(make-test-case
"recertify context test (3)"
(let-values ([(go test-m01.4)
(make-module-eval
(module m1 "../lang.ss"
(define (bar n)
`(n ,@(list 1 2 3)))
(bar 7)))])
(go)
(assert-true #t)))
;; start-interaction may be called mutitple times
;; each call overwrites the previous interaction
;; continuation with the latest one.

View File

@ -2,17 +2,7 @@
(provide make-module-eval
make-eval/mod-path)
(define-syntax (make-module-eval m-expr)
(syntax-case m-expr (module)
[(_ (module m-id . rest))
#'(let ([ns (make-namespace)])
(parameterize ([current-namespace ns])
(eval '(require "../abort-resume.ss"
(lib "serialize.ss")))
(eval '(module m-id . rest))
(eval '(require m-id)))
(values
(define (go ns)
(lambda ()
(parameterize ([current-namespace ns])
(eval '(abort/cc
@ -22,7 +12,20 @@
(start-interaction
(lambda (k*v)
(lambda (k*v)
((car k*v) k*v)))))))))))
((car k*v) k*v))))))))))))
(define-syntax (make-module-eval m-expr)
(syntax-case m-expr (module)
[(_ (module m-id . rest))
#'(let ([ns (make-namespace)])
(parameterize ([current-namespace ns])
(eval '(require (lib "abort-resume.ss" "web-server" "prototype-web-server")
(lib "serialize.ss")))
(eval '(module m-id . rest))
(eval '(require m-id)))
(values
(go ns)
(lambda (s-expr)
(parameterize ([current-namespace ns])
(eval s-expr)))))]
@ -32,9 +35,10 @@
(define (make-eval/mod-path pth)
(let ([ns (make-namespace)])
(parameterize ([current-namespace ns])
(eval `(require (lib "client.ss" "web-server" "prototype-web-server")
(eval `(require (lib "abort-resume.ss" "web-server" "prototype-web-server")
(lib "serialize.ss")
(file ,pth))))
(values (go ns)
(lambda (expr)
(parameterize ([current-namespace ns])
(eval expr))))))
(eval expr)))))))

View File

@ -48,29 +48,32 @@
(make-test-case
"compose url-parts and recover-serial (1)"
(let* ([ev (make-eval/mod-path "modules/mm00.ss")]
[k0 (simplify-unsimplify (ev '(serialize (dispatch-start 'foo)))
(let-values ([(go ev) (make-eval/mod-path "modules/mm00.ss")])
(go)
(let* ([k0 (simplify-unsimplify (ev '(serialize (dispatch-start 'foo)))
`(file "modules/mm00.ss"))]
[k1 (simplify-unsimplify (ev `(serialize (dispatch (list (deserialize ',k0) 1))))
`(file "modules/mm00.ss"))]
[k2 (simplify-unsimplify (ev `(serialize (dispatch (list (deserialize ',k1) 2))))
`(file "modules/mm00.ss"))])
(assert-true (= 6 (ev `(dispatch (list (deserialize ',k2) 3)))))))
(assert-true (= 6 (ev `(dispatch (list (deserialize ',k2) 3))))))))
(make-test-case
"compose url-parts and recover-serial (2)"
(let* ([ev (make-eval/mod-path "modules/mm01.ss")]
[k0 (simplify-unsimplify (ev '(serialize (dispatch-start 'foo)))
(let-values ([(go ev) (make-eval/mod-path "modules/mm01.ss")])
(go)
(let* ([k0 (simplify-unsimplify (ev '(serialize (dispatch-start 'foo)))
`(file "modules/mm01.ss"))])
(assert-true (= 7 (ev `(dispatch (list (deserialize ',k0) 7)))))))
(assert-true (= 7 (ev `(dispatch (list (deserialize ',k0) 7))))))))
(make-test-case
"compose stuff-url and unstuff-url and recover the serial"
(let* ([ev (make-eval/mod-path "modules/mm00.ss")]
[k0 (stuff-unstuff (ev '(serialize (dispatch-start 'foo)))
(let-values ([(go ev) (make-eval/mod-path "modules/mm00.ss")])
(go)
(let* ([k0 (stuff-unstuff (ev '(serialize (dispatch-start 'foo)))
uri0 `(file "modules/mm00.ss"))]
[k1 (stuff-unstuff (ev `(serialize (dispatch (list (deserialize ',k0) 1))))
uri0 `(file "modules/mm00.ss"))]
[k2 (stuff-unstuff (ev `(serialize (dispatch (list (deserialize ',k1) 2))))
uri0 `(file "modules/mm00.ss"))])
(assert-true (= 6 (ev `(dispatch (list (deserialize ',k2) 3))))))))))
(assert-true (= 6 (ev `(dispatch (list (deserialize ',k2) 3)))))))))))

View File

@ -1,11 +1,13 @@
(module suite mzscheme
(require (planet "graphical-ui.ss" ("schematics" "schemeunit.plt" 1))
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 1))
(planet "test.ss" ("schematics" "schemeunit.plt" 1 1))
"persistent-close-tests.ss"
"test-normalizer.ss"
"closure-tests.ss"
"labels-tests.ss"
"lang-tests.ss"
"certify-tests.ss"
"stuff-url-tests.ss")
(test/graphical-ui
@ -17,4 +19,5 @@
closure-tests-suite
labels-tests-suite
lang-suite
certify-suite
)))