From d0459d58b0f9d7fd724a4098c45548b7061e701c Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 28 May 2015 19:18:26 -0400 Subject: [PATCH] =?UTF-8?q?move=20type=3D=3F=20out=20of=20typecheck.rkt=20?= =?UTF-8?q?and=20into=20each=20language=20def?= --- tapl/ext-stlc.rkt | 7 ++- tapl/stlc+box.rkt | 2 +- tapl/stlc+cons.rkt | 2 +- tapl/stlc+rec+sub.rkt | 7 +-- tapl/stlc+tup.rkt | 10 ++-- tapl/stlc+var.rkt | 39 +++++++++++++-- tapl/stlc.rkt | 28 ++++++++++- tapl/sysf.rkt | 44 ++++++++++++++--- tapl/tests/lam-testing-tests.rkt | 2 +- tapl/tests/rackunit-typechecking.rkt | 4 +- tapl/tests/run-all-tests.rkt | 13 +++++ tapl/typecheck.rkt | 71 ++++++++++++++++------------ 12 files changed, 169 insertions(+), 60 deletions(-) create mode 100644 tapl/tests/run-all-tests.rkt diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt index 0bd72aa..576c4e7 100644 --- 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 index cbf2a5a..70dc5a5 100644 --- 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 index c04dc55..b5d9547 100644 --- 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 index 5dd4389..b17c732 100644 --- 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 index bb8fd9c..3a30095 100644 --- 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 index 9effa14..0fd6a05 100644 --- 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 index ba840e8..4e0c906 100644 --- 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 index e9c7998..fe0dc8a 100644 --- 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 index b5667bd..4775603 100644 --- 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 index f458523..a6accf1 100644 --- 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 new file mode 100644 index 0000000..e9e4ee6 --- /dev/null +++ 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 index e84efe1..4e72a85 100644 --- 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