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

Make simple substitution happen all at once.

Browse Source 
Closes pr12920.

original commit: 2e3965e7772594a19aac32d9673fb0c98e19bbdd
This commit is contained in:
Eric Dobson 2012-08-12 21:40:36 -07:00 committed by Sam Tobin-Hochstadt
parent 23a26e8533
commit f071ccf186
4 changed files with 76 additions and 59 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
collects/tests/typed-racket/succeed/type-alias-rec-struct.rkt Normal file
View File

@ -0,0 +1,6 @@
#lang typed/racket/base
;; Iteratee
(define-type (Alias A D) (U #f (Main A D)))
(struct: (A D) Main
([resume : (Alias A D)])) ;

29
collects/typed-racket/private/parse-type.rkt
View File

@ -366,33 +366,13 @@
(let loop
([rator (parse-type #'id)]
[args (map parse-type (syntax->list #'(arg args ...)))])
(resolve-app-check-error rator args stx)
(match rator
[(Name: n)
(when (and (current-poly-struct)
(free-identifier=? n (poly-name (current-poly-struct)))
(not (or (ormap Error? args)
(andmap type-equal? args (poly-vars (current-poly-struct))))))
(tc-error "Structure type constructor ~a applied to non-regular arguments ~a" rator args))
(make-App rator args stx)]
[(Poly: ns _)
(unless (= (length args) (length ns))
(tc-error "Wrong number of arguments to type ~a, expected ~a but got ~a" rator (length ns) (length args)))
(instantiate-poly rator args)]
[(Name: _) (make-App rator args stx)]
[(Poly: _ _) (instantiate-poly rator args)]
[(Mu: _ _) (loop (unfold rator) args)]
[(Error:) Err]
[_ (tc-error/delayed "Type ~a cannot be applied, arguments were: ~a" rator args)
Err]))
#;
(let ([ty (parse-type #'id)])
#;(printf "ty is ~a" ty)
(unless (Poly? ty)
(tc-error "not a polymorphic type: ~a" (syntax-e #'id)))
(unless (= (length (syntax->list #'(arg args ...))) (Poly-n ty))
(tc-error "wrong number of arguments to type constructor ~a: expected ~a, got ~a"
(syntax-e #'id)
(Poly-n ty)
(length (syntax->list #'(arg args ...)))))
(instantiate-poly ty (map parse-type (syntax->list #'(arg args ...)))))]
[_ Err]))]
[t:atom
(-val (syntax-e #'t))]
[_ (tc-error "not a valid type: ~a" (syntax->datum stx))])))
@ -463,4 +443,3 @@
(define parse-tc-results/id (parse/id parse-tc-results))
(define parse-type/id (parse/id parse-type))

28
collects/typed-racket/types/resolve.rkt
View File

@ -8,7 +8,8 @@
racket/match
racket/contract)
(provide resolve-name resolve-app needs-resolving? resolve)
(provide resolve-name resolve-app needs-resolving?
resolve resolve-app-check-error)
(provide/cond-contract [resolve-once (Type/c . -> . (or/c Type/c #f))])
(define-struct poly (name vars) #:prefab)
@ -21,24 +22,35 @@
(define already-resolving? (make-parameter #f))
(define (resolve-app rator rands stx)
(parameterize ([current-orig-stx stx]
[already-resolving? #t])
(define (resolve-app-check-error rator rands stx)
(parameterize ([current-orig-stx stx])
(match rator
[(Poly-unsafe: n _)
(unless (= n (length rands))
(tc-error "wrong number of arguments to polymorphic type: expected ~a and got ~a"
n (length rands)))
(instantiate-poly rator rands)]
n (length rands)))]
[(Name: n)
(when (and (current-poly-struct)
(free-identifier=? n (poly-name (current-poly-struct)))
(not (or (ormap Error? rands)
(andmap type-equal? rands (poly-vars (current-poly-struct))))))
(tc-error "Structure type constructor ~a applied to non-regular arguments ~a" rator rands))
(tc-error "Structure type constructor ~a applied to non-regular arguments ~a" rator rands))]
[(Mu: _ _) (void)]
[(App: _ _ _) (void)]
[(Error:) (void)]
[_ (tc-error/delayed "Type ~a cannot be applied, arguments were: ~a" rator rands)])))
(define (resolve-app rator rands stx)
(parameterize ([current-orig-stx stx]
[already-resolving? #t])
(resolve-app-check-error rator rands stx)
(match rator
[(Name: _)
(let ([r (resolve-name rator)])
(and r (resolve-app r rands stx)))]
(and r (resolve-app r rands stx)))]
[(Poly: _ _) (instantiate-poly rator rands)]
[(Mu: _ _) (resolve-app (unfold rator) rands stx)]
[(App: r r* s) (resolve-app (resolve-app r r* s) rands stx)]
[_ (tc-error "cannot apply a non-polymorphic type: ~a" rator)])))

72
collects/typed-racket/types/substitute.rkt
View File

@ -21,6 +21,7 @@
(define-struct/cond-contract (i-subst/dotted subst-rhs) ([types (listof Type/c)] [dty Type/c] [dbound symbol?]) #:transparent)
(define substitution/c (hash/c symbol? subst-rhs? #:immutable #t))
(define simple-substitution/c (hash/c symbol? Type/c #:immutable #t))
(define (subst v t e) (substitute t v e))
@ -32,38 +33,48 @@
(values v (t-subst t))))
;; substitute : Type Name Type -> Type
(define/cond-contract (substitute image name target #:Un [Un (lambda (args) (apply Un args))])
((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
(define (sb t) (substitute image name t #:Un Un))
(if (hash-ref (free-vars* target) name #f)
;; substitute-many : Hash[Name,Type] Type -> Type
(define/cond-contract (substitute-many subst target #:Un [Un (lambda (args) (apply Un args))])
((simple-substitution/c Type?) (#:Un procedure?) . ->* . Type?)
(define (sb t) (substitute-many subst t #:Un Un))
(define names (hash-keys subst))
(if (ormap (lambda (name) (hash-has-key? (free-vars* target) name)) names)
(type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
target
[#:Union tys (Un (map sb tys))]
[#:F name* (if (eq? name* name) image target)]
[#:F name (hash-ref subst name target)]
[#:arr dom rng rest drest kws
(begin
(when (and (pair? drest)
(eq? name (cdr drest))
(not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws)))]
(cond
((and (pair? drest) (ormap (and/c (cdr drest) (not/c bound-tvar?)) names)) =>
(lambda (name)
(int-err "substitute used on ... variable ~a in type ~a" name target)))
(else
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws))))]
[#:ValuesDots types dty dbound
(begin
(when (and (eq? name dbound) (not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(cond
((ormap (and/c dbound (not/c bound-tvar?)) names) =>
(lambda (name)
(int-err "substitute used on ... variable ~a in type ~a" name target)))
(make-ValuesDots (map sb types) (sb dty) dbound))]
[#:ListDots dty dbound
(begin
(when (and (eq? name dbound) (not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(cond
((ormap (and/c dbound (not/c bound-tvar?)) names) =>
(lambda (name)
(int-err "substitute used on ... variable ~a in type ~a" name target)))
(make-ListDots (sb dty) dbound))])
target))
;; substitute : Type Name Type -> Type
(define/cond-contract (substitute image name target #:Un [Un (lambda (args) (apply Un args))])
((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
(substitute-many (hash name image) target #:Un Un))
;; implements angle bracket substitution from the formalism
;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
(define/cond-contract (substitute-dots images rimage name target)
@ -142,12 +153,21 @@
;; substitute many variables
;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
;; subst-all : substitution Type -> Type
(define/cond-contract (subst-all s t)
(define/cond-contract (subst-all s ty)
(substitution/c Type? . -> . Type?)
(for/fold ([t t]) ([(v r) (in-hash s)])
(define t-substs
(for/fold ([acc (hash)]) ([(v r) (in-hash s)])
(match r
[(t-subst img)
(hash-set acc v img)]
[_ acc])))
(define t-substed-ty (substitute-many t-substs ty))
(for/fold ([t t-substed-ty]) ([(v r) (in-hash s)])
(match r
[(t-subst img)
(substitute img v t)]
[(t-subst img) t]
[(i-subst imgs)
(substitute-dots imgs #f v t)]
[(i-subst/starred imgs rest)