commit 4dd2b66d2b1bfd2e024703f5607b4795a98f31e1
parent a07fa92d25c1379592e17099c88930db884f7eb5
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 14 Oct 2015 14:55:12 -0400
generalize fomega ty= to avoid specific types; add tests
- fixes fomega bug where kind annotations were not being compared
- fix subst bug: must tranfer props (ie types) when replacing an id
- add exist tests to check proper subst in ty=
Diffstat:
5 files changed, 32 insertions(+), 15 deletions(-)
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -69,19 +69,16 @@
(define (type=? t1 t2)
(or (and (★? t1) (#%type? t2))
(and (#%type? t1) (★? t2))
- (and (syntax-parse (list t1 t2) #:datum-literals (:)
- [((~∀ ([tv1 : k1]) tbody1)
- (~∀ ([tv2 : k2]) tbody2))
- ((current-type=?) #'k1 #'k2)]
- [_ #t])
- (old-type=? t1 t2))))
+ (let ([k1 (typeof t1)][k2 (typeof t2)])
+ (and (or (and (not k1) (not k2))
+ (and k1 k2 ((current-type=?) k1 k2)))
+ (old-type=? t1 t2)))))
(current-type=? type=?)
(current-typecheck-relation (current-type=?)))
(define-typed-syntax Λ
[(_ bvs:kind-ctx e)
- #:with ((tv- ...) e- τ_e)
- (infer/ctx+erase #'bvs #'e)
+ #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e)
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
(define-typed-syntax inst
@@ -100,10 +97,11 @@
(define-typed-syntax tyλ
[(_ bvs:kind-ctx τ_body)
#:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
- #:when ((current-kind?) #'k_body)
+ #:fail-unless ((current-kind?) #'k_body)
+ (format "not a valid kind: ~a\n" (type->str #'k_body))
(⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))])
-(define-typed-syntax tyapp #:export-as tyapp
+(define-typed-syntax tyapp
[(_ τ_fn τ_arg ...)
#:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
#:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
diff --git a/tapl/tests/exist-tests.rkt b/tapl/tests/exist-tests.rkt
@@ -7,6 +7,16 @@
(check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X))
(typecheck-fail (pack (Int #t) as (∃ (X) X)))
+(check-type (pack (Int (pack (Int 0) as (∃ (X) X))) as (∃ (Y) (∃ (X) X)))
+ : (∃ (Y) (∃ (X) X)))
+(check-type (pack (Int +) as (∃ (X) (→ X Int Int))) : (∃ (X) (→ X Int Int)))
+(check-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int))))
+ as (∃ (Y) (∃ (X) (→ X Y Int))))
+ : (∃ (Y) (∃ (X) (→ X Y Int))))
+(check-not-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int))))
+ as (∃ (Y) (∃ (X) (→ X Y Int))))
+ : (∃ (X) (∃ (X) (→ X X Int))))
+
; 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)
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
@@ -9,6 +9,12 @@
(typecheck-fail (→ 1))
(check-type 1 : Int)
+(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid kind: Int")
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) :
+ (∀ ([X : (∀★ ★)]) (→ X X)))
+
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
diff --git a/tapl/tests/fomega2-tests.rkt b/tapl/tests/fomega2-tests.rkt
@@ -9,6 +9,9 @@
(typecheck-fail (→ 1))
(check-type 1 : Int)
+;; this should error but it doesnt
+#;(λ ([x : ★]) 1)
+
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -136,7 +136,9 @@
;; typeof : Syntax -> Type or #f
;; Retrieves type of given stx, or #f if input has not been assigned a type.
- (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
+ (define (typeof stx #:tag [tag 'type])
+ (define ty (syntax-property stx tag))
+ (if (cons? ty) (car ty) ty))
;; - infers type of e
;; - checks that type of e matches the specified type
@@ -457,9 +459,7 @@
(format "wrong number of type vars, expected ~a ~a" 'bvs-op 'bvs-n)
#:fail-unless (op (stx-length #'args) n)
(format "wrong number of arguments, expected ~a ~a" 'op 'n)
- #:with (bvs- τs- _)
- (infers/ctx+erase #'bvs #'args) ;#'([bv : #%kind] (... ...)) #'args
-; #:expand (current-type-eval))
+ #:with (bvs- τs- _) (infers/ctx+erase #'bvs #'args)
#:with (~! (~var _ kind) (... ...)) #'τs-
#:with ([tv (~datum :) k_arg] (... ...)) #'bvs
; #:with (k_arg+ (... ...)) (stx-map (current-type-eval) #'(k_arg (... ...)))
@@ -572,7 +572,7 @@
; subst τ for y in e, if (bound-id=? x y)
(define (subst τ x e)
(syntax-parse e
- [y:id #:when (bound-identifier=? e x) τ]
+ [y:id #:when (bound-identifier=? e x) (syntax-track-origin τ #'y #'y)]
[(esub ...)
#:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...))
(syntax-track-origin #'(esub_subst ...) e x)]
