commit e678912c2c7d3ce8cb48670fcc597b886cfc81ae parent 46598499d108b3553036853f459014a1a0469e52 Author: Stephen Chang <stchang@ccs.neu.edu> Date: Wed, 8 Jul 2015 17:24:15 -0400 add stlc+rec-iso files; rename record files; start exist - previously forgot to add stlc+rec-iso.rkt and tests - rename files with records (eg stlc+var, stlc+rec+sub) - use "reco" to avoid confusion with recursive types ("rec") - start exist.rkt --- existential types Diffstat:
| M | tapl/README.md | | | 5 | +++-- |
| A | tapl/exist.rkt | | | 12 | ++++++++++++ |
| M | tapl/stlc+cons.rkt | | | 10 | +++++----- |
| D | tapl/stlc+rec+sub.rkt | | | 60 | ------------------------------------------------------------ |
| A | tapl/stlc+rec-iso.rkt | | | 53 | +++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | tapl/stlc+reco+sub.rkt | | | 60 | ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | tapl/stlc+reco+var.rkt | | | 103 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| D | tapl/stlc+var.rkt | | | 103 | ------------------------------------------------------------------------------- |
| A | tapl/tests/exist-tests.rkt | | | 181 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| M | tapl/tests/run-all-tests.rkt | | | 5 | +++-- |
| D | tapl/tests/stlc+rec+sub-tests.rkt | | | 88 | ------------------------------------------------------------------------------- |
| A | tapl/tests/stlc+rec-iso-tests.rkt | | | 231 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | tapl/tests/stlc+reco+sub-tests.rkt | | | 88 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | tapl/tests/stlc+reco+var-tests.rkt | | | 181 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| D | tapl/tests/stlc+var-tests.rkt | | | 181 | ------------------------------------------------------------------------------- |
15 files changed, 920 insertions(+), 441 deletions(-)
diff --git a/tapl/README.md b/tapl/README.md @@ -6,12 +6,13 @@ A file extends its immediate parent file. - stlc+lit.rkt - ext-stlc.rkt - stlc+tup.rkt - - stlc+var.rkt + - stlc+reco+var.rkt - stlc+cons.rkt - stlc+box.rkt - stlc+rec-iso.rkt + - exist.rkt - stlc+sub.rkt - - stlc+rec+sub.rkt (also pull in tup from stlc+var.rkt) + - stlc+reco+sub.rkt (also pull in tup from stlc+reco+var.rkt) - sysf.rkt - fomega.rkt - fomega2.rkt \ No newline at end of file diff --git a/tapl/exist.rkt b/tapl/exist.rkt @@ -0,0 +1,12 @@ +#lang racket/base +(require "typecheck.rkt") +(require (except-in "stlc+reco+var.rkt" #%app λ) + (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ))) +(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])) +(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ)) + +;; existential types +;; Types: +;; - types from stlc+reco+var.rkt +;; Terms: +;; - terms from stlc+reco+var.rkt diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt @@ -1,17 +1,17 @@ #lang racket/base (require "typecheck.rkt") -(require (prefix-in stlc: (only-in "stlc+var.rkt" #%app)) - (except-in "stlc+var.rkt" #%app)) +(require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app)) + (except-in "stlc+reco+var.rkt" #%app)) (provide (rename-out [stlc:#%app #%app] [cons/tc cons])) -(provide (except-out (all-from-out "stlc+var.rkt") stlc:#%app)) +(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app)) (provide nil isnil head tail) ;; Simply-Typed Lambda Calculus, plus cons ;; Types: -;; - types from stlc+var.rkt +;; - types from stlc+reco+var.rkt ;; - List constructor ;; Terms: -;; - terms from stlc+var.rkt +;; - terms from stlc+reco+var.rkt ;; TODO: enable HO use of list primitives diff --git a/tapl/stlc+rec+sub.rkt b/tapl/stlc+rec+sub.rkt @@ -1,59 +0,0 @@ -#lang racket/base -(require "typecheck.rkt") -;; want to use type=? and eval-type from stlc+var.rkt, not stlc+sub.rkt -(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=? type-eval) - (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?)) - (except-in "stlc+var.rkt" #%app #%datum +) - (prefix-in var: (only-in "stlc+var.rkt" #%datum))) -(provide (rename-out [stlc:#%app #%app] - [datum/tc #%datum])) -(provide (except-out (all-from-out "stlc+sub.rkt") stlc:#%app stlc:#%datum - (for-syntax stlc:sub?)) - (except-out (all-from-out "stlc+var.rkt") var:#%datum)) -(provide (for-syntax sub?)) - -;; Simply-Typed Lambda Calculus, plus subtyping, plus records -;; Types: -;; - types from stlc+sub.rkt -;; Type relations: -;; - sub? extended to records -;; Terms: -;; - terms from stlc+sub.rkt, can leave record form as is - -(define-syntax (datum/tc stx) - (syntax-parse stx - [(_ . n:number) #'(stlc:#%datum . n)] - [(_ . x) #'(var:#%datum . x)])) - -(begin-for-syntax - (define (sub? τ1 τ2) - (or - (syntax-parse (list τ1 τ2) #:literals (× ∨ quote) - [(tup1 tup2) - #:when (and (×? #'tup1) (×? #'tup2)) - #:with (['k:str τk] ...) (stx-map :-args (×-args #'tup1)) - #:with (['l:str τl] ...) (stx-map :-args (×-args #'tup2)) - #:when (subset? (stx-map syntax-e (syntax->list #'(l ...))) - (stx-map syntax-e (syntax->list #'(k ...)))) - (stx-andmap - (syntax-parser - [(l:str τl) - #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...)) - ((current-sub?) #'τk_match #'τl)]) - #'([l τl] ...))] - [(var1 var2) - #:when (and (∨? #'var1) (∨? #'var2)) - #:with (['k:str τk] ...) (stx-map :-args (∨-args #'var1)) - #:with (['l:str τl] ...) (stx-map :-args (∨-args #'var2)) - #:when (subset? (stx-map syntax-e (syntax->list #'(l ...))) - (stx-map syntax-e (syntax->list #'(k ...)))) - (stx-andmap - (syntax-parser - [(l:str τl) - #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...)) - ((current-sub?) #'τk_match #'τl)]) - #'([l τl] ...))] - [_ #f]) - (stlc:sub? τ1 τ2))) - (current-sub? sub?) - (current-typecheck-relation (current-sub?))) -\ No newline at end of file diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt @@ -0,0 +1,52 @@ +#lang racket/base +(require "typecheck.rkt") +(require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ type=?)) + (except-in "stlc+reco+var.rkt" #%app λ type=?)) +(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])) +(provide (except-out (all-from-out "stlc+reco+var.rkt") + stlc:#%app stlc:λ (for-syntax stlc:type=?))) +(provide μ fld unfld (for-syntax type=?)) + +;; stlc + (iso) recursive types +;; Types: +;; - types from stlc+reco+var.rkt +;; - μ +;; Terms: +;; - terms from stlc+reco+var.rkt +;; - fld/unfld + +(begin-for-syntax + ;; extend to handle μ + (define (type=? τ1 τ2) + ;(printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1)) + ;(printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2)) + (syntax-parse (list τ1 τ2) + [(((~literal #%plain-lambda) (x:id ...) k1 ... t1) + ((~literal #%plain-lambda) (y:id ...) k2 ... t2)) + #:when (= (stx-length #'(x ...)) (stx-length #'(y ...))) + #:with (z ...) (generate-temporaries #'(x ...)) + ((current-type=?) (substs #'(z ...) #'(x ...) #'t1) + (substs #'(z ...) #'(y ...) #'t2))] + [_ (stlc:type=? τ1 τ2)])) + (current-type=? type=?) + (current-typecheck-relation type=?)) + +(define-syntax (μ stx) + (syntax-parse stx + [(_ (tv:id) τ_body) + #'(λ (tv) τ_body)])) + +(define-syntax (unfld stx) + (syntax-parse stx + [(_ τ:ann e) + #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm + #:with [e- τ_e] (infer+erase #'e) + #:when ((current-typecheck-relation) #'τ_e #'τ.norm) + (⊢ #'e- (subst #'τ.norm #'tv #'τ_body))])) +(define-syntax (fld stx) + (syntax-parse stx + [(_ τ:ann e) + #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm + #:with [e- τ_e] (infer+erase #'e) + #:when ((current-typecheck-relation) #'τ_e (subst #'τ.norm #'tv #'τ_body)) + (⊢ #'e- #'τ.norm)])) +\ No newline at end of file diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt @@ -0,0 +1,59 @@ +#lang racket/base +(require "typecheck.rkt") +;; want to use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt +(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=? type-eval) + (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?)) + (except-in "stlc+reco+var.rkt" #%app #%datum +) + (prefix-in var: (only-in "stlc+reco+var.rkt" #%datum))) +(provide (rename-out [stlc:#%app #%app] + [datum/tc #%datum])) +(provide (except-out (all-from-out "stlc+sub.rkt") stlc:#%app stlc:#%datum + (for-syntax stlc:sub?)) + (except-out (all-from-out "stlc+reco+var.rkt") var:#%datum)) +(provide (for-syntax sub?)) + +;; Simply-Typed Lambda Calculus, plus subtyping, plus records +;; Types: +;; - types from stlc+sub.rkt +;; Type relations: +;; - sub? extended to records +;; Terms: +;; - terms from stlc+sub.rkt, can leave record form as is + +(define-syntax (datum/tc stx) + (syntax-parse stx + [(_ . n:number) #'(stlc:#%datum . n)] + [(_ . x) #'(var:#%datum . x)])) + +(begin-for-syntax + (define (sub? τ1 τ2) + (or + (syntax-parse (list τ1 τ2) #:literals (× ∨ quote) + [(tup1 tup2) + #:when (and (×? #'tup1) (×? #'tup2)) + #:with (['k:str τk] ...) (stx-map :-args (×-args #'tup1)) + #:with (['l:str τl] ...) (stx-map :-args (×-args #'tup2)) + #:when (subset? (stx-map syntax-e (syntax->list #'(l ...))) + (stx-map syntax-e (syntax->list #'(k ...)))) + (stx-andmap + (syntax-parser + [(l:str τl) + #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...)) + ((current-sub?) #'τk_match #'τl)]) + #'([l τl] ...))] + [(var1 var2) + #:when (and (∨? #'var1) (∨? #'var2)) + #:with (['k:str τk] ...) (stx-map :-args (∨-args #'var1)) + #:with (['l:str τl] ...) (stx-map :-args (∨-args #'var2)) + #:when (subset? (stx-map syntax-e (syntax->list #'(l ...))) + (stx-map syntax-e (syntax->list #'(k ...)))) + (stx-andmap + (syntax-parser + [(l:str τl) + #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...)) + ((current-sub?) #'τk_match #'τl)]) + #'([l τl] ...))] + [_ #f]) + (stlc:sub? τ1 τ2))) + (current-sub? sub?) + (current-typecheck-relation (current-sub?))) +\ No newline at end of file diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt @@ -0,0 +1,102 @@ +#lang racket/base +(require "typecheck.rkt") +(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin tup proj let type=?)) + (except-in "stlc+tup.rkt" #%app begin tup proj let type=?)) +(provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin] + [define/tc define])) +(provide (except-out (all-from-out "stlc+tup.rkt") + stlc:#%app stlc:let stlc:begin stlc:tup stlc:proj + (for-syntax stlc:type=?))) +(provide tup proj var case) +(provide (for-syntax type=?)) + + +;; Simply-Typed Lambda Calculus, plus records and variants +;; Type relations: +;; - type=? extended to strings +;; define-type-alias (also provided to programmer) +;; Types: +;; - types from stlc+tup.rkt +;; - extend tuple type × to include records +;; - sum type constructor ∨ +;; Terms: +;; - terms from stlc+tup.rkt +;; - extend tup to include records +;; - sums (var) +;; TopLevel: +;; - define (values only) + +(begin-for-syntax + ; extend to: + ; 1) accept strings (ie, record labels) + (define (type=? τ1 τ2) + (syntax-parse (list τ1 τ2) + [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))] + [_ (stlc:type=? τ1 τ2)])) + + (current-type=? type=?) + (current-typecheck-relation (current-type=?))) + +(provide define-type-alias) +(define-syntax define-type-alias + (syntax-parser + [(_ alias:id τ:type) + ; must eval, otherwise undefined types will be allowed + #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))])) + +(define-type-constructor : #:arity 2) + +;; records +(define-syntax (tup stx) + (syntax-parse stx #:datum-literals (=) + [(_ [l:str = e] ...) + #:with ((e- τ) ...) (infers+erase #'(e ...)) + (⊢ #'(list (list l e-) ...) #'(× [: l τ] ...))] + [(_ e ...) + #'(stlc:tup e ...)])) +(define-syntax (proj stx) + (syntax-parse stx #:literals (quote) + [(_ rec l:str) + #:with (rec- τ_rec) (infer+erase #'rec) + #:fail-unless (×? #'τ_rec) "not record type" + #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec)) + #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...)) + (⊢ #'(cadr (assoc l rec)) #'τ_match)] + [(_ e ...) #'(stlc:proj e ...)])) + + +(define-type-constructor ∨) + +(define-syntax (var stx) + (syntax-parse stx #:datum-literals (as =) #:literals (quote) + [(_ l:str = e as τ:type) + #:when (∨? #'τ.norm) + #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm)) + #:with (l_match:str τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...)) + #:with (e- τ_e) (infer+erase #'e) + #:when (typecheck? #'τ_e #'τ_match) + (⊢ #'(list l e) #'τ.norm)])) +(define-syntax (case stx) + (syntax-parse stx #:datum-literals (of =>) #:literals (quote) + [(_ e [l:str x => e_l] ...) + #:fail-when (null? (syntax->list #'(l ...))) "no clauses" + #:with (e- τ_e) (infer+erase #'e) + #:when (∨? #'τ_e) + #:with (['l_x:str τ_x] ...) (stx-map :-args (∨-args #'τ_e)) + #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses" + #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive" + #:with (((x-) e_l- τ_el) ...) + (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...)) + #:fail-unless (same-types? #'(τ_el ...)) "branches have different types" + (⊢ #'(let ([l_e (car e-)]) + (cond [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...)) + (stx-car #'(τ_el ...)))])) + +(define-syntax (define/tc stx) + (syntax-parse stx + [(_ x:id e) + #:with (e- τ) (infer+erase #'e) + #:with y (generate-temporary) + #'(begin + (define-syntax x (make-rename-transformer (⊢ #'y #'τ))) + (define y e-))])) +\ No newline at end of file diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt @@ -1,102 +0,0 @@ -#lang racket/base -(require "typecheck.rkt") -(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin tup proj let type=?)) - (except-in "stlc+tup.rkt" #%app begin tup proj let type=?)) -(provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin] - [define/tc define])) -(provide (except-out (all-from-out "stlc+tup.rkt") - stlc:#%app stlc:let stlc:begin stlc:tup stlc:proj - (for-syntax stlc:type=?))) -(provide tup proj var case) -(provide (for-syntax type=?)) - - -;; Simply-Typed Lambda Calculus, plus variants -;; Type relations: -;; - type=? extended to strings -;; define-type-alias (also provided to programmer) -;; Types: -;; - types from stlc+tup.rkt -;; - extend tuple type × to include records -;; - sum type constructor ∨ -;; Terms: -;; - terms from stlc+tup.rkt -;; - extend tup to include records -;; - sums (var) -;; TopLevel: -;; - define (values only) - -(begin-for-syntax - ; extend to: - ; 1) accept strings (ie, record labels) - (define (type=? τ1 τ2) - (syntax-parse (list τ1 τ2) - [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))] - [_ (stlc:type=? τ1 τ2)])) - - (current-type=? type=?) - (current-typecheck-relation (current-type=?))) - -(provide define-type-alias) -(define-syntax define-type-alias - (syntax-parser - [(_ alias:id τ:type) - ; must eval, otherwise undefined types will be allowed - #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))])) - -(define-type-constructor : #:arity 2) - -;; records -(define-syntax (tup stx) - (syntax-parse stx #:datum-literals (=) - [(_ [l:str = e] ...) - #:with ((e- τ) ...) (infers+erase #'(e ...)) - (⊢ #'(list (list l e-) ...) #'(× [: l τ] ...))] - [(_ e ...) - #'(stlc:tup e ...)])) -(define-syntax (proj stx) - (syntax-parse stx #:literals (quote) - [(_ rec l:str) - #:with (rec- τ_rec) (infer+erase #'rec) - #:fail-unless (×? #'τ_rec) "not record type" - #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec)) - #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...)) - (⊢ #'(cadr (assoc l rec)) #'τ_match)] - [(_ e ...) #'(stlc:proj e ...)])) - - -(define-type-constructor ∨) - -(define-syntax (var stx) - (syntax-parse stx #:datum-literals (as =) #:literals (quote) - [(_ l:str = e as τ:type) - #:when (∨? #'τ.norm) - #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm)) - #:with (l_match:str τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...)) - #:with (e- τ_e) (infer+erase #'e) - #:when (typecheck? #'τ_e #'τ_match) - (⊢ #'(list l e) #'τ.norm)])) -(define-syntax (case stx) - (syntax-parse stx #:datum-literals (of =>) #:literals (quote) - [(_ e [l:str x => e_l] ...) - #:fail-when (null? (syntax->list #'(l ...))) "no clauses" - #:with (e- τ_e) (infer+erase #'e) - #:when (∨? #'τ_e) - #:with (['l_x:str τ_x] ...) (stx-map :-args (∨-args #'τ_e)) - #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses" - #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive" - #:with (((x-) e_l- τ_el) ...) - (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...)) - #:fail-unless (same-types? #'(τ_el ...)) "branches have different types" - (⊢ #'(let ([l_e (car e-)]) - (cond [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...)) - (stx-car #'(τ_el ...)))])) - -(define-syntax (define/tc stx) - (syntax-parse stx - [(_ x:id e) - #:with (e- τ) (infer+erase #'e) - #:with y (generate-temporary) - #'(begin - (define-syntax x (make-rename-transformer (⊢ #'y #'τ))) - (define y e-))])) -\ No newline at end of file diff --git a/tapl/tests/exist-tests.rkt b/tapl/tests/exist-tests.rkt @@ -0,0 +1,181 @@ +#lang s-exp "../exist.rkt" +(require "rackunit-typechecking.rkt") + +;; define-type-alias +(define-type-alias Integer Int) +(define-type-alias ArithBinOp (→ Int Int Int)) +;(define-type-alias C Complex) ; error, Complex undefined + +(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer) +(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int) +(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer) +(check-type + : ArithBinOp) +(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int)) + +;; records (ie labeled tuples) +(check-type "Stephen" : String) +(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "phone" Int] [: "male?" Bool])) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone") + : Int ⇒ 781) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?") + : Bool ⇒ #t) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "phone" Int] [: "is-male?" Bool])) + +;; variants +(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit])) +(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) +(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x) + (var "coffee" = (void) as (∨ [: "coffee" Unit])))) +(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) +(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) + : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) + +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => 1])) ; not enough clauses +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => 1] + ["teaaaaaa" x => 2])) ; wrong clause +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => 1] + ["tea" x => 2] + ["coke" x => 3])) ; too many clauses +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => "1"] + ["tea" x => 2])) ; mismatched branch types +(check-type + (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit])) + ["coffee" x => x] + ["tea" x => 2]) : Int ⇒ 1) +(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])) +(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) +(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int)) +(check-type + (case ((λ ([d : Drink]) d) + (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))) + ["coffee" x => (+ (+ x x) (+ x x))] + ["tea" x => 2] + ["coke" y => 3]) + : Int ⇒ 4) + +(check-type + (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink)) + ["coffee" x => (+ (+ x x) (+ x x))] + ["tea" x => 2] + ["coke" y => 3]) + : Int ⇒ 4) + +;; previous tests: ------------------------------------------------------------ +;; tests for tuples ----------------------------------------------------------- +(check-type (tup 1 2 3) : (× Int Int Int)) +(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit))) + +(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1) +(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2") +(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f) +(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large +(typecheck-fail (proj 1 2)) ; not tuple + +;; ext-stlc.rkt tests --------------------------------------------------------- +;; should still pass + +;; 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 pass, some failing may now pass due to added types/forms +(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/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt @@ -3,15 +3,16 @@ (require "stlc+lit-tests.rkt") (require "ext-stlc-tests.rkt") (require "stlc+tup-tests.rkt") -(require "stlc+var-tests.rkt") +(require "stlc+reco+var-tests.rkt") (require "stlc+cons-tests.rkt") (require "stlc+box-tests.rkt") (require "stlc+rec-iso-tests.rkt") (require "stlc+sub-tests.rkt") -(require "stlc+rec+sub-tests.rkt") +(require "stlc+reco+sub-tests.rkt") (require "sysf-tests.rkt") +(require "exist-tests.rkt") (require "fomega-tests.rkt") (require "fomega2-tests.rkt") \ No newline at end of file diff --git a/tapl/tests/stlc+rec+sub-tests.rkt b/tapl/tests/stlc+rec+sub-tests.rkt @@ -1,88 +0,0 @@ -#lang s-exp "../stlc+rec+sub.rkt" -(require "rackunit-typechecking.rkt") - -;; record subtyping tests -(check-type "coffee" : String) -(check-type (tup ["coffee" = 3]) : (× [: "coffee" Int])) ; element subtyping -(check-type (var "coffee" = 3 as (∨ [: "coffee" Nat])) : (∨ [: "coffee" Int])) ; element subtyping -(check-type (tup ["coffee" = 3]) : (× [: "coffee" Nat])) -(check-type (tup ["coffee" = 3]) : (× [: "coffee" Top])) -(check-type (var "coffee" = 3 as (∨ [: "coffee" Int])) : (∨ [: "coffee" Top])) ; element subtyping (twice) -(check-type (tup ["coffee" = 3]) : (× [: "coffee" Num])) -(check-not-type (tup ["coffee" = -3]) : (× [: "coffee" Nat])) -(check-type (tup ["coffee" = -3]) : (× [: "coffee" Num])) -(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× [: "coffee" Int])) ; width subtyping -(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× [: "coffee" Num])) ; width+element subtyping - -;; record + fns -(check-type (tup ["plus" = +]) : (× [: "plus" (→ Num Num Num)])) -(check-type + : (→ Num Num Num)) -(check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Num)])) -(check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Top)])) -(check-type (tup ["plus" = +] ["mul" = *]) : (× [: "plus" (→ Int Num Top)])) - -;; previous record tests -;; records (ie labeled tuples) -(check-type "Stephen" : String) -(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [: "name" String] [: "phone" Int] [: "male?" Bool])) -(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") - : String ⇒ "Stephen") -(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") - : String ⇒ "Stephen") -(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone") - : Int ⇒ 781) -(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?") - : Bool ⇒ #t) -(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) -(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) -(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [: "name" String] [: "phone" Int] [: "is-male?" Bool])) - - -;; previous basic subtyping tests ------------------------------------------------------ -(check-type 1 : Top) -(check-type 1 : Num) -(check-type 1 : Int) -(check-type 1 : Nat) -(check-type -1 : Top) -(check-type -1 : Num) -(check-type -1 : Int) -(check-not-type -1 : Nat) -(check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1) -(check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1) -(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1) -(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1) -(typecheck-fail ((λ ([x : Nat]) x) -1)) -(check-type (λ ([x : Int]) x) : (→ Int Int)) -(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output -(check-not-type (λ ([x : Int]) x) : (→ Int Nat)) -(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input -(check-not-type (λ ([x : Int]) x) : (→ Num Int)) - -;; previous tests ------------------------------------------------------------- -;; some change due to more specific types -(check-type 1 : Int) -(check-not-type 1 : (→ Int Int)) -;(typecheck-fail "one") ; unsupported literal -;(typecheck-fail #f) ; unsupported literal -(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) -; Bool now defined -;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type -;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not 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) -;; changed test -(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 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) : Num ⇒ 20) diff --git a/tapl/tests/stlc+rec-iso-tests.rkt b/tapl/tests/stlc+rec-iso-tests.rkt @@ -0,0 +1,231 @@ +#lang s-exp "../stlc+rec-iso.rkt" +(require "rackunit-typechecking.rkt") + +(define-type-alias IntList (μ (X) (∨ [: "nil" Unit] [: "cons" (× Int X)]))) +(define-type-alias ILBody (∨ [: "nil" Unit] [: "cons" (× Int IntList)])) +;; nil +(define nil (fld {IntList} (var "nil" = (void) as ILBody))) +(check-type nil : IntList) +; cons +(define cons (λ ([n : Int] [lst : IntList]) (fld {IntList} (var "cons" = (tup n lst) as ILBody)))) +(check-type cons : (→ Int IntList IntList)) +(check-type (cons 1 nil) : IntList) +(typecheck-fail (cons 1 2)) +(typecheck-fail (cons "1" nil)) + +; isnil +(define isnil + (λ ([lst : IntList]) + (case (unfld {IntList} lst) + ["nil" n => #t] + ["cons" p => #f]))) +(check-type isnil : (→ IntList Bool)) +(check-type (isnil nil) : Bool ⇒ #t) +(check-type (isnil (cons 1 nil)) : Bool ⇒ #f) +(typecheck-fail (isnil 1)) +(typecheck-fail (isnil (cons 1 2))) +(check-type (λ ([f : (→ IntList Bool)]) (f nil)) : (→ (→ IntList Bool) Bool)) +(check-type ((λ ([f : (→ IntList Bool)]) (f nil)) isnil) : Bool ⇒ #t) + +; hd +(define hd + (λ ([lst : IntList]) + (case (unfld {IntList} lst) + ["nil" n => 0] + ["cons" p => (proj p 0)]))) +(check-type hd : (→ IntList Int)) +(check-type (hd nil) : Int ⇒ 0) +(typecheck-fail (hd 1)) +(check-type (hd (cons 11 nil)) : Int ⇒ 11) + +; tl +(define tl + (λ ([lst : IntList]) + (case (unfld {IntList} lst) + ["nil" n => lst] + ["cons" p => (proj p 1)]))) +(check-type tl : (→ IntList IntList)) +(check-type (tl nil) : IntList ⇒ nil) +(check-type (tl (cons 1 nil)) : IntList ⇒ nil) +(check-type (tl (cons 1 (cons 2 nil))) : IntList ⇒ (cons 2 nil)) +(typecheck-fail (tl 1)) + +;; previous stlc+var tests ---------------------------------------------------- +;; define-type-alias +(define-type-alias Integer Int) +(define-type-alias ArithBinOp (→ Int Int Int)) +;(define-type-alias C Complex) ; error, Complex undefined + +(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer) +(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int) +(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer) +(check-type + : ArithBinOp) +(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int)) + +;; records (ie labeled tuples) +(check-type "Stephen" : String) +(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "phone" Int] [: "male?" Bool])) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone") + : Int ⇒ 781) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?") + : Bool ⇒ #t) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "phone" Int] [: "is-male?" Bool])) + +;; variants +(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit])) +(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) +(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x) + (var "coffee" = (void) as (∨ [: "coffee" Unit])))) +(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) +(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) + : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) + +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => 1])) ; not enough clauses +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => 1] + ["teaaaaaa" x => 2])) ; wrong clause +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => 1] + ["tea" x => 2] + ["coke" x => 3])) ; too many clauses +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => "1"] + ["tea" x => 2])) ; mismatched branch types +(check-type + (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit])) + ["coffee" x => x] + ["tea" x => 2]) : Int ⇒ 1) +(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])) +(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) +(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int)) +(check-type + (case ((λ ([d : Drink]) d) + (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))) + ["coffee" x => (+ (+ x x) (+ x x))] + ["tea" x => 2] + ["coke" y => 3]) + : Int ⇒ 4) + +(check-type + (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink)) + ["coffee" x => (+ (+ x x) (+ x x))] + ["tea" x => 2] + ["coke" y => 3]) + : Int ⇒ 4) + +;; previous tests: ------------------------------------------------------------ +;; tests for tuples ----------------------------------------------------------- +(check-type (tup 1 2 3) : (× Int Int Int)) +(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit))) + +(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1) +(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2") +(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f) +(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large +(typecheck-fail (proj 1 2)) ; not tuple + +;; ext-stlc.rkt tests --------------------------------------------------------- +;; should still pass + +;; 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 pass, some failing may now pass due to added types/forms +(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/tests/stlc+reco+sub-tests.rkt b/tapl/tests/stlc+reco+sub-tests.rkt @@ -0,0 +1,88 @@ +#lang s-exp "../stlc+reco+sub.rkt" +(require "rackunit-typechecking.rkt") + +;; record subtyping tests +(check-type "coffee" : String) +(check-type (tup ["coffee" = 3]) : (× [: "coffee" Int])) ; element subtyping +(check-type (var "coffee" = 3 as (∨ [: "coffee" Nat])) : (∨ [: "coffee" Int])) ; element subtyping +(check-type (tup ["coffee" = 3]) : (× [: "coffee" Nat])) +(check-type (tup ["coffee" = 3]) : (× [: "coffee" Top])) +(check-type (var "coffee" = 3 as (∨ [: "coffee" Int])) : (∨ [: "coffee" Top])) ; element subtyping (twice) +(check-type (tup ["coffee" = 3]) : (× [: "coffee" Num])) +(check-not-type (tup ["coffee" = -3]) : (× [: "coffee" Nat])) +(check-type (tup ["coffee" = -3]) : (× [: "coffee" Num])) +(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× [: "coffee" Int])) ; width subtyping +(check-type (tup ["coffee" = -3] ["tea" = 3]) : (× [: "coffee" Num])) ; width+element subtyping + +;; record + fns +(check-type (tup ["plus" = +]) : (× [: "plus" (→ Num Num Num)])) +(check-type + : (→ Num Num Num)) +(check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Num)])) +(check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Top)])) +(check-type (tup ["plus" = +] ["mul" = *]) : (× [: "plus" (→ Int Num Top)])) + +;; previous record tests +;; records (ie labeled tuples) +(check-type "Stephen" : String) +(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "phone" Int] [: "male?" Bool])) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone") + : Int ⇒ 781) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?") + : Bool ⇒ #t) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "phone" Int] [: "is-male?" Bool])) + + +;; previous basic subtyping tests ------------------------------------------------------ +(check-type 1 : Top) +(check-type 1 : Num) +(check-type 1 : Int) +(check-type 1 : Nat) +(check-type -1 : Top) +(check-type -1 : Num) +(check-type -1 : Int) +(check-not-type -1 : Nat) +(check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1) +(check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1) +(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1) +(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1) +(typecheck-fail ((λ ([x : Nat]) x) -1)) +(check-type (λ ([x : Int]) x) : (→ Int Int)) +(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output +(check-not-type (λ ([x : Int]) x) : (→ Int Nat)) +(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input +(check-not-type (λ ([x : Int]) x) : (→ Num Int)) + +;; previous tests ------------------------------------------------------------- +;; some change due to more specific types +(check-type 1 : Int) +(check-not-type 1 : (→ Int Int)) +;(typecheck-fail "one") ; unsupported literal +;(typecheck-fail #f) ; unsupported literal +(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) +; Bool now defined +;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type +;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not 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) +;; changed test +(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 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) : Num ⇒ 20) diff --git a/tapl/tests/stlc+reco+var-tests.rkt b/tapl/tests/stlc+reco+var-tests.rkt @@ -0,0 +1,181 @@ +#lang s-exp "../stlc+reco+var.rkt" +(require "rackunit-typechecking.rkt") + +;; define-type-alias +(define-type-alias Integer Int) +(define-type-alias ArithBinOp (→ Int Int Int)) +;(define-type-alias C Complex) ; error, Complex undefined + +(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer) +(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int) +(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer) +(check-type + : ArithBinOp) +(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int)) + +;; records (ie labeled tuples) +(check-type "Stephen" : String) +(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "phone" Int] [: "male?" Bool])) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone") + : Int ⇒ 781) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?") + : Bool ⇒ #t) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× [: "name" String] [: "phone" Int] [: "is-male?" Bool])) + +;; variants +(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit])) +(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) +(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x) + (var "coffee" = (void) as (∨ [: "coffee" Unit])))) +(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) +(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) + : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) + +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => 1])) ; not enough clauses +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => 1] + ["teaaaaaa" x => 2])) ; wrong clause +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => 1] + ["tea" x => 2] + ["coke" x => 3])) ; too many clauses +(typecheck-fail + (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) + ["coffee" x => "1"] + ["tea" x => 2])) ; mismatched branch types +(check-type + (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit])) + ["coffee" x => x] + ["tea" x => 2]) : Int ⇒ 1) +(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])) +(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) +(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int)) +(check-type + (case ((λ ([d : Drink]) d) + (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))) + ["coffee" x => (+ (+ x x) (+ x x))] + ["tea" x => 2] + ["coke" y => 3]) + : Int ⇒ 4) + +(check-type + (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink)) + ["coffee" x => (+ (+ x x) (+ x x))] + ["tea" x => 2] + ["coke" y => 3]) + : Int ⇒ 4) + +;; previous tests: ------------------------------------------------------------ +;; tests for tuples ----------------------------------------------------------- +(check-type (tup 1 2 3) : (× Int Int Int)) +(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit))) + +(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1) +(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2") +(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f) +(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large +(typecheck-fail (proj 1 2)) ; not tuple + +;; ext-stlc.rkt tests --------------------------------------------------------- +;; should still pass + +;; 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 pass, some failing may now pass due to added types/forms +(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/tests/stlc+var-tests.rkt b/tapl/tests/stlc+var-tests.rkt @@ -1,181 +0,0 @@ -#lang s-exp "../stlc+var.rkt" -(require "rackunit-typechecking.rkt") - -;; define-type-alias -(define-type-alias Integer Int) -(define-type-alias ArithBinOp (→ Int Int Int)) -;(define-type-alias C Complex) ; error, Complex undefined - -(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer) -(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int) -(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer) -(check-type + : ArithBinOp) -(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int)) - -;; records (ie labeled tuples) -(check-type "Stephen" : String) -(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [: "name" String] [: "phone" Int] [: "male?" Bool])) -(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") - : String ⇒ "Stephen") -(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") - : String ⇒ "Stephen") -(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone") - : Int ⇒ 781) -(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?") - : Bool ⇒ #t) -(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) -(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) -(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [: "name" String] [: "phone" Int] [: "is-male?" Bool])) - -;; variants -(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit])) -(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) -(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x) - (var "coffee" = (void) as (∨ [: "coffee" Unit])))) -(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) -(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) - : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) - -(typecheck-fail - (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) - ["coffee" x => 1])) ; not enough clauses -(typecheck-fail - (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) - ["coffee" x => 1] - ["teaaaaaa" x => 2])) ; wrong clause -(typecheck-fail - (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) - ["coffee" x => 1] - ["tea" x => 2] - ["coke" x => 3])) ; too many clauses -(typecheck-fail - (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) - ["coffee" x => "1"] - ["tea" x => 2])) ; mismatched branch types -(check-type - (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit])) - ["coffee" x => x] - ["tea" x => 2]) : Int ⇒ 1) -(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])) -(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) -(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int)) -(check-type - (case ((λ ([d : Drink]) d) - (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))) - ["coffee" x => (+ (+ x x) (+ x x))] - ["tea" x => 2] - ["coke" y => 3]) - : Int ⇒ 4) - -(check-type - (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink)) - ["coffee" x => (+ (+ x x) (+ x x))] - ["tea" x => 2] - ["coke" y => 3]) - : Int ⇒ 4) - -;; previous tests: ------------------------------------------------------------ -;; tests for tuples ----------------------------------------------------------- -(check-type (tup 1 2 3) : (× Int Int Int)) -(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int))) -(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int))) -(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int))) -(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int))) -(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit))) - -(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1) -(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2") -(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f) -(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large -(typecheck-fail (proj 1 2)) ; not tuple - -;; ext-stlc.rkt tests --------------------------------------------------------- -;; should still pass - -;; 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 pass, some failing may now pass due to added types/forms -(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) -