3 Rackunit-Style Test Forms for Turnstile
| (require rackunit/turnstile) | |
| package: rackunit-macrotypes-lib | |
This section describes rackunit-style test forms that are used primarily for testing the type checking of Turnstile-created languages.
This section will use the following Turnstile-defined, simply typed language to demonstrate the testing forms:
; types (define-base-types Int Bool) (define-type-constructor β #:arity = 2) ; rule for Int and Bool literals
(define-typed-syntax #%datum [(_ . n:integer) β« -------- [β’ 'n β Int]] [(_ . b:boolean) β« -------- [β’ 'b β Bool]] [(_ . x) β« -------- [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]]) ; single-arity Ξ»
(define-typed-syntax Ξ» [(_ [x:id (~datum :) Ο_in:type] e) β« [[x β« x- : Ο_in.norm] β’ e β« e- β Ο_out] ------- [β’ (#%plain-lambda (x-) e-) β (β Ο_in.norm Ο_out)]] [(_ x:id e) β (~β Ο_in Ο_out) β« [[x β« x- : Ο_in] β’ e β« e- β Ο_out] --------- [β’ (#%plain-lambda (x-) e-)]]) ; single-arity function application
(define-typed-syntax (#%app e_fn e_arg) β« [β’ e_fn β« e_fn- β (~β Ο_in Ο_out)] [β’ e_arg β« e_arg- β Ο_in] -------- [β’ (#%plain-app e_fn- e_arg-) β Ο_out]) ; add1 primop (define-primop add1 : (β Int Int)) ; top-level define
(define-syntax define (syntax-parser [(_ f [x:id (~datum :) Ο_in] : Ο_out e) #'(define-typed-variable f (Ξ» x e) β (β Ο_in Ο_out))]))
3.1 Expression Test Forms
syntax
(check-type e tag Ο)
(check-type e tag Ο -> val) (check-type e tag Ο β val)
The expression eβs "type" is determined by tag, which must be an identifier and is used as a symbol key for a syntax property lookup on eβs expanded form. The supplied tag will be most commonly be :.
During type checking, Ο is set as eβs "expected type". Thus, a ruleβs "check" (β) variant, if defined, will be invoked to type check e.
If an optional val argument is specified, the test additionally evaluates e at run time and checks that the result is equal to val according to check-equal? (from rackunit).
> (check-type Int :: #%type) > (check-type add1 : (β Int Int)) ; pass > (check-type (add1 2) : Int) ; type check fail > (check-type (add1 2) : Bool) eval:11:0: check-type: Expression (add1 2) [loc 11:0] has
type Int, expected Bool
at: (check-type (add1 2) : Bool)
in: (check-type (add1 2) : Bool)
; pass > (check-type (add1 2) : Int -> 3) ; run time fail > (check-type (add1 2) : Int -> 4)
--------------------
FAILURE
name: check-equal?
location: eval:13:0
actual: 3
expected: 4
--------------------
syntax
(check-not-type e : Ο)
This test form is particularly useful for languages with subtyping.
; pass > (check-not-type add1 : Int) ; fail > (check-not-type add1 : (β Int Int)) eval:15:0: check-not-type: (15:0) Expression add1 has type
(β Int Int); should not typecheck with (β Int Int)
at: (check-not-type add1 : (β Int Int))
in: (check-not-type add1 : (β Int Int))
syntax
(typecheck-fail e)
(typecheck-fail e #:with-msg msg-pat) (typecheck-fail e #:verb-msg msg-str)
Supplying an optional msg-pat argument requires the error message to match the given pattern according to regexp-match?.
Supplying an optional msg-str argument requires the error message to include the given string verbatim.
; pass: because type checking fails > (typecheck-fail (add1 #f)) ; fail: because type checking succeeds > (typecheck-fail (add1 1))
--------------------
FAILURE
expected: ""
location: eval:17:0
name: typecheck-fail
params: '((add1 1) "")
message: "No exception raised"
--------------------
; pass > (typecheck-fail (add1 add1) #:with-msg "expected Int, given \\(β Int Int\\)") ; fail: msg does not match because some chars must be escaped > (typecheck-fail (add1 add1) #:with-msg "expected Int, given (β Int Int)")
--------------------
FAILURE
expected: "expected Int, given (β Int Int)"
location: eval:19:0
name: typecheck-fail
params: '((add1 add1) "expected Int, given (β Int Int)")
message: "Wrong exception raised"
exn-message:
"eval:19:0: #%app: type mismatch: expected Int, given (β Int Int)\n expression: add1\n at: add1\n in: (#%app add1 add1)"
exn:
#(struct:exn:fail:syntax "eval:19:0: #%app: type mismatch: expected Int, given (β Int Int)\n expression: add1\n at: add1\n in: (#%app add1 add1)" #<continuation-mark-set> (#<syntax:eval:19:0 add1>))
--------------------
; pass, with unescaped msg using #:verb-msg > (typecheck-fail (add1 add1) #:verb-msg "expected Int, given (β Int Int)")
syntax
3.2 Top-Level Test Forms
syntax
(typecheck-fail/toplvl def)
(typecheck-fail/toplvl def #:with-msg msg-pat) (typecheck-fail/toplvl def #:verb-msg msg-str)
> (typecheck-fail/toplvl (define f [x : Int] : Bool (add1 x)))
> (typecheck-fail/toplvl (define f [x : Int] : Bool (add1 x)) #:with-msg "expected Bool, given Int.* expression: \\(add1 x\\)")
syntax
(typecheck-fail/definitions [def ...])
(typecheck-fail/definitions [def ...] #:with-msg msg-pat) (typecheck-fail/definitions [def ...] #:verb-msg msg-str)
3.3 Other Debugging Forms
syntax
(print-type e)
(print-type e #:tag tag) (print-type e #:raw)
Unless explicitly given a tag argument, the returned type is the syntax property at tag ':.
If written with the #:raw declaration, returns the internal representation of the type. Otherwise, the type is first resugared according to type->str.