From c4813ebd95508c59278e468d45560d72067e9263 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 20 May 2015 18:10:39 -0400 Subject: [PATCH] add ext-stlc, not including data structures --- tapl/ext-stlc.rkt | 129 ++++++++++++++++++++++++++++++++++ tapl/stlc.rkt | 2 +- tapl/tests/ext-stlc-tests.rkt | 87 +++++++++++++++++++++++ tapl/typecheck.rkt | 34 ++++++++- 4 files changed, 249 insertions(+), 3 deletions(-) create mode 100644 tapl/ext-stlc.rkt create mode 100644 tapl/tests/ext-stlc-tests.rkt diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt new file mode 100644 index 0000000..31b63aa --- /dev/null +++ b/tapl/ext-stlc.rkt @@ -0,0 +1,129 @@ +#lang racket/base +(require + (for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt") + "typecheck.rkt") +(require (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ #%datum)) + (except-in "stlc+lit.rkt" #%app λ #%datum)) +(provide (rename-out [datum/tc #%datum] + [stlc:#%app #%app] + [stlc:λ λ] + [and/tc and] [or/tc or] [if/tc if] + [begin/tc begin] + [let/tc let] [let*/tc let*] [letrec/tc letrec]) + ann) +(provide (all-from-out "stlc+lit.rkt")) + +;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11) +;; Types: +;; - types from stlc+lit.rkt +;; - Bool, String +;; - Unit +;; Terms: +;; - terms from stlc+lit.rkt +;; - literals: bool, string +;; - prims: and, or, not, zero? +;; - prim void : (→ Unit) +;; - begin +;; - ascription (ann) +;; - let + +(define-base-type Bool) +(define-base-type String) + +(define-syntax (datum/tc stx) + (syntax-parse stx + [(_ . b:boolean) (⊢ (syntax/loc stx (#%datum . b)) #'Bool)] + [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)] + [(_ . x) #'(stlc:#%datum . x)])) + +(define-primop zero? : (Int → Bool)) +(define-primop = : (Int Int → Bool)) +(define-primop - : (Int Int → Int)) +(define-primop add1 : (Int → Int)) +(define-primop sub1 : (Int → Int)) +(define-primop not : (Bool → Bool)) + +(define-syntax (and/tc stx) + (syntax-parse stx + [(_ e1 e2) + #:with (e1- τ1) (infer+erase #'e1) + #: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)])) + +(define-syntax (or/tc stx) + (syntax-parse stx + [(_ e1 e2) + #:with (e1- τ1) (infer+erase #'e1) + #: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)])) + +(define-syntax (if/tc stx) + (syntax-parse stx + [(_ e_tst e1 e2) + #:with (e_tst- τ_tst) (infer+erase #'e_tst) + #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst)) + #:with (e1- τ1) (infer+erase #'e1) + #:with (e2- τ2) (infer+erase #'e2) + #:when (type=? #'τ1 #'τ2) + (⊢ #'(if e_tst- e1- e2-) #'τ1)])) + +(define-base-type Unit) +(define-primop void : (→ Unit)) + +(define-syntax (begin/tc stx) + (syntax-parse stx + [(_ e_unit ... e) + #:with ((e_unit- τ_unit) ...) (infers+erase #'(e_unit ...)) + #:with (e- τ) (infer+erase #'e) + #:fail-unless (stx-andmap Unit? #'(τ_unit ...)) + (string-append + "all begin expressions except the last one should have type Unit\n" + (string-join + (stx-map + (λ (e τ) (format "~a : ~a" (syntax->datum e) (syntax->datum τ))) + #'(e_unit ...) #'(τ_unit ...)) + "\n") + "\n") + (⊢ #'(begin e_unit- ... e-) #'τ)])) + +(define-syntax (ann stx) + (syntax-parse stx #:datum-literals (:) + [(_ e : ascribed-τ) + #:with (e- τ) (infer+erase #'e) + #:fail-unless (type=? #'ascribed-τ #'τ) + (format "~a does not have type ~a\n" + (syntax->datum #'e) (syntax->datum #'ascribed-τ)) + (⊢ #'e- #'τ)])) + +(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)])) + +(define-syntax (let*/tc stx) + (syntax-parse stx + [(_ () e_body) #'e_body] + [(_ ([x e] [x_rst e_rst] ...) e_body) + #'(let/tc ([x e]) (let*/tc ([x_rst e_rst] ...) e_body))])) + +(define-syntax (letrec/tc stx) + (syntax-parse stx + [(_ ([b:typed-binding e] ...) e_body) + #:with ((x- ...) (e- ... e_body-) (τ ... τ_body)) + (infers/type-ctxt+erase #'(b ...) #'(e ... e_body)) + #:fail-unless (types=? #'(b.τ ...) #'(τ ...)) + (string-append + "letrec: type check fail, args have wrong type:\n" + (string-join + (stx-map (λ (e τ τ-expect) (format "~a has type ~a, expected ~a")) + #'(e ...) #'(τ ...) #'(b.τ ...)) + "\n")) + (⊢ #'(letrec ([x- e-] ...) e_body-) #'τ_body)])) + + \ No newline at end of file diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index 8ccc1cc..24539c1 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -38,7 +38,7 @@ (string-join (map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...))) ", ") - "\nexpect arguments with type: " + "\nexpected arguments with type: " (string-join (map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...))) ", ")) diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt new file mode 100644 index 0000000..dad46df --- /dev/null +++ b/tapl/tests/ext-stlc-tests.rkt @@ -0,0 +1,87 @@ +#lang s-exp "../ext-stlc.rkt" +(require "rackunit-typechecking.rkt") + +;; tests for stlc extensions + +;; new literals and base types +(check-type "one" : String) ; literal now supported +(check-type #f : Bool) ; literal now supported + +(check-type (λ ([x : Bool]) x) : (Bool → Bool)) ; Bool is now valid type + +;; Unit +(check-type (void) : Unit) +(check-type void : (→ Unit)) +(typecheck-fail ((λ ([x : Unit]) x) 2)) +(typecheck-fail ((λ ([x : Unit])) void)) +(check-type ((λ ([x : Unit]) x) (void)) : Unit) + +;; begin +(typecheck-fail (begin)) +(check-type (begin 1) : Int) +(typecheck-fail (begin 1 2 3)) +(check-type (begin (void) 1) : Int ⇒ 1) + +;;ascription +(typecheck-fail (ann 1 : Bool)) +(check-type (ann 1 : Int) : Int ⇒ 1) +(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) + +; 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 + +(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) +(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1)) + +; letrec +(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y)) +(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x)) + +(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) + +;; recursive +(check-type + (letrec ([(countdown : (Int → String)) + (λ ([i : Int]) + (if (= i 0) + "liftoff" + (countdown (- i 1))))]) + (countdown 10)) : String ⇒ "liftoff") + +;; mutually recursive +(check-type + (letrec ([(is-even? : (Int → Bool)) + (λ ([n : Int]) + (or (zero? n) + (is-odd? (sub1 n))))] + [(is-odd? : (Int → Bool)) + (λ ([n : Int]) + (and (not (zero? n)) + (is-even? (sub1 n))))]) + (is-odd? 11)) : Bool ⇒ #t) + +;; tests from stlc+lit-tests.rkt - most should still pass -------------------------- +(check-type 1 : Int) +;(check-not-type 1 : (Int → Int)) +;(typecheck-fail "one") ; literal now supported +;(typecheck-fail #f) ; literal now supported +(check-type (λ ([x : Int] [y : Int]) x) : (Int Int → Int)) +(check-not-type (λ ([x : Int]) x) : Int) +(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)) ; Bool is now valid type +(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type +(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 ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) + diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index adafa79..11d45fc 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -23,11 +23,15 @@ (define-syntax (define-base-type stx) (syntax-parse stx [(_ τ:id) + #:with τ? (format-id #'τ "~a?" #'τ) #'(begin (provide τ) (define-syntax (τ stx) (syntax-parse stx - [_ (error 'Int "Cannot use type at run time.")])))])) + [_ (error 'Int "Cannot use type at run time.")])) + (define-for-syntax (τ? τ1) + (type=? τ1 #'τ)))])) + (define-syntax (define-type-constructor stx) (syntax-parse stx [(_ τ:id) @@ -44,6 +48,19 @@ (type=? #'τ id))] [_ #f])) )])) +;(define-syntax (define-constant-type stx) +; (syntax-parse stx +; [(_ τ:id) +; #:with constructor +; (datum->syntax #'τ (string->symbol (string-downcase (symbol->string (syntax>datum #'τ))))) +; #:with const-name +; (generate-temporary #'constructor) +; #'(begin +; (provide τ constructor) +; (struct +; (define-syntax (τ stx) +; (syntax-parse stx +; [_ (error 'Int "Cannot use type at run time.")])))])) ;; type classes (begin-for-syntax @@ -78,7 +95,20 @@ (expand/df #`(λ (x ...) (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e))) - (list #'xs+ #'e+ (typeof #'e+))])) + (list #'xs+ #'e+ (typeof #'e+))] + [([x τ] ...) (infer/type-ctxt+erase #'([x : τ] ...) e)])) + (define (infers/type-ctxt+erase ctxt es) + (syntax-parse ctxt + [(b:typed-binding ...) + #:with (x ...) #'(b.x ...) + #:with (τ ...) #'(b.τ ...) + #:with + (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+ ...))) + (expand/df + #`(λ (x ...) + (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,@es))) + (list #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))] + [([x τ] ...) (infers/type-ctxt+erase #'([x : τ] ...) es)])) (define (infer+erase e) (define e+ (expand/df e))