suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

consolidate typecheck.rkt: impl everything in terms of infer fn

Browse Source
This commit is contained in:
Stephen Chang 2015-07-09 15:30:12 -04:00
parent b0a8d192ef
commit f0d314b46d
3 changed files with 19 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
tapl/exist.rkt
View File

@ -40,7 +40,6 @@
#:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body))
(⊢ #'e- #'∃τ)]))
; TODO: the colon syntax might be misleading, since tv is not the type of x
(define-syntax (open stx)
(syntax-parse stx #:datum-literals (<=)
[(_ ([(tv:id x:id) <= e_packed]) e)

6
tapl/fomega2.rkt
View File

@ -163,8 +163,8 @@
#: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 ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:with ((~literal #%plain-app) _ τ:type ... τ_res) #'τ_fn
#:with ([e_arg- τ_arg:type] ...) (infers+erase #'(e_arg ...))
#:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
(string-append
(format
@ -177,7 +177,7 @@
(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
", ")
(format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
#:fail-unless (typechecks? #'(τ_arg.norm ...) #'(τ.norm ...))
(string-append
(format
"Arguments to function ~a have wrong type:\ngiven: "

21
tapl/typecheck.rkt
View File

@ -137,12 +137,18 @@
;; 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 (infers/type-ctxt+erase x+τs (list e))
(syntax-parse (infer (list e) #:ctx x+τs)
[(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)])
#;(syntax-parse (infers/type-ctxt+erase x+τs (list e))
[(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)
(syntax-parse ctxt
;(printf "~a\n" (infer es #:ctx ctxt))
(stx-cdr (infer es #:ctx ctxt)) ; drop (empty) tyvars from result
#;(syntax-parse (infer es #:ctx ctxt)
[(tvs xs es+ τs) (list #'xs #'es+ #'τs)])
#;(syntax-parse ctxt
[(b:typed-binding ...)
#:with (x ...) #'(b.x ...)
#:with (τ ...) #'(b.τ ...)
@ -168,10 +174,14 @@
(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 (expand/df #`(λ #,tvs (#%expression #,e))) #:literals (#%expression)
(syntax-parse (infer (list e) #:tvs tvs)
[(tvs xs (e+) (τ)) (list #'tvs #'e+ #'τ)])
#;(syntax-parse (expand/df #`(λ #,tvs (#%expression #,e))) #:literals (#%expression)
[(lam tvs+ (#%expression e+))
(list #'tvs+ #'e+ (syntax-local-introduce (typeof #'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.
(define (infer es #:ctx [ctx null] #:tvs [tvs null])
(syntax-parse ctx #:datum-literals (:)
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
@ -190,8 +200,9 @@
(λ (x ...)
(let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
(#%expression e) ...))))
(list #'tvs+ #'xs+ #'(e+ ...) (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
[([x τ] ...) (infer+erase es #:ctx #'([x : τ] ...) #:tvs tvs)]))
(list #'tvs+ #'xs+ #'(e+ ...)
(stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
[([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvs tvs)]))
(define current-typecheck-relation (make-parameter #f))
(define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))