From 3d422803f6a1b0404168c0454d8fdb76aaa8fb97 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 12 Jun 2015 19:30:00 -0400 Subject: [PATCH] make define-type-const a macro to enable error checking --- tapl/stlc+var.rkt | 22 +++++++---------- tapl/stlc.rkt | 35 +++++++++++++++++----------- tapl/sysf.rkt | 22 +++++------------ tapl/tests/rackunit-typechecking.rkt | 2 +- tapl/tests/stlc+lit-tests.rkt | 4 +++- tapl/tests/stlc+var-tests.rkt | 1 + tapl/typecheck.rkt | 13 ++++++++++- 7 files changed, 53 insertions(+), 46 deletions(-) diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt index 02c2b3c..3f1269b 100644 --- a/tapl/stlc+var.rkt +++ b/tapl/stlc+var.rkt @@ -27,17 +27,17 @@ (begin-for-syntax ;; type expansion ;; extend to handle strings - (define (eval-τ τ) + (define (eval-τ τ . rst) (syntax-parse τ [s:str τ] ; record field - [_ (stlc:eval-τ τ)])) + [_ (apply stlc:eval-τ τ rst)])) (current-τ-eval eval-τ) ; extend to: ; 1) first eval types, to accomodate aliases ; 2) accept strings (ie, record labels) (define (type=? τ1 τ2) - (syntax-parse (list (eval-τ τ1) (eval-τ τ2)) + (syntax-parse (list τ1 τ2) [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))] [_ (stlc:type=? τ1 τ2)])) @@ -45,17 +45,11 @@ (current-typecheck-relation (current-type=?))) (provide define-type-alias) -(define-syntax (define-type-alias stx) - (syntax-parse stx - [(_ τ:id τ-expanded) - (if (identifier? #'τ-expanded) - #'(define-syntax τ (make-rename-transformer #'τ-expanded)) - #'(define-syntax τ - (λ (stx) - (syntax-parse stx - ; τ-expanded must have the context of its use, not definition - ; so the appropriate #%app is used - [x:id (datum->syntax #'x 'τ-expanded)]))))])) +(define-syntax define-type-alias + (syntax-parser + [(_ alias:id τ) + ; must eval, otherwise undefined types will be allowed + #'(define-syntax alias (syntax-parser [x:id ((current-τ-eval) #'τ)]))])) ;; records (define-syntax (tup stx) diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index 8d1da6b..26717f2 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -14,18 +14,27 @@ (begin-for-syntax ;; type expansion - ;; must structurally recur to check nested identifiers - (define (eval-τ τ) - ; we want #%app in τ's ctxt, not here (which is racket's #%app) + ;; - must structurally recur to check nested identifiers + ;; - rst allows adding extra args later + (define (eval-τ τ . rst) + ; app is #%app in τ's ctxt, not here (which is racket's #%app) (define app (datum->syntax τ '#%app)) - ;; stop right before expanding #%app, - ;; since type constructors dont have types (ie kinds) (yet) - ;; so the type checking in #%app will fail - (syntax-parse (local-expand τ 'expression (list app)) - [x:id (local-expand #'x 'expression null)] ; full expansion - [(t ...) - ;; recursively expand - (stx-map (current-τ-eval) #'(t ...))])) + ;; stop right before expanding: + ;; - #%app, this should mean tycon via define-type-constructor + ;; - app, other compound types, like variants + ;; - ow, the type checking in #%app will fail + ;; (could leave this case out until adding variants but it's general + ;; enough, so leave it here) + ;; could match specific type constructors like → before expanding + ;; but this is more general and wont require subsequent extensions for + ;; every defined type constructor + (syntax-parse (local-expand τ 'expression (list app #'#%app)) + ; full expansion checks for undefined types + [x:id (local-expand #'x 'expression null)] + [((~literal #%app) tcon t ...) + #`(tcon #,@(stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...)))] + ; else just structurually eval + [(t ...) (stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...))])) (current-τ-eval eval-τ)) (begin-for-syntax @@ -61,13 +70,13 @@ (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))])) (define-syntax (app/tc stx) - (syntax-parse stx #:literals (→) + (syntax-parse stx [(_ 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 (_ τ ... τ_res) #'τ_fn #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...)) #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...)) (string-append diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt index cf8c8b4..94a4cd5 100644 --- a/tapl/sysf.rkt +++ b/tapl/sysf.rkt @@ -1,10 +1,10 @@ #lang racket/base (require "typecheck.rkt") -(require (except-in "stlc+lit.rkt" #%app type=? λ eval-τ) - (prefix-in stlc: (only-in "stlc+lit.rkt" #%app type=? λ))) +(require (except-in "stlc+lit.rkt" #%app λ type=? eval-τ) + (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ type=? eval-τ))) (provide (rename-out [stlc:#%app #%app] [stlc:λ λ])) (provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app - (for-syntax stlc:type=?))) + (for-syntax stlc:type=? stlc:eval-τ))) (provide Λ inst) (provide (for-syntax type=? eval-τ)) @@ -23,23 +23,13 @@ (begin-for-syntax ;; Extend to handle ∀, skip typevars - (define (eval-τ τ [tvs #'()]) + (define (eval-τ τ [tvs #'()] . rst) (syntax-parse τ [x:id #:when (stx-member τ tvs) τ] [((~literal ∀) ts t-body) - #`(∀ ts #,((current-τ-eval) #'t-body (stx-append tvs #'ts)))] + #`(∀ ts #,(apply (current-τ-eval) #'t-body (stx-append tvs #'ts) rst))] ;; need to duplicate stlc:eval-τ here to pass extra params - [_ - ; we want #%app in τ's ctxt, not here (which is racket's #%app) - (define app (datum->syntax τ '#%app)) - ;; stop right before expanding #%app, - ;; since type constructors dont have types (ie kinds) (yet) - ;; so the type checking in #%app will fail - (syntax-parse (local-expand τ 'expression (list app)) - [x:id (local-expand #'x 'expression null)] ; full expansion - [(t ...) - ;; recursively expand - (stx-map (λ (x) ((current-τ-eval) x tvs)) #'(t ...))])])) + [_ (apply stlc:eval-τ τ tvs rst)])) (current-τ-eval eval-τ) ;; extend to handle ∀ diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt index 88ee5a1..2cdd635 100644 --- a/tapl/tests/rackunit-typechecking.rkt +++ b/tapl/tests/rackunit-typechecking.rkt @@ -34,7 +34,7 @@ exn:fail? (λ () (expand/df #'e)) (format - "Expression ~a has valid type, expected type check failure." + "Expected type check failure but expression ~a has valid type." (syntax->datum #'e))) #'(void)])) diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt index 521ee75..b91f79d 100644 --- a/tapl/tests/stlc+lit-tests.rkt +++ b/tapl/tests/stlc+lit-tests.rkt @@ -8,7 +8,9 @@ (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) (check-not-type (λ ([x : Int]) x) : Int) (check-type (λ ([x : Int]) x) : (→ Int Int)) -(check-type (λ ([x : (→ →)]) x) : (→ (→ →) (→ →))) ; TODO: should this fail? +(typecheck-fail (λ ([x : →]) x)) +(typecheck-fail (λ ([x : (→ →)]) x)) +(typecheck-fail (λ ([x : (→)]) x)) (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type diff --git a/tapl/tests/stlc+var-tests.rkt b/tapl/tests/stlc+var-tests.rkt index be5c30e..8131a10 100644 --- a/tapl/tests/stlc+var-tests.rkt +++ b/tapl/tests/stlc+var-tests.rkt @@ -4,6 +4,7 @@ ;; define-type-alias (define-type-alias Integer Int) (define-type-alias ArithBinOp (→ Int Int Int)) +;(define-type-alias C Complex) ; error, Complex undefined (check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer) (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 8f49943..52380dd 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -31,13 +31,24 @@ (define τ (void)) (define-for-syntax (τ? τ1) (typecheck? τ1 #'τ)))])) +;; TODO: refine this to enable specifying arity information +;; type constructors currently must have 1+ arguments (define-syntax (define-type-constructor stx) (syntax-parse stx [(_ τ:id) #:with τ? (format-id #'τ "~a?" #'τ) + #:with tmp (generate-temporary) #'(begin (provide τ (for-syntax τ?)) - (define τ (void)) + (define-syntax (τ stx) + (syntax-parse stx + [x:id + (type-error #:src #'x + #:msg "Cannot use type constructor in non-application position")] + [(_) (type-error #:src stx + #:msg "Type constructor must have at least one argument.")] + ; this is racket's #%app + [(_ x (... ...)) #'(#%app τ x (... ...))])) (define-for-syntax (τ? stx) (syntax-parse ((current-τ-eval) stx) [(τcons τ_arg (... ...)) (typecheck? #'τcons #'τ)]