commit d0459d58b0f9d7fd724a4098c45548b7061e701c
parent f56fae94ab205493dd491f412ac170cdb8350642
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 28 May 2015 19:18:26 -0400
move type=? out of typecheck.rkt and into each language def
Diffstat:
12 files changed, 171 insertions(+), 61 deletions(-)
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -2,16 +2,15 @@
(require
(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
"typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ #%datum))
- (except-in "stlc+lit.rkt" #%app λ #%datum))
+(require (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum))
+ (except-in "stlc+lit.rkt" #%app #%datum))
(provide (rename-out [datum/tc #%datum]
[stlc:#%app #%app]
- [stlc:λ λ]
[and/tc and] [or/tc or] [if/tc if]
[begin/tc begin]
[let/tc let] [let*/tc let*] [letrec/tc letrec])
ann)
-(provide (all-from-out "stlc+lit.rkt"))
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:#%datum))
;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11)
;; Types:
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
@@ -34,5 +34,5 @@
[(_ e_ref e)
#:with (e_ref- ((~literal Ref) τ1)) (infer+erase #'e_ref)
#:with (e- τ2) (infer+erase #'e)
- #:when (τ= #'τ1 #'τ2)
+ #:when (type=? #'τ1 #'τ2)
(⊢ #'(set-box! e_ref- e-) #'Unit)]))
\ No newline at end of file
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
@@ -45,7 +45,7 @@
[(_ e1 e2)
#:with (e1- τ1) (infer+erase #'e1)
#:with (e2- ((~literal List) τ2)) (infer+erase #'e2)
- #:when (τ= #'τ1 #'τ2)
+ #:when (type=? #'τ1 #'τ2)
(⊢ #'(cons e1- e2-) #'(List τ1))]))
(define-syntax (isnil stx)
(syntax-parse stx
diff --git a/tapl/stlc+rec+sub.rkt b/tapl/stlc+rec+sub.rkt
@@ -2,14 +2,15 @@
(require
(for-syntax racket/base syntax/parse racket/string syntax/stx racket/set "stx-utils.rkt")
"typecheck.rkt")
-(require (except-in "stlc+sub.rkt" #%app #%datum sub?)
+(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=? types=? same-types?)
(prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?))
(except-in "stlc+var.rkt" #%app #%datum +)
(prefix-in var: (only-in "stlc+var.rkt" #%datum)))
(provide (rename-out [stlc:#%app #%app]
[datum/tc #%datum]))
-(provide (except-out (all-from-out "stlc+sub.rkt") stlc:#%app)
- (all-from-out "stlc+var.rkt"))
+(provide (except-out (all-from-out "stlc+sub.rkt") stlc:#%app stlc:#%datum
+ (for-syntax stlc:sub?))
+ (except-out (all-from-out "stlc+var.rkt") var:#%datum))
(provide (for-syntax sub?))
;; Simply-Typed Lambda Calculus, plus subtyping, plus records
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
@@ -2,17 +2,19 @@
(require
(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
"typecheck.rkt")
-(require (prefix-in stlc: (only-in "ext-stlc.rkt" #%app λ))
- (except-in "ext-stlc.rkt" #%app λ))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])
+(require (prefix-in stlc: (only-in "ext-stlc.rkt" #%app))
+ (except-in "ext-stlc.rkt" #%app))
+(provide (rename-out [stlc:#%app #%app])
tup proj)
-(provide (all-from-out "ext-stlc.rkt"))
+(provide (except-out (all-from-out "ext-stlc.rkt") stlc:#%app))
;; Simply-Typed Lambda Calculus, plus tuples
;; Types:
;; - types from ext-stlc.rkt
+;; - ×
;; Terms:
;; - terms from ext-stlc.rkt
+;; - tup and proj
(define-type-constructor ×)
diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt
@@ -5,14 +5,18 @@
(for-meta 2 racket/base syntax/parse racket/syntax)
"typecheck.rkt")
(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let))
- (except-in "stlc+tup.rkt" #%app λ tup proj let))
+ (except-in "stlc+tup.rkt" #%app λ tup proj let type=? types=? same-types?))
(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
-(provide (except-out (all-from-out "stlc+tup.rkt") stlc:#%app stlc:#%datum))
+(provide (except-out (all-from-out "stlc+tup.rkt")
+ stlc:#%app stlc:λ stlc:let stlc:tup stlc:proj))
;(provide define-type-alias define-variant module quote submod)
(provide tup proj var case)
+(provide (for-syntax type=? types=? same-types?))
;; Simply-Typed Lambda Calculus, plus variants
+;; Type relations:
+;; - type=? extended to strings
;; define-type-alias (also provided to programmer)
;; Types:
;; - types from stlc+tup.rkt
@@ -23,6 +27,30 @@
;; - extend tup to include records
;; - sums (var)
+(begin-for-syntax
+ ;; type=? : Type Type -> Boolean
+ ;; Indicates whether two types are equal
+ ;; TODO: fix this code duplication, should call stlc:type=?
+ (define (type=? τ1 τ2)
+ (syntax-parse (list τ1 τ2)
+ [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
+ [(x:id y:id) (free-identifier=? τ1 τ2)]
+ [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
+ [_ #f]))
+
+ ;; redefine these to use the new type=?
+
+ ;; type equality = structurally recursive identifier equality
+ ;; uses the type=? in the context of τs1 instead of here
+ (define (types=? τs1 τs2)
+ (and (= (stx-length τs1) (stx-length τs2))
+ (stx-andmap type=? τs1 τs2)))
+ ;; uses the type=? in the context of τs instead of here
+ (define (same-types? τs)
+ (define τs-lst (syntax->list τs))
+ (or (null? τs-lst)
+ (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst)))))
+
(provide define-type-alias)
(define-syntax (define-type-alias stx)
(syntax-parse stx
@@ -61,12 +89,13 @@
(define-syntax (var stx)
(syntax-parse stx #:datum-literals (as =)
[(_ l:str = e as τ)
- #:when (∨? #'τ)
- #:with (∨ (l_τ τ_l) ...) (eval-τ #'τ)
+ #:with τ+ (eval-τ #'τ)
+ #:when (∨? #'τ+)
+ #:with (∨ (l_τ τ_l) ...) #'τ+
#:with (l_match τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...))
#:with (e- τ_e) (infer+erase #'e)
#:when (type=? #'τ_match #'τ_e)
- (⊢ #'(list l e) #'τ)]))
+ (⊢ #'(list l e) #'τ+)]))
(define-syntax (case stx)
(syntax-parse stx #:datum-literals (of =>)
[(_ e [l:str x => e_l] ...)
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -3,7 +3,8 @@
(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
"typecheck.rkt")
(provide (rename-out [λ/tc λ] [app/tc #%app]))
-(provide #%module-begin #%top-interaction #%top require)
+(provide (for-syntax type=? types=? same-types?))
+(provide #%module-begin #%top-interaction #%top require) ; from racket
;; Simply-Typed Lambda Calculus
;; - no base type so cannot write any terms
@@ -15,6 +16,29 @@
(define-type-constructor →)
+(begin-for-syntax
+ ;; type=? : Type Type -> Boolean
+ ;; Indicates whether two types are equal
+ ;; structurally checks for free-identifier=?
+ (define (type=? τ1 τ2)
+ ;(printf "~a\n" (syntax->datum τ1))
+ ;(printf "~a\n" (syntax-property τ1 'surface-type))
+ (syntax-parse (list τ1 τ2)
+ [(x:id y:id) (free-identifier=? τ1 τ2)]
+ [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
+ [_ #f]))
+
+ ;; type equality = structurally recursive identifier equality
+ ;; uses the type=? in the context of τs1 instead of here
+ (define (types=? τs1 τs2)
+ (and (= (stx-length τs1) (stx-length τs2))
+ (stx-andmap type=? τs1 τs2)))
+ ;; uses the type=? in the context of τs instead of here
+ (define (same-types? τs)
+ (define τs-lst (syntax->list τs))
+ (or (null? τs-lst)
+ (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst)))))
+
(define-syntax (λ/tc stx)
(syntax-parse stx
[(_ (b:typed-binding ...) e)
@@ -30,7 +54,7 @@
(syntax->datum #'e_fn) (syntax->datum #'τ_fn))
#:with (→ τ ... τ_res) #'τ_fn
#:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
- #:fail-unless (types=? #'(τ ...) #'(τ_arg ...))
+ #:fail-unless ((eval-syntax (datum->syntax #'e_fn 'types=?)) #'(τ ...) #'(τ_arg ...))
(string-append
(format
"Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
@@ -1,16 +1,18 @@
#lang racket/base
(require
- (for-syntax racket/base syntax/parse)
-; (for-meta 2 racket/base)
+ (for-syntax racket/base syntax/parse "stx-utils.rkt")
"typecheck.rkt")
-(require (except-in "stlc+lit.rkt" λ #%app)
- (prefix-in stlc: (only-in "stlc+lit.rkt" λ #%app)))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:λ stlc:#%app))
+(require (except-in "stlc+lit.rkt" #%app type=? types=? same-types?)
+ (prefix-in stlc: (only-in "stlc+lit.rkt" #%app)))
+(provide (rename-out [stlc:#%app #%app]))
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app))
(provide Λ inst)
+(provide (for-syntax type=? types=? same-types?))
;; System F
+;; Type relation:
+;; - extend type=? with ∀
;; Types:
;; - types from stlc+lit.rkt
;; - ∀
@@ -20,6 +22,36 @@
(define-type-constructor ∀)
+(begin-for-syntax
+ ;; type=? : Type Type -> Boolean
+ ;; Indicates whether two types are equal
+ (define (type=? τ1 τ2)
+ ;(printf "t1 = ~a\n" (syntax->datum τ1))
+ ;(printf "t2 = ~a\n" (syntax->datum τ2))
+ (syntax-parse (list τ1 τ2) #:literals (∀)
+ [((∀ (x ...) t1) (∀ (y ...) t2))
+ #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
+ #:with (z ...) (generate-temporaries #'(x ...))
+ (type=? (substs #'(z ...) #'(x ...) #'t1)
+ (substs #'(z ...) #'(y ...) #'t2))]
+ [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
+ [(x:id y:id) (free-identifier=? τ1 τ2)]
+ [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
+ [_ #f]))
+
+ ;; redefine these to use the new type=?
+
+ ;; type equality = structurally recursive identifier equality
+ ;; uses the type=? in the context of τs1 instead of here
+ (define (types=? τs1 τs2)
+ (and (= (stx-length τs1) (stx-length τs2))
+ (stx-andmap type=? τs1 τs2)))
+ ;; uses the type=? in the context of τs instead of here
+ (define (same-types? τs)
+ (define τs-lst (syntax->list τs))
+ (or (null? τs-lst)
+ (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst)))))
+
(define-syntax (Λ stx)
(syntax-parse stx
[(_ (tv:id ...) e)
diff --git a/tapl/tests/lam-testing-tests.rkt b/tapl/tests/lam-testing-tests.rkt
@@ -1,3 +1,3 @@
-#lang s-exp "lam-testing.rkt"
+#lang s-exp "../lam-testing.rkt"
((λ (x y) x) 1 2)
\ No newline at end of file
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
@@ -12,7 +12,7 @@
#:with τ-expected+ (eval-τ #'τ-expected)
#:fail-unless
;; use subtyping if it's bound in the context of #'e
- (with-handlers ([exn:fail? (λ _ (type=? #'τ #'τ-expected+))])
+ (with-handlers ([exn:fail? (λ _ ((eval-syntax (datum->syntax #'e 'type=?)) #'τ #'τ-expected+))])
((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'τ-expected+))
(format
"Expression ~a [loc ~a:~a] has type ~a, expected ~a"
@@ -26,7 +26,7 @@
#:with τ (typeof (expand/df #'e))
#:with not-τ+ (eval-τ #'not-τ)
#:fail-when
- (with-handlers ([exn:fail? (λ _ (type=? #'τ #'not-τ+))])
+ (with-handlers ([exn:fail? (λ _ ((eval-syntax (datum->syntax #'e 'type=?)) #'τ #'not-τ+))])
((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'not-τ+))
(format
"(~a:~a) Expression ~a should not have type ~a"
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
@@ -0,0 +1,13 @@
+#lang racket
+(require "stlc-tests.rkt")
+(require "stlc+lit-tests.rkt")
+(require "ext-stlc-tests.rkt")
+(require "stlc+tup-tests.rkt")
+(require "stlc+var-tests.rkt")
+(require "stlc+cons-tests.rkt")
+(require "stlc+box-tests.rkt")
+
+(require "stlc+sub-tests.rkt")
+(require "stlc+rec+sub-tests.rkt")
+
+(require "sysf-tests.rkt")
+\ No newline at end of file
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -29,7 +29,7 @@
#'(begin
(provide τ (for-syntax τ?))
(define τ (void))
- (define-for-syntax (τ? τ1) (type=? (eval-τ τ1) #'τ)))]))
+ (define-for-syntax (τ? τ1) (free-identifier=? #'τ τ1)))]))
(define-syntax (define-type-constructor stx)
(syntax-parse stx
@@ -39,7 +39,7 @@
(provide τ (for-syntax τ?))
(define τ (void))
(define-for-syntax (τ? stx)
- (syntax-parse (eval-τ stx) #:literals (τ)
+ (syntax-parse stx #:literals (τ)
[(τ τ_arg (... ...)) #t]
[_ #f])))]))
@@ -108,32 +108,40 @@
(syntax-parse (expand/df #`(λ #,tvs (#%expression #,e))) #:literals (#%expression)
[(lam tvs+ (#%expression e+)) (list #'tvs+ #'e+ (typeof #'e+))]))
- ;; type equality = structurally recursive identifier equality
- (define (types=? τs1 τs2)
- (and (= (stx-length τs1) (stx-length τs2))
- (stx-andmap type=? τs1 τs2)))
- (define (same-types? τs)
- (define τs-lst (syntax->list τs))
- (or (null? τs-lst)
- (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst))))
-
- ;; type=? : Type Type -> Boolean
- ;; Indicates whether two types are equal
- (define (type=? τ1 τ2)
- (syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀)
- ;; TODO: should not have any datum literals
- [(x:id y:id) (free-identifier=? τ1 τ2)]
- [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
- [((∀ (x ...) t1) (∀ (y ...) t2))
- #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
- #:with (z ...) (generate-temporaries #'(x ...))
- (type=? (substs #'(z ...) #'(x ...) #'t1)
- (substs #'(z ...) #'(y ...) #'t2))]
- [((τ1 ...) (τ2 ...)) (types=? #'(τ1 ...) #'(τ2 ...))]
- [_ #f]))
-
- (define τ= type=?)
-
+; ;; type equality = structurally recursive identifier equality
+; (define (types=? τs1 τs2)
+; (and (= (stx-length τs1) (stx-length τs2))
+; (stx-andmap type=? τs1 τs2)))
+; (define (same-types? τs)
+; (define τs-lst (syntax->list τs))
+; (or (null? τs-lst)
+; (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst))))
+;
+; ;; type=? : Type Type -> Boolean
+; ;; Indicates whether two types are equal
+; (define (type=? τ1 τ2)
+; (syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀)
+; ;; TODO: should not have any datum literals
+; [(x:id y:id) (free-identifier=? τ1 τ2)]
+; [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
+; [((∀ (x ...) t1) (∀ (y ...) t2))
+; #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
+; #:with (z ...) (generate-temporaries #'(x ...))
+; (type=? (substs #'(z ...) #'(x ...) #'t1)
+; (substs #'(z ...) #'(y ...) #'t2))]
+; [((τ1 ...) (τ2 ...)) (types=? #'(τ1 ...) #'(τ2 ...))]
+; [_ #f]))
+
+ (define (add-origin τ τ-orig)
+ (define surface-τs/#f (syntax-property τ-orig 'surface-type))
+ (if surface-τs/#f
+ (syntax-property τ 'surface-type (cons τ-orig surface-τs/#f))
+ (syntax-property τ 'surface-type (list τ-orig))))
+ (define (get-origin τ)
+ (define surface-τs/#f (syntax-property τ 'surface-type))
+ (if surface-τs/#f
+ (car (reverse surface-τs/#f))
+ τ))
;; type expansion
(define (eval-τ τ [tvs #'()])
(syntax-parse τ
@@ -147,11 +155,12 @@
;; manually remove app and recursively expand
(if (identifier? maybe-app-τ) ; base type
;; full expansion checks that type is a bound name
- (local-expand maybe-app-τ 'expression null)
+ ;; 'surface-type property is like 'origin (which seems to get lost)
+ (add-origin (local-expand maybe-app-τ 'expression null) τ)
(syntax-parse maybe-app-τ
- [(τ ...)
- #:with (τ-exp ...) (stx-map (λ (t) (eval-τ t tvs)) #'(τ ...))
- #'(τ-exp ...)]))]))
+ [(τ1 ...)
+ #:with (τ-exp ...) (stx-map (λ (t) (eval-τ t tvs)) #'(τ1 ...))
+ (add-origin #'(τ-exp ...) τ)]))]))
;; term expansion
;; expand/df : Syntax -> Syntax
