From 8d6eaf227e55331afea6823dd36e0e4a0fa9f9a8 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 28 Jul 2015 19:32:16 -0400 Subject: [PATCH] ext-stlc-tests.rkt passing --- tapl/ext-stlc.rkt | 32 ++++++++------- tapl/tests/ext-stlc-tests.rkt | 76 +++++++++++++++++++++++++++-------- tapl/tests/stlc+lit-tests.rkt | 1 - 3 files changed, 78 insertions(+), 31 deletions(-) diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt index 34b01c0..f97dffe 100644 --- a/tapl/ext-stlc.rkt +++ b/tapl/ext-stlc.rkt @@ -2,7 +2,7 @@ (require "typecheck.rkt") ;; prefix-in an identifier if: ;; - it will be extended, eg #%datum -;; - want to use racket's version in this file, eg #%app +;; - want to use racket's version in implemetation (this) file, eg #%app (require (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum)) (except-in "stlc+lit.rkt" #%app #%datum)) (provide (rename-out [datum/tc #%datum] @@ -33,8 +33,8 @@ (define-syntax (datum/tc stx) (syntax-parse stx - [(_ . b:boolean) (⊢ (syntax/loc stx (#%datum . b)) #'Bool)] - [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)] + [(_ . b:boolean) (⊢ (#%datum . b) : Bool)] + [(_ . s:str) (⊢ (#%datum . s) : String)] [(_ . x) #'(stlc:#%datum . x)])) (define-primop zero? : (→ Int Bool)) @@ -51,7 +51,7 @@ #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1)) #:with (e2- τ2) (infer+erase #'e2) #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2)) - (⊢ #'(and e1- e2-) #'Bool)])) + (⊢ (and e1- e2-) : Bool)])) (define-syntax (or/tc stx) (syntax-parse stx @@ -60,7 +60,7 @@ #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1)) #:with (e2- τ2) (infer+erase #'e2) #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2)) - (⊢ #'(or e1- e2-) #'Bool)])) + (⊢ (or e1- e2-) : Bool)])) (define-syntax (if/tc stx) (syntax-parse stx @@ -70,7 +70,7 @@ #:with (e1- τ1) (infer+erase #'e1) #:with (e2- τ2) (infer+erase #'e2) #:when ((current-type=?) #'τ1 #'τ2) - (⊢ #'(if e_tst- e1- e2-) #'τ1)])) + (⊢ (if e_tst- e1- e2-) : τ1)])) (define-base-type Unit) (define-primop void : (→ Unit)) @@ -89,7 +89,7 @@ #'(e_unit ...) #'(τ_unit ...)) "\n") "\n") - (⊢ #'(begin e_unit- ... e-) #'τ)])) + (⊢ (begin e_unit- ... e-) : τ)])) (define-syntax (ann stx) (syntax-parse stx #:datum-literals (:) @@ -98,14 +98,14 @@ #:fail-unless (typecheck? #'τ #'ascribed-τ) (format "~a does not have type ~a\n" (syntax->datum #'e) (syntax->datum #'ascribed-τ)) - (⊢ #'e- #'ascribed-τ)])) + (⊢ e- : ascribed-τ)])) (define-syntax (let/tc stx) (syntax-parse stx [(_ ([x e] ...) e_body) #:with ((e- τ) ...) (infers+erase #'(e ...)) #:with ((x- ...) e_body- τ_body) (infer/type-ctxt+erase #'([x τ] ...) #'e_body) - (⊢ #'(let ([x- e-] ...) e_body-) #'τ_body)])) + (⊢ (let ([x- e-] ...) e_body-) : τ_body)])) (define-syntax (let*/tc stx) (syntax-parse stx @@ -118,13 +118,17 @@ [(_ ([b:typed-binding e] ...) e_body) #:with ((x- ...) (e- ... e_body-) (τ ... τ_body)) (infers/type-ctxt+erase #'(b ...) #'(e ... e_body)) - #:fail-unless (typechecks? #'(b.τ ...) #'(τ ...)) + #:fail-unless (typechecks? (type-evals #'(b.τ ...)) #'(τ ...)) (string-append - "letrec: type check fail, args have wrong type:\n" + "type check fail, args have wrong type:\n" (string-join - (stx-map (λ (e τ τ-expect) (format "~a has type ~a, expected ~a" e τ τ-expect)) - #'(e ...) #'(τ ...) #'(b.τ ...)) + (stx-map + (λ (e τ τ-expect) + (format + "~a has type ~a, expected ~a" + (syntax->datum e) (type->str τ) (type->str τ-expect))) + #'(e ...) #'(τ ...) #'(b.τ ...)) "\n")) - (⊢ #'(letrec ([x- e-] ...) e_body-) #'τ_body)])) + (⊢ (letrec ([x- e-] ...) e_body-) : τ_body)])) \ No newline at end of file diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt index a6759cd..e7db535 100644 --- a/tapl/tests/ext-stlc-tests.rkt +++ b/tapl/tests/ext-stlc-tests.rkt @@ -12,14 +12,26 @@ ;; Unit (check-type (void) : Unit) (check-type void : (→ Unit)) -(typecheck-fail ((λ ([x : Unit]) x) 2)) -(typecheck-fail ((λ ([x : Unit])) void)) + +(typecheck-fail + ((λ ([x : Unit]) x) 2) + #:with-msg + "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Unit") +(typecheck-fail + ((λ ([x : Unit]) x) void) + #:with-msg + "Arguments to function.+have wrong type.+Given:.+(→ Unit).+Expected:.+Unit") + (check-type ((λ ([x : Unit]) x) (void)) : Unit) ;; begin -(typecheck-fail (begin)) (check-type (begin 1) : Int) -(typecheck-fail (begin 1 2 3)) + +(typecheck-fail (begin) #:with-msg "expected more terms") +(typecheck-fail + (begin 1 2 3) + #:with-msg "all begin expressions except the last one should have type Unit") + (check-type (begin (void) 1) : Int ⇒ 1) (check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int) (check-type ((λ ([x : Int]) (begin x)) 1) : Int) @@ -28,23 +40,37 @@ (check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int) ;;ascription -(typecheck-fail (ann 1 : Bool)) (check-type (ann 1 : Int) : Int ⇒ 1) (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) +(typecheck-fail (ann 1 : Bool) #:with-msg "ann: 1 does not have type Bool") ; let (check-type (let () (+ 1 1)) : Int ⇒ 2) (check-type (let ([x 10]) (+ 1 2)) : Int) -(typecheck-fail (let ([x #f]) (+ x 1))) (check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) -(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier +(typecheck-fail + (let ([x #f]) (+ x 1)) + #:with-msg + "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int") +(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y)) + #:with-msg "x: unbound identifier") (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) -(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1)) +(typecheck-fail + (let* ([x #t] [y (+ x 1)]) 1) + #:with-msg + "Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int") + ; letrec -(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y)) -(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x)) +(typecheck-fail + (letrec ([(x : Int) #f] [(y : Int) 1]) y) + #:with-msg + "letrec: type check fail, args have wrong type:\n#f has type Bool, expected Int") +(typecheck-fail + (letrec ([(y : Int) 1] [(x : Int) #f]) x) + #:with-msg + "letrec: type check fail, args have wrong type:.+#f has type Bool, expected Int") (check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) @@ -80,14 +106,32 @@ (check-type (λ ([x : Int]) x) : (→ Int Int)) (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) -(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type + +(typecheck-fail + ((λ ([x : Bool]) x) 1) + #:with-msg + "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Bool") ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type -(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type +(typecheck-fail (λ ([f : Int]) (f 1 2)) + #:with-msg + "Expected type with pattern: \\(→ τ_in ... τ_out\\), got: Int") + (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) : (→ (→ Int Int Int) Int Int Int)) -(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) -(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int -(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int -(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args +(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) + : Int ⇒ 3) + +(typecheck-fail + (+ 1 (λ ([x : Int]) x)) + #:with-msg + "Arguments to function \\+ have wrong type.+Given:\n 1 : Int.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int") +(typecheck-fail + (λ ([x : (→ Int Int)]) (+ x x)) + #:with-msg + "Arguments to function \\+ have wrong type.+Given:.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int") +(typecheck-fail + ((λ ([x : Int] [y : Int]) y) 1) + #:with-msg "Arguments to function.+have.+wrong number of arguments") + (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt index 80976cc..48cfc5e 100644 --- a/tapl/tests/stlc+lit-tests.rkt +++ b/tapl/tests/stlc+lit-tests.rkt @@ -46,7 +46,6 @@ (λ ([x : (→ Int Int)]) (+ x x)) #:with-msg "Arguments to function \\+ have wrong type.+Given:.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int") - (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1) #:with-msg "Arguments to function.+have.+wrong number of arguments")