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.