start copying tests over to macrotypes/examples/tests
This commit is contained in:
AlexKnauth
parent
308fb84792
commit
a8f1634baa
|
|
@ -1,6 +1,6 @@
|
|||
#lang s-exp macrotypes/typecheck
|
||||
(extends "stlc+lit.rkt" #:except #%datum)
|
||||
(provide (for-syntax current-join))
|
||||
(provide ⊔ (for-syntax current-join))
|
||||
|
||||
;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11)
|
||||
;; Types:
|
||||
|
|
@ -38,16 +38,19 @@
|
|||
|
||||
(define-typed-syntax and
|
||||
[(and e1 e2)
|
||||
#:with e1- (⇑ e1 as Bool)
|
||||
#:with e2- (⇑ e2 as Bool)
|
||||
#:with Bool* ((current-type-eval) #'Bool)
|
||||
#:with [e1- τ_e1] (infer+erase #'e1)
|
||||
#:with [e2- τ_e2] (infer+erase #'e2)
|
||||
#:fail-unless (typecheck? #'τ_e1 #'Bool*) (typecheck-fail-msg/1 #'Bool* #'τ_e1 #'e1)
|
||||
#:fail-unless (typecheck? #'τ_e2 #'Bool*) (typecheck-fail-msg/1 #'Bool* #'τ_e2 #'e2)
|
||||
(⊢ (and- e1- e2-) : Bool)])
|
||||
|
||||
(define-typed-syntax or
|
||||
[(or e ...)
|
||||
#:with (e- ...) (⇑s (e ...) as Bool)
|
||||
; #:with e1- (⇑ e1 as Bool)
|
||||
; #:with e2- (⇑ e2 as Bool)
|
||||
; (⊢ (or- e1- e2-) : Bool)])
|
||||
#:with ([_ Bool*] ...) #`([e #,((current-type-eval) #'Bool)] ...)
|
||||
#:with ([e- τ_e] ...) (infers+erase #'(e ...))
|
||||
#:fail-unless (typechecks? #'(τ_e ...) #'(Bool* ...))
|
||||
(typecheck-fail-msg/multi #'(Bool* ...) #'(τ_e ...) #'(e ...))
|
||||
(⊢ (or- e- ...) : Bool)])
|
||||
|
||||
(begin-for-syntax
|
||||
|
|
@ -60,17 +63,22 @@
|
|||
#:msg "branches have incompatible types: ~a and ~a" x y))
|
||||
x))))
|
||||
|
||||
(define-syntax ⊔
|
||||
(syntax-parser
|
||||
[(⊔ τ1 τ2 ...)
|
||||
(for/fold ([τ ((current-type-eval) #'τ1)])
|
||||
([τ2 (in-list (stx-map (current-type-eval) #'[τ2 ...]))])
|
||||
((current-join) τ τ2))]))
|
||||
|
||||
(define-typed-syntax if
|
||||
[(if e_tst e1 e2)
|
||||
#:with τ-expected (get-expected-type stx)
|
||||
; #:with e_tst- (⇑ e_tst as Bool)
|
||||
#:with [e_tst- _] (infer+erase #'e_tst)
|
||||
#:with e1_ann #'(add-expected e1 τ-expected)
|
||||
#:with e2_ann #'(add-expected e2 τ-expected)
|
||||
#:with (e1- τ1) (infer+erase #'e1_ann)
|
||||
#:with (e2- τ2) (infer+erase #'e2_ann)
|
||||
#:with τ-out ((current-join) #'τ1 #'τ2)
|
||||
(⊢ (if- e_tst- e1- e2-) : τ-out)])
|
||||
(⊢ (if- e_tst- e1- e2-) : (⊔ τ1 τ2))])
|
||||
|
||||
(define-base-type Unit)
|
||||
(define-primop void : (→ Unit))
|
||||
|
|
@ -86,8 +94,7 @@
|
|||
[(ann e : ascribed-τ:type)
|
||||
#:with (e- τ) (infer+erase #'(add-expected e ascribed-τ.norm))
|
||||
#:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
|
||||
(format "~a does not have type ~a\n"
|
||||
(syntax->datum #'e) (syntax->datum #'ascribed-τ))
|
||||
(typecheck-fail-msg/1 #'ascribed-τ.norm #'τ #'e)
|
||||
(⊢ e- : ascribed-τ)])
|
||||
|
||||
(define-typed-syntax let
|
||||
|
|
@ -96,9 +103,8 @@
|
|||
#:with ((e- τ) ...) (infers+erase #'(e ...))
|
||||
#:with ((x- ...) e_body- τ_body) (infer/ctx+erase #'([x τ] ...) #'(add-expected e_body τ-expected))
|
||||
#:fail-unless (or (not (syntax-e #'τ-expected)) ; no expected type
|
||||
(typecheck? #'τ_body ((current-type-eval) #'τ-expected)))
|
||||
(format "let body has type ~a, which does not match expected type ~a"
|
||||
(type->str #'τ_body) (type->str #'τ-expected))
|
||||
(typecheck? #'τ_body ((current-type-eval) #'τ-expected)))
|
||||
(typecheck-fail-msg/1 #'τ-expected #'τ_body #'e_body)
|
||||
(⊢ (let- ([x- e-] ...) e_body-) : τ_body)])
|
||||
|
||||
; dont need to manually transfer expected type
|
||||
|
|
@ -118,17 +124,7 @@
|
|||
#:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
|
||||
(infers/ctx+erase #'(b ...) #'((add-expected e b.type) ... e_body))
|
||||
#:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
|
||||
(type-error #:src stx
|
||||
#:msg (string-append
|
||||
"letrec: type check fail, args have wrong type:\n"
|
||||
(string-join
|
||||
(stx-map
|
||||
(λ (e τ τ-expect)
|
||||
(format
|
||||
"~a has type ~a, expected ~a"
|
||||
(syntax->datum e) (type->str τ) (type->str τ-expect)))
|
||||
#'(e ...) #'(τ ...) #'(b.type ...))
|
||||
"\n")))
|
||||
(⊢ (letrec- ([x- e-] ...) e_body-) : τ_body)])
|
||||
(typecheck-fail-msg/multi #'(b.type ...) #'(τ ...) #'(e ...))
|
||||
(⊢ (letrec- ([x- e-] ...) e_body-) : τ_body)])
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -116,9 +116,14 @@
|
|||
|
||||
(define (raise-app-poly-infer-error stx expected-tys given-tys e_fn)
|
||||
(type-error #:src stx
|
||||
#:msg (mk-app-err-msg stx #:expected expected-tys #:given given-tys
|
||||
#:note (format "Could not infer instantiation of polymorphic function ~a."
|
||||
(syntax->datum (get-orig e_fn))))))
|
||||
#:msg (format
|
||||
(string-append
|
||||
"Could not infer instantiation of polymorphic function ~s.\n"
|
||||
" expected: ~a\n"
|
||||
" given: ~a")
|
||||
(syntax->datum (get-orig e_fn))
|
||||
(string-join (stx-map type->str expected-tys) ", ")
|
||||
(string-join (stx-map type->str given-tys) ", "))))
|
||||
|
||||
;; covariant-Xs? : Type -> Bool
|
||||
;; Takes a possibly polymorphic type, and returns true if all of the
|
||||
|
|
@ -459,14 +464,13 @@
|
|||
#:when (stx-null? #'(τ ...))
|
||||
#:with τ-expected (syntax-property #'C 'expected-type)
|
||||
#:fail-unless (syntax-e #'τ-expected)
|
||||
(raise
|
||||
(exn:fail:type:infer
|
||||
(string-append
|
||||
(format "TYPE-ERROR: ~a (~a:~a): "
|
||||
(syntax-source stx) (syntax-line stx) (syntax-column stx))
|
||||
(format "cannot infer type of ~a; add annotations"
|
||||
(syntax->datum #'C)))
|
||||
(current-continuation-marks)))
|
||||
(raise
|
||||
(exn:fail:type:infer
|
||||
(format "~a (~a:~a): ~a: ~a"
|
||||
(syntax-source stx) (syntax-line stx) (syntax-column stx)
|
||||
(syntax-e #'C)
|
||||
(no-expected-type-fail-msg))
|
||||
(current-continuation-marks)))
|
||||
#:with (NameExpander τ-expected-arg (... ...)) ((current-type-eval) #'τ-expected)
|
||||
#'(C {τ-expected-arg (... ...)})]
|
||||
[_:id (⊢ StructName (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))] ; HO fn
|
||||
|
|
@ -483,9 +487,7 @@
|
|||
(infer+erase (set-stx-prop/preserved e 'expected-type τ_e)))
|
||||
#'(e_arg ...) #'(τ_in.norm (... ...)))
|
||||
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
|
||||
(mk-app-err-msg (syntax/loc stx (#%app C e_arg ...))
|
||||
#:expected #'(τ_in.norm (... ...)) #:given #'(τ_arg ...)
|
||||
#:name (format "constructor ~a" 'Cons))
|
||||
(typecheck-fail-msg/multi #'(τ_in.norm (... ...)) #'(τ_arg ...) #'(e_arg ...))
|
||||
(⊢ (StructName e_arg- ...) : (Name τ_X (... ...)))]
|
||||
[(C . args) ; no type annotations, must infer instantiation
|
||||
#:with StructName/ty
|
||||
|
|
@ -834,19 +836,18 @@
|
|||
|
||||
; all λs have type (?∀ (X ...) (→ τ_in ... τ_out))
|
||||
(define-typed-syntax λ
|
||||
[(λ (x:id ...+) body)
|
||||
[(λ (x:id ...) body)
|
||||
#:with (~?∀ Xs expected) (get-expected-type stx)
|
||||
#:do [(unless (→? #'expected)
|
||||
(type-error #:src stx #:msg "λ parameters must have type annotations"))]
|
||||
#:fail-unless (→? #'expected)
|
||||
(no-expected-type-fail-msg)
|
||||
#:with (~ext-stlc:→ arg-ty ... body-ty) #'expected
|
||||
#:do [(unless (stx-length=? #'[x ...] #'[arg-ty ...])
|
||||
(type-error #:src stx #:msg
|
||||
(format "expected a function of ~a arguments, got one with ~a arguments"
|
||||
(stx-length #'[arg-ty ...] #'[x ...]))))]
|
||||
#`(?Λ Xs (ext-stlc:λ ([x : arg-ty] ...) #,(add-expected-ty #'body #'body-ty)))]
|
||||
[(λ args body)
|
||||
#:fail-unless (stx-length=? #'[x ...] #'[arg-ty ...])
|
||||
(format "expected a function of ~a arguments, got one with ~a arguments"
|
||||
(stx-length #'[arg-ty ...]) (stx-length #'[x ...]))
|
||||
#`(?Λ Xs (ext-stlc:λ ([x : arg-ty] ...) (add-expected body body-ty)))]
|
||||
[(λ (~and args ([_ (~datum :) ty] ...)) body)
|
||||
#:with (~?∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx)
|
||||
#`(?Λ () (ext-stlc:λ args #,(add-expected-ty #'body #'body-ty)))]
|
||||
#`(?Λ () (ext-stlc:λ args (add-expected body body-ty)))]
|
||||
[(λ (~and x+tys ([_ (~datum :) ty] ...)) . body)
|
||||
#:with Xs (compute-tyvars #'(ty ...))
|
||||
;; TODO is there a way to have λs that refer to ids defined after them?
|
||||
|
|
@ -856,64 +857,32 @@
|
|||
;; #%app --------------------------------------------------
|
||||
(define-typed-syntax mlish:#%app #:export-as #%app
|
||||
[(_ e_fn . e_args)
|
||||
;; ) compute fn type (ie ∀ and →)
|
||||
;; compute fn type (ie ∀ and →)
|
||||
#:with [e_fn- (~?∀ Xs (~ext-stlc:→ . tyX_args))] (infer+erase #'e_fn)
|
||||
(cond
|
||||
[(stx-null? #'Xs)
|
||||
(syntax-parse #'(e_args tyX_args)
|
||||
[((e_arg ...) (τ_inX ... _))
|
||||
#:fail-unless (stx-length=? #'(e_arg ...) #'(τ_inX ...))
|
||||
(mk-app-err-msg stx #:expected #'(τ_inX ...)
|
||||
#:note "Wrong number of arguments.")
|
||||
#:with e_fn/ty (⊢ e_fn- : (ext-stlc:→ . tyX_args))
|
||||
#'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
|
||||
[else
|
||||
;; ) solve for type variables Xs
|
||||
(define/with-syntax ((e_arg- ...) Xs* cs) (solve #'Xs #'tyX_args stx))
|
||||
;; ) instantiate polymorphic function type
|
||||
(syntax-parse (inst-types/cs #'Xs* #'cs #'tyX_args)
|
||||
[(τ_in ... τ_out) ; concrete types
|
||||
#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
|
||||
;; ) arity check
|
||||
#:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
|
||||
(mk-app-err-msg stx #:expected #'(τ_in ...)
|
||||
#:note "Wrong number of arguments.")
|
||||
;; ) compute argument types
|
||||
#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
|
||||
;; ) typecheck args
|
||||
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
|
||||
(mk-app-err-msg stx
|
||||
#:given #'(τ_arg ...)
|
||||
#:expected
|
||||
(stx-map
|
||||
(lambda (tyin)
|
||||
(define old-orig (get-orig tyin))
|
||||
(define new-orig
|
||||
(and old-orig
|
||||
(substs
|
||||
(stx-map get-orig (lookup-Xs/keep-unsolved #'Xs* #'cs))
|
||||
#'Xs*
|
||||
old-orig
|
||||
(lambda (x y)
|
||||
(equal? (syntax->datum x) (syntax->datum y))))))
|
||||
(set-stx-prop/preserved tyin 'orig (list new-orig)))
|
||||
#'(τ_in ...)))
|
||||
#:with τ_out* (if (stx-null? #'(unsolved-X ...))
|
||||
#'τ_out
|
||||
(syntax-parse #'τ_out
|
||||
[(~?∀ (Y ...) τ_out)
|
||||
(unless (→? #'τ_out)
|
||||
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
|
||||
(for ([X (in-list (syntax->list #'(unsolved-X ...)))])
|
||||
(unless (covariant-X? X #'τ_out)
|
||||
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)))
|
||||
#'(∀ (unsolved-X ... Y ...) τ_out)]))
|
||||
(⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])])]
|
||||
[(_ e_fn . e_args) ; err case; e_fn is not a function
|
||||
#:with [e_fn- τ_fn] (infer+erase #'e_fn)
|
||||
(type-error #:src stx
|
||||
#:msg (format "Expected expression ~a to have → type, got: ~a"
|
||||
(syntax->datum #'e_fn) (type->str #'τ_fn)))])
|
||||
;; solve for type variables Xs
|
||||
#:with [(e_arg- ...) Xs* cs] (solve #'Xs #'tyX_args stx)
|
||||
;; instantiate polymorphic function type
|
||||
#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
|
||||
#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
|
||||
;; arity check
|
||||
#:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
|
||||
(num-args-fail-msg #'e_fn #'(τ_in ...) #'e_args)
|
||||
;; compute argument types
|
||||
#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
|
||||
;; typecheck args
|
||||
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
|
||||
(typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'e_args)
|
||||
#:with τ_out* (if (stx-null? #'(unsolved-X ...))
|
||||
#'τ_out
|
||||
(syntax-parse #'τ_out
|
||||
[(~?∀ (Y ...) τ_out)
|
||||
(unless (→? #'τ_out)
|
||||
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
|
||||
(for ([X (in-list (syntax->list #'(unsolved-X ...)))])
|
||||
(unless (covariant-X? X #'τ_out)
|
||||
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)))
|
||||
#'(∀ (unsolved-X ... Y ...) τ_out)]))
|
||||
(⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])
|
||||
|
||||
|
||||
;; cond and other conditionals
|
||||
|
|
@ -1107,10 +1076,7 @@
|
|||
#:with [(acc- x- ...) body- ty_body]
|
||||
(infer/ctx+erase #'([acc : ty_init][x : ty] ...) #'body)
|
||||
#:fail-unless (typecheck? #'ty_body #'ty_init)
|
||||
(type-error #:src stx
|
||||
#:msg
|
||||
"for/fold: Type of body and initial accumulator must be the same, given ~a and ~a"
|
||||
#'ty_init #'ty_body)
|
||||
(typecheck-fail-msg/1 #'ty_init #'ty_body #'body)
|
||||
(⊢ (for/fold- ([acc- init-]) ([x- e-] ...) body-) : ty_body)])
|
||||
|
||||
(define-typed-syntax for/hash
|
||||
|
|
|
|||
|
|
@ -13,15 +13,16 @@
|
|||
|
||||
(define-typed-syntax ref
|
||||
[(ref e)
|
||||
#:with (e- τ) (infer+erase #'e)
|
||||
#:with [e- τ] (infer+erase #'e)
|
||||
(⊢ (box- e-) : (Ref τ))])
|
||||
(define-typed-syntax deref
|
||||
[(deref e)
|
||||
#:with (e- (τ)) (⇑ e as Ref)
|
||||
#:with [e- (~Ref τ)] (infer+erase #'e)
|
||||
(⊢ (unbox- e-) : τ)])
|
||||
(define-typed-syntax := #:literals (:=)
|
||||
[(:= e_ref e)
|
||||
#:with (e_ref- (τ1)) (⇑ e_ref as Ref)
|
||||
#:with (e- τ2) (infer+erase #'e)
|
||||
#:when (typecheck? #'τ1 #'τ2)
|
||||
#:with [e_ref- (~Ref τ1)] (infer+erase #'e_ref)
|
||||
#:with [e- τ2] (infer+erase #'e)
|
||||
#:fail-unless (typecheck? #'τ1 #'τ2)
|
||||
(typecheck-fail-msg/1 #'τ1 #'τ2 #'e)
|
||||
(⊢ (set-box!- e_ref- e-) : Unit)])
|
||||
|
|
|
|||
|
|
@ -17,48 +17,43 @@
|
|||
(⊢ null- : (List τi.norm))]
|
||||
; minimal type inference
|
||||
[nil:id #:with expected-τ (get-expected-type #'nil)
|
||||
#:when (syntax-e #'expected-τ) ; 'expected-type property exists (ie, not false)
|
||||
#:with ty_lst (local-expand #'expected-τ 'expression null) ; canonicalize
|
||||
#:fail-unless (List? #'ty_lst)
|
||||
#:fail-unless (syntax-e #'expected-τ) ; 'expected-type property exists (ie, not false)
|
||||
(raise (exn:fail:type:infer
|
||||
(format "~a (~a:~a): nil: ~a"
|
||||
(syntax-source stx) (syntax-line stx) (syntax-column stx)
|
||||
(no-expected-type-fail-msg))
|
||||
(current-continuation-marks)))
|
||||
#:fail-unless (List? #'expected-τ)
|
||||
(raise (exn:fail:type:infer
|
||||
(format "~a (~a:~a): Inferred ~a type for nil, which is not a List."
|
||||
(syntax-source stx) (syntax-line stx) (syntax-column stx)
|
||||
(type->str #'ty_lst))
|
||||
(current-continuation-marks)))
|
||||
#:with (~List τ) #'ty_lst
|
||||
(⊢ null- : (List τ))]
|
||||
[_:id #:fail-when #t
|
||||
(raise (exn:fail:type:infer
|
||||
(format "~a (~a:~a): nil requires type annotation"
|
||||
(syntax-source stx) (syntax-line stx) (syntax-column stx))
|
||||
(current-continuation-marks)))
|
||||
#'(void-)])
|
||||
(⊢ null- : expected-τ)])
|
||||
(define-typed-syntax cons
|
||||
[(cons e1 e2)
|
||||
#:with [e1- τ1] (infer+erase #'e1)
|
||||
; #:with e2ann (add-expected-type #'e2 #'(List τ1))
|
||||
#:with (e2- (τ2)) (⇑ (add-expected e2 (List τ1)) as List)
|
||||
#:fail-unless (typecheck? #'τ1 #'τ2)
|
||||
(format "trying to cons expression ~a with type ~a to list ~a with type ~a\n"
|
||||
(syntax->datum #'e1) (type->str #'τ1)
|
||||
(syntax->datum #'e2) (type->str #'(List τ2)))
|
||||
#:with [e1- τ_e1] (infer+erase #'e1)
|
||||
#:with τ_list ((current-type-eval) #'(List τ_e1))
|
||||
#:with [e2- τ_e2] (infer+erase (add-expected-ty #'e2 #'τ_list))
|
||||
#:fail-unless (typecheck? #'τ_e2 #'τ_list)
|
||||
(typecheck-fail-msg/1 #'τ_list #'τ_e2 #'e2)
|
||||
;; propagate up inferred types of variables
|
||||
#:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e1- e2-))))
|
||||
#:with result-cons (add-env #'(cons- e1- e2-) #'env)
|
||||
(⊢ result-cons : (List τ1))])
|
||||
(⊢ result-cons : τ_list)])
|
||||
(define-typed-syntax isnil
|
||||
[(isnil e)
|
||||
#:with (e- _) (⇑ e as List)
|
||||
#:with [e- (~List _)] (infer+erase #'e)
|
||||
(⊢ (null?- e-) : Bool)])
|
||||
(define-typed-syntax head
|
||||
[(head e)
|
||||
#:with (e- (τ)) (⇑ e as List)
|
||||
#:with [e- (~List τ)] (infer+erase #'e)
|
||||
(⊢ (car- e-) : τ)])
|
||||
(define-typed-syntax tail
|
||||
[(tail e)
|
||||
#:with (e- τ-lst) (infer+erase #'e)
|
||||
#:when (List? #'τ-lst)
|
||||
(⊢ (cdr- e-) : τ-lst)])
|
||||
#:with [e- τ_lst] (infer+erase #'e)
|
||||
#:when (List? #'τ_lst)
|
||||
(⊢ (cdr- e-) : τ_lst)])
|
||||
(define-typed-syntax list
|
||||
[(list) #'nil]
|
||||
[(_ x . rst) ; has expected type
|
||||
|
|
|
|||
|
|
@ -53,14 +53,10 @@
|
|||
#:with tyds (get-deref-effects #'ty_fn)
|
||||
#:with (~→ τ_in ... τ_out) #'ty_fn
|
||||
#:with ([e_arg- τ_arg ns as ds] ...) (infers+erase/eff #'(e ...))
|
||||
; #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
|
||||
#:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...))
|
||||
(mk-app-err-msg stx #:expected #'(τ_in ...)
|
||||
#:given #'(τ_arg ...)
|
||||
#:note "Wrong number of arguments.")
|
||||
(num-args-fail-msg #'efn #'(τ_in ...) #'(e ...))
|
||||
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
|
||||
(mk-app-err-msg stx #:expected #'(τ_in ...)
|
||||
#:given #'(τ_arg ...))
|
||||
(typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'(e ...))
|
||||
(assign-type/eff #'(#%app- e_fn- e_arg- ...) #'τ_out
|
||||
(stx-flatten #'(fns tyns . (ns ...)))
|
||||
(stx-flatten #'(fas tyas . (as ...)))
|
||||
|
|
@ -108,20 +104,20 @@
|
|||
|
||||
(define-typed-syntax ref
|
||||
[(ref e)
|
||||
#:with (e- τ ns as ds) (infer+erase/eff #'e)
|
||||
#:with [e- τ ns as ds] (infer+erase/eff #'e)
|
||||
(assign-type/eff #'(box- e-) #'(Ref τ)
|
||||
(cons (syntax-position stx) #'ns) #'as #'ds)])
|
||||
(define-typed-syntax deref
|
||||
[(deref e)
|
||||
#:with (e- (~Ref ty) ns as ds) (infer+erase/eff #'e)
|
||||
#:with [e- (~Ref ty) ns as ds] (infer+erase/eff #'e)
|
||||
(assign-type/eff #'(unbox- e-) #'ty
|
||||
#'ns #'as (cons (syntax-position stx) #'ds))])
|
||||
(define-typed-syntax := #:literals (:=)
|
||||
[(:= e_ref e)
|
||||
;#:with (e_ref- (τ1)) (⇑ e_ref as Ref)
|
||||
#:with [e_ref- (~Ref ty1) ns1 as1 ds1] (infer+erase/eff #'e_ref)
|
||||
#:with [e- ty2 ns2 as2 ds2] (infer+erase/eff #'e)
|
||||
#:when (typecheck? #'ty1 #'ty2)
|
||||
#:fail-unless (typecheck? #'ty1 #'ty2)
|
||||
(typecheck-fail-msg/1 #'ty1 #'ty2 #'e)
|
||||
(assign-type/eff #'(set-box!- e_ref- e-) #'Unit
|
||||
(stx-append #'ns1 #'ns2)
|
||||
(cons (syntax-position stx) (stx-append #'as1 #'as2))
|
||||
|
|
|
|||
|
|
@ -61,6 +61,20 @@
|
|||
#:src #'any
|
||||
#:msg "Expected × type, got: ~a" #'any))))]))))
|
||||
|
||||
(begin-for-syntax
|
||||
(define (stx-assoc-ref stx-lst lookup-k #:else [fail (λ () #f)])
|
||||
(define match_res (stx-assoc lookup-k stx-lst))
|
||||
(cond [match_res
|
||||
(stx-cadr match_res)]
|
||||
[else
|
||||
(fail)]))
|
||||
(define (×-ref ×-type l)
|
||||
(syntax-parse ×-type
|
||||
[(~× [l_τ : τ] ...)
|
||||
(define res
|
||||
(stx-assoc-ref #'([l_τ τ] ...) l #:else (λ () (error 'X-ref "bad!"))))
|
||||
(add-orig res (get-orig res))])))
|
||||
|
||||
;; records
|
||||
(define-typed-syntax tup #:datum-literals (=)
|
||||
[(tup [l:id = e] ...)
|
||||
|
|
@ -68,9 +82,12 @@
|
|||
(⊢ (list- (list- 'l e-) ...) : (× [l : τ] ...))])
|
||||
(define-typed-syntax proj #:literals (quote)
|
||||
[(proj e_rec l:id)
|
||||
#:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
|
||||
#:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
|
||||
(⊢ (cadr- (assoc- 'l e_rec-)) : τ_match)])
|
||||
#:with [e_rec- τ_e] (infer+erase #'e_rec)
|
||||
#:fail-unless (×? #'τ_e)
|
||||
(format "Expected expression ~s to have × type, got: ~a"
|
||||
(syntax->datum #'e_rec) (type->str #'τ_e))
|
||||
#:with τ_l (×-ref #'τ_e #'l)
|
||||
(⊢ (cadr- (assoc- 'l e_rec-)) : τ_l)])
|
||||
|
||||
(define-type-constructor ∨/internal #:arity >= 0)
|
||||
|
||||
|
|
@ -107,26 +124,36 @@
|
|||
#:msg "Expected ∨ type, got: ~a" #'any))))
|
||||
~!)])))) ; dont backtrack here
|
||||
|
||||
(begin-for-syntax
|
||||
(define (∨-ref ∨-type l #:else [fail (λ () #f)])
|
||||
(syntax-parse ∨-type
|
||||
[(~∨ [l_τ : τ] ...)
|
||||
(define res
|
||||
(stx-assoc-ref #'([l_τ τ] ...) l #:else fail))
|
||||
(add-orig res (get-orig res))])))
|
||||
|
||||
(define-typed-syntax var #:datum-literals (as =)
|
||||
[(var l:id = e as τ:type)
|
||||
#:with (~∨* [l_τ : τ_l] ...) #'τ.norm
|
||||
#:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
|
||||
#:fail-unless (syntax-e #'match_res)
|
||||
(format "~a field does not exist" (syntax->datum #'l))
|
||||
#:with (_ τ_match) #'match_res
|
||||
#:with (e- τ_e) (infer+erase #'e)
|
||||
#:when (typecheck? #'τ_e #'τ_match)
|
||||
(⊢ (list- 'l e) : τ)])
|
||||
#:fail-unless (∨? #'τ.norm)
|
||||
(format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ.norm))
|
||||
#:with τ_match
|
||||
(∨-ref #'τ.norm #'l #:else
|
||||
(λ () (raise-syntax-error #f
|
||||
(format "~a field does not exist" (syntax->datum #'l))
|
||||
stx)))
|
||||
#:with [e- τ_e] (infer+erase #'e)
|
||||
#:fail-unless (typecheck? #'τ_e #'τ_match)
|
||||
(typecheck-fail-msg/1 #'τ_match #'τ_e #'e)
|
||||
(⊢ (list- 'l e) : τ.norm)])
|
||||
(define-typed-syntax case
|
||||
#:datum-literals (of =>)
|
||||
[(case e [l:id x:id => e_l] ...)
|
||||
#:fail-when (null? (syntax->list #'(l ...))) "no clauses"
|
||||
#:with (e- ([l_x τ_x] ...)) (⇑ e as ∨)
|
||||
#:with [e- (~∨* [l_x : τ_x] ...)] (infer+erase #'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/ctx+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
|
||||
#:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
|
||||
(⊢ (let- ([l_e (car- e-)])
|
||||
(cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))
|
||||
: #,(stx-car #'(τ_el ...)))])
|
||||
: (⊔ τ_el ...))])
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@
|
|||
(⊢ (list- e- ...) : (× τ ...))])
|
||||
(define-typed-syntax proj
|
||||
[(proj e_tup n:nat)
|
||||
#:with [e_tup- τs_tup] (⇑ e_tup as ×)
|
||||
#:with [e_tup- (~× . τs_tup)] (infer+erase #'e_tup)
|
||||
#:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
|
||||
(⊢ (list-ref- e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))])
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
#lang s-exp macrotypes/typecheck
|
||||
(provide (for-syntax current-type=? types=?))
|
||||
(provide (for-syntax mk-app-err-msg))
|
||||
|
||||
(require (for-syntax racket/list))
|
||||
|
||||
|
|
@ -81,50 +80,12 @@
|
|||
#:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
|
||||
(⊢ (λ- xs- e-) : (→ bvs.type ... τ_res))])
|
||||
|
||||
(define-for-syntax (mk-app-err-msg stx #:expected [expected-τs #'()]
|
||||
#:given [given-τs #'()]
|
||||
#:note [note ""]
|
||||
#:name [name #f])
|
||||
(syntax-parse stx
|
||||
#;[(app . rst)
|
||||
#:when (not (equal? '#%app (syntax->datum #'app)))
|
||||
(mk-app-err-msg (syntax/loc stx (#%app app . rst))
|
||||
#:expected expected-τs
|
||||
#:given given-τs
|
||||
#:note note
|
||||
#:name name)]
|
||||
[(app e_fn e_arg ...)
|
||||
(define fn-name
|
||||
(if name name
|
||||
(format "function ~a"
|
||||
(syntax->datum (or (get-orig #'e_fn) #'e_fn)))))
|
||||
(string-append
|
||||
(format "~a (~a:~a):\nType error applying "
|
||||
(syntax-source stx) (syntax-line stx) (syntax-column stx))
|
||||
fn-name ". " note "\n"
|
||||
(format " Expected: ~a argument(s) with type(s): " (stx-length expected-τs))
|
||||
(string-join (stx-map type->str expected-τs) ", " #:after-last "\n")
|
||||
" Given:\n"
|
||||
(string-join
|
||||
(map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
|
||||
(syntax->datum #'(e_arg ...))
|
||||
(if (stx-length=? #'(e_arg ...) given-τs)
|
||||
(stx-map type->str given-τs)
|
||||
(stx-map (lambda (e) "?") #'(e_arg ...))))
|
||||
"\n")
|
||||
"\n")]))
|
||||
|
||||
(define-typed-syntax #%app #:literals (#%app)
|
||||
[(#%app e_fn e_arg ...)
|
||||
#:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
|
||||
#:with [e_fn- (~→ τ_in ... τ_out)] (infer+erase #'e_fn)
|
||||
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
|
||||
#:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...))
|
||||
(type-error #:src stx
|
||||
#:msg (mk-app-err-msg stx #:expected #'(τ_in ...)
|
||||
#:given #'(τ_arg ...)
|
||||
#:note "Wrong number of arguments."))
|
||||
(num-args-fail-msg #'e_fn #'(τ_in ...) #'(e_arg ...))
|
||||
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
|
||||
(type-error #:src stx
|
||||
#:msg (mk-app-err-msg stx #:expected #'(τ_in ...)
|
||||
#:given #'(τ_arg ...)))
|
||||
(⊢ (#%app- e_fn- e_arg- ...) : τ_out)])
|
||||
(typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'(e_arg ...))
|
||||
(⊢ (#%app- e_fn- e_arg- ...) : τ_out)])
|
||||
|
|
|
|||
171
macrotypes/examples/tests/ext-stlc-tests.rkt
Normal file
171
macrotypes/examples/tests/ext-stlc-tests.rkt
Normal file
|
|
@ -0,0 +1,171 @@
|
|||
#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)
|
||||
#:with-msg "expected: +Unit\n *given: +Int\n *expressions: 2")
|
||||
(typecheck-fail
|
||||
((λ ([x : Unit]) x) void)
|
||||
#:with-msg "expected: +Unit\n *given: +\\(→ Unit\\)\n *expressions: void")
|
||||
|
||||
(check-type ((λ ([x : Unit]) x) (void)) : Unit)
|
||||
|
||||
;; begin
|
||||
(check-type (begin 1) : Int)
|
||||
|
||||
(typecheck-fail (begin) #:with-msg "expected more terms")
|
||||
;; 2016-03-06: begin terms dont need to be Unit
|
||||
(check-type (begin 1 2 3) : Int)
|
||||
#;(typecheck-fail
|
||||
(begin 1 2 3)
|
||||
#:with-msg "Expected expression 1 to have Unit type, got: Int")
|
||||
|
||||
(check-type (begin (void) 1) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
|
||||
(check-type ((λ ([x : Int]) (begin x)) 1) : Int)
|
||||
(check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int)
|
||||
(check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int)
|
||||
(check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int)
|
||||
|
||||
;;ascription
|
||||
(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: type mismatch: expected Bool, given Int\n *expression: 1")
|
||||
;ann errs
|
||||
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
|
||||
(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann Int : Int)
|
||||
#:with-msg "ann: type mismatch: expected Int, given #%type\n *expression: Int")
|
||||
|
||||
; let
|
||||
(check-type (let () (+ 1 1)) : Int ⇒ 2)
|
||||
(check-type (let ([x 10]) (+ 1 2)) : Int)
|
||||
(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
|
||||
(typecheck-fail
|
||||
(let ([x #f]) (+ x 1))
|
||||
#:with-msg "expected: +Int, Int\n *given: +Bool, Int\n *expressions: x, 1")
|
||||
(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)
|
||||
#:with-msg "expected: +Int, Int\n *given: +Bool, Int\n *expressions: x, 1")
|
||||
|
||||
; letrec
|
||||
(typecheck-fail
|
||||
(letrec ([(x : Int) #f] [(y : Int) 1]) y)
|
||||
#:with-msg
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1")
|
||||
(typecheck-fail
|
||||
(letrec ([(y : Int) 1] [(x : Int) #f]) x)
|
||||
#:with-msg
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f")
|
||||
(typecheck-fail
|
||||
(ann (letrec ([(x : Int) #f] [(y : Int) 1]) y) : Int)
|
||||
#:with-msg
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1")
|
||||
(typecheck-fail
|
||||
(ann (letrec ([(y : Int) 1] [(x : Int) #f]) x) : Int)
|
||||
#:with-msg
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f")
|
||||
|
||||
(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)
|
||||
|
||||
;; check some more err msgs
|
||||
(typecheck-fail
|
||||
(and "1" #f)
|
||||
#:with-msg
|
||||
"and: type mismatch: expected Bool, given String\n *expression: \"1\"")
|
||||
(typecheck-fail
|
||||
(and #t "2")
|
||||
#:with-msg
|
||||
"and: type mismatch: expected Bool, given String\n *expression: \"2\"")
|
||||
(typecheck-fail
|
||||
(or "1" #f)
|
||||
#:with-msg
|
||||
"or: type mismatch\n *expected: +Bool, Bool\n *given: +String, Bool\n *expressions: \"1\", #f")
|
||||
(typecheck-fail
|
||||
(or #t "2")
|
||||
#:with-msg
|
||||
"or: type mismatch\n *expected: +Bool, Bool\n *given: +Bool, String\n *expressions: #t, \"2\"")
|
||||
;; 2016-03-10: change if to work with non-false vals
|
||||
(check-type (if "true" 1 2) : Int -> 1)
|
||||
(typecheck-fail
|
||||
(if #t 1 "2")
|
||||
#:with-msg
|
||||
"branches have incompatible types: Int and String")
|
||||
|
||||
;; 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)
|
||||
#:with-msg "expected: +Bool\n *given: +Int\n *expressions: 1")
|
||||
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
|
||||
(typecheck-fail
|
||||
(λ ([f : Int]) (f 1 2))
|
||||
#:with-msg
|
||||
"Expected → type, 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))
|
||||
#:with-msg (string-append "expected: +Int, Int\n *given: +Int, \\(→ Int Int\\)\n"
|
||||
" *expressions: 1, \\(λ \\(\\(x : Int\\)\\) x\\)"))
|
||||
(typecheck-fail
|
||||
(λ ([x : (→ Int Int)]) (+ x x))
|
||||
#:with-msg "expected: +Int, Int\n *given: +\\(→ Int Int\\), \\(→ Int Int\\)\n *expressions: x, x")
|
||||
(typecheck-fail
|
||||
((λ ([x : Int] [y : Int]) y) 1)
|
||||
#:with-msg "wrong number of arguments: expected 2, given 1")
|
||||
|
||||
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
|
||||
|
||||
|
|
@ -69,7 +69,7 @@
|
|||
; list abbrv
|
||||
(check-type (list 1 2 3) : (List Int))
|
||||
(typecheck-fail (list 1 "3")
|
||||
#:with-msg "cons expression.+with type Int to list.+with type \\(List String\\)")
|
||||
#:with-msg "expected \\(List Int\\), given \\(List String\\)\n *expression: \\(list \"3\"\\)")
|
||||
|
||||
|
||||
(define {X Y} (map [f : (→ X Y)] [lst : (List X)] → (List Y))
|
||||
|
|
@ -241,12 +241,12 @@
|
|||
;;ascription
|
||||
(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")
|
||||
(typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
|
||||
;ann errs
|
||||
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
|
||||
(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann Int : Int) #:with-msg "does not have type Int")
|
||||
(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int")
|
||||
|
||||
; let
|
||||
(check-type (let () (+ 1 1)) : Int ⇒ 2)
|
||||
|
|
@ -269,11 +269,11 @@
|
|||
(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")
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1")
|
||||
(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")
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f")
|
||||
|
||||
(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
|
||||
|
||||
|
|
@ -301,19 +301,19 @@
|
|||
;; check some more err msgs
|
||||
(typecheck-fail
|
||||
(and "1" #f)
|
||||
#:with-msg "Expected expression \"1\" to have Bool type, got: String")
|
||||
#:with-msg "and: type mismatch: expected Bool, given String\n *expression: \"1\"")
|
||||
(typecheck-fail
|
||||
(and #t "2")
|
||||
#:with-msg
|
||||
"Expected expression \"2\" to have Bool type, got: String")
|
||||
"and: type mismatch: expected Bool, given String\n *expression: \"2\"")
|
||||
(typecheck-fail
|
||||
(or "1" #f)
|
||||
#:with-msg
|
||||
"Expected expression \"1\" to have Bool type, got: String")
|
||||
"or: type mismatch\n expected: +Bool, Bool\n *given: +String, Bool\n *expressions: \"1\", #f")
|
||||
(typecheck-fail
|
||||
(or #t "2")
|
||||
#:with-msg
|
||||
"Expected expression \"2\" to have Bool type, got: String")
|
||||
"or: type mismatch\n expected: +Bool, Bool\n *given: +Bool, String\n *expressions: #t, \"2\"")
|
||||
;; 2016-03-10: change if to work with non-false vals
|
||||
(check-type (if "true" 1 2) : Int -> 1)
|
||||
(typecheck-fail
|
||||
|
|
|
|||
788
macrotypes/examples/tests/mlish-tests.rkt
Normal file
788
macrotypes/examples/tests/mlish-tests.rkt
Normal file
|
|
@ -0,0 +1,788 @@
|
|||
#lang s-exp "../mlish.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; match on tups
|
||||
(check-type
|
||||
(match (tup 1 2) with
|
||||
[x y -> (+ x y)])
|
||||
: Int -> 3)
|
||||
|
||||
;; tests more or less copied from infer-tests.rkt ------------------------------
|
||||
(typecheck-fail (λ (x) x) #:with-msg "λ: no expected type, add annotations")
|
||||
|
||||
;; top-level defines
|
||||
(define (f [x : Int] → Int) x)
|
||||
(typecheck-fail (f 1 2) #:with-msg "f: wrong number of arguments: expected 1, given 2")
|
||||
(check-type f : (→ Int Int))
|
||||
(check-type (f 1) : Int ⇒ 1)
|
||||
(typecheck-fail (f (λ ([x : Int]) x)))
|
||||
|
||||
(define (g [x : X] → X) x)
|
||||
(check-type g : (→/test X X))
|
||||
|
||||
;; (inferred) polymorpic instantiation
|
||||
(check-type (g 1) : Int ⇒ 1)
|
||||
(check-type (g #f) : Bool ⇒ #f) ; different instantiation
|
||||
(check-type (g add1) : (→ Int Int))
|
||||
(check-type (g +) : (→ Int Int Int))
|
||||
|
||||
;; function polymorphic in list element
|
||||
(define-type (List X)
|
||||
Nil
|
||||
(Cons X (List X)))
|
||||
|
||||
;; arity err
|
||||
(typecheck-fail (Cons 1) #:with-msg "Cons: wrong number of arguments: expected 2, given 1")
|
||||
|
||||
;; type err
|
||||
(typecheck-fail (Cons 1 1)
|
||||
#:with-msg "expected: \\(List Int\\)\n *given: Int")
|
||||
|
||||
(typecheck-fail
|
||||
(match (Cons 1 Nil) with
|
||||
[Nil -> 1])
|
||||
#:with-msg "match: clauses not exhaustive; missing: Cons")
|
||||
(typecheck-fail
|
||||
(match (Cons 1 Nil) with
|
||||
[Cons x xs -> 1])
|
||||
#:with-msg "match: clauses not exhaustive; missing: Nil")
|
||||
|
||||
(define (g2 [lst : (List Y)] → (List Y)) lst)
|
||||
(check-type g2 : (→/test (List Y) (List Y)))
|
||||
(typecheck-fail (g2 1)
|
||||
#:with-msg
|
||||
"expected: \\(List Y\\)\n *given: Int")
|
||||
|
||||
;; todo? allow polymorphic nil?
|
||||
(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
|
||||
(check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool}))
|
||||
(check-type (g2 (Nil {(List Int)})) : (List (List Int)) ⇒ (Nil {(List Int)}))
|
||||
(check-type (g2 (Nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (Nil {(List (→ Int Int))}))
|
||||
;; annotations unneeded: same as tests above, but without annotations
|
||||
(check-type (g2 Nil) : (List Int) ⇒ Nil)
|
||||
(check-type (g2 Nil) : (List Bool) ⇒ Nil)
|
||||
(check-type (g2 Nil) : (List (List Int)) ⇒ Nil)
|
||||
(check-type (g2 Nil) : (List (→ Int Int)) ⇒ Nil)
|
||||
|
||||
(check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
|
||||
(check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
|
||||
|
||||
;; mlish cant type this fn (ie, incomplete cases on variant --- what to put for Nil case?)
|
||||
;(define (g3 [lst : (List X)] → X) (hd lst))
|
||||
;(check-type g3 : (→ {X} (List X) X))
|
||||
;(check-type g3 : (→ {A} (List A) A))
|
||||
;(check-not-type g3 : (→ {A B} (List A) B))
|
||||
;(typecheck-fail (g3) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg
|
||||
;(check-type (g3 (nil {Int})) : Int) ; runtime fail
|
||||
;(check-type (g3 (nil {Bool})) : Bool) ; runtime fail
|
||||
;(check-type (g3 (cons 1 nil)) : Int ⇒ 1)
|
||||
;(check-type (g3 (cons "1" nil)) : String ⇒ "1")
|
||||
|
||||
;; recursive fn
|
||||
(define (recf [x : Int] → Int) (recf x))
|
||||
(check-type recf : (→ Int Int))
|
||||
|
||||
(define (countdown [x : Int] → Int)
|
||||
(if (zero? x)
|
||||
0
|
||||
(countdown (sub1 x))))
|
||||
(check-type (countdown 0) : Int ⇒ 0)
|
||||
(check-type (countdown 10) : Int ⇒ 0)
|
||||
(typecheck-fail (countdown "10") #:with-msg "expected: Int\n *given: String")
|
||||
|
||||
;; list fns ----------
|
||||
|
||||
; map: tests whether match and define properly propagate 'expected-type
|
||||
(define (map [f : (→ X Y)] [lst : (List X)] → (List Y))
|
||||
(match lst with
|
||||
[Nil -> Nil]
|
||||
[Cons x xs -> (Cons (f x) (map f xs))]))
|
||||
(check-type map : (→/test (→ X Y) (List X) (List Y)))
|
||||
(check-type map : (→/test {Y X} (→ Y X) (List Y) (List X)))
|
||||
(check-type map : (→/test (→ A B) (List A) (List B)))
|
||||
(check-not-type map : (→/test (→ A B) (List B) (List A)))
|
||||
(check-not-type map : (→/test (→ X X) (List X) (List X))) ; only 1 bound tyvar
|
||||
|
||||
; nil without annotation; tests fn-first, left-to-right arg inference
|
||||
; does work yet, need to add left-to-right inference in #%app
|
||||
(check-type (map add1 Nil) : (List Int) ⇒ Nil)
|
||||
(check-type (map add1 (Cons 1 (Cons 2 (Cons 3 Nil))))
|
||||
: (List Int) ⇒ (Cons 2 (Cons 3 (Cons 4 Nil))))
|
||||
(typecheck-fail (map add1 (Cons "1" Nil))
|
||||
#:with-msg "expected: Int\n *given: String")
|
||||
(check-type (map (λ ([x : Int]) (+ x 2)) (Cons 1 (Cons 2 (Cons 3 Nil))))
|
||||
: (List Int) ⇒ (Cons 3 (Cons 4 (Cons 5 Nil))))
|
||||
;; ; doesnt work yet: all lambdas need annotations
|
||||
;; (check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
|
||||
|
||||
(define (filter [p? : (→ X Bool)] [lst : (List X)] → (List X))
|
||||
(match lst with
|
||||
[Nil -> Nil]
|
||||
[Cons x xs -> (if (p? x)
|
||||
(Cons x (filter p? xs))
|
||||
(filter p? xs))]))
|
||||
(define (filter/guard [p? : (→ X Bool)] [lst : (List X)] → (List X))
|
||||
(match lst with
|
||||
[Nil -> Nil]
|
||||
[Cons x xs #:when (p? x) -> (Cons x (filter p? xs))]
|
||||
[Cons x xs -> (filter p? xs)]))
|
||||
(check-type (filter zero? Nil) : (List Int) ⇒ Nil)
|
||||
(check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil))))
|
||||
: (List Int) ⇒ Nil)
|
||||
(check-type (filter zero? (Cons 0 (Cons 1 (Cons 2 Nil))))
|
||||
: (List Int) ⇒ (Cons 0 Nil))
|
||||
(check-type (filter (λ (x) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil))))
|
||||
: (List Int) ⇒ (Cons 1 (Cons 2 Nil)))
|
||||
(check-type (filter/guard zero? Nil) : (List Int) ⇒ Nil)
|
||||
(check-type (filter/guard zero? (Cons 1 (Cons 2 (Cons 3 Nil))))
|
||||
: (List Int) ⇒ Nil)
|
||||
(check-type (filter/guard zero? (Cons 0 (Cons 1 (Cons 2 Nil))))
|
||||
: (List Int) ⇒ (Cons 0 Nil))
|
||||
(check-type
|
||||
(filter/guard (λ (x) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil))))
|
||||
: (List Int) ⇒ (Cons 1 (Cons 2 Nil)))
|
||||
; doesnt work yet: all lambdas need annotations
|
||||
;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2))
|
||||
|
||||
(define (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y)
|
||||
(match lst with
|
||||
[Nil -> base]
|
||||
[Cons x xs -> (f x (foldr f base xs))]))
|
||||
(define (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y)
|
||||
(match lst with
|
||||
[Nil -> acc]
|
||||
[Cons x xs -> (foldr f (f x acc) xs)]))
|
||||
|
||||
(define (all? [p? : (→ X Bool)] [lst : (List X)] → Bool)
|
||||
(match lst with
|
||||
[Nil -> #t]
|
||||
[Cons x xs #:when (p? x) -> (all? p? xs)]
|
||||
[Cons x xs -> #f]))
|
||||
|
||||
(define (tails [lst : (List X)] → (List (List X)))
|
||||
(match lst with
|
||||
[Nil -> (Cons Nil Nil)]
|
||||
[Cons x xs -> (Cons lst (tails xs))]))
|
||||
|
||||
(define (build-list [n : Int] [f : (→ Int X)] → (List X))
|
||||
(if (zero? (sub1 n))
|
||||
(Cons (f 0) Nil)
|
||||
(Cons (f (sub1 n)) (build-list (sub1 n) f))))
|
||||
(check-type (build-list 1 add1) : (List Int) ⇒ (Cons 1 Nil))
|
||||
(check-type (build-list 3 add1) : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 Nil))))
|
||||
(check-type (build-list 5 sub1)
|
||||
: (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 (Cons 0 (Cons -1 Nil))))))
|
||||
(check-type (build-list 5 (λ (x) (add1 (add1 x))))
|
||||
: (List Int) ⇒ (Cons 6 (Cons 5 (Cons 4 (Cons 3 (Cons 2 Nil))))))
|
||||
|
||||
(define (build-list/comp [i : Int] [n : Int] [nf : (→ Int Int)] [f : (→ Int X)] → (List X))
|
||||
(if (= i n)
|
||||
Nil
|
||||
(Cons (f (nf i)) (build-list/comp (add1 i) n nf f))))
|
||||
|
||||
(define built-list-1 (build-list/comp 0 3 (λ (x) (* 2 x)) add1))
|
||||
(define built-list-2 (build-list/comp 0 3 (λ (x) (* 2 x)) number->string))
|
||||
(check-type built-list-1 : (List Int) -> (Cons 1 (Cons 3 (Cons 5 Nil))))
|
||||
(check-type built-list-2 : (List String) -> (Cons "0" (Cons "2" (Cons "4" Nil))))
|
||||
|
||||
(define (~>2 [a : A] [f : (→ A A)] [g : (→ A B)] → B)
|
||||
(g (f a)))
|
||||
|
||||
(define ~>2-result-1 (~>2 1 (λ (x) (* 2 x)) add1))
|
||||
(define ~>2-result-2 (~>2 1 (λ (x) (* 2 x)) number->string))
|
||||
(check-type ~>2-result-1 : Int -> 3)
|
||||
(check-type ~>2-result-2 : String -> "2")
|
||||
|
||||
(define (append [lst1 : (List X)] [lst2 : (List X)] → (List X))
|
||||
(match lst1 with
|
||||
[Nil -> lst2]
|
||||
[Cons x xs -> (Cons x (append xs lst2))]))
|
||||
|
||||
(check-type (λ (a f g) (g (f a) (+ (f 1) (f 2))))
|
||||
: (→/test Int (→ Int Int) (→ Int Int C) C))
|
||||
|
||||
(check-type ((λ ([a : A] [f : (→ Int A)]) a) 4 (λ (x) x))
|
||||
: Int)
|
||||
|
||||
;; end infer.rkt tests --------------------------------------------------
|
||||
|
||||
;; algebraic data types
|
||||
(define-type IntList
|
||||
INil
|
||||
(ConsI Int IntList))
|
||||
|
||||
;; HO, monomorphic
|
||||
(check-type ConsI : (→ Int IntList IntList))
|
||||
(define (new-cons [c : (→ Int IntList IntList)] [x : Int] [xs : IntList]
|
||||
-> IntList)
|
||||
(c x xs))
|
||||
(check-type (new-cons ConsI 1 INil) : IntList -> (ConsI 1 INil))
|
||||
|
||||
;; check that ConsI and INil are available as tyvars
|
||||
(define (f10 [x : INil] [y : ConsI] -> ConsI) y)
|
||||
(check-type f10 : (→/test X Y Y))
|
||||
|
||||
(check-type INil : IntList)
|
||||
(check-type (ConsI 1 INil) : IntList)
|
||||
(check-type
|
||||
(match INil with
|
||||
[INil -> 1]
|
||||
[ConsI x xs -> 2]) : Int ⇒ 1)
|
||||
(check-type
|
||||
(match (ConsI 1 INil) with
|
||||
[INil -> 1]
|
||||
[ConsI x xs -> 2]) : Int ⇒ 2)
|
||||
(typecheck-fail (match 1 with [INil -> 1]))
|
||||
|
||||
(typecheck-fail (ConsI #f INil)
|
||||
#:with-msg
|
||||
"expected: Int\n *given: Bool")
|
||||
|
||||
;; annotated
|
||||
(check-type (Nil {Int}) : (List Int))
|
||||
(check-type (Cons {Int} 1 (Nil {Int})) : (List Int))
|
||||
(check-type (Cons {Int} 1 (Cons 2 (Nil {Int}))) : (List Int))
|
||||
;; partial annotations
|
||||
(check-type (Cons 1 (Nil {Int})) : (List Int))
|
||||
(check-type (Cons 1 (Cons 2 (Nil {Int}))) : (List Int))
|
||||
(check-type (Cons {Int} 1 Nil) : (List Int))
|
||||
(check-type (Cons {Int} 1 (Cons 2 Nil)) : (List Int))
|
||||
(check-type (Cons 1 (Cons {Int} 2 Nil)) : (List Int))
|
||||
; no annotations
|
||||
(check-type (Cons 1 Nil) : (List Int))
|
||||
(check-type (Cons 1 (Cons 2 Nil)) : (List Int))
|
||||
|
||||
(define-type (Tree X)
|
||||
(Leaf X)
|
||||
(Node (Tree X) (Tree X)))
|
||||
(check-type (Leaf 10) : (Tree Int))
|
||||
(check-type (Node (Leaf 10) (Leaf 11)) : (Tree Int))
|
||||
|
||||
(typecheck-fail Nil #:with-msg "Nil: no expected type, add annotations")
|
||||
(typecheck-fail (Cons 1 (Nil {Bool}))
|
||||
#:with-msg
|
||||
"expected: \\(List Int\\)\n *given: \\(List Bool\\)")
|
||||
(typecheck-fail (Cons {Bool} 1 (Nil {Int}))
|
||||
#:with-msg
|
||||
(string-append
|
||||
"Cons: type mismatch\n *expected: +Bool, \\(List Bool\\)\n *given: +Int, \\(List Int\\)\n"
|
||||
" *expressions: 1, \\(Nil \\(Int\\)\\)"))
|
||||
(typecheck-fail (Cons {Bool} 1 Nil)
|
||||
#:with-msg
|
||||
(string-append
|
||||
"Cons: type mismatch\n *expected: +Bool, \\(List Bool\\)\n *given: +Int, \\(List Bool\\)\n"
|
||||
" *expressions: 1, Nil"))
|
||||
|
||||
(typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1])
|
||||
#:with-msg "Nil: no expected type, add annotations")
|
||||
(check-type
|
||||
(match (Nil {Int}) with
|
||||
[Cons x xs -> 2]
|
||||
[Nil -> 1])
|
||||
: Int ⇒ 1)
|
||||
|
||||
(check-type
|
||||
(match (Nil {Int}) with
|
||||
[Nil -> 1]
|
||||
[Cons x xs -> 2])
|
||||
: Int ⇒ 1)
|
||||
|
||||
(check-type
|
||||
(match (Cons 1 Nil) with
|
||||
[Nil -> 3]
|
||||
[Cons y ys -> (+ y 4)])
|
||||
: Int ⇒ 5)
|
||||
|
||||
(check-type
|
||||
(match (Cons 1 Nil) with
|
||||
[Cons y ys -> (+ y 5)]
|
||||
[Nil -> 3])
|
||||
: Int ⇒ 6)
|
||||
|
||||
;; check expected-type propagation for other match paterns
|
||||
|
||||
(define-type (Option A)
|
||||
(None)
|
||||
(Some A))
|
||||
|
||||
(define (None* → (Option A)) None)
|
||||
|
||||
(check-type (match (tup 1 2) with [a b -> None]) : (Option Int) -> None)
|
||||
(check-type
|
||||
(match (list 1 2) with
|
||||
[[] -> None]
|
||||
[[x y] -> None])
|
||||
: (Option Int) -> None)
|
||||
|
||||
(check-type
|
||||
(match (list 1 2) with
|
||||
[[] -> None]
|
||||
[x :: xs -> None])
|
||||
: (Option Int) -> None)
|
||||
|
||||
(define-type (Pairof A B) (C A B))
|
||||
(check-type (match (C 1 2) with [C a b -> None]) : (Option Int) -> None)
|
||||
|
||||
;; type variable inference
|
||||
|
||||
; F should remain valid tyvar, even though it's bound
|
||||
(define (F [x : X] -> X) x)
|
||||
(define (tvf1 [x : F] -> F) x)
|
||||
(check-type tvf1 : (→/test X X))
|
||||
|
||||
; G should remain valid tyvar
|
||||
(define-type (Type1 X) (G X))
|
||||
(define (tvf5 [x : G] -> G) x)
|
||||
(check-type tvf5 : (→/test X X))
|
||||
|
||||
; TY should not be tyvar, bc it's a valid type
|
||||
(define-type-alias TY (Pairof Int Int))
|
||||
(define (tvf2 [x : TY] -> TY) x)
|
||||
(check-not-type tvf2 : (→/test X X))
|
||||
|
||||
; same with Bool
|
||||
(define (tvf3 [x : Bool] -> Bool) x)
|
||||
(check-not-type tvf3 : (→/test X X))
|
||||
|
||||
;; X in lam should not be a new tyvar
|
||||
(define (tvf4 [x : X] -> (→ X X))
|
||||
(λ (y) x))
|
||||
(check-type tvf4 : (→/test X (→ X X)))
|
||||
(check-not-type tvf4 : (→/test X (→ Y X)))
|
||||
|
||||
(define (tvf6 [x : X] -> (→ Y X))
|
||||
(λ (y) x))
|
||||
(check-type tvf6 : (→/test X (→ Y X)))
|
||||
|
||||
;; nested lambdas
|
||||
|
||||
(check-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test X (→ X X)))
|
||||
(check-not-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test {X} X (→/test {Y} Y Y)))
|
||||
(check-type (λ ([x : X]) (λ ([y : Y]) y)) : (→/test {X} X (→/test {Y} Y Y)))
|
||||
(check-not-type (λ ([x : X]) (λ ([y : Y]) x)) : (→/test X (→ X X)))
|
||||
|
||||
(check-type
|
||||
((λ ([x : X]) (λ ([y : Y]) y)) 1)
|
||||
: (→/test Y Y))
|
||||
|
||||
;; TODO?
|
||||
;; - this fails if polymorphic functions are allowed as HO args
|
||||
;; - do we want to allow this?
|
||||
;; - must explicitly instantiate before passing fn
|
||||
(check-type
|
||||
((λ ([x : (→ X (→ Y Y))]) x)
|
||||
(inst (λ ([x : X]) (inst (λ ([y : Y]) y) Int)) Int))
|
||||
: (→ Int (→ Int Int)))
|
||||
|
||||
(check-type
|
||||
((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1)
|
||||
: (→/test {Y} Y (→/test {Z} Z Z)))
|
||||
|
||||
(check-type (inst Cons (→/test X X))
|
||||
: (→ (→/test X X) (List (→/test X X)) (List (→/test X X))))
|
||||
(check-type map : (→/test (→ X Y) (List X) (List Y)))
|
||||
|
||||
(check-type (Cons (λ ([x : X]) x) Nil)
|
||||
: (List (→/test {X} X X)))
|
||||
|
||||
(define (nn [x : X] -> (→ (× X (→ Y Y))))
|
||||
(λ () (tup x (λ ([x : Y]) x))))
|
||||
(typecheck-fail (nn 1) #:with-msg "Could not infer instantiation of polymorphic function nn.")
|
||||
(check-type (nn 1) : (→ (× Int (→ String String))))
|
||||
(check-type (nn 1) : (→ (× Int (→ (List Int) (List Int)))))
|
||||
|
||||
(define (nn2 [x : X] -> (→ (× X (→ Y Y) (List Z))))
|
||||
(λ () (tup x (λ ([x : Y]) x) Nil)))
|
||||
(typecheck-fail (nn2 1) #:with-msg "Could not infer instantiation of polymorphic function nn2.")
|
||||
(check-type (nn2 1) : (→ (× Int (→ String String) (List (List Int)))))
|
||||
(check-type (nn2 1) : (→ (× Int (→ (List Int) (List Int)) (List String))))
|
||||
;; test inst order
|
||||
(check-type ((inst nn2 Int String (List Int)) 1)
|
||||
: (→ (× Int (→ String String) (List (List Int)))))
|
||||
(check-type ((inst nn2 Int (List Int) String) 1)
|
||||
: (→ (× Int (→ (List Int) (List Int)) (List String))))
|
||||
|
||||
(define (nn3 [x : X] -> (→ (× X (Option Y) (Option Z))))
|
||||
(λ () (tup x None None)))
|
||||
(check-type (nn3 1) : (→/test (× Int (Option Y) (Option Z))))
|
||||
(check-type (nn3 1) : (→ (× Int (Option String) (Option (List Int)))))
|
||||
(check-type ((nn3 1)) : (× Int (Option String) (Option (List Int))))
|
||||
(check-type ((nn3 1)) : (× Int (Option (List Int)) (Option String)))
|
||||
;; test inst order
|
||||
(check-type ((inst (nn3 1) String (List Int))) : (× Int (Option String) (Option (List Int))))
|
||||
(check-type ((inst (nn3 1) (List Int) String)) : (× Int (Option (List Int)) (Option String)))
|
||||
|
||||
(define (nn4 -> (→ (Option X)))
|
||||
(λ () (None*)))
|
||||
(check-type (let ([x (nn4)])
|
||||
x)
|
||||
: (→/test (Option X)))
|
||||
|
||||
(define (nn5 -> (→ (Ref (Option X))))
|
||||
(λ () (ref (None {X}))))
|
||||
(typecheck-fail (let ([x (nn5)])
|
||||
x)
|
||||
#:with-msg "Could not infer instantiation of polymorphic function nn5.")
|
||||
|
||||
(define (nn6 -> (→ (Option X)))
|
||||
(let ([r (((inst nn5 X)))])
|
||||
(λ () (deref r))))
|
||||
(check-type (nn6) : (→/test (Option X)))
|
||||
|
||||
;; A is covariant, B is invariant.
|
||||
(define-type (Cps A B)
|
||||
(cps (→ (→ A B) B)))
|
||||
(define (cps* [f : (→ (→ A B) B)] → (Cps A B))
|
||||
(cps f))
|
||||
|
||||
(define (nn7 -> (→ (Cps (Option A) B)))
|
||||
(let ([r (((inst nn5 A)))])
|
||||
(λ () (cps* (λ (k) (k (deref r)))))))
|
||||
(typecheck-fail (let ([x (nn7)])
|
||||
x)
|
||||
#:with-msg "Could not infer instantiation of polymorphic function nn7.")
|
||||
|
||||
(define (nn8 -> (→ (Cps (Option A) Int)))
|
||||
(nn7))
|
||||
(check-type (let ([x (nn8)])
|
||||
x)
|
||||
: (→/test (Cps (Option A) Int)))
|
||||
|
||||
(define-type (Result A B)
|
||||
(Ok A)
|
||||
(Error B))
|
||||
|
||||
(define (ok [a : A] → (Result A B))
|
||||
(Ok a))
|
||||
(define (error [b : B] → (Result A B))
|
||||
(Error b))
|
||||
|
||||
(define (ok-fn [a : A] -> (→ (Result A B)))
|
||||
(λ () (ok a)))
|
||||
(define (error-fn [b : B] -> (→ (Result A B)))
|
||||
(λ () (error b)))
|
||||
|
||||
(check-type (let ([x (ok-fn 1)])
|
||||
x)
|
||||
: (→/test (Result Int B)))
|
||||
(check-type (let ([x (error-fn "bad")])
|
||||
x)
|
||||
: (→/test (Result A String)))
|
||||
|
||||
(define (nn9 [a : A] -> (→ (Result A (Ref B))))
|
||||
(ok-fn a))
|
||||
(define (nn10 [a : A] -> (→ (Result A (Ref String))))
|
||||
(nn9 a))
|
||||
(define (nn11 -> (→ (Result (Option A) (Ref String))))
|
||||
(nn10 (None*)))
|
||||
|
||||
(typecheck-fail (let ([x (nn9 1)])
|
||||
x)
|
||||
#:with-msg "Could not infer instantiation of polymorphic function nn9.")
|
||||
(check-type (let ([x (nn10 1)])
|
||||
x)
|
||||
: (→ (Result Int (Ref String))))
|
||||
(check-type (let ([x (nn11)])
|
||||
x)
|
||||
: (→/test (Result (Option A) (Ref String))))
|
||||
|
||||
(check-type (if (zero? (random 2))
|
||||
(ok 0)
|
||||
(error "didn't get a zero"))
|
||||
: (Result Int String))
|
||||
|
||||
(define result-if-0
|
||||
(λ ([b : (Result A1 B1)] [succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
|
||||
(match b with
|
||||
[Ok a -> (succeed a)]
|
||||
[Error b -> (fail b)])))
|
||||
(check-type result-if-0
|
||||
: (→/test (Result A1 B1) (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
|
||||
(Result A2 B2)))
|
||||
|
||||
(define (result-if-1 [b : (Result A1 B1)]
|
||||
→ (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
|
||||
(Result A2 B2)))
|
||||
(λ ([succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
|
||||
(result-if-0 b succeed fail)))
|
||||
(check-type result-if-1
|
||||
: (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
|
||||
(Result A2 B2))))
|
||||
(check-type ((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
|
||||
: (→ (→ Int (Result (List Int) (List String)))
|
||||
(→ String (Result (List Int) (List String)))
|
||||
(Result (List Int) (List String))))
|
||||
(check-type ((inst result-if-1 Int String (List Int) (List String)) (Error "bad"))
|
||||
: (→ (→ Int (Result (List Int) (List String)))
|
||||
(→ String (Result (List Int) (List String)))
|
||||
(Result (List Int) (List String))))
|
||||
(check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
|
||||
(λ ([a : Int]) (ok (Cons a Nil)))
|
||||
(λ ([b : String]) (error (Cons b Nil))))
|
||||
: (Result (List Int) (List String)))
|
||||
;; same thing, but without the lambda annotations:
|
||||
(check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
|
||||
(λ (a) (ok (Cons a Nil)))
|
||||
(λ (b) (error (Cons b Nil))))
|
||||
: (Result (List Int) (List String)))
|
||||
|
||||
(define (result-if-2 [b : (Result A1 B1)]
|
||||
→ (→ (→ A1 (Result A2 B2))
|
||||
(→ (→ B1 (Result A2 B2))
|
||||
(Result A2 B2))))
|
||||
(λ ([succeed : (→ A1 (Result A2 B2))])
|
||||
(λ ([fail : (→ B1 (Result A2 B2))])
|
||||
(result-if-0 b succeed fail))))
|
||||
(check-type result-if-2
|
||||
: (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2))
|
||||
(→ (→ B1 (Result A2 B2))
|
||||
(Result A2 B2)))))
|
||||
(check-type ((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
|
||||
: (→/test (→ Int (Result (List Int) (List String)))
|
||||
(→ (→ String (Result (List Int) (List String)))
|
||||
(Result (List Int) (List String)))))
|
||||
(check-type (((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
|
||||
(λ (a) (Ok (Cons a Nil))))
|
||||
: (→/test (→ String (Result (List Int) (List String)))
|
||||
(Result (List Int) (List String))))
|
||||
(check-type ((((inst result-if-2 Int String (List Int) (List String)) (Ok 1))
|
||||
(λ (a) (Ok (Cons a Nil))))
|
||||
(λ (b) (Error (Cons b Nil))))
|
||||
: (Result (List Int) (List String)))
|
||||
|
||||
(define (tup* [a : A] [b : B] -> (× A B))
|
||||
(tup a b))
|
||||
|
||||
(define (nn12 -> (→ (× (Option A) (Option B))))
|
||||
(λ () (tup* (None*) (None*))))
|
||||
(check-type (let ([x (nn12)])
|
||||
x)
|
||||
: (→/test (× (Option A) (Option B))))
|
||||
|
||||
(define (nn13 -> (→ (× (Option A) (Option (Ref B)))))
|
||||
(nn12))
|
||||
(typecheck-fail (let ([x (nn13)])
|
||||
x)
|
||||
#:with-msg "Could not infer instantiation of polymorphic function nn13.")
|
||||
|
||||
;; records and automatically-defined accessors and predicates
|
||||
(define-type (RecoTest X Y)
|
||||
(RT1 [x : X] [y : Y] [z : String])
|
||||
(RT2 [a : Y] [b : X] [c : (List X)])
|
||||
(RT3 X Y)) ; mixing records and non-records allowed
|
||||
|
||||
(check-type RT1-x : (→/test (RecoTest X Y) X))
|
||||
(check-type RT1-y : (→/test (RecoTest X Y) Y))
|
||||
(check-type RT1-z : (→/test (RecoTest X Y) String))
|
||||
(check-type RT2-a : (→/test (RecoTest X Y) Y))
|
||||
(check-type RT2-b : (→/test (RecoTest X Y) X))
|
||||
|
||||
(check-type RT1? : (→/test (RecoTest X Y) Bool))
|
||||
(check-type RT2? : (→/test (RecoTest X Y) Bool))
|
||||
(check-type RT3? : (→/test (RecoTest X Y) Bool))
|
||||
|
||||
(check-type (RT1-x (RT1 1 #t "2")) : Int -> 1)
|
||||
(check-type (RT1-y (RT1 1 #t "2")) : Bool -> #t)
|
||||
(check-type (RT1-z (RT1 1 #t "2")) : String -> "2")
|
||||
|
||||
(check-type (RT2-a (RT2 1 #f Nil)) : Int -> 1)
|
||||
(check-type (RT2-b (RT2 1 #f Nil)) : Bool -> #f)
|
||||
(check-type (RT2-c (RT2 1 #f Nil)) : (List Bool) -> Nil)
|
||||
|
||||
(check-type (RT1? (RT1 1 2 "3")) : Bool -> #t)
|
||||
(check-type (RT1? (RT2 1 2 Nil)) : Bool -> #f)
|
||||
(check-type (RT1? (RT3 1 "2")) : Bool -> #f)
|
||||
(check-type (RT3? (RT3 1 2)) : Bool -> #t)
|
||||
(check-type (RT3? (RT1 1 2 "3")) : Bool -> #f)
|
||||
|
||||
(typecheck-fail RT3-x #:with-msg "unbound identifier")
|
||||
|
||||
;; accessors produce runtime exception if given wrong variant
|
||||
(check-runtime-exn (RT1-x (RT2 1 #f (Cons #t Nil))))
|
||||
(check-runtime-exn (RT1-y (RT2 1 #f (Cons #t Nil))))
|
||||
(check-runtime-exn (RT1-z (RT2 1 #f (Cons #t Nil))))
|
||||
(check-runtime-exn (RT1-x (RT3 1 2)))
|
||||
(check-runtime-exn (RT2-a (RT1 1 #f "2")))
|
||||
(check-runtime-exn (RT2-c (RT1 1 #f "2")))
|
||||
(check-runtime-exn (RT2-c (RT1 1 #f "2")))
|
||||
(check-runtime-exn (RT2-a (RT3 #f #t)))
|
||||
|
||||
;; non-match version
|
||||
(define (rt-fn [rt : (RecoTest X Y)] -> X)
|
||||
(if (RT1? rt)
|
||||
(RT1-x rt)
|
||||
(if (RT2? rt)
|
||||
(RT2-b rt)
|
||||
(match rt with [RT3 x y -> x][RT1 x y z -> x][RT2 a b c -> b]))))
|
||||
(check-type (rt-fn (RT1 1 #f "3")) : Int -> 1)
|
||||
(check-type (rt-fn (RT2 #f 2 Nil)) : Int -> 2)
|
||||
(check-type (rt-fn (RT3 10 20)) : Int -> 10)
|
||||
|
||||
;; HO constructors
|
||||
(check-type RT1 : (→/test X Y String (RecoTest X Y)))
|
||||
(check-type RT2 : (→/test {X Y} Y X (List X) (RecoTest X Y)))
|
||||
(check-type RT3 : (→/test X Y (RecoTest X Y)))
|
||||
|
||||
(typecheck-fail (for/fold ([x 1]) () "hello")
|
||||
#:with-msg "for/fold: type mismatch: expected Int, given String\n *expression: \"hello\"")
|
||||
|
||||
; ext-stlc tests --------------------------------------------------
|
||||
|
||||
; 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)
|
||||
#:with-msg
|
||||
"expected: Unit\n *given: Int")
|
||||
(typecheck-fail
|
||||
((λ ([x : Unit]) x) void)
|
||||
#:with-msg
|
||||
"expected: Unit\n *given: \\(→ Unit\\)")
|
||||
|
||||
(check-type ((λ ([x : Unit]) x) (void)) : Unit)
|
||||
|
||||
;; begin
|
||||
(check-type (begin 1) : Int)
|
||||
|
||||
(typecheck-fail (begin) #:with-msg "expected more terms")
|
||||
;; 2016-03-06: begin terms dont need to be Unit
|
||||
(check-type (begin 1 2 3) : Int)
|
||||
#;(typecheck-fail
|
||||
(begin 1 2 3)
|
||||
#:with-msg "Expected expression 1 to have Unit type, got: Int")
|
||||
|
||||
(check-type (begin (void) 1) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
|
||||
(check-type ((λ ([x : Int]) (begin x)) 1) : Int)
|
||||
(check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int)
|
||||
(check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int)
|
||||
(check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int)
|
||||
|
||||
;;ascription
|
||||
(check-type (ann 1 : Int) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
|
||||
(typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1")
|
||||
;ann errs
|
||||
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
|
||||
(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
|
||||
(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int")
|
||||
|
||||
; let
|
||||
(check-type (let () (+ 1 1)) : Int ⇒ 2)
|
||||
(check-type (let ([x 10]) (+ 1 2)) : Int)
|
||||
(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
|
||||
(typecheck-fail
|
||||
(let ([x #f]) (+ x 1))
|
||||
#:with-msg "expected: Int\n *given: Bool")
|
||||
(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)
|
||||
#:with-msg "expected: Int\n *given: Bool")
|
||||
|
||||
; letrec
|
||||
(typecheck-fail
|
||||
(letrec ([(x : Int) #f] [(y : Int) 1]) y)
|
||||
#:with-msg
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1")
|
||||
(typecheck-fail
|
||||
(letrec ([(y : Int) 1] [(x : Int) #f]) x)
|
||||
#:with-msg
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f")
|
||||
|
||||
(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
|
||||
|
||||
;; recursive
|
||||
(check-type
|
||||
(letrec ([(countdown : (→ Int String))
|
||||
(λ (i)
|
||||
(if (= i 0)
|
||||
"liftoff"
|
||||
(countdown (- i 1))))])
|
||||
(countdown 10)) : String ⇒ "liftoff")
|
||||
|
||||
;; mutually recursive
|
||||
(check-type
|
||||
(letrec ([(is-even? : (→ Int Bool))
|
||||
(λ (n)
|
||||
(or (zero? n)
|
||||
(is-odd? (sub1 n))))]
|
||||
[(is-odd? : (→ Int Bool))
|
||||
(λ (n)
|
||||
(and (not (zero? n))
|
||||
(is-even? (sub1 n))))])
|
||||
(is-odd? 11)) : Bool ⇒ #t)
|
||||
|
||||
;; check some more err msgs
|
||||
(typecheck-fail
|
||||
(and "1" #f)
|
||||
#:with-msg "and: type mismatch: expected Bool, given String\n *expression: \"1\"")
|
||||
(typecheck-fail
|
||||
(and #t "2")
|
||||
#:with-msg
|
||||
"and: type mismatch: expected Bool, given String\n *expression: \"2\"")
|
||||
(typecheck-fail
|
||||
(or "1" #f)
|
||||
#:with-msg
|
||||
"or: type mismatch\n *expected: +Bool, Bool\n *given: +String, Bool\n *expressions: \"1\", #f")
|
||||
(typecheck-fail
|
||||
(or #t "2")
|
||||
#:with-msg
|
||||
"or: type mismatch\n *expected: +Bool, Bool\n *given: +Bool, String\n *expressions: #t, \"2\"")
|
||||
;; 2016-03-09: now ok
|
||||
(check-type (if "true" 1 2) : Int -> 1)
|
||||
(typecheck-fail
|
||||
(if #t 1 "2")
|
||||
#:with-msg
|
||||
"branches have incompatible types: Int and String")
|
||||
|
||||
;; 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 y) x) : (→ Int Int Int))
|
||||
(check-not-type (λ ([x : Int]) x) : Int)
|
||||
(check-type (λ (x) x) : (→ Int Int))
|
||||
(check-type (λ (f) 1) : (→ (→ Int Int) Int))
|
||||
(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
|
||||
|
||||
(typecheck-fail
|
||||
((λ ([x : Bool]) x) 1)
|
||||
#:with-msg "expected: Bool\n *given: Int")
|
||||
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
|
||||
(typecheck-fail
|
||||
(λ ([f : Int]) (f 1 2))
|
||||
#:with-msg
|
||||
"Expected → type, got: Int")
|
||||
|
||||
(check-type (λ (f x y) (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))
|
||||
#:with-msg "expected: Int\n *given: \\(→ Int Int\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (→ Int Int)]) (+ x x))
|
||||
#:with-msg "expected: Int\n *given: \\(→ Int Int\\)")
|
||||
(typecheck-fail
|
||||
((λ ([x : Int] [y : Int]) y) 1)
|
||||
#:with-msg "wrong number of arguments: expected 2, given 1\n *expected: +Int, Int\n *arguments: 1")
|
||||
|
||||
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
|
||||
|
||||
3
macrotypes/examples/tests/rackunit-typechecking.rkt
Normal file
3
macrotypes/examples/tests/rackunit-typechecking.rkt
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
#lang racket/base
|
||||
(provide (all-from-out turnstile/examples/tests/rackunit-typechecking))
|
||||
(require turnstile/examples/tests/rackunit-typechecking)
|
||||
243
macrotypes/examples/tests/stlc+box-tests.rkt
Normal file
243
macrotypes/examples/tests/stlc+box-tests.rkt
Normal file
|
|
@ -0,0 +1,243 @@
|
|||
#lang s-exp "../stlc+box.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(define x (ref 10))
|
||||
(check-type x : (Ref Int))
|
||||
(check-type (deref x) : Int ⇒ 10)
|
||||
(check-type (:= x 20) : Unit) ; x still 10 because check-type does not evaluate
|
||||
(check-type (begin (:= x 20) (deref x)) : Int ⇒ 20)
|
||||
(check-type x : (Ref Int))
|
||||
(check-type (deref (ref 20)) : Int ⇒ 20)
|
||||
(check-type (deref x) : Int ⇒ 20)
|
||||
|
||||
(check-type ((λ ([b : (Ref Int)]) (deref b)) (ref 10)) : Int ⇒ 10)
|
||||
(check-type ((λ ([b : (Ref Int)]) (begin (begin (:= b 20) (deref b)))) (ref 10)) : Int ⇒ 20)
|
||||
|
||||
;; Ref err msgs
|
||||
; wrong arity
|
||||
(typecheck-fail
|
||||
(λ ([lst : (Ref Int Int)]) lst)
|
||||
#:with-msg
|
||||
"Improper usage of type constructor Ref: \\(Ref Int Int\\), expected = 1 arguments")
|
||||
(typecheck-fail
|
||||
(λ ([lst : (Ref)]) lst)
|
||||
#:with-msg
|
||||
"Improper usage of type constructor Ref: \\(Ref\\), expected = 1 arguments")
|
||||
(typecheck-fail
|
||||
(deref 1)
|
||||
#:with-msg
|
||||
"Expected Ref type, got: Int")
|
||||
(typecheck-fail
|
||||
(:= 1 1)
|
||||
#:with-msg
|
||||
"Expected Ref type, got: Int")
|
||||
(typecheck-fail
|
||||
(:= (ref 1) "hi")
|
||||
#:with-msg
|
||||
":=: type mismatch: expected Int, given String\n *expression: \"hi\"")
|
||||
|
||||
;; previous tests: ------------------------------------------------------------
|
||||
(typecheck-fail (cons 1 2))
|
||||
;(typecheck-fail (cons 1 nil)) ; works now
|
||||
(check-type (cons 1 nil) : (List Int))
|
||||
(check-type (cons 1 (nil {Int})) : (List Int))
|
||||
(typecheck-fail nil)
|
||||
(typecheck-fail (nil Int))
|
||||
(typecheck-fail (nil (Int)))
|
||||
; passes bc ⇒-rhs is only used for its runtime value
|
||||
(check-type (nil {Int}) : (List Int) ⇒ (nil {Bool}))
|
||||
(check-not-type (nil {Bool}) : (List Int))
|
||||
(check-type (nil {Bool}) : (List Bool))
|
||||
(check-type (nil {(→ Int Int)}) : (List (→ Int Int)))
|
||||
(define fn-lst (cons (λ ([x : Int]) (+ 10 x)) (nil {(→ Int Int)})))
|
||||
(check-type fn-lst : (List (→ Int Int)))
|
||||
(check-type (isnil fn-lst) : Bool ⇒ #f)
|
||||
(typecheck-fail (isnil (head fn-lst))) ; head lst is not List
|
||||
(check-type (isnil (tail fn-lst)) : Bool ⇒ #t)
|
||||
(check-type (head fn-lst) : (→ Int Int))
|
||||
(check-type ((head fn-lst) 25) : Int ⇒ 35)
|
||||
(check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)}))
|
||||
|
||||
;; previous tests: ------------------------------------------------------------
|
||||
;; define-type-alias
|
||||
(define-type-alias Integer Int)
|
||||
(define-type-alias ArithBinOp (→ Int Int Int))
|
||||
|
||||
(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))
|
||||
|
||||
(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]))
|
||||
|
||||
|
||||
(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 -----------------------------------------------------------
|
||||
; fail bc tuple changed syntax
|
||||
;(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)
|
||||
;; 2016-03-06: begin terms dont need to be Unit
|
||||
(check-type (begin 1 2 3) : Int)
|
||||
#;(typecheck-fail
|
||||
(begin 1 2 3)
|
||||
#:with-msg "Expected expression 1 to have Unit type, got: Int")
|
||||
(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)
|
||||
|
||||
229
macrotypes/examples/tests/stlc+cons-tests.rkt
Normal file
229
macrotypes/examples/tests/stlc+cons-tests.rkt
Normal file
|
|
@ -0,0 +1,229 @@
|
|||
#lang s-exp "../stlc+cons.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(typecheck-fail (cons 1 2)
|
||||
#:with-msg "expected \\(List Int\\), given Int\n *expression: 2")
|
||||
;(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: no expected type, add annotations")
|
||||
(typecheck-fail
|
||||
(nil Int)
|
||||
#:with-msg
|
||||
"Improperly formatted type annotation: Int; should have shape {τ}, where τ is a valid type.")
|
||||
(typecheck-fail
|
||||
(nil (Int))
|
||||
#:with-msg
|
||||
"Improperly formatted type annotation: \\(Int\\); should have shape {τ}, where τ is a valid type.")
|
||||
(typecheck-fail
|
||||
(λ ([lst : (List Int Int)]) lst)
|
||||
#:with-msg
|
||||
"Improper usage of type constructor List: \\(List Int Int\\), expected = 1 arguments")
|
||||
(typecheck-fail
|
||||
(λ ([lst : (List)]) lst)
|
||||
#:with-msg
|
||||
"Improper usage of type constructor List: \\(List\\), expected = 1 arguments")
|
||||
;; passes bc ⇒-rhs is only used for its runtime value
|
||||
(check-type (nil {Int}) : (List Int) ⇒ (nil {Bool}))
|
||||
(check-not-type (nil {Bool}) : (List Int))
|
||||
(check-type (nil {Bool}) : (List Bool))
|
||||
(check-type (nil {(→ Int Int)}) : (List (→ Int Int)))
|
||||
(define fn-lst (cons (λ ([x : Int]) (+ 10 x)) (nil {(→ Int Int)})))
|
||||
(check-type fn-lst : (List (→ Int Int)))
|
||||
(check-type (isnil fn-lst) : Bool ⇒ #f)
|
||||
(typecheck-fail
|
||||
(isnil (head fn-lst))
|
||||
#:with-msg
|
||||
"Expected List type, got: \\(→ Int Int\\)")
|
||||
(check-type (isnil (tail fn-lst)) : Bool ⇒ #t)
|
||||
(check-type (head fn-lst) : (→ Int Int))
|
||||
(check-type ((head fn-lst) 25) : Int ⇒ 35)
|
||||
(check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)}))
|
||||
|
||||
; more list errors
|
||||
(typecheck-fail
|
||||
(cons 1 1)
|
||||
#:with-msg
|
||||
"expected \\(List Int\\), given Int\n *expression: 1")
|
||||
|
||||
;; previous tests: ------------------------------------------------------------
|
||||
;; define-type-alias
|
||||
(define-type-alias Integer Int)
|
||||
(define-type-alias ArithBinOp (→ Int Int Int))
|
||||
|
||||
(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]))
|
||||
|
||||
|
||||
(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 -----------------------------------------------------------
|
||||
; fail because changed tuple syntax
|
||||
;(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)
|
||||
|
||||
245
macrotypes/examples/tests/stlc+effect-tests.rkt
Normal file
245
macrotypes/examples/tests/stlc+effect-tests.rkt
Normal file
|
|
@ -0,0 +1,245 @@
|
|||
#lang s-exp "../stlc+effect.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(check-props ν (ref 11) : (88))
|
||||
(check-props ! (deref (ref 11)) : (121))
|
||||
(check-props ν (deref (ref 11)) : (170))
|
||||
(check-props ν ((λ ([x : Int]) (ref x)) 21) : (221))
|
||||
|
||||
(define x (ref 10))
|
||||
(check-type x : (Ref Int))
|
||||
(check-type (deref x) : Int ⇒ 10)
|
||||
(check-type (:= x 20) : Unit) ; x still 10 because check-type does not evaluate
|
||||
(check-type (begin (:= x 20) (deref x)) : Int ⇒ 20)
|
||||
(check-type x : (Ref Int))
|
||||
(check-type (deref (ref 20)) : Int ⇒ 20)
|
||||
(check-type (deref x) : Int ⇒ 20)
|
||||
|
||||
(check-type ((λ ([b : (Ref Int)]) (deref b)) (ref 10)) : Int ⇒ 10)
|
||||
(check-type ((λ ([x : Int]) x) ((λ ([b : (Ref Int)]) (deref b)) (ref 10))) : Int ⇒ 10)
|
||||
(check-type ((λ ([b : (Ref Int)]) (begin (begin (:= b 20) (deref b)))) (ref 10)) : Int ⇒ 20)
|
||||
|
||||
;; Ref err msgs
|
||||
; wrong arity
|
||||
(typecheck-fail
|
||||
(λ ([lst : (Ref Int Int)]) lst)
|
||||
#:with-msg
|
||||
"Improper usage of type constructor Ref: \\(Ref Int Int\\), expected = 1 arguments")
|
||||
(typecheck-fail
|
||||
(λ ([lst : (Ref)]) lst)
|
||||
#:with-msg
|
||||
"Improper usage of type constructor Ref: \\(Ref\\), expected = 1 arguments")
|
||||
(typecheck-fail
|
||||
(deref 1)
|
||||
#:with-msg
|
||||
"Expected Ref type, got: Int")
|
||||
(typecheck-fail
|
||||
(:= 1 1)
|
||||
#:with-msg
|
||||
"Expected Ref type, got: Int")
|
||||
(typecheck-fail
|
||||
(:= (ref 1) "hi")
|
||||
#:with-msg
|
||||
":=: type mismatch: expected Int, given String\n *expression: \"hi\"")
|
||||
|
||||
;; previous tests: ------------------------------------------------------------
|
||||
(typecheck-fail (cons 1 2))
|
||||
;(typecheck-fail (cons 1 nil)) ; works now
|
||||
(check-type (cons 1 nil) : (List Int))
|
||||
(check-type (cons 1 (nil {Int})) : (List Int))
|
||||
(typecheck-fail nil)
|
||||
(typecheck-fail (nil Int))
|
||||
(typecheck-fail (nil (Int)))
|
||||
; passes bc ⇒-rhs is only used for its runtime value
|
||||
(check-type (nil {Int}) : (List Int) ⇒ (nil {Bool}))
|
||||
(check-not-type (nil {Bool}) : (List Int))
|
||||
(check-type (nil {Bool}) : (List Bool))
|
||||
(check-type (nil {(→ Int Int)}) : (List (→ Int Int)))
|
||||
(define fn-lst (cons (λ ([x : Int]) (+ 10 x)) (nil {(→ Int Int)})))
|
||||
(check-type fn-lst : (List (→ Int Int)))
|
||||
(check-type (isnil fn-lst) : Bool ⇒ #f)
|
||||
(typecheck-fail (isnil (head fn-lst))) ; head lst is not List
|
||||
(check-type (isnil (tail fn-lst)) : Bool ⇒ #t)
|
||||
(check-type (head fn-lst) : (→ Int Int))
|
||||
(check-type ((head fn-lst) 25) : Int ⇒ 35)
|
||||
(check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)}))
|
||||
|
||||
;; previous tests: ------------------------------------------------------------
|
||||
;; define-type-alias
|
||||
(define-type-alias Integer Int)
|
||||
(define-type-alias ArithBinOp (→ Int Int Int))
|
||||
|
||||
(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))
|
||||
|
||||
(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]))
|
||||
|
||||
|
||||
(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 -----------------------------------------------------------
|
||||
; fail bc tuple changed syntax
|
||||
;(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)
|
||||
|
||||
62
macrotypes/examples/tests/stlc+lit-tests.rkt
Normal file
62
macrotypes/examples/tests/stlc+lit-tests.rkt
Normal file
|
|
@ -0,0 +1,62 @@
|
|||
#lang s-exp "../stlc+lit.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; thunk
|
||||
(check-type (λ () 1) : (→ Int))
|
||||
|
||||
(check-type 1 : Int)
|
||||
(check-not-type 1 : (→ Int Int))
|
||||
|
||||
(typecheck-fail "one" #:with-msg "Unsupported literal")
|
||||
(typecheck-fail #f #:with-msg "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))
|
||||
|
||||
(typecheck-fail
|
||||
(λ ([x : →]) x)
|
||||
#:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
|
||||
(typecheck-fail
|
||||
(λ ([x : (→ →)]) x)
|
||||
#:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
|
||||
(typecheck-fail
|
||||
(λ ([x : (→)]) x)
|
||||
#:with-msg "Improper usage of type constructor →: \\(→\\), expected >= 1 arguments")
|
||||
|
||||
(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
|
||||
(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
|
||||
|
||||
(typecheck-fail ((λ ([x : Bool]) x) 1)
|
||||
#:with-msg "Bool: unbound identifier")
|
||||
(typecheck-fail (λ ([x : (→ Bool Bool)]) x)
|
||||
#:with-msg "Bool: unbound identifier")
|
||||
(typecheck-fail (λ ([x : Bool]) x)
|
||||
#:with-msg "Bool: unbound identifier")
|
||||
(typecheck-fail
|
||||
(λ ([f : Int]) (f 1 2))
|
||||
#:with-msg
|
||||
"Expected → type, 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))
|
||||
#:with-msg (string-append "expected: +Int, Int\n *given: +Int, \\(→ Int Int\\)\n"
|
||||
" *expressions: 1, \\(λ \\(\\(x : Int\\)\\) x\\)"))
|
||||
(typecheck-fail
|
||||
(λ ([x : (→ Int Int)]) (+ x x))
|
||||
#:with-msg "expected: +Int, Int\n *given: +\\(→ Int Int\\), \\(→ Int Int\\)\n *expressions: x, x")
|
||||
(typecheck-fail
|
||||
((λ ([x : Int] [y : Int]) y) 1)
|
||||
#:with-msg "wrong number of arguments: expected 2, given 1")
|
||||
|
||||
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
|
||||
|
||||
(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a valid type")
|
||||
|
||||
|
|
@ -75,7 +75,7 @@
|
|||
|
||||
(typecheck-fail
|
||||
((resolve to-string Num) "hello")
|
||||
#:with-msg (expected "Num" #:given "Str"))
|
||||
#:with-msg "expected: +Num\n *given: +Str\n *expressions: \"hello\"")
|
||||
|
||||
;; -- instances are type-checked. They must match
|
||||
(typecheck-fail
|
||||
|
|
|
|||
232
macrotypes/examples/tests/stlc+reco+var-tests.rkt
Normal file
232
macrotypes/examples/tests/stlc+reco+var-tests.rkt
Normal file
|
|
@ -0,0 +1,232 @@
|
|||
#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) : (×))
|
||||
(check-type (tup [name = "Stephen"]) : (× [name : String]))
|
||||
(check-type (proj (tup [name = "Stephen"]) name) : String ⇒ "Stephen")
|
||||
(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]))
|
||||
|
||||
;; record errors
|
||||
(typecheck-fail
|
||||
(proj 1 "a")
|
||||
#:with-msg
|
||||
"expected identifier")
|
||||
(typecheck-fail
|
||||
(proj 1 a)
|
||||
#:with-msg
|
||||
"Expected expression 1 to have × type, got: Int")
|
||||
|
||||
;; 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])))
|
||||
#:with-msg
|
||||
"expected: +\\(∨ \\(coffee : Unit\\) \\(tea : Unit\\)\\)\n *given: +\\(∨ \\(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])
|
||||
#:with-msg "wrong number of case clauses")
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => 1]
|
||||
[teaaaaaa x => 2])
|
||||
#:with-msg "case clauses not exhaustive")
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => 1]
|
||||
[tea x => 2]
|
||||
[coke x => 3])
|
||||
#:with-msg "wrong number of case clauses")
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => "1"]
|
||||
[tea x => 2])
|
||||
#:with-msg "branches have incompatible types: String and Int")
|
||||
(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)
|
||||
|
||||
;; variant errors
|
||||
(typecheck-fail
|
||||
(var name = "Steve" as Int)
|
||||
#:with-msg
|
||||
"Expected the expected type to be a ∨ type, got: Int")
|
||||
(typecheck-fail
|
||||
(case 1 [racket x => 1])
|
||||
#:with-msg
|
||||
"Expected ∨ type, got: Int")
|
||||
(typecheck-fail
|
||||
(λ ([x : (∨)]) x)
|
||||
#:with-msg "Improper usage of type constructor ∨: \\(∨\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (∨ 1)]) x)
|
||||
#:with-msg "Improper usage of type constructor ∨: \\(∨ 1\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (∨ [1 2])]) x)
|
||||
#:with-msg "Improper usage of type constructor ∨: \\(∨ \\(1 2\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (∨ [a 2])]) x)
|
||||
#:with-msg "Improper usage of type constructor ∨: \\(∨ \\(a 2\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (∨ [a Int])]) x)
|
||||
#:with-msg "Improper usage of type constructor ∨: \\(∨ \\(a Int\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (∨ [1 : Int])]) x)
|
||||
#:with-msg "Improper usage of type constructor ∨: \\(∨ \\(1 : Int\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (∨ [a : 1])]) x)
|
||||
#:with-msg "Improper usage of type constructor ∨: \\(∨ \\(a : 1\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
|
||||
|
||||
;; previous tuple tests: ------------------------------------------------------------
|
||||
;; wont work anymore
|
||||
;;(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)
|
||||
|
||||
107
macrotypes/examples/tests/stlc+tup-tests.rkt
Normal file
107
macrotypes/examples/tests/stlc+tup-tests.rkt
Normal file
|
|
@ -0,0 +1,107 @@
|
|||
#lang s-exp "../stlc+tup.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; 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) -1) #:with-msg "expected exact-nonnegative-integer")
|
||||
(typecheck-fail (proj (tup 1 "2" #f) 3) #:with-msg "index too large")
|
||||
(typecheck-fail
|
||||
(proj 1 2)
|
||||
#:with-msg
|
||||
"proj: Expected × type, got: Int")
|
||||
|
||||
;; 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)
|
||||
|
||||
12
macrotypes/examples/tests/stlc-tests.rkt
Normal file
12
macrotypes/examples/tests/stlc-tests.rkt
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
#lang s-exp "../stlc.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; cannot write any terms without base types, but can check some errors
|
||||
|
||||
(typecheck-fail (λ ([x : Undef]) x) #:with-msg "Undef: unbound identifier")
|
||||
(typecheck-fail (λ ([x : →]) x)
|
||||
#:with-msg "Improper usage of type constructor →.+expected >= 1 arguments")
|
||||
(typecheck-fail (λ ([x : (→)]) x)
|
||||
#:with-msg "Improper usage of type constructor →.+expected >= 1 arguments")
|
||||
(typecheck-fail (λ ([x : (→ →)]) x)
|
||||
#:with-msg "Improper usage of type constructor →.+expected >= 1 arguments")
|
||||
|
|
@ -50,6 +50,9 @@
|
|||
(cons (list (lookup #'a substs) #'b)
|
||||
#'rst)
|
||||
orig-cs)]
|
||||
[(and (identifier? #'b) (var? #'b) (free-identifier=? #'a #'b))
|
||||
;; #'a and #'b are equal, drop this constraint
|
||||
(add-constraints/var? Xs var? substs #'rst orig-cs)]
|
||||
[else
|
||||
(define entry (occurs-check (list #'a #'b) orig-cs))
|
||||
(add-constraints/var?
|
||||
|
|
|
|||
|
|
@ -118,7 +118,7 @@
|
|||
(format (string-append
|
||||
"Could not infer instantiation of polymorphic function ~s.\n"
|
||||
" expected: ~a\n"
|
||||
" given: ~a")
|
||||
" given: ~a")
|
||||
(syntax->datum (get-orig e_fn))
|
||||
(string-join (stx-map type->str expected-tys) ", ")
|
||||
(string-join (stx-map type->str given-tys) ", ")))
|
||||
|
|
|
|||
|
|
@ -31,6 +31,10 @@
|
|||
(:= 1 1)
|
||||
#:with-msg
|
||||
"Expected Ref type, got: Int")
|
||||
(typecheck-fail
|
||||
(:= (ref 1) "hi")
|
||||
#:with-msg
|
||||
":=: type mismatch: expected Int, given String\n *expression: \"hi\"")
|
||||
|
||||
;; previous tests: ------------------------------------------------------------
|
||||
(typecheck-fail (cons 1 2))
|
||||
|
|
|
|||
|
|
@ -37,6 +37,10 @@
|
|||
(:= 1 1)
|
||||
#:with-msg
|
||||
"Expected Ref type, got: Int")
|
||||
(typecheck-fail
|
||||
(:= (ref 1) "hi")
|
||||
#:with-msg
|
||||
":=: type mismatch: expected Int, given String\n *expression: \"hi\"")
|
||||
|
||||
;; previous tests: ------------------------------------------------------------
|
||||
(typecheck-fail (cons 1 2))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user