commit 3d4fe8f71a487f40fa97145e122bb01215fa7439
parent 0dde065949bf910fb5408171af53e9a48dbf41d2
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 7 Aug 2015 18:12:47 -0400
new define-type-constructor: exist-tests.rkt passing
Diffstat:
4 files changed, 94 insertions(+), 81 deletions(-)
diff --git a/tapl/exist.rkt b/tapl/exist.rkt
@@ -26,25 +26,28 @@
(current-typecheck-relation type=?))
;; TODO: disambiguate expanded representation of ∃, ok to use lambda in this calculus
-(provide ∃)
-(define-syntax (∃ stx)
- (syntax-parse stx
- [(_ (tv:id) body)
- (syntax/loc stx (#%plain-lambda (tv) body))]))
+(define-type-constructor (∃ [[X]] τ_body))
+;(provide ∃)
+;(define-syntax (∃ stx)
+; (syntax-parse stx
+; [(_ (tv:id) body)
+; (syntax/loc stx (#%plain-lambda (tv) body))]))
(define-syntax (pack stx)
(syntax-parse stx
[(_ (τ:type e) as ∃τ:type)
- #:with (#%plain-lambda (τ_abstract:id) τ_body) #'∃τ.norm
+ #:with (~∃ [[τ_abstract]] τ_body) #'∃τ.norm
+; #:with (#%plain-lambda (τ_abstract:id) τ_body) #'∃τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body))
- (⊢ #'e- #'∃τ)]))
+ (⊢ e- : ∃τ)]))
(define-syntax (open stx)
(syntax-parse stx #:datum-literals (<=)
[(_ ([(tv:id x:id) <= e_packed]) e)
- #:with [e_packed- τ_packed] (infer+erase #'e_packed)
- #:with (#%plain-lambda (τ_abstract:id) τ_body) #'τ_packed ; existential
+ #:with [e_packed- (~∃ [[τ_abstract]] τ_body)] (infer+erase #'e_packed)
+; #:with [e_packed- τ_packed] (infer+erase #'e_packed)
+; #:with (#%plain-lambda (τ_abstract:id) τ_body) #'τ_packed ; existential
;; The subst below appears to be a hack, but it's not really.
;; It's the (TaPL) type rule itself that is fast and loose.
;; Leveraging the macro system's management of binding reveals this.
@@ -91,4 +94,4 @@
#:with [tvs- (x-) (e-) (τ_e)]
(infer #'(e) #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)])
#:tvs #'(tv))
- (⊢ #'(let ([x- e_packed-]) e-) #'τ_e)]))
-\ No newline at end of file
+ (⊢ (let ([x- e_packed-]) e-) : τ_e)]))
+\ No newline at end of file
diff --git a/tapl/tests/exist-tests.rkt b/tapl/tests/exist-tests.rkt
@@ -1,39 +1,39 @@
#lang s-exp "../exist.rkt"
(require "rackunit-typechecking.rkt")
-(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (X) X))
-(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (Y) Y))
-(typecheck-fail (pack (Int 0) as (∃ (X) Y)))
-(check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X))
-(typecheck-fail (pack (Int #t) as (∃ (X) X)))
+(check-type (pack (Int 0) as (∃ [[X]] X)) : (∃ [[X]] X))
+(check-type (pack (Int 0) as (∃ [[X]] X)) : (∃ [[Y]] Y))
+(typecheck-fail (pack (Int 0) as (∃ [[X]] Y)))
+(check-type (pack (Bool #t) as (∃ [[X]] X)) : (∃ [[X]] X))
+(typecheck-fail (pack (Int #t) as (∃ [[X]] X)))
; cant typecheck bc X has local scope, and no X elimination form
-;(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) x) : X)
+;(check-type (open ([(X x) <= (pack (Int 0) as (∃ [[X]] X))]) x) : X)
(check-type 0 : Int)
(check-type (+ 0 1) : Int ⇒ 1)
(check-type ((λ ([x : Int]) (+ x 1)) 0) : Int ⇒ 1)
-(typecheck-fail (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) (+ x 1))) ; can't use as Int
+(typecheck-fail (open ([(X x) <= (pack (Int 0) as (∃ [[X]] X))]) (+ x 1))) ; can't use as Int
-(check-type (λ ([x : (∃ (X) X)]) x) : (→ (∃ (X) X) (∃ (Y) Y)))
-(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Int 0) as (∃ (Z) Z)))
- : (∃ (X) X) ⇒ 0)
-(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Bool #t) as (∃ (Z) Z)))
- : (∃ (X) X) ⇒ #t)
+(check-type (λ ([x : (∃ [[X]] X)]) x) : (→ (∃ [[X]] X) (∃ [[Y]] Y)))
+(check-type ((λ ([x : (∃ [[X]] X)]) x) (pack (Int 0) as (∃ [[Z]] Z)))
+ : (∃ [[X]] X) ⇒ 0)
+(check-type ((λ ([x : (∃ [[X]] X)]) x) (pack (Bool #t) as (∃ [[Z]] Z)))
+ : (∃ [[X]] X) ⇒ #t)
;; example where the two binding X's are conflated, see exist.rkt for explanation
-(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) ((λ ([y : X]) 1) x))
+(check-type (open ([(X x) <= (pack (Int 0) as (∃ [[X]] X))]) ((λ ([y : X]) 1) x))
: Int ⇒ 1)
(check-type
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ (X) (× [: "a" X] [: "f" (→ X X)])))
- : (∃ (X) (× [: "a" X] [: "f" (→ X X)])))
+ as (∃ [[X]] (× [: "a" X] [: "f" (→ X X)])))
+ : (∃ [[X]] (× [: "a" X] [: "f" (→ X X)])))
(define p4
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ (X) (× [: "a" X] [: "f" (→ X Int)]))))
-(check-type p4 : (∃ (X) (× [: "a" X] [: "f" (→ X Int)])))
+ as (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)]))))
+(check-type p4 : (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)])))
(check-not-type (open ([(X x) <= p4]) (proj x "a")) : Int) ; type is X, not Int
; type is (→ X X), not (→ Int Int)
@@ -43,37 +43,37 @@
(check-type (open ([(X x) <= p4]) ((λ ([y : X]) ((proj x "f") y)) (proj x "a"))) : Int ⇒ 6)
(check-type
- (open ([(X x) <= (pack (Int 0) as (∃ (Y) Y))])
+ (open ([(X x) <= (pack (Int 0) as (∃ [[Y]] Y))])
((λ ([y : X]) 1) x))
: Int ⇒ 1)
(check-type
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ (X) (× [: "a" Int] [: "f" (→ Int Int)])))
- : (∃ (X) (× [: "a" Int] [: "f" (→ Int Int)])))
+ as (∃ [[X]] (× [: "a" Int] [: "f" (→ Int Int)])))
+ : (∃ [[X]] (× [: "a" Int] [: "f" (→ Int Int)])))
(typecheck-fail
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ (X) (× [: "a" Int] [: "f" (→ Bool Int)]))))
+ as (∃ [[X]] (× [: "a" Int] [: "f" (→ Bool Int)]))))
(typecheck-fail
(pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
- as (∃ (X) (× [: "a" X] [: "f" (→ X Bool)]))))
+ as (∃ [[X]] (× [: "a" X] [: "f" (→ X Bool)]))))
(check-type
(pack (Bool (tup ["a" = #t] ["f" = (λ ([x : Bool]) (if x 1 2))]))
- as (∃ (X) (× [: "a" X] [: "f" (→ X Int)])))
- : (∃ (X) (× [: "a" X] [: "f" (→ X Int)])))
+ as (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)])))
+ : (∃ [[X]] (× [: "a" X] [: "f" (→ X Int)])))
(define counterADT
(pack (Int (tup ["new" = 1]
["get" = (λ ([i : Int]) i)]
["inc" = (λ ([i : Int]) (+ i 1))]))
- as (∃ (Counter) (× [: "new" Counter]
+ as (∃ [[Counter]] (× [: "new" Counter]
[: "get" (→ Counter Int)]
[: "inc" (→ Counter Counter)]))))
(check-type counterADT :
- (∃ (Counter) (× [: "new" Counter]
+ (∃ [[Counter]] (× [: "new" Counter]
[: "get" (→ Counter Int)]
[: "inc" (→ Counter Counter)])))
(check-type
@@ -107,7 +107,7 @@
["read" = (λ ([c : Counter]) (is-even? (get c)))]
["toggle" = (λ ([c : Counter]) (inc c))]
["reset" = (λ ([c : Counter]) (new))]))
- as (∃ (FlipFlop) (× [: "new" FlipFlop]
+ as (∃ [[FlipFlop]] (× [: "new" FlipFlop]
[: "read" (→ FlipFlop Bool)]
[: "toggle" (→ FlipFlop FlipFlop)]
[: "reset" (→ FlipFlop FlipFlop)])))])
@@ -121,11 +121,11 @@
(tup ["new" = (tup ["x" = 1])]
["get" = (λ ([i : (× [: "x" Int])]) (proj i "x"))]
["inc" = (λ ([i : (× [: "x" Int])]) (tup ["x" = (+ 1 (proj i "x"))]))]))
- as (∃ (Counter) (× [: "new" Counter]
+ as (∃ [[Counter]] (× [: "new" Counter]
[: "get" (→ Counter Int)]
[: "inc" (→ Counter Counter)]))))
(check-type counterADT2 :
- (∃ (Counter) (× [: "new" Counter]
+ (∃ [[Counter]] (× [: "new" Counter]
[: "get" (→ Counter Int)]
[: "inc" (→ Counter Counter)])))
@@ -148,7 +148,7 @@
["read" = (λ ([c : Counter]) (is-even? (get c)))]
["toggle" = (λ ([c : Counter]) (inc c))]
["reset" = (λ ([c : Counter]) (new))]))
- as (∃ (FlipFlop) (× [: "new" FlipFlop]
+ as (∃ [[FlipFlop]] (× [: "new" FlipFlop]
[: "read" (→ FlipFlop Bool)]
[: "toggle" (→ FlipFlop FlipFlop)]
[: "reset" (→ FlipFlop FlipFlop)])))])
@@ -189,40 +189,40 @@
(× [: "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])
@@ -237,18 +237,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
+;; old tuple syntax not supported here
+;(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/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
@@ -12,8 +12,8 @@
(require "stlc+rec-iso-tests.rkt")
;(require "exist-tests.rkt")
-;
-;;; subtyping
+
+;; subtyping
;(require "stlc+sub-tests.rkt")
;(require "stlc+reco+sub-tests.rkt")
;(require "fsub-tests.rkt")
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -162,7 +162,9 @@
(define-syntax define-type-constructor
(syntax-parser
- [(_ (τ:id (~optional bvs-pat:bound-vars #:defaults ([bvs-pat.stx #'[[]]])) . pat)
+ [(_ (τ:id (~optional (~and bvs-pat:bound-vars bvs-test)
+ #:defaults ([bvs-pat.stx #'[[]]]))
+ . pat)
; lits must have ~ prefix (for syntax-parse compat) for now
(~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
decls ...
@@ -269,7 +271,8 @@
(current-continuation-marks)))))
(define-syntax (τ stx)
(syntax-parse stx #:literals (lit ...)
- [(_ (~optional (~and bvs:bound-vars bvs-pat.stx) #:defaults ([(bvs.x 1) null]))
+ [(_ (~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 ~!)
@@ -280,6 +283,10 @@
(let-syntax ([bvs.x (syntax-parser [bvs.x:id #'(#%type bvs.x)])] (... ...))
(tycon . args))))])]
[_
+ #:with expected-pat
+ #,(if (attribute bvs-test)
+ #'(quote-syntax (τ bvs-pat.stx . pat))
+ #'(quote-syntax (τ . pat)))
(type-error #:src stx
#:msg (string-append
"Improper usage of type constructor ~a: ~a, expected pattern ~a, "
@@ -290,7 +297,7 @@
(λ (typ clss) (format "~a is a ~a" typ clss))
#'(ty (... ...)) #'(cls (... ...)))
", ")))
- #'τ stx (quote-syntax (τ . pat)))])))]))
+ #'τ stx #'expected-pat)])))]))
;; TODO: refine this to enable specifying arity information
;; type constructors currently must have 1+ arguments
@@ -429,6 +436,7 @@
(syntax-parse ctx #:datum-literals (:)
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
#:with (e ...) es
+ #:with (tv ...) tvs
#:with
; old expander pattern
#;((~literal #%plain-lambda) tvs+
@@ -439,16 +447,17 @@
((~literal #%expression) e+) ...)))))
; new expander pattern
((~literal #%plain-lambda) tvs+
- ((~literal #%expression)
- ((~literal #%plain-lambda) xs+
- ((~literal let-values) ()
- ((~literal let-values) ()
- ((~literal #%expression) e+) ...)))))
+ ((~literal let-values) () ((~literal let-values) ()
+ ((~literal #%expression)
+ ((~literal #%plain-lambda) xs+
+ ((~literal let-values) () ((~literal let-values) ()
+ ((~literal #%expression) e+) ...)))))))
(expand/df
- #`(λ #,tvs
- (λ (x ...)
- (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ #:tag '#,tag))] ...)
- (#%expression e) ...))))
+ #`(λ (tv ...)
+ (let-syntax ([tv (syntax-parser [tv:id #'(#%type tv)])] ...)
+ (λ (x ...)
+ (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ #:tag '#,tag))] ...)
+ (#%expression e) ...)))))
(list #'tvs+ #'xs+ #'(e+ ...)
(stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
[([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvs tvs)]))
