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

Doc changes.

Browse Source 
svn: r11732

original commit: 37796884d8599d6411bff0ebbf6fc88e6f6bf285
This commit is contained in:
Sam Tobin-Hochstadt 2008-09-13 22:45:22 +00:00
commit dd509b80f3
63 changed files with 4960 additions and 135 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/tests/typed-scheme/fail/values-dots.ss
View File

@ -7,8 +7,8 @@
(: map-with-funcs (All (b ...) ((b ... b -> b) ... b -> (b ... b -> (values b ... b)))))
(define (map-with-funcs . fs)
(lambda bs
(apply values* (map (lambda: ([f : (b ... b -> b)])
(apply f bs)) fs))))
(apply values (map (lambda: ([f : (b ... b -> b)])
(apply f bs)) fs))))
(map-with-funcs (lambda () 1))

2
collects/tests/typed-scheme/succeed/nested-poly.ss
View File

@ -13,7 +13,7 @@
(B ... B -> (values A ... A))))))
(define (map-with-funcs . fs)
(lambda as
(apply values* (map (lambda: ([f : (B ... B -> A)])
(apply values (map (lambda: ([f : (B ... B -> A)])
(apply f as))
fs))))

8
collects/tests/typed-scheme/succeed/values-dots.ss
View File

@ -5,16 +5,16 @@
(call-with-values (lambda () (values 1 2)) (lambda: ([x : Number] [y : Number]) (+ x y)))
(#{call-with-values* @ Integer Integer Integer} (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y)))
(#{call-with-values @ Integer Integer Integer} (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y)))
(call-with-values* (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y)))
(call-with-values (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y)))
(: map-with-funcs (All (b ...) ((b ... b -> b) ... b -> (b ... b -> (values b ... b)))))
(define (map-with-funcs . fs)
(lambda bs
(apply values* (map (lambda: ([f : (b ... b -> b)])
(apply f bs)) fs))))
(apply values (map (lambda: ([f : (b ... b -> b)])
(apply f bs)) fs))))
(map-with-funcs + - * /)

2
collects/tests/typed-scheme/unit-tests/all-tests.ss
View File

@ -12,7 +12,7 @@
"subst-tests.ss"
"infer-tests.ss")
(require (private planet-requires infer infer-dummy))
(require (utils planet-requires) (r:infer infer infer-dummy))
(require (schemeunit))

7
collects/tests/typed-scheme/unit-tests/infer-tests.ss
View File

@ -1,7 +1,10 @@
#lang scheme/base
(require "test-utils.ss" (for-syntax scheme/base))
(require (private planet-requires type-effect-convenience type-rep union infer type-utils)
(prefix-in table: (private tables)))
(require (utils planet-requires)
(rep type-rep)
(r:infer infer)
(private type-effect-convenience union type-utils)
(prefix-in table: (utils tables)))
(require (schemeunit))

8
collects/tests/typed-scheme/unit-tests/parse-type-tests.ss
View File

@ -1,8 +1,10 @@
#lang scheme/base
(require "test-utils.ss" (for-syntax scheme/base))
(require (private planet-requires type-comparison parse-type type-rep
tc-utils type-environments type-alias-env subtype
type-name-env init-envs union type-utils))
(require (utils planet-requires tc-utils)
(env type-alias-env type-environments type-name-env init-envs)
(rep type-rep)
(private type-comparison parse-type subtype
union type-utils))
(require (rename-in (private type-effect-convenience) [-> t:->])
(except-in (private base-types) Un)

5
collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss
View File

@ -1,6 +1,9 @@
#lang scheme/base
(require "test-utils.ss" (for-syntax scheme/base))
(require (private type-rep type-effect-convenience planet-requires remove-intersect subtype union infer))
(require (rep type-rep)
(utils planet-requires)
(r:infer infer)
(private type-effect-convenience remove-intersect subtype union))
(require (schemeunit))

4
collects/tests/typed-scheme/unit-tests/subst-tests.ss
View File

@ -1,7 +1,9 @@
#lang scheme/base
(require "test-utils.ss" (for-syntax scheme/base))
(require (private planet-requires type-utils type-effect-convenience type-rep))
(require (utils planet-requires)
(rep type-rep)
(private type-utils type-effect-convenience))
(require (schemeunit))
(define-syntax-rule (s img var tgt result)

8
collects/tests/typed-scheme/unit-tests/subtype-tests.ss
View File

@ -2,8 +2,12 @@
(require "test-utils.ss")
(require (private subtype type-rep type-effect-convenience
planet-requires init-envs type-environments union infer infer-dummy))
(require (private subtype type-effect-convenience union)
(rep type-rep)
(utils planet-requires)
(env init-envs type-environments)
(r:infer infer infer-dummy))
(require (schemeunit)
(for-syntax scheme/base))

19
collects/tests/typed-scheme/unit-tests/test-utils.ss
View File

@ -3,25 +3,12 @@
(require scheme/require-syntax
scheme/match
typed-scheme/utils/utils
(for-syntax scheme/base))
(define-require-syntax private
(lambda (stx)
(syntax-case stx ()
[(_ id ...)
(andmap identifier? (syntax->list #'(id ...)))
(with-syntax ([(id* ...) (map (lambda (id) (datum->syntax
id
(string->symbol
(string-append
"typed-scheme/private/"
(symbol->string (syntax-e id))))
id id))
(syntax->list #'(id ...)))])
(syntax/loc stx (combine-in id* ...)))])))
(require (private planet-requires type-comparison utils type-utils))
(require (utils planet-requires) (private type-comparison type-utils))
(provide private typecheck (rename-out [infer r:infer]) utils env rep)
(require (schemeunit))
(define (mk-suite ts)

3
collects/tests/typed-scheme/unit-tests/type-equal-tests.ss
View File

@ -1,7 +1,8 @@
#lang scheme/base
(require "test-utils.ss" (for-syntax scheme/base))
(require (private planet-requires type-rep type-comparison type-effect-convenience union subtype))
(require (utils planet-requires) (rep type-rep)
(private type-comparison type-effect-convenience union subtype))
(require (schemeunit))
(provide type-equal-tests)

18
collects/tests/typed-scheme/unit-tests/typecheck-tests.ss
View File

@ -3,14 +3,16 @@
(require "test-utils.ss"
(for-syntax scheme/base)
(for-template scheme/base))
(require (private base-env))
(require (private base-env mutated-vars type-utils union prims type-effect-convenience type-annotation)
(typecheck typechecker)
(rep type-rep effect-rep)
(utils tc-utils planet-requires)
(env type-name-env type-environments init-envs))
(require (private planet-requires typechecker
type-rep type-effect-convenience type-env
prims type-environments tc-utils union
type-name-env init-envs mutated-vars
effect-rep type-annotation type-utils)
(for-syntax (private tc-utils typechecker base-env type-env))
(require (for-syntax (utils tc-utils)
(typecheck typechecker)
(env type-env)
(private base-env))
(for-template (private base-env base-types)))
(require (schemeunit))
@ -669,7 +671,7 @@
(tc-l #t (-val #t))
(tc-l "foo" -String)
(tc-l foo (-val 'foo))
(tc-l #:foo -Keyword)
(tc-l #:foo (-val '#:foo))
(tc-l #f (-val #f))
(tc-l #"foo" -Bytes)
[tc-l () (-val null)]

81
collects/typed-scheme/env/init-envs.ss vendored Normal file
View File

@ -0,0 +1,81 @@
#lang scheme/base
(provide (all-defined-out))
(require "../utils/utils.ss")
(require "type-env.ss"
"type-name-env.ss"
(rep type-rep effect-rep)
(for-template (rep type-rep effect-rep)
(private union)
mzlib/pconvert mzlib/shared scheme/base)
(private type-effect-convenience union)
"type-alias-env.ss"
mzlib/pconvert scheme/match mzlib/shared)
(define (initialize-type-name-env initial-type-names)
(for-each (lambda (nm/ty) (register-resolved-type-alias (car nm/ty) (cadr nm/ty))) initial-type-names))
(define (initialize-type-env initial-env)
(for-each (lambda (nm/ty) (register-type (car nm/ty) (cadr nm/ty))) initial-env))
(define (converter v basic sub)
(define (gen-constructor sym)
(string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
(match v
[(Union: elems) `(make-Union (list ,@(map sub elems)))]
[(Name: stx) `(make-Name (quote-syntax ,stx))]
[(Struct: name parent flds proc poly? pred-id cert)
`(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))]
[(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
[(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
[(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
[(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
[(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]
[(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals)))
`(,(gen-constructor tag) ,@(map sub vals))]
[(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals)))
`(,(gen-constructor tag) ,@(map sub vals))]
[_ (basic v)]))
(define (bound-in-this-module id)
(let ([binding (identifier-binding id)])
(if (and (list? binding) (module-path-index? (car binding)))
(let-values ([(mp base) (module-path-index-split (car binding))])
(not mp))
#f)))
(define (tname-env-init-code)
(define (f id ty)
(if (bound-in-this-module id)
#`(register-type-name #'#,id #,(datum->syntax #'here (print-convert ty)))
#f))
(parameterize ((current-print-convert-hook converter)
(show-sharing #f)
(booleans-as-true/false #f))
(with-syntax ([registers (filter (lambda (x) x) (type-name-env-map f))])
#'(begin (begin-for-syntax . registers)))))
(define (talias-env-init-code)
(define (f id ty)
(if (bound-in-this-module id)
#`(register-resolved-type-alias #'#,id #,(datum->syntax #'here (print-convert ty)))
#f))
(parameterize ((current-print-convert-hook converter)
(show-sharing #f)
(booleans-as-true/false #f))
(with-syntax ([registers (filter (lambda (x) x) (type-alias-env-map f))])
#'(begin (begin-for-syntax . registers)))))
(define (env-init-code)
(define (f id ty)
(if (bound-in-this-module id)
#`(register-type #'#,id #,(datum->syntax #'here (print-convert ty)))
#f))
(parameterize ((current-print-convert-hook converter)
(show-sharing #f)
(booleans-as-true/false #f))
(with-syntax ([registers (filter (lambda (x) x) (type-env-map f))])
#'(begin (begin-for-syntax . registers)))))

62
collects/typed-scheme/env/lexical-env.ss vendored Normal file
View File

@ -0,0 +1,62 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require "type-environments.ss"
(utils tc-utils)
"type-env.ss"
(private mutated-vars)
(private type-utils)
(private type-effect-convenience))
(provide (all-defined-out))
;; the current lexical environment
(define lexical-env (make-parameter (make-empty-env free-identifier=?)))
;; run code in a new env
(define-syntax with-lexical-env
(syntax-rules ()
[(_ e . b) (parameterize ([lexical-env e]) . b)]))
;; run code in an extended env
(define-syntax with-lexical-env/extend
(syntax-rules ()
[(_ is ts . b) (parameterize ([lexical-env (extend/values is ts (lexical-env))]) . b)]))
;; find the type of identifier i, looking first in the lexical env, then in the top-level env
;; identifer -> Type
(define (lookup-type/lexical i)
(lookup (lexical-env) i
(lambda (i) (lookup-type
i (lambda ()
(cond [(lookup (dotted-env) i (lambda _ #f))
=>
(lambda (a)
(-lst (substitute Univ (cdr a) (car a))))]
[else (lookup-fail (syntax-e i))]))))))
;; refine the type of i in the lexical env
;; (identifier type -> type) identifier -> environment
(define (update-type/lexical f i)
;; do the updating on the given env
;; (identifier type -> type) identifier environment -> environment
(define (update f k env)
(parameterize
([current-orig-stx k])
(let* ([v (lookup-type/lexical k)]
[new-v (f k v)]
[new-env (extend env k new-v)])
new-env)))
;; check if i is ever the target of a set!
(if (is-var-mutated? i)
;; if it is, we do nothing
(lexical-env)
;; otherwise, refine the type
(update f i (lexical-env))))
;; convenience macro for typechecking in the context of an updated env
(define-syntax with-update-type/lexical
(syntax-rules ()
[(_ f i . b)
(with-lexical-env (update-type/lexical f i) . b)]))

68
collects/typed-scheme/env/type-alias-env.ss vendored Normal file
View File

@ -0,0 +1,68 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require syntax/boundmap
(utils tc-utils)
mzlib/trace
scheme/match)
(provide register-type-alias
lookup-type-alias
resolve-type-aliases
register-resolved-type-alias
type-alias-env-map)
(define-struct alias-def () #:inspector #f)
(define-struct (unresolved alias-def) (stx [in-process #:mutable]) #:inspector #f)
(define-struct (resolved alias-def) (ty) #:inspector #f)
;; a mapping from id -> alias-def (where id is the name of the type)
(define the-mapping
(make-module-identifier-mapping))
(define (mapping-put! id v) (module-identifier-mapping-put! the-mapping id v))
;(trace mapping-put!)
;; add a name to the mapping
;; identifier type-stx -> void
(define (register-type-alias id stx)
;(printf "registering type ~a~n~a~n" (syntax-e id) id)
(mapping-put! id (make-unresolved stx #f)))
(define (register-resolved-type-alias id ty)
#;(when (eq? 'Number (syntax-e id))
(printf "registering type ~a ~a~n~a~n" id (syntax-e id) ty))
(mapping-put! id (make-resolved ty)))
(define (lookup-type-alias id parse-type [k (lambda () (tc-error "Unknown type alias: ~a" (syntax-e id)))])
(let/ec return
(match (module-identifier-mapping-get the-mapping id (lambda () (return (k))))
[(struct unresolved (stx #f))
(resolve-type-alias id parse-type)]
[(struct unresolved (stx #t))
(tc-error/stx stx "Recursive Type Alias Reference")]
[(struct resolved (t)) t])))
(define (resolve-type-alias id parse-type)
(define v (module-identifier-mapping-get the-mapping id))
(match v
[(struct unresolved (stx _))
(set-unresolved-in-process! v #t)
(let ([t (parse-type stx)])
(mapping-put! id (make-resolved t))
t)]
[(struct resolved (t))
t]))
(define (resolve-type-aliases parse-type)
(module-identifier-mapping-for-each the-mapping (lambda (id _) (resolve-type-alias id parse-type))))
;; map over the-mapping, producing a list
;; (id type -> T) -> listof[T]
(define (type-alias-env-map f)
(define sym (gensym))
(filter (lambda (e) (not (eq? sym e)))
(module-identifier-mapping-map the-mapping (lambda (id t) (if (resolved? t)
(f id (resolved-ty t))
sym)))))

65
collects/typed-scheme/env/type-env.ss vendored Normal file
View File

@ -0,0 +1,65 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require syntax/boundmap
(utils tc-utils)
(private type-utils))
(provide register-type
finish-register-type
maybe-finish-register-type
register-type/undefined
lookup-type
register-types
check-all-registered-types
type-env-map)
;; module-identifier-mapping from id -> type or Box[type]
;; where id is a variable, and type is the type of the variable
;; if the result is a box, then the type has not actually been defined, just registered
(define the-mapping (make-module-identifier-mapping))
;; add a single type to the mapping
;; identifier type -> void
(define (register-type id type)
;(printf "register-type ~a~n" (syntax-e id))
(module-identifier-mapping-put! the-mapping id type))
;; add a single type to the mapping
;; identifier type -> void
(define (register-type/undefined id type)
;(printf "register-type/undef ~a~n" (syntax-e id))
(module-identifier-mapping-put! the-mapping id (box type)))
;; add a bunch of types to the mapping
;; listof[id] listof[type] -> void
(define (register-types ids types)
(for-each register-type ids types))
;; given an identifier, return the type associated with it
;; if none found, calls lookup-fail
;; identifier -> type
(define (lookup-type id [fail-handler (lambda () (lookup-fail (syntax-e id)))])
(let ([v (module-identifier-mapping-get the-mapping id fail-handler)])
(if (box? v) (unbox v) v)))
(define (maybe-finish-register-type id)
(let ([v (module-identifier-mapping-get the-mapping id)])
(if (box? v)
(register-type id (unbox v))
#f)))
(define (finish-register-type id)
(unless (maybe-finish-register-type id)
(int-err "finishing type that was already finished: ~a" (syntax-e id))))
(define (check-all-registered-types)
(module-identifier-mapping-for-each
the-mapping
(lambda (id e)
(when (box? e) (tc-error/stx id "Declaration for ~a provided, but with no definition" (syntax-e id))))))
;; map over the-mapping, producing a list
;; (id type -> T) -> listof[T]
(define (type-env-map f)
(module-identifier-mapping-map the-mapping f))

69
collects/typed-scheme/env/type-environments.ss vendored Normal file
View File

@ -0,0 +1,69 @@
#lang scheme/base
(provide current-tvars
extend
lookup
make-empty-env
extend-env
extend/values
dotted-env
initial-tvar-env
with-dotted-env/extend)
(require (prefix-in r: "../utils/utils.ss"))
(require scheme/match
(r:utils tc-utils))
;; eq? has the type of equal?, and l is an alist (with conses!)
(define-struct env (eq? l))
;; the initial type variable environment - empty
;; this is used in the parsing of types
(define initial-tvar-env (make-env eq? '()))
;; a parameter for the current type variables
(define current-tvars (make-parameter initial-tvar-env))
(define (make-empty-env p?) (make-env p? '()))
;; the environment for types of ... variables
(define dotted-env (make-parameter (make-empty-env free-identifier=?)))
;; extend that works on single arguments
(define (extend e k v)
(match e
[(struct env (f l)) (make-env f (cons (cons k v) l))]
[_ (int-err "extend: expected environment, got ~a" e)]))
(define (extend-env ks vs e)
(match e
[(struct env (f l)) (make-env f (append (map cons ks vs) l))]
[_ (int-err "extend-env: expected environment, got ~a" e)]))
(define (lookup e key fail)
(match e
[(struct env (f? l))
(let loop ([l l])
(cond [(null? l) (fail key)]
[(f? (caar l) key) (cdar l)]
[else (loop (cdr l))]))]
[_ (int-err "lookup: expected environment, got ~a" e)]))
;; takes two lists of sets to be added, which are either added one at a time, if the
;; elements are not lists, or all at once, if the elements are lists
(define (extend/values kss vss env)
(foldr (lambda (ks vs env)
(cond [(and (list? ks) (list? vs))
(extend-env ks vs env)]
[(or (list? ks) (list? vs))
(int-err "not both lists in extend/values: ~a ~a" ks vs)]
[else (extend-env (list ks) (list vs) env)]))
env kss vss))
;; run code in an extended dotted env
(define-syntax with-dotted-env/extend
(syntax-rules ()
[(_ i t v . b) (parameterize ([dotted-env (extend/values (list i) (list (cons t v)) (dotted-env))]) . b)]))

44
collects/typed-scheme/env/type-name-env.ss vendored Normal file
View File

@ -0,0 +1,44 @@
#lang scheme/base
(require "../utils/utils.ss")
(require syntax/boundmap
mzlib/trace
(utils tc-utils)
(private type-utils))
(provide register-type-name
lookup-type-name
register-type-names
type-name-env-map)
;; a mapping from id -> type (where id is the name of the type)
(define the-mapping
(make-module-identifier-mapping))
(define (mapping-put! id v) (module-identifier-mapping-put! the-mapping id v))
;(trace mapping-put!)
;; add a name to the mapping
;; identifier Type -> void
(define (register-type-name id [type #t])
;(printf "registering type ~a~n~a~n" (syntax-e id) id)
(mapping-put! id type))
;; add a bunch of names to the mapping
;; listof[identifier] listof[type] -> void
(define (register-type-names ids types)
(for-each register-type-name ids types))
;; given an identifier, return the type associated with it
;; optional argument is failure continuation - default calls lookup-fail
;; identifier (-> error) -> type
(define (lookup-type-name id [k (lambda () (lookup-fail (syntax-e id)))])
(begin0
(module-identifier-mapping-get the-mapping id k)
(add-type-name-reference id)))
;; map over the-mapping, producing a list
;; (id type -> T) -> listof[T]
(define (type-name-env-map f)
(module-identifier-mapping-map the-mapping f))

51
collects/typed-scheme/infer/constraint-structs.ss Normal file
View File

@ -0,0 +1,51 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require (rep type-rep)
scheme/contract)
;; S, T types
;; X a var
(define-struct c (S X T) #:prefab)
;; fixed : Listof[c]
;; rest : option[c]
(define-struct dcon (fixed rest) #:prefab)
;; fixed : Listof[c]
;; rest : c
(define-struct dcon-exact (fixed rest) #:prefab)
;; type : c
;; bound : var
(define-struct dcon-dotted (type bound) #:prefab)
;; map : hash mapping variable to dcon or dcon-dotted
(define-struct dmap (map) #:prefab)
;; maps is a list of pairs of
;; - functional maps from vars to c's
;; - dmaps (see dmap.ss)
;; we need a bunch of mappings for each cset to handle case-lambda
;; because case-lambda can generate multiple possible solutions, and we
;; don't want to rule them out too early
(define-struct cset (maps) #:prefab)
(define (hashof k/c v/c)
(flat-named-contract
(format "#<hashof ~a ~a>" k/c v/c)
(lambda (h)
(define k/c? (if (flat-contract? k/c) (flat-contract-predicate k/c) k/c))
(define v/c? (if (flat-contract? v/c) (flat-contract-predicate v/c) v/c))
(and (hash? h)
(for/and ([(k v) h])
(and (k/c? k)
(v/c? v)))))))
(provide/contract (struct c ([S Type?] [X symbol?] [T Type?]))
(struct dcon ([fixed (listof c?)] [rest (or/c c? false/c)]))
(struct dcon-exact ([fixed (listof c?)] [rest c?]))
(struct dcon-dotted ([type c?] [bound symbol?]))
(struct dmap ([map (hashof symbol? (or/c dcon? dcon-exact? dcon-dotted?))]))
(struct cset ([maps (listof (cons/c (hashof symbol? c?) dmap?))])))

92
collects/typed-scheme/infer/constraints.ss Normal file
View File

@ -0,0 +1,92 @@
#lang scheme/unit
(require (except-in "../utils/utils.ss" extend))
(require (private type-effect-convenience type-utils union subtype)
(rep type-rep)
(utils tc-utils)
"signatures.ss" "constraint-structs.ss"
scheme/match)
(import restrict^ dmap^)
(export constraints^)
(define-values (fail-sym exn:infer?)
(let ([sym (gensym)])
(values sym (lambda (s) (eq? s sym)))))
;; why does this have to be duplicated?
;; inference failure - masked before it gets to the user program
(define-syntaxes (fail!)
(syntax-rules ()
[(_ s t) (raise fail-sym)]))
;; Widest constraint possible
(define (no-constraint v)
(make-c (Un) v Univ))
(define (empty-cset X)
(make-cset (list (cons (for/hash ([x X]) (values x (no-constraint x)))
(make-dmap (make-immutable-hash null))))))
(define (insert cs var S T)
(match cs
[(struct cset (maps))
(make-cset (for/list ([(map dmap) (in-pairs maps)])
(cons (hash-set map var (make-c S var T))
dmap)))]))
;; a stupid impl
(define (meet S T)
(let ([s* (restrict S T)])
(if (and (subtype s* S)
(subtype s* T))
s*
(Un))))
(define (join T U) (Un T U))
(define (c-meet c1 c2 [var #f])
(match* (c1 c2)
[((struct c (S X T)) (struct c (S* X* T*)))
(unless (or var (eq? X X*))
(int-err "Non-matching vars in c-meet: ~a ~a" X X*))
(let ([S (join S S*)] [T (meet T T*)])
(unless (subtype S T)
(fail! S T))
(make-c S (or var X) T))]))
(define (subst-all/c sub -c)
(match -c
[(struct c (S X T))
(make-c (subst-all sub S)
(F-n (subst-all sub (make-F X)))
(subst-all sub T))]))
(define (cset-meet x y)
(match* (x y)
[((struct cset (maps1)) (struct cset (maps2)))
(let ([maps (filter values
(for*/list
([(map1 dmap1) (in-pairs maps1)]
[(map2 dmap2) (in-pairs maps2)])
(with-handlers ([exn:infer? (lambda (_) #f)])
(cons
(hash-union map1 map2 (lambda (k v1 v2) (c-meet v1 v2)))
(dmap-meet dmap1 dmap2)))))])
(when (null? maps)
(fail! maps1 maps2))
(make-cset maps))]
[(_ _) (int-err "Got non-cset: ~a ~a" x y)]))
(define (cset-meet* args)
(for/fold ([c (make-cset (list (cons (make-immutable-hash null)
(make-dmap (make-immutable-hash null)))))])
([a args])
(cset-meet a c)))
(define (cset-combine l)
(let ([mapss (map cset-maps l)])
(make-cset (apply append mapss))))

66
collects/typed-scheme/infer/dmap.ss Normal file
View File

@ -0,0 +1,66 @@
#lang scheme/unit
(require (except-in "../utils/utils.ss" extend))
(require "signatures.ss" "constraint-structs.ss"
(utils tc-utils)
scheme/match)
(import constraints^)
(export dmap^)
;; dcon-meet : dcon dcon -> dcon
(define (dcon-meet dc1 dc2)
(match* (dc1 dc2)
[((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2))
(struct dcon-exact (fixed2 rest2))))
(unless (and rest2 (= (length fixed1) (length fixed2)))
(fail! fixed1 fixed2))
(make-dcon-exact
(for/list ([c1 fixed1]
[c2 fixed2])
(c-meet c1 c2 (c-X c1)))
(c-meet rest1 rest2 (c-X rest1)))]
[((struct dcon (fixed1 rest1)) (struct dcon-exact (fixed2 rest2)))
(dcon-meet dc2 dc1)]
[((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f)))
(unless (= (length fixed1) (length fixed2))
(fail! fixed1 fixed2))
(make-dcon
(for/list ([c1 fixed1]
[c2 fixed2])
(c-meet c1 c2 (c-X c1)))
#f)]
[((struct dcon (fixed1 #f)) (struct dcon (fixed2 rest)))
(unless (>= (length fixed1) (length fixed2))
(fail! fixed1 fixed2))
(make-dcon
(for/list ([c1 fixed1]
[c2 (in-list-forever fixed2 rest)])
(c-meet c1 c2 (c-X c1)))
#f)]
[((struct dcon (fixed1 rest)) (struct dcon (fixed2 #f)))
(dcon-meet dc2 dc1)]
[((struct dcon (fixed1 rest1)) (struct dcon (fixed2 rest2)))
(let-values ([(shorter longer srest lrest)
(if (< (length fixed1) (length fixed2))
(values fixed1 fixed2 rest1 rest2)
(values fixed2 fixed1 rest2 rest1))])
(make-dcon
(for/list ([c1 longer]
[c2 (in-list-forever shorter srest)])
(c-meet c1 c2 (c-X c1)))
(c-meet lrest srest (c-X lrest))))]
[((struct dcon-dotted (c1 bound1)) (struct dcon-dotted (c2 bound2)))
(unless (eq? bound1 bound2)
(fail! bound1 bound2))
(make-dcon-dotted (c-meet c1 c2 bound1) bound1)]
[((struct dcon _) (struct dcon-dotted _))
(fail! dc1 dc2)]
[((struct dcon-dotted _) (struct dcon _))
(fail! dc1 dc2)]
[(_ _) (int-err "Got non-dcons: ~a ~a" dc1 dc2)]))
(define (dmap-meet dm1 dm2)
(make-dmap
(hash-union (dmap-map dm1) (dmap-map dm2)
(lambda (k dc1 dc2) (dcon-meet dc1 dc2)))))

491
collects/typed-scheme/infer/infer-unit.ss Normal file
View File

@ -0,0 +1,491 @@
#lang scheme/unit
(require (except-in "../utils/utils.ss"))
(require (rep free-variance type-rep effect-rep rep-utils)
(private type-effect-convenience union subtype remove-intersect)
(utils tc-utils)
(env type-name-env)
(except-in (private type-utils) Dotted)
"constraint-structs.ss"
"signatures.ss"
(only-in (env type-environments) lookup current-tvars)
scheme/match
mzlib/etc
mzlib/trace
scheme/list)
(import dmap^ constraints^ promote-demote^)
(export infer^)
(define (empty-set) '())
(define current-seen (make-parameter (empty-set)))
(define (seen-before s t) (cons (Type-seq s) (Type-seq t)))
(define (remember s t A) (cons (seen-before s t) A))
(define (seen? s t) (member (seen-before s t) (current-seen)))
(define (dmap-constraint dmap dbound v)
(let ([dc (hash-ref dmap dbound #f)])
(match dc
[(struct dcon (fixed #f))
(if (eq? dbound v)
(no-constraint v)
(hash-ref fixed v (no-constraint v)))]
[(struct dcon (fixed rest))
(if (eq? dbound v)
rest
(hash-ref fixed v (no-constraint v)))]
[(struct dcon-dotted (type bound))
(if (eq? bound v)
type
(no-constraint v))]
[_ (no-constraint v)])))
(define (map/cset f cset)
(make-cset (for/list ([(cmap dmap) (in-pairs (cset-maps cset))])
(f cmap dmap))))
(define (singleton-dmap dbound dcon)
(make-dmap (make-immutable-hash (list (cons dbound dcon)))))
(define (hash-remove* hash keys)
(for/fold ([h hash]) ([k (in-list keys)]) (hash-remove h k)))
(define (mover cset dbound vars f)
(map/cset
(lambda (cmap dmap)
(cons (hash-remove* cmap vars)
(dmap-meet
(singleton-dmap
dbound
(f cmap))
dmap)))
cset))
(define (move-vars-to-dmap cset dbound vars)
(mover cset dbound vars
(lambda (cmap)
(make-dcon (for/list ([v vars])
(hash-ref cmap v
(lambda () (int-err "No constraint for new var ~a" v))))
#f))))
(define (move-rest-to-dmap cset dbound #:exact [exact? #f])
(mover cset dbound (list dbound)
(lambda (cmap)
((if exact? make-dcon-exact make-dcon)
null
(hash-ref cmap dbound
(lambda () (int-err "No constraint for bound ~a" dbound)))))))
(define (move-vars+rest-to-dmap cset dbound vars #:exact [exact? #f])
(map/cset
(lambda (cmap dmap)
(cons (hash-remove* cmap vars)
(dmap-meet
(singleton-dmap
dbound
((if exact? make-dcon-exact make-dcon)
(for/list ([v vars])
(hash-ref cmap v
(lambda () (int-err "No constraint for new var ~a" v))))
(hash-ref cmap dbound
(lambda () (int-err "No constraint for bound ~a" dbound)))))
dmap)))
cset))
;; t and s must be *latent* effects
(define (cgen/eff V X t s)
(match* (t s)
[(e e) (empty-cset X)]
[((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: s))
(cset-meet (cgen V X t s) (cgen V X s t))]
[((Latent-Remove-Effect: t) (Latent-Remove-Effect: s))
(cset-meet (cgen V X t s) (cgen V X s t))]
[(_ _) (fail! t s)]))
(define (cgen/eff/list V X ts ss)
(unless (>= (length ts) (length ss)) (fail! ts ss))
(cset-meet* (for/list ([t ts] [s ss]) (cgen/eff V X t s))))
(define (cgen/arr V X t-arr s-arr)
(define (cg S T) (cgen V X S T))
(match* (t-arr s-arr)
[((arr: ts t #f #f '() t-thn-eff t-els-eff)
(arr: ss s #f #f '() s-thn-eff s-els-eff))
(cset-meet*
(list (cgen/list V X ss ts)
(cg t s)
(cgen/eff/list V X t-thn-eff s-thn-eff)
(cgen/eff/list V X t-els-eff s-els-eff)))]
[((arr: ts t t-rest #f '() t-thn-eff t-els-eff)
(arr: ss s s-rest #f '() s-thn-eff s-els-eff))
(let ([arg-mapping
(cond [(and t-rest s-rest (<= (length ts) (length ss)))
(cgen/list V X (cons s-rest ss) (cons t-rest (extend ss ts t-rest)))]
[(and t-rest s-rest (>= (length ts) (length ss)))
(cgen/list V X (cons s-rest (extend ts ss s-rest)) (cons t-rest ts))]
[(and t-rest (not s-rest) (<= (length ts) (length ss)))
(cgen/list V X ss (extend ss ts t-rest))]
[(and s-rest (not t-rest) (>= (length ts) (length ss)))
(cgen/list V X (extend ts ss s-rest) ts)]
[else (fail! S T)])]
[ret-mapping (cg t s)])
(cset-meet*
(list arg-mapping ret-mapping
(cgen/eff/list V X t-thn-eff s-thn-eff)
(cgen/eff/list V X t-els-eff s-els-eff))))]
[((arr: ts t #f (cons dty dbound) '() t-thn-eff t-els-eff)
(arr: ss s #f #f '() s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ts) (length ss))
(fail! S T))
(let* ([num-vars (- (length ss) (length ts))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))]
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null t-thn-eff t-els-eff) s-arr)])
(move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f #f '() t-thn-eff t-els-eff)
(arr: ss s #f (cons dty dbound) '() s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ss) (length ts))
(fail! S T))
(let* ([num-vars (- (length ts) (length ss))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))]
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null s-thn-eff s-els-eff))])
(move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f (cons t-dty dbound) '() t-thn-eff t-els-eff)
(arr: ss s #f (cons s-dty dbound) '() s-thn-eff s-els-eff))
(unless (= (length ts) (length ss))
(fail! S T))
;; If we want to infer the dotted bound, then why is it in both types?
(when (memq dbound X)
(fail! S T))
(let* ([arg-mapping (cgen/list V X ss ts)]
[darg-mapping (cgen V X s-dty t-dty)]
[ret-mapping (cg t s)])
(cset-meet*
(list arg-mapping darg-mapping ret-mapping
(cgen/eff/list V X t-thn-eff s-thn-eff)
(cgen/eff/list V X t-els-eff s-els-eff))))]
[((arr: ts t #f (cons t-dty dbound) '() t-thn-eff t-els-eff)
(arr: ss s #f (cons s-dty dbound*) '() s-thn-eff s-els-eff))
(unless (= (length ts) (length ss))
(fail! S T))
(let* ([arg-mapping (cgen/list V X ss ts)]
[darg-mapping (cgen V (cons dbound* X) s-dty t-dty)]
[ret-mapping (cg t s)])
(cset-meet*
(list arg-mapping darg-mapping ret-mapping
(cgen/eff/list V X t-thn-eff s-thn-eff)
(cgen/eff/list V X t-els-eff s-els-eff))))]
[((arr: ts t t-rest #f '() t-thn-eff t-els-eff)
(arr: ss s #f (cons s-dty dbound) '() s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(if (<= (length ts) (length ss))
;; the simple case
(let* ([arg-mapping (cgen/list V X ss (extend ss ts t-rest))]
[darg-mapping (move-rest-to-dmap (cgen V X s-dty t-rest) dbound)]
[ret-mapping (cg t s)])
(cset-meet* (list arg-mapping darg-mapping ret-mapping
(cgen/eff/list V X t-thn-eff s-thn-eff)
(cgen/eff/list V X t-els-eff s-els-eff))))
;; the hard case
(let* ([num-vars (- (length ts) (length ss))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))]
[new-cset (cgen/arr V (append vars X) t-arr
(make-arr (append ss new-tys) s #f (cons s-dty dbound) null s-thn-eff s-els-eff))])
(move-vars+rest-to-dmap new-cset dbound vars)))]
;; If dotted <: starred is correct, add it below. Not sure it is.
[((arr: ts t #f (cons t-dty dbound) '() t-thn-eff t-els-eff)
(arr: ss s s-rest #f '() s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(cond [(< (length ts) (length ss))
;; the hard case
(let* ([num-vars (- (length ss) (length ts))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound t-dty))]
[arg-mapping (cgen/list V (append vars X) ss (append ts new-tys))]
[darg-mapping (cgen V X s-rest t-dty)]
[ret-mapping (cg t s)]
[new-cset
(cset-meet* (list arg-mapping darg-mapping ret-mapping
(cgen/eff/list V X t-thn-eff s-thn-eff)
(cgen/eff/list V X t-els-eff s-els-eff)))])
(move-vars+rest-to-dmap new-cset dbound vars #:exact #t))]
[else
;; the simple case
(let* ([arg-mapping (cgen/list V X (extend ts ss s-rest) ts)]
[darg-mapping (move-rest-to-dmap (cgen V X s-rest t-dty) dbound #:exact #t)]
[ret-mapping (cg t s)])
(cset-meet* (list arg-mapping darg-mapping ret-mapping
(cgen/eff/list V X t-thn-eff s-thn-eff)
(cgen/eff/list V X t-els-eff s-els-eff))))])]
[(_ _) (fail! S T)]))
;; determine constraints on the variables in X that would make T a supertype of S
;; the resulting constraints will not mention V
(define (cgen V X S T)
(define (cg S T) (cgen V X S T))
(define empty (empty-cset X))
(define (singleton S X T)
(insert empty X S T))
(if (seen? S T)
empty
(parameterize ([match-equality-test type-equal?]
[current-seen (remember S T (current-seen))])
(match*
(S T)
[(a a) empty]
[(_ (Univ:)) empty]
[((F: (? (lambda (e) (memq e X)) v)) S)
(when (match S
[(F: v*)
(just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
[_ #f])
(fail! S T))
(singleton (Un) v (var-demote S V))]
[(S (F: (? (lambda (e) (memq e X)) v)))
(when (match S
[(F: v*)
(just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
[_ #f])
(fail! S T))
(singleton (var-promote S V) v Univ)]
;; two unions with the same number of elements, so we just try to unify them pairwise
#;[((Union: l1) (Union: l2))
(=> unmatch)
(unless (= (length l1) (length l2))
(unmatch))
(cgen-union V X l1 l2)]
#;[((Poly: v1 b1) (Poly: v2 b2))
(unless (= (length v1) (length v2))
(fail! S T))
(let ([b2* (subst-all (map list v2 v1) b2)])
(cg b1 b2*))]
#;[((PolyDots: (list v1 ... r1) b1) (PolyDots: (list v2 ... r2) b2))
(unless (= (length v1) (length v2))
(fail! S T))
(let ([b2* (substitute-dotted v1 v1 v2 (subst-all (map list v2 v1) b2))])
(cg b1 b2*))]
[((Poly: v1 b1) T)
(cgen (append v1 V) X b1 T)]
#;[((PolyDots: (list v1 ... r1) b1) T)
(let ([b1* (var-demote b1 (cons r1 v1))])
(cg b1* T))]
#;
[((Poly-unsafe: n b) (Poly-unsafe: n* b*))
(unless (= n n*)
(fail! S T))
(cg b b*)]
[((Union: es) S) (cset-meet* (cons empty (for/list ([e es]) (cg e S))))]
;; we might want to use multiple csets here, but I don't think it makes a difference
[(S (Union: es)) (or
(for/or
([e es])
(with-handlers
([exn:infer? (lambda _ #f)])
(cg S e)))
(fail! S T))]
[((Struct: nm p flds proc _ _ _) (Struct: nm p flds* proc* _ _ _))
(let-values ([(flds flds*)
(cond [(and proc proc*)
(values (cons proc flds) (cons proc* flds*))]
[(or proc proc*)
(fail! S T)]
[else (values flds flds*)])])
(cgen/list V X flds flds*))]
[((Name: n) (Name: n*))
(if (free-identifier=? n n*)
null
(fail! S T))]
[((Pair: a b) (Pair: a* b*))
(cset-meet (cg a a*) (cg b b*))]
;; if we have two mu's, we rename them to have the same variable
;; and then compare the bodies
[((Mu-unsafe: s) (Mu-unsafe: t))
(cg s t)]
;; other mu's just get unfolded
[(s (? Mu? t)) (cg s (unfold t))]
[((? Mu? s) t) (cg (unfold s) t)]
;; type application
[((App: (Name: n) args _)
(App: (Name: n*) args* _))
(unless (free-identifier=? n n*)
(fail! S T))
(let ([x (instantiate-poly (lookup-type-name n) args)]
[y (instantiate-poly (lookup-type-name n) args*)])
(cg x y))]
[((Values: ss) (Values: ts))
(unless (= (length ss) (length ts))
(fail! ss ts))
(cgen/list V X ss ts)]
[((Values: ss) (ValuesDots: ts t-dty dbound))
(unless (>= (length ss) (length ts))
(fail! ss ts))
(unless (memq dbound X)
(fail! S T))
(let* ([num-vars (- (length ss) (length ts))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound t-dty))]
[new-cset (cgen/list V (append vars X) ss (append ts new-tys))])
(move-vars-to-dmap new-cset dbound vars))]
[((ValuesDots: ss s-dty dbound) (Values: ts))
(unless (>= (length ts) (length ss))
(fail! ss ts))
(unless (memq dbound X)
(fail! S T))
(let* ([num-vars (- (length ts) (length ss))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))]
[new-cset (cgen/list V (append vars X) (append ss new-tys) ts)])
(move-vars-to-dmap new-cset dbound vars))]
[((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
(when (memq dbound X) (fail! ss ts))
(cgen/list V X (cons s-dty ss) (cons t-dty ts))]
[((Vector: e) (Vector: e*))
(cset-meet (cg e e*) (cg e* e))]
[((Box: e) (Box: e*))
(cset-meet (cg e e*) (cg e* e))]
[((Hashtable: s1 s2) (Hashtable: t1 t2))
;; the key is covariant, the value is invariant
(cset-meet* (list (cg s1 t1) (cg t2 s2) (cg s2 t2)))]
[((Syntax: s1) (Syntax: s2))
(cg s1 s2)]
;; parameters are just like one-arg functions
[((Param: in1 out1) (Param: in2 out2))
(cset-meet (cg in2 in1) (cg out1 out2))]
[((Function: (list t-arr ...))
(Function: (list s-arr ...)))
(=> unmatch)
(cset-combine
(filter
values ;; only generate the successful csets
(for*/list
([t-arr t-arr] [s-arr s-arr])
(with-handlers ([exn:infer? (lambda (_) #f)])
(cgen/arr V X t-arr s-arr)))))]
[(_ _)
(cond [(subtype S T) empty]
;; or, nothing worked, and we fail
[else (fail! S T)])]))))
(define (check-vars must-vars subst)
(and (for/and ([v must-vars])
(assq v subst))
subst))
(define (subst-gen C R must-vars)
(define (constraint->type v #:variable [variable #f])
(match v
[(struct c (S X T))
(let ([var (hash-ref (free-vars* R) (or variable X) Constant)])
;(printf "variance was: ~a~nR was ~a~nX was ~a~n" var R (or variable X))
(evcase var
[Constant S]
[Covariant S]
[Contravariant T]
[Invariant S]
[Dotted T]))]))
(match (car (cset-maps C))
[(cons cmap (struct dmap (dm)))
(check-vars
must-vars
(append
(for/list ([(k dc) dm])
(match dc
[(struct dcon (fixed rest))
(list k
(for/list ([f fixed])
(constraint->type f #:variable k))
(and rest (constraint->type rest)))]
[(struct dcon-exact (fixed rest))
(list k
(for/list ([f fixed])
(constraint->type f #:variable k))
(constraint->type rest))]))
(for/list ([(k v) cmap])
(list k (constraint->type v)))))]))
(define (cgen/list V X S T)
(unless (= (length S) (length T))
(fail! S T))
(cset-meet* (for/list ([s S] [t T]) (cgen V X s t))))
;; X : variables to infer
;; S : actual argument types
;; T : formal argument types
;; R : result type
;; must-vars : variables that must be in the substitution
;; expected : boolean
;; returns a substitution
;; if R is #f, we don't care about the substituion
;; just return a boolean result
(define (infer X S T R must-vars [expected #f])
(with-handlers ([exn:infer? (lambda _ #f)])
(let ([cs (cgen/list null X S T)])
(if (not expected)
(subst-gen cs R must-vars)
(cset-meet cs (cgen null X R expected))))))
;; like infer, but T-var is the vararg type:
(define (infer/vararg X S T T-var R must-vars [expected #f])
(define new-T (extend S T T-var))
(and ((length S) . >= . (length T))
(infer X S new-T R must-vars expected)))
;; like infer, but dotted-var is the bound on the ...
;; and T-dotted is the repeated type
(define (infer/dots X dotted-var S T T-dotted R must-vars [expected #f])
(with-handlers ([exn:infer? (lambda _ #f)])
(let* ([short-S (take S (length T))]
[rest-S (drop S (length T))]
[cs-short (cgen/list null (cons dotted-var X) short-S T)]
[new-vars (for/list ([i (in-range (length rest-S))]) (gensym dotted-var))]
[new-Ts (for/list ([v new-vars])
(substitute (make-F v) dotted-var
(substitute-dots (map make-F new-vars) #f dotted-var T-dotted)))]
[cs-dotted (cgen/list null (append new-vars X) rest-S new-Ts)]
[cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)]
[cs (cset-meet cs-short cs-dotted*)])
(if (not expected)
(subst-gen cs R must-vars)
(cset-meet cs (cgen null X R expected))))))
(define (infer/simple S T R)
(infer (fv/list T) S T R))
(define (i s t r)
(infer/simple (list s) (list t) r))
;(trace cgen/arr #;cgen #;cgen/list)

12
collects/typed-scheme/infer/infer.ss Normal file
View File

@ -0,0 +1,12 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" infer))
(require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss"
"restrict.ss" "promote-demote.ss"
(only-in scheme/unit provide-signature-elements)
(utils unit-utils))
(provide-signature-elements restrict^ infer^)
(define-values/link-units/infer
infer@ constraints@ dmap@ restrict@ promote-demote@)

92
collects/typed-scheme/infer/promote-demote.ss Normal file
View File

@ -0,0 +1,92 @@
#lang scheme/unit
(require "../utils/utils.ss")
(require (rep type-rep)
(private type-effect-convenience union type-utils)
"signatures.ss"
scheme/list)
(import)
(export promote-demote^)
(define (V-in? V . ts)
(for/or ([e (append* (map fv ts))])
(memq e V)))
(define (var-promote T V)
(define (vp t) (var-promote t V))
(define (inv t) (if (V-in? V t) Univ t))
(type-case vp T
[#:F name (if (memq name V) Univ T)]
[#:Vector t (make-Vector (inv t))]
[#:Box t (make-Box (inv t))]
[#:Hashtable k v
(if (V-in? V v)
Univ
(make-Hashtable (vp k) v))]
[#:Param in out
(make-Param (var-demote in V)
(vp out))]
[#:arr dom rng rest drest kws thn els
(cond
[(apply V-in? V (append thn els))
(make-arr null (Un) Univ #f null null)]
[(and drest (memq (cdr drest) V))
(make-arr (for/list ([d dom]) (var-demote d V))
(vp rng)
(var-demote (car drest) V)
#f
(for/list ([(kw kwt) (in-pairs kws)])
(cons kw (var-demote kwt V)))
thn
els)]
[else
(make-arr (for/list ([d dom]) (var-demote d V))
(vp rng)
(and rest (var-demote rest V))
(and drest
(cons (var-demote (car drest) V)
(cdr drest)))
(for/list ([(kw kwt) (in-pairs kws)])
(cons kw (var-demote kwt V)))
thn
els)])]))
(define (var-demote T V)
(define (vd t) (var-demote t V))
(define (inv t) (if (V-in? V t) (Un) t))
(type-case vd T
[#:F name (if (memq name V) (Un) T)]
[#:Vector t (make-Vector (inv t))]
[#:Box t (make-Box (inv t))]
[#:Hashtable k v
(if (V-in? V v)
(Un)
(make-Hashtable (vd k) v))]
[#:Param in out
(make-Param (var-promote in V)
(vd out))]
[#:arr dom rng rest drest kws thn els
(cond
[(apply V-in? V (append thn els))
(make-arr null (Un) Univ #f null null)]
[(and drest (memq (cdr drest) V))
(make-arr (for/list ([d dom]) (var-promote d V))
(vd rng)
(var-promote (car drest) V)
#f
(for/list ([(kw kwt) (in-pairs kws)])
(cons kw (var-promote kwt V)))
thn
els)]
[else
(make-arr (for/list ([d dom]) (var-promote d V))
(vd rng)
(and rest (var-promote rest V))
(and drest
(cons (var-promote (car drest) V)
(cdr drest)))
(for/list ([(kw kwt) (in-pairs kws)])
(cons kw (var-promote kwt V)))
thn
els)])]))

37
collects/typed-scheme/infer/restrict.ss Normal file
View File

@ -0,0 +1,37 @@
#lang scheme/unit
(require "../utils/utils.ss")
(require (rep type-rep)
(private type-utils union remove-intersect subtype)
"signatures.ss"
scheme/match)
(import infer^)
(export restrict^)
;; NEW IMPL
;; restrict t1 to be a subtype of t2
(define (restrict t1 t2)
;; we don't use union map directly, since that might produce too many elements
(define (union-map f l)
(match l
[(Union: es)
(let ([l (map f es)])
;(printf "l is ~a~n" l)
(apply Un l))]))
(cond
[(subtype t1 t2) t1] ;; already a subtype
[(match t2
[(Poly: vars t)
(let ([subst (infer vars (list t1) (list t) t1 vars)])
(and subst (restrict t1 (subst-all subst t1))))]
[_ #f])]
[(Union? t1) (union-map (lambda (e) (restrict e t2)) t1)]
[(Mu? t1)
(restrict (unfold t1) t2)]
[(Mu? t2) (restrict t1 (unfold t2))]
[(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
[(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
[else t2] ;; t2 and t1 have a complex relationship, so we punt
))

29
collects/typed-scheme/infer/signatures.ss Normal file
View File

@ -0,0 +1,29 @@
#lang scheme/base
(require scheme/unit)
(provide (all-defined-out))
(define-signature dmap^
(dmap-meet))
(define-signature promote-demote^
(var-promote var-demote))
(define-signature constraints^
(exn:infer?
fail-sym
;; inference failure - masked before it gets to the user program
(define-syntaxes (fail!)
(syntax-rules ()
[(_ s t) (raise fail-sym)]))
cset-meet cset-meet*
no-constraint
empty-cset
insert
cset-combine
c-meet))
(define-signature restrict^
(restrict))
(define-signature infer^
(infer infer/vararg infer/dots))

5
collects/typed-scheme/no-check.ss Normal file
View File

@ -0,0 +1,5 @@
#lang scheme/base
(require "private/prims.ss")
(provide (all-from-out scheme/base)
(all-from-out "private/prims.ss"))

13
collects/typed-scheme/no-check/lang/reader.ss Normal file
View File

@ -0,0 +1,13 @@
#lang scheme/base
(require (prefix-in r: "../../typed-reader.ss")
(only-in syntax/module-reader wrap-read-all))
(define (*read in modpath line col pos)
(wrap-read-all 'typed-scheme/no-check in r:read modpath #f line col pos))
(define (*read-syntax src in modpath line col pos)
(wrap-read-all
'typed-scheme/no-check in (lambda (in) (r:read-syntax src in))
modpath src line col pos))
(provide (rename-out [*read read] [*read-syntax read-syntax]))

35
collects/typed-scheme/private/base-env.ss
View File

@ -3,6 +3,7 @@
;; these are libraries providing functions we add types to that are not in scheme/base
(require
"extra-procs.ss"
"../utils/utils.ss"
(only-in scheme/list cons? take drop add-between last filter-map)
(only-in rnrs/lists-6 fold-left)
'#%paramz
@ -15,13 +16,12 @@
;; these are all for constructing the types given to variables
(require (for-syntax
scheme/base
"init-envs.ss"
"effect-rep.ss"
(except-in "type-rep.ss" make-arr)
(env init-envs)
(except-in (rep effect-rep type-rep) make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"
"tc-structs.ss"))
(typecheck tc-structs)))
(define-for-syntax (initialize-others)
(d-s date
@ -57,6 +57,9 @@
[qq-append qq-append-ty]
[id ty] ...)))]))
(define-for-syntax (one-of/c . args)
(apply Un (map -val args)))
(define-initial-env initial-env
;; make-promise
@ -145,9 +148,13 @@
[string-append (->* null -String -String)]
[open-input-string (-> -String -Input-Port)]
[open-output-file
(cl->
[(-Pathlike) -Port]
[(-Pathlike Sym) -Port])]
(->key -Pathlike
#:mode (one-of/c 'binary 'text) #f
#:exists (one-of/c 'error 'append 'update 'can-update
'replace 'truncate
'must-truncate 'truncate/replace)
#f
-Output-Port)]
[read (cl->
[(-Port) -Sexp]
[() -Sexp])]
@ -205,9 +212,7 @@
[remove* (-poly (a b)
(cl-> [((-lst a) (-lst a)) (-lst a)]
[((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))]
[call-with-values (-poly (a b) (-> (-> a) (-> a b) b))]
(error
(make-Function (list
(make-arr null (Un))
@ -246,7 +251,6 @@
(- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N)))
(max (->* (list N) N N))
(min (->* (list N) N N))
[values (make-Poly '(a) (-> (-v a) (-v a)))]
[vector-ref
(make-Poly (list 'a) ((make-Vector (-v a)) N . -> . (-v a)))]
[build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (make-Vector a)))]
@ -467,7 +471,7 @@
[(-Bytes N) -Bytes]
[(-Bytes N N) -Bytes])]
[bytes-length (-> -Bytes N)]
[open-input-file (-> -Pathlike -Input-Port)]
[open-input-file (->key -Pathlike #:mode (Un (-val 'binary) (-val 'text)) #f -Input-Port)]
[close-input-port (-> -Input-Port -Void)]
[close-output-port (-> -Output-Port -Void)]
[read-line (cl->
@ -553,8 +557,11 @@
[syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a))
(-> (-Syntax Univ) Univ Univ)))]
[values* (-polydots (a) (null (a a) . ->... . (make-ValuesDots null a 'a)))]
[call-with-values* (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b))]
[values (-polydots (a) (null (a a) . ->... . (make-ValuesDots null a 'a)))]
[call-with-values (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b))]
[eof (-val eof)]
[read-accept-reader (-Param B B)]
)
(begin-for-syntax

5
collects/typed-scheme/private/base-types.ss
View File

@ -1,9 +1,10 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require (for-syntax
scheme/base
"init-envs.ss"
(except-in "type-rep.ss" make-arr)
(env init-envs)
(except-in (rep type-rep) make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"))

7
collects/typed-scheme/private/extra-procs.ss
View File

@ -1,5 +1,5 @@
#lang scheme/base
(provide assert call-with-values* values*)
(provide assert call-with-values* values* foo)
(define (assert v)
(unless v
@ -15,4 +15,7 @@
(car as) (map car bss))))
(define call-with-values* call-with-values)
(define values* values)
(define values* values)
(define (foo x #:bar [bar #f])
bar)

13
collects/typed-scheme/private/mutated-vars.ss
View File

@ -14,12 +14,11 @@
;; syntax -> void
(define (fmv/list lstx)
(for-each find-mutated-vars (syntax->list lstx)))
;(printf "called with ~a~n" (syntax->datum form))
;(when (and (pair? (syntax->datum form))) (printf "called with ~a~n" (syntax->datum form)))
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal require/typed-internal)
;; what we care about: set!
[(set! v e)
(begin
;(printf "mutated var found: ~a~n" (syntax-e #'v))
(module-identifier-mapping-put! table #'v #t))]
[(define-values (var ...) expr)
(find-mutated-vars #'expr)]
@ -28,15 +27,13 @@
[(begin0 . rest) (fmv/list #'rest)]
[(#%plain-lambda _ . rest) (fmv/list #'rest)]
[(case-lambda (_ . rest) ...) (for-each fmv/list (syntax->list #'(rest ...)))]
[(if e1 e2) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e2))]
[(if e1 e2 e3) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e1) (find-mutated-vars #'e3))]
[(with-continuation-mark e1 e2 e3) (begin (find-mutated-vars #'e1)
(find-mutated-vars #'e1)
(find-mutated-vars #'e3))]
[(if . es) (fmv/list #'es)]
[(with-continuation-mark . es) (fmv/list #'es)]
[(let-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
(fmv/list #'b))]
[(letrec-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
(fmv/list #'b))]
(fmv/list #'b))]
[(#%expression e) (find-mutated-vars #'e)]
;; all the other forms don't have any expression subforms (like #%top)
[_ (void)]))

13
collects/typed-scheme/private/parse-type.ss
View File

@ -2,16 +2,15 @@
(provide parse-type parse-type/id)
(require (except-in "type-rep.ss" make-arr)
(require (except-in "../utils/utils.ss" extend))
(require (except-in (rep type-rep) make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"tc-utils.ss"
(utils tc-utils)
"union.ss"
syntax/stx
(except-in "type-environments.ss")
"type-name-env.ss"
"type-alias-env.ss"
"type-utils.ss"
(env type-environments type-name-env type-alias-env)
"type-utils.ss"
scheme/match)
(define enable-mu-parsing (make-parameter #t))
@ -213,7 +212,7 @@
;(printf "found a type name ~a~n" #'id)
(make-Name #'id)]
[else
(tc-error/delayed "unbound type ~a" (syntax-e #'id))
(tc-error/delayed "unbound type name ~a" (syntax-e #'id))
Univ])]
[(All . rest) (eq? (syntax-e #'All) 'All) (tc-error "All: bad syntax")]

10
collects/typed-scheme/private/prims.ss
View File

@ -22,20 +22,20 @@ This file defines two sorts of primitives. All of them are provided into any mod
(provide (all-defined-out)
(rename-out [define-typed-struct define-struct:]))
(require (except-in "../utils/utils.ss" extend))
(require (for-syntax
scheme/base
"type-rep.ss"
(rep type-rep)
mzlib/match
"parse-type.ss"
syntax/struct
syntax/stx
"utils.ss"
"tc-utils.ss"
"type-name-env.ss"
(utils utils tc-utils)
(env type-name-env)
"type-contract.ss"))
(require "require-contract.ss"
"internal-forms.ss"
(typecheck internal-forms)
(except-in mzlib/contract ->)
(only-in mzlib/contract [-> c->])
mzlib/struct

5
collects/typed-scheme/private/remove-intersect.ss
View File

@ -1,7 +1,8 @@
#lang scheme/base
(require "type-rep.ss" "union.ss" "subtype.ss"
"type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss"
(require (except-in "../utils/utils.ss" extend))
(require (rep type-rep)
(private union subtype resolve-type type-effect-convenience type-utils)
mzlib/plt-match mzlib/trace)
(provide (rename-out [*remove remove]) overlap)

3
collects/typed-scheme/private/resolve-type.ss
View File

@ -1,6 +1,7 @@
#lang scheme/base
(require "../utils/utils.ss")
(require "type-rep.ss" "type-name-env.ss" "tc-utils.ss"
(require (rep type-rep) (env type-name-env) (utils tc-utils)
"type-utils.ss"
mzlib/plt-match
mzlib/trace)

27
collects/typed-scheme/private/subtype.ss
View File

@ -1,12 +1,13 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (except-in "type-rep.ss" sub-eff) "type-utils.ss"
"tc-utils.ss"
"effect-rep.ss"
(require (except-in (rep type-rep effect-rep) sub-eff)
(utils tc-utils)
"type-utils.ss"
"type-comparison.ss"
"resolve-type.ss"
"type-name-env.ss"
(only-in "infer-dummy.ss" unify)
(env type-name-env)
(only-in (infer infer-dummy) unify)
mzlib/plt-match
mzlib/trace)
@ -100,10 +101,13 @@
(match (list s t)
;; top for functions is above everything
[(list _ (top-arr:)) A0]
[(list (arr: s1 s2 #f #f thn-eff els-eff) (arr: t1 t2 #f #f thn-eff els-eff))
(let ([A1 (subtypes* A0 t1 s1)])
[(list (arr: s1 s2 #f #f (list (cons kw s-kw-ty) ...) thn-eff els-eff)
(arr: t1 t2 #f #f (list (cons kw t-kw-ty) ...) thn-eff els-eff))
(let* ([A1 (subtypes* A0 t1 s1)]
[A2 (subtypes* A1 t-kw-ty s-kw-ty)])
(subtype* A1 s2 t2))]
[(list (arr: s1 s2 s3 #f thn-eff els-eff) (arr: t1 t2 t3 #f thn-eff* els-eff*))
[(list (arr: s1 s2 s3 #f (list (cons kw s-kw-ty) ...) thn-eff els-eff)
(arr: t1 t2 t3 #f (list (cons kw t-kw-ty) ...) thn-eff* els-eff*))
(unless
(or (and (null? thn-eff*) (null? els-eff*))
(and (effects-equal? thn-eff thn-eff*)
@ -115,10 +119,11 @@
(andmap sub-eff els-eff els-eff*)))
(fail! s t))
;; either the effects have to be the same, or the supertype can't have effects
(let ([A (subtypes*/varargs A0 t1 s1 s3)])
(let* ([A2 (subtypes*/varargs A0 t1 s1 s3)]
[A3 (subtypes* A2 t-kw-ty s-kw-ty)])
(if (not t3)
(subtype* A s2 t2)
(let ([A1 (subtype* A t3 s3)])
(subtype* A3 s2 t2)
(let ([A1 (subtype* A3 t3 s3)])
(subtype* A1 s2 t2))))]
[else
(fail! s t)])))

8
collects/typed-scheme/private/type-annotation.ss
View File

@ -1,7 +1,11 @@
#lang scheme/base
(require "type-rep.ss" "parse-type.ss" "tc-utils.ss" "subtype.ss" "utils.ss"
"type-env.ss" "type-effect-convenience.ss" "resolve-type.ss" "union.ss"
(require (except-in "../utils/utils.ss" extend))
(require (rep type-rep)
(utils tc-utils)
(env type-env)
"parse-type.ss" "subtype.ss"
"type-effect-convenience.ss" "resolve-type.ss" "union.ss"
scheme/match mzlib/trace)
(provide type-annotation
get-type

33
collects/typed-scheme/private/type-effect-convenience.ss
View File

@ -1,14 +1,16 @@
#lang scheme/base
(require "type-rep.ss"
"effect-rep.ss"
(require "../utils/utils.ss")
(require (rep type-rep effect-rep)
(utils tc-utils)
scheme/match
"type-comparison.ss"
"type-effect-printer.ss"
"union.ss"
"subtype.ss"
"type-utils.ss"
"tc-utils.ss"
scheme/promise
(for-syntax macro-debugger/stxclass/stxclass)
(for-syntax scheme/base))
(provide (all-defined-out))
@ -33,7 +35,7 @@
[(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
[(True-Effect:) eff]
[(False-Effect:) eff]
[_ (error 'internal-tc-error "can't add var to effect ~a" eff)]))
[_ (int-err "can't add var ~a to effect ~a" v eff)]))
(define-syntax (-> stx)
(syntax-case* stx (:) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
@ -78,11 +80,26 @@
[(Function: as) as]))
(make-Function (map car (map funty-arities args))))
(define-syntax (->key stx)
(syntax-parse stx
[(_ ty:expr ... ((k:keyword kty:expr opt:boolean)) ...* rng)
#'(make-Function
(list
(make-arr* (list ty ...)
rng
#f
#f
(list (make-Keyword 'k kty opt) ...)
null
null)))]))
(define make-arr*
(case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
[(dom rng rest) (make-arr dom rng rest #f (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest #f eff1 eff2)]
[(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest eff1 eff2)]))
(case-lambda [(dom rng) (make-arr dom rng #f #f null (list) (list))]
[(dom rng rest) (make-arr dom rng rest #f null (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest #f null eff1 eff2)]
[(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest null eff1 eff2)]
[(dom rng rest drest kws eff1 eff2)
(make-arr dom rng rest drest (sort #:key Keyword-kw kws keyword<?) eff1 eff2)]))
(define (make-arr-dots dom rng dty dbound)
(make-arr* dom rng #f (cons dty dbound) null null))

16
collects/typed-scheme/private/type-effect-printer.ss
View File

@ -1,5 +1,9 @@
#lang scheme/base
(require "type-rep.ss" "effect-rep.ss" "rep-utils.ss" "tc-utils.ss" "planet-requires.ss" scheme/match)
(require "../utils/utils.ss")
(require (rep type-rep effect-rep rep-utils)
(utils planet-requires tc-utils)
scheme/match)
;; do we attempt to find instantiations of polymorphic types to print?
;; FIXME - currently broken
@ -46,9 +50,15 @@
(match a
[(top-arr:)
(fp "Procedure")]
[(arr: dom rng rest drest thn-eff els-eff)
[(arr: dom rng rest drest kws thn-eff els-eff)
(fp "(")
(for-each (lambda (t) (fp "~a " t)) dom)
(for ([kw kws])
(match kw
[(Keyword: k t req?)
(if req?
(fp "~a ~a " k t)
(fp "[~a ~a] " k t))]))
(when rest
(fp "~a* " rest))
(when drest
@ -102,7 +112,7 @@
(lambda (e) (fp " ") (print-arr e))
b)
(fp ")")]))]
[(arr: _ _ _ _ _ _) (print-arr c)]
[(arr: _ _ _ _ _ _ _) (print-arr c)]
[(Vector: e) (fp "(Vectorof ~a)" e)]
[(Box: e) (fp "(Box ~a)" e)]
[(Union: elems) (fp "~a" (cons 'U elems))]

24
collects/typed-scheme/private/type-utils.ss
View File

@ -1,10 +1,10 @@
#lang scheme/base
(require "type-rep.ss"
"effect-rep.ss"
"tc-utils.ss"
"rep-utils.ss"
(only-in "free-variance.ss" combine-frees)
(require "../utils/utils.ss")
(require (rep type-rep effect-rep rep-utils)
(utils tc-utils)
(only-in (rep free-variance) combine-frees)
mzlib/plt-match
scheme/list
mzlib/trace
@ -37,7 +37,7 @@
(if (hash-ref (free-vars* target) name #f)
(type-case sb target
[#:F name* (if (eq? name* name) image target)]
[#:arr dom rng rest drest thn-eff els-eff
[#:arr dom rng rest drest kws thn-eff els-eff
(begin
(when (and (pair? drest)
(eq? name (cdr drest))
@ -47,6 +47,8 @@
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(for/list ([kw kws])
(cons (car kw) (sb (cdr kw))))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff)))]
[#:ValuesDots types dty dbound
@ -70,7 +72,7 @@
(let ([expanded (sb dty)])
(map (lambda (img) (substitute img name expanded)) images))))
(make-ValuesDots (map sb types) (sb dty) dbound))]
[#:arr dom rng rest drest thn-eff els-eff
[#:arr dom rng rest drest kws thn-eff els-eff
(if (and (pair? drest)
(eq? name (cdr drest)))
(make-arr (append
@ -81,12 +83,16 @@
(sb rng)
rimage
#f
(for/list ([kw kws])
(cons (car kw) (sb (cdr kw))))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff))
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(for/list ([kw kws])
(cons (car kw) (sb (cdr kw))))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff)))])
target))
@ -105,13 +111,15 @@
(if (eq? name* name)
image
target)]
[#:arr dom rng rest drest thn-eff els-eff
[#:arr dom rng rest drest kws thn-eff els-eff
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest
(cons (sb (car drest))
(if (eq? name (cdr drest)) image-bound (cdr drest))))
(for/list ([kw kws])
(cons (car kw) (sb (cdr kw))))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff))])
target))

8
collects/typed-scheme/private/union.ss
View File

@ -1,7 +1,11 @@
#lang scheme/base
(require "type-rep.ss" "subtype.ss" "tc-utils.ss"
"type-effect-printer.ss" "rep-utils.ss"
(require "../utils/utils.ss")
(require (rep type-rep rep-utils)
(utils tc-utils)
"subtype.ss"
"type-effect-printer.ss"
"type-comparison.ss"
scheme/match mzlib/trace)

39
collects/typed-scheme/rep/effect-rep.ss Normal file
View File

@ -0,0 +1,39 @@
#lang scheme/base
(require mzlib/plt-match)
(require mzlib/etc)
(require "rep-utils.ss" "free-variance.ss")
(de True-Effect () [#:frees #f] [#:fold-rhs #:base])
(de False-Effect () [#:frees #f] [#:fold-rhs #:base])
;; v is an identifier
(de Var-True-Effect (v) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
;; v is an identifier
(de Var-False-Effect (v) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
;; t is a Type
;; v is an identifier
(de Restrict-Effect (t v) [#:intern (list t (hash-id v))] [#:frees (free-vars* t) (free-idxs* t)]
[#:fold-rhs (*Restrict-Effect (type-rec-id t) v)])
;; t is a Type
;; v is an identifier
(de Remove-Effect (t v)
[#:intern (list t (hash-id v))]
[#:frees (free-vars* t) (free-idxs* t)]
[#:fold-rhs (*Remove-Effect (type-rec-id t) v)])
;; t is a Type
(de Latent-Restrict-Effect (t))
;; t is a Type
(de Latent-Remove-Effect (t))
(de Latent-Var-True-Effect () [#:frees #f] [#:fold-rhs #:base])
(de Latent-Var-False-Effect () [#:frees #f] [#:fold-rhs #:base])
;; could also have latent true/false effects, but seems pointless

104
collects/typed-scheme/rep/free-variance.ss Normal file
View File

@ -0,0 +1,104 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (for-syntax scheme/base)
(utils tc-utils)
mzlib/etc)
;; this file contains support for calculating the free variables/indexes of types
;; actual computation is done in rep-utils.ss and type-rep.ss
(define-values (Covariant Contravariant Invariant Constant Dotted)
(let ()
(define-struct Variance () #:inspector #f)
(define-struct (Covariant Variance) () #:inspector #f)
(define-struct (Contravariant Variance) () #:inspector #f)
(define-struct (Invariant Variance) () #:inspector #f)
(define-struct (Constant Variance) () #:inspector #f)
;; not really a variance, but is disjoint with the others
(define-struct (Dotted Variance) () #:inspector #f)
(values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted))))
(provide Covariant Contravariant Invariant Constant Dotted)
;; hashtables for keeping track of free variables and indexes
(define index-table (make-weak-hasheq))
;; maps Type to List[Cons[Number,Variance]]
(define var-table (make-weak-hasheq))
;; maps Type to List[Cons[Symbol,Variance]]
(define (free-idxs* t) (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" (syntax-e t)))))
(define (free-vars* t) (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" (syntax-e t)))))
(define empty-hash-table (make-immutable-hasheq null))
(provide free-vars* free-idxs* empty-hash-table make-invariant)
;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
;; (listof frees) -> frees
(define (combine-frees freess)
(define ht (make-hasheq))
(define (combine-var v w)
(cond
[(eq? v w) v]
[(eq? v Dotted) w]
[(eq? w Dotted) v]
[(eq? v Constant) w]
[(eq? w Constant) v]
[else Invariant]))
(for* ([old-ht (in-list freess)]
[(sym var) (in-hash old-ht)])
(let* ([sym-var (hash-ref ht sym (lambda () #f))])
(if sym-var
(hash-set! ht sym (combine-var var sym-var))
(hash-set! ht sym var))))
ht)
;; given a set of free variables, change bound to ...
;; (if bound wasn't free, this will add it as Dotted
;; appropriately so that things that expect to see
;; it as "free" will -- fixes the case where the
;; dotted pre-type base doesn't use the bound).
(define (fix-bound vs bound)
(define vs* (hash-map* (lambda (k v) v) vs))
(hash-set! vs* bound Dotted)
vs*)
;; frees -> frees
(define (flip-variances vs)
(hash-map*
(lambda (k v)
(evcase
v
[Covariant Contravariant]
[Contravariant Covariant]
[v v]))
vs))
(define (make-invariant vs)
(hash-map*
(lambda (k v) Invariant)
vs))
(define (hash-map* f ht)
(define new-ht (make-hasheq))
(for ([(k v) (in-hash ht)])
(hash-set! new-ht k (f k v)))
new-ht)
(define (without-below n frees)
(define new-ht (make-hasheq))
(for ([(k v) (in-hash frees)])
(when (>= k n) (hash-set! new-ht k v)))
new-ht)
(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table
fix-bound)
(define-syntax (unless-in-table stx)
(syntax-case stx ()
[(_ table val . body)
(quasisyntax/loc stx
(hash-ref table val #,(syntax/loc #'body (lambda () . body))))]))

50
collects/typed-scheme/rep/interning.ss Normal file
View File

@ -0,0 +1,50 @@
#lang scheme/base
(require syntax/boundmap)
(provide defintern hash-id)
(define-syntax defintern
(syntax-rules ()
[(_ name+args make-name key)
(defintern name+args (lambda () (make-hash #;'weak)) make-name key)]
[(_ (*name arg ...) make-ht make-name key-expr)
(define *name
(let ([table (make-ht)])
(lambda (arg ...)
#;(all-count!)
(let ([key key-expr])
(hash-ref table key
(lambda ()
(let ([new (make-name (count!) arg ...)])
(hash-set! table key new)
new)))))))]))
(define (make-count!)
(let ([state 0])
(lambda () (begin0 state (set! state (add1 state)))))
#;
(let ([ch (make-channel)])
(thread (lambda () (let loop ([n 0]) (channel-put ch n) (loop (add1 n)))))
(lambda () (channel-get ch))))
(provide #;count! #;all-count! union-count!)
(define count! (make-count!))
(define union-count! (make-count!))
(define all-count! (make-count!))
(define id-count! (make-count!))
(define identifier-table (make-module-identifier-mapping))
(define (hash-id id)
(module-identifier-mapping-get
identifier-table
id
(lambda () (let ([c (id-count!)])
(module-identifier-mapping-put! identifier-table id c)
c))))

162
collects/typed-scheme/rep/rep-utils.ss Normal file
View File

@ -0,0 +1,162 @@
#lang scheme/base
(require "../utils/utils.ss")
(require mzlib/struct
mzlib/plt-match
syntax/boundmap
(utils planet-requires)
"free-variance.ss"
"interning.ss"
mzlib/etc
(for-syntax
scheme/base
syntax/struct
syntax/stx
(utils utils)))
(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq)
;; hash table for defining folds over types
(define-values-for-syntax (type-name-ht effect-name-ht)
(values (make-hasheq) (make-hasheq)))
(provide (for-syntax type-name-ht effect-name-ht))
;; all types are Type?
(define-struct/printer Type (seq) (lambda (a b c) ((unbox print-type*) a b c)))
(define-struct/printer Effect (seq) (lambda (a b c) ((unbox print-effect*) a b c)))
;; type/effect definition macro
(define-for-syntax type-rec-id #'type-rec-id)
(define-for-syntax effect-rec-id #'effect-rec-id)
(define-for-syntax fold-target #'fold-target)
(provide (for-syntax type-rec-id effect-rec-id fold-target))
(define-syntaxes (dt de)
(let ()
(define (parse-opts opts stx)
(let loop ([provide? #t] [intern? #f] [frees #t] [fold-rhs #f] [opts opts])
(cond
[(null? opts) (values provide? intern? frees fold-rhs)]
[(eq? '#:no-provide (syntax-e (stx-car opts)))
(loop #f intern? frees fold-rhs (cdr opts))]
[(eq? '#:no-frees (syntax-e (stx-car opts)))
(loop #f intern? #f fold-rhs (cdr opts))]
[(not (and (stx-pair? opts) (stx-pair? (stx-car opts))))
(raise-syntax-error #f "bad options" stx)]
[(eq? '#:intern (syntax-e (stx-car (car opts))))
(loop provide? (stx-car (stx-cdr (car opts))) frees fold-rhs (cdr opts))]
[(eq? '#:frees (syntax-e (stx-car (car opts))))
(loop provide? intern? (stx-cdr (car opts)) fold-rhs (cdr opts))]
[(eq? '#:fold-rhs (syntax-e (stx-car (car opts))))
(loop provide? intern? frees (stx-cdr (car opts)) (cdr opts))]
[else (raise-syntax-error #f "bad options" stx)])))
(define (mk par ht-stx)
(lambda (stx)
(syntax-case stx ()
[(dform nm flds . opts)
(let*-values ([(provide? intern? frees fold-rhs) (parse-opts (syntax->list #'opts) #'opts)]
[(kw) (string->keyword (symbol->string (syntax-e #'nm)))])
(with-syntax*
([ex (id #'nm #'nm ":")]
[kw-stx kw]
[parent par]
[(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)]
[(flds* ...) #'flds]
[*maker (id #'nm "*" #'nm)]
[**maker (id #'nm "**" #'nm)]
[ht-stx ht-stx]
[bfs-fold-rhs (cond [(and fold-rhs (eq? (syntax-e (stx-car fold-rhs)) '#:base))
#`(lambda (tr er) #,fold-target)]
[(and fold-rhs (stx-pair? fold-rhs))
(with-syntax ([fr (stx-car fold-rhs)])
#'(lambda (tr er)
#'fr))]
[fold-rhs (raise-syntax-error fold-rhs "something went wrong")]
[else #'(lambda (type-rec-id effect-rec-id) #`(*maker (#,type-rec-id flds*) ...))])]
[provides (if provide?
#`(begin
(provide ex pred acc ...)
(provide (rename-out [*maker maker])))
#'(begin))]
[intern (cond
[(syntax? intern?)
#`(defintern (**maker . flds) maker #,intern?)]
[(null? (syntax-e #'flds))
#'(defintern (**maker . flds) maker #f)]
[(stx-null? (stx-cdr #'flds)) #'(defintern (**maker . flds) maker . flds)]
[else #'(defintern (**maker . flds) maker (list . flds))])]
[frees (cond
[(not frees) #'(begin)]
;; we know that this has no free vars
[(and (pair? frees) (syntax? (car frees)) (not (syntax-e (car frees))))
(syntax/loc stx
(define (*maker . flds)
(define v (**maker . flds))
#;(printf "~a entered in #f case~n" '*maker)
(unless-in-table
var-table v
(hash-set! var-table v empty-hash-table)
(hash-set! index-table v empty-hash-table))
v))]
;; we provided an expression each for calculating the free vars and free idxs
;; this should really be 2 expressions, one for each kind
[(and (pair? frees) (pair? (cdr frees)))
(quasisyntax/loc
stx
(define (*maker . flds)
(define v (**maker . flds))
#;(printf "~a entered in expr case ~n~a~n~a ~n" '*maker '#,(car frees) '#,(cadr frees))
#,
(quasisyntax/loc (car frees)
(unless-in-table
var-table v
(hash-set! var-table v #,(car frees))
(hash-set! index-table v #,(cadr frees))))
#;(printf "~a exited in expr case~n" '*maker)
v))]
[else
(let
([combiner
(lambda (f flds)
(syntax-case flds ()
[() #'empty-hash-table]
[(e) #`(#,f e)]
[(e ...) #`(combine-frees (list (#,f e) ...))]))])
(quasisyntax/loc stx
(define (*maker . flds)
(define v (**maker . flds))
#;(printf "~a entered in default case~n" '*maker)
(unless-in-table
var-table v
(define fvs #,(combiner #'free-vars* #'flds))
(define fis #,(combiner #'free-idxs* #'flds))
(hash-set! var-table v fvs)
(hash-set! index-table v fis))
v)))])])
#`(begin
(define-struct (nm parent) flds #:inspector #f)
(define-match-expander ex
(lambda (s)
(...
(syntax-case s ()
[(__ . fs)
(with-syntax ([flds** (syntax/loc s (_ . fs))])
(quasisyntax/loc s (struct nm flds**)))]))))
(begin-for-syntax
(hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx)))
intern
provides
frees)))])))
(values (mk #'Type #'type-name-ht) (mk #'Effect #'effect-name-ht))))

577
collects/typed-scheme/rep/type-rep.ss Normal file
View File

@ -0,0 +1,577 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (utils planet-requires tc-utils)
"rep-utils.ss" "effect-rep.ss" "free-variance.ss"
mzlib/trace scheme/match
(for-syntax scheme/base))
(define name-table (make-weak-hasheq))
;; Name = Symbol
;; Type is defined in rep-utils.ss
;; t must be a Type
(dt Scope (t))
;; i is an nat
(dt B (i)
[#:frees empty-hash-table (make-immutable-hasheq (list (cons i Covariant)))]
[#:fold-rhs #:base])
;; n is a Name
(dt F (n) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base])
;; id is an Identifier
(dt Name (id) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
;; rator is a type
;; rands is a list of types
;; stx is the syntax of the pair of parens
(dt App (rator rands stx)
[#:intern (list rator rands)]
[#:frees (combine-frees (map free-vars* (cons rator rands)))
(combine-frees (map free-idxs* (cons rator rands)))]
[#:fold-rhs (*App (type-rec-id rator)
(map type-rec-id rands)
stx)])
;; left and right are Types
(dt Pair (left right))
;; elem is a Type
(dt Vector (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])
;; elem is a Type
(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])
;; name is a Symbol (not a Name)
(dt Base (name) [#:frees #f] [#:fold-rhs #:base])
;; body is a Scope
(dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))]
[#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))])
;; n is how many variables are bound here
;; body is a Scope
(dt Poly (n body) #:no-provide
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
[#:fold-rhs (let ([body* (remove-scopes n body)])
(*Poly n (add-scopes n (type-rec-id body*))))])
;; n is how many variables are bound here
;; there are n-1 'normal' vars and 1 ... var
;; body is a Scope
(dt PolyDots (n body) #:no-provide
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
[#:fold-rhs (let ([body* (remove-scopes n body)])
(*PolyDots n (add-scopes n (type-rec-id body*))))])
;; pred : identifier
;; cert : syntax certifier
(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base])
;; name : symbol
;; parent : Struct
;; flds : Listof[Type]
;; proc : Function Type
;; poly? : is this a polymorphic type?
;; pred-id : identifier for the predicate of the struct
;; cert : syntax certifier for pred-id
(dt Struct (name parent flds proc poly? pred-id cert)
[#:intern (list name parent flds proc)]
[#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds)))
(combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) flds)))]
[#:fold-rhs (*Struct name
(and parent (type-rec-id parent))
(map type-rec-id flds)
(and proc (type-rec-id proc))
poly?
pred-id
cert)])
;; kw : keyword?
;; ty : Type
;; required? : Boolean
(dt Keyword (kw ty required?)
[#:frees (free-vars* ty)
(free-idxs* ty)]
[#:fold-rhs (*Keyword kw (type-rec-id ty))])
;; dom : Listof[Type]
;; rng : Type
;; rest : Option[Type]
;; drest : Option[Cons[Type,Name or nat]]
;; kws : Listof[Keyword]
;; rest and drest NOT both true
;; thn-eff : Effect
;; els-eff : Effect
;; arr is NOT a Type
(dt arr (dom rng rest drest kws thn-eff els-eff)
[#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null)
(map Keyword-ty kws)
dom)))
(match drest
[(cons t (? symbol? bnd))
(list (fix-bound (flip-variances (free-vars* t)) bnd))]
[(cons t bnd) (list (flip-variances (free-vars* t)))]
[_ null])
(list (free-vars* rng))
(map make-invariant
(map free-vars* (append thn-eff els-eff)))))
(combine-frees (append (map flip-variances (map free-idxs* (append (if rest (list rest) null)
(map Keyword-ty kws)
dom)))
(match drest
[(cons t (? number? bnd))
(list (fix-bound (flip-variances (free-idxs* t)) bnd))]
[(cons t bnd) (list (flip-variances (free-idxs* t)))]
[_ null])
(list (free-idxs* rng))
(map make-invariant
(map free-idxs* (append thn-eff els-eff)))))]
[#:fold-rhs (*arr (map type-rec-id dom)
(type-rec-id rng)
(and rest (type-rec-id rest))
(and drest (cons (type-rec-id (car drest)) (cdr drest)))
(for/list ([kw kws])
(cons (Keyword-kw kw) (type-rec-id (Keyword-ty kw)) (Keyword-require? kw)))
(map effect-rec-id thn-eff)
(map effect-rec-id els-eff))])
;; top-arr is the supertype of all function types
(dt top-arr ()
[#:frees #f] [#:fold-rhs #:base])
;; arities : Listof[arr]
(dt Function (arities) [#:frees (combine-frees (map free-vars* arities))
(combine-frees (map free-idxs* arities))]
[#:fold-rhs (*Function (map type-rec-id arities))])
;; v : Scheme Value
(dt Value (v) [#:frees #f] [#:fold-rhs #:base])
;; elems : Listof[Type]
(dt Union (elems) [#:frees (combine-frees (map free-vars* elems))
(combine-frees (map free-idxs* elems))]
[#:fold-rhs ((unbox union-maker) (map type-rec-id elems))])
(dt Univ () [#:frees #f] [#:fold-rhs #:base])
;; types : Listof[Type]
(dt Values (types)
#:no-provide
[#:frees (combine-frees (map free-vars* types))
(combine-frees (map free-idxs* types))]
[#:fold-rhs (*Values (map type-rec-id types))])
(dt ValuesDots (types dty dbound)
[#:frees (combine-frees (map free-vars* (cons dty types)))
(combine-frees (map free-idxs* (cons dty types)))]
[#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)])
;; in : Type
;; out : Type
(dt Param (in out))
;; key : Type
;; value : Type
(dt Hashtable (key value))
;; t : Type
(dt Syntax (t))
;; pos-flds : (Listof Type)
;; name-flds : (Listof (Tuple Symbol Type Boolean))
;; methods : (Listof (Tuple Symbol Function))
(dt Class (pos-flds name-flds methods)
[#:frees (combine-frees
(map free-vars* (append pos-flds
(map cadr name-flds)
(map cadr methods))))
(combine-frees
(map free-idxs* (append pos-flds
(map cadr name-flds)
(map cadr methods))))]
[#:fold-rhs (match (list pos-flds name-flds methods)
[(list
pos-tys
(list (list init-names init-tys) ___)
(list (list mname mty) ___))
(*Class
(map type-rec-id pos-tys)
(map list
init-names
(map type-rec-id init-tys))
(map list mname (map type-rec-id mty)))])])
;; cls : Class
(dt Instance (cls))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Ugly hack - should use units
(define union-maker (box #f))
(define (set-union-maker! v) (set-box! union-maker v))
(provide set-union-maker!)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; remove-dups: List[Type] -> List[Type]
;; removes duplicate types from a SORTED list
(define (remove-dups types)
(cond [(null? types) types]
[(null? (cdr types)) types]
[(type-equal? (car types) (cadr types)) (remove-dups (cdr types))]
[else (cons (car types) (remove-dups (cdr types)))]))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; type/effect fold
(define-syntaxes (type-case effect-case)
(let ()
(define (mk ht)
(lambda (stx)
(let ([ht (hash-copy ht)])
(define (mk-matcher kw)
(datum->syntax stx (string->symbol (string-append (keyword->string kw) ":"))))
(define (add-clause cl)
(syntax-case cl ()
[(kw #:matcher mtch pats ... expr)
(hash-set! ht (syntax-e #'kw) (list #'mtch
(syntax/loc cl (pats ...))
(lambda (tr er) #'expr)
cl))]
[(kw pats ... expr)
(hash-set! ht (syntax-e #'kw) (list (mk-matcher (syntax-e #'kw))
(syntax/loc cl (pats ...))
(lambda (tr er) #'expr)
cl))]))
(define rid #'type-rec-id)
(define erid #'effect-rec-id)
(define (gen-clause k v)
(define match-ex (car v))
(define pats (cadr v))
(define body-f (caddr v))
(define src (cadddr v))
(define pat (quasisyntax/loc src (#,match-ex . #,pats)))
(define cl (quasisyntax/loc src (#,pat #,(body-f rid erid))))
cl)
(syntax-case stx ()
[(tc rec-id ty clauses ...)
(syntax-case #'(clauses ...) ()
[([kw pats ... es] ...) #t]
[_ #f])
(syntax/loc stx (tc rec-id (lambda (e) (sub-eff rec-id e)) ty clauses ...))]
[(tc rec-id e-rec-id ty clauses ...)
(begin
(map add-clause (syntax->list #'(clauses ...)))
(with-syntax ([old-rec-id type-rec-id])
#`(let ([#,rid rec-id]
[#,erid e-rec-id]
[#,fold-target ty])
;; then generate the fold
#,(quasisyntax/loc stx
(match #,fold-target
#,@(hash-map ht gen-clause))))))]))))
(values (mk type-name-ht) (mk effect-name-ht))))
(provide type-case effect-case)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; sub-eff : (Type -> Type) Eff -> Eff
(define (sub-eff sb eff)
(effect-case sb eff))
(define (add-scopes n t)
(if (zero? n) t
(add-scopes (sub1 n) (*Scope t))))
(define (remove-scopes n sc)
(if (zero? n)
sc
(match sc
[(Scope: sc*) (remove-scopes (sub1 n) sc*)]
[_ (int-err "Tried to remove too many scopes: ~a" sc)])))
;; abstract-many : Names Type -> Scope^n
;; where n is the length of names
(define (abstract-many names ty)
(define (nameTo name count type)
(let loop ([outer 0] [ty type])
(define (sb t) (loop outer t))
(type-case
sb ty
[#:F name* (if (eq? name name*) (*B (+ count outer)) ty)]
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions
[#:arr dom rng rest drest kws thn-eff els-eff
(*arr (map sb dom)
(sb rng)
(if rest (sb rest) #f)
(if drest
(cons (sb (car drest))
(if (eq? (cdr drest) name) (+ count outer) (cdr drest)))
#f)
(for/list ([kw kws])
(cons (car kw) (sb (cdr kw))))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff))]
[#:ValuesDots tys dty dbound
(*ValuesDots (map sb tys)
(sb dty)
(if (eq? dbound name) (+ count outer) dbound))]
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
[#:PolyDots n body*
(let ([body (remove-scopes n body*)])
(*PolyDots n (*Scope (loop (+ n outer) body))))]
[#:Poly n body*
(let ([body (remove-scopes n body*)])
(*Poly n (*Scope (loop (+ n outer) body))))])))
(let ([n (length names)])
(let loop ([ty ty] [names names] [count (sub1 n)])
(if (zero? count)
(add-scopes n (nameTo (car names) 0 ty))
(loop (nameTo (car names) count ty)
(cdr names)
(sub1 count))))))
;; instantiate-many : List[Type] Scope^n -> Type
;; where n is the length of types
;; all of the types MUST be Fs
(define (instantiate-many images sc)
(define (replace image count type)
(let loop ([outer 0] [ty type])
(define (sb t) (loop outer t))
(type-case
sb ty
[#:B idx (if (= (+ count outer) idx)
image
ty)]
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions
[#:arr dom rng rest drest kws thn-eff els-eff
(*arr (map sb dom)
(sb rng)
(if rest (sb rest) #f)
(if drest
(cons (sb (car drest))
(if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
#f)
(for/list ([kw kws])
(cons (car kw) (sb (cdr kw))))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff))]
[#:ValuesDots tys dty dbound
(*ValuesDots (map sb tys)
(sb dty)
(if (eqv? dbound (+ count outer)) (F-n image) dbound))]
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
[#:PolyDots n body*
(let ([body (remove-scopes n body*)])
(*PolyDots n (*Scope (loop (+ n outer) body))))]
[#:Poly n body*
(let ([body (remove-scopes n body*)])
(*Poly n (*Scope (loop (+ n outer) body))))])))
(let ([n (length images)])
(let loop ([ty (remove-scopes n sc)] [images images] [count (sub1 n)])
(if (zero? count)
(replace (car images) 0 ty)
(loop (replace (car images) count ty)
(cdr images)
(sub1 count))))))
(define (abstract name ty)
(abstract-many (list name) ty))
(define (instantiate type sc)
(instantiate-many (list type) sc))
#;(trace instantiate-many abstract-many)
;; the 'smart' constructor
(define (Mu* name body)
(let ([v (*Mu (abstract name body))])
(hash-set! name-table v name)
v))
;; the 'smart' destructor
(define (Mu-body* name t)
(match t
[(Mu: scope)
(instantiate (*F name) scope)]))
;; the 'smart' constructor
(define (Poly* names body)
(if (null? names) body
(let ([v (*Poly (length names) (abstract-many names body))])
(hash-set! name-table v names)
v)))
;; the 'smart' destructor
(define (Poly-body* names t)
(match t
[(Poly: n scope)
(unless (= (length names) n)
(int-err "Wrong number of names: expected ~a got ~a" n (length names)))
(instantiate-many (map *F names) scope)]))
;; the 'smart' constructor
(define (PolyDots* names body)
(if (null? names) body
(let ([v (*PolyDots (length names) (abstract-many names body))])
(hash-set! name-table v names)
v)))
;; the 'smart' destructor
(define (PolyDots-body* names t)
(match t
[(PolyDots: n scope)
(unless (= (length names) n)
(int-err "Wrong number of names: expected ~a got ~a" n (length names)))
(instantiate-many (map *F names) scope)]))
(print-struct #t)
(define-match-expander Mu-unsafe:
(lambda (stx)
(syntax-case stx ()
[(_ bp) #'(? Mu? (app (lambda (t) (Scope-t (Mu-body t))) bp))])))
(define-match-expander Poly-unsafe:
(lambda (stx)
(syntax-case stx ()
[(_ n bp) #'(? Poly? (app (lambda (t) (list (Poly-n t) (Poly-body t))) (list n bp)))])))
(define-match-expander PolyDots-unsafe:
(lambda (stx)
(syntax-case stx ()
[(_ n bp) #'(? PolyDots? (app (lambda (t) (list (PolyDots-n t) (PolyDots-body t))) (list n bp)))])))
(define-match-expander Mu:*
(lambda (stx)
(syntax-case stx ()
[(_ np bp)
#'(? Mu?
(app (lambda (t) (let ([sym (gensym)])
(list sym (Mu-body* sym t))))
(list np bp)))])))
(define-match-expander Mu-name:
(lambda (stx)
(syntax-case stx ()
[(_ np bp)
#'(? Mu?
(app (lambda (t) (let ([sym (hash-ref name-table t (lambda _ (gensym)))])
(list sym (Mu-body* sym t))))
(list np bp)))])))
;; This match expander wraps the smart constructor
;; names are generated with gensym
(define-match-expander Poly:*
(lambda (stx)
(syntax-case stx ()
[(_ nps bp)
#'(? Poly?
(app (lambda (t)
(let* ([n (Poly-n t)]
[syms (build-list n (lambda _ (gensym)))])
(list syms (Poly-body* syms t))))
(list nps bp)))])))
;; This match expander uses the names from the hashtable
(define-match-expander Poly-names:
(lambda (stx)
(syntax-case stx ()
[(_ nps bp)
#'(? Poly?
(app (lambda (t)
(let* ([n (Poly-n t)]
[syms (hash-ref name-table t (lambda _ (build-list n (lambda _ (gensym)))))])
(list syms (Poly-body* syms t))))
(list nps bp)))])))
;; This match expander wraps the smart constructor
;; names are generated with gensym
(define-match-expander PolyDots:*
(lambda (stx)
(syntax-case stx ()
[(_ nps bp)
#'(? PolyDots?
(app (lambda (t)
(let* ([n (PolyDots-n t)]
[syms (build-list n (lambda _ (gensym)))])
(list syms (PolyDots-body* syms t))))
(list nps bp)))])))
;; This match expander uses the names from the hashtable
(define-match-expander PolyDots-names:
(lambda (stx)
(syntax-case stx ()
[(_ nps bp)
#'(? PolyDots?
(app (lambda (t)
(let* ([n (PolyDots-n t)]
[syms (hash-ref name-table t (lambda _ (build-list n (lambda _ (gensym)))))])
(list syms (PolyDots-body* syms t))))
(list nps bp)))])))
;; type equality
(define type-equal? eq?)
;; inequality - good
(define (type<? s t)
(< (Type-seq s) (Type-seq t)))
(define (type-compare s t)
(cond [(eq? s t) 0]
[(type<? s t) 1]
[else -1]))
(define (Values* l)
(if (and (pair? l) (null? (cdr l)))
(car l)
(*Values l)))
;(trace subst subst-all)
(provide
Mu-name: Poly-names:
PolyDots-names:
Type-seq Effect-seq
Mu-unsafe: Poly-unsafe:
PolyDots-unsafe:
Mu? Poly? PolyDots?
arr
Type? Effect?
Poly-n
PolyDots-n
free-vars*
type-equal? type-compare type<?
remove-dups
sub-eff
Values: Values? Values-types
(rename-out [Values* make-Values])
(rename-out [Mu:* Mu:]
[Poly:* Poly:]
[PolyDots:* PolyDots:]
[Mu* make-Mu]
[Poly* make-Poly]
[PolyDots* make-PolyDots]
[Mu-body* Mu-body]
[Poly-body* Poly-body]
[PolyDots-body* PolyDots-body]))
;(trace unfold)

88
collects/typed-scheme/typecheck/check-subforms-unit.ss Normal file
View File

@ -0,0 +1,88 @@
#lang scheme/unit
(require (except-in "../utils/utils.ss" extend))
(require syntax/kerncase
scheme/match
"signatures.ss"
(private type-utils type-effect-convenience union subtype)
(utils tc-utils)
(rep type-rep))
(import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-expr^)
(export check-subforms^)
;; find the subexpressions that need to be typechecked in an ignored form
;; syntax -> void
(define (check-subforms/with-handlers form)
(define handler-tys '())
(define body-ty #f)
(define (get-result-ty t)
(match t
[(Function: (list (arr: _ rngs #f _ '() _ _) ...)) (apply Un rngs)]
[_ (tc-error "Internal error in get-result-ty: not a function type: ~n~a" t)]))
(let loop ([form form])
(parameterize ([current-orig-stx form])
(kernel-syntax-case* form #f (#%app)
[stx
;; if this needs to be checked
(syntax-property form 'typechecker:with-type)
;; the form should be already ascribed the relevant type
(void
(tc-expr form))]
[stx
;; this is a hander function
(syntax-property form 'typechecker:exn-handler)
(let ([t (tc-expr/t form)])
(unless (subtype t (-> (Un) Univ))
(tc-error "Exception handler must be a single-argument function, got ~n~a"))
(set! handler-tys (cons (get-result-ty t) handler-tys)))]
[stx
;; this is the body of the with-handlers
(syntax-property form 'typechecker:exn-body)
(let ([t (tc-expr/t form)])
(set! body-ty t))]
[(a . b)
(begin
(loop #'a)
(loop #'b))]
[_ (void)])))
(ret (apply Un body-ty handler-tys)))
(define (check-subforms/with-handlers/check form expected)
(let loop ([form form])
(parameterize ([current-orig-stx form])
(kernel-syntax-case* form #f ()
[stx
;; if this needs to be checked
(syntax-property form 'typechecker:with-type)
;; the form should be already ascribed the relevant type
(tc-expr form)]
[stx
;; this is a hander function
(syntax-property form 'typechecker:exn-handler)
(tc-expr/check form (-> (Un) expected))]
[stx
;; this is the body of the with-handlers
(syntax-property form 'typechecker:exn-body)
(tc-expr/check form expected)]
[(a . b)
(begin
(loop #'a)
(loop #'b))]
[_ (void)])))
(ret expected))
;; typecheck the expansion of a with-handlers form
;; syntax -> type
(define (check-subforms/ignore form)
(let loop ([form form])
(kernel-syntax-case* form #f ()
[stx
;; if this needs to be checked
(syntax-property form 'typechecker:with-type)
;; the form should be already ascribed the relevant type
(tc-expr form)]
[(a . b)
(loop #'a)
(loop #'b)]
[_ (void)])))

11
collects/typed-scheme/typecheck/def-binding.ss Normal file
View File

@ -0,0 +1,11 @@
#lang scheme/base
(require scheme/contract)
(define-struct binding (name) #:transparent)
(define-struct (def-binding binding) (ty) #:transparent)
(define-struct (def-stx-binding binding) () #:transparent)
(provide/contract (struct binding ([name identifier?]))
(struct (def-binding binding) ([name identifier?] [ty any/c]))
(struct (def-stx-binding binding) ([name identifier?])))

14
collects/typed-scheme/typecheck/internal-forms.ss Normal file
View File

@ -0,0 +1,14 @@
#lang scheme/base
(require (for-syntax scheme/base))
(define-syntax-rule (internal-forms nms ...)
(begin
(provide nms ...)
(define-syntax (nms stx) (raise-syntax-error 'typecheck "Internal typechecker form used out of context" stx)) ...))
(internal-forms require/typed-internal define-type-alias-internal
define-typed-struct-internal
define-typed-struct/exec-internal
assert-predicate-internal
:-internal)

90
collects/typed-scheme/typecheck/provide-handling.ss Normal file
View File

@ -0,0 +1,90 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require (only-in srfi/1/list s:member)
syntax/kerncase
mzlib/trace
(private type-contract)
(rep type-rep)
(utils tc-utils)
"def-binding.ss")
(require (for-template scheme/base
scheme/contract))
(provide remove-provides provide? generate-prov)
(define (provide? form)
(kernel-syntax-case form #f
[(#%provide . rest) form]
[_ #f]))
(define (remove-provides forms)
(filter (lambda (e) (not (provide? e))) (syntax->list forms)))
(define ((generate-prov stx-defs val-defs) form)
(define (mem? i vd)
(cond [(s:member i vd (lambda (i j) (free-identifier=? i (binding-name j)))) => car]
[else #f]))
(define (lookup-id i vd)
(def-binding-ty (mem? i vd)))
(define (mk internal-id external-id)
(cond
[(mem? internal-id val-defs)
=>
(lambda (b)
(with-syntax ([id internal-id]
[out-id external-id])
(cond [(type->contract (def-binding-ty b) (lambda () #f))
=>
(lambda (cnt)
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
#`(begin
(define/contract cnt-id #,cnt id)
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(make-rename-transformer #'cnt-id)))
(#%provide (rename export-id out-id)))))]
[else
(with-syntax ([(export-id) (generate-temporaries #'(id))])
#`(begin
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
(provide (rename-out [export-id out-id]))))])))]
[(mem? internal-id stx-defs)
=>
(lambda (b)
(with-syntax ([id internal-id]
[out-id external-id])
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
#`(begin
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(lambda (stx)
(tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
(provide (rename-out [export-id out-id]))))))]
[(eq? (syntax-e internal-id) (syntax-e external-id))
#`(provide #,internal-id)]
[else #`(provide (rename-out [#,internal-id #,external-id]))]))
(kernel-syntax-case form #f
[(#%provide form ...)
(map
(lambda (f)
(parameterize ([current-orig-stx f])
(syntax-case* f (struct rename all-defined protect all-defined-except all-from all-from-except)
(lambda (a b) (eq? (syntax-e a) (syntax-e b)))
[id
(identifier? #'id)
(mk #'id #'id)]
[(rename in out)
(mk #'in #'out)]
[(protect . _)
(tc-error "provide: protect not supported by Typed Scheme")]
[_ (int-err "unknown provide form")])))
(syntax->list #'(form ...)))]
[_ (int-err "non-provide form! ~a" (syntax->datum form))]))

28
collects/typed-scheme/typecheck/signatures.ss Normal file
View File

@ -0,0 +1,28 @@
#lang scheme/base
(require scheme/unit)
(provide (all-defined-out))
(define-signature typechecker^
(type-check tc-toplevel-form))
(define-signature tc-expr^
(tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t))
(define-signature check-subforms^
(check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check))
(define-signature tc-if^
(tc/if-onearm tc/if-twoarm tc/if-onearm/check tc/if-twoarm/check))
(define-signature tc-lambda^
(tc/lambda tc/lambda/check tc/rec-lambda/check))
(define-signature tc-app^
(tc/app tc/app/check tc/funapp))
(define-signature tc-let^
(tc/let-values tc/letrec-values tc/let-values/check tc/letrec-values/check))
(define-signature tc-dots^
(tc/dots))

734
collects/typed-scheme/typecheck/tc-app-unit.ss Normal file
View File

@ -0,0 +1,734 @@
#lang scheme/unit
(require (only-in "../utils/utils.ss" debug in-syntax printf/log in-pairs rep utils private env [infer r:infer]))
(require "signatures.ss"
(rep type-rep effect-rep)
(utils tc-utils)
(private subtype type-utils union type-effect-convenience type-effect-printer resolve-type
type-annotation)
(r:infer infer)
(env type-environments)
(only-in srfi/1 alist-delete)
(only-in scheme/private/class-internal make-object do-make-object)
mzlib/trace mzlib/pretty syntax/kerncase scheme/match
(for-syntax scheme/base)
(for-template
"internal-forms.ss" scheme/base
(only-in scheme/private/class-internal make-object do-make-object)))
(require (r:infer constraint-structs))
(import tc-expr^ tc-lambda^ tc-dots^)
(export tc-app^)
;; comparators that inform the type system
(define (comparator? i)
(or (free-identifier=? i #'eq?)
(free-identifier=? i #'equal?)
(free-identifier=? i #'eqv?)
(free-identifier=? i #'=)
(free-identifier=? i #'string=?)))
;; typecheck eq? applications
;; identifier identifier expression expression expression
;; identifier expr expr expr expr -> tc-result
(define (tc/eq comparator v1 v2)
(define (e? i) (free-identifier=? i comparator))
(define (do id val)
(define-syntax alt (syntax-rules () [(_ nm pred ...)
(and (e? #'nm) (or (pred val) ...))]))
(if (or (alt symbol=? symbol?)
(alt string=? string?)
(alt = number?)
(alt eq? boolean? keyword? symbol?)
(alt eqv? boolean? keyword? symbol? number?)
(alt equal? (lambda (x) #t)))
(values (list (make-Restrict-Effect (-val val) id))
(list (make-Remove-Effect (-val val) id)))
(values (list) (list))))
(match (list (tc-expr v1) (tc-expr v2))
[(list (tc-result: id-t (list (Var-True-Effect: id1)) (list (Var-False-Effect: id2))) (tc-result: (Value: val)))
(do id1 val)]
[(list (tc-result: (Value: val)) (tc-result: id-t (list (Var-True-Effect: id1)) (list (Var-False-Effect: id2))))
(do id1 val)]
[_ (values (list) (list))]))
;; typecheck an application:
;; arg-types: the types of the actual parameters
;; arg-effs: the effects of the arguments
;; dom-types: the types of the function's fixed arguments
;; rest-type: the type of the functions's rest parameter, or #f
;; latent-eff: the latent effect of the function
;; arg-stxs: the syntax for each actual parameter, for error reporting
;; [Type] [Type] Maybe[Type] [Syntax] -> (values Listof[Effect] Listof[Effect])
(define (tc-args arg-types arg-thn-effs arg-els-effs dom-types rest-type latent-thn-eff latent-els-eff arg-stxs)
(define (var-true-effect-v e) (match e
[(Var-True-Effect: v) v]))
(define (var-false-effect-v e) (match e
[(Var-False-Effect: v) v]))
;; special case for predicates:
(if (and (not (null? latent-thn-eff))
(not (null? latent-els-eff))
(not rest-type)
;(printf "got to =~n")
(= (length arg-types) (length dom-types) 1)
;(printf "got to var preds~n")
(= (length (car arg-thn-effs)) (length (car arg-els-effs)) 1)
(Var-True-Effect? (caar arg-thn-effs)) ;; thn-effs is a list for each arg
(Var-False-Effect? (caar arg-els-effs)) ;; same with els-effs
(free-identifier=? (var-true-effect-v (caar arg-thn-effs))
(var-false-effect-v (caar arg-els-effs)))
(subtype (car arg-types) (car dom-types)))
;; then this was a predicate application, so we construct the appropriate type effect
(values (map (add-var (var-true-effect-v (caar arg-thn-effs))) latent-thn-eff)
(map (add-var (var-true-effect-v (caar arg-thn-effs))) latent-els-eff))
;; otherwise, we just ignore the effects.
(let loop ([args arg-types] [doms dom-types] [stxs arg-stxs] [arg-count 1])
(cond
[(and (null? args) (null? doms)) (values null null)] ;; here, we just return the empty effect
[(null? args)
(tc-error/delayed
"Insufficient arguments to function application, expected ~a, got ~a"
(length dom-types) (length arg-types))
(values null null)]
[(and (null? doms) rest-type)
(if (subtype (car args) rest-type)
(loop (cdr args) doms (cdr stxs) (add1 arg-count))
(begin
(tc-error/delayed #:stx (car stxs)
"Rest argument had wrong type, expected: ~a and got: ~a"
rest-type (car args))
(values null null)))]
[(null? doms)
(tc-error/delayed "Too many arguments to function, expected ~a, got ~a" (length dom-types) (length arg-types))
(values null null)]
[(subtype (car args) (car doms))
(loop (cdr args) (cdr doms) (cdr stxs) (add1 arg-count))]
[else
(tc-error/delayed
#:stx (car stxs)
"Wrong function argument type, expected ~a, got ~a for argument ~a"
(car doms) (car args) arg-count)
(loop (cdr args) (cdr doms) (cdr stxs) (add1 arg-count))]))))
;(trace tc-args)
(define (stringify-domain dom rst drst)
(let ([doms-string (if (null? dom) "" (string-append (stringify dom) " "))])
(cond [drst
(format "~a~a ... ~a" doms-string (car drst) (cdr drst))]
[rst
(format "~a~a *" doms-string rst)]
[else (stringify dom)])))
(define (domain-mismatches ty doms rests drests arg-tys tail-ty tail-bound)
(cond
[(null? doms)
(int-err "How could doms be null: ~a ~a" ty)]
[(= 1 (length doms))
(format "Domain: ~a~nArguments: ~a~n"
(stringify-domain (car doms) (car rests) (car drests))
(stringify-domain arg-tys (if (not tail-bound) tail-ty #f) (if tail-bound (cons tail-ty tail-bound) #f)))]
[else
(format "Domains: ~a~nArguments: ~a~n"
(stringify (map stringify-domain doms rests drests) "~n\t")
(stringify-domain arg-tys (if (not tail-bound) tail-ty #f) (if tail-bound (cons tail-ty tail-bound) #f)))]))
(define (do-apply-log subst fun arg)
(match* (fun arg)
[('star 'list) (printf/log "Polymorphic apply called with uniform rest arg, list argument\n")]
[('star 'dots) (printf/log "Polymorphic apply called with uniform rest arg, dotted argument\n")]
[('dots 'dots) (printf/log "Polymorphic apply called with non-uniform rest arg, dotted argument\n")])
(log-result subst))
(define (tc/apply f args)
(define f-ty (tc-expr f))
;; produces the first n-1 elements of the list, and the last element
(define (split l)
(let loop ([l l] [acc '()])
(if (null? (cdr l))
(values (reverse acc) (car l))
(loop (cdr l) (cons (car l) acc)))))
(define-values (fixed-args tail) (split (syntax->list args)))
(match f-ty
[(tc-result: (Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ...)))
(when (null? doms)
(tc-error/expr #:return (ret (Un))
"empty case-lambda given as argument to apply"))
(let ([arg-tys (map tc-expr/t fixed-args)])
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
(cond [(null? doms*)
(let-values ([(tail-ty tail-bound)
(with-handlers ([exn:fail? (lambda _ (values (tc-expr/t tail) #f))])
(tc/dots tail))])
(tc-error/expr #:return (ret (Un))
(string-append
"Bad arguments to function in apply:~n"
(domain-mismatches f-ty doms rests drests arg-tys tail-ty tail-bound))))]
[(and (car rests*)
(let-values ([(tail-ty tail-bound)
(with-handlers ([exn:fail? (lambda _ (values #f #f))])
(tc/dots tail))])
(and tail-ty
(subtype (apply -lst* arg-tys #:tail (make-Listof tail-ty))
(apply -lst* (car doms*) #:tail (make-Listof (car rests*)))))))
(printf/log "Non-poly apply, ... arg\n")
(ret (car rngs*))]
[(and (car rests*)
(let ([tail-ty (with-handlers ([exn:fail? (lambda _ #f)])
(tc-expr/t tail))])
(and tail-ty
(subtype (apply -lst* arg-tys #:tail tail-ty)
(apply -lst* (car doms*) #:tail (make-Listof (car rests*)))))))
(printf/log (if (memq (syntax->datum f) '(+ - * / max min))
"Simple arithmetic non-poly apply\n"
"Simple non-poly apply\n"))
(ret (car rngs*))]
[(and (car drests*)
(let-values ([(tail-ty tail-bound)
(with-handlers ([exn:fail? (lambda _ (values #f #f))])
(tc/dots tail))])
(and tail-ty
(eq? (cdr (car drests*)) tail-bound)
(subtypes arg-tys (car doms*))
(subtype tail-ty (car (car drests*))))))
(printf/log "Non-poly apply, ... arg\n")
(ret (car rngs*))]
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ..1))))
(let*-values ([(arg-tys) (map tc-expr/t fixed-args)]
[(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))])
(tc/dots tail))])
#;(for-each (lambda (x) (unless (not (Poly? x))
(tc-error "Polymorphic argument of type ~a to polymorphic function in apply not allowed" x)))
(cons tail-ty arg-tys))
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
(cond [(null? doms*)
(match f-ty
[(tc-result: (Poly-names: _ (Function: (list (arr: doms rngs rests drests '() _ _) ..1))))
(tc-error/expr #:return (ret (Un))
(string-append
"Bad arguments to polymorphic function in apply:~n"
(domain-mismatches f-ty doms rests drests arg-tys tail-ty tail-bound)))])]
;; the actual work, when we have a * function and a list final argument
[(and (car rests*)
(not tail-bound)
(<= (length (car doms*))
(length arg-tys))
(infer/vararg vars
(cons tail-ty arg-tys)
(cons (make-Listof (car rests*))
(car doms*))
(car rests*)
(car rngs*)
(fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg
[(and (car rests*)
tail-bound
(<= (length (car doms*))
(length arg-tys))
(infer/vararg vars
(cons (make-Listof tail-ty) arg-tys)
(cons (make-Listof (car rests*))
(car doms*))
(car rests*)
(car rngs*)
(fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg
[(and (car drests*)
tail-bound
(eq? tail-bound (cdr (car drests*)))
(= (length (car doms*))
(length arg-tys))
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (Poly: vars (Function: '())))
(tc-error/expr #:return (ret (Un))
"Function has no cases")]
[(tc-result: (PolyDots: (and vars (list fixed-vars ... dotted-var))
(Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ..1))))
(let*-values ([(arg-tys) (map tc-expr/t fixed-args)]
[(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))])
(tc/dots tail))])
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
(cond [(null? doms*)
(match f-ty
[(tc-result: (PolyDots-names: _ (Function: (list (arr: doms rngs rests drests '() _ _) ..1))))
(tc-error/expr #:return (ret (Un))
(string-append
"Bad arguments to polymorphic function in apply:~n"
(domain-mismatches f-ty doms rests drests arg-tys tail-ty tail-bound)))])]
;; the actual work, when we have a * function and a list final argument
[(and (car rests*)
(not tail-bound)
(<= (length (car doms*))
(length arg-tys))
(infer/vararg vars
(cons tail-ty arg-tys)
(cons (make-Listof (car rests*))
(car doms*))
(car rests*)
(car rngs*)
(fv (car rngs*))))
=> (lambda (substitution)
(do-apply-log substitution 'star 'list)
(ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg
[(and (car rests*)
tail-bound
(<= (length (car doms*))
(length arg-tys))
(infer/vararg vars
(cons (make-Listof tail-ty) arg-tys)
(cons (make-Listof (car rests*))
(car doms*))
(car rests*)
(car rngs*)
(fv (car rngs*))))
=> (lambda (substitution)
(do-apply-log substitution 'star 'dots)
(ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, same bound on ...
[(and (car drests*)
tail-bound
(eq? tail-bound (cdr (car drests*)))
(= (length (car doms*))
(length arg-tys))
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))
=> (lambda (substitution)
(do-apply-log substitution 'dots 'dots)
(ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, different bound on ...
[(and (car drests*)
tail-bound
(not (eq? tail-bound (cdr (car drests*))))
(= (length (car doms*))
(length arg-tys))
(parameterize ([current-tvars (extend-env (list tail-bound (cdr (car drests*)))
(list (make-DottedBoth (make-F tail-bound))
(make-DottedBoth (make-F (cdr (car drests*)))))
(current-tvars))])
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))))
=> (lambda (substitution)
(define drest-bound (cdr (car drests*)))
(do-apply-log substitution 'dots 'dots)
(ret (substitute-dotted (cadr (assq drest-bound substitution))
tail-bound
drest-bound
(subst-all (alist-delete drest-bound substitution eq?)
(car rngs*)))))]
;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (PolyDots: vars (Function: '())))
(tc-error/expr #:return (ret (Un))
"Function has no cases")]
[(tc-result: f-ty) (tc-error/expr #:return (ret (Un))
"Type of argument to apply is not a function type: ~n~a" f-ty)]))
(define (log-result subst)
(define (dmap-length d)
(match d
[(struct dcon (fixed rest)) (length fixed)]
[(struct dcon-exact (fixed rest)) (length fixed)]))
(define (dmap-rest? d)
(match d
[(struct dcon (fixed rest)) rest]
[(struct dcon-exact (fixed rest)) rest]))
(if (list? subst)
(for ([s subst])
(match s
[(list v (list imgs ...) starred)
(printf/log "Instantiated ... variable ~a with ~a types\n" v (length imgs))]
[_ (void)]))
(for* ([(cmap dmap) (in-pairs (cset-maps subst))]
[(k v) (dmap-map dmap)])
(printf/log "Instantiated ... variable ~a with ~a types~a\n" k (dmap-length v)
(if (dmap-rest? v)
" and a starred type"
"")))))
(define-syntax (handle-clauses stx)
(syntax-case stx ()
[(_ (lsts ... rngs) f-stx pred infer t argtypes expected)
(with-syntax ([(vars ... rng) (generate-temporaries #'(lsts ... rngs))])
(syntax/loc stx
(or (for/or ([vars lsts] ... [rng rngs]
#:when (pred vars ... rng))
(let ([substitution (infer vars ... rng)])
(and substitution
(log-result substitution)
(or expected
(ret (subst-all substitution rng))))))
(poly-fail t argtypes #:name (and (identifier? f-stx) f-stx)))))]))
(define (poly-fail t argtypes #:name [name #f])
(match t
[(or (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '() _ _) ...)))
(PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '() _ _) ...))))
(let ([fcn-string (if name
(format "function ~a (over ~~a)" (syntax->datum name))
"function over ~a")])
(if (and (andmap null? msg-doms)
(null? argtypes))
(tc-error/expr #:return (ret (Un))
(string-append
"Could not infer types for applying polymorphic "
fcn-string
"\n")
(stringify msg-vars))
(tc-error/expr #:return (ret (Un))
(string-append
"Polymorphic " fcn-string " could not be applied to arguments:~n"
(domain-mismatches t msg-doms msg-rests msg-drests argtypes #f #f))
(stringify msg-vars))))]))
(define (tc/funapp f-stx args-stx ftype0 argtys expected)
(match-let* ([(list (tc-result: argtypes arg-thn-effs arg-els-effs) ...) argtys])
(let outer-loop ([ftype ftype0]
[argtypes argtypes]
[arg-thn-effs arg-thn-effs]
[arg-els-effs arg-els-effs]
[args args-stx])
(match ftype
;; procedural structs
[(tc-result: (and sty (Struct: _ _ _ (? Type? proc-ty) _ _ _)) thn-eff els-eff)
(outer-loop (ret proc-ty thn-eff els-eff)
(cons (tc-result-t ftype0) argtypes)
(cons (list) arg-thn-effs)
(cons (list) arg-els-effs)
#`(#,(syntax/loc f-stx dummy) #,@args))]
;; mu types, etc
[(tc-result: (? needs-resolving? t) thn-eff els-eff)
(outer-loop (ret (resolve-once t) thn-eff els-eff) argtypes arg-thn-effs arg-els-effs args)]
;; parameters
[(tc-result: (Param: in out))
(match argtypes
[(list) (ret out)]
[(list t)
(if (subtype t in)
(ret -Void)
(tc-error/expr #:return (ret (Un))
"Wrong argument to parameter - expected ~a and got ~a" in t))]
[_ (tc-error/expr #:return (ret (Un))
"Wrong number of arguments to parameter - expected 0 or 1, got ~a"
(length argtypes))])]
;; single clause functions
;; FIXME - error on non-optional keywords
[(tc-result: (and t (Function: (list (arr: dom rng rest #f _ latent-thn-effs latent-els-effs))))
thn-eff els-eff)
(let-values ([(thn-eff els-eff)
(tc-args argtypes arg-thn-effs arg-els-effs dom rest
latent-thn-effs latent-els-effs
(syntax->list args))])
(ret rng thn-eff els-eff))]
;; non-polymorphic case-lambda functions
[(tc-result: (and t (Function: (list (arr: doms rngs rests (and drests #f) '() latent-thn-effs latent-els-effs) ..1)))
thn-eff els-eff)
(let loop ([doms* doms] [rngs rngs] [rests* rests])
(cond [(null? doms*)
(tc-error/expr
#:return (ret (Un))
(string-append "No function domains matched in function application:\n"
(domain-mismatches t doms rests drests argtypes #f #f)))]
[(subtypes/varargs argtypes (car doms*) (car rests*))
(when (car rests*)
(printf/log "Simple varargs function application (~a)\n" (syntax->datum f-stx)))
(ret (car rngs))]
[else (loop (cdr doms*) (cdr rngs) (cdr rests*))]))]
;; simple polymorphic functions, no rest arguments
[(tc-result: (and t
(or (Poly: vars
(Function: (list (arr: doms rngs (and rests #f) (and drests #f) '() thn-effs els-effs) ...)))
(PolyDots: (list vars ... _)
(Function: (list (arr: doms rngs (and rests #f) (and drests #f) '() thn-effs els-effs) ...))))))
(handle-clauses (doms rngs) f-stx
(lambda (dom _) (= (length dom) (length argtypes)))
(lambda (dom rng) (infer (fv/list (cons rng dom)) argtypes dom rng (fv rng) expected))
t argtypes expected)]
;; polymorphic varargs
[(tc-result: (and t
(or (Poly: vars (Function: (list (arr: doms rngs rests (and drests #f) '() thn-effs els-effs) ...)))
;; we want to infer the dotted-var here as well, and we don't use these separately
;; so we can just use "vars" instead of (list fixed-vars ... dotted-var)
(PolyDots: vars (Function: (list (arr: doms rngs rests (and drests #f) '() thn-effs els-effs) ...))))))
(printf/log "Polymorphic varargs function application (~a)\n" (syntax->datum f-stx))
(handle-clauses (doms rests rngs) f-stx
(lambda (dom rest rng) (<= (length dom) (length argtypes)))
(lambda (dom rest rng) (infer/vararg vars argtypes dom rest rng (fv rng) expected))
t argtypes expected)]
;; polymorphic ... type
[(tc-result: (and t (PolyDots:
(and vars (list fixed-vars ... dotted-var))
(Function: (list (arr: doms rngs (and #f rests) (cons dtys dbounds) '() thn-effs els-effs) ...)))))
(printf/log "Polymorphic ... function application (~a)\n" (syntax->datum f-stx))
(handle-clauses (doms dtys dbounds rngs) f-stx
(lambda (dom dty dbound rng) (and (<= (length dom) (length argtypes))
(eq? dotted-var dbound)))
(lambda (dom dty dbound rng) (infer/dots fixed-vars dotted-var argtypes dom dty rng (fv rng) expected))
t argtypes expected)]
;; Union of function types works if we can apply all of them
[(tc-result: (Union: (list (and fs (Function: _)) ...)) e1 e2)
(match-let ([(list (tc-result: ts) ...) (map (lambda (f) (outer-loop
(ret f e1 e2) argtypes arg-thn-effs arg-els-effs args)) fs)])
(ret (apply Un ts)))]
[(tc-result: f-ty _ _) (tc-error/expr #:return (ret (Un))
"Cannot apply expression of type ~a, since it is not a function type" f-ty)]))))
;(trace tc/funapp)
(define (tc/app form) (tc/app/internal form #f))
(define (tc/app/check form expected)
(define t (tc/app/internal form expected))
(check-below t expected)
(ret expected))
;; expr id -> type or #f
;; if there is a binding in stx of the form:
;; (let ([x (reverse name)]) e)
;; where x has a type annotation, return that annotation, otherwise #f
(define (find-annotation stx name)
(define (find s) (find-annotation s name))
(define (match? b)
(kernel-syntax-case* b #f (reverse)
[[(v) (#%plain-app reverse n)]
(free-identifier=? name #'n)
(begin ;(printf "found annotation: ~a ~a~n~a~n" (syntax-e name) (syntax-e #'v) (type-annotation #'v))
(type-annotation #'v))]
[_ #f]))
(kernel-syntax-case*
stx #f (reverse letrec-syntaxes+values)
[(let-values (binding ...) body)
(cond [(ormap match? (syntax->list #'(binding ...)))]
[else (find #'body)])]
[(#%plain-app e ...) (ormap find (syntax->list #'(e ...)))]
[(if e1 e2 e3) (ormap find (syntax->list #'(e1 e2 e3)))]
[(letrec-values ([(v ...) e] ...) b)
(ormap find (syntax->list #'(e ... b)))]
[(letrec-syntaxes+values _ ([(v ...) e] ...) b)
(ormap find (syntax->list #'(e ... b)))]
[(begin . es)
(ormap find (syntax->list #'es))]
[(#%plain-lambda (v ...) e)
(find #'e)]
[_ #f]))
(define (check-do-make-object cl pos-args names named-args)
(let* ([names (map syntax-e (syntax->list names))]
[name-assoc (map list names (syntax->list named-args))])
(let loop ([t (tc-expr cl)])
(match t
[(tc-result: (? Mu? t)) (loop (ret (unfold t)))]
[(tc-result: (and c (Class: pos-tys (list (and tnflds (list tnames _ _)) ...) _)))
(unless (= (length pos-tys)
(length (syntax->list pos-args)))
(tc-error/delayed "expected ~a positional arguments, but got ~a"
(length pos-tys) (length (syntax->list pos-args))))
;; use for, since they might be different lengths in error case
(for ([pa (in-syntax pos-args)]
[pt (in-list pos-tys)])
(tc-expr/check pa pt))
(for ([n names]
#:when (not (memq n tnames)))
(tc-error/delayed
"unknown named argument ~a for class~nlegal named arguments are ~a"
n (stringify tnames)))
(for-each (match-lambda
[(list tname tfty opt?)
(let ([s (cond [(assq tname name-assoc) => cadr]
[(not opt?)
(tc-error/delayed "value not provided for named init arg ~a" tname)
#f]
[else #f])])
(if s
;; this argument was present
(tc-expr/check s tfty)
;; this argument wasn't provided, and was optional
#f))])
tnflds)
(ret (make-Instance c))]
[(tc-result: t)
(tc-error/expr #:return (ret (Un)) "expected a class value for object creation, got: ~a" t)]))))
(define (tc-keywords form arities kws kw-args pos-args expected)
(match arities
[(list (arr: dom rng rest #f ktys _ _))
;; assumes that everything is in sorted order
(let loop ([actual-kws kws]
[actuals (map tc-expr/t (syntax->list kw-args))]
[formals ktys])
(match* (actual-kws formals)
[('() '())
(void)]
[(_ '())
(tc-error/expr #:return (ret (Un))
"Unexpected keyword argument ~a" (car actual-kws))]
[('() (cons fst rst))
(match fst
[(Keyword: k _ #t)
(tc-error/expr #:return (ret (Un))
"Missing keyword argument ~a" k)]
[_ (loop actual-kws actuals rst)])]
[((cons k kws-rest) (cons (Keyword: k* t req?) form-rest))
(cond [(eq? k k*) ;; we have a match
(unless (subtype (car actuals) t)
(tc-error/delayed
"Wrong function argument type, expected ~a, got ~a for keyword argument ~a"
t (car actuals) k))
(loop kws-rest (cdr actuals) form-rest)]
[req? ;; this keyword argument was required
(tc-error/delayed "Missing keyword argument ~a" k*)
(loop kws-rest (cdr actuals) form-rest)]
[else ;; otherwise, ignore this formal param, and continue
(loop actual-kws actuals form-rest)])]))
(tc/funapp (car (syntax-e form)) kw-args (ret (make-Function arities)) (map tc-expr (syntax->list pos-args)) expected)]
[_ (int-err "case-lambda w/ keywords not supported")]))
(define (type->list t)
(match t
[(Pair: (Value: (? keyword? k)) b) (cons k (type->list b))]
[(Value: '()) null]
[_ (int-err "bad value in type->list: ~a" t)]))
(define (tc/app/internal form expected)
(kernel-syntax-case* form #f
(values apply not list list* call-with-values do-make-object make-object cons
andmap ormap) ;; the special-cased functions
;; special cases for classes
[(#%plain-app make-object cl . args)
(check-do-make-object #'cl #'args #'() #'())]
[(#%plain-app do-make-object cl (#%plain-app list . pos-args) (#%plain-app list (#%plain-app cons 'names named-args) ...))
(check-do-make-object #'cl #'pos-args #'(names ...) #'(named-args ...))]
[(#%plain-app do-make-object . args)
(int-err "bad do-make-object : ~a" (syntax->datum #'args))]
;; call-with-values
[(#%plain-app call-with-values prod con)
(match-let* ([(tc-result: prod-t) (tc-expr #'prod)])
(define (values-ty->list t)
(match t
[(Values: ts) ts]
[_ (list t)]))
(match prod-t
[(Function: (list (arr: (list) vals _ #f '() _ _)))
(tc/funapp #'con #'prod (tc-expr #'con) (map ret (values-ty->list vals)) expected)]
[_ (tc-error/expr #:return (ret (Un))
"First argument to call with values must be a function that can accept no arguments, got: ~a"
prod-t)]))]
;; special cases for `values'
;; special case the single-argument version to preserve the effects
[(#%plain-app values arg) (tc-expr #'arg)]
[(#%plain-app values . args)
(let ([tys (map tc-expr/t (syntax->list #'args))])
(ret (-values tys)))]
;; special case for `list'
[(#%plain-app list . args)
(let ([tys (map tc-expr/t (syntax->list #'args))])
(ret (apply -lst* tys)))]
;; special case for `list*'
[(#%plain-app list* . args)
(match-let* ([(list last tys-r ...) (reverse (map tc-expr/t (syntax->list #'args)))]
[tys (reverse tys-r)])
(ret (foldr make-Pair last tys)))]
;; in eq? cases, call tc/eq
[(#%plain-app eq? v1 v2)
(and (identifier? #'eq?) (comparator? #'eq?))
(begin
;; make sure the whole expression is type correct
(tc/funapp #'eq? #'(v1 v2) (tc-expr #'eq?) (map tc-expr (syntax->list #'(v1 v2))) expected)
;; check thn and els with the eq? info
(let-values ([(thn-eff els-eff) (tc/eq #'eq? #'v1 #'v2)])
(ret B thn-eff els-eff)))]
;; special case for `not'
[(#%plain-app not arg)
(match (tc-expr #'arg)
;; if arg was a predicate application, we swap the effects
[(tc-result: t thn-eff els-eff)
(ret B (map var->type-eff els-eff) (map var->type-eff thn-eff))])]
;; special case for `apply'
[(#%plain-app apply f . args) (tc/apply #'f #'args)]
;; special case for keywords
[(#%plain-app
(#%plain-app kpe kws num fn)
kw-list
(#%plain-app list . kw-arg-list)
. pos-args)
(eq? (syntax-e #'kpe) 'keyword-procedure-extract)
(match (tc-expr #'fn)
[(tc-result: (Function: arities))
(tc-keywords form arities (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected)]
[t (tc-error/expr #:return (ret (Un))
"Cannot apply expression of type ~a, since it is not a function type" t)])]
;; even more special case for match
[(#%plain-app (letrec-values ([(lp) (#%plain-lambda args . body)]) lp*) . actuals)
(and expected (not (andmap type-annotation (syntax->list #'args))) (free-identifier=? #'lp #'lp*))
(let-loop-check form #'lp #'actuals #'args #'body expected)]
;; or/andmap of ... argument
[(#%plain-app or/andmap f arg)
(and
(identifier? #'or/andmap)
(or (free-identifier=? #'or/andmap #'ormap)
(free-identifier=? #'or/andmap #'andmap))
(with-handlers ([exn:fail? (lambda _ #f)])
(tc/dots #'arg)
#t))
(let-values ([(ty bound) (tc/dots #'arg)])
(parameterize ([current-tvars (extend-env (list bound)
(list (make-DottedBoth (make-F bound)))
(current-tvars))])
(match-let* ([ft (tc-expr #'f)]
[(tc-result: t) (tc/funapp #'f #'(arg) ft (list (ret ty)) #f)])
(ret (Un (-val #f) t)))))]
;; default case
[(#%plain-app f args ...)
(tc/funapp #'f #'(args ...) (tc-expr #'f) (map tc-expr (syntax->list #'(args ...))) expected)]))
(define (let-loop-check form lp actuals args body expected)
(kernel-syntax-case* #`(#,args #,body #,actuals) #f (null?)
[((val acc ...)
((if (#%plain-app null? val*) thn els))
(actual actuals ...))
(and (free-identifier=? #'val #'val*)
(ormap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
(syntax->list #'(acc ...))))
(let* ([ts1 (generalize (tc-expr/t #'actual))]
[ann-ts (for/list ([a (in-syntax #'(acc ...))]
[ac (in-syntax #'(actuals ...))])
(or (find-annotation #'(if (#%plain-app null? val*) thn els) a)
(generalize (tc-expr/t ac))))]
[ts (cons ts1 ann-ts)])
;; check that the actual arguments are ok here
(map tc-expr/check (syntax->list #'(actuals ...)) ann-ts)
;; then check that the function typechecks with the inferred types
(tc/rec-lambda/check form args body lp ts expected)
(ret expected))]
;; special case when argument needs inference
[_
(let ([ts (map (compose generalize tc-expr/t) (syntax->list actuals))])
(tc/rec-lambda/check form args body lp ts expected)
(ret expected))]))
(define (matches? stx)
(let loop ([stx stx] [ress null] [acc*s null])
(syntax-case stx (#%plain-app reverse)
[([(res) (#%plain-app reverse acc*)] . more)
(loop #'more (cons #'res ress) (cons #'acc* acc*s))]
[rest
(syntax->list #'rest)
(begin
;(printf "ress: ~a~n" (map syntax-e ress))
(list (reverse ress) (reverse acc*s) #'rest))]
[_ #f])))
;(trace tc/app/internal)

331
collects/typed-scheme/typecheck/tc-expr-unit.ss Normal file
View File

@ -0,0 +1,331 @@
#lang scheme/unit
(require (rename-in "../utils/utils.ss" [private r:private]))
(require syntax/kerncase
scheme/match
"signatures.ss"
(r:private type-utils type-effect-convenience union subtype parse-type type-annotation)
(rep type-rep effect-rep)
(utils tc-utils)
(env lexical-env)
(only-in (env type-environments) lookup current-tvars extend-env)
scheme/private/class-internal
(only-in srfi/1 split-at))
(require (for-template scheme/base scheme/private/class-internal))
(import tc-if^ tc-lambda^ tc-app^ tc-let^ check-subforms^)
(export tc-expr^)
;; return the type of a literal value
;; scheme-value -> type
(define (tc-literal v-stx)
;; find the meet of the types of a list of expressions
;; list[syntax] -> type
(define (types-of-literals es)
(apply Un (map tc-literal es)))
(define v (syntax-e v-stx))
(cond
[(integer? v) -Integer]
[(number? v) N]
[(char? v) -Char]
[(boolean? v) (-val v)]
[(null? v) (-val null)]
[(symbol? v) (-val v)]
[(string? v) -String]
[(keyword? v) (-val v)]
[(bytes? v) -Bytes]
[(list? v) (-Tuple (map tc-literal v))]
[(vector? v) (make-Vector (types-of-literals (vector->list v)))]
[(pregexp? v) -PRegexp]
[(byte-pregexp? v) -Byte-PRegexp]
[(byte-regexp? v) -Byte-Regexp]
[(regexp? v) -Regexp]
[else Univ]))
(define (do-inst stx ty)
(define inst (syntax-property stx 'type-inst))
(define (split-last l)
(let-values ([(all-but last-list) (split-at l (sub1 (length l)))])
(values all-but (car last-list))))
(cond [(not inst) ty]
[(not (or (Poly? ty) (PolyDots? ty)))
(tc-error/expr #:return (ret (Un)) "Cannot instantiate non-polymorphic type ~a" ty)]
[(and (Poly? ty)
(not (= (length (syntax->list inst)) (Poly-n ty))))
(tc-error/expr #:return (ret (Un))
"Wrong number of type arguments to polymorphic type ~a:~nexpected: ~a~ngot: ~a"
ty (Poly-n ty) (length (syntax->list inst)))]
[(and (PolyDots? ty) (not (>= (length (syntax->list inst)) (sub1 (PolyDots-n ty)))))
;; we can provide 0 arguments for the ... var
(tc-error/expr #:return (ret (Un))
"Wrong number of type arguments to polymorphic type ~a:~nexpected at least: ~a~ngot: ~a"
ty (sub1 (PolyDots-n ty)) (length (syntax->list inst)))]
[(PolyDots? ty)
;; In this case, we need to check the last thing. If it's a dotted var, then we need to
;; use instantiate-poly-dotted, otherwise we do the normal thing.
(let-values ([(all-but-last last-stx) (split-last (syntax->list inst))])
(match (syntax-e last-stx)
[(cons last-ty-stx (? identifier? last-id-stx))
(unless (Dotted? (lookup (current-tvars) (syntax-e last-id-stx) (lambda _ #f)))
(tc-error/stx last-id-stx "~a is not a type variable bound with ..." (syntax-e last-id-stx)))
(let* ([last-id (syntax-e last-id-stx)]
[last-ty
(parameterize ([current-tvars (extend-env (list last-id)
(list (make-DottedBoth (make-F last-id)))
(current-tvars))])
(parse-type last-ty-stx))])
(instantiate-poly-dotted ty (map parse-type all-but-last) last-ty last-id))]
[_
(instantiate-poly ty (map parse-type (syntax->list inst)))]))]
[else
(instantiate-poly ty (map parse-type (syntax->list inst)))]))
;; typecheck an identifier
;; the identifier has variable effect
;; tc-id : identifier -> tc-result
(define (tc-id id)
(let* ([ty (lookup-type/lexical id)])
(ret ty (list (make-Var-True-Effect id)) (list (make-Var-False-Effect id)))))
;; typecheck an expression, but throw away the effect
;; tc-expr/t : Expr -> Type
(define (tc-expr/t e) (match (tc-expr e)
[(tc-result: t) t]
[t (int-err "tc-expr returned ~a, not a tc-result, for ~a" t (syntax->datum e))]))
(define (tc-expr/check/t e t)
(match (tc-expr/check e t)
[(tc-result: t) t]))
;; check-below : (/\ (Result Type -> Result)
;; (Type Type -> Type))
(define (check-below tr1 expected)
(match (list tr1 expected)
[(list (tc-result: t1 te1 ee1) t2)
(unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
(ret expected)]
[(list t1 t2)
(unless (subtype t1 t2)
(tc-error/expr"Expected ~a, but got ~a" t2 t1))
expected]))
(define (tc-expr/check form expected)
(parameterize ([current-orig-stx form])
;(printf "form: ~a~n" (syntax-object->datum form))
;; the argument must be syntax
(unless (syntax? form)
(int-err "bad form input to tc-expr: ~a" form))
(let (;; a local version of ret that does the checking
[ret
(lambda args
(define te (apply ret args))
(check-below te expected)
(ret expected))])
(kernel-syntax-case* form #f
(letrec-syntaxes+values find-method/who) ;; letrec-syntaxes+values is not in kernel-syntax-case literals
[stx
(syntax-property form 'typechecker:with-handlers)
(check-subforms/with-handlers/check form expected)]
[stx
(syntax-property form 'typechecker:ignore-some)
(let ([ty (check-subforms/ignore form)])
(unless ty
(int-err "internal error: ignore-some"))
(check-below ty expected))]
;; data
[(quote #f) (ret (-val #f) (list (make-False-Effect)) (list (make-False-Effect)))]
[(quote #t) (ret (-val #t) (list (make-True-Effect)) (list (make-True-Effect)))]
[(quote val) (ret (tc-literal #'val))]
;; syntax
[(quote-syntax datum) (ret Any-Syntax)]
;; mutation!
[(set! id val)
(match-let* ([(tc-result: id-t) (tc-expr #'id)]
[(tc-result: val-t) (tc-expr #'val)])
(unless (subtype val-t id-t)
(tc-error/expr "Mutation only allowed with compatible types:~n~a is not a subtype of ~a" val-t id-t))
(ret -Void))]
;; top-level variable reference - occurs at top level
[(#%top . id) (check-below (tc-id #'id) expected)]
;; weird
[(#%variable-reference . _)
(tc-error/expr #:return (ret expected) "#%variable-reference is not supported by Typed Scheme")]
;; identifiers
[x (identifier? #'x)
(check-below (tc-id #'x) expected)]
;; w-c-m
[(with-continuation-mark e1 e2 e3)
(begin (tc-expr/check #'e1 Univ)
(tc-expr/check #'e2 Univ)
(tc-expr/check #'e3 expected))]
;; application
[(#%plain-app . _) (tc/app/check form expected)]
;; #%expression
[(#%expression e) (tc-expr/check #'e expected)]
;; syntax
;; for now, we ignore the rhs of macros
[(letrec-syntaxes+values stxs vals . body)
(tc-expr/check (syntax/loc form (letrec-values vals . body)) expected)]
;; begin
[(begin e . es) (tc-exprs/check (syntax->list #'(e . es)) expected)]
[(begin0 e . es)
(begin (tc-exprs/check (syntax->list #'es) Univ)
(tc-expr/check #'e expected))]
;; if
[(if tst body) (tc/if-onearm/check #'tst #'body expected)]
[(if tst thn els) (tc/if-twoarm/check #'tst #'thn #'els expected)]
;; lambda
[(#%plain-lambda formals . body)
(tc/lambda/check form #'(formals) #'(body) expected)]
[(case-lambda [formals . body] ...)
(tc/lambda/check form #'(formals ...) #'(body ...) expected)]
;; send
[(let-values (((_) meth))
(let-values (((_ _) (#%plain-app find-method/who _ rcvr _)))
(#%plain-app _ _ args ...)))
(tc/send #'rcvr #'meth #'(args ...) expected)]
;; let
[(let-values ([(name ...) expr] ...) . body)
(tc/let-values/check #'((name ...) ...) #'(expr ...) #'body form expected)]
[(letrec-values ([(name ...) expr] ...) . body)
(tc/letrec-values/check #'((name ...) ...) #'(expr ...) #'body form expected)]
;; other
[_ (tc-error/expr #:return (ret expected) "cannot typecheck unknown form : ~a~n" (syntax->datum form))]
))))
;; type check form in the current type environment
;; if there is a type error in form, or if it has the wrong annotation, error
;; otherwise, produce the type of form
;; syntax[expr] -> type
(define (tc-expr form)
;; do the actual typechecking of form
;; internal-tc-expr : syntax -> Type
(define (internal-tc-expr form)
(kernel-syntax-case* form #f
(letrec-syntaxes+values #%datum #%app lambda find-method/who) ;; letrec-syntaxes+values is not in kernel-syntax-case literals
;;
[stx
(syntax-property form 'typechecker:with-handlers)
(let ([ty (check-subforms/with-handlers form)])
(unless ty
(int-err "internal error: with-handlers"))
ty)]
[stx
(syntax-property form 'typechecker:ignore-some)
(let ([ty (check-subforms/ignore form)])
(unless ty
(int-err "internal error: ignore-some"))
ty)]
;; data
[(quote #f) (ret (-val #f) (list (make-False-Effect)) (list (make-False-Effect)))]
[(quote #t) (ret (-val #t) (list (make-True-Effect)) (list (make-True-Effect)))]
[(quote val) (ret (tc-literal #'val))]
;; syntax
[(quote-syntax datum) (ret Any-Syntax)]
;; w-c-m
[(with-continuation-mark e1 e2 e3)
(begin (tc-expr/check #'e1 Univ)
(tc-expr/check #'e2 Univ)
(tc-expr #'e3))]
;; lambda
[(#%plain-lambda formals . body)
(tc/lambda form #'(formals) #'(body))]
[(case-lambda [formals . body] ...)
(tc/lambda form #'(formals ...) #'(body ...))]
;; send
[(let-values (((_) meth))
(let-values (((_ _) (#%plain-app find-method/who _ rcvr _)))
(#%plain-app _ _ args ...)))
(tc/send #'rcvr #'meth #'(args ...))]
;; let
[(let-values ([(name ...) expr] ...) . body)
(tc/let-values #'((name ...) ...) #'(expr ...) #'body form)]
[(letrec-values ([(name ...) expr] ...) . body)
(tc/letrec-values #'((name ...) ...) #'(expr ...) #'body form)]
;; mutation!
[(set! id val)
(match-let* ([(tc-result: id-t) (tc-expr #'id)]
[(tc-result: val-t) (tc-expr #'val)])
(unless (subtype val-t id-t)
(tc-error/expr "Mutation only allowed with compatible types:~n~a is not a subtype of ~a" val-t id-t))
(ret -Void))]
;; top-level variable reference - occurs at top level
[(#%top . id) (tc-id #'id)]
;; #%expression
[(#%expression e) (tc-expr #'e)]
;; weird
[(#%variable-reference . _)
(tc-error/expr #:return (ret (Un)) "#%variable-reference is not supported by Typed Scheme")]
;; identifiers
[x (identifier? #'x) (tc-id #'x)]
;; application
[(#%plain-app . _) (tc/app form)]
;; if
[(if tst body) (tc/if-twoarm #'tst #'body #'(#%app void))]
[(if tst thn els) (tc/if-twoarm #'tst #'thn #'els)]
;; syntax
;; for now, we ignore the rhs of macros
[(letrec-syntaxes+values stxs vals . body)
(tc-expr (syntax/loc form (letrec-values vals . body)))]
;; begin
[(begin e . es) (tc-exprs (syntax->list #'(e . es)))]
[(begin0 e . es)
(begin (tc-exprs (syntax->list #'es))
(tc-expr #'e))]
;; other
[_ (tc-error/expr #:return (ret (Un)) "cannot typecheck unknown form : ~a~n" (syntax->datum form))]))
(parameterize ([current-orig-stx form])
;(printf "form: ~a~n" (syntax->datum form))
;; the argument must be syntax
(unless (syntax? form)
(int-err "bad form input to tc-expr: ~a" form))
;; typecheck form
(let ([ty (cond [(type-ascription form) => (lambda (ann)
(tc-expr/check form ann))]
[else (internal-tc-expr form)])])
(match ty
[(tc-result: t eff1 eff2)
(let ([ty* (do-inst form t)])
(ret ty* eff1 eff2))]))))
(define (tc/send rcvr method args [expected #f])
(match (tc-expr rcvr)
[(tc-result: (Instance: (and c (Class: _ _ methods))))
(match (tc-expr method)
[(tc-result: (Value: (? symbol? s)))
(let* ([ftype (cond [(assq s methods) => cadr]
[else (tc-error/expr "send: method ~a not understood by class ~a" s c)])]
[ret-ty (tc/funapp rcvr args (ret ftype) (map tc-expr (syntax->list args)) expected)])
(if expected
(begin (check-below ret-ty expected) (ret expected))
ret-ty))]
[(tc-result: t) (int-err "non-symbol methods not supported by Typed Scheme: ~a" t)])]
[(tc-result: t) (tc-error/expr #:return (or expected (Un)) "send: expected a class instance, got ~a" t)]))
;; type-check a list of exprs, producing the type of the last one.
;; if the list is empty, the type is Void.
;; list[syntax[expr]] -> tc-result
(define (tc-exprs exprs)
(cond [(null? exprs) (ret -Void)]
[(null? (cdr exprs)) (tc-expr (car exprs))]
[else (tc-expr/check (car exprs) Univ)
(tc-exprs (cdr exprs))]))
(define (tc-exprs/check exprs expected)
(cond [(null? exprs) (check-below (ret -Void) expected)]
[(null? (cdr exprs)) (tc-expr/check (car exprs) expected)]
[else (tc-expr/check (car exprs) Univ)
(tc-exprs/check (cdr exprs) expected)]))

294
collects/typed-scheme/typecheck/tc-lambda-unit.ss Normal file
View File

@ -0,0 +1,294 @@
#lang scheme/unit
(require (rename-in "../utils/utils.ss" [infer r:infer] [extend r:extend]))
(require "signatures.ss"
mzlib/trace
scheme/list
(except-in (rep type-rep effect-rep) make-arr) ;; doesn't need tests
(private type-effect-convenience type-annotation union type-utils)
(env type-environments lexical-env)
(utils tc-utils)
mzlib/plt-match
(only-in (private type-effect-convenience) [make-arr* make-arr]))
(require (for-template scheme/base "internal-forms.ss"))
(import tc-expr^)
(export tc-lambda^)
(define (remove-var id thns elss)
(let/ec exit
(define (fail) (exit #f))
(define (rv e)
(match e
[(Var-True-Effect: v) (if (free-identifier=? v id) (make-Latent-Var-True-Effect) (fail))]
[(Var-False-Effect: v) (if (free-identifier=? v id) (make-Latent-Var-False-Effect) (fail))]
[(or (True-Effect:) (False-Effect:)) e]
[(Restrict-Effect: t v) (if (free-identifier=? v id) (make-Latent-Restrict-Effect t) (fail))]
[(Remove-Effect: t v) (if (free-identifier=? v id) (make-Latent-Remove-Effect t) (fail))]))
(cons (map rv thns) (map rv elss))))
(define (expected-str tys-len rest-ty drest arg-len rest)
(format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a"
tys-len
(if (= tys-len 1) "" "s")
(if (or rest-ty
drest)
" and a rest arg"
"")
arg-len
(if (= arg-len 1) "" "s")
(if rest " and a rest arg" "")))
;; listof[id] option[id] block listof[type] option[type] option[(cons type var)] type
(define (check-clause arg-list rest body arg-tys rest-ty drest ret-ty)
(let* ([arg-len (length arg-list)]
[tys-len (length arg-tys)]
[arg-types (if (andmap type-annotation arg-list)
(map get-type arg-list)
(cond
[(= arg-len tys-len) arg-tys]
[(< arg-len tys-len) (take arg-tys arg-len)]
[(> arg-len tys-len) (append arg-tys
(map (lambda _ (or rest-ty (Un)))
(drop arg-list tys-len)))]))])
(define (check-body)
(with-lexical-env/extend
arg-list arg-types
(match (tc-exprs/check (syntax->list body) ret-ty)
[(tc-result: t thn els)
(cond
;; this is T-AbsPred
;; if this function takes only one argument, and all the effects are about that one argument
[(and (not rest-ty) (not drest) (= 1 (length arg-list)) (remove-var (car arg-list) thn els))
=> (lambda (thn/els) (make-arr arg-types t rest-ty drest (car thn/els) (cdr thn/els)))]
;; otherwise, the simple case
[else (make-arr arg-types t rest-ty drest null null)])]
[t (int-err "bad match - not a tc-result: ~a ~a ~a" t ret-ty (syntax->datum body))])))
#;(for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) arg-list)
(when (or (not (= arg-len tys-len))
(and rest (and (not rest-ty)
(not drest))))
(tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest)))
(cond
[(not rest)
(check-body)]
[drest
(with-dotted-env/extend
rest (car drest) (cdr drest)
(check-body))]
[(dotted? rest)
=>
(lambda (b)
(let ([dty (get-type rest)])
(with-dotted-env/extend
rest dty b
(check-body))))]
[else
(let ([rest-type (cond
[rest-ty rest-ty]
[(type-annotation rest) (get-type rest)]
[(< arg-len tys-len) (list-ref arg-tys arg-len)]
[else (Un)])])
(with-lexical-env/extend
(list rest) (list (-lst rest-type))
(check-body)))])))
;; typecheck a single lambda, with argument list and body
;; drest-ty and drest-bound are both false or not false
;; syntax-list[id] block listof[type] type option[type] option[(cons type var)] -> arr
(define (tc/lambda-clause/check args body arg-tys ret-ty rest-ty drest)
(syntax-case args ()
[(args* ...)
(check-clause (syntax->list #'(args* ...)) #f body arg-tys rest-ty drest ret-ty)]
[(args* ... . rest)
(check-clause (syntax->list #'(args* ...)) #'rest body arg-tys rest-ty drest ret-ty)]))
;; syntax-list[id] block -> arr
(define (tc/lambda-clause args body)
(syntax-case args ()
[(args ...)
(let* ([arg-list (syntax->list #'(args ...))]
[arg-types (map get-type arg-list)])
#;(for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) arg-list)
(with-lexical-env/extend
arg-list arg-types
(match (tc-exprs (syntax->list body))
[(tc-result: t thn els)
(cond
;; this is T-AbsPred
;; if this function takes only one argument, and all the effects are about that one argument
[(and (= 1 (length arg-list)) (remove-var (car arg-list) thn els))
=> (lambda (thn/els) (make-arr arg-types t #f (car thn/els) (cdr thn/els)))]
;; otherwise, the simple case
[else (make-arr arg-types t)])]
[t (int-err "bad match - not a tc-result: ~a no ret-ty" t)])))]
[(args ... . rest)
(let* ([arg-list (syntax->list #'(args ...))]
[arg-types (map get-type arg-list)])
#;(for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) (cons #'rest arg-list))
(cond
[(dotted? #'rest)
=>
(lambda (bound)
(unless (Dotted? (lookup (current-tvars) bound
(lambda _ (tc-error/stx #'rest
"Bound on ... type (~a) was not in scope" bound))))
(tc-error "Bound on ... type (~a) is not an appropriate type variable" bound))
(let ([rest-type (parameterize ([current-tvars
(extend-env (list bound)
(list (make-DottedBoth (make-F bound)))
(current-tvars))])
(get-type #'rest))])
(with-lexical-env/extend
arg-list
arg-types
(parameterize ([dotted-env (extend-env (list #'rest)
(list (cons rest-type bound))
(dotted-env))])
(match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))])
(make-arr-dots arg-types t rest-type bound))))))]
[else
(let ([rest-type (get-type #'rest)])
(with-lexical-env/extend
(cons #'rest arg-list)
(cons (make-Listof rest-type) arg-types)
(match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))])
(make-arr arg-types t rest-type))))]))]))
;(trace tc-args)
;; tc/mono-lambda : syntax-list syntax-list -> Funty
;; typecheck a sequence of case-lambda clauses
(define (tc/mono-lambda formals bodies expected)
(define (syntax-len s)
(cond [(syntax->list s) => length]
[else (let loop ([s s])
(cond
[(pair? s)
(+ 1 (loop (cdr s)))]
[(pair? (syntax-e s))
(+ 1 (loop (cdr (syntax-e s))))]
[else 1]))]))
(if (and expected
(= 1 (length (syntax->list formals))))
;; special case for not-case-lambda
(let loop ([expected expected])
(match expected
[(Mu: _ _) (loop (unfold expected))]
[(Function: (list (arr: argss rets rests drests '() _ _) ...))
(for ([args argss] [ret rets] [rest rests] [drest drests])
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest drest))
expected]
[t (let ([t (tc/mono-lambda formals bodies #f)])
(check-below t expected))]))
(let loop ([formals (syntax->list formals)]
[bodies (syntax->list bodies)]
[formals* null]
[bodies* null]
[nums-seen null])
(cond
[(null? formals)
(make-Function (map tc/lambda-clause (reverse formals*) (reverse bodies*)))]
[(memv (syntax-len (car formals)) nums-seen)
;; we check this clause, but it doesn't contribute to the overall type
(tc/lambda-clause (car formals) (car bodies))
(loop (cdr formals) (cdr bodies) formals* bodies* nums-seen)]
[else
(loop (cdr formals) (cdr bodies)
(cons (car formals) formals*)
(cons (car bodies) bodies*)
(cons (syntax-len (car formals)) nums-seen))]))))
(define (tc/lambda form formals bodies)
(tc/lambda/internal form formals bodies #f))
;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> Type
(define (tc/lambda/internal form formals bodies expected)
(if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected))
(tc/plambda form formals bodies expected)
(ret (tc/mono-lambda formals bodies expected))))
(define (tc/lambda/check form formals bodies expected)
(tc/lambda/internal form formals bodies expected))
;; tc/plambda syntax syntax-list syntax-list type -> Poly
;; formals and bodies must by syntax-lists
(define (tc/plambda form formals bodies expected)
(define (maybe-loop form formals bodies expected)
(match expected
[(Function: _) (tc/mono-lambda formals bodies expected)]
[(or (Poly: _ _) (PolyDots: _ _))
(tc/plambda form formals bodies expected)]))
(match expected
[(Poly-names: ns expected*)
(let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
(when (and (pair? p) (eq? '... (car (last p))))
(tc-error "Expected a polymorphic function without ..., but given function had ..."))
(or (and p (map syntax-e (syntax->list p)))
ns))]
[literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
(maybe-loop form formals bodies expected*))])
;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
(ret expected))]
[(PolyDots-names: (list ns ... dvar) expected*)
(let-values
([(tvars dotted)
(let ([p (syntax-property form 'typechecker:plambda)])
(if p
(match (map syntax-e (syntax->list p))
[(list var ... dvar '...)
(values var dvar)]
[_ (tc-error "Expected a polymorphic function with ..., but given function had no ...")])
(values ns dvar)))])
(let* ([literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env (cons dotted literal-tvars)
(cons (make-Dotted (make-F dotted))
new-tvars)
(current-tvars))])
(maybe-loop form formals bodies expected*))])
(ret expected)))]
[#f
(match (map syntax-e (syntax->list (syntax-property form 'typechecker:plambda)))
[(list tvars ... dotted-var '...)
(let* ([literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env (cons dotted-var literal-tvars)
(cons (make-Dotted (make-F dotted-var)) new-tvars)
(current-tvars))])
(tc/mono-lambda formals bodies #f))])
(ret (make-PolyDots (append literal-tvars (list dotted-var)) ty)))]
[tvars
(let* ([literal-tvars tvars]
[new-tvars (map make-F literal-tvars)]
[ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
(tc/mono-lambda formals bodies #f))])
;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
(ret (make-Poly literal-tvars ty)))])]
[_
(unless (check-below (tc/plambda form formals bodies #f) expected)
(tc-error/expr #:return (ret expected) "Expected a value of type ~a, but got a polymorphic function." expected))
(ret expected)]))
;; form : a syntax object for error reporting
;; formals : the formal arguments to the loop
;; body : a block containing the body of the loop
;; name : the name of the loop
;; args : the types of the actual arguments to the loop
;; ret : the expected return type of the whole expression
(define (tc/rec-lambda/check form formals body name args ret)
(with-lexical-env/extend
(syntax->list formals) args
(let ([t (->* args ret)])
(with-lexical-env/extend
(list name) (list t)
(begin (tc-exprs/check (syntax->list body) ret)
(make-Function (list t)))))))
;(trace tc/mono-lambda)

141
collects/typed-scheme/typecheck/tc-let-unit.ss Normal file
View File

@ -0,0 +1,141 @@
#lang scheme/unit
(require (rename-in "../utils/utils.ss" [infer r:infer]))
(require "signatures.ss"
(private type-effect-convenience type-annotation parse-type type-utils)
(env lexical-env type-alias-env type-env)
syntax/free-vars
mzlib/trace
scheme/match
syntax/kerncase
(for-template
scheme/base
"internal-forms.ss"))
(require (only-in srfi/1/list s:member))
(import tc-expr^)
(export tc-let^)
(define (do-check expr->type namess types form exprs body clauses expected)
;; extend the lexical environment for checking the body
(with-lexical-env/extend
;; the list of lists of name
namess
;; the types
types
(for-each expr->type
clauses
exprs
(map -values types))
(if expected
(tc-exprs/check (syntax->list body) expected)
(tc-exprs (syntax->list body)))))
#|
;; this is more abstract, but sucks
(define ((mk f) namess exprs body form)
(let* ([names (map syntax->list (syntax->list namess))]
[exprs (syntax->list exprs)])
(f (lambda (e->t namess types exprs) (do-check e->t namess types form exprs body)) names exprs)))
(define tc/letrec-values
(mk (lambda (do names exprs)
(let ([types (map (lambda (l) (map get-type l)) names)])
(do tc-expr/t names types exprs)))))
(define tc/let-values
(mk (lambda (do names exprs)
(let* (;; the types of the exprs
[inferred-types (map tc-expr/t exprs)]
;; the annotated types of the name (possibly using the inferred types)
[types (map get-type/infer names inferred-types)])
(do (lambda (x) x) names types inferred-types)))))
|#
(define (tc/letrec-values/check namess exprs body form expected)
(tc/letrec-values/internal namess exprs body form expected))
(define (tc/letrec-values namess exprs body form)
(tc/letrec-values/internal namess exprs body form #f))
(define (tc-expr/maybe-expected/t e name)
(define expecteds
(map (lambda (stx) (lookup-type stx (lambda () #f))) name))
(define mk (if (and (pair? expecteds) (null? (cdr expecteds)))
car
-values))
(define tcr
(if
(andmap values expecteds)
(tc-expr/check e (mk expecteds))
(tc-expr e)))
(match tcr
[(tc-result: t) t]))
(define (tc/letrec-values/internal namess exprs body form expected)
(let* ([names (map syntax->list (syntax->list namess))]
[flat-names (apply append names)]
[exprs (syntax->list exprs)]
;; the clauses for error reporting
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
(for-each (lambda (names body)
(kernel-syntax-case* body #f (values :-internal define-type-alias-internal)
[(begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values))
(register-resolved-type-alias #'nm (parse-type #'ty))]
[(begin (quote-syntax (:-internal nm ty)) (#%plain-app values))
(register-type/undefined #'nm (parse-type #'ty))]
[_ (void)]))
names
exprs)
(let loop ([names names] [exprs exprs] [flat-names flat-names] [clauses clauses])
(cond
;; after everything, check the body expressions
[(null? names)
(if expected (tc-exprs/check (syntax->list body) expected) (tc-exprs (syntax->list body)))]
;; if none of the names bound in the letrec are free vars of this rhs
[(not (ormap (lambda (n) (s:member n flat-names bound-identifier=?)) (free-vars (car exprs))))
;; then check this expression separately
(with-lexical-env/extend
(list (car names))
(list (get-type/infer (car names) (car exprs) (lambda (e) (tc-expr/maybe-expected/t e (car names))) tc-expr/check/t))
(loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses)))]
[else
;(for-each (lambda (vs) (for-each (lambda (v) (printf/log "Letrec Var: ~a~n" (syntax-e v))) vs)) names)
(do-check (lambda (stx e t) (tc-expr/check/t e t))
names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)]))))
;; this is so match can provide us with a syntax property to
;; say that this binding is only called in tail position
(define ((tc-expr-t/maybe-expected expected) e)
(kernel-syntax-case e #f
[(#%plain-lambda () _)
(and expected (syntax-property e 'typechecker:called-in-tail-position))
(begin
(tc-expr/check e (-> expected))
(-> expected))]
[_ (tc-expr/t e)]))
(define (tc/let-values/internal namess exprs body form expected)
(let* (;; a list of each name clause
[names (map syntax->list (syntax->list namess))]
;; all the trailing expressions - the ones actually bound to the names
[exprs (syntax->list exprs)]
;; the types of the exprs
#;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)]
;; the annotated types of the name (possibly using the inferred types)
[types (for/list ([name names] [e exprs]) (get-type/infer name e (tc-expr-t/maybe-expected expected) tc-expr/check/t))]
;; the clauses for error reporting
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
(do-check void names types form types body clauses expected)))
(define (tc/let-values/check namess exprs body form expected)
(tc/let-values/internal namess exprs body form expected))
(define (tc/let-values namess exprs body form)
(tc/let-values/internal namess exprs body form #f))
;(trace tc/letrec-values/internal)

210
collects/typed-scheme/typecheck/tc-structs.ss Normal file
View File

@ -0,0 +1,210 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require (rep type-rep)
(private type-effect-convenience
type-utils parse-type
union resolve-type)
(env type-env type-environments type-name-env)
(utils tc-utils)
"def-binding.ss"
syntax/kerncase
syntax/struct
mzlib/trace
scheme/match
(for-syntax scheme/base))
(require (for-template scheme/base
"internal-forms.ss"))
(provide tc/struct tc/poly-struct names-of-struct tc/builtin-struct d-s)
(define (names-of-struct stx)
(define (parent? stx)
(syntax-case stx ()
[(a b)
(and (identifier? #'a)
(identifier? #'b))
#t]
[a
(identifier? #'a)
#t]
[_ #f]))
(kernel-syntax-case* stx #f
(define-typed-struct-internal values)
[(#%define-values () (begin (quote-syntax (define-typed-struct-internal (ids ...) nm/par . rest)) (#%plain-app values)))
(and (andmap identifier? (syntax->list #'(ids ...)))
(parent? #'nm/par))
(let-values ([(nm _1 _2 _3 _4) (parse-parent #'nm/par)])
(list nm))]
[(#%define-values () (begin (quote-syntax (define-typed-struct-internal nm/par . rest)) (#%plain-app values)))
(let-values ([(nm _1 _2 _3 _4) (parse-parent #'nm/par)])
(list nm))]
[(#%define-values () (begin (quote-syntax (define-typed-struct/exec-internal nm/par . rest)) (#%plain-app values)))
(let-values ([(nm _1 _2 _3 _4) (parse-parent #'nm/par)])
(list nm))]
[_ (int-err "not define-typed-struct: ~a" (syntax->datum stx))]))
;; parse name field of struct, determining whether a parent struct was specified
;; syntax -> (values identifier Option[Type](must be name) Option[Type](must be struct) List[Types] Symbol Type)
(define (parse-parent nm/par)
(syntax-case nm/par ()
[nm (identifier? #'nm) (values #'nm #f #f (syntax-e #'nm) (make-F (syntax-e #'nm)))]
[(nm par) (let* ([parent0 (parse-type #'par)]
[parent (resolve-name parent0)])
(values #'nm parent0 parent (syntax-e #'nm) (make-F (syntax-e #'nm))))]
[_ (int-err "not a parent: ~a" (syntax->datum nm/par))]))
;; generate struct names given type name and field names
;; generate setters if setters? is true
;; all have syntax loc of name
;; identifier listof[identifier] boolean -> (values identifier identifier list[identifier] Option[list[identifier]])
(define (struct-names nm flds setters?)
(define (split l)
(let loop ([l l] [getters '()] [setters '()])
(if (null? l)
(values (reverse getters) (reverse setters))
(loop (cddr l) (cons (car l) getters) (cons (cadr l) setters)))))
(match (build-struct-names nm flds #f (not setters?) nm)
[(list _ maker pred getters/setters ...)
(if setters?
(let-values ([(getters setters) (split getters/setters)])
(values maker pred getters setters))
(values maker pred getters/setters #f))]))
;; gets the fields of the parent type, if they exist
;; Option[Struct-Ty] -> Listof[Type]
(define (get-parent-flds p)
(match p
[(Struct: _ _ flds _ _ _ _) flds]
[(Name: n) (get-parent-flds (lookup-type-name n))]
[#f null]))
;; construct all the various types for structs, and then register the approriate names
;; identifier listof[identifier] type listof[Type] listof[Type] boolean -> Type listof[Type] listof[Type]
(define (mk/register-sty nm flds parent parent-field-types types
#:wrapper [wrapper values]
#:type-wrapper [type-wrapper values]
#:mutable [setters? #f]
#:proc-ty [proc-ty #f]
#:maker [maker #f]
#:constructor-return [cret #f]
#:poly? [poly? #f])
;; create the approriate names that define-struct will bind
(define-values (maker pred getters setters) (struct-names nm flds setters?))
(let* ([name (syntax-e nm)]
[fld-types (append parent-field-types types)]
[sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier))]
[external-fld-types/no-parent types]
[external-fld-types fld-types])
(register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
#:wrapper wrapper
#:type-wrapper type-wrapper
#:maker maker
#:constructor-return cret)))
;; generate names, and register the approriate types give field types and structure type
;; optionally wrap things
;; identifier Type Listof[identifer] Listof[Type] Listof[Type] #:wrapper (Type -> Type) #:maker identifier
(define (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
#:wrapper [wrapper (lambda (x) x)]
#:type-wrapper [type-wrapper values]
#:maker [maker* #f]
#:constructor-return [cret #f])
;; create the approriate names that define-struct will bind
(define-values (maker pred getters setters) (struct-names nm flds setters?))
;; the type name that is used in all the types
(define name (type-wrapper (make-Name nm)))
;; the list of names w/ types
(define bindings
(append
(list (cons (or maker* maker)
(wrapper (->* external-fld-types (if cret cret name))))
(cons pred
(make-pred-ty (wrapper name))))
(map (lambda (g t) (cons g (wrapper (->* (list name) t)))) getters external-fld-types/no-parent)
(if setters?
(map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent)
null)))
(register-type-name nm (wrapper sty))
(for/list ([e bindings])
(let ([nm (car e)]
[t (cdr e)])
(register-type nm t)
(make-def-binding nm t))))
;; check and register types for a polymorphic define struct
;; tc/poly-struct : Listof[identifier] (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void
(define (tc/poly-struct vars nm/par flds tys)
;; parent field types can't actually be determined here
(define-values (nm parent-name parent name name-tvar) (parse-parent nm/par))
;; create type variables for the new type parameters
(define tvars (map syntax-e vars))
(define new-tvars (map make-F tvars))
;; parse the types
(define types
;; add the type parameters of this structure to the tvar env
(parameterize ([current-tvars (extend-env tvars new-tvars (current-tvars))])
;; parse the field types
(map parse-type tys)))
;; instantiate the parent if necessary, with new-tvars
(define concrete-parent
(if (Poly? parent)
(instantiate-poly parent new-tvars)
parent))
;; get the fields of the parent, if it exists
(define parent-field-types (get-parent-flds concrete-parent))
;; create the actual structure type, and the types of the fields
;; that the outside world will see
;; then register them
(mk/register-sty nm flds parent-name parent-field-types types
;; wrap everything in the approriate forall
#:wrapper (lambda (t) (make-Poly tvars t))
#:type-wrapper (lambda (t) (make-App t new-tvars #f))
#:poly? #t))
;; typecheck a non-polymophic struct and register the approriate types
;; tc/struct : (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void
(define (tc/struct nm/par flds tys [proc-ty #f] #:maker [maker #f] #:constructor-return [cret #f] #:mutable [mutable #f])
;; get the parent info and create some types and type variables
(define-values (nm parent-name parent name name-tvar) (parse-parent nm/par))
;; parse the field types, and determine if the type is recursive
(define types (map parse-type tys))
(define proc-ty-parsed
(if proc-ty
(parse-type proc-ty)
#f))
;; create the actual structure type, and the types of the fields
;; that the outside world will see
(mk/register-sty nm flds parent-name (get-parent-flds parent) types
;; procedure
#:proc-ty proc-ty-parsed
#:maker maker
#:constructor-return (and cret (parse-type cret))
#:mutable mutable))
;; register a struct type
;; convenience function for built-in structs
;; tc/builtin-struct : identifier identifier Listof[identifier] Listof[Type] Listof[Type] -> void
(define (tc/builtin-struct nm parent flds tys parent-tys)
(let ([parent* (if parent (make-Name parent) #f)])
(mk/register-sty nm flds parent* parent-tys tys
#:mutable #t)))
;; syntax for tc/builtin-struct
(define-syntax (d-s stx)
(syntax-case stx (:)
[(_ (nm par) ([fld : ty] ...) (par-ty ...))
#'(tc/builtin-struct #'nm #'par
(list #'fld ...)
(list ty ...)
(list par-ty ...))]
[(_ nm ([fld : ty] ...) (par-ty ...))
#'(tc/builtin-struct #'nm #f
(list #'fld ...)
(list ty ...)
(list par-ty ...))]))

242
collects/typed-scheme/typecheck/tc-toplevel.ss Normal file
View File

@ -0,0 +1,242 @@
#lang scheme/unit
(require (rename-in "../utils/utils.ss" [infer r:infer]))
(require syntax/kerncase
mzlib/etc
scheme/match
"signatures.ss"
"tc-structs.ss"
(private type-utils type-effect-convenience parse-type type-annotation mutated-vars type-contract)
(env type-env init-envs type-name-env type-alias-env)
(utils tc-utils)
"provide-handling.ss"
"def-binding.ss"
(for-template
"internal-forms.ss"
mzlib/contract
scheme/base))
(import tc-expr^ check-subforms^)
(export typechecker^)
(define (tc-toplevel/pass1 form)
;(printf "form-top: ~a~n" form)
;; first, find the mutated variables:
(find-mutated-vars form)
(parameterize ([current-orig-stx form])
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal
define-typed-struct/exec-internal :-internal assert-predicate-internal
require/typed-internal values)
;; forms that are handled in other ways
[stx
(or (syntax-property form 'typechecker:ignore)
(syntax-property form 'typechecker:ignore-some))
(list)]
;; type aliases have already been handled by an earlier pass
[(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)))
(list)]
;; require/typed
[(define-values () (begin (quote-syntax (require/typed-internal nm ty)) (#%plain-app values)))
(register-type #'nm (parse-type #'ty))]
;; define-typed-struct
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...))) (#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))]
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...) #:mutable)) (#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:mutable #t)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...) #:maker m #:constructor-return t))
(#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:maker #'m #:constructor-return #'t)]
;; define-typed-struct w/ polymorphism
[(define-values () (begin (quote-syntax (define-typed-struct-internal (vars ...) nm ([fld : ty] ...))) (#%plain-app values)))
(tc/poly-struct (syntax->list #'(vars ...)) #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))]
;; executable structs - this is a big hack
[(define-values () (begin (quote-syntax (define-typed-struct/exec-internal nm ([fld : ty] ...) proc-ty)) (#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #'proc-ty)]
;; predicate assertion - needed for define-type b/c or doesn't work
[(define-values () (begin (quote-syntax (assert-predicate-internal ty pred)) (#%plain-app values)))
(register-type #'pred (make-pred-ty (parse-type #'ty)))]
;; top-level type annotation
[(define-values () (begin (quote-syntax (:-internal id ty)) (#%plain-app values)))
(identifier? #'id)
(register-type/undefined #'id (parse-type #'ty))]
;; values definitions
[(define-values (var ...) expr)
(let* ([vars (syntax->list #'(var ...))])
(cond
;; if all the variables have types, we stick them into the environment
[(andmap (lambda (s) (syntax-property s 'type-label)) vars)
(let ([ts (map get-type vars)])
(for-each register-type vars ts)
(map make-def-binding vars ts))]
;; if this already had an annotation, we just construct the binding reps
[(andmap (lambda (s) (lookup-type s (lambda () #f))) vars)
(for-each finish-register-type vars)
(map (lambda (s) (make-def-binding s (lookup-type s))) vars)]
;; special case to infer types for top level defines - should handle the multiple values case here
[(and (= 1 (length vars))
(with-handlers ([exn:fail? (lambda _ #f)])
(save-errors!)
(begin0 (tc-expr #'expr)
(restore-errors!))))
=> (match-lambda
[(tc-result: t)
(register-type (car vars) t)
(list (make-def-binding (car vars) t))]
[t (int-err "~a is not a tc-result" t)])]
[else
(tc-error "Untyped definition : ~a" (map syntax-e vars))]))]
;; to handle the top-level, we have to recur into begins
[(begin . rest)
(apply append (filter list? (map tc-toplevel/pass1 (syntax->list #'rest))))]
;; define-syntaxes just get noted
[(define-syntaxes (var ...) . rest)
(andmap identifier? (syntax->list #'(var ...)))
(map make-def-stx-binding (syntax->list #'(var ...)))]
;; otherwise, do nothing in this pass
;; handles expressions, provides, requires, etc and whatnot
[_ (list)])))
;; typecheck the expressions of a module-top-level form
;; no side-effects
;; syntax -> void
(define (tc-toplevel/pass2 form)
(parameterize ([current-orig-stx form])
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal
require/typed-internal values)
;; these forms we have been instructed to ignore
[stx
(syntax-property form 'typechecker:ignore)
(void)]
;; this is a form that we mostly ignore, but we check some interior parts
[stx
(syntax-property form 'typechecker:ignore-some)
(check-subforms/ignore form)]
;; these forms should always be ignored
[(#%require . _) (void)]
[(#%provide . _) (void)]
[(define-syntaxes . _) (void)]
[(define-values-for-syntax . _) (void)]
;; these forms are handled in pass1
[(define-values () (begin (quote-syntax (require/typed-internal . rest)) (#%plain-app values)))
(void)]
[(define-values () (begin (quote-syntax (define-type-alias-internal . rest)) (#%plain-app values)))
(void)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal . rest)) (#%plain-app values)))
(void)]
;; definitions just need to typecheck their bodies
[(define-values (var ...) expr)
(let* ([vars (syntax->list #'(var ...))]
[ts (map lookup-type vars)])
(tc-expr/check #'expr (-values ts)))
(void)]
;; to handle the top-level, we have to recur into begins
[(begin) (void)]
[(begin . rest)
(let loop ([l (syntax->list #'rest)])
(if (null? (cdr l))
(tc-toplevel/pass2 (car l))
(begin (tc-toplevel/pass2 (car l))
(loop (cdr l)))))]
;; otherwise, the form was just an expression
[_ (tc-expr form)])))
;; new implementation of type-check
(define-syntax-rule (internal-syntax-pred nm)
(lambda (form)
(kernel-syntax-case* form #f
(nm values)
[(define-values () (begin (quote-syntax (nm . rest)) (#%plain-app values)))
#t]
[_ #f])))
(define (parse-def x)
(kernel-syntax-case x #f
[(define-values (nm ...) . rest) (syntax->list #'(nm ...))]
[_ #f]))
(define (parse-syntax-def x)
(kernel-syntax-case x #f
[(define-syntaxes (nm ...) . rest) (syntax->list #'(nm ...))]
[_ #f]))
(define (add-type-name! names)
(for-each register-type-name names))
(define (parse-type-alias form)
(kernel-syntax-case* form #f
(define-type-alias-internal values)
[(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)))
(values #'nm #'ty)]
[_ (int-err "not define-type-alias")]))
(define (type-check forms0)
(begin-with-definitions
(define forms (syntax->list forms0))
(define-values (type-aliases struct-defs stx-defs0 val-defs0 provs reqs)
(filter-multiple
forms
(internal-syntax-pred define-type-alias-internal)
(lambda (e) (or ((internal-syntax-pred define-typed-struct-internal) e)
((internal-syntax-pred define-typed-struct/exec-internal) e)))
parse-syntax-def
parse-def
provide?
define/fixup-contract?))
(for-each (compose register-type-alias parse-type-alias) type-aliases)
;; add the struct names to the type table
(for-each (compose add-type-name! names-of-struct) struct-defs)
;; resolve all the type aliases, and error if there are cycles
(resolve-type-aliases parse-type)
;; do pass 1, and collect the defintions
(define defs (apply append (filter list? (map tc-toplevel/pass1 forms))))
;; separate the definitions into structures we'll handle for provides
(define stx-defs (filter def-stx-binding? defs))
(define val-defs (filter def-binding? defs))
;; typecheck the expressions and the rhss of defintions
(for-each tc-toplevel/pass2 forms)
;; check that declarations correspond to definitions
(check-all-registered-types)
;; report delayed errors
(report-all-errors)
;; compute the new provides
(with-syntax
([((new-provs ...) ...) (map (generate-prov stx-defs val-defs) provs)])
#`(begin
#,(env-init-code)
#,(tname-env-init-code)
#,(talias-env-init-code)
(begin new-provs ... ...)))))
;; typecheck a top-level form
;; used only from #%top-interaction
;; syntax -> void
(define (tc-toplevel-form form)
(tc-toplevel/pass1 form)
(begin0 (tc-toplevel/pass2 form)
(report-all-errors)))

15
collects/typed-scheme/typecheck/typechecker.ss Normal file
View File

@ -0,0 +1,15 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (utils unit-utils)
mzlib/trace
(only-in scheme/unit provide-signature-elements)
"signatures.ss" "tc-toplevel.ss"
"tc-if-unit.ss" "tc-lambda-unit.ss" "tc-app-unit.ss"
"tc-let-unit.ss" "tc-dots-unit.ss"
"tc-expr-unit.ss" "check-subforms-unit.ss")
(provide-signature-elements typechecker^ tc-expr^)
(define-values/link-units/infer
tc-toplevel@ tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@)

7
collects/typed-scheme/typed-scheme.scrbl
View File

@ -436,13 +436,16 @@ The following base types are parameteric in their type arguments.
@defform*[#:id -> #:literals (* ...)
[(dom ... -> rng)
(dom ... rest * -> rng)
(dom ... rest ... bound -> rng)]]{is the type of functions from the (possibly-empty)
(dom ... rest ... bound -> rng)
(dom -> rng : pred)]]{is the type of functions from the (possibly-empty)
sequence @scheme[dom ...] to the @scheme[rng] type. The second form
specifies a uniform rest argument of type @scheme[rest], and the
third form specifies a non-uniform rest argument of type
@scheme[rest] with bound @scheme[bound]. In the third form, the
second occurrence of @scheme[...] is literal, and @scheme[bound]
must be an identifier denoting a type variable.}
must be an identifier denoting a type variable. In the fourth form,
there must be only one @scheme[dom] and @scheme[pred] is the type
checked by the predicate.}
@defform[(U t ...)]{is the union of the types @scheme[t ...]}
@defform[(case-lambda fun-ty ...)]{is a function that behaves like all of
the @scheme[fun-ty]s. The @scheme[fun-ty]s must all be function

28
collects/typed-scheme/typed-scheme.ss
View File

@ -1,22 +1,18 @@
#lang scheme/base
(require "private/base-env.ss"
"private/base-types.ss"
(require (rename-in "utils/utils.ss" [infer r:infer]))
(require (private base-env base-types)
(for-syntax
scheme/base
"private/type-utils.ss"
"private/typechecker.ss"
"private/type-rep.ss"
"private/provide-handling.ss"
"private/type-environments.ss"
"private/tc-utils.ss"
"private/type-name-env.ss"
"private/type-alias-env.ss"
(except-in "private/utils.ss" extend)
(only-in "private/infer-dummy.ss" infer-param)
"private/infer.ss"
"private/type-effect-convenience.ss"
"private/type-contract.ss"
(private type-utils type-contract type-effect-convenience)
(typecheck typechecker provide-handling)
(env type-environments type-name-env type-alias-env)
(r:infer infer)
(utils tc-utils)
(rep type-rep)
(except-in (utils utils) infer extend)
(only-in (r:infer infer-dummy) infer-param)
scheme/nest
syntax/kerncase
scheme/match))
@ -31,7 +27,7 @@
(provide (rename-out [module-begin #%module-begin]
[top-interaction #%top-interaction]
[#%plain-lambda lambda]
[#%plain-app #%app]
[#%app #%app]
[require require]))
(define-for-syntax catch-errors? #f)

134
collects/typed-scheme/utils/tc-utils.ss Normal file
View File

@ -0,0 +1,134 @@
#lang scheme/base
(provide (all-defined-out))
(require "syntax-traversal.ss" (for-syntax scheme/base) scheme/match)
;; a parameter representing the original location of the syntax being currently checked
(define current-orig-stx (make-parameter #'here))
(define orig-module-stx (make-parameter #f))
(define expanded-module-stx (make-parameter #f))
(define (stringify l [between " "])
(define (intersperse v l)
(cond [(null? l) null]
[(null? (cdr l)) l]
[else (cons (car l) (cons v (intersperse v (cdr l))))]))
(apply string-append (intersperse between (map (lambda (s) (format "~a" s)) l))))
;; helper function, not currently used
(define (find-origin stx)
(cond [(syntax-property stx 'origin) => (lambda (orig)
(let ([r (reverse orig)])
(let loop ([r (reverse orig)])
(if (null? r) #f
(if (syntax-source (car r)) (car r)
(loop (cdr r)))))))]
[else #f]))
;; do we print the fully-expanded syntax in error messages?
(define print-syntax? (make-parameter #f))
(define check-unreachable-code? (make-parameter #f))
(define (locate-stx stx)
(define omodule (orig-module-stx))
(define emodule (expanded-module-stx))
;(printf "orig: ~a~n" (syntax-object->datum omodule))
;(printf "exp: ~a~n" (syntax-object->datum emodule))
;(printf "stx (locate): ~a~n" (syntax-object->datum stx))
(if (and (not (print-syntax?)) omodule emodule stx)
(look-for-in-orig omodule emodule stx)
stx))
(define (raise-typecheck-error msg stxs)
(raise (make-exn:fail:syntax (string-append "typecheck: " msg)
(current-continuation-marks)
stxs)))
(define delayed-errors null)
(define-struct err (msg stx) #:prefab)
(define-values (save-errors! restore-errors!)
(let ([v (box #f)])
(values (lambda () (set-box! v delayed-errors))
(lambda () (set! delayed-errors (unbox v))))))
(define (report-all-errors)
(define (reset!) (set! delayed-errors null))
(match (reverse delayed-errors)
[(list) (void)]
[(list (struct err (msg stx)))
(reset!)
(raise-typecheck-error msg stx)]
[l
(let ([stxs
(for/list ([e l])
(sync (thread (lambda () (raise-typecheck-error (err-msg e) (err-stx e)))))
(err-stx e))])
(reset!)
(unless (null? stxs)
(raise-typecheck-error (format "Summary: ~a errors encountered" (length stxs)) (apply append stxs))))]))
(define delay-errors? (make-parameter #f))
(define (tc-error/delayed msg #:stx [stx* (current-orig-stx)] . rest)
(let ([stx (locate-stx stx*)])
(unless (syntax? stx)
(int-err "erroneous syntax was not a syntax object: ~a ~a" stx (syntax->datum stx*)))
(if (delay-errors?)
(set! delayed-errors (cons (make-err (apply format msg rest) (list stx)) delayed-errors))
(raise-typecheck-error (apply format msg rest) (list stx)))))
;; produce a type error, using the current syntax
(define (tc-error msg . rest)
(let ([stx (locate-stx (current-orig-stx))])
;; If this isn't original syntax, then we can get some pretty bogus error messages. Note
;; that this is from a macro expansion, so that introduced vars and such don't confuse the user.
(cond
[(not (orig-module-stx))
(raise-typecheck-error (apply format msg rest) (list stx))]
[(eq? (syntax-source (current-orig-stx)) (syntax-source (orig-module-stx)))
(raise-typecheck-error (apply format msg rest) (list stx))]
[else (raise-typecheck-error (apply format (string-append "Error in macro expansion -- " msg) rest) (list stx))])))
;; produce a type error, given a particular syntax
(define (tc-error/stx stx msg . rest)
(parameterize ([current-orig-stx stx])
(apply tc-error msg rest)))
;; check two identifiers to see if they have the same name
(define (symbolic-identifier=? a b)
(eq? (syntax-e a) (syntax-e b)))
;; parameter for currently-defined type aliases
;; this is used only for printing type names
(define current-type-names (make-parameter (lambda () '())))
;; for reporting internal errors in the type checker
(define-struct (exn:fail:tc exn:fail) ())
;; raise an internal error - typechecker bug!
(define (int-err msg . args)
(raise (make-exn:fail:tc (string-append "Internal Typechecker Error: "
(apply format msg args)
(format "\nwhile typechecking\n~a" (syntax->datum (current-orig-stx))))
(current-continuation-marks))))
(define-syntax (nyi stx)
(syntax-case stx ()
[(_ str)
(quasisyntax/loc stx (int-err "~a: not yet implemented: ~a" str #,(syntax/loc stx (this-expression-file-name))))]
[(_) (syntax/loc stx (nyi ""))]))
;; are we currently expanding in a typed module (or top-level form)?
(define typed-context? (box #f))
;; what type names have been referred to in this module?
(define type-name-references (make-parameter '()))
(define (add-type-name-reference t)
(type-name-references (cons t (type-name-references))))

224
collects/typed-scheme/utils/utils.ss Normal file
View File

@ -0,0 +1,224 @@
#lang scheme/base
(require (for-syntax scheme/base)
mzlib/plt-match
scheme/require-syntax
mzlib/struct)
(provide with-syntax* syntax-map start-timing do-time reverse-begin printf/log
with-logging-to-file log-file-name ==
print-type*
print-effect*
define-struct/printer
id
filter-multiple
hash-union
in-pairs
in-list-forever
extend
debug
in-syntax
;; require macros
rep utils typecheck infer env private)
(define-syntax (define-requirer stx)
(syntax-case stx ()
[(_ nm)
#`(...
(define-require-syntax nm
(lambda (stx)
(syntax-case stx ()
[(_ id ...)
(andmap identifier? (syntax->list #'(id ...)))
(with-syntax ([(id* ...)
(map (lambda (id)
(datum->syntax
id
(string->symbol
(string-append
"typed-scheme/"
#,(symbol->string (syntax-e #'nm))
"/"
(symbol->string (syntax-e id))))
id id))
(syntax->list #'(id ...)))])
(syntax/loc stx (combine-in id* ...)))]))))]))
(define-requirer rep)
(define-requirer infer)
(define-requirer typecheck)
(define-requirer utils)
(define-requirer env)
(define-requirer private)
(define-sequence-syntax in-syntax
(lambda () #'syntax->list)
(lambda (stx)
(syntax-case stx ()
[[ids (_ arg)]
#'[ids (in-list (syntax->list arg))]])))
(define-syntax debug
(syntax-rules ()
[(_ (f . args))
(begin (printf "starting ~a~n" 'f)
(let ([l (list . args)])
(printf "arguments are:~n")
(for/list ([arg 'args]
[val l])
(printf "\t~a: ~a~n" arg val))
(let ([e (apply f l)])
(printf "result was ~a~n" e)
e)))]
[(_ . args)
(begin (printf "starting ~a~n" 'args)
(let ([e args])
(printf "result was ~a~n" e)
e))]))
(define-syntax (with-syntax* stx)
(syntax-case stx ()
[(_ (cl) body ...) #'(with-syntax (cl) body ...)]
[(_ (cl cls ...) body ...)
#'(with-syntax (cl) (with-syntax* (cls ...) body ...))]
))
(define (filter-multiple l . fs)
(apply values
(map (lambda (f) (filter f l)) fs)))
(define (syntax-map f stxl)
(map f (syntax->list stxl)))
(define-syntax reverse-begin
(syntax-rules () [(_ h . forms) (begin0 (begin . forms) h)]))
#;
(define-syntax define-simple-syntax
(syntax-rules ()
[(dss (n . pattern) template)
(define-syntax n (syntax-rules () [(n . pattern) template]))]))
(define log-file (make-parameter #f))
(define-for-syntax logging? #f)
(require (only-in mzlib/file file-name-from-path))
(define-syntax (printf/log stx)
(if logging?
(syntax-case stx ()
[(_ fmt . args)
#'(when (log-file)
(fprintf (log-file) (string-append "~a: " fmt)
(file-name-from-path (object-name (log-file)))
. args))])
#'(void)))
(define (log-file-name src module-name)
(if (path? src)
(path-replace-suffix src ".log")
(format "~a.log" module-name)))
(define-syntax (with-logging-to-file stx)
(syntax-case stx ()
[(_ file . body)
(if logging?
#'(parameterize ([log-file (open-output-file file #:exists 'append)])
. body)
#'(begin . body))]))
(define-for-syntax timing? #f)
(define last-time (make-parameter #f))
(define-syntaxes (start-timing do-time)
(if timing?
(values
(syntax-rules ()
[(_ msg)
(begin
(when (last-time)
(error #f "Timing already started"))
(last-time (current-process-milliseconds))
(printf "Starting ~a at ~a~n" msg (last-time)))])
(syntax-rules ()
[(_ msg)
(begin
(unless (last-time)
(start-timing msg))
(let* ([t (current-process-milliseconds)]
[old (last-time)]
[diff (- t old)])
(last-time t)
(printf "Timing ~a at ~a@~a~n" msg diff t)))]))
(values (lambda _ #'(void)) (lambda _ #'(void)))))
(define (symbol-append . args)
(string->symbol (apply string-append (map symbol->string args))))
(define-match-expander
==
(lambda (stx)
(syntax-case stx ()
[(_ val)
#'(? (lambda (x) (equal? val x)))])))
(define-for-syntax printing? #t)
(define print-type* (box (lambda _ (error "print-type* not yet defined"))))
(define print-effect* (box (lambda _ (error "print-effect* not yet defined"))))
(define-syntax (define-struct/printer stx)
(syntax-case stx ()
[(form name (flds ...) printer)
#`(define-struct/properties name (flds ...)
#,(if printing? #'([prop:custom-write printer]) #'())
#f)]))
(define (id kw . args)
(define (f v)
(cond [(string? v) v]
[(symbol? v) (symbol->string v)]
[(identifier? v) (symbol->string (syntax-e v))]))
(datum->syntax kw (string->symbol (apply string-append (map f args)))))
;; map map (key val val -> val) -> map
(define (hash-union h1 h2 f)
(for/fold ([h* h1])
([(k v2) h2])
(let* ([v1 (hash-ref h1 k #f)]
[new-val (if v1
(f k v1 v2)
v2)])
(hash-set h* k new-val))))
(define (in-pairs seq)
(make-do-sequence
(lambda ()
(let-values ([(more? gen) (sequence-generate seq)])
(values (lambda (e) (let ([e (gen)]) (values (car e) (cdr e))))
(lambda (_) #t)
#t
(lambda (_) (more?))
(lambda _ #t)
(lambda _ #t))))))
(define (in-list-forever seq val)
(make-do-sequence
(lambda ()
(let-values ([(more? gen) (sequence-generate seq)])
(values (lambda (e) (let ([e (if (more?) (gen) val)]) e))
(lambda (_) #t)
#t
(lambda (_) #t)
(lambda _ #t)
(lambda _ #t))))))
;; Listof[A] Listof[B] B -> Listof[B]
;; pads out t to be as long as s
(define (extend s t extra)
(append t (build-list (- (length s) (length t)) (lambda _ extra))))