From 0dde065949bf910fb5408171af53e9a48dbf41d2 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 7 Aug 2015 17:26:53 -0400 Subject: [PATCH] new define-type-constructor: support binding forms - tests passing up to stlc+rec-iso.rkt --- tapl/ext-stlc.rkt | 27 +-- tapl/stlc+box.rkt | 10 +- tapl/stlc+cons.rkt | 17 +- tapl/stlc+rec-iso.rkt | 41 +++-- tapl/stlc+reco+var.rkt | 38 ++--- tapl/stlc+tup.rkt | 6 +- tapl/stlc.rkt | 10 +- tapl/tests/ext-stlc-tests.rkt | 11 +- tapl/tests/run-all-tests.rkt | 8 +- tapl/tests/stlc+box-tests.rkt | 38 ++--- tapl/tests/stlc+cons-tests.rkt | 44 ++--- tapl/tests/stlc+lit-tests.rkt | 2 +- tapl/tests/stlc+rec-iso-tests.rkt | 80 +++++---- tapl/tests/stlc+reco+var-tests.rkt | 66 ++++---- tapl/tests/stlc+tup-tests.rkt | 1 + tapl/typecheck.rkt | 263 ++++++++++++++++++----------- 16 files changed, 383 insertions(+), 279 deletions(-) diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt index de11e4d..ebb4fa2 100644 --- a/tapl/ext-stlc.rkt +++ b/tapl/ext-stlc.rkt @@ -47,26 +47,31 @@ (define-syntax (and/tc stx) (syntax-parse stx [(_ e1 e2) - #:with (e1- τ1) (infer+erase #'e1) - #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1)) - #:with (e2- τ2) (infer+erase #'e2) - #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2)) + #:with e1- (inferBool+erase #'e1) + #:with e2- (inferBool+erase #'e2) +; #:with (e1- τ1) (infer+erase #'e1) +; #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1)) +; #:with (e2- τ2) (infer+erase #'e2) +; #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2)) (⊢ (and e1- e2-) : Bool)])) (define-syntax (or/tc stx) (syntax-parse stx [(_ e1 e2) - #:with (e1- τ1) (infer+erase #'e1) - #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1)) - #:with (e2- τ2) (infer+erase #'e2) - #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2)) + #:with e1- (inferBool+erase #'e1) + #:with e2- (inferBool+erase #'e2) +; #:with (e1- τ1) (infer+erase #'e1) +; #:fail-unless (Bool? #'τ1) (format "given non-Bool arg: ~a\n" (syntax->datum #'e1)) +; #:with (e2- τ2) (infer+erase #'e2) +; #:fail-unless (Bool? #'τ2) (format "given non-Bool arg: ~a\n" (syntax->datum #'e2)) (⊢ (or e1- e2-) : Bool)])) (define-syntax (if/tc stx) (syntax-parse stx [(_ e_tst e1 e2) - #:with (e_tst- τ_tst) (infer+erase #'e_tst) - #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst)) + #:with e_tst- (inferBool+erase #'e_tst) +; #:with (e_tst- τ_tst) (infer+erase #'e_tst) +; #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst)) #:with (e1- τ1) (infer+erase #'e1) #:with (e2- τ2) (infer+erase #'e2) #:when ((current-type=?) #'τ1 #'τ2) @@ -118,7 +123,7 @@ [(_ ([b:typed-binding e] ...) e_body) #:with ((x- ...) (e- ... e_body-) (τ ... τ_body)) (infers/type-ctxt+erase #'(b ...) #'(e ... e_body)) - #:fail-unless (typechecks? (type-evals #'(b.τ ...)) #'(τ ...)) + #:fail-unless (typechecks? #'(b.τ ...) #;(type-evals #'(b.τ ...)) #'(τ ...)) (string-append "type check fail, args have wrong type:\n" (string-join diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt index cc4e769..c6672d1 100644 --- a/tapl/stlc+box.rkt +++ b/tapl/stlc+box.rkt @@ -23,14 +23,16 @@ (define-syntax (deref stx) (syntax-parse stx [(_ e) - #:with (e- ref-τ) (infer+erase #'e) - #:with τ (Ref-get τ from ref-τ) + #:with (e- (τ)) (inferRef+erase #'e) +; #:with (e- ref-τ) (infer+erase #'e) +; #:with τ (Ref-get τ from ref-τ) (⊢ (unbox e-) : τ)])) (define-syntax (:= stx) (syntax-parse stx [(_ e_ref e) - #:with (e_ref- ref-τ) (infer+erase #'e_ref) - #:with τ1 (Ref-get τ from ref-τ) + #:with (e_ref- (τ1)) (inferRef+erase #'e_ref) +; #:with (e_ref- ref-τ) (infer+erase #'e_ref) +; #:with τ1 (Ref-get τ from ref-τ) #:with (e- τ2) (infer+erase #'e) #:when (typecheck? #'τ1 #'τ2) (⊢ (set-box! e_ref- e-) : Unit)])) \ No newline at end of file diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt index 3a9da8c..9326136 100644 --- a/tapl/stlc+cons.rkt +++ b/tapl/stlc+cons.rkt @@ -28,23 +28,24 @@ (syntax-parse stx [(_ e1 e2) #:with (e1- τ1) (infer+erase #'e1) - #:with (e2- τ-lst) (infer+erase #'e2) -; #:when (displayln #'τ-lst) - #:with τ2 (List-get τ from τ-lst) - ; #:when (displayln #'τ2) + #:with (e2- (~List τ2)) (infer+erase #'e2) +; #:with (e2- τ-lst) (infer+erase #'e2) +; #:with τ2 (List-get τ from τ-lst) #:when (typecheck? #'τ1 #'τ2) (⊢ (cons e1- e2-) : (List τ1))])) (define-syntax (isnil stx) (syntax-parse stx [(_ e) - #:with (e- τ-lst) (infer+erase #'e) - #:fail-unless (List? #'τ-lst) "expected argument of List type" + #:with (e- _) (inferList+erase #'e) +; #:with (e- τ-lst) (infer+erase #'e) +; #:fail-unless (List? #'τ-lst) "expected argument of List type" (⊢ (null? e-) : Bool)])) (define-syntax (head stx) (syntax-parse stx [(_ e) - #:with (e- τ-lst) (infer+erase #'e) - #:with τ (List-get τ from τ-lst) + #:with (e- (τ)) (inferList+erase #'e) +; #:with (e- τ-lst) (infer+erase #'e) +; #:with τ (List-get τ from τ-lst) (⊢ (car e-) : τ)])) (define-syntax (tail stx) (syntax-parse stx diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt index 67e97ab..0b01ec4 100644 --- a/tapl/stlc+rec-iso.rkt +++ b/tapl/stlc+rec-iso.rkt @@ -1,10 +1,12 @@ #lang racket/base (require "typecheck.rkt") (require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ type=?)) - (except-in "stlc+reco+var.rkt" #%app λ type=?)) + (except-in "stlc+reco+var.rkt" #%app λ type=? × tup proj) + (only-in "stlc+tup.rkt" × tup proj)) (provide (rename-out [stlc:#%app #%app] [stlc:λ λ])) (provide (except-out (all-from-out "stlc+reco+var.rkt") - stlc:#%app stlc:λ (for-syntax stlc:type=?))) + stlc:#%app stlc:λ (for-syntax stlc:type=?)) + (all-from-out "stlc+tup.rkt")) (provide μ fld unfld (for-syntax type=?)) ;; stlc + (iso) recursive types @@ -15,11 +17,23 @@ ;; - terms from stlc+reco+var.rkt ;; - fld/unfld +(define-type-constructor + (μ [[tv]] τ_body)) +; can't enforce this because bound ids wont have #%type tag + ;#:declare τ_body type) +#;(define-syntax (μ stx) + (syntax-parse stx + [(_ (tv:id) τ_body) + #'(#%type + (λ (tv) + (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])]) + τ_body)))])) + (begin-for-syntax ;; extend to handle μ (define (type=? τ1 τ2) - ;(printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1)) - ;(printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2)) +; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1)) +; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2)) (syntax-parse (list τ1 τ2) [(((~literal #%plain-lambda) (x:id ...) k1 ... t1) ((~literal #%plain-lambda) (y:id ...) k2 ... t2)) @@ -31,22 +45,19 @@ (current-type=? type=?) (current-typecheck-relation type=?)) -(define-syntax (μ stx) - (syntax-parse stx - [(_ (tv:id) τ_body) - #'(λ (tv) τ_body)])) - (define-syntax (unfld stx) (syntax-parse stx [(_ τ:ann e) - #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm + #:with (~μ [[tv]] τ_body) #'τ.norm +; #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm #:with [e- τ_e] (infer+erase #'e) - #:when ((current-typecheck-relation) #'τ_e #'τ.norm) - (⊢ #'e- (subst #'τ.norm #'tv #'τ_body))])) + #:when (typecheck? #'τ_e #'τ.norm) + (⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))])) (define-syntax (fld stx) (syntax-parse stx [(_ τ:ann e) - #:with ((~literal #%plain-lambda) (tv:id) τ_body) #'τ.norm + #:with (~μ [[tv]] τ_body) #'τ.norm +; #:with ((~literal #%plain-type) ((~literal #%plain-lambda) (tv:id) τ_body)) #'τ.norm #:with [e- τ_e] (infer+erase #'e) - #:when ((current-typecheck-relation) #'τ_e (subst #'τ.norm #'tv #'τ_body)) - (⊢ #'e- #'τ.norm)])) \ No newline at end of file + #:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body)) + (⊢ e- : τ.τ)])) \ No newline at end of file diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt index 4ea8fa6..88cbdec 100644 --- a/tapl/stlc+reco+var.rkt +++ b/tapl/stlc+reco+var.rkt @@ -1,7 +1,7 @@ #lang racket/base (require "typecheck.rkt") (require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin tup proj let type=?)) - (except-in "stlc+tup.rkt" #%app begin tup proj let type=? ×)) + (except-in "stlc+tup.rkt" #%app begin tup proj let type=? × ~×)) (provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin] [define/tc define])) (provide (except-out (all-from-out "stlc+tup.rkt") @@ -56,7 +56,8 @@ ; re-define tuples as records (define-type-constructor - (× [~× label τ_fld] ...) #:lits (~×) + ;(× [~× label τ_fld] ...) #:lits (~×) + (× [: label τ_fld] ...) #:lits (:) #:declare label str #:declare τ_fld type ) @@ -68,26 +69,24 @@ (syntax-parse stx #:datum-literals (=) [(_ [l:str = e] ...) #:with ([e- τ] ...) (infers+erase #'(e ...)) - (⊢ (list (list l e-) ...) : (× [~× l τ] ...))] + ;(⊢ (list (list l e-) ...) : (× [~× l τ] ...))] + (⊢ (list (list l e-) ...) : (× [: l τ] ...))] #;[(_ e ...) #'(stlc:tup e ...)])) (define-syntax (proj stx) (syntax-parse stx #:literals (quote) - [(_ rec l:str) - #:with [rec- τ_rec] (infer+erase #'rec) -; #:when (printf "inferred type: ~a\n" (syntax->datum #'τ_rec)) -; #:when (printf "inferred type eval ~a\n" (syntax->datum ((current-type-eval) #'τ_rec))) - #:with ('l_τ:str ...) (×-get label from τ_rec) - #:with (τ ...) (×-get τ_fld from τ_rec) -; #:fail-unless (×? #'τ_rec) (format "not record type: ~a" (syntax->datum #'τ_rec)) -; #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec)) + [(_ e_rec l:str) + #:with (e_rec- (~× [: 'l_τ τ] ...)) (infer+erase #'e_rec) +; #:with [rec- τ_rec] (infer+erase #'e_rec) ; match method #2: get +; #:with ('l_τ:str ...) (×-get label from τ_rec) +; #:with (τ ...) (×-get τ_fld from τ_rec) #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...)) - (⊢ (cadr (assoc l rec)) : τ_match)] + (⊢ (cadr (assoc l e_rec-)) : τ_match)] #;[(_ e ...) #'(stlc:proj e ...)])) (define-type-constructor - (∨ [~∨ label τ_var] ...) #:lits (~∨) + (∨ [<> label τ_var] ...) #:lits (<>) #:declare label str #:declare τ_var type) @@ -96,8 +95,9 @@ [(_ l:str = e as τ:type) ; #:when (∨? #'τ.norm) ; #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm)) - #:with ('l_τ:str ...) (∨-get label from τ) - #:with (τ_l ...) (∨-get τ_var from τ) + #:with (~∨ [<> 'l_τ τ_l] ...) #'τ.norm +; #:with ('l_τ:str ...) (∨-get label from τ) +; #:with (τ_l ...) (∨-get τ_var from τ) #:with (l_match:str τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...)) #:with (e- τ_e) (infer+erase #'e) #:when (typecheck? #'τ_e #'τ_match) @@ -106,11 +106,9 @@ (syntax-parse stx #:datum-literals (of =>) #:literals (quote) [(_ e [l:str x => e_l] ...) #:fail-when (null? (syntax->list #'(l ...))) "no clauses" - #:with (e- τ_e) (infer+erase #'e) - #:with ('l_x:str ...) (∨-get label from τ_e) - #:with (τ_x ...) (∨-get τ_var from τ_e) -; #:when (∨? #'τ_e) -; #:with (['l_x:str τ_x] ...) (stx-map :-args (∨-args #'τ_e)) + #:with (e- (~∨ [<> 'l_x τ_x] ...)) (infer+erase #'e) +; #:with ('l_x:str ...) (∨-get label from τ_e) +; #:with (τ_x ...) (∨-get τ_var from τ_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) ...) diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt index 1b2c3c4..a143203 100644 --- a/tapl/stlc+tup.rkt +++ b/tapl/stlc+tup.rkt @@ -23,8 +23,8 @@ (⊢ (list e- ...) : (× τ ...))])) (define-syntax (proj stx) (syntax-parse stx - [(_ e_tup n:integer) - #:with [e_tup- τs_tup] (×-match+erase #'e_tup) - #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "proj index too large" + [(_ e_tup n:nat) + #: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)))])) \ No newline at end of file diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index e59d7fc..c18860a 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -61,10 +61,12 @@ (define-syntax (app/tc stx) (syntax-parse stx [(_ e_fn e_arg ...) -; #:with [e_fn- τ_fn] (infer+erase #'e_fn) -; #:with (τ_in ...) (→-get τ_in from #'τ_fn) -; #:with τ_out (→-get τ_out from #'τ_fn) - #:with [e_fn- (τ_in ... τ_out)] (→-match+erase #'e_fn) + ;; 2015-08-06: there are currently three alternative tycon matching syntaxes + #:with [e_fn- (~→ τ_in ... τ_out)] (infer+erase #'e_fn) ; #1 (external) pattern expander + ;#:with [e_fn- τ_fn] (infer+erase #'e_fn) ; #2 get, via (internal) pattern expander + ;#:with (τ_in ...) (→-get τ_in from #'τ_fn) + ;#:with τ_out (→-get τ_out from #'τ_fn) + ;#:with [e_fn- (τ_in ... τ_out)] (infer→+erase #'e_fn) ; #3 work directly on term #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...)) #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) (string-append diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt index 443b03f..995d713 100644 --- a/tapl/tests/ext-stlc-tests.rkt +++ b/tapl/tests/ext-stlc-tests.rkt @@ -2,7 +2,6 @@ (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 @@ -95,6 +94,14 @@ (is-even? (sub1 n))))]) (is-odd? 11)) : Bool ⇒ #t) +;; check some more err msgs +(typecheck-fail (and "1" #f) #:with-msg "Expected type of.+to be Bool") +(typecheck-fail (and #t "2") #:with-msg "Expected type of.+to be Bool") +(typecheck-fail (or "1" #f) #:with-msg "Expected type of.+to be Bool") +(typecheck-fail (or #t "2") #:with-msg "Expected type of.+to be Bool") +(typecheck-fail (if "true" 1 2) #:with-msg "Expected type of.+to be Bool") + + ;; tests from stlc+lit-tests.rkt -------------------------- ; most should pass, some failing may now pass due to added types/forms (check-type 1 : Int) @@ -115,7 +122,7 @@ (typecheck-fail (λ ([f : Int]) (f 1 2)) #:with-msg - "Expected type of expression f to match pattern \\(→ τ_in ... τ_out\\), got: Int") + "Expected type of expression to match pattern \\(→ τ_in ... τ_out\\), got: Int") (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) : (→ (→ Int Int Int) Int Int Int)) diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt index c459991..5b4588e 100644 --- a/tapl/tests/run-all-tests.rkt +++ b/tapl/tests/run-all-tests.rkt @@ -7,10 +7,10 @@ (require "stlc+tup-tests.rkt") (require "stlc+reco+var-tests.rkt") (require "stlc+cons-tests.rkt") -;(require "stlc+box-tests.rkt") -; -;(require "stlc+rec-iso-tests.rkt") -; +(require "stlc+box-tests.rkt") + +(require "stlc+rec-iso-tests.rkt") + ;(require "exist-tests.rkt") ; ;;; subtyping diff --git a/tapl/tests/stlc+box-tests.rkt b/tapl/tests/stlc+box-tests.rkt index 7c600ea..742ce76 100644 --- a/tapl/tests/stlc+box-tests.rkt +++ b/tapl/tests/stlc+box-tests.rkt @@ -50,7 +50,7 @@ (check-type "Stephen" : String) (check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [~× "name" String] [~× "phone" Int] [~× "male?" Bool])) + (× [: "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") @@ -60,48 +60,48 @@ (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])) + (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [~× "name" String] [~× "my-phone" Int] [~× "male?" Bool])) + (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [~× "name" String] [~× "phone" Int] [~× "is-male?" Bool])) + (× [: "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])) +(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])) + (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])) + (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])) + (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])) + (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])) + (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])) +(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]))) + (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool]))) ["coffee" x => (+ (+ x x) (+ x x))] ["tea" x => 2] ["coke" y => 3]) diff --git a/tapl/tests/stlc+cons-tests.rkt b/tapl/tests/stlc+cons-tests.rkt index 3553bcc..3221af6 100644 --- a/tapl/tests/stlc+cons-tests.rkt +++ b/tapl/tests/stlc+cons-tests.rkt @@ -25,8 +25,10 @@ (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 argument of List type") +(typecheck-fail + (isnil (head fn-lst)) + #:with-msg + "Expected type of expression \\(head fn-lst) to match pattern \\(List τ), 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) @@ -46,7 +48,7 @@ ;; records (ie labeled tuples) (check-type "Stephen" : String) (check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [~× "name" String] [~× "phone" Int] [~× "male?" Bool])) + (× [: "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") @@ -56,48 +58,48 @@ (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])) + (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [~× "name" String] [~× "my-phone" Int] [~× "male?" Bool])) + (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [~× "name" String] [~× "phone" Int] [~× "is-male?" Bool])) + (× [: "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])) +(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])) + (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])) + (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])) + (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])) + (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])) + (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])) +(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]))) + (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool]))) ["coffee" x => (+ (+ x x) (+ x x))] ["tea" x => 2] ["coke" y => 3]) diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt index 8c1fdd8..a30a4d8 100644 --- a/tapl/tests/stlc+lit-tests.rkt +++ b/tapl/tests/stlc+lit-tests.rkt @@ -33,7 +33,7 @@ (typecheck-fail (λ ([f : Int]) (f 1 2)) #:with-msg - "Expected type of expression f to match pattern \\(→ τ_in ... τ_out\\), got: Int") + "Expected type of expression to match pattern \\(→ τ_in ... τ_out\\), got: Int") (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) : (→ (→ Int Int Int) Int Int Int)) diff --git a/tapl/tests/stlc+rec-iso-tests.rkt b/tapl/tests/stlc+rec-iso-tests.rkt index 09154c6..c97fbbc 100644 --- a/tapl/tests/stlc+rec-iso-tests.rkt +++ b/tapl/tests/stlc+rec-iso-tests.rkt @@ -1,19 +1,21 @@ #lang s-exp "../stlc+rec-iso.rkt" (require "rackunit-typechecking.rkt") -(define-type-alias IntList (μ (X) (∨ [: "nil" Unit] [: "cons" (× Int X)]))) -(define-type-alias ILBody (∨ [: "nil" Unit] [: "cons" (× Int IntList)])) +(define-type-alias IntList (μ [[X]] (∨ [<> "nil" Unit] [<> "cons" (× Int X)]))) +(define-type-alias ILBody (∨ [<> "nil" Unit] [<> "cons" (× Int IntList)])) + ;; nil (define nil (fld {IntList} (var "nil" = (void) as ILBody))) (check-type nil : IntList) -; cons + +;; cons (define cons (λ ([n : Int] [lst : IntList]) (fld {IntList} (var "cons" = (tup n lst) as ILBody)))) (check-type cons : (→ Int IntList IntList)) (check-type (cons 1 nil) : IntList) (typecheck-fail (cons 1 2)) (typecheck-fail (cons "1" nil)) -; isnil +;; isnil (define isnil (λ ([lst : IntList]) (case (unfld {IntList} lst) @@ -27,7 +29,7 @@ (check-type (λ ([f : (→ IntList Bool)]) (f nil)) : (→ (→ IntList Bool) Bool)) (check-type ((λ ([f : (→ IntList Bool)]) (f nil)) isnil) : Bool ⇒ #t) -; hd +;; hd (define hd (λ ([lst : IntList]) (case (unfld {IntList} lst) @@ -38,7 +40,7 @@ (typecheck-fail (hd 1)) (check-type (hd (cons 11 nil)) : Int ⇒ 11) -; tl +;; tl (define tl (λ ([lst : IntList]) (case (unfld {IntList} lst) @@ -63,59 +65,60 @@ (check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int)) ;; records (ie labeled tuples) +; no records, only 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 (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : +; (× [: "name" String] [: "phone" Int] [: "male?" Bool])) +;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") +; : String ⇒ "Stephen") +;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") +; : String ⇒ "Stephen") +;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone") +; : Int ⇒ 781) +;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?") +; : Bool ⇒ #t) +;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : +; (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) +;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : +; (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) +;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : +; (× [: "name" String] [: "phone" Int] [: "is-male?" Bool])) ;; variants -(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit])) -(check-not-type (var "coffee" = (void) as (∨ [: "coffee" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) -(typecheck-fail ((λ ([x : (∨ [: "coffee" Unit] [: "tea" Unit])]) x) - (var "coffee" = (void) as (∨ [: "coffee" Unit])))) -(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit])) -(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) - : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit])) +(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])) + (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])) + (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])) + (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])) + (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])) + (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])) +(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]))) + (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool]))) ["coffee" x => (+ (+ x x) (+ x x))] ["tea" x => 2] ["coke" y => 3]) @@ -141,7 +144,10 @@ (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 +(typecheck-fail + (proj 1 2) + #:with-msg + "Expected type of expression 1 to match pattern \\(× τ ...), got: Int") ;; ext-stlc.rkt tests --------------------------------------------------------- ;; should still pass diff --git a/tapl/tests/stlc+reco+var-tests.rkt b/tapl/tests/stlc+reco+var-tests.rkt index 9465c91..2c630d4 100644 --- a/tapl/tests/stlc+reco+var-tests.rkt +++ b/tapl/tests/stlc+reco+var-tests.rkt @@ -15,10 +15,10 @@ ; records (ie labeled tuples) (check-type "Stephen" : String) (check-type (tup) : (×)) -(check-type (tup ["name" = "Stephen"]) : (× [~× "name" String])) +(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])) + (× [: "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") @@ -28,53 +28,53 @@ (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])) + (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [~× "name" String] [~× "my-phone" Int] [~× "male?" Bool])) + (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) (check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : - (× [~× "name" String] [~× "phone" Int] [~× "is-male?" Bool])) + (× [: "name" String] [: "phone" Int] [: "is-male?" Bool])) ;; variants -(check-type (var "coffee" = (void) as (∨ [~∨ "coffee" Unit])) : (∨ [~∨ "coffee" Unit])) -(check-not-type (var "coffee" = (void) as (∨ [~∨ "coffee" Unit])) : (∨ [~∨ "coffee" Unit] [~∨ "tea" Unit])) -(typecheck-fail ((λ ([x : (∨ [~∨ "coffee" Unit] [~∨ "tea" Unit])]) x) - (var "coffee" = (void) as (∨ [~∨ "coffee" Unit]))) +(check-type (var "coffee" = (void) as (∨ [<> "coffee" Unit])) : (∨ [<> "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 "Arguments to function.+have wrong type") -(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])) +(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])) + (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])) + (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])) + (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])) + (case (var "coffee" = (void) as (∨ [<> "coffee" Unit] [<> "tea" Unit])) ["coffee" x => "1"] ["tea" x => 2]) #:with-msg "branches have different types") (check-type - (case (var "coffee" = 1 as (∨ [~∨ "coffee" Int] [~∨ "tea" Unit])) + (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])) +(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]))) + (var "coffee" = 1 as (∨ [<> "coffee" Int] [<> "tea" Unit] [<> "coke" Bool]))) ["coffee" x => (+ (+ x x) (+ x x))] ["tea" x => 2] ["coke" y => 3]) @@ -89,18 +89,18 @@ ;; 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 +;;(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 @@ -139,7 +139,7 @@ (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) (typecheck-fail (let* ([x #t] [y (+ x 1)]) 1)) -; letrec +;; letrec (typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y)) (typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x)) diff --git a/tapl/tests/stlc+tup-tests.rkt b/tapl/tests/stlc+tup-tests.rkt index 04882c2..10c3529 100644 --- a/tapl/tests/stlc+tup-tests.rkt +++ b/tapl/tests/stlc+tup-tests.rkt @@ -12,6 +12,7 @@ (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) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 584b195..0a579db 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -4,7 +4,7 @@ syntax/parse racket/syntax syntax/stx "stx-utils.rkt" syntax/parse/debug) - (for-meta 2 racket/base syntax/parse racket/syntax) + (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt") (for-meta 3 racket/base syntax/parse racket/syntax) racket/provide) (provide @@ -66,8 +66,10 @@ [(_ τ:id) #:with τ? (format-id #'τ "~a?" #'τ) #:with τ-internal (generate-temporary #'τ) + #:with inferτ+erase (format-id #'τ "infer~a+erase" #'τ) + #:with τ-cls (generate-temporary #'τ) #'(begin - (provide τ (for-syntax τ?)) + (provide τ (for-syntax τ? inferτ+erase)) (define τ-internal (λ () (raise (exn:fail:type:runtime (format "~a: Cannot use type at run time" 'τ) @@ -75,10 +77,25 @@ (define-syntax (τ stx) (syntax-parse stx [x:id (add-orig #'(#%type (τ-internal)) #'τ)])) - (define-for-syntax (τ? t) - (syntax-parse ((current-type-eval) t) - [((~literal #%plain-type) ((~literal #%plain-app) ty)) - (typecheck? #'ty #'τ-internal)])))])) + (begin-for-syntax + ; expanded form of τ + (define-syntax-class τ-cls + (pattern ((~literal #%plain-type) ((~literal #%plain-app) ty)))) + (define (τ? t) + (syntax-parse ((current-type-eval) t) + [expanded-type + #:declare expanded-type τ-cls + (typecheck? #'expanded-type.ty #'τ-internal)])) + (define (inferτ+erase e) + (syntax-parse (infer+erase e) #:context e + [(e- expanded-type) + #:declare expanded-type τ-cls + #:fail-unless (typecheck? #'expanded-type.ty #'τ-internal) + (format + "~a (~a:~a): Expected type of expression ~v to be ~a, got: ~a" + (syntax-source e) (syntax-line e) (syntax-column e) + (syntax->datum e) (type->str #'τ) (type->str #'expanded-type)) + #'e-]))))])) (begin-for-syntax ;; type validation @@ -114,7 +131,10 @@ (syntax-parse stx [(_ ty tycon cls) #'(syntax-parse ((current-type-eval) ty) - [((~literal #%plain-type) ((~literal #%plain-app) t . args)) + [((~literal #%plain-type) + ((~literal #%plain-lambda) (tv:id (... ...)) + ((~literal let-values) () ((~literal let-values) () + ((~literal #%plain-app) t . args))))) #:declare args cls ; check shape of arguments #:fail-unless (typecheck? #'t #'tycon) ; check tycons match (format "Type error: expected ~a type, got ~a" @@ -123,9 +143,26 @@ [_ #f])])) ) +(begin-for-syntax + (define (bracket? stx) + (define paren-shape/#f (syntax-property stx 'paren-shape)) + (and paren-shape/#f (char=? paren-shape/#f #\[))) + (define-syntax-class bound-vars + (pattern (~and stx [[x:id ...]]) + #:when (and (bracket? #'stx) + (bracket? (stx-car #'stx))))) + (begin-for-syntax + (define (bracket? stx) + (define paren-shape/#f (syntax-property stx 'paren-shape)) + (and paren-shape/#f (char=? paren-shape/#f #\[))) + (define-syntax-class bound-vars + (pattern (~and stx [[x:id ...]]) + #:when (and (bracket? #'stx) + (bracket? (stx-car #'stx))))))) + (define-syntax define-type-constructor (syntax-parser - [(_ (τ:id . pat) + [(_ (τ:id (~optional bvs-pat:bound-vars #:defaults ([bvs-pat.stx #'[[]]])) . pat) ; lits must have ~ prefix (for syntax-parse compat) for now (~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null])) decls ... @@ -134,7 +171,8 @@ #:with τ-match (format-id #'τ "~a-match" #'τ) #:with τ? (format-id #'τ "~a?" #'τ) #:with τ-get (format-id #'τ "~a-get" #'τ) - #:with τ-match+erase (format-id #'τ "~a-match+erase" #'τ) + #:with τ-match+erase (format-id #'τ "infer~a+erase" #'τ) + #:with τ-expander (format-id #'τ "~~~a" #'τ) #:with pat-class (generate-temporary #'τ) ; syntax-class name #:with tycon (generate-temporary #'τ) ; need a runtime id for expansion #:with (lit-tmp ...) (generate-temporaries #'(lit ...)) @@ -145,35 +183,45 @@ (define lit-tmp void) ... (define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ... (provide lit ...) - (provide τ) + (provide τ (for-syntax τ-expander)) (begin-for-syntax - (define-syntax lit + #'(define-syntax lit (pattern-expander (syntax-parser [(_ . xs) - ;#:when (displayln "pattern expanding") #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ... + (define-syntax τ-expander + (pattern-expander + (syntax-parser + [(_ (~optional + (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null])) + . match-pat) + #:with pat-from-constructor (quote-syntax (τ . pat)) + ;; manually replace literals with expanded form, to get around ~ restriction + #:with new-match-pat + #`#,(subst-datum-lits + #`((#,(quote-syntax ~seq) (~literal #%plain-app) (~literal lit-tmp)) ...) + #'(lit ...) + #'match-pat) + #'(~and + (~or + ((~literal #%plain-type) + ((~literal #%plain-lambda) (bvs.x (... ...)) + ((~literal let-values) () ((~literal let-values) () + ((~literal #%plain-app) (~literal tycon) . new-match-pat))))) + (~and any + (~do + (type-error #:src #'any + #:msg + "Expected type of expression to match pattern ~a, got: ~a" + (quote-syntax pat-from-constructor) #'any)))) + ~!)]))) (define-syntax-class pat-class ;; dont check is-type? here; should already be types ;; only check is-type? for user-entered types, eg tycon call ;; thus, dont include decls here, only want shape - #;(pattern (~and pre (~do (printf "trying to match: ~a\n"(syntax->datum #'pre))) pat (~do (displayln "no")))) ; uses "lit" pattern expander - (pattern pat) - #;(pattern any - #:when (printf "trying to match: ~a\n" (syntax->datum #'any)) - #:when (printf "orig: ~a\n" (type->str #'any)) - #:when (printf "against pattern: ~a\n" (syntax->datum (quote-syntax pat))) - #:when (displayln #`(#,(stx-cdr (stx-car #'any)))) - #:when (pretty-print (debug-parse #`(#,(stx-cdr (stx-car #'any))) pat)) - #:with pat #'any) ;#`(#,(stx-cdr (stx-car #'any)))) - #;(pattern any - #:when (displayln "match failed") - #:when (displayln "pat: ") - #:when (displayln (quote-syntax pat)) - #:when (displayln #'any) - #:when (displayln "orig") - #:when (displayln (type->str #'any)) - #:with pat #'any)) + ; uses "lit" pattern expander + (pattern pat)) (define (τ-match ty) (or (match-type ty tycon pat-class) ;; error msg should go in specific macro def? @@ -206,7 +254,10 @@ (format "~a (~a:~a) Expected type with pattern: ~a, got: ~a" (syntax-source #'typ) (syntax-line #'typ) (syntax-column #'typ) (type->str (quote-syntax the-pat)) (type->str #'typ)) - #:with ((~literal #%plain-type) ((~literal #%plain-app) f . args)) + #:with ((~literal #%plain-type) + ((~literal #%plain-lambda) tvs + ((~literal let-values) () ((~literal let-values) () + ((~literal #%plain-app) f . args))))) ((current-type-eval) #'typ) #:declare args pat-class ; check shape of arguments ; #:fail-unless (typecheck? #'f #'tycon) ; check tycons match @@ -218,12 +269,16 @@ (current-continuation-marks))))) (define-syntax (τ stx) (syntax-parse stx #:literals (lit ...) - [(_ . (~and pat !~ args)) ; first check shape + [(_ (~optional (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null])) + . (~and pat !~ args)) ; first check shape ; this inner syntax-parse gets the ~! to register ; otherwise, apparently #:declare's get subst into pat (before ~!) (syntax-parse #'args #:literals (lit ...) [pat #,@#'(decls ...) ; then check declarations (eg, valid type) - #'(#%type (tycon . args))])] + #'(#%type + (λ (bvs.x (... ...)) + (let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...)) + (tycon . args))))])] [_ (type-error #:src stx #:msg (string-append @@ -239,61 +294,61 @@ ;; TODO: refine this to enable specifying arity information ;; type constructors currently must have 1+ arguments -#;(define-syntax (define-type-constructor stx) - (syntax-parse stx - [(_ τ:id (~optional (~seq #:arity n:exact-positive-integer))) - #:with τ? (format-id #'τ "~a?" #'τ) - #:with τ-ref (format-id #'τ "~a-ref" #'τ) - #:with τ-num-args (format-id #'τ "~a-num-args" #'τ) - #:with τ-args (format-id #'τ "~a-args" #'τ) - #:with τ-match (format-id #'τ "~a-match" #'τ) - #:with tmp (generate-temporary #'τ) - #`(begin - ;; TODO: define syntax class instead of these separate tycon fns - (provide τ (for-syntax τ? τ-ref τ-num-args τ-args)) - (define tmp (λ _ (raise (exn:fail:type:runtime - (format "~a: Cannot use type at run time" 'τ) - (current-continuation-marks))))) - (define-syntax (τ stx) - (syntax-parse stx - [x:id - (type-error #:src #'x - #:msg "Cannot use type constructor ~a in non-application position" - #'τ)] - [(_) ; default tycon requires 1+ args - #:when (not #,(attribute n)) - (type-error #:src stx - #:msg "Type constructor must have at least 1 argument.")] - [(_ x (... ...)) - #:when #,(and (attribute n) - #'(not (= n (stx-length #'(x (... ...)))))) - #:with m #,(and (attribute n) #'n) - (type-error #:src stx - #:msg "Type constructor ~a expected ~a argument(s), given: ~a" - #'τ #'m #'(x (... ...)))] - ; this is racket's #%app - [(_ x (... ...)) #'(tmp x (... ...))])) - ; TODO: ok to assume type in canonical (ie, fully expanded) form? - ;; yes for now - (define-for-syntax (τ? stx) - (syntax-parse ((current-promote) stx) - [((~literal #%plain-app) tycon τ_arg (... ...)) (typecheck? #'tycon #'tmp)] - [_ #f])) - (define-for-syntax (τ-ref stx m) - (syntax-parse stx - [((~literal #%plain-app) tycon τ_arg (... ...)) - #:when (typecheck? #'tycon #'tmp) - (stx-list-ref #'(τ_arg (... ...)) m)])) - (define-for-syntax (τ-args stx) - (syntax-parse ((current-promote) stx) - [((~literal #%plain-app) tycon τ_arg (... ...)) - #:when (typecheck? #'tycon #'tmp) - #'(τ_arg (... ...))])) - (define-for-syntax (τ-num-args stx) - (syntax-parse stx - [((~literal #%plain-app) tycon τ_arg (... ...)) - #:when (typecheck? #'tycon #'tmp) - (stx-length #'(τ_arg (... ...)))])))])) +;#;(define-syntax (define-type-constructor stx) +; (syntax-parse stx +; [(_ τ:id (~optional (~seq #:arity n:exact-positive-integer))) +; #:with τ? (format-id #'τ "~a?" #'τ) +; #:with τ-ref (format-id #'τ "~a-ref" #'τ) +; #:with τ-num-args (format-id #'τ "~a-num-args" #'τ) +; #:with τ-args (format-id #'τ "~a-args" #'τ) +; #:with τ-match (format-id #'τ "~a-match" #'τ) +; #:with tmp (generate-temporary #'τ) +; #`(begin +; ;; TODO: define syntax class instead of these separate tycon fns +; (provide τ (for-syntax τ? τ-ref τ-num-args τ-args)) +; (define tmp (λ _ (raise (exn:fail:type:runtime +; (format "~a: Cannot use type at run time" 'τ) +; (current-continuation-marks))))) +; (define-syntax (τ stx) +; (syntax-parse stx +; [x:id +; (type-error #:src #'x +; #:msg "Cannot use type constructor ~a in non-application position" +; #'τ)] +; [(_) ; default tycon requires 1+ args +; #:when (not #,(attribute n)) +; (type-error #:src stx +; #:msg "Type constructor must have at least 1 argument.")] +; [(_ x (... ...)) +; #:when #,(and (attribute n) +; #'(not (= n (stx-length #'(x (... ...)))))) +; #:with m #,(and (attribute n) #'n) +; (type-error #:src stx +; #:msg "Type constructor ~a expected ~a argument(s), given: ~a" +; #'τ #'m #'(x (... ...)))] +; ; this is racket's #%app +; [(_ x (... ...)) #'(tmp x (... ...))])) +; ; TODO: ok to assume type in canonical (ie, fully expanded) form? +; ;; yes for now +; (define-for-syntax (τ? stx) +; (syntax-parse ((current-promote) stx) +; [((~literal #%plain-app) tycon τ_arg (... ...)) (typecheck? #'tycon #'tmp)] +; [_ #f])) +; (define-for-syntax (τ-ref stx m) +; (syntax-parse stx +; [((~literal #%plain-app) tycon τ_arg (... ...)) +; #:when (typecheck? #'tycon #'tmp) +; (stx-list-ref #'(τ_arg (... ...)) m)])) +; (define-for-syntax (τ-args stx) +; (syntax-parse ((current-promote) stx) +; [((~literal #%plain-app) tycon τ_arg (... ...)) +; #:when (typecheck? #'tycon #'tmp) +; #'(τ_arg (... ...))])) +; (define-for-syntax (τ-num-args stx) +; (syntax-parse stx +; [((~literal #%plain-app) tycon τ_arg (... ...)) +; #:when (typecheck? #'tycon #'tmp) +; (stx-length #'(τ_arg (... ...)))])))])) ;; syntax classes (begin-for-syntax @@ -471,17 +526,31 @@ (define-for-syntax (mk-pred x) (format-id x "~a?" x)) (define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field)) -; subst τ for y in e, if (bound-id=? x y) -(define-for-syntax (subst τ x e) - (syntax-parse e - [y:id #:when (bound-identifier=? e x) τ] - [(esub ...) - #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...)) - (syntax-track-origin #'(esub_subst ...) e x)] - [_ e])) +(begin-for-syntax + ; subst τ for y in e, if (bound-id=? x y) + (define (subst τ x e) + (syntax-parse e + [y:id #:when (bound-identifier=? e x) τ] + [(esub ...) + #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...)) + (syntax-track-origin #'(esub_subst ...) e x)] + [_ e])) + + (define (substs τs xs e) + (stx-fold subst e τs xs)) + + ; subst τ for y in e, if (equal? (syntax-e x) (syntax-e y)) + (define-for-syntax (subst-datum-lit τ x e) + (syntax-parse e + [y:id #:when (equal? (syntax-e e) (syntax-e x)) τ] + [(esub ...) + #:with (esub_subst ...) (stx-map (λ (e1) (subst-datum-lit τ x e1)) #'(esub ...)) + (syntax-track-origin #'(esub_subst ...) e x)] + [_ e])) + + (define-for-syntax (subst-datum-lits τs xs e) + (stx-fold subst-datum-lit e τs xs))) -(define-for-syntax (substs τs xs e) - (stx-fold subst e τs xs)) ;; type environment ----------------------------------------------------------- #;(begin-for-syntax