commit 0dde065949bf910fb5408171af53e9a48dbf41d2
parent 75b4dae95f271c7aaa955300a62778b19da1b3e4
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 7 Aug 2015 17:26:53 -0400
new define-type-constructor: support binding forms
- tests passing up to stlc+rec-iso.rkt
Diffstat:
16 files changed, 385 insertions(+), 281 deletions(-)
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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]))
-
-(define-for-syntax (substs τs xs e)
- (stx-fold subst e τs xs))
+(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)))
+
;; type environment -----------------------------------------------------------
#;(begin-for-syntax
