commit a07fa92d25c1379592e17099c88930db884f7eb5
parent 94b610c93b4738300cd2b6c3d89cc0dec773aca3
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Mon, 12 Oct 2015 12:42:00 -0400
clean up fomega2/3, remove many type-eval
- remove expand-fn optional arg in infer fn
Diffstat:
4 files changed, 49 insertions(+), 101 deletions(-)
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -31,7 +31,7 @@
(define-syntax define-type-alias
(syntax-parser
[(_ alias:id τ)
- #:with (τ- k_τ) (infer+erase #'τ #:expand (current-type-eval))
+ #:with (τ- k_τ) (infer+erase #'τ)
#:fail-unless ((current-kind?) #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ))
#'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
@@ -81,14 +81,13 @@
(define-typed-syntax Λ
[(_ bvs:kind-ctx e)
#:with ((tv- ...) e- τ_e)
- (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+ (infer/ctx+erase #'bvs #'e)
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
(define-typed-syntax inst
[(_ e τ ...)
#:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
- #:with ([τ- k_τ] ...)
- (infers+erase #'(τ ...) #:expand (current-type-eval))
+ #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
#:when (stx-andmap
(λ (t k) (or ((current-kind?) k)
(type-error #:src t #:msg "not a valid type: ~a" t)))
@@ -100,15 +99,14 @@
;; - see fomega2.rkt
(define-typed-syntax tyλ
[(_ bvs:kind-ctx τ_body)
- #:with (tvs- τ_body- k_body)
- (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+ #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
#:when ((current-kind?) #'k_body)
(⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))])
(define-typed-syntax tyapp #:export-as tyapp
[(_ τ_fn τ_arg ...)
#:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
- #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:expand (current-type-eval))
+ #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
#:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
(string-append
(format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
@@ -1,5 +1,5 @@
#lang s-exp "typecheck.rkt"
-(extends "sysf.rkt" #:except #%datum ∀ Λ inst #:rename [~∀ ~sysf:∀])
+(extends "sysf.rkt" #:except #%datum ∀ Λ inst);#:rename [~∀ ~sysf:∀])
(reuse String #%datum #:from "stlc+reco+var.rkt")
; same as fomega.rkt except here λ and #%app works as both type and terms
@@ -34,64 +34,37 @@
(define-syntax define-type-alias
(syntax-parser
[(_ alias:id τ)
- #:with (τ- k_τ) (infer+erase #'τ #:expand (current-type-eval))
+ #:with (τ- k_τ) (infer+erase #'τ)
#'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
-(begin-for-syntax
- (define sysf:type-eval (current-type-eval))
- ;; extend type-eval to handle tyapp
- ;; - requires manually handling all other forms
- (define (type-eval τ)
- (beta (sysf:type-eval τ)))
- (define (beta τ)
- (syntax-parse τ
- [((~literal #%plain-app) τ_fn τ_arg ...)
- #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'τ_fn
- ((current-type-eval) (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
- [((~literal #%plain-lambda) (x ...) τ_body ...)
- #:with (τ_body+ ...) (stx-map beta #'(τ_body ...))
- (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
- [((~literal #%plain-app) arg ...)
- #:with (arg+ ...) (stx-map beta #'(arg ...))
- (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
- [_ τ]))
- (current-type-eval type-eval))
-
(define-base-kind ★)
(define-kind-constructor ∀★ #:arity >= 0)
+(define-type-constructor ∀ #:bvs >= 0 #:arr ∀★)
-(define-typed-syntax ∀ #:export-as ∀
- [(_ bvs:kind-ctx τ_body)
- ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
- #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
- ; expand so kind gets overwritten
- (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))])
+;; alternative: normalize before type=?
+; but then also need to normalize in current-promote
(begin-for-syntax
- (define-syntax ~∀
- (pattern-expander
- (syntax-parser #:datum-literals (:)
- [(_ ([tv:id : k] ...) τ)
- #:with ∀τ (generate-temporary)
- #'(~and ∀τ
- (~parse (~sysf:∀ (tv ...) τ) #'∀τ)
- (~parse (~∀★ k ...) (typeof #'∀τ)))]
- [(_ . args)
- #:with ∀τ (generate-temporary)
- #'(~and ∀τ
- (~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ)
- (~parse (~∀★ k (... ...)) (typeof #'∀τ))
- (~parse args #'(([tv k] (... ...)) τ)))])))
- (define-syntax ~∀*
- (pattern-expander
- (syntax-parser #:datum-literals (<:)
- [(_ . args)
- #'(~or
- (~∀ . args)
- (~and any (~do
- (type-error
- #:src #'any
- #:msg "Expected ∀ type, got: ~a" #'any))))])))
- (define sysf:type=? (current-type=?))
+ (define (normalize τ)
+ (syntax-parse τ
+ [x:id #'x]
+ [((~literal #%plain-app) ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...)
+ (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
+ [((~literal #%plain-lambda) (x ...) . bodys)
+ #:with bodys_norm (stx-map normalize #'bodys)
+ (syntax-track-origin #'(#%plain-lambda (x ...) . bodys_norm) τ #'plain-lambda)]
+ [((~literal #%plain-app) x:id . args)
+ #:with args_norm (stx-map normalize #'args)
+ (syntax-track-origin #'(#%plain-app x . args_norm) τ #'#%plain-app)]
+ [((~literal #%plain-app) . args)
+ #:with args_norm (stx-map normalize #'args)
+ (syntax-track-origin (normalize #'(#%plain-app . args_norm)) τ #'#%plain-app)]
+ [_ τ]))
+
+ (define old-eval (current-type-eval))
+ (define (type-eval τ) (normalize (old-eval τ)))
+ (current-type-eval type-eval)
+
+ (define old-type=? (current-type=?))
(define (type=? t1 t2)
(or (and (★? t1) (#%type? t2))
(and (#%type? t1) (★? t2))
@@ -100,20 +73,20 @@
(~∀ ([tv2 : k2]) tbody2))
((current-type=?) #'k1 #'k2)]
[_ #t])
- (sysf:type=? t1 t2))))
+ (old-type=? t1 t2))))
(current-type=? type=?)
(current-typecheck-relation (current-type=?)))
(define-typed-syntax Λ
[(_ bvs:kind-ctx e)
#:with ((tv- ...) e- τ_e)
- (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+ (infer/ctx+erase #'bvs #'e)
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
(define-typed-syntax inst
[(_ e τ ...)
- #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
- #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
+ #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
+ #:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
#:when (stx-andmap (λ (t k) (or ((current-kind?) k)
(type-error #:src t #:msg "not a valid type: ~a" t)))
#'(τ ...) #'(k_τ ...))
diff --git a/tapl/fomega3.rkt b/tapl/fomega3.rkt
@@ -30,24 +30,3 @@
(let ([k (typeof t)])
(or (★? k) (∀★? k)))
((current-kind?) t)))))
-
-;; extend to handle #%app and λ used as both terms and types
-(begin-for-syntax
- (define sysf:type-eval (current-type-eval))
- ;; extend type-eval to handle tyapp
- ;; - requires manually handling all other forms
- (define (type-eval τ)
- (beta (sysf:type-eval τ)))
- (define (beta τ)
- (syntax-parse τ
- [((~literal #%plain-app) τ_fn τ_arg ...)
- #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'τ_fn
- ((current-type-eval) (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
- [((~literal #%plain-lambda) (x ...) τ_body ...)
- #:with (τ_body+ ...) (stx-map beta #'(τ_body ...))
- (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
- [((~literal #%plain-app) arg ...)
- #:with (arg+ ...) (stx-map beta #'(arg ...))
- (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
- [_ τ]))
- (current-type-eval type-eval))
-\ No newline at end of file
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -197,12 +197,12 @@
;; basic infer function with no context:
;; infers the type and erases types in an expression
- (define (infer+erase e #:expand [expand-fn expand/df])
- (define e+ (expand-fn e))
+ (define (infer+erase e)
+ (define e+ (expand/df e))
(list e+ (typeof e+)))
;; infers the types and erases types in multiple expressions
- (define (infers+erase es #:expand [expand-fn expand/df])
- (stx-map (λ (e) (infer+erase e #:expand expand-fn)) es))
+ (define (infers+erase es)
+ (stx-map infer+erase es))
;; 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.
@@ -211,8 +211,7 @@
;; octx + tag = some other context (and an associated tag)
;; eg bounded quantification in Fsub
(define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
- #:octx [octx tvctx] #:tag [tag 'unused]
- #:expand [expand-fn expand/df])
+ #:octx [octx tvctx] #:tag [tag 'unused])
(syntax-parse ctx #:datum-literals (:)
[([x : τ] ...) ; dont expand yet bc τ may have references to tvs
#:with ([tv : k] ...) tvctx
@@ -233,7 +232,7 @@
((~literal #%plain-lambda) xs+
((~literal let-values) () ((~literal let-values) ()
((~literal #%expression) e+) ... (~literal void))))))))
- (expand-fn
+ (expand/df
#`(λ (tv ...)
(let-syntax ([tv (make-rename-transformer
(assign-type
@@ -260,11 +259,11 @@
;; shorter names
; ctx = type env for bound vars in term e, etc
; can also use for bound tyvars in type e
- (define (infer/ctx+erase ctx e #:expand [expand-fn expand/df])
- (syntax-parse (infer (list e) #:ctx ctx #:expand expand-fn)
+ (define (infer/ctx+erase ctx e)
+ (syntax-parse (infer (list e) #:ctx ctx)
[(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
- (define (infers/ctx+erase ctx es #:expand [expand-fn expand/df])
- (stx-cdr (infer es #:ctx ctx #:expand expand-fn)))
+ (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)
@@ -459,13 +458,13 @@
#:fail-unless (op (stx-length #'args) n)
(format "wrong number of arguments, expected ~a ~a" 'op 'n)
#:with (bvs- τs- _)
- (infers/ctx+erase #'bvs #'args ;#'([bv : #%kind] (... ...)) #'args
- #:expand (current-type-eval))
+ (infers/ctx+erase #'bvs #'args) ;#'([bv : #%kind] (... ...)) #'args
+; #:expand (current-type-eval))
#:with (~! (~var _ kind) (... ...)) #'τs-
#:with ([tv (~datum :) k_arg] (... ...)) #'bvs
- #:with (k_arg+ (... ...)) (stx-map (current-type-eval) #'(k_arg (... ...)))
+; #:with (k_arg+ (... ...)) (stx-map (current-type-eval) #'(k_arg (... ...)))
#:with k_result (if #,(attribute has-annotations?)
- #'(tycon k_arg+ (... ...))
+ #'(tycon k_arg (... ...))
#'#%kind)
(assign-type #'(τ-internal (λ bvs- void . τs-)) #'k_result)]
;; else fail with err msg
