From e4a234afbc6d3a6c1fd08a877ffdc424a46f694e Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 10 Jun 2015 15:56:27 -0400 Subject: [PATCH] code cleanup --- tapl/ext-stlc.rkt | 4 +--- tapl/stlc+box.rkt | 6 +----- tapl/stlc+cons.rkt | 6 +----- tapl/stlc+lit.rkt | 4 +--- tapl/stlc+rec+sub.rkt | 6 ++---- tapl/stlc+sub.rkt | 40 ++-------------------------------------- tapl/stlc+tup.rkt | 4 +--- tapl/stlc+var.rkt | 27 +++------------------------ tapl/stlc.rkt | 7 +------ tapl/sysf.rkt | 36 ++++++++---------------------------- tapl/typecheck.rkt | 36 +++++------------------------------- 11 files changed, 26 insertions(+), 150 deletions(-) diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt index db7728b..7f9e90b 100644 --- a/tapl/ext-stlc.rkt +++ b/tapl/ext-stlc.rkt @@ -1,7 +1,5 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt") - "typecheck.rkt") +(require "typecheck.rkt") (require (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum)) (except-in "stlc+lit.rkt" #%app #%datum)) (provide (rename-out [datum/tc #%datum] diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt index 338ec34..4ca769d 100644 --- a/tapl/stlc+box.rkt +++ b/tapl/stlc+box.rkt @@ -1,9 +1,5 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse syntax/stx racket/syntax racket/string - "stx-utils.rkt" "typecheck.rkt") - #;(for-meta 2 racket/base syntax/parse racket/syntax) - "typecheck.rkt") +(require "typecheck.rkt") (require (prefix-in stlc: (only-in "stlc+cons.rkt" #%app λ)) (except-in "stlc+cons.rkt" #%app λ)) (provide (rename-out [stlc:#%app #%app] [stlc:λ λ])) diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt index fb05c39..4656a90 100644 --- a/tapl/stlc+cons.rkt +++ b/tapl/stlc+cons.rkt @@ -1,9 +1,5 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse syntax/stx racket/syntax racket/string - "stx-utils.rkt" "typecheck.rkt") - #;(for-meta 2 racket/base syntax/parse racket/syntax) - "typecheck.rkt") +(require "typecheck.rkt") (require (prefix-in stlc: (only-in "stlc+var.rkt" #%app λ let begin)) (except-in "stlc+var.rkt" #%app λ let begin)) (provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let] [stlc:begin begin] diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt index b444f7d..9e82685 100644 --- a/tapl/stlc+lit.rkt +++ b/tapl/stlc+lit.rkt @@ -1,7 +1,5 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse) - "typecheck.rkt") +(require "typecheck.rkt") (require "stlc.rkt") (provide (all-from-out "stlc.rkt")) (provide (rename-out [datum/tc #%datum])) diff --git a/tapl/stlc+rec+sub.rkt b/tapl/stlc+rec+sub.rkt index ef4010e..6012a12 100644 --- a/tapl/stlc+rec+sub.rkt +++ b/tapl/stlc+rec+sub.rkt @@ -1,8 +1,6 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse racket/string syntax/stx racket/set "stx-utils.rkt") - "typecheck.rkt") -;; want to use type=? from stlc+var.rkt +(require "typecheck.rkt") +;; want to use type=? from stlc+var.rkt, not stlc+sub.rkt (require (except-in "stlc+sub.rkt" #%app #%datum sub? type=?) (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?)) (except-in "stlc+var.rkt" #%app #%datum +) diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt index 8471dc3..7233def 100644 --- a/tapl/stlc+sub.rkt +++ b/tapl/stlc+sub.rkt @@ -1,7 +1,5 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse racket/string "stx-utils.rkt") - "typecheck.rkt") +(require "typecheck.rkt") (require (except-in "stlc+lit.rkt" #%datum + #%app) (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum))) (provide (rename-out #;[app/tc #%app] [stlc:#%app #%app] [datum/tc #%datum])) @@ -41,10 +39,8 @@ (begin-for-syntax (define (sub? τ1 τ2) (or ((current-type=?) τ1 τ2) - #;(and (identifier? τ2) (free-identifier=? τ2 #'Top)) (syntax-parse (list τ1 τ2) #:literals (→ Nat Int Num Top) [(_ Top) #t] - #;[(t1:id t2:id) (free-identifier=? #'t1 #'t2)] [(Nat τ) ((current-sub?) #'Int #'τ)] [(Int τ) ((current-sub?) #'Num #'τ)] [(τ Num) ((current-sub?) #'τ #'Int)] @@ -54,37 +50,5 @@ ((current-sub?) #'s2 #'t2))] [_ #f]))) (define current-sub? (make-parameter sub?)) - (current-typecheck-relation (current-sub?)) + (current-typecheck-relation sub?) (define (subs? τs1 τs2) (stx-andmap (current-sub?) τs1 τs2))) - -#;(define-syntax (app/tc stx) - (syntax-parse stx - [(_ x ...) - #:with res - (parameterize ([current-type=? (current-sub?)]) - (local-expand #'(stlc:#%app x ...) 'expression null)) - #'res])) - -#;(define-syntax (app/tc stx) - (syntax-parse stx #:literals (→) - [(_ e_fn e_arg ...) - #:with (e_fn- τ_fn) (infer+erase #'e_fn) - #:fail-unless (→? #'τ_fn) - (format "Type error: Attempting to apply a non-function ~a with type ~a\n" - (syntax->datum #'e_fn) (syntax->datum #'τ_fn)) - #:with (→ τ ... τ_res) #'τ_fn - #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...)) -; #:fail-unless (types=? #'(τ ...) #'(τ_arg ...)) - #:fail-unless (subs? #'(τ_arg ...) #'(τ ...)) - (string-append - (format - "Wrong number of args given to function ~a, or args have wrong type:\ngiven: " - (syntax->datum #'e_fn)) - (string-join - (map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...))) - ", ") - "\nexpected arguments with type: " - (string-join - (map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...))) - ", ")) - (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)])) diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt index 5157e23..d042c34 100644 --- a/tapl/stlc+tup.rkt +++ b/tapl/stlc+tup.rkt @@ -1,7 +1,5 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt") - "typecheck.rkt") +(require "typecheck.rkt") (require (prefix-in stlc: (only-in "ext-stlc.rkt" #%app)) (except-in "ext-stlc.rkt" #%app)) (provide (rename-out [stlc:#%app #%app]) diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt index e3a8d8d..a29aff9 100644 --- a/tapl/stlc+var.rkt +++ b/tapl/stlc+var.rkt @@ -1,9 +1,5 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse syntax/stx racket/syntax racket/string - "stx-utils.rkt" "typecheck.rkt") - #;(for-meta 2 racket/base syntax/parse racket/syntax) - "typecheck.rkt") +(require "typecheck.rkt") (require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let type=?)) (except-in "stlc+tup.rkt" #%app λ tup proj let type=?)) (provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let])) @@ -31,29 +27,13 @@ (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))] - [_ (stlc:type=? τ1 τ2)] - #;[(x:id y:id) (free-identifier=? τ1 τ2)] - #;[((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))] - #;[_ #f])) + [_ (stlc:type=? τ1 τ2)])) (current-type=? type=?) - (current-typecheck-relation (current-type=?)) - ;; 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))))) + (current-typecheck-relation (current-type=?))) (provide define-type-alias) (define-syntax (define-type-alias stx) @@ -108,7 +88,6 @@ #:with (∨ (l_x τ_x) ...) #'τ_e #:fail-when (null? (syntax->list #'(l ...))) "no clauses" #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses" -; #:fail-unless (stx-andmap stx-str=? #'(l ...) #'(l_x ...)) "case clauses not exhaustive" #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive" #:with (((x-) e_l- τ_el) ...) (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...)) diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index ec522d1..9b1bb9e 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -1,7 +1,5 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt") - "typecheck.rkt") +(require "typecheck.rkt") (provide (rename-out [λ/tc λ] [app/tc #%app])) (provide (for-syntax type=? types=? same-types? current-type=?)) (provide #%module-begin #%top-interaction #%top require) ; from racket @@ -21,8 +19,6 @@ ;; 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 ...))] @@ -57,7 +53,6 @@ (syntax->datum #'e_fn) (syntax->datum #'τ_fn)) #:with (→ τ ... τ_res) #'τ_fn #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...)) -; #:fail-unless ((eval-syntax (datum->syntax #'e_fn 'types=?)) #'(τ ...) #'(τ_arg ...)) #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...)) (string-append (format diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt index a90261f..3c08dad 100644 --- a/tapl/sysf.rkt +++ b/tapl/sysf.rkt @@ -1,10 +1,8 @@ #lang racket/base -(require - #;(for-syntax racket/base syntax/parse "stx-utils.rkt") - "typecheck.rkt") -(require (except-in "stlc+lit.rkt" #%app type=?) - (prefix-in stlc: (only-in "stlc+lit.rkt" #%app type=?))) -(provide (rename-out [stlc:#%app #%app])) +(require "typecheck.rkt") +(require (except-in "stlc+lit.rkt" #%app type=? λ) + (prefix-in stlc: (only-in "stlc+lit.rkt" #%app type=? λ))) +(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])) (provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app (for-syntax stlc:type=?))) (provide Λ inst) (provide (for-syntax type=?)) @@ -25,35 +23,17 @@ (begin-for-syntax ;; type=? : Type Type -> Boolean ;; Indicates whether two types are equal + ;; Extend to handle ∀ (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))] + ((current-type=?) (substs #'(z ...) #'(x ...) #'t1) + (substs #'(z ...) #'(y ...) #'t2))] [_ (stlc:type=? τ1 τ2)])) (current-type=? type=?) - (current-typecheck-relation (current-type=?)) -; [(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))))) + (current-typecheck-relation type=?)) (define-syntax (Λ stx) (syntax-parse stx diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 92e0ef2..04e4c5b 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -1,7 +1,6 @@ #lang racket/base (require - (for-syntax racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt") - #;(for-meta 2 racket/base syntax/parse racket/list syntax/stx "stx-utils.rkt")) + (for-syntax racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt")) (provide (for-syntax (all-defined-out)) (all-defined-out) @@ -50,7 +49,7 @@ (pattern τ:expr)) (define-syntax-class typed-binding #:datum-literals (:) (pattern [x:id : τ:type]) - (pattern (~not [x:id : τ:type]) + (pattern (~and any (~not [x:id : τ:type])) #:with x #f #:with τ #f #:fail-when #t @@ -88,8 +87,9 @@ #:with (e ...) es #:with ((~literal #%plain-lambda) xs+ - (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 - ((~literal #%expression) e+) ...))) + ((~literal letrec-syntaxes+values) stxs1 () + ((~literal letrec-syntaxes+values) stxs2 () + ((~literal #%expression) e+) ...))) (expand/df #'(λ (x ...) (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) @@ -113,32 +113,6 @@ (define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2)) (define (typechecks? τs1 τs2) (stx-andmap (current-typecheck-relation) τs1 τs2)) - ; (define current-type=? (make-parameter #f)) - ; (define current-sub? (make-parameter #f)) - -; ;; 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])) ;; type expansion (define (eval-τ τ [tvs #'()])