commit 995926e7357ce6a4b21333fbb6d1943f0a53e105
parent 4068d655d2df9e9e919854d94a4905285dc1011b
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 18 Nov 2016 16:55:16 -0500
do some optimizations in typecheck.rkt: as much as 85% speedup in benchmarks
- move 'env prop logic to infer.rkt
- eliminate some dup expands (eg type-evals)
some before/afters --------------------
macrotypes/run-all-tests: 2m11s/20s 85%
macrotypes/mlish-general: 117s/34s 71%
macrotypes/mlish-shootout/rwo: 81s/31s 62%
macrotypes/mlish-typeclasses: 179s/149s 17%
turnstile/run-all-tests: 2m31s/29s 81%
turnstile/mlish-general: 139s/46s 67%
turnstile/mlish-typeclasses: 181s/155s 14%
Diffstat:
6 files changed, 91 insertions(+), 48 deletions(-)
diff --git a/macrotypes/examples/ext-stlc.rkt b/macrotypes/examples/ext-stlc.rkt
@@ -119,14 +119,14 @@
[(_ e_unit ... e)
#:with ([e_unit- _] ...) (infers+erase #'(e_unit ...))
#:with (e- τ) (infer+erase #'e)
- (⊢ (begin- e_unit- ... e-) : τ)])
+ (⊢/no-teval (begin- e_unit- ... e-) : τ)])
(define-typed-syntax ann #:datum-literals (:)
[(_ e : ascribed-τ:type)
#:with (e- τ) (infer+erase #'(add-expected e ascribed-τ.norm))
#:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
(typecheck-fail-msg/1 #'ascribed-τ.norm #'τ #'e)
- (⊢ e- : ascribed-τ)])
+ (⊢/no-teval e- : ascribed-τ.norm)])
(define-typed-syntax let
[(_ ([x e] ...) e_body)
@@ -137,7 +137,7 @@
#:fail-unless (or (not (syntax-e #'τ-expected)) ; no expected type
(typecheck? #'τ_body ((current-type-eval) #'τ-expected)))
(typecheck-fail-msg/1 #'τ-expected #'τ_body #'e_body)
- (⊢ (let- ([x- e-] ...) e_body-) : τ_body)])
+ (⊢/no-teval (let- ([x- e-] ...) e_body-) : τ_body)])
; dont need to manually transfer expected type
; result template automatically propagates properties
@@ -157,4 +157,4 @@
(infers/ctx+erase #'(b ...) #'((add-expected e b.type) ... e_body))
#:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
(typecheck-fail-msg/multi #'(b.type ...) #'(τ ...) #'(e ...))
- (⊢ (letrec- ([x- e-] ...) e_body-) : τ_body)])
+ (⊢/no-teval (letrec- ([x- e-] ...) e_body-) : τ_body)])
diff --git a/macrotypes/examples/infer.rkt b/macrotypes/examples/infer.rkt
@@ -31,6 +31,74 @@
[(_ . rst) (add-orig #'(∀ () (ext-stlc:→ . rst)) (get-orig this-syntax))]))
(begin-for-syntax
+;; redefine all inferX functions to use 'env prop --------------------
+ (define (infer es #:ctx [ctx null] #:tvctx [tvctx null])
+ (syntax-parse ctx #:datum-literals (:)
+ [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
+ #:with ([tv (~seq sep:id tvk) ...] ...) tvctx
+ #:with (e ...) es
+ #:with
+ ((~literal #%plain-lambda) tvs+
+ ((~literal let-values) () ((~literal let-values) ()
+ ((~literal #%expression)
+ ((~literal #%plain-lambda) xs+
+ ((~literal let-values) () ((~literal let-values) ()
+ ((~literal #%expression) e+) ... (~literal void))))))))
+ (expand/df
+ #`(λ- (tv ...)
+ (let-syntax ([tv (make-rename-transformer
+ (set-stx-prop/preserved
+ (for/fold ([tv-id #'tv])
+ ([s (in-list (list 'sep ...))]
+ [k (in-list (list #'tvk ...))])
+ (assign-type tv-id k #:tag s))
+ 'tyvar #t))] ...)
+ (λ- (x ...)
+ (let-syntax
+ ([x
+ (syntax-parser
+ [i:id
+ (if (and (identifier? #'τ) (free-identifier=? #'x #'τ))
+ (if (get-expected-type #'i)
+ (add-env
+ (assign-type #'x (get-expected-type #'i))
+ #`((x #,(get-expected-type #'i))))
+ (raise
+ (exn:fail:type:infer
+ (format "~a (~a:~a): could not infer type of ~a; add annotation(s)"
+ (syntax-source #'x) (syntax-line #'x) (syntax-column #'x)
+ (syntax->datum #'x))
+ (current-continuation-marks))))
+ (assign-type #'x #'τ))]
+ [(o . rst) ; handle if x used in fn position
+ #:fail-when (and (identifier? #'τ) (free-identifier=? #'x #'τ))
+ (raise (exn:fail:type:infer
+ (format "~a (~a:~a): could not infer type of function ~a; add annotation(s)"
+ (syntax-source #'o) (syntax-line #'o) (syntax-column #'o)
+ (syntax->datum #'o))
+ (current-continuation-marks)))
+ #:with app (datum->syntax #'o '#%app)
+ (datum->syntax this-syntax
+ (list* #'app (assign-type #'x #'τ) #'rst)
+ this-syntax)])] ...)
+ (#%expression e) ... void)))))
+ (list #'tvs+ #'xs+ #'(e+ ...)
+ (stx-map typeof #'(e+ ...)))]
+ [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
+
+ (define (infer/ctx+erase ctx e)
+ (syntax-parse (infer (list e) #:ctx ctx)
+ [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
+ (define (infers/ctx+erase ctx es)
+ (stx-cdr (infer es #:ctx ctx)))
+ ; tyctx = kind env for bound type vars in term e
+ (define (infer/tyctx+erase ctx e)
+ (syntax-parse (infer (list e) #:tvctx ctx)
+ [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
+ (define (infers/tyctx+erase ctx es)
+ (syntax-parse (infer es #:tvctx ctx)
+ [(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)]))
+
;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id)
;; finds the free Xs in the type
(define (find-free-Xs Xs ty)
diff --git a/macrotypes/examples/stlc+box.rkt b/macrotypes/examples/stlc+box.rkt
@@ -20,7 +20,7 @@
(define-typed-syntax deref
[(_ e)
#:with [e- (~Ref τ)] (infer+erase #'e)
- (⊢ (unbox- e-) : τ)])
+ (⊢/no-teval (unbox- e-) : τ)])
(define-typed-syntax := #:literals (:=)
[(_ e_ref e)
#:with [e_ref- (~Ref τ1)] (infer+erase #'e_ref)
diff --git a/macrotypes/examples/stlc+cons.rkt b/macrotypes/examples/stlc+cons.rkt
@@ -50,7 +50,7 @@
;; propagate up inferred types of variables
#:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e1- e2-))))
#:with result-cons (add-env #'(cons- e1- e2-) #'env)
- (⊢ result-cons : τ_list)])
+ (⊢/no-teval result-cons : τ_list)])
(define-typed-syntax isnil
[(_ e)
#:with [e- (~List _)] (infer+erase #'e)
@@ -58,12 +58,12 @@
(define-typed-syntax head
[(_ e)
#:with [e- (~List τ)] (infer+erase #'e)
- (⊢ (car- e-) : τ)])
+ (⊢/no-teval (car- e-) : τ)])
(define-typed-syntax tail
[(_ e)
#:with [e- τ_lst] (infer+erase #'e)
#:when (List? #'τ_lst)
- (⊢ (cdr- e-) : τ_lst)])
+ (⊢/no-teval (cdr- e-) : τ_lst)])
(define-typed-syntax list
[(_) #'nil]
[(_ x . rst) ; has expected type
@@ -77,7 +77,7 @@
[(_ e)
#:with (e- τ-lst) (infer+erase #'e)
#:when (List? #'τ-lst)
- (⊢ (reverse- e-) : τ-lst)])
+ (⊢/no-teval (reverse- e-) : τ-lst)])
(define-typed-syntax length
[(_ e)
#:with (e- τ-lst) (infer+erase #'e)
@@ -87,7 +87,7 @@
[(_ e n)
#:with (e- (ty)) (⇑ e as List)
#:with n- (⇑ n as Int)
- (⊢ (list-ref- e- n-) : ty)])
+ (⊢/no-teval (list-ref- e- n-) : ty)])
(define-typed-syntax member
[(_ v e)
#:with (e- (ty)) (⇑ e as List)
diff --git a/macrotypes/examples/stlc.rkt b/macrotypes/examples/stlc.rkt
@@ -32,4 +32,4 @@
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
(typecheck-fail-msg/multi
#'(τ_in ...) #'(τ_arg ...) #'(e_arg ...))
- (⊢ (#%app- e_fn- e_arg- ...) : τ_out)])
+ (⊢/no-teval (#%app- e_fn- e_arg- ...) : τ_out)])
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -191,6 +191,10 @@
(syntax-parse stx #:datum-literals (:)
[(_ e : τ) #'(assign-type #`e #`τ)]
[(_ e τ) #'(⊢ e : τ)]))
+ (define-syntax (⊢/no-teval stx)
+ (syntax-parse stx #:datum-literals (:)
+ [(_ e : τ) #'(fast-assign-type #`e #`τ)]
+ [(_ e τ) #'(⊢/no-teval e : τ)]))
;; Actual type assignment function.
;; assign-type Type -> Syntax
@@ -198,8 +202,10 @@
;; - eval here so all types are stored in canonical form
;; - syntax-local-introduce fixes marks on types
;; which didnt get marked bc they were syntax properties
+ (define (fast-assign-type e τ #:tag [tag ':])
+ (set-stx-prop/preserved e tag (syntax-local-introduce τ)))
(define (assign-type e τ #:tag [tag ':])
- (set-stx-prop/preserved e tag (syntax-local-introduce ((current-type-eval) τ))))
+ (fast-assign-type e ((current-type-eval) τ) #:tag tag))
(define (add-expected-type e τ)
(if (and (syntax? τ) (syntax-e τ))
@@ -314,10 +320,8 @@
;; 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.
- ;; ctx = vars and their types
+ ;; ctx = vars and their types (or other props, denoted with "sep")
;; tvctx = tyvars and their kinds
- ;; octx + tag = some other context (and an associated tag)
- ;; eg bounded quantification in Fsub
(define (infer es #:ctx [ctx null] #:tvctx [tvctx null])
(syntax-parse ctx #:datum-literals (:)
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
@@ -348,39 +352,10 @@
(assign-type tv-id k #:tag s))
'tyvar #t))] ...)
(λ (x ...)
- (let-syntax
- ([x
- (syntax-parser
- [i:id
- (if (and (identifier? #'τ) (free-identifier=? #'x #'τ))
- (if (get-expected-type #'i)
- (add-env
- (assign-type #'x (get-expected-type #'i))
- #`((x #,(get-expected-type #'i))))
- (raise
- (exn:fail:type:infer
- (format "~a (~a:~a): could not infer type of ~a; add annotation(s)"
- (syntax-source #'x) (syntax-line #'x) (syntax-column #'x)
- (syntax->datum #'x))
- (current-continuation-marks))))
- (assign-type #'x #'τ))]
- [(o . rst) ; handle if x used in fn position
- #:fail-when (and (identifier? #'τ) (free-identifier=? #'x #'τ))
- (raise (exn:fail:type:infer
- (format "~a (~a:~a): could not infer type of function ~a; add annotation(s)"
- (syntax-source #'o) (syntax-line #'o) (syntax-column #'o)
- (syntax->datum #'o))
- (current-continuation-marks)))
- #:with app (datum->syntax #'o '#%app)
- (datum->syntax this-syntax
- (list* #'app (assign-type #'x #'τ) #'rst)
- this-syntax)])] ...)
- (#%expression e) ... void)))))
- (list #'tvs+ #'xs+ #'(e+ ...)
- (stx-map ; need this check when combining #%type and kinds
- (λ (t) (or (false? t)
- (syntax-local-introduce t)))
- (stx-map typeof #'(e+ ...))))]
+ (let-syntax
+ ([x (make-variable-like-transformer (assign-type #'x #'τ))] ...)
+ (#%expression e) ... void)))))
+ (list #'tvs+ #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))]
[([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
;; fns derived from infer ---------------------------------------------------
