suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

stlc+cons: inference testing

Browse Source
This commit is contained in:
Stephen Chang 2015-12-09 17:30:11 -05:00
parent 6f7edcc431
commit 7999f1cc8c
2 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
tapl/stlc+cons.rkt
View File

@ -14,11 +14,14 @@
(define-typed-syntax nil
[(_ ~! τi:type-ann) (⊢ null : (List τi.norm))]
; minimal type inference
[ni:id #:with τ (syntax-property #'ni 'type) #:when (syntax-e #'τ) (⊢ null : (List τ))]
[_:id #:fail-when #t (error 'nil "requires type annotation") #'(void)])
(define-typed-syntax cons
[(_ e1 e2)
#:with (e1- τ1) (infer+erase #'e1)
#:with (e2- (τ2)) (⇑ e2 as List)
#:with [e1- τ1] (infer+erase #'e1)
#:with e2+ (syntax-property #'e2 'type #'τ1)
#:with (e2- (τ2)) (⇑ e2+ as List)
#:when (typecheck? #'τ1 #'τ2)
(⊢ (cons e1- e2-) : (List τ1))])
(define-typed-syntax isnil

5
tapl/tests/stlc+cons-tests.rkt
View File

@ -3,8 +3,9 @@
(typecheck-fail (cons 1 2)
#:with-msg "Expected type with pattern: \\(List τ)")
(typecheck-fail (cons 1 nil)
#:with-msg "nil: requires type annotation")
;(typecheck-fail (cons 1 nil)
; #:with-msg "nil: requires type annotation")
(check-type (cons 1 nil) : (List Int))
(check-type (cons 1 (nil {Int})) : (List Int))
(typecheck-fail nil #:with-msg "nil: requires type annotation")
(typecheck-fail