commit 176b48208dfcb2f33515a4058111041073be7522
parent f0d314b46d90eeebd47441367e1e732d2c87312c
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 9 Jul 2015 15:34:36 -0400
cleanup
Diffstat:
3 files changed, 7 insertions(+), 70 deletions(-)
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -28,7 +28,6 @@
;; extend type-eval to handle tyapp
;; - requires manually handling all other forms
(define (type-eval τ)
-; (printf "eval: ~a\n" (syntax->datum τ))
(syntax-parse τ
[((~literal #%plain-app) τ_fn τ_arg ...)
#:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn)
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
@@ -34,7 +34,6 @@
;; extend type-eval to handle tyapp
;; - requires manually handling all other forms
(define (type-eval τ)
-; (printf "eval: ~a\n" (syntax->datum τ))
(syntax-parse τ
[((~literal #%plain-app) τ_fn τ_arg ...)
#:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn)
@@ -103,44 +102,6 @@
#:when (typechecks? #'(k ...) #'(k_tv ...))
(⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
-;; TODO: merge with regular λ and app?
-#;(define-syntax (tyλ stx)
- (syntax-parse stx
- [(_ (b:typed-binding ...) τ)
- #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
- ;; b.τ's here are actually kinds
- (⊢ #'(λ tvs- τ-) #'(⇒ b.τ ... k))]))
-
-#;(define-syntax (tyapp stx)
- (syntax-parse stx
- [(_ τ_fn τ_arg ...)
- #:with [τ_fn- k_fn] (infer+erase #'τ_fn)
- #:fail-unless (⇒? #'k_fn)
- (format "Kind error: Attempting to apply a non-tyλ with kind ~a\n"
- (syntax->datum #'τ_fn) (syntax->datum #'k_fn))
- #:with ((~literal #%plain-app) _ k ... k_res) #'k_fn
- #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
- #:fail-unless (typechecks? #'(k_arg ...) #'(k ...))
- (string-append
- (format
- "Wrong number of args given to tyλ ~a, or args have wrong kind:\ngiven: "
- (syntax->datum #'τ_fn))
- (string-join
- (map
- (λ (τ+k) (format "~a : ~a" (car τ+k) (cadr τ+k)))
- (syntax->datum #'([τ_arg k_arg] ...)))
- ", ")
- "\nexpected arguments with type: "
- (string-join
- (map (λ (x) (format "~a" x)) (syntax->datum #'(k ...)))
- ", "))
- ;; cant do type-subst here bc τ_fn might be a (forall) tyvar
- ;#:with τ_res ((current-type-eval) #'(tyapply τ_fn- τ_arg- ...))
- (⊢ #'(#%app τ_fn- τ_arg- ...) #'k_res)]))
-
-;; must override #%app and λ and primops to use new →
-;; TODO: parameterize →?
-
(define-primop + : (→ Int Int Int))
(define-syntax (λ/tc stx)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -138,33 +138,11 @@
;; 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+ #'τ)])
- #;(syntax-parse (infers/type-ctxt+erase x+τs (list e))
- [(xs (e+) (τ)) (list #'xs #'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)
- ;(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.τ ...)
- #:with (e ...) es
- #:with
- ((~literal #%plain-lambda) xs+
- ((~literal letrec-syntaxes+values) stxs1 ()
- ((~literal letrec-syntaxes+values) stxs2 ()
- ((~literal #%expression) e+) ...)))
- (expand/df
- #'(λ (x ...)
- (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
- (#%expression e) ...)))
- (list #'xs+ #'(e+ ...) (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
- [([x τ] ...) (infers/type-ctxt+erase #'([x : τ] ...) 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))
@@ -175,18 +153,17 @@
;; 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 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+)))]))
+ [(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.
+ ;; NOTE: differs slightly from infer/type-ctxt+erase in that types are not
+ ;; expanded before wrapping in lambda
+ ;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
+ ;; the types before typechecking, which is acceptable
(define (infer es #:ctx [ctx null] #:tvs [tvs null])
(syntax-parse ctx #:datum-literals (:)
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
-; #:with (x ...) #'(b.x ...)
-; #:with (τ ...) #'(b.τ ...)
#:with (e ...) es
#:with
((~literal #%plain-lambda) tvs+
