commit daecc5c62402bbd290ba9d336fc0b38897b378ed
parent 0e1a8484653110af2ab14ac6982f1239b6cb9c90
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 24 Jul 2015 16:26:04 -0400
add tycon pattern matching to stlc
- fix stlc+lit tests
- current-promote is currently broken
- add err msg checking unit rackunit-typechecking
- works with new expander
Diffstat:
6 files changed, 243 insertions(+), 71 deletions(-)
diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
@@ -2,14 +2,14 @@
(require "typecheck.rkt")
(require (except-in "sysf.rkt" #%app #%datum + ∀ Λ inst type=?)
(prefix-in sysf: (only-in "sysf.rkt" #%app ∀ Λ inst type=?))
- (except-in "stlc+reco+sub.rkt" #%app + type=?)
- (prefix-in stlc: (only-in "stlc+reco+sub.rkt" type=?)))
-(provide (rename-out [sysf:#%app #%app]))
+ (except-in "stlc+reco+sub.rkt" #%app + type=? sub?)
+ (prefix-in stlc: (only-in "stlc+reco+sub.rkt" type=? sub?)))
+(provide (rename-out [sysf:#%app #%app]) (for-syntax sub?))
(provide (except-out (all-from-out "sysf.rkt")
sysf:#%app sysf:∀ sysf:Λ sysf:inst
(for-syntax sysf:type=?))
(except-out (all-from-out "stlc+reco+sub.rkt")
- (for-syntax stlc:type=?)))
+ (for-syntax stlc:type=? stlc:sub?)))
(provide ∀ Λ inst)
;; System F<:
@@ -27,6 +27,9 @@
(if sub (expose sub) t)]
[else t]))
(current-promote expose)
+ (define (sub? t1 t2)
+ (stlc:sub? (expose t1) (expose t2)))
+ (current-sub? sub?)
;; extend to handle new ∀
(define (type=? τ1 τ2)
(syntax-parse (list τ1 τ2)
diff --git a/tapl/notes.txt b/tapl/notes.txt
@@ -1,3 +1,13 @@
+2015-07-24
+When to canonicalize (ie, eval) types:
+- calling eval before matching is too late
+ - wont catch things like unbound types
+- syntax-class evaling is too eager
+ - sometimes get error when you shouldnt or wrong erro
+ - eg type (-> 1 2)
+- I think the right place is to have \vdash eval
+ - and rackunit testing forms
+
2015-06-30
when extending a typed language, use prefix-in for identifiers:
- that are extended, eg #%datum in ext-stlc.rkt
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -44,7 +44,33 @@
(or (null? τs-lst)
(andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst)))))
-(define-type-constructor →)
+;(define-type-constructor →)
+
+;;; when defining a type constructor tycon, can't define tycon as both
+;;; - an appliable constructor (ie a macro)
+;;; - and a syntax class
+;;; alternate solution: automatically define a tycon-match function
+;(define-syntax define-tycon
+; (syntax-parser
+; [(_ (τ arg ...))
+; #:with pat (generate-temporary) ; syntax-class name
+; #:with fn (generate-temporary) ; need a runtime id for expansion
+; #'(begin
+; (begin-for-syntax
+; (define-syntax-class pat
+; (pattern (arg ...))))
+; (define-syntax τ
+; (syntax-parser
+; [x:id #'pat]
+; [(_ x ( ... ...)) #'(fn x (... ...))])))]))
+;(define-tycon (→ τ ... τ_res))
+;
+;(define-for-syntax match-type-as
+; (syntax-parser
+; [( τ pat)
+; #:with
+
+(define-tycon (→ τ_in ... τ_out))
(define-syntax (λ/tc stx)
(syntax-parse stx
@@ -55,37 +81,42 @@
(define-syntax (app/tc stx)
(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) (→-args #'τ_fn)
+ #:with (e_fn- (τ_in ... τ_out)) (→-match+erase #'e_fn)
+ ;#:with (e_fn- τ_fn) (infer+erase #'e_fn)
+ ;#:with (e_fn- (τ_in ... τ_out)) (match+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 (τ_in ... τ_out) (→-match #'τ_fn)
#:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
- #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
- (string-append
- (format
- "Wrong number of args given to function ~a:\ngiven: "
- (syntax->datum #'e_fn))
- (string-join
- (map
- (λ (e t) (format "~a : ~a" e t))
- (syntax->datum #'(e_arg ...))
- (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
- ", ")
- (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
- #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
+; #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
+; (string-append
+; (format
+; "Wrong number of args given to function ~a:\ngiven: "
+; (syntax->datum #'e_fn))
+; (string-join
+; (map
+; (λ (e t) (format "~a : ~a" e t))
+; (syntax->datum #'(e_arg ...))
+; (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+; ", ")
+; (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
(string-append
- (format
- "Arguments to function ~a have wrong type:\ngiven: "
- (syntax->datum #'e_fn))
+ (format "Arguments to function ~a have wrong type(s), "
+ (syntax->datum #'e_fn))
+ "or wrong number of arguments:\n"
+ "given: "
(string-join
(map
(λ (e t) (format "~a : ~a" e t))
(syntax->datum #'(e_arg ...))
(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
", ")
- "\nexpected arguments with type: "
+ "\n"
+ (format "expected ~a arguments with type(s): "
+ (stx-length #'(τ_in ...)))
(string-join
- (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
+ (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ_in ...))))
", "))
- (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
+ (⊢ #'(#%app e_fn- e_arg- ...) #'τ_out)]))
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
@@ -7,7 +7,7 @@
[(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
[(_ e : τ-expected:type)
#:with τ (typeof (expand/df #'e))
- #:fail-unless (typecheck? #'τ #'τ-expected.norm)
+ #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected))
(format
"Expression ~a [loc ~a:~a] has type ~a, expected ~a"
(syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
@@ -18,7 +18,7 @@
(syntax-parse stx #:datum-literals (:)
[(_ e : not-τ:type)
#:with τ (typeof (expand/df #'e))
- #:fail-when (typecheck? #'τ #'not-τ.norm)
+ #:fail-when (typecheck? #'τ ((current-type-eval) #'not-τ.norm))
(format
"(~a:~a) Expression ~a should not have type ~a"
(syntax-line stx) (syntax-column stx)
@@ -27,12 +27,24 @@
(define-syntax (typecheck-fail stx)
(syntax-parse stx #:datum-literals (:)
- [(_ e)
+ [(_ e (~optional (~seq #:with-msg msg-pat:str) #:defaults ([msg-pat ""])))
#:when (check-exn
- exn:fail?
- (λ () (expand/df #'e))
+ (λ (ex) (or (exn:fail? ex) (exn:test:check? ex)))
+ (λ ()
+ (with-handlers
+ ; check err msg matches
+ ([exn:fail?
+ (λ (ex)
+ (unless (regexp-match? (syntax-e #'msg-pat) (exn-message ex))
+ (printf
+ (string-append
+ "ERROR: wrong err msg produced by expression ~v:\n"
+ "expected msg matching pattern ~v, got:\n ~v")
+ (syntax->datum #'e) (syntax-e #'msg-pat) (exn-message ex)))
+ (raise ex))])
+ (expand/df #'e)))
(format
- "Expected type check failure but expression ~a has valid type."
+ "Expected type check failure but expression ~a has valid type, OR wrong err msg received."
(syntax->datum #'e)))
#'(void)]))
diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
@@ -3,24 +3,56 @@
(check-type 1 : Int)
(check-not-type 1 : (→ Int Int))
-(typecheck-fail "one") ; unsupported literal
-(typecheck-fail #f) ; unsupported literal
+
+(typecheck-fail "one" #:with-msg "Unsupported literal")
+(typecheck-fail #f #:with-msg "Unsupported literal")
+
(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
(check-not-type (λ ([x : Int]) x) : Int)
(check-type (λ ([x : Int]) x) : (→ Int Int))
-(typecheck-fail (λ ([x : →]) x))
-(typecheck-fail (λ ([x : (→ →)]) x))
-(typecheck-fail (λ ([x : (→)]) x))
+
+(typecheck-fail
+ (λ ([x : →]) x)
+ #:with-msg "Improper usage of type constructor →: →, expected pattern")
+(typecheck-fail
+ (λ ([x : (→ →)]) x)
+ #:with-msg "Improper usage of type constructor →: →, expected pattern")
+(typecheck-fail
+ (λ ([x : (→)]) x)
+ #:with-msg "Improper usage of type constructor →: \\(→\\), expected pattern")
+
(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
-(typecheck-fail (λ ([x : (→ Bool Bool)]) x)) ; Bool is not valid type
-(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
-(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+
+(typecheck-fail ((λ ([x : Bool]) x) 1)
+ #:with-msg "Bool: unbound identifier")
+(typecheck-fail (λ ([x : (→ Bool Bool)]) x)
+ #:with-msg "Bool: unbound identifier")
+(typecheck-fail (λ ([x : Bool]) x)
+ #:with-msg "Bool: unbound identifier")
+(typecheck-fail (λ ([f : Int]) (f 1 2))
+ #:with-msg
+ "didn't match expected type pattern: \\(→ τ_in ... τ_out\\)")
+
(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
: (→ (→ Int Int Int) Int Int Int))
(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
-(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
-(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
-(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+
+(typecheck-fail
+ (+ 1 (λ ([x : Int]) x))
+ #:with-msg
+ "Arguments to function \\+ have wrong type.+given: 1 : Int.+→.+expected 2 arguments with type.+Int\\, Int")
+(typecheck-fail
+ (λ ([x : (→ Int Int)]) (+ x x))
+ #:with-msg
+ "Arguments to function \\+ have wrong type.+given: x.+→.+expected 2 arguments with type.+Int\\, Int")
+(typecheck-fail
+ ((λ ([x : Int] [y : Int]) y) 1)
+ #:with-msg "Arguments to function.+have.+wrong number of arguments")
+
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
+(typecheck-fail (λ ([x : (→ 1 2)]) x)
+ #:with-msg "Improperly formatted type annotation")
+(typecheck-fail (λ ([x : 1]) x)
+ #:with-msg "Improperly formatted type annotation")
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -1,6 +1,7 @@
#lang racket/base
(require
- (for-syntax racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
+ (for-syntax racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
+ (for-meta 2 racket/base syntax/parse))
(provide
(for-syntax (all-defined-out)) (all-defined-out)
(for-syntax
@@ -40,6 +41,70 @@
(define (get-orig τ)
(car (reverse (or (syntax-property τ 'orig) (list τ))))))
+(begin-for-syntax
+ (define-syntax (match-type stx)
+ (syntax-parse stx
+ [(_ ty tycon cls)
+ #'(syntax-parse ty ;((current-type-eval) ty)
+ [((~literal #%plain-app) t . args)
+ #:declare args cls
+ #:fail-unless (typecheck? #'t #'tycon)
+ (format "Type error: expected ~a type, got ~a"
+ (syntax->datum #'τ) (syntax->datum ty))
+ #'args]
+ [_ #f
+ #;(type-error #:src ty
+ #:msg "~a didn't match expected type pattern: ~a"
+ ty pat)])])))
+
+(define-syntax define-tycon
+ (syntax-parser
+ [(_ (τ:id . pat))
+ #:with τ-match (format-id #'τ "~a-match" #'τ)
+ #:with τ? (format-id #'τ "~a?" #'τ)
+ #:with τ-match+erase (format-id #'τ "~a-match+erase" #'τ)
+ #:with pat-class (generate-temporary #'τ) ; syntax-class name
+ #:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
+ #'(begin
+ (provide τ)
+ (begin-for-syntax
+ (define-syntax-class pat-class
+ (pattern pat))
+ (define (τ-match ty)
+ (or (match-type ty tycon pat-class)
+ (type-error #:src ty
+ #:msg "~a didn't match expected type pattern: ~a"
+ ty (quote-syntax (τ . pat))))
+ #;(syntax-parse ty
+ [((~literal #%plain-app) t . args)
+ #:declare args pat-class
+ #:fail-unless (typecheck? #'t #'tycon)
+ (format "Type error: expected ~a type, got ~a"
+ (syntax->datum #'τ) (syntax->datum ty))
+ #'args]
+ [_ (type-error #:src ty
+ #:msg "~a didn't match expected type pattern: ~a"
+ ty (quote-syntax (τ . pat)))]))
+ ; predicate version of τ-match
+ (define (τ? ty) (match-type ty tycon pat-class))
+ ;; expression version of τ-match
+ (define (τ-match+erase e)
+ (syntax-parse (infer+erase e)
+ [(e- τ)
+ #:with τ_matched (τ-match #'τ)
+ #'(e- τ_matched)])))
+ (define tycon (λ _ (raise (exn:fail:type:runtime
+ (format "~a: Cannot use type at run time" 'τ)
+ (current-continuation-marks)))))
+ (define-syntax (τ stx)
+ (syntax-parse stx
+ [(_ . pat) #'(tycon . pat)]
+ [_
+ (type-error #:src stx
+ #:msg "Improper usage of type constructor ~a: ~a, expected pattern ~a"
+ #'τ stx (quote-syntax (τ . pat)))]))
+ )]))
+
;; TODO: refine this to enable specifying arity information
;; type constructors currently must have 1+ arguments
(define-syntax (define-type-constructor stx)
@@ -49,6 +114,7 @@
#:with τ-ref (format-id #'τ "~a-ref" #'τ)
#:with τ-num-args (format-id #'τ "~a-num-args" #'τ)
#:with τ-args (format-id #'τ "~a-args" #'τ)
+ #:with τ-match (format-id #'τ "~a-match" #'τ)
#:with tmp (generate-temporary #'τ)
#`(begin
;; TODO: define syntax class instead of these separate tycon fns
@@ -102,17 +168,32 @@
(define-syntax-class type
;; stx = surface syntax, as written
;; norm = canonical form for the type
- (pattern stx:expr
- #:with norm ((current-type-eval) #'stx)
- #:with τ #'norm)) ; backwards compat
+ (pattern tycon:id
+ #:when (procedure? (syntax-local-value #'tycon (λ _ #f)))
+ #:with norm #f ; should this be #f?
+ #:with τ #f)
+ (pattern T:id
+ #:with norm #'T ;((current-type-eval) #'T)
+ #:with τ #'norm) ; backwards compat
+ (pattern (t:type ...)
+ #:with norm #'(t ...) ;((current-type-eval) #'(t ...))
+ #:with τ #'norm) ; backwards compat
+ (pattern any
+ #:with norm #f #:with τ #f
+ #:fail-when #t
+ (format "~a is not a valid type" (syntax->datum #'any))))
+
(define-syntax-class typed-binding #:datum-literals (:)
(pattern [x:id : stx:type] #:with τ #'stx.τ)
(pattern (~and any (~not [x:id : τ:type]))
#:with x #f
#:with τ #f
#:fail-when #t
- (format "Improperly formatted type annotation: ~a; should have shape [x : τ]"
- (syntax->datum #'any))))
+ (format
+ (string-append
+ "Improperly formatted type annotation: ~a; should have shape [x : τ], "
+ "where τ is a valid type.")
+ (syntax->datum #'any))))
(define (brace? stx)
(define paren-shape/#f (syntax-property stx 'paren-shape))
(and paren-shape/#f (char=? paren-shape/#f #\{)))
@@ -129,20 +210,12 @@
;; must eval here, to catch unbound types
(define (⊢ e τ #:tag [tag 'type])
(syntax-property e tag (syntax-local-introduce ((current-type-eval) τ))))
+ ;(syntax-property e tag τ))
;; 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))
- ;; infers type and erases types in a single expression,
- ;; in the context of the given bindings and their types
- (define (infer/type-ctxt+erase x+τs e)
- (syntax-parse (infer (list e) #:ctx x+τs)
- [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
- ;; infers type and erases types in multiple expressions,
- ;; in the context of (one set of) given bindings and their tpyes
- (define (infers/type-ctxt+erase ctxt es)
- (stx-cdr (infer es #:ctx ctxt))) ; drop (empty) tyvars from result
;; infers the type and erases types in an expression
(define (infer+erase e)
(define e+ (expand/df e))
@@ -150,10 +223,6 @@
;; infers the types and erases types in multiple expressions
(define (infers+erase es)
(stx-map infer+erase es))
- ;; infers and erases types in an expression, in the context of given type vars
- (define (infer/tvs+erase e tvs)
- (syntax-parse (infer (list e) #:tvs tvs)
- [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
;; This is the main "infer" function. All others are defined in terms of this.
;; It should be named infer+erase but leaving it for now for backward compat.
@@ -167,14 +236,14 @@
#:with (e ...) es
#:with
; old expander pattern
- ((~literal #%plain-lambda) tvs+
+ #;((~literal #%plain-lambda) tvs+
((~literal #%expression)
((~literal #%plain-lambda) xs+
((~literal letrec-syntaxes+values) stxs1 ()
((~literal letrec-syntaxes+values) stxs2 ()
((~literal #%expression) e+) ...)))))
; new expander pattern
- #;((~literal #%plain-lambda) tvs+
+ ((~literal #%plain-lambda) tvs+
((~literal #%expression)
((~literal #%plain-lambda) xs+
((~literal let-values) ()
@@ -189,11 +258,26 @@
(stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
[([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvs tvs)]))
+ ;; fns derived from infer ---------------------------------------------------
+ ;; some are syntactic shortcuts, some are for backwards compat
+
+ ;; infers type and erases types in a single expression,
+ ;; in the context of the given bindings and their types
+ (define (infer/type-ctxt+erase x+τs e)
+ (syntax-parse (infer (list e) #:ctx x+τs)
+ [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
+ ;; infers type and erases types in multiple expressions,
+ ;; in the context of (one set of) given bindings and their tpyes
+ (define (infers/type-ctxt+erase ctxt es)
+ (stx-cdr (infer es #:ctx ctxt))) ; drop (empty) tyvars from result
+ ;; infers and erases types in an expression, in the context of given type vars
+ (define (infer/tvs+erase e tvs)
+ (syntax-parse (infer (list e) #:tvs tvs)
+ [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
+
(define current-typecheck-relation (make-parameter #f))
(define (typecheck? t1 t2)
- ((current-typecheck-relation)
- ((current-promote) t1)
- ((current-promote) t2)))
+ ((current-typecheck-relation) t1 t2))
(define (typechecks? τs1 τs2)
(and (= (stx-length τs1) (stx-length τs2))
(stx-andmap typecheck? τs1 τs2)))
