commit c151463a6f88ad5d3eed80b1c46254d0a0dd8980
parent a12e85d4bc691b5ba7572915895543a61c7f3f6d
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 4 Aug 2015 17:31:36 -0400
use #%type in stlc+reco+var.rkt; tests passing
Diffstat:
3 files changed, 176 insertions(+), 163 deletions(-)
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
@@ -7,7 +7,7 @@
(provide (except-out (all-from-out "stlc+tup.rkt")
stlc:#%app stlc:let stlc:begin stlc:tup stlc:proj
(for-syntax stlc:type=?)))
-(provide tup proj); var case)
+(provide tup proj var case)
(provide (for-syntax type=?))
@@ -56,7 +56,7 @@
; re-define tuples as records
(define-type-constructor
- (× [~$ label τ_fld] ...) #:lits (~$)
+ (× [~× label τ_fld] ...) #:lits (~×)
#:declare label str
#:declare τ_fld type
)
@@ -68,12 +68,12 @@
(syntax-parse stx #:datum-literals (=)
[(_ [l:str = e] ...)
#:with ([e- τ] ...) (infers+erase #'(e ...))
- (⊢ (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 ~!)
+ [(_ 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)))
@@ -86,32 +86,39 @@
#;[(_ e ...) #'(stlc:proj e ...)]))
-#;(define-type-constructor (∨ [: label τ] ...))
+(define-type-constructor
+ (∨ [~∨ label τ_var] ...) #:lits (~∨)
+ #:declare label str
+ #:declare τ_var type)
-#;(define-syntax (var stx)
+(define-syntax (var stx)
(syntax-parse stx #:datum-literals (as =) #:literals (quote)
[(_ l:str = e as τ:type)
- #:when (∨? #'τ.norm)
- #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.norm))
+; #:when (∨? #'τ.norm)
+; #:with (['l_τ:str τ_l] ...) (stx-map :-args (∨-args #'τ.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)
- (⊢ #'(list l e) #'τ.norm)]))
-#;(define-syntax (case stx)
+ (⊢ (list l e) : τ)]))
+(define-syntax (case stx)
(syntax-parse stx #:datum-literals (of =>) #:literals (quote)
[(_ e [l:str x => e_l] ...)
#:fail-when (null? (syntax->list #'(l ...))) "no clauses"
#:with (e- τ_e) (infer+erase #'e)
- #:when (∨? #'τ_e)
- #:with (['l_x:str τ_x] ...) (stx-map :-args (∨-args #'τ_e))
+ #: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))
#:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
#:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
#:with (((x-) e_l- τ_el) ...)
(stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
#:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
- (⊢ #'(let ([l_e (car e-)])
- (cond [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...))
- (stx-car #'(τ_el ...)))]))
+ (⊢ (let ([l_e (car e-)])
+ (cond [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...))
+ : #,(stx-car #'(τ_el ...)))]))
(define-syntax (define/tc stx)
(syntax-parse stx
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
@@ -6,21 +6,21 @@
(require "ext-stlc-tests.rkt")
(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 "exist-tests.rkt")
-
-;; subtyping
-(require "stlc+sub-tests.rkt")
-(require "stlc+reco+sub-tests.rkt")
-(require "fsub-tests.rkt")
-
-;; system F
-(require "sysf-tests.rkt")
-
-;; F_omega
-(require "fomega-tests.rkt")
-(require "fomega2-tests.rkt")
-\ No newline at end of file
+;(require "stlc+cons-tests.rkt")
+;(require "stlc+box-tests.rkt")
+;
+;(require "stlc+rec-iso-tests.rkt")
+;
+;(require "exist-tests.rkt")
+;
+;;; subtyping
+;(require "stlc+sub-tests.rkt")
+;(require "stlc+reco+sub-tests.rkt")
+;(require "fsub-tests.rkt")
+;
+;;; system F
+;(require "sysf-tests.rkt")
+;
+;;; F_omega
+;(require "fomega-tests.rkt")
+;(require "fomega2-tests.rkt")
+\ No newline at end of file
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,58 +28,64 @@
(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] [: "tea" Unit])) : (∨ [: "coffee" Unit] [: "tea" Unit]))
-;(check-type (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
-; : (∨ [: "coffee" Unit] [: "tea" Unit] [: "coke" Unit]))
-;
-;(typecheck-fail
-; (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
-; ["coffee" x => 1])) ; not enough clauses
-;(typecheck-fail
-; (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
-; ["coffee" x => 1]
-; ["teaaaaaa" x => 2])) ; wrong clause
-;(typecheck-fail
-; (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
-; ["coffee" x => 1]
-; ["tea" x => 2]
-; ["coke" x => 3])) ; too many clauses
-;(typecheck-fail
-; (case (var "coffee" = (void) as (∨ [: "coffee" Unit] [: "tea" Unit]))
-; ["coffee" x => "1"]
-; ["tea" x => 2])) ; mismatched branch types
-;(check-type
-; (case (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit]))
-; ["coffee" x => x]
-; ["tea" x => 2]) : Int ⇒ 1)
-;(define-type-alias Drink (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool]))
-;(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
-;(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
-;(check-type
-; (case ((λ ([d : Drink]) d)
-; (var "coffee" = 1 as (∨ [: "coffee" Int] [: "tea" Unit] [: "coke" Bool])))
-; ["coffee" x => (+ (+ x x) (+ x x))]
-; ["tea" x => 2]
-; ["coke" y => 3])
-; : Int ⇒ 4)
-;
-;(check-type
-; (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
-; ["coffee" x => (+ (+ x x) (+ x x))]
-; ["tea" x => 2]
-; ["coke" y => 3])
-; : Int ⇒ 4)
+(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]))
+
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ [~∨ "coffee" Unit] [~∨ "tea" Unit]))
+ ["coffee" x => 1])
+ #:with-msg "wrong number of case clauses")
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ [~∨ "coffee" Unit] [~∨ "tea" Unit]))
+ ["coffee" x => 1]
+ ["teaaaaaa" x => 2])
+ #:with-msg "case clauses not exhaustive")
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ [~∨ "coffee" Unit] [~∨ "tea" Unit]))
+ ["coffee" x => 1]
+ ["tea" x => 2]
+ ["coke" x => 3])
+ #:with-msg "wrong number of case clauses")
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ [~∨ "coffee" Unit] [~∨ "tea" Unit]))
+ ["coffee" x => "1"]
+ ["tea" x => 2])
+ #:with-msg "branches have different types")
+(check-type
+ (case (var "coffee" = 1 as (∨ [~∨ "coffee" Int] [~∨ "tea" Unit]))
+ ["coffee" x => x]
+ ["tea" x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ [~∨ "coffee" Int] [~∨ "tea" Unit] [~∨ "coke" Bool]))
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
+(check-type
+ (case ((λ ([d : Drink]) d)
+ (var "coffee" = 1 as (∨ [~∨ "coffee" Int] [~∨ "tea" Unit] [~∨ "coke" Bool])))
+ ["coffee" x => (+ (+ x x) (+ x x))]
+ ["tea" x => 2]
+ ["coke" y => 3])
+ : Int ⇒ 4)
+
+(check-type
+ (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
+ ["coffee" x => (+ (+ x x) (+ x x))]
+ ["tea" x => 2]
+ ["coke" y => 3])
+ : Int ⇒ 4)
;; previous tuple tests: ------------------------------------------------------------
;; wont work anymore
@@ -100,85 +106,85 @@
;; should still pass
;; new literals and base types
-;(check-type "one" : String) ; literal now supported
-;(check-type #f : Bool) ; literal now supported
-;
-;(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
-;
-;;; Unit
-;(check-type (void) : Unit)
-;(check-type void : (→ Unit))
-;(typecheck-fail ((λ ([x : Unit]) x) 2))
-;(typecheck-fail ((λ ([x : Unit])) void))
-;(check-type ((λ ([x : Unit]) x) (void)) : Unit)
-;
-;;; begin
-;(typecheck-fail (begin))
-;(check-type (begin 1) : Int)
-;(typecheck-fail (begin 1 2 3))
-;(check-type (begin (void) 1) : Int ⇒ 1)
-;
-;;;ascription
-;(typecheck-fail (ann 1 : Bool))
-;(check-type (ann 1 : Int) : Int ⇒ 1)
-;(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
-;
+(check-type "one" : String) ; literal now supported
+(check-type #f : Bool) ; literal now supported
+
+(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
+
+;; Unit
+(check-type (void) : Unit)
+(check-type void : (→ Unit))
+(typecheck-fail ((λ ([x : Unit]) x) 2))
+(typecheck-fail ((λ ([x : Unit])) void))
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(typecheck-fail (begin))
+(check-type (begin 1) : Int)
+(typecheck-fail (begin 1 2 3))
+(check-type (begin (void) 1) : Int ⇒ 1)
+
+;;ascription
+(typecheck-fail (ann 1 : Bool))
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+
;; let
-;(check-type (let () (+ 1 1)) : Int ⇒ 2)
-;(check-type (let ([x 10]) (+ 1 2)) : Int)
-;(typecheck-fail (let ([x #f]) (+ x 1)))
-;(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
-;(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
-;
-;(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
-;(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
-;
-;; letrec
-;(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
-;(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
-;
-;(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
-;
-;;; recursive
-;(check-type
-; (letrec ([(countdown : (→ Int String))
-; (λ ([i : Int])
-; (if (= i 0)
-; "liftoff"
-; (countdown (- i 1))))])
-; (countdown 10)) : String ⇒ "liftoff")
-;
-;;; mutually recursive
-;(check-type
-; (letrec ([(is-even? : (→ Int Bool))
-; (λ ([n : Int])
-; (or (zero? n)
-; (is-odd? (sub1 n))))]
-; [(is-odd? : (→ Int Bool))
-; (λ ([n : Int])
-; (and (not (zero? n))
-; (is-even? (sub1 n))))])
-; (is-odd? 11)) : Bool ⇒ #t)
-;
-;;; tests from stlc+lit-tests.rkt --------------------------
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(typecheck-fail (let ([x #f]) (+ x 1)))
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
+
+; letrec
+(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
+(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
+
+(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+
+;; recursive
+(check-type
+ (letrec ([(countdown : (→ Int String))
+ (λ ([i : Int])
+ (if (= i 0)
+ "liftoff"
+ (countdown (- i 1))))])
+ (countdown 10)) : String ⇒ "liftoff")
+
+;; mutually recursive
+(check-type
+ (letrec ([(is-even? : (→ Int Bool))
+ (λ ([n : Int])
+ (or (zero? n)
+ (is-odd? (sub1 n))))]
+ [(is-odd? : (→ Int Bool))
+ (λ ([n : Int])
+ (and (not (zero? n))
+ (is-even? (sub1 n))))])
+ (is-odd? 11)) : Bool ⇒ #t)
+
+;; tests from stlc+lit-tests.rkt --------------------------
;; most should pass, some failing may now pass due to added types/forms
-;(check-type 1 : Int)
-;;(check-not-type 1 : (Int → Int))
-;;(typecheck-fail "one") ; literal now supported
-;;(typecheck-fail #f) ; literal now supported
-;(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
-;(check-not-type (λ ([x : Int]) x) : Int)
-;(check-type (λ ([x : Int]) x) : (→ Int Int))
-;(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
-;(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail "one") ; literal now supported
+;(typecheck-fail #f) ; literal now supported
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type
-;;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
-;(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
-;(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
-; : (→ (→ Int Int Int) Int Int Int))
-;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
-;(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
-;(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
-;(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
-;(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
-;
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+ : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
