commit 75b4dae95f271c7aaa955300a62778b19da1b3e4
parent 6e91837992269d955d024f32e6a1e483e704bfd2
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 4 Aug 2015 18:24:33 -0400
use new define-type-constructor and #%type in stlc+box
Diffstat:
4 files changed, 43 insertions(+), 42 deletions(-)
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
@@ -13,24 +13,24 @@
;; Terms:
;; - terms from stlc+cons.rkt
-(define-type-constructor Ref #:arity 1)
+(define-type-constructor (Ref τ) #:declare τ type)
(define-syntax (ref stx)
(syntax-parse stx
[(_ e)
#:with (e- τ) (infer+erase #'e)
- (⊢ #'(box e-) #'(Ref τ))]))
+ (⊢ (box e-) : (Ref τ))]))
(define-syntax (deref stx)
(syntax-parse stx
[(_ e)
#:with (e- ref-τ) (infer+erase #'e)
- #:with (τ) (Ref-args #'ref-τ)
- (⊢ #'(unbox 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-args #'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
+ (⊢ (set-box! e_ref- e-) : Unit)]))
+\ No newline at end of file
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
@@ -6,7 +6,7 @@
(require "ext-stlc-tests.rkt")
(require "stlc+tup-tests.rkt")
(require "stlc+reco+var-tests.rkt")
-;(require "stlc+cons-tests.rkt")
+(require "stlc+cons-tests.rkt")
;(require "stlc+box-tests.rkt")
;
;(require "stlc+rec-iso-tests.rkt")
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])
@@ -116,18 +116,19 @@
;; previous tests: ------------------------------------------------------------
;; tests for tuples -----------------------------------------------------------
-(check-type (tup 1 2 3) : (× Int Int Int))
-(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
-(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
-(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
-(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
-(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
-
-(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
-(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
-(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
-(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
-(typecheck-fail (proj 1 2)) ; not tuple
+; fail bc tuple changed syntax
+;(check-type (tup 1 2 3) : (× Int Int Int))
+;(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
+;(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
+;
+;(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
+;(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
+;(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
+;(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
+;(typecheck-fail (proj 1 2)) ; not tuple
;; ext-stlc.rkt tests ---------------------------------------------------------
;; should still pass
diff --git a/tapl/tests/stlc+cons-tests.rkt b/tapl/tests/stlc+cons-tests.rkt
@@ -130,10 +130,10 @@
;; should still pass
;; new literals and base types
-;(check-type "one" : String) ; literal now supported
-;(check-type #f : Bool) ; literal now supported
+(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
+(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
;; Unit
(check-type (void) : Unit)
