From 75b4dae95f271c7aaa955300a62778b19da1b3e4 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 4 Aug 2015 18:24:33 -0400 Subject: [PATCH] use new define-type-constructor and #%type in stlc+box --- tapl/stlc+box.rkt | 12 +++---- tapl/tests/run-all-tests.rkt | 2 +- tapl/tests/stlc+box-tests.rkt | 63 +++++++++++++++++----------------- tapl/tests/stlc+cons-tests.rkt | 6 ++-- 4 files changed, 42 insertions(+), 41 deletions(-) diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt index 26a7bb1..cc4e769 100644 --- 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 index 94fc405..c459991 100644 --- 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 index 4751e13..7c600ea 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]) @@ -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 index 24ecc9d..3553bcc 100644 --- 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)