Add Typed Scheme as a collection.

svn: r8864
This commit is contained in:
Sam Tobin-Hochstadt 2008-03-03 22:57:55 +00:00
parent 83398c1c1b
commit 0d54ed5e74
58 changed files with 7414 additions and 0 deletions

View File

@ -0,0 +1,4 @@
#lang setup/infotab
(define name "Typed Scheme")
(define scribblings '(("typed-scheme.scrbl")))

View File

@ -0,0 +1,9 @@
#lang s-exp "minimal.ss"
(providing (libs (except scheme/base require #%module-begin #%top-interaction with-handlers lambda #%app))
(basics #%module-begin
#%top-interaction
with-handlers
lambda
#%app)
(from scheme require))

View File

@ -0,0 +1,29 @@
#lang scheme/base
(provide #%module-begin provide require rename-in rename-out prefix-in only-in all-from-out except-out except-in
providing begin)
(require (for-syntax scheme/base))
(define-for-syntax ts-mod "../typed-scheme.ss")
(define-syntax (providing stx)
(syntax-case stx (libs from basics except)
[(form (libs (except lb ex ...) ...) (basics b ...) (from spec id ...) ...)
(datum->syntax
stx
(syntax->datum
(with-syntax ([(b* ...) (generate-temporaries #'(b ...))]
[ts ts-mod])
(syntax/loc
stx
(begin
(require (except-in ts b ...))
(require (only-in ts [b b*] ...))
(require (except-in lb ex ...) ...)
(require (only-in spec id ...) ...)
(provide id ...) ...
(provide (rename-out [b* b] ...))
(provide (all-from-out ts))
(provide (all-from-out lb) ...))))))]))

View File

@ -0,0 +1,15 @@
(module reader scheme/base
(require (prefix-in r: "../typed-reader.ss")
(only-in syntax/module-reader wrap-read-all))
(define (*read in)
(wrap-read-all 'typed-scheme/lang/main in r:read))
(define (*read-syntax src in)
(wrap-read-all 'typed-scheme/lang/main
in
(lambda (in)
(r:read-syntax src in))))
(provide (rename-out [*read read] [*read-syntax read-syntax])))

View File

@ -0,0 +1,570 @@
#lang scheme/base
(require (for-template (only-in (lib "list.ss") foldl)
scheme/base
'#%paramz
scheme/promise
string-constants/string-constant
#;'#%more-scheme
#;'#%qq-and-or
(lib "match-error.ss" "mzlib" "private" "match"))
)
(require
"extra-procs.ss"
scheme/promise
(except-in "type-rep.ss" make-arr)
(only-in scheme/list cons?)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"
string-constants/string-constant
(lib "match-error.ss" "mzlib" "private" "match")
"tc-structs.ss")
(require (for-syntax
scheme/base
"init-envs.ss"
(except-in "type-rep.ss" make-arr)
(only-in (lib "list.ss") foldl)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"
string-constants/string-constant
(lib "match-error.ss" "mzlib" "private" "match")
"tc-structs.ss"))
(define-for-syntax (initialize-others)
(d-s date
([second : N] [minute : N] [hour : N] [day : N] [month : N]
[year : N] [weekday : N] [year-day : N] [dst? : B] [time-zone-offset : N])
())
(d-s exn ([message : -String] [continuation-marks : Univ]) ())
(d-s (exn:fail exn) () (-String Univ))
(d-s (exn:fail:read exn:fail) ([srclocs : (-lst Univ)]) (-String Univ))
)
(provide (for-syntax initial-env initialize-others))
(define-for-syntax initial-env
(let ([make-lst make-Listof]
[make-lst/elements -pair])
(make-env
[string->sexpr (-> -String (-mu x (Un Sym -String N B (-lst x))))]
(car (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v a)]
[((make-lst (-v a))) (-v a)])))
[first (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v a)]
[((make-lst (-v a))) (-v a)]))]
[second (-poly (a b c)
(cl->
[((-pair a (-pair b c))) b]
[((-lst a)) a]))]
[third (-poly (a b c d)
(cl->
[((-pair a (-pair b (-pair c d)))) c]
[((-lst a)) a]))]
[fourth (-poly (a) ((-lst a) . -> . a))]
[fifth (-poly (a) ((-lst a) . -> . a))]
[sixth (-poly (a) ((-lst a) . -> . a))]
[rest (-poly (a) ((-lst a) . -> . (-lst a)))]
(cadr
(-poly (a b c)
(cl->
[((-pair a (-pair b c))) b]
[((-lst a)) a])))
(caddr (-poly (a) (-> (-lst a) a)))
(cadddr (-poly (a) (-> (-lst a) a)))
(cdr (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v b)]
[((make-lst (-v a))) (make-lst (-v a))])))
(cddr (make-Poly (list 'a) (-> (make-lst (-v a)) (make-lst (-v a)))))
(cdddr (make-Poly (list 'a) (-> (make-lst (-v a)) (make-lst (-v a)))))
(cons (-poly (a b)
(cl-> [(a (-lst a)) (-lst a)]
[(a b) (-pair a b)])))
[*cons (-poly (a b) (cl->
[(a b) (-pair a b)]
[(a (-lst a)) (-lst a)]))]
[*list? (make-pred-ty (-lst Univ))]
(null? (make-pred-ty (-val null)))
(eof-object? (make-pred-ty (-val eof)))
[null (-val null)]
(number? (make-pred-ty N))
(integer? (make-pred-ty -Integer))
(boolean? (make-pred-ty B))
(add1 (-> N N))
(sub1 (-> N N))
(eq? (-> Univ Univ B))
(eqv? (-> Univ Univ B))
(equal? (-> Univ Univ B))
(even? (-> N B))
[assert (-poly (a) (-> (*Un a (-val #f)) a))]
[gensym (cl-> [(Sym) Sym]
[() Sym])]
[string-append (->* null -String -String)]
[open-input-string (-> -String -Input-Port)]
[open-output-file
(cl->
[(-Pathlike) -Port]
[(-Pathlike Sym) -Port])]
[read (cl->
[(-Port) -Sexp]
[() -Sexp])]
[ormap (-poly (a b) ((-> a b) (-lst a) . -> . b))]
[andmap (-poly (a b) ((-> a b) (-lst a) . -> . b))]
[newline (cl-> [() -Void]
[(-Port) -Void])]
[not (-> Univ B)]
[floor (-> N N)]
[box (-poly (a) (a . -> . (make-Box a)))]
[unbox (-poly (a) ((make-Box a) . -> . a))]
[set-box! (-poly (a) ((make-Box a) a . -> . -Void))]
[box? (make-pred-ty (make-Box Univ))]
[cons? (make-pred-ty (-pair Univ Univ))]
[pair? (make-pred-ty (-pair Univ Univ)) #;(-poly (a b) (make-pred-ty (-pair a b)))]
[empty? (make-pred-ty (-val null))]
[empty (-val null)]
[string? (make-pred-ty -String)]
[string (->* '() -Char -String)]
[symbol? (make-pred-ty Sym)]
[list? (make-pred-ty (-lst Univ))]
[list (-poly (a) (->* '() a (-lst a)))]
[procedure? (make-pred-ty (make-Function (list (make-top-arr))))]
[map
(-poly (a b c d)
(cl-> [((-> a b) (-lst a)) (-lst b)]
[((-> a b c) (-lst a) (-lst b)) (-lst c)]
[((-> a b c d) (-lst a) (-lst b) (-lst c)) (-lst d)]))]
[for-each
(-poly (a b c)
(cl-> [((-> a b) (-lst a)) -Void]
[((-> a b c) (-lst a) (-lst b)) -Void]))]
[foldl (-poly (a b)
((a b . -> . b) b (make-lst a) . -> . b))]
[call-with-values (-poly (a b) (-> (-> a) (-> a b) b))]
(error
(make-Function (list
(make-arr null (Un))
(make-arr (list Sym -String) (Un) Univ)
(make-arr (list -String) (Un) Univ)
(make-arr (list Sym) (Un)))))
[namespace-variable-value
(cl->
[(Sym) Univ]
[(Sym B -Namespace (-> Univ)) Univ])]
(match:error (Univ . -> . (Un)))
(display
(cl->
[(Univ) -Void]
[(Univ -Port) -Void]))
[void (->* '() Univ -Void)]
[void? (make-pred-ty -Void)]
[printf (->* (list -String) Univ -Void)]
[fprintf (->* (list -Output-Port -String) Univ -Void)]
[format (->* (list -String) Univ -String)]
(fst (make-Poly (list 'a 'b) (-> (make-lst/elements (-v a) (-v b)) (-v a))))
(snd (make-Poly (list 'a 'b) (-> (make-lst/elements (-v a) (-v b)) (-v b))))
(= (->* (list N N) N B))
(>= (->* (list N N) N B))
(< (->* (list N N) N B))
(<= (->* (list N N) N B))
[> (->* (list N) N B)]
(zero? (N . -> . B))
(* (->* '() N N))
(/ (->* (list N) N N))
(+ (->* '() N N))
(- (->* (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) (N (N . -> . a) . -> . (make-Vector a)))]
[reverse (make-Poly '(a) (-> (make-lst (-v a)) (make-lst (-v a))))]
[append (-poly (a) (->* (list) (-lst a) (-lst a)))]
[length (make-Poly '(a) (-> (make-lst (-v a)) N))]
[memq (make-Poly (list 'a) (-> (-v a) (make-lst (-v a)) (-opt (make-lst (-v a)))))]
[memv (make-Poly (list 'a) (-> (-v a) (make-lst (-v a)) (-opt (make-lst (-v a)))))]
[member
(-poly (a) (a (-lst a) . -> . (-opt (-lst a))))]
[string<? (->* (list -String -String) -String B)]
[string>? (->* (list -String -String) -String B)]
[string=? (->* (list -String -String) -String B)]
[char=? (->* (list -Char -Char) -Char B)]
[string<=? (->* (list -String -String) -String B)]
[string>=? (->* (list -String -String) -String B)]
[string-ci<? (->* (list -String -String) -String B)]
[string-ci>? (->* (list -String -String) -String B)]
[string-ci=? (->* (list -String -String) -String B)]
[string-ci<=? (->* (list -String -String) -String B)]
[string-ci>=? (->* (list -String -String) -String B)]
[string-upcase (-> -String -String)]
[string-downcase (-> -String -String)]
[string-titlecase (-> -String -String)]
[string-foldcase (-> -String -String)]
[string-normalize-nfd (-> -String -String)]
[string-normalize-nfkd (-> -String -String)]
[string-normalize-nfc (-> -String -String)]
[string-normalize-nfkc (-> -String -String)]
[string-ref (-> -String N -Char)]
[substring (cl->*
(-> -String N -String)
(-> -String N N -String))]
[string->path (-> -String -Path)]
[file-exists? (-> -Pathlike B)]
[assq (-poly (a) (-> Univ (-lst (-pair Univ a)) a))]
[build-path ((list -Pathlike*) -Pathlike* . ->* . -Path)]
[string->number (-> -String (-opt N))]
[with-input-from-file
(-poly (a)
(cl->
[(-Pathlike (-> a)) a]
[(-Pathlike (-> a) Sym) a]))]
[with-output-to-file
(-poly (a)
(cl->
[(-Pathlike (-> a)) a]
[(-Pathlike (-> a) Sym) a]))]
[random (cl->
[(N) N]
[() N])]
[assoc (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[list-ref (-poly (a) ((-lst a) N . -> . a))]
[positive? (-> N B)]
[negative? (-> N B)]
[odd? (-> N B)]
[even? (-> N B)]
[apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
[quotient (N N . -> . N)]
[remainder (N N . -> . N)]
[quotient/remainder (N N . -> . (-values (list N N)))]
;; parameter stuff
[parameterization-key Sym]
[extend-parameterization (-poly (a b) (-> Univ (-Param a b) a Univ))]
[continuation-mark-set-first (-> (-opt -Cont-Mark-Set) Univ Univ)]
[make-parameter (-poly (a b) (cl-> [(a) (-Param a a)]
[(b (a . -> . b)) (-Param a b)]))]
[current-directory (-Param -Pathlike -Path)]
[current-namespace (-Param -Namespace -Namespace)]
[print-struct (-Param B B)]
[read-decimal-as-inexact (-Param B B)]
[current-command-line-arguments (-Param (make-Vector -String) (make-Vector -String))]
;; regexp stuff
[regexp-match
(cl->
[((*Un -String -Regexp) -String) (-opt (-lst (-opt -String)))]
[(-Pattern -String) (-opt (-lst (-opt (*Un -Bytes -String))))]
[(-Pattern -String N) (-opt (-lst (-opt (*Un -Bytes -String))))]
[(-Pattern -String N (-opt N)) (-opt (-lst (-opt (*Un -Bytes -String))))]
[(-Pattern -String N (-opt N) (-opt -Output-Port)) (-lst (-opt (*Un -Bytes -String)))]
[(-Pattern -String (-opt N) (-opt -Output-Port)) (-lst (-opt (*Un -Bytes -String)))]
[(-Pattern -String (-opt -Output-Port)) (-lst (-opt (*Un -Bytes -String)))]
[(-Pattern (*Un -Input-Port -Bytes)) (-opt (-lst (-opt -Bytes)))]
[(-Pattern (*Un -Input-Port -Bytes) N) (-opt (-lst (-opt -Bytes)))]
[(-Pattern (*Un -Input-Port -Bytes) N (-opt N)) (-opt (-lst (-opt -Bytes)))]
[(-Pattern (*Un -Input-Port -Bytes) (-opt N)) (-opt (-lst (-opt -Bytes)))]
[(-Pattern (*Un -Input-Port -Bytes) N (-opt N) (-opt -Output-Port)) (-lst (-opt -Bytes))])]
[number->string (N . -> . -String)]
[current-milliseconds (-> N)]
[modulo (N N . -> . N)]
;; errors
[raise-type-error
(cl->
[(Sym -String Univ) (Un)]
[(Sym -String N (-lst Univ)) (Un)])]
;; this is a hack
[match:error ((list) Univ . ->* . (Un))]
[vector-set! (-poly (a) (-> (make-Vector a) N a -Void))]
[vector->list (-poly (a) (-> (make-Vector a) (-lst a)))]
[list->vector (-poly (a) (-> (-lst a) (make-Vector a)))]
[exact? (N . -> . B)]
[inexact? (N . -> . B)]
[expt (N N . -> . N)]
[vector (-poly (a) (->* (list) a (make-Vector a)))]
[real? (Univ . -> . B)]
[real-part (N . -> . N)]
[imag-part (N . -> . N)]
[magnitude (N . -> . N)]
[angle (N . -> . N)]
[numerator (N . -> . N)]
[denominator (N . -> . N)]
[exact->inexact (N . -> . N)]
[inexact->exact (N . -> . N)]
[make-string
(cl->
[(N) -String]
[(N -Char) -String])]
[arithmetic-shift (N N . -> . N)]
[abs (N . -> . N)]
[substring (cl-> [(-String N) -String]
[(-String N N) -String])]
[string-length (-String . -> . N)]
[string-set! (-String N -Char . -> . -Void)]
[make-vector
(-poly (a)
(cl->
[(N) (make-Vector N)]
[(N a) (make-Vector a)]))]
[file-exists? (-Pathlike . -> . B)]
[string->symbol (-String . -> . Sym)]
[symbol->string (Sym . -> . -String)]
[vector-length (-poly (a) ((make-Vector a) . -> . N))]
[call-with-input-file (-poly (a)
(cl->
[(-String (-Port . -> . a)) a]
[(-String (-Port . -> . a) Sym) a]))]
[call-with-output-file (-poly (a)
(cl->
[(-String (-Port . -> . a)) a]
[(-String (-Port . -> . a) Sym) a]))]
[current-output-port (-Param -Output-Port -Output-Port)]
[current-error-port (-Param -Output-Port -Output-Port)]
[current-input-port (-Param -Input-Port -Input-Port)]
[round (N . -> . N)]
[seconds->date (N . -> . (make-Struct 'date #f (list N N N N N N N N B N) #f))]
[current-seconds (-> N)]
[sqrt (-> N N)]
[path->string (-> -Path -String)]
[link-exists? (-> -Pathlike B)]
[directory-exists? (-> -Pathlike B)]
[file-exists? (-> -Pathlike B)]
[directory-list (cl-> [() (-lst -Path)]
[(-Path) (-lst -Path)])]
[make-hash-table (let ([ht-opt (*Un (-val 'weak) (-val 'equal))])
(-poly (a b)
(cl-> [() (-HT a b)]
[(ht-opt) (-HT a b)]
[(ht-opt ht-opt) (-HT a b)])))]
[hash-table-put! (-poly (a b) ((-HT a b) a b . -> . -Void))]
[hash-table-map (-poly (a b c) ((-HT a b) (a b . -> . c) . -> . (-lst c)))]
[hash-table-get (-poly (a b c)
(cl->
(((-HT a b) a) b)
(((-HT a b) a (-> c)) (*Un b c))
(((-HT a b) a c) (*Un b c))))]
#;[hash-table-index (-poly (a b) ((-HT a b) a b . -> . -Void))]
[bytes (->* (list) N -Bytes)]
[bytes-ref (-> -Bytes N N)]
[bytes-append (->* (list -Bytes) -Bytes -Bytes)]
[subbytes (cl->
[(-Bytes N) -Bytes]
[(-Bytes N N) -Bytes])]
[bytes-length (-> -Bytes N)]
[open-input-file (-> -Pathlike -Input-Port)]
[close-input-port (-> -Input-Port -Void)]
[close-output-port (-> -Output-Port -Void)]
[read-line (cl->
[() -String]
[(-Input-Port) -String]
[(-Input-Port Sym) -String])]
[copy-file (-> -Pathlike -Pathlike -Void)]
[bytes->string/utf-8 (-> -Bytes -String)]
;; language
[(expand #'(this-language))
Sym
string-constants/string-constant]
;; make-promise
[(cadr (syntax->list (expand #'(delay 3))))
(-poly (a) (-> (-> a) (-Promise a)))
scheme/promise]
;; qq-append
[(cadr (syntax->list (expand #'`(,@'() 1))))
(-poly (a b)
(cl->*
(-> (-lst a) (-val '()) (-lst a))
(-> (-lst a) (-lst b) (-lst (*Un a b)))))]
[force (-poly (a) (-> (-Promise a) a))]
[bytes<? (->* (list -Bytes) -Bytes B)]
[regexp-replace*
(cl->*
(-Pattern (*Un -Bytes -String) (*Un -Bytes -String) . -> . -Bytes)
(-Pattern -String -String . -> . -String))]
[peek-char
(cl->*
[-> -Char]
[-Input-Port . -> . -Char]
[-Input-Port N . -> . -Char]
[N . -> . -Char])]
[peek-byte
(cl->*
[-> -Byte]
[-Input-Port . -> . -Byte]
[-Input-Port N . -> . -Byte]
[N . -> . -Byte])]
[make-pipe
(cl->*
[-> (-values (list -Input-Port -Output-Port))]
[N . -> . (-values (list -Input-Port -Output-Port))])]
[open-output-bytes
(cl->*
[-> -Output-Port]
[Univ . -> . -Output-Port])]
[get-output-bytes
(cl->*
[-Output-Port . -> . -Bytes]
[-Output-Port Univ . -> . -Bytes]
[-Output-Port Univ N . -> . -Bytes]
[-Output-Port Univ N N . -> . -Bytes]
[-Output-Port N . -> . -Bytes]
[-Output-Port N N . -> . -Bytes])]
#;[exn:fail? (-> Univ B)]
#;[exn:fail:read? (-> Univ B)]
[write (-> -Sexp -Void)]
[open-output-string (-> -Output-Port)]
;; FIXME - wrong
[get-output-string (-> -Output-Port -String)]
[make-directory (-> -Path -Void)]
[hash-table-for-each (-poly (a b c)
(-> (-HT a b) (-> a b c) -Void))]
[delete-file (-> -Pathlike -Void)]
[make-namespace (cl->* (-> -Namespace)
(-> (*Un (-val 'empty) (-val 'initial)) -Namespace))]
[eval (-> -Sexp Univ)]
[exit (-> (Un))]
;; syntax operations
[syntax-source (-poly (a) (-> (-Syntax a) Univ))]
[syntax-position (-poly (a) (-> (-Syntax a) (-opt N)))]
[datum->syntax (cl->*
(-> (-opt (-Syntax Univ)) Sym (-Syntax Sym))
(-> (-opt (-Syntax Univ)) Univ (-Syntax Univ)))]
[syntax->datum (-poly (a) (-> (-Syntax a) Univ))]
[syntax-e (-poly (a) (-> (-Syntax a) a))]
[syntax-original? (-poly (a) (-> (-Syntax a) B))]
[identifier? (make-pred-ty (-Syntax Sym))]
[syntax? (make-pred-ty (-Syntax Univ))]
[syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a))
(-> (-Syntax Univ) Univ Univ)))]
)))
(begin-for-syntax (initialize-type-env initial-env)
(initialize-others))
;; the initial type name environment - just the base types
(define-syntax (define-tname-env stx)
(syntax-case stx ()
[(_ var provider [nm ty] ...)
#`(begin
(define-syntax nm (lambda (stx) (raise-syntax-error 'type-check "type name used out of context" stx))) ...
(provide nm) ...
(define-syntax provider (lambda (stx) #'(begin (provide nm) ...)))
(provide provider)
(begin-for-syntax
(initialize-type-name-env
(list (list #'nm ty) ...))))]))
(define-syntax (define-other-types stx)
(syntax-case stx ()
[(_ provider requirer nm ...)
(with-syntax ([(nms ...) (generate-temporaries #'(nm ...))])
(let ([body-maker (lambda (stx)
(map (lambda (nm nms) (datum->syntax stx `(rename ,#'mod ,nm ,nms)))
(syntax->list #'(nm ...))
(syntax->list #'(nms ...))))])
#'(begin (define-syntax nms (lambda (stx) (raise-syntax-error 'type-check "type name used out of context" stx))) ...
(provide nms) ...
(define-syntax (requirer stx)
(syntax-case stx ()
[(_ mod)
(datum->syntax
stx
`(require . ,(map (lambda (nm* nms*) (datum->syntax stx `(rename ,#'mod ,nm* ,nms*)))
(list 'nm ...)
(list #'nms ...))))]))
(define-syntax provider (lambda (stx) #'(begin (provide (rename-out [nms nm])) ...)))
(provide provider requirer))))]))
;; the initial set of available type names
(define-tname-env initial-type-names provide-tnames
[Number N]
[Integer -Integer]
[Void -Void]
[Boolean B]
[Symbol Sym]
[String -String]
[Any Univ]
[Port -Port]
[Path -Path]
[Regexp -Regexp]
[PRegexp -PRegexp]
[Char -Char]
[Option (-poly (a) (-opt a))]
[List (-lst Univ)]
[Listof -Listof]
[Namespace -Namespace]
[Input-Port -Input-Port]
[Output-Port -Output-Port]
[Bytes -Bytes]
[EOF (-val eof)]
[Keyword -Keyword]
[HashTable (-poly (a b) (-HT a b))]
[Promise (-poly (a) (-Promise a))]
[Pair (-poly (a b) (-pair a b))]
[Box (-poly (a) (make-Box a))]
[Syntax Any-Syntax]
[Identifier Ident]
)
(define-other-types
provide-extra-tnames
require-extra-tnames
-> U mu Un All Opaque Vectorof
Parameter Tuple Class
)
(provide-extra-tnames)

View File

@ -0,0 +1,110 @@
#lang scheme/unit
(require (prefix-in 1: srfi/1)
syntax/kerncase
syntax/struct
syntax/stx
mzlib/etc
mzlib/plt-match
"type-contract.ss"
"signatures.ss"
"tc-structs.ss"
"type-utils.ss"
"utils.ss" ;; doesn't need tests
"type-rep.ss" ;; doesn't need tests
"unify.ss" ;; needs tests
"infer.ss"
"type-effect-convenience.ss" ;; maybe needs tests
"union.ss"
"subtype.ss" ;; has tests
"internal-forms.ss" ;; doesn't need tests
"planet-requires.ss" ;; doesn't need tests
"type-env.ss" ;; maybe needs tests
"parse-type.ss" ;; has tests
"tc-utils.ss" ;; doesn't need tests
"type-environments.ss" ;; doesn't need tests
"lexical-env.ss" ;; maybe needs tests
"type-annotation.ss" ;; has tests
"type-name-env.ss" ;; maybe needs tests
"init-envs.ss"
"effect-rep.ss"
"mutated-vars.ss")
(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 _ _ _) ...)) (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)])))
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)])))

View File

@ -0,0 +1,10 @@
#lang scheme/base
(provide (struct-out binding)
(struct-out def-binding)
(struct-out def-stx-binding))
(define-struct binding (name) #:inspector #f)
(define-struct (def-binding binding) (ty) #:inspector #f)
(define-struct (def-stx-binding binding) () #:inspector #f)

View File

@ -0,0 +1,22 @@
(module defstruct-unit mzscheme
(require (lib "struct.ss") (lib "unit.ss"))
(provide (all-defined))
(define-syntax defstructs/sig/unit
(syntax-rules (define-struct/properties)
[(_ signame unitname (imps ...)
def
(define-struct/properties nm1 (flds1 ...) props #f)
(define-struct/properties (nm par) (flds ...) () #f) ...)
(begin
(define-signature signame
((struct nm1 (flds1 ...))
(struct nm (flds ...)) ...))
(define-unit unitname
(import imps ...)
(export signame)
def
(define-struct/properties nm1 (flds1 ...) props #f)
(define-struct (nm par) (flds ...) #f) ...))]))
)

View File

@ -0,0 +1,39 @@
#lang scheme/base
(require (lib "plt-match.ss"))
(require (lib "etc.ss"))
(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

View File

@ -0,0 +1,9 @@
(module extra-procs mzscheme
(provide assert)
(define (assert v)
(unless v
(error "Assertion failed - value was #f"))
v)
)

View File

@ -0,0 +1,98 @@
#lang scheme/base
(require (for-syntax scheme/base)
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)
(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)
(values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant))))
(provide Covariant Contravariant Invariant Constant)
;; hashtables for keeping track of free variables and indexes
(define index-table (make-hash-table 'weak))
;; maps Type to List[Cons[Number,Variance]]
(define var-table (make-hash-table 'weak))
;; maps Type to List[Cons[Symbol,Variance]]
(define (free-idxs* t) (hash-table-get index-table t (lambda _ (error "type not in index-table" (syntax-e t)))))
(define (free-vars* t) (hash-table-get var-table t (lambda _ (error "type not in var-table" (syntax-e t)))))
(define empty-hash-table (make-immutable-hash-table 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-hash-table))
(define (combine-var v w)
(cond
[(eq? v w) v]
[(eq? v Constant) w]
[(eq? w Constant) v]
[else Invariant]))
(for-each
(lambda (old-ht)
(hash-table-for-each
old-ht
(lambda (sym var)
(let* ([sym-var (hash-table-get ht sym (lambda () #f))])
(if sym-var
(hash-table-put! ht sym (combine-var var sym-var))
(hash-table-put! ht sym var))))))
freess)
ht)
;; frees -> frees
(define (flip-variances vs)
(hash-table-map*
(lambda (k v)
(evcase
v
[Covariant Contravariant]
[Contravariant Covariant]
[v v]))
vs))
(define (make-invariant vs)
(hash-table-map*
(lambda (k v) Invariant)
vs))
(define (hash-table-map* f ht)
(define new-ht (hash-table-copy ht))
(hash-table-for-each
new-ht
(lambda (k v)
(hash-table-put!
new-ht
k
(f k v))))
new-ht)
(define (without-below n frees)
(define new-ht (hash-table-copy frees))
(hash-table-for-each
new-ht
(lambda (k v)
(when (< k n) (hash-table-remove! new-ht k))))
new-ht)
(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table)
(define-syntax (unless-in-table stx)
(syntax-case stx ()
[(_ table val . body)
(quasisyntax/loc stx
(hash-table-get table val #,(syntax/loc #'body (lambda () . body))))]))

View File

@ -0,0 +1,410 @@
#lang scheme/base
(require "unify.ss" "type-comparison.ss" "type-rep.ss" "effect-rep.ss" "subtype.ss"
"planet-requires.ss" "tc-utils.ss" "union.ss"
"resolve-type.ss"
"type-effect-convenience.ss"
(lib "trace.ss")
(lib "plt-match.ss")
(lib "list.ss"))
(require (galore))
(provide infer infer/list infer/list/vararg combine table:un exn:infer?)
;; exn representing failure of inference
;; s,t both types
#;
(define-struct (exn:infer exn:fail) (s t))
(define-values (fail-sym exn:infer?)
(let ([sym (gensym)])
(values sym (lambda (s) (eq? s sym)))))
;; inference failure - masked before it gets to the user program
(define-syntax fail!
(syntax-rules ()
[(_ s t) (raise fail-sym)
#;(raise (make-exn:infer "inference failed" (current-continuation-marks) s t))
#;(error "inference failed" s t)]))
;; conveneice function
(define (alist->mapping vars) (table:alist->eq (map (lambda (x) (cons x 'fail)) vars)))
;; flag is one of: 'co, 'contra, 'both, #f
;; Mapping is a table that maps symbols to Results
;; A Result is one of:
;; - 'fail (not yet filled in)
;; - #f (not a variable we're concerned with)
;; - (list flag type)
;;
;; s, t : Type
;; vars : Listof[Symbol]
;; produces a substitution for vars, or #f
;; the substitution makes s a supertype of t
;; only vars will be substituted, regardless of other free vars
(define ((mk-infer f) s t vars)
(let ([mapping (alist->mapping vars)])
(with-handlers
([exn:infer? (lambda _ #f)])
(mapping->subst (f s t mapping 'co)))))
;; table[symbol, (list flag type)] -> substitution
;; convert a mapping to a substitution
(define (mapping->subst x)
(define sexp (table:to-sexp x))
(define result (filter (lambda (x) (list? (cadr x))) sexp))
;(printf "sexp: ~a~n" sexp)
(map (lambda (x) (list (car x) (cadr (cadr x)))) result))
;(trace mapping->subst)
;; least upper bound of two flags
;; the lattice is like this:
;; 'both
;; / \
;; 'co 'contra
;; \ /
;; #f
(define (lub a b)
(match (list a b)
[(list x x) x]
[(list #f x) x]
[(list x #f) x]
[(list 'both x) 'both]
[(list x 'both) 'both]
[(list x y) 'both]))
;; combine: flag -> Result Result -> Result
;; combine two results into one
(define ((combine flag*) s t)
(define (type-lub s t)
(cond [(subtype s t) t]
[(subtype t s) s]
[else (Un s t)]))
(define (type-glb s t)
(cond [(subtype s t) s]
[(subtype t s) t]
[else (fail! s t)]))
(define (go flag s t)
(cond [(and (eq? flag 'both) (type-equal? s t)) s]
[(eq? flag 'both) (fail! s t)]
[(eq? flag 'co) (type-lub s t)]
[(eq? flag 'contra) (type-glb s t)]
[(eq? flag #f) (go flag* s t)]
[else (int-err "bad flag value ~a" flag)]))
(match (list s t)
[(list 'fail t) t]
[(list t 'fail) t]
[(list (list sf s) (list tf t))
(let* ([flag (lub flag* (lub sf tf))]
[new-ty (go flag s t)])
(list flag new-ty))]))
#;
;(printf "flags : ~a ~a~n" sf tf)
(cond
[(and sf tf (type-equal? s t)) (list (if (eq? sf tf) sf 'both) s)] ;; equal is fine
[(memq 'both (list sf tf)) (fail! s t)] ;; not equal, needed to be
[(and sf tf (not (eq? sf tf))) (fail! s t)] ;; not equal, needed to be
[else
(let ([flag (or sf tf flag)])
(printf "flag is ~a~n" flag)
(cond
[(eq? 'co flag) (list 'co (Un s t))]
[(and (eq? 'contra flag) (subtype s t)) (list 'contra s)]
[(and (eq? 'contra flag) (subtype t s)) (list 'contra t)]
[else (fail! s t)]))])
;(trace combine)
;; combine two tables
;; table:un : flag -> Mapping Mapping -> Mapping
(define ((table:un flag) a b) (table:union/value a b (combine flag)))
;; infer/int/union : Listof[Type] Listof[Type] Mapping Flag -> Mapping
;; ss and ts represent unions of types
(define (infer/int/union ss ts mapping flag)
(unless (= (length ss) (length ts))
(fail! ss ts))
;; first, we remove common elements of ss and ts
(let-values ([(ss* ts*)
(values (filter (lambda (se) (not (memq se ts))) ss)
(filter (lambda (te) (not (memq te ss))) ts))])
;; we need to try all the pairwise possibilites
(let ([l (map (lambda (x y) (infer/int x y mapping flag)) ss* ts*)])
(foldl (table:un flag) (table:make-eq) l))))
;; infer/int/list : Listof[Type] Listof[Type] Mapping Flag -> Mapping
(define (infer/int/list ss ts mapping flag)
(unless (= (length ss) (length ts))
(fail! ss ts))
(let ([l (map (lambda (x y) (infer/int x y mapping flag)) ss ts)])
(foldl (table:un flag) (table:make-eq) l)))
;; infer/int/list/eff : Listof[Effect] Listof[Effect] Mapping Flag -> Mapping
(define (infer/int/list/eff ss ts mapping flag)
(cond [(or (null? ss) (null? ts)) mapping]
[(not (= (length ss) (length ts)))
;(error 'bad "~a ~a" ss ts)
(fail! ss ts)]
[else (let ([l (map (lambda (x y) (infer/int/eff x y mapping flag)) ss ts)])
(foldl (table:un flag) (table:make-eq) l))]))
;; infer/int/list/vararg : Listof[Type] Type Listof[Type] Mapping Flag Boolean -> Mapping
(define (infer/int/list/vararg ss rest ts mapping flag [direction #t])
(unless (<= (length ss) (length ts))
(printf "failing!~n")
(fail! ss ts))
(let loop-types
([ss ss]
[ts ts]
[tbl mapping])
(define (ii a b)
(if direction
(infer/int a b tbl flag)
(infer/int b a tbl flag)))
(cond [(null? ts) tbl]
[(and rest (null? ss))
(let ([tbl* (ii rest (car ts))])
(loop-types ss (cdr ts) tbl*))]
[else
(let ([tbl* (ii (car ss) (car ts))])
(loop-types (cdr ss) (cdr ts) tbl*))])))
(define (infer/list/vararg ss rest ts vars)
(let ([mapping (alist->mapping vars)])
(with-handlers
([exn:infer? (lambda _ #f)])
(mapping->subst (infer/int/list/vararg ss rest ts mapping 'co)))))
;; Flag -> Flag
(define (swap flag) (case flag
[(co) 'contra]
[(contra) 'co]
[(both) 'both]
[(start) 'start]
[else (int-err "bad flag: ~a" flag)]))
(define (co? x) (eq? x 'co))
(define (contra? x) (eq? x 'contra))
(define (infer/int/eff s t mapping flag)
(let ([fail! (case-lambda [() (fail! s t)]
[(s t) (fail! s t)])])
(parameterize ([match-equality-test type-equal?])
(match (list s t)
[(list t t) mapping]
[(list (Latent-Restrict-Effect: t1) (Latent-Restrict-Effect: t2)) (infer/int t1 t2 mapping flag)]
[(list (Latent-Remove-Effect: t1) (Latent-Remove-Effect: t2)) (infer/int t1 t2 mapping flag)]
))))
;(trace fail!)
;; type type mapping -> mapping
(define (infer/int s t mapping flag)
(let ([fail! (case-lambda [() (fail! s t)]
[(s t) (fail! s t)])])
(define (i/i s t) (infer/int s t mapping flag))
(parameterize ([match-equality-test type-equal?])
(match (list s t)
[(list t t) mapping]
[(list (F: v) t)
(let ([cur (table:lookup v mapping)])
(match cur
;; we haven't yet seen this variable
['fail
(cond [(and (eq? flag 'contra) (type-equal? Univ t)) mapping]
[(and (eq? flag 'co) (type-equal? (Un) t)) mapping]
[else
(table:insert v (list #f t) mapping)])]
;; we are ignoring this variable, but they weren't the same
[#f (fail!)]
;; this variable has already been unified
[(list cur-flag cur-t)
(cond
[(or (not cur-flag) (eq? flag cur-flag))
;; this variable has only been handled once, or
;; we're still going in the correct direction
(cond
;; this is the same type we've already seen, so don't change the flag
[(type-equal? cur-t t) mapping]
;; this is a supertype of what's been found before
[(and (eq? flag 'co) (subtype cur-t t))
(table:insert v (list flag t) mapping)]
;; this is a subtype of what's been found before
[(and (eq? flag 'co) (subtype t cur-t))
(table:insert v (list flag cur-t) mapping)]
[(eq? flag 'co)
(table:insert v (list flag (Un t cur-t)) mapping)]
;; this is a subtype of what we found before
[(and (eq? flag 'contra) (subtype t cur-t))
(table:insert v (list flag t) mapping)]
;; this is a supertype of what we found before
[(and (eq? flag 'contra) (subtype t cur-t))
(table:insert v (list flag cur-t) mapping)]
[(and (eq? flag 'both) (subtype t cur-t) (subtype cur-t t))
mapping]
[(eq? flag 'both)
(fail! cur-t t)]
;; impossible
[else (int-err "bad flag value: ~a" flag)])]
;; we've switched directions at least once
[(type-equal? cur-t t)
;; we're still ok
(table:insert (list 'both cur-t) mapping)]
[else
;; we're not ok
(fail! cur-t t)])]))]
;; names are compared for equality
[(list (Name: n) (Name: n*))
(if (free-identifier=? n n*)
mapping
(fail!))]
;; type application
[(list (App: (Name: n) args _)
(App: (Name: n*) args* _))
(unless (free-identifier=? n n*)
(fail!))
(infer/int/list args args* mapping flag)]
;; vectors and boxes just recur, but are invariant
[(list (Vector: s) (Vector: t)) (infer/int s t mapping 'both)]
[(list (Box: s) (Box: t)) (infer/int s t mapping 'both)]
;; pairs just recur
[(list (Pair: s1 s2) (Pair: t1 t2))
(infer/int/list (list s1 s2) (list t1 t2) mapping flag)]
;; ht just recur
[(list (Hashtable: s1 s2) (Hashtable: t1 t2))
(infer/int/list (list s1 s2) (list t1 t2) mapping 'both)]
[(list (Syntax: s1) (Syntax: s2))
(infer/int s1 s2 mapping flag)]
;; structs just recur
[(list (Struct: nm p flds proc) (Struct: nm p flds* proc*))
(cond [(and proc proc*)
(infer/int/list (cons proc flds) (cons proc* flds*) mapping flag)]
[(or proc proc*)
(fail!)]
[else (infer/int/list flds flds* mapping flag)])]
;; parameters just recur
[(list (Param: in1 out1) (Param: in2 out2))
(infer/int/list (list in1 out1) (list in2 out2) mapping flag)]
;; if we have two mu's, we rename them to have the same variable
;; and then compare the bodies
[(list (Mu-unsafe: s) (Mu-unsafe: t))
(infer/int s t mapping flag)]
;; other mu's just get unfolded
[(list s (? Mu? t)) (infer/int s (unfold t) mapping flag)]
[(list (? Mu? s) t) (infer/int (unfold s) t mapping flag)]
;; two unions with the same number of elements, so we just try to unify them pairwise
[(list (Union: l1) (Union: l2))
(=> unmatch)
(unless (= (length l1) (length l2))
(unmatch))
(infer/int/union l1 l2 mapping flag)]
;; new impl for functions
[(list (Function: (list t-arr ...))
(Function: (list s-arr ...)))
(=> unmatch)
(let loop ([t-arr t-arr] [s-arr s-arr] [mapping mapping])
(define (U a b) ((table:un flag) a b))
(define (unmatch!) (unmatch))
(cond [(and (null? t-arr) (null? s-arr)) mapping]
[(or (null? t-arr) (null? s-arr)) (unmatch!)]
[else (match (list (car t-arr) (car s-arr))
[(list (arr: ts t t-rest t-thn-eff t-els-eff) (arr: ss s s-rest s-thn-eff s-els-eff))
(let ([arg-mapping
(cond [(and t-rest s-rest (= (length ts) (length ss)))
(infer/int/list (cons t-rest ts) (cons s-rest ss) mapping (swap flag))]
[(and (not t-rest) (not s-rest) (= (length ts) (length ss)))
(infer/int/list ts ss mapping (swap flag))]
[(and t-rest (not s-rest) (<= (length ts) (length ss)))
(infer/int/list/vararg ts t-rest ss mapping (swap flag) #t)]
[(and s-rest (not t-rest) (>= (length ts) (length ss)))
(infer/int/list/vararg ss s-rest ts mapping (swap flag) #f)]
[else (unmatch!)])]
[ret-mapping (infer/int t s mapping flag)]
[thn-mapping (infer/int/list/eff t-thn-eff s-thn-eff mapping flag)]
[els-mapping (infer/int/list/eff t-els-eff s-els-eff mapping flag)])
(loop (cdr t-arr) (cdr s-arr)
(U mapping (U (U arg-mapping ret-mapping) (U thn-mapping els-mapping)))))])]))]
;; arrow types - just add a whole bunch of new constraints
[(list (Function: (list (arr: ts t t-rest t-thn-eff t-els-eff) ...))
(Function: (list (arr: ss s s-rest s-thn-eff s-els-eff) ...)))
(=> unmatch)
(define (compatible-rest t-rest s-rest)
(andmap (lambda (x y) (or (and x y) (and (not x) (not y)))) ;; either both #f or both not #f
t-rest s-rest))
(define (U a b) ((table:un flag) a b))
(let-values ([(s-thn-eff s-els-eff) (if (and (null? (car t-thn-eff)) (null? (cdr t-thn-eff))
(null? (car t-els-eff)) (null? (cdr t-els-eff)))
(values (list null) (list null))
(values s-thn-eff s-els-eff))])
(unless (and (= (length ts) (length ss))
(= (length t-thn-eff) (length s-thn-eff))
(= (length t-els-eff) (length s-els-eff))
(compatible-rest t-rest s-rest))
(unmatch))
(let ([arg-mapping (infer/int/list (apply append ts) (apply append ss) mapping (swap flag))]
[ret-mapping (infer/int/list t s mapping flag)]
[thn-mapping (infer/int/list/eff (apply append t-thn-eff) (apply append s-thn-eff) mapping flag)]
[els-mapping (infer/int/list/eff (apply append t-els-eff) (apply append s-els-eff) mapping flag)])
(U (U arg-mapping ret-mapping) (U thn-mapping els-mapping))))]
;; here, we try to handle a case-lambda as the argument to a polymorphic function
[(list (Function: ftys) (and t (Function: (list (arr: ss s s-rest s-thn-eff s-els-eff)))))
(=> unmatch)
(when (= 1 (length ftys)) (unmatch)) ;; we should have handled this case already
(or
(ormap
(lambda (fty)
(with-handlers
([exn:infer? (lambda _ #f)])
(infer/int (make-Function (list fty)) t mapping flag)))
ftys)
(fail!))]
[(list (and t (Function: (list (arr: ss s s-rest s-thn-eff s-els-eff)))) (Function: ftys))
(=> unmatch)
(when (= 1 (length ftys)) (unmatch)) ;; we should have handled this case already
(or
(ormap
(lambda (fty)
(with-handlers
([exn:infer? (lambda _ #f)])
(infer/int t (make-Function (list fty)) mapping flag)))
ftys)
(fail!))]
;; if t is a union, all of the elements have to match
[(list s (Union: e1))
(infer/int/list (map (lambda (_) s) e1) e1 mapping flag)]
;; if s is a union, we can just try to find one of its elements that works
[(list (Union: e1) t)
(or
(ormap
(lambda (e)
(with-handlers
([exn:infer? (lambda _ #f)])
(infer/int e t mapping flag)))
e1)
(fail!))]
;; otherwise, if we have a {sub,super}type, we're all good
[else (cond [(and (co? flag) (subtype t s)) mapping]
[(and (contra? flag) (subtype s t)) mapping]
;; or, nothing worked, and we fail
[else (fail!)])]
))))
;; infer: Type Type List[Symbol] -> Substitution
(define infer (mk-infer infer/int))
;; infer/list: Listof[Type] Listof[Type] List[Symbol] -> Substitution
(define infer/list (mk-infer infer/int/list))
;(trace infer infer/int/list infer/int infer/list)

View File

@ -0,0 +1,78 @@
(module init-envs mzscheme
(provide (all-defined))
(require "type-env.ss" "type-rep.ss" "type-name-env.ss" "union.ss" "effect-rep.ss" (lib "shared.ss")
"type-effect-convenience.ss" "type-alias-env.ss"
"type-alias-env.ss")
(require (lib "pconvert.ss") (lib "plt-match.ss") (lib "list.ss"))
(require-for-template (lib "pconvert.ss"))
(require-for-template (lib "shared.ss"))
(require-for-template mzscheme "type-rep.ss" "union.ss" "effect-rep.ss" (lib "shared.ss"))
(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))]
[(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))]
[(? 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-object #'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-object #'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-object #'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)))))
)

View File

@ -0,0 +1,15 @@
(module internal-forms mzscheme
(define-syntax internal-forms
(syntax-rules ()
[(_ 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)
)

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-table #;'weak 'equal)) 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-table-get table key
(lambda ()
(let ([new (make-name (count!) arg ...)])
(hash-table-put! 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))))

View File

@ -0,0 +1,51 @@
(module lexical-env mzscheme
(require "type-environments.ss" "tc-utils.ss" "type-env.ss" "mutated-vars.ss")
(provide (all-defined))
;; the current lexical environment
(define lexical-env (make-parameter (make-empty-env module-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))))
;; 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)]))
)

View File

@ -0,0 +1,52 @@
(module mutated-vars mzscheme
(require-for-template mzscheme)
(require (lib "boundmap.ss" "syntax")
(lib "kerncase.ss" "syntax")
(lib "trace.ss"))
;; mapping telling whether an identifer is mutated
;; maps id -> boolean
(define table (make-module-identifier-mapping))
;; find and add to mapping all the set!'ed variables in form
;; syntax -> void
(define (find-mutated-vars form)
;; syntax -> void
(define (fmv/list lstx)
(for-each find-mutated-vars (syntax->list lstx)))
;(printf "called with ~a~n" (syntax-object->datum form))
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal require/typed-internal #%app lambda)
;; 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)]
[(#%app . rest) (fmv/list #'rest)]
[(begin . rest) (fmv/list #'rest)]
[(begin0 . rest) (fmv/list #'rest)]
[(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))]
[(let-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
(fmv/list #'b))]
[(letrec-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
(fmv/list #'b))]
;; all the other forms don't have any expression subforms (like #%top)
[_ (void)]))
;(trace find-mutated-vars)
;; checks to see if a particular variable is ever set!'d
;; is-var-mutated? : identifier -> boolean
(define (is-var-mutated? id) (module-identifier-mapping-get table id (lambda _ #f)))
(provide find-mutated-vars is-var-mutated?)
)

View File

@ -0,0 +1,10 @@
#lang scheme/base
(provide nest)
(define-syntax nest
(syntax-rules ()
[(nest () body0 body ...)
(let () body0 body ...)]
[(nest ([form forms ...] . more) body0 body ...)
(form forms ... (nest more body0 body ...))]))

View File

@ -0,0 +1,210 @@
#lang scheme/base
(provide parse-type parse-type/id)
(require (except-in "type-rep.ss" make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"tc-utils.ss"
"union.ss"
(lib "stx.ss" "syntax")
(except-in "type-environments.ss")
"type-name-env.ss"
"type-alias-env.ss"
"type-utils.ss"
(only-in (lib "list.ss") foldl foldr)
#;(except-in (lib "list.ss" "srfi" "1") unfold remove)
(lib "plt-match.ss"))
(define enable-mu-parsing (make-parameter #t))
(define (parse-type/id loc datum)
#;(printf "parse-type/id id : ~a~n ty: ~a~n" (syntax-object->datum loc) (syntax-object->datum stx))
(let* ([stx* (datum->syntax loc datum loc loc)])
(parse-type stx*)))
(define (stx-cadr stx) (stx-car (stx-cdr stx)))
(define (parse-type stx)
(parameterize ([current-orig-stx stx])
(syntax-case* stx ()
symbolic-identifier=?
[(fst . rst)
(not (syntax->list #'rst))
(-pair (parse-type #'fst) (parse-type #'rst))]
[(Class (pos-args ...) ([fname fty . rest] ...) ([mname mty] ...))
(eq? (syntax-e #'Class) 'Class)
(make-Class
(map parse-type (syntax->list #'(pos-args ...)))
(map list
(map syntax-e (syntax->list #'(fname ...)))
(map parse-type (syntax->list #'(fty ...)))
(map (lambda (e) (syntax-case e ()
[(#t) #t]
[_ #f]))
(syntax->list #'(rest ...))))
(map list
(map syntax-e (syntax->list #'(mname ...)))
(map parse-type (syntax->list #'(mty ...)))))]
[(Instance t)
(eq? (syntax-e #'Instance) 'Instance)
(let ([v (parse-type #'t)])
(unless (or (Mu? v) (Class? v) (Union? v))
(tc-error "Argument to Instance must be a class type, got ~a" v))
(make-Instance v))]
[(Tuple ts ...)
(or (eq? (syntax-e #'Tuple) 'Tuple)
(eq? (syntax-e #'Tuple) 'List))
(begin
(add-type-name-reference (stx-car stx))
(-Tuple (map parse-type (syntax->list #'(ts ...)))))]
[(cons fst rst)
(eq? (syntax-e #'cons) 'cons)
(-pair (parse-type #'fst) (parse-type #'rst))]
[(pred t)
(eq? (syntax-e #'pred) 'pred)
(make-pred-ty (parse-type #'t))]
[(dom -> rng : pred-ty)
(and
(eq? (syntax-e #'->) '->)
(eq? (syntax-e #':) ':))
(begin
(add-type-name-reference (stx-cadr stx))
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty)))]
[(dom ... rest ::: -> rng)
(and (eq? (syntax-e #'->) '->)
(or (symbolic-identifier=? #'::: (quote-syntax ..))
(symbolic-identifier=? #'::: (quote-syntax ...))))
(begin
(add-type-name-reference #'->)
(->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng)))]
;; has to be below the previous one
[(dom ... -> rng)
(eq? (syntax-e #'->) '->)
(begin
(add-type-name-reference #'->)
(->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rng)))]
[(values tys ...)
(eq? (syntax-e #'values) 'values)
(-values (map parse-type (syntax->list #'(tys ...))))]
[(case-lambda tys ...)
(eq? (syntax-e #'case-lambda) 'case-lambda)
(make-Function (map (lambda (ty)
(syntax-case* ty (->) symbolic-identifier=?
[(dom ... -> rng)
(make-arr
(map parse-type (syntax->list #'(dom ...)))
(parse-type #'rng))]))
(syntax->list #'(tys ...))))]
;; I wish I could write this
#;[(case-lambda ([dom ... -> rng] ...)) (make-funty (list (make-arr (list (parse-type #'dom) ...) (parse-type #'rng)) ...))]
#;[(list-of t) (make-lst (parse-type #'t))]
#;[(Listof t) (make-lst (parse-type #'t))]
[(Vectorof t)
(eq? (syntax-e #'Vectorof) 'Vectorof)
(begin
(add-type-name-reference #'Vectorof)
(make-Vector (parse-type #'t)))]
[(mu x t)
(and (identifier? #'x)
(memq (syntax-e #'mu) '(mu Rec))
(enable-mu-parsing))
(let* ([var (syntax-e #'x)]
[tvar (make-F var)])
(add-type-name-reference #'mu)
(parameterize ([current-tvars (extend-env (list var) (list tvar) (current-tvars))])
(make-Mu var (parse-type #'t))))]
[(U ts ...)
(eq? (syntax-e #'U) 'U)
(begin
(add-type-name-reference #'U)
(apply Un (map parse-type (syntax->list #'(ts ...)))))]
[(Un-pat ts ...)
(eq? (syntax-e #'Un-pat) 'Un)
(apply Un (map parse-type (syntax->list #'(ts ...))))]
[(quot t)
(eq? (syntax-e #'quot) 'quote)
(-val (syntax-e #'t))]
[(All (vars ...) t)
(and (eq? (syntax-e #'All) 'All)
(andmap identifier? (syntax->list #'(vars ...))))
(let* ([vars (map syntax-e (syntax->list #'(vars ...)))]
[tvars (map make-F vars)])
(add-type-name-reference #'All)
(parameterize ([current-tvars (extend-env vars tvars (current-tvars))])
(make-Poly vars (parse-type #'t))))]
[(Opaque p?)
(eq? (syntax-e #'Opaque) 'Opaque)
(begin
(add-type-name-reference #'Opaque)
(make-Opaque #'p? (syntax-local-certifier)))]
[(Parameter t)
(eq? (syntax-e #'Parameter) 'Parameter)
(let ([ty (parse-type #'t)])
(add-type-name-reference #'Parameter)
(-Param ty ty))]
[(Parameter t1 t2)
(eq? (syntax-e #'Parameter) 'Parameter)
(begin
(add-type-name-reference #'Parameter)
(-Param (parse-type #'t1) (parse-type #'t2)))]
[id
(identifier? #'id)
(cond
;; if it's a type variable, we just produce the corresponding reference (which is in the HT)
[(lookup (current-tvars) (syntax-e #'id) (lambda (_) #f))]
;; if it's a type alias, we expand it (the expanded type is stored in the HT)
[(lookup-type-alias #'id parse-type (lambda () #f))
=>
(lambda (t)
(add-type-name-reference #'id)
t)]
;; if it's a type name, we just use the name
[(lookup-type-name #'id (lambda () #f))
(add-type-name-reference #'id)
(make-Name #'id)]
[else
(tc-error "unbound type ~a" (syntax-e #'id))])]
[(All . rest) (eq? (syntax-e #'All) 'All) (tc-error "All: bad syntax")]
[(Opaque . rest) (eq? (syntax-e #'Opaque) 'Opqaue) (tc-error "Opaque: bad syntax")]
[(U . rest) (eq? (syntax-e #'U) 'U) (tc-error "Union: bad syntax")]
[(Vectorof . rest) (eq? (syntax-e #'Vectorof) 'Vectorof) (tc-error "Vectorof: bad syntax")]
[(mu . rest) (eq? (syntax-e #'mu) 'mu) (tc-error "mu: bad syntax")]
[(Un . rest) (eq? (syntax-e #'Un) 'Un) (tc-error "Union: bad syntax")]
[(t ... -> . rest) (eq? (syntax-e #'->) '->) (tc-error "->: bad syntax")]
[(id arg args ...)
(let loop
([rator (parse-type #'id)]
[args (map parse-type (syntax->list #'(arg args ...)))])
(match rator
[(Name: _)
(make-App rator args stx)]
[(Poly: ns _)
(unless (= (length args) (length ns))
(tc-error "Wrong number of arguments to type ~a, expected ~a but got ~a" rator (length ns) (length args)))
(instantiate-poly rator args)]
[(Mu: _ _) (loop (unfold rator) args)]
[_ (tc-error "Type ~a cannot be applied, arguments were: ~a" rator args)]))
#;
(let ([ty (parse-type #'id)])
#;(printf "ty is ~a" ty)
(unless (Poly? ty)
(tc-error "not a polymorphic type: ~a" (syntax-e #'id)))
(unless (= (length (syntax->list #'(arg args ...))) (Poly-n ty))
(tc-error "wrong number of arguments to type constructor ~a: expected ~a, got ~a"
(syntax-e #'id)
(Poly-n ty)
(length (syntax->list #'(arg args ...)))))
(instantiate-poly ty (map parse-type (syntax->list #'(arg args ...)))))]
[t
(or (boolean? (syntax-e #'t)) (number? (syntax-e #'t))
(string? (syntax-e #'t)))
(-val (syntax-e #'t))]
[_ (tc-error "not a valid type: ~a" (syntax->datum stx))])))

View File

@ -0,0 +1,49 @@
#lang scheme/base
(require (for-syntax scheme/base scheme/require-transform))
(define-for-syntax (splice-requires specs)
(define subs (map (compose cons expand-import) specs))
(values (apply append (map car subs)) (apply append (map cdr subs))))
(define-syntax define-module
(lambda (stx)
(syntax-case stx ()
[(_ nm spec ...)
(syntax/loc stx
(define-syntax nm
(make-require-transformer
(lambda (stx)
(splice-requires (list (syntax-local-introduce (quote-syntax spec)) ...))))))])))
(define-syntax planet/multiple
(make-require-transformer
(lambda (stx)
(syntax-case stx ()
[(_ plt files ...)
(let ([mk (lambda (spc)
(syntax-case spc (prefix-in)
[e
(string? (syntax-e #'e))
(datum->syntax spc `(planet ,#'e ,#'plt) spc)]
[(prefix-in p e)
(datum->syntax spc `(prefix-in ,#'p (planet ,#'e ,#'plt)) spc)]))])
(splice-requires (map mk (syntax->list #'(files ...)))))]))))
(provide galore schemeunit)
;; why is this neccessary?
(provide planet/multiple)
(define-module galore
(prefix-in table: "tables.ss"))
(define-module schemeunit
(planet/multiple ("schematics" "schemeunit.plt" 2 3)
"test.ss"
"graphical-ui.ss"
"text-ui.ss"
"util.ss")
(planet/multiple ("cce" "fasttest.plt" 1 2)
"random.ss"
"schemeunit.ss"))

View File

@ -0,0 +1,335 @@
#lang scheme/base
#|
This file defines two sorts of primitives. All of them are provided into any module using the typed scheme language.
1. macros for defining type annotated code.
this includes: lambda:, define:, etc
potentially, these macros should be replacements for the mzscheme ones in the user program
however, it's nice to be able to use both when the sugar is more limited
for example: (define ((f x) y) (+ x y))
2. macros for defining 'magic' code
examples: define-typed-struct, require/typed
these expand into (ignored) mzscheme code, and declarations that a typechecker understands
in order to protect the declarations, they are wrapped in `#%app void' so that local-expand of the module body
will not expand them on the first pass of the macro expander (when the stop list is ignored)
|#
(provide (all-defined-out))
(require (for-syntax
scheme/base
"type-rep.ss"
(lib "match.ss")
"parse-type.ss"
(lib "struct.ss" "syntax")
(lib "stx.ss" "syntax")
"utils.ss"
"tc-utils.ss"
"type-name-env.ss"
"type-contract.ss"))
(require "require-contract.ss"
"internal-forms.ss"
"planet-requires.ss"
(lib "etc.ss")
(except-in (lib "contract.ss") ->)
(only-in (lib "contract.ss") [-> c->])
(lib "struct.ss")
"base-env.ss")
(define-for-syntax (ignore stx) (syntax-property stx 'typechecker:ignore #t))
(define-for-syntax (internal stx)
(quasisyntax/loc stx
(define-values ()
(begin
(quote-syntax #,stx)
(#%plain-app values)))))
(define-syntax (require/typed stx)
(syntax-case* stx (rename) (lambda (x y) (eq? (syntax-e x) (syntax-e y)))
[(_ lib [nm ty] ...)
#'(begin (require/typed nm ty lib) ...)]
[(_ nm ty lib)
(identifier? #'nm)
(quasisyntax/loc stx (begin
#,(syntax-property (syntax-property #'(define cnt* #f)
'typechecker:contract-def #'ty)
'typechecker:ignore #t)
#,(internal #'(require/typed-internal nm ty))
#,(syntax-property #'(require/contract nm cnt* lib)
'typechecker:ignore #t)))]
[(_ (rename internal-nm nm) ty lib)
(raise-syntax-error "rename not currently supported" stx)
#; #;
(identifier? #'nm)
(quasisyntax/loc stx (begin
#,(syntax-property (syntax-property #'(define cnt* #f)
'typechecker:contract-def #'ty)
'typechecker:ignore #t)
#,(internal #'(require/typed-internal internal-nm ty))
#,(syntax-property #'(require/contract nm cnt* lib)
'typechecker:ignore #t)))]))
(define-syntax (require/opaque-type stx)
(syntax-case stx ()
[(_ ty pred lib)
(and (identifier? #'ty) (identifier? #'pred))
(begin
(register-type-name #'ty (make-Opaque #'pred (syntax-local-certifier)))
(quasisyntax/loc stx
(begin
#,(syntax-property #'(define pred-cnt (any/c . c-> . boolean?))
'typechecker:ignore #t)
#,(internal #'(require/typed-internal pred (Any -> Boolean : (Opaque pred))))
(define-type-alias ty (Opaque pred))
#,(syntax-property #'(require/contract pred pred-cnt lib)
'typechecker:ignore #t))))]))
(define-for-syntax (types-of-formals stx src)
(syntax-case stx (:)
[([var : ty] ...) (quasisyntax/loc stx (ty ...))]
[([var : ty] ... . [rest : rest-ty]) (syntax/loc stx (ty ... rest-ty ..))]
[_
(let loop ([stx stx])
(syntax-case stx ()
;; should never happen
[() (raise-syntax-error #f "bad annotation syntax" src stx)]
[([var : ty] . rest)
(identifier? #'var)
(loop #'rest)]
[([var : ty] . rest)
(raise-syntax-error #f "not a variable" src #'var)]
[(e . rest)
(raise-syntax-error #f "expected annotated variable of the form [x : T], got something else" src #'e)]))]))
(define-syntax (plambda: stx)
(syntax-case stx ()
[(plambda: (tvars ...) formals . body)
(syntax-property #'(lambda: formals . body)
'typechecker:plambda
#'(tvars ...))]))
(define-syntax (pcase-lambda: stx)
(syntax-case stx ()
[(pcase-lambda: (tvars ...) cl ...)
(syntax-property #'(case-lambda: cl ...)
'typechecker:plambda
#'(tvars ...))]))
(define-syntax (pdefine: stx)
(syntax-case stx (:)
[(pdefine: tvars (nm . formals) : ret-ty . body)
(with-syntax* ([(tys ...) (types-of-formals #'formals stx)]
[type (syntax/loc #'ret-ty (All tvars (tys ... -> ret-ty)))])
(syntax/loc stx
(define: nm : type
(plambda: tvars formals . body))))]))
(define-syntax (ann stx)
(syntax-case stx (:)
[(_ arg : ty)
#;#'(let: ([id : ty arg]) id)
(syntax-property #'arg 'type-ascription #'ty)]))
(define-syntax (: stx)
(let ([stx*
;; make it possible to add another colon after the id for clarity
(syntax-case stx (:)
[(: id : . more) (syntax/loc stx (: id . more))]
[_ stx])])
(syntax-case stx* ()
[(_ id ty)
(identifier? #'id)
(syntax-property
(internal (syntax/loc stx (:-internal id ty)))
'disappeared-use #'id)]
[(_ id ty)
(raise-syntax-error '|type declaration| "can only annotate identifiers with types"
stx #'id)]
[(_ _ _ _ . _)
(raise-syntax-error '|type declaration| "too many arguments" stx)]
[(_ _)
(raise-syntax-error '|type declaration| "too few arguments" stx)])))
(define-syntax (inst stx)
(syntax-case stx (:)
[(_ arg : tys ...)
(syntax-property #'arg 'type-inst #'(tys ...))]))
(define-syntax (define: stx)
(syntax-case stx (:)
[(define: (nm . formals) : ret-ty body ...)
(identifier? #'nm)
(with-syntax* ([(tys ...) (types-of-formals #'formals stx)]
[arrty (syntax/loc stx (tys ... -> ret-ty))])
(syntax/loc stx
(define: nm : arrty
(lambda: formals body ...))))]
[(define: nm : ty body)
(identifier? #'nm)
(with-syntax ([new-nm (syntax-property #'nm 'type-label #'ty)])
(syntax/loc stx (define new-nm body)))]
[(define: (vars ...) (f args ...) : ret body ...)
(andmap identifier? (syntax->list #'(vars ...)))
#'(pdefine: (vars ...) (f args ...) : ret body ...)]
[(define: (nm . formals) body ...)
(raise-syntax-error #f "missing return type annotation" stx)]
[(define: nm body)
(raise-syntax-error #f "missing type annotation" stx)]))
;; helper function for annoating the bound names
(define-for-syntax (annotate-names stx)
(define (label-one var ty)
(syntax-property var 'type-label ty))
(define (label vars tys)
(map label-one
(syntax->list vars)
(syntax->list tys)))
(syntax-case stx (:)
[[var : ty] (label-one #'var #'ty)]
[([var : ty] ...)
(label #'(var ...) #'(ty ...))]
[([var : ty] ... . [rest : rest-ty])
(append (label #'(var ...) #'(ty ...)) (label-one #'rest #'rest-ty))]))
(define-syntax-rule (λ: . args) (lambda: . args))
(define-syntax (lambda: stx)
(syntax-case stx (:)
[(lambda: formals . body)
(with-syntax ([labeled-formals (annotate-names #'formals)])
(syntax/loc stx (lambda labeled-formals . body)))]))
(define-syntax (case-lambda: stx)
(syntax-case stx (:)
[(case-lambda: [formals . body] ...)
(with-syntax ([(lab-formals ...) (map annotate-names (syntax->list #'(formals ...)))])
(syntax/loc stx (case-lambda [lab-formals . body] ...)))]))
(define-syntaxes (let-internal: let*: letrec:)
(let ([mk (lambda (form)
(lambda (stx)
(syntax-case stx (:)
[(_ ([nm : ty . exprs] ...) . body)
(with-syntax* ([(vars ...) (annotate-names #'([nm : ty] ...))]
[bindings (map (lambda (v e loc)
(quasisyntax/loc loc [#,v . #,e]))
(syntax->list #'(vars ...))
(syntax->list #'(exprs ...))
(syntax->list (syntax-case stx () [(_ bs . body) #'bs])))])
(quasisyntax/loc stx (#,form bindings . body)))])))])
(values (mk #'let) (mk #'let*) (mk #'letrec))))
(define-syntax (let: stx)
(syntax-case stx (:)
[(let: nm : ret-ty ([arg : ty val] ...) . body)
(identifier? #'nm)
(syntax/loc stx ((letrec: ([nm : (ty ... -> ret-ty) (lambda: ([arg : ty] ...) . body)]) nm) val ...))]
[(let: . rest)
(syntax/loc stx (let-internal: . rest))]))
(define-syntax (define-type-alias stx)
(syntax-case stx ()
[(_ tname rest)
(identifier? #'tname)
(begin
#`(begin
#,(ignore #'(define-syntax tname (lambda (stx) (raise-syntax-error 'type-check "type name used out of context" stx))))
#,(internal (syntax/loc stx (define-type-alias-internal tname rest)))))]
[(_ (tname . args) rest)
(andmap identifier? (syntax->list #'args))
#'(define-type-alias tname (All args rest))]))
(define-syntax (define-typed-struct/exec stx)
(syntax-case stx (:)
[(_ nm ([fld : ty] ...) [proc : proc-ty])
(with-syntax*
([proc* (syntax-property #'(ann proc : proc-ty) 'typechecker:with-type #t)]
[d-s (syntax-property (syntax/loc stx (define-struct/properties nm (fld ...)
([prop:procedure proc*])))
'typechecker:ignore-some #t)]
[dtsi (internal (syntax/loc stx (define-typed-struct/exec-internal nm ([fld : ty] ...) proc-ty)))])
#'(begin d-s dtsi))]))
(define-syntax (with-handlers: stx)
(syntax-case stx ()
[(_ ([pred? action] ...) . body)
(with-syntax ([(pred?* ...) (map (lambda (s) (syntax-property #`(ann #,s : (Any -> Any)) 'typechecker:with-type #t))
(syntax->list #'(pred? ...)))]
[(action* ...)
(map (lambda (s) (syntax-property s 'typechecker:exn-handler #t)) (syntax->list #'(action ...)))]
[body* (syntax-property #'(begin . body) 'typechecker:exn-body #t)])
(syntax-property #'(with-handlers ([pred?* action*] ...) body*)
'typechecker:with-handlers
#t))]))
(define-syntax (define-typed-struct stx)
(syntax-case stx (:)
[(_ nm ([fld : ty] ...) . opts)
(with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts))
'typechecker:ignore #t)]
[dtsi (internal (syntax/loc stx (define-typed-struct-internal nm ([fld : ty] ...))))])
#'(begin d-s dtsi))]
[(_ (vars ...) nm ([fld : ty] ...) . opts)
(with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts))
'typechecker:ignore #t)]
[dtsi (internal (syntax/loc stx (define-typed-struct-internal (vars ...) nm ([fld : ty] ...))))])
#'(begin d-s dtsi))]))
(define-syntax (require-typed-struct stx)
(syntax-case stx (:)
[(_ nm ([fld : ty] ...) lib)
(with-syntax* ([(struct-info maker pred sel ...) (build-struct-names #'nm (syntax->list #'(fld ...)) #f #t)]
[oty #'(Opaque pred)])
#'(begin
(require/opaque-type nm pred lib)
(require/typed maker (ty ... -> oty) lib)
(require/typed sel (oty -> ty) lib) ...))]))
(define-syntax (do: stx)
(syntax-case stx (:)
[(_ : ty ((var : tys init . step) ...) (e0 e1 ...) c ...)
(with-syntax ([(step ...)
(map (lambda (v s)
(syntax-case s ()
[() v]
[(e) #'e]
[_ (raise-syntax-error
#f
"bad variable syntax"
stx)]))
(syntax->list #'(var ...))
(syntax->list #'(step ...)))])
(syntax-case #'(e1 ...) ()
[() (syntax/loc
stx
(let: doloop : ty ([var : tys init] ...)
(if (not e0)
(begin c ... (doloop step ...)))))]
[(e1 e2 ...)
(syntax/loc
stx
(let: doloop : ty ([var : tys init] ...)
(if e0
(begin e1 e2 ...)
(begin c ... (doloop step ...)))))]))]))

View File

@ -0,0 +1,109 @@
#lang scheme/base
(require (only-in (lib "1.ss" "srfi") [assoc assoc*])
(prefix-in 1: (lib "1.ss" "srfi"))
(lib "kerncase.ss" "syntax")
(lib "struct.ss" "syntax")
(lib "stx.ss" "syntax")
(lib "etc.ss")
(except-in (lib "list.ss") remove)
"type-contract.ss"
"signatures.ss"
"tc-structs.ss"
"utils.ss" ;; doesn't need tests
"type-rep.ss" ;; doesn't need tests
"unify.ss" ;; needs tests
"infer.ss"
"type-effect-convenience.ss" ;; maybe needs tests
"union.ss"
"subtype.ss" ;; has tests
"internal-forms.ss" ;; doesn't need tests
"planet-requires.ss" ;; doesn't need tests
"type-env.ss" ;; maybe needs tests
"parse-type.ss" ;; has tests
"tc-utils.ss" ;; doesn't need tests
"type-environments.ss" ;; doesn't need tests
"lexical-env.ss" ;; maybe needs tests
"type-annotation.ss" ;; has tests
"type-name-env.ss" ;; maybe needs tests
"init-envs.ss"
"effect-rep.ss"
"mutated-vars.ss"
"def-binding.ss"
(lib "plt-match.ss"))
(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 [(1: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 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 export-id out-id))))))]
[(eq? (syntax-e internal-id) (syntax-e external-id))
#`(provide #,internal-id)]
[else #`(provide (rename #,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))]))

View File

@ -0,0 +1,96 @@
#lang scheme/base
(require "type-rep.ss" "unify.ss" "union.ss" "infer.ss" "subtype.ss"
"type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss"
mzlib/plt-match mzlib/trace)
(provide restrict (rename-out [*remove remove]) overlap)
(define (overlap t1 t2)
(match (list t1 t2)
[(list (Univ:) _) #t]
[(list _ (Univ:)) #t]
[(list (F: _) _) #t]
[(list _ (F: _)) #t]
[(list (Name: n) (Name: n*)) (free-identifier=? n n*)]
[(list (? Mu?) _) (overlap (unfold t1) t2)]
[(list _ (? Mu?)) (overlap t1 (unfold t2))]
[(list (Union: e) t)
(ormap (lambda (t*) (overlap t* t)) e)]
[(list t (Union: e))
(ormap (lambda (t*) (overlap t t*)) e)]
[(or (list _ (? Poly?)) (list (? Poly?) _))
#t] ;; these can have overlap, conservatively
[(list (Base: s1) (Base: s2)) (eq? s1 s2)]
[(list (Base: _) (Value: _)) (subtype t2 t1)] ;; conservative
[(list (Value: _) (Base: _)) (subtype t1 t2)] ;; conservative
[(list (Syntax: t) (Syntax: t*))
(overlap t t*)]
[(or (list (Syntax: _) _)
(list _ (Syntax: _)))
#f]
[(list (Base: _) _) #f]
[(list _ (Base: _)) #f]
[(list (Value: (? pair? v)) (Pair: _ _)) #t]
[(list (Pair: _ _) (Value: (? pair? v))) #t]
[(list (Pair: a b) (Pair: a* b*))
(and (overlap a a*)
(overlap b b*))]
[(or (list (Pair: _ _) _)
(list _ (Pair: _ _)))
#f]
[else #t]))
;; this is *definitely* not yet correct
;; 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 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
))
;(trace restrict)
;; also not yet correct
;; produces old without the contents of rem
(define (*remove old rem)
(define initial
(if (subtype old rem)
(Un) ;; the empty type
(match (list old rem)
[(list (or (App: _ _ _) (Name: _)) t)
;; must be different, since they're not subtypes
;; and n must refer to a distinct struct type
old]
[(list (Union: l) rem)
(apply Un (map (lambda (e) (*remove e rem)) l))]
[(list (? Mu? old) t) (*remove (unfold old) t)]
[(list (Poly: vs b) t) (make-Poly vs (*remove b rem))]
[_ old])))
(if (subtype old initial) old initial))
;(trace *remove)
;(trace restrict)

View File

@ -0,0 +1,164 @@
#lang scheme/base
(require mzlib/struct
mzlib/plt-match
syntax/boundmap
"planet-requires.ss"
"free-variance.ss"
"utils.ss"
"interning.ss"
mzlib/etc
(for-syntax
scheme/base
syntax/struct
syntax/stx
"utils.ss"))
(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-hash-table) (make-hash-table)))
(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-table-put! var-table v empty-hash-table)
(hash-table-put! 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-table-put! var-table v #,(car frees))
(hash-table-put! 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-table-put! var-table v fvs)
(hash-table-put! index-table v fis))
v)))])])
#'(begin
(define-struct (nm parent) flds #:inspector #f)
(define-match-expander ex
(lambda (s)
(...
(syntax-case s ()
[(__ fs ...) (syntax/loc s (struct nm (_ fs ...)))]))))
(begin-for-syntax
(hash-table-put! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs)))
intern
provides
frees)))])))
(values (mk #'Type #'type-name-ht) (mk #'Effect #'effect-name-ht))))

View File

@ -0,0 +1,40 @@
#lang scheme/base
(require scheme/contract (for-syntax scheme/base syntax/kerncase))
(provide require/contract define-ignored)
(define-syntax (define-ignored stx)
(syntax-case stx ()
[(_ name expr)
(syntax-case (local-expand/capture-lifts #'expr 'expression
(list #'define-values))
(begin define-values)
[(begin (define-values (n) e) e*)
#'(begin (define-values (n) e)
(define name e*))]
[e #'(define name e)])]))
(define-syntax (require/contract stx)
(syntax-case stx ()
[(require/contract nm cnt lib)
#`(begin (require (only-in lib [nm tmp]))
(define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen #'#,stx)))]))
#|
(module a mzscheme
(provide x)
(define (x a) 'hi))
(module z mzscheme
(require require-contract)
(require (lib "contract.ss"))
(define-struct b (X Y))
(require/contract x (b? . -> . b?) a )
(x 'no)
)
(require z)
|#

View File

@ -0,0 +1,79 @@
#lang scheme/base
(require "type-rep.ss" "type-name-env.ss" "tc-utils.ss"
"type-utils.ss"
mzlib/plt-match
mzlib/trace)
(provide resolve-name resolve-app needs-resolving? resolve-once)
(define (resolve-name t)
(match t
[(Name: n) (lookup-type-name n)]
[_ (int-err "resolve-name: not a name ~a" t)]))
(define (resolve-app rator rands stx)
(parameterize ([current-orig-stx stx])
(match rator
[(Poly: _ _)
(instantiate-poly rator rands)]
[(Name: _) (resolve-app (resolve-name rator) rands stx)]
[(Mu: _ _) (resolve-app (unfold rator) rands)]
[(App: r r* s) (resolve-app (resolve-app r r* s) rands)]
[_ (tc-error "resolve-app: not a proper operator ~a" rator)])))
(define (needs-resolving? t)
(or (Mu? t) (App? t) (Name? t)))
(define (resolve-once t)
(match t
[(Mu: _ _) (unfold t)]
[(App: r r* s) (resolve-app r r* s)]
[(Name: _) (resolve-name t)]))
#|
(define (resolve-tc-result tcr)
(match tcr
[(tc-result: t e1s e2s)
(ret (resolve-type t) (map resolve-effect e1s) (map resolve-effect e2s))]))
(define (resolve-effect* e)
(effect-case resolve-type resolve-effect e))
(define (resolve-type* t)
(define (int t)
(type-case resolve-type t
[#:Name stx (lookup-type-name stx)]
[#:Poly #:matcher Poly: names body (make-Poly names (resolve-type body))]
[#:Mu #:matcher Mu: name body (make-Mu name (resolve-type body))]
[#:App rator rands stx
(let ([rator (resolve-type rator)]
[rands (map resolve-type rands)])
(unless (Poly? rator)
(tc-error/stx stx "Cannot apply non-polymorphic type: ~a, arguments were: ~a" rator rands))
(instantiate-poly rator rands))]))
(let loop ([t (int t)])
(if (or (Name? t) (App? t))
(loop (resolve-type t))
t)))
(define table (make-hash-table))
(define (resolve-type t)
(hash-table-get table t
(lambda () (let ([v (resolve-type* t)])
(hash-table-put! table t v)
v))))
(define (resolve-effect t)
(hash-table-get table t
(lambda () (let ([v (resolve-effect* t)])
(hash-table-put! table t v)
v))))
;(trace resolve-type)
|#

View File

@ -0,0 +1,42 @@
(module signatures mzscheme
(require (lib "unit.ss"))
(provide (all-defined))
;; cycle 1
(define-signature type-printer^
(print-type has-name print-effect)) ;; done
(define-signature infer^
(unify1 fv fv/list unfold)) ;; done
(define-signature subst^
(subst subst-all)) ;; done
(define-signature type-equal^
(type-equal? type-compare type<? rename tc-result-equal?)) ;; done
;; cycle 2
(define-signature typechecker^
(type-check tc-toplevel-form))
(define-signature tc-expr^
(tc-expr tc-expr/check check-below tc-literal tc-exprs tc-exprs/check tc-expr/t #;check-expr))
(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))
)

View File

@ -0,0 +1,272 @@
#lang scheme/base
(require "type-rep.ss" "unify.ss" "type-utils.ss"
"tc-utils.ss"
"effect-rep.ss"
"type-comparison.ss"
"resolve-type.ss"
"type-name-env.ss"
mzlib/plt-match
mzlib/trace)
;; exn representing failure of subtyping
;; s,t both types
(define-struct (exn:subtype exn:fail) (s t))
#;
(define-values (fail-sym exn:subtype?)
(let ([sym (gensym)])
(values sym (lambda (s) (eq? s sym)))))
;; inference failure - masked before it gets to the user program
(define-syntax fail!
(syntax-rules ()
[(_ s t) #;(raise fail-sym)
(raise (make-exn:subtype "subtyping failed" (current-continuation-marks) s t))
#;(error "inference failed" s t)]))
;; data structures for remembering things on recursive calls
(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)))
;; is s a subtype of t?
;; type type -> boolean
(define (subtype s t)
(with-handlers
([exn:subtype? (lambda _ #f)])
(subtype* (current-seen) s t)))
;; are all the s's subtypes of all the t's?
;; [type] [type] -> boolean
(define (subtypes s t)
(with-handlers
([exn:subtype? (lambda _ #f)])
(subtypes* (current-seen) s t)))
;; subtyping under constraint set, but produces boolean result instead of raising exn
;; List[(cons Number Number)] type type -> maybe[List[(cons Number Number)]]
(define (subtype*/no-fail A s t)
(with-handlers
([exn:subtype? (lambda _ #f)])
(subtype* A s t)))
;; type type -> (does not return)
;; subtying fails
#;
(define (fail! s t) (raise (make-exn:subtype "subtyping failed" (current-continuation-marks) s t)))
;; check subtyping for two lists of types
;; List[(cons Number Number)] listof[type] listof[type] -> List[(cons Number Number)]
(define (subtypes* A ss ts)
(cond [(and (null? ss) (null? ts) A)]
[(or (null? ss) (null? ts)) (fail! ss ts)]
[(subtype* A (car ss) (car ts))
=>
(lambda (A*) (subtypes* A* (cdr ss) (cdr ts)))]
[else (fail! (car ss) (car ts))]))
;; check if s is a supertype of any element of ts
(define (supertype-of-one/arr A s ts)
(ormap (lambda (e) (arr-subtype*/no-fail A e s)) ts))
(define (sub-eff e1 e2)
(match (list e1 e2)
[(list e e) #t]
[(list (Latent-Restrict-Effect: t) (Latent-Restrict-Effect: t*))
(and (subtype t t*)
(subtype t* t))]
[(list (Latent-Remove-Effect: t) (Latent-Remove-Effect: t*))
(and (subtype t t*)
(subtype t* t))]
[else #f]))
;(trace sub-eff)
;; simple co/contra-variance for ->
(define (arr-subtype*/no-fail A0 s t)
(with-handlers
([exn:subtype? (lambda _ #f)])
(match (list s t)
;; top for functions is above everything
[(list _ (top-arr:)) A0]
[(list (arr: s1 s2 #f thn-eff els-eff) (arr: t1 t2 #f (or '() thn-eff) (or '() els-eff)))
(let ([A1 (subtypes* A0 t1 s1)])
(subtype* A1 s2 t2))]
[(list (arr: s1 s2 s3 thn-eff els-eff) (arr: t1 t2 t3 thn-eff* els-eff*))
(unless
(or (and (null? thn-eff*) (null? els-eff*))
(and (effects-equal? thn-eff thn-eff*)
(effects-equal? els-eff els-eff*))
(and (andmap sub-eff thn-eff thn-eff*)
(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)])
(if (not t3)
(subtype* A s2 t2)
(let ([A1 (subtype* A t3 s3)])
(subtype* A1 s2 t2))))]
[else
(fail! s t)])))
(define (subtypes/varargs args dom rst)
(with-handlers
([exn:subtype? (lambda _ #f)])
(subtypes*/varargs (empty-set) args dom rst)))
(define (subtypes*/varargs A0 argtys dom rst)
(let loop-varargs ([dom dom] [argtys argtys] [A A0])
(cond
[(and (null? dom) (null? argtys)) A]
[(null? argtys) (fail! argtys dom)]
[(and (null? dom) rst)
(cond [(subtype* A (car argtys) rst) => (lambda (A) (loop-varargs dom (cdr argtys) A))]
[else (fail! (car argtys) rst)])]
[(null? dom) (fail! argtys dom)]
[(subtype* A (car argtys) (car dom)) => (lambda (A) (loop-varargs (cdr dom) (cdr argtys) A))]
[else (fail! (car argtys) (car dom))])))
;(trace subtypes*/varargs)
;; the algorithm for recursive types transcribed directly from TAPL, pg 305
;; List[(cons Number Number)] type type -> List[(cons Number Number)]
;; potentially raises exn:subtype, when the algorithm fails
;; is s a subtype of t, taking into account constraints A
(define (subtype* A s t)
(parameterize ([match-equality-test type-equal?]
[current-seen A])
(if (seen? s t)
A
(let* ([A0 (remember s t A)])
(parameterize ([current-seen A0])
#;(match t
[(Name: n) (when (eq? 'heap (syntax-e n))
(trace subtype*))]
[_ #f])
(match (list s t)
;; subtyping is reflexive
[(list t t) A0]
;; univ is top
[(list _ (Univ:)) A0]
;; (Un) is bot
[(list _ (Union: (list))) (fail! s t)]
[(list (Union: (list)) _) A0]
;; value types
[(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
;; integers are numbers too
[(list (Base: 'Integer) (Base: 'Number)) A0]
;; values are subtypes of their "type"
[(list (Value: (? integer? n)) (Base: 'Integer)) A0]
[(list (Value: (? number? n)) (Base: 'Number)) A0]
[(list (Value: (? boolean? n)) (Base: 'Boolean)) A0]
[(list (Value: (? symbol? n)) (Base: 'Symbol)) A0]
[(list (Value: (? string? n)) (Base: 'String)) A0]
;; tvars are equal if they are the same variable
[(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
;; case-lambda
[(list (Function: arr1) (Function: arr2))
(when (null? arr1) (fail! s t))
(let loop-arities ([A* A0]
[arr2 arr2])
(cond
[(null? arr2) A*]
[(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
[else (fail! s t)]))]
;; recur structurally on pairs
[(list (Pair: a d) (Pair: a* d*))
(let ([A1 (subtype* A0 a a*)])
(and A1 (subtype* A1 d d*)))]
;; quantification over two types preserves subtyping
[(list (Poly: ns b1) (Poly: ms b2))
(=> unmatch)
(unless (= (length ns) (length ms))
(unmatch))
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
;; use unification to see if we can use the polytype here
[(list (Poly: vs b) s)
(=> unmatch)
(if (unify1 s b) A0 (unmatch))]
[(list s (Poly: vs b))
(=> unmatch)
(if (null? (fv b)) (subtype* A0 s b) (unmatch))]
;; names are compared for equality:
[(list (Name: n) (Name: n*))
(=> unmatch)
(if (free-identifier=? n n*)
A0
(unmatch))]
;; just unfold the recursive types
[(list _ (? Mu?)) (subtype* A0 s (unfold t))]
[(list (? Mu?) _) (subtype* A0 (unfold s) t)]
;; for unions, we check the cross-product
[(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
[(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
;; subtyping on immutable structs is covariant
[(list (Struct: nm _ flds #f) (Struct: nm _ flds* #f))
(subtypes* A0 flds flds*)]
[(list (Struct: nm _ flds proc) (Struct: nm _ flds* proc*))
(subtypes* A0 (cons proc flds) (cons proc* flds*))]
;; subtyping on structs follows the declared hierarchy
[(list (Struct: nm (? Type? parent) flds proc) other)
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
(subtype* A0 parent other)]
;; applications and names are structs too
[(list (App: (Name: n) args _) other)
(let ([t (lookup-type-name n)])
(unless (Type? t)
(fail! s t))
#;(printf "subtype: app-name: name: ~a type: ~a other: ~a ~ninst: ~a~n" (syntax-e n) t other
(instantiate-poly t args))
(let ([v (subtype* A0 (instantiate-poly t args) other)])
#;(printf "val: ~a~n" v)
v))]
[(list (Name: n) other)
(let ([t (lookup-type-name n)])
;(printf "subtype: name: ~a ~a ~a~n" (syntax-e n) t other)
(if (Type? t)
(subtype* A0 t other)
(fail! s t)))]
;; Promises are covariant
[(list (Struct: 'Promise _ (list t) _) (Struct: 'Promise _ (list t*) _)) (subtype* A0 t t*)]
;; subtyping on values is pointwise
[(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
;; single values shouldn't actually happen, but they're just like the type
[(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
;; subtyping on other stuff
[(list (Syntax: t) (Syntax: t*))
(subtype* A0 t t*)]
[(list (Instance: t) (Instance: t*))
(subtype* A0 t t*)]
;; otherwise, not a subtype
[_ (fail! s t) (printf "failed")]))))))
(define (type-compare? a b)
(and (subtype a b) (subtype b a)))
(provide subtype type-compare? subtypes/varargs subtypes)
;(trace subtype*)
;(trace supertype-of-one/arr)
;(trace arr-subtype*/no-fail)
;(trace subtype-of-one)
;(trace subtype*/no-fail)
;(trace subtypes*)
;(trace subtype)
;(subtype (-> Univ B) (-> Univ Univ))
;(subtype (make-poly '(a) (make-tvar 'a)) (make-lst N))

View File

@ -0,0 +1,59 @@
#lang scheme/base
(require mzlib/trace)
;; from Eli
(provide (all-defined-out))
;; -------------------- utilities
(define (pull-from-syntax stx . locs)
(let loop ([stx stx] [locs locs])
(if (null? locs)
stx
(loop (list-ref (syntax->list stx) (car locs)) (cdr locs)))))
(define (syntax-loc stx) (list (syntax-position stx) (syntax-span stx)))
;; -------------------- the real stuff
;; Look for `lookfor' in `enclosing', return chain of syntaxes from
;; the innermost out of only syntaxes with the given src, returns #f
;; if it can't find it.
(define (enclosing-syntaxes-with-source enclosing lookfor src)
(let loop ([r '()] [stx enclosing])
(let* ([r (if (and (syntax? stx) (eq? src (syntax-source stx)))
(cons stx r)
r)]
[loop (lambda (stx) (loop r stx))])
(if (eq? stx lookfor)
r
(let ([stx (if (syntax? stx) (syntax-e stx) stx)])
(and (pair? stx)
(or (loop (car stx)) (loop (cdr stx)))))))))
;; Look for (the outermost) syntax in `orig' that has the same
;; location as `lookfor' which is coming from the expanded `orig',
;; given in `expanded'.
(define (look-for-in-orig orig expanded lookfor)
(define src (syntax-source orig))
;; we just might get a lookfor that is already in the original
(if (eq? src (syntax-source lookfor))
lookfor
(let ([enclosing (enclosing-syntaxes-with-source expanded lookfor src)]
[syntax-locs (make-hash-table 'equal)])
;; find all syntax locations in original code
(let loop ([stx orig])
(when (syntax? stx) (hash-table-put! syntax-locs (syntax-loc stx) stx))
(let ([stx (if (syntax? stx) (syntax-e stx) stx)])
(when (pair? stx) (loop (car stx)) (loop (cdr stx)))))
;; look for some enclosing expression
(and enclosing
(ormap (lambda (enc) (hash-table-get syntax-locs (syntax-loc enc) #f))
enclosing)))))
;(trace look-for-in-orig)

View File

@ -0,0 +1,42 @@
#lang scheme/base
(require mzlib/plt-match)
(provide (all-defined-out))
;; a table is represented by an association list, (cons key value)
;; alist->eq : alist -> table
(define (alist->eq l) l)
;; to-sexp : table -> Listof(List k v)
(define (to-sexp t)
(map (match-lambda [(cons k v) (list k v)]) t))
;; union/value : table(k,v) table(k,v) (v v -> v) -> table(k,v)
(define (union/value t1 t2 f)
(define ks1 (map car t1))
(define ks2 (map car t2))
;; everything but the common ones
(define t1* (filter (match-lambda [(cons k v) (not (memq k ks2))]) t1))
(define t2* (filter (match-lambda [(cons k v) (not (memq k ks1))]) t2))
(define pre-result (append t1* t2*))
;; the common ones
(define *t1 (filter (match-lambda [(cons k v) (memq k ks2)]) t1))
(define *t2 (filter (match-lambda [(cons k v) (memq k ks1)]) t2))
(define merged (map (match-lambda [(cons k v1)
(let ([v2 (cdr (assq k *t2))])
(cons k (f v1 v2)))])
*t1))
(append pre-result merged))
(define (make-eq) null)
(define (lookup k t)
(cond [(assq k t) => cdr]
[else #f]))
(define (insert k v t)
(cons (cons k v) t))

View File

@ -0,0 +1,462 @@
#lang scheme/unit
(require "signatures.ss"
(lib "plt-match.ss")
(lib "list.ss")
(prefix-in 1: srfi/1)
"type-rep.ss"
"effect-rep.ss"
"tc-utils.ss"
"subtype.ss"
"unify.ss"
"infer.ss"
"union.ss"
"type-utils.ss"
"type-effect-convenience.ss"
"type-effect-printer.ss"
"type-annotation.ss"
"resolve-type.ss"
(only-in scheme/private/class-internal make-object do-make-object)
(lib "pretty.ss")
(lib "trace.ss")
(lib "kerncase.ss" "syntax"))
(require (for-template (lib "plt-match.ss") "internal-forms.ss" scheme/base
(only-in scheme/private/class-internal make-object do-make-object)))
(require (for-syntax (lib "plt-match.ss") "internal-forms.ss"))
(import tc-expr^ tc-lambda^)
(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] -> 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
#;(printf "got to mi= ~a ~a ~n~a ~a~n"
(var-true-effect-v (caar arg-thn-effs)) (var-true-effect-v (caar arg-els-effs))
(syntax-e (var-true-effect-v (caar arg-thn-effs))) (syntax-e (var-false-effect-v (caar arg-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 "Insufficient arguments to function application, expected ~a, got ~a"
(length dom-types) (length arg-types))]
[(and (null? doms) rest-type)
(if (subtype (car args) rest-type)
(loop (cdr args) doms (cdr stxs) (add1 arg-count))
(tc-error/stx (car stxs) "Rest argument had wrong type, expected: ~a and got: ~a" rest-type (car args)))]
[(null? doms)
(tc-error "Too many arguments to function, expected ~a, got ~a" (length dom-types) (length arg-types))]
[(subtype (car args) (car doms))
(loop (cdr args) (cdr doms) (cdr stxs) (add1 arg-count))]
[else
(tc-error/stx (car stxs) "Wrong function argument type, expected ~a, got ~a for argument ~a"
(car doms) (car args) arg-count)]))))
;(trace tc-args)
(define (tc/apply f args)
(let* ([f-ty (tc-expr f)]
[arg-tys0 (map tc-expr/t (syntax->list args))])
;; 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)))))
(let-values ([(arg-tys tail-ty) (split arg-tys0)])
(define (printable dom rst)
(list dom rst '..))
(match f-ty
[(tc-result: (Function: (list (arr: doms rngs rests thn-effs els-effs) ..1)))
(let loop ([doms* doms] [rngs* rngs] [rests* rests])
(cond [(null? doms*)
(if (and (not (null? doms)) (null? (cdr doms)))
(tc-error
"bad arguments to apply - function expected ~a fixed arguments and (Listof ~a) rest argument, given ~a"
(car doms) (car rests) arg-tys0)
(tc-error "no function domain matched - domains were: ~a arguments were ~a"
(map printable doms rests)
arg-tys0))]
[(and (subtypes arg-tys (car doms*)) (car rests*) (subtype tail-ty (make-Listof (car rests*))))
(ret (car rngs*))]
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*))]))]
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests thn-effs els-effs) ..1))))
(for-each (lambda (x) (unless (not (Poly? x))
(tc-error "Polymorphic argument ~a to polymorphic function not allowed" x)))
arg-tys0)
(let loop ([doms* doms] [rngs* rngs] [rests* rests])
(cond [(null? doms*)
(if (= 1 (length doms))
(tc-error "polymorphic function domain did not match - domain was: ~a arguments were ~a"
(car doms) arg-tys0)
(tc-error "no polymorphic function domain matched - domains were: ~a arguments were ~a" doms arg-tys0))]
[(and (= (length (car doms*))
(length arg-tys))
(infer/list (append (car doms*) (list (make-Listof (car rests*)))) arg-tys0 vars))
=> (lambda (substitution)
(let* ([s (lambda (t) (subst-all substitution t))]
[new-doms* (append (map s (car doms*)) (list (make-Listof (s (car rests*)))))])
(unless (andmap subtype arg-tys0 new-doms*)
(int-err "Inconsistent substitution - arguments not subtypes")))
(ret (subst-all substitution (car rngs*))))]
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*))]))]
[(tc-result: (Poly: vars (Function: '())))
(tc-error "Function has no cases")]
[f-ty (tc-error "Type of argument to apply is not a function type: ~n~a" f-ty)]))))
(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))))
(define (tc/funapp f-stx args-stx ftype0 argtys)
(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
[(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))]
[(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)]
[(tc-result: (Param: in out))
(match argtypes
[(list) (ret out)]
[(list t)
(if (subtype t in)
(ret -Void)
(tc-error "Wrong argument to parameter - expected ~a and got ~a" in t))]
[_ (tc-error "Wrong number of arguments to parameter - expected 0 or 1, got ~a" (length argtypes))])]
[(tc-result: (Function: (list (arr: doms rngs rests latent-thn-effs latent-els-effs) ..1)) thn-eff els-eff)
(if (= 1 (length doms))
(let-values ([(thn-eff els-eff)
(tc-args argtypes arg-thn-effs arg-els-effs (car doms) (car rests)
(car latent-thn-effs) (car latent-els-effs)
(syntax->list args))])
(ret (car rngs) thn-eff els-eff)
#;(if (false-effect? eff)
(ret (-val #f) eff)
(ret (car rngs) eff)))
(let loop ([doms* doms] [rngs rngs] [rests rests])
(cond [(null? doms*)
(tc-error "no function domain matched - domains were: ~a arguments were ~a" doms argtypes)]
[(subtypes/varargs argtypes (car doms*) (car rests)) (ret (car rngs))]
[else (loop (cdr doms*) (cdr rngs) (cdr rests))])))]
[(and rft (tc-result: (Poly: vars (Function: (list (arr: doms rngs #f thn-effs els-effs) ...)))))
;(printf "Typechecking poly app~nftype: ~a~n" ftype)
;(printf "ftype again: ~a~n" ftype)
;(printf "resolved ftype: ~a : ~a~n" (equal? rft ftype) rft)
;(printf "reresolving: ~a~n" (resolve-tc-result ftype))
;(printf "argtypes: ~a~ndoms: ~a~n" argtypes doms)
(for-each (lambda (x) (unless (not (Poly? x))
(tc-error "Polymorphic argument ~a to polymorphic function not allowed" x)))
argtypes)
(let loop ([doms* doms] [rngs* rngs])
(cond [(null? doms*)
(match-let ([(tc-result: (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs #f _ _) ...)))) ftype])
(if (= 1 (length doms))
(tc-error "Polymorphic function could not be applied to arguments:~nExpected: ~a ~nActual: ~a"
(car msg-doms) argtypes)
(tc-error "no polymorphic function domain matched - possible domains were: ~n~a~narguments: were ~n~a"
(stringify (map stringify msg-doms) "\n") (stringify argtypes))))]
[(and (= (length (car doms*))
(length argtypes))
(infer/list (car doms*) argtypes vars))
=> (lambda (substitution)
(let* ([s (lambda (t) (subst-all substitution t))]
[new-doms* (map s (car doms*))])
(unless (andmap subtype argtypes new-doms*)
(int-err "Inconsistent substitution - arguments not subtypes")))
#;(printf "subst is:~a~nret is: ~a~nvars is: ~a~n" substitution (car rngs*) vars)
(ret (subst-all substitution (car rngs*))))]
[else (loop (cdr doms*) (cdr rngs*))]))]
;; polymorphic varargs
[(tc-result: (Poly: vars (Function: (list (arr: dom rng rest thn-eff els-eff)))))
(for-each (lambda (x) (unless (not (Poly? x))
(tc-error "Polymorphic argument ~a to polymorphic function not allowed" x)))
argtypes)
(unless (<= (length dom) (length argtypes))
(tc-error "incorrect number of arguments to function: ~a ~a" dom argtypes))
(let ([substitution (infer/list/vararg dom rest argtypes vars)])
(if substitution
(let* ([s (lambda (t) (subst-all substitution t))]
[new-dom (map s dom)]
[new-rest (s rest)])
(unless (subtypes/varargs argtypes new-dom new-rest)
(int-err "Inconsistent substitution - arguments not subtypes"))
(ret (subst-all substitution rng)))
(tc-error "no polymorphic function domain matched - domain was: ~a rest type was: ~a arguments were ~a"
(stringify dom) rest (stringify argtypes))))]
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests thn-effs els-effs) ...))))
(tc-error "polymorphic vararg case-lambda application not yet supported")]
;; 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 "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)
(type-annotation #'v)]
[_ #f]))
(kernel-syntax-case*
stx #f (reverse)
[(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)))]
[(#%plain-lambda (v ...) e)
(find #'e)]
[_ #f]))
(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])))
(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) ;; the special-cased functions
;; special cases for classes
[(#%plain-app make-object cl args ...)
(tc/app/internal #'(#%plain-app do-make-object cl (#%plain-app list args ...) (#%plain-app list)) expected)]
[(#%plain-app do-make-object cl (#%plain-app list pos-args ...) (#%plain-app list (#%plain-app cons '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 "expected ~a positional arguments, but got ~a" (length pos-tys) (length (syntax->list #'(pos-args ...)))))
(for-each tc-expr/check (syntax->list #'(pos-args ...)) pos-tys)
(for-each (lambda (n) (unless (memq n tnames)
(tc-error "unknown named argument ~a for class~nlegal named arguments are ~a" n (stringify tnames))))
names)
(for-each (match-lambda
[(list tname tfty opt?)
(let ([s (cond [(assq tname name-assoc) => cadr]
[(not opt?)
(tc-error "value not provided for named init arg ~a" tname)]
[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 "expected a class value for object creation, got: ~a" t)])))]
[(#%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)]
[(tc-result: con-t) (tc-expr #'con)])
(match (list prod-t con-t)
[(list (Function: (list (arr: (list) vals #f _ _))) (Function: (list (arr: dom rng #f _ _))))
(=> unmatch)
(match (list vals dom)
[(list (Values: v) (list t ...))
(if (subtypes v t)
(ret rng)
(unmatch))]
[(list t1 (list t2))
(if (subtype t1 t2) (ret rng) (unmatch))]
[_ (unmatch)])]
[_ (tc-error "Incorrect arguments to call with values: ~a ~a" prod-t con-t)]))]
;; special cases for `values'
[(#%plain-app values arg) (tc-expr #'arg)]
[(#%plain-app values . args)
(let ([tys (map tc-expr/t (syntax->list #'args))])
(ret (list->values-ty 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))))
;; 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)]
;; even more special case for match
[(#%plain-app
(letrec-values
([(lp) (#%plain-lambda (val acc ...)
(if (#%plain-app null? val*)
thn
els))])
lp*)
actual actuals ...)
(and ;(printf "got here 0:~a~n" (syntax->datum #'body))
expected
;(printf "got here 1~n")
(not (andmap type-annotation (syntax->list #'(val acc ...))))
(free-identifier=? #'val #'val*)
(andmap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
(syntax->list #'(acc ...)))
;(printf "got here 2~n")
#;
(match (matches? #'lv-bindings)
[(list res acc* more)
(and
(andmap type-annotation res)
(andmap free-identifier=? (syntax->list #'(acc ...)) acc*)
(free-identifier=? #'lp #'lp*))]
[_ #f]))
(let* ([ts1 (tc-expr/t #'actual)]
[ts1 (generalize ts1)]
[ann-ts (map (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
(syntax->list #'(acc ...)))]
[ts (cons ts1 ann-ts)])
;(printf "doing match case actuals:~a ann-ts: ~a~n"
; (syntax->datum #'(actuals ...)) ann-ts)
;; check that the actual arguments are ok here
(map tc-expr/check (syntax->list #'(actuals ...)) ann-ts)
;(printf "done here ts = ~a~n" ts)
;; then check that the function typechecks with the inferred types
(tc/rec-lambda/check form
#'(val acc ...)
#'((if (#%plain-app null? val*)
thn
els))
#'lp
ts
expected)
(ret expected))]
;; special case when argument needs inference
[(#%plain-app (letrec-values ([(lp) (#%plain-lambda (args ...) . body)]) lp*) . actuals)
(and ;(printf "special case 0 ~a~n" expected)
expected
;(printf "special case 1~n")
(not (andmap type-annotation (syntax->list #'(args ...))))
(free-identifier=? #'lp #'lp*))
(let ([ts (map tc-expr/t (syntax->list #'actuals))])
;(printf "special case~n")
(tc/rec-lambda/check form #'(args ...) #'body #'lp ts expected)
(ret expected))]
;; default case
[(#%plain-app f args ...)
(begin
;(printf "default case~n~a~n" (syntax->datum form))
(tc/funapp #'f #'(args ...) (tc-expr #'f) (map tc-expr (syntax->list #'(args ...)))))]))
;(trace tc/app/internal)

View File

@ -0,0 +1,314 @@
#lang scheme/unit
(require (prefix-in 1: srfi/1)
syntax/kerncase
syntax/struct
syntax/stx
mzlib/etc
mzlib/plt-match
"type-contract.ss"
"signatures.ss"
"tc-structs.ss"
"type-utils.ss"
"utils.ss" ;; doesn't need tests
"type-rep.ss" ;; doesn't need tests
"unify.ss" ;; needs tests
"infer.ss"
"type-effect-convenience.ss" ;; maybe needs tests
"union.ss"
"subtype.ss" ;; has tests
"internal-forms.ss" ;; doesn't need tests
"planet-requires.ss" ;; doesn't need tests
"type-env.ss" ;; maybe needs tests
"parse-type.ss" ;; has tests
"tc-utils.ss" ;; doesn't need tests
"type-environments.ss" ;; doesn't need tests
"lexical-env.ss" ;; maybe needs tests
"type-annotation.ss" ;; has tests
"type-name-env.ss" ;; maybe needs tests
"init-envs.ss"
"effect-rep.ss"
"mutated-vars.ss"
(lib "plt-match.ss")
scheme/private/class-internal)
(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) -Keyword]
[(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 (begin (printf "checking literal : ~a~n" v) Univ)]))
;; typecheck an identifier
;; the identifier has variable effect
;; tc-id : identifier -> tc-result
(define (tc-id id)
(let* ([ty (lookup-type/lexical id)]
[inst (syntax-property id 'type-inst)])
(when (and inst
(not (Poly? ty)))
(tc-error "Cannot instantiate non-polymorphic type ~a" ty))
(when (and inst
(not (= (length (syntax->list inst)) (Poly-n ty))))
(tc-error "Wrong number of type arguments to polymorphic type ~a:~nexpected: ~a~ngot: ~a"
ty (Poly-n ty) (length (syntax->list inst))))
(let ([ty* (if inst
(begin
(printf/log "Type Instantiation: ~a~n" (syntax-e id))
(instantiate-poly ty (map parse-type (syntax->list inst))))
ty)])
(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]))
(define (check-below tr1 expected)
(match (list tr1 expected)
[(list (tc-result: t1 te1 ee1) t2)
(unless (subtype t1 t2)
(tc-error "Expected ~a, but got ~a" t2 t1))
(ret expected)]
[(list t1 t2)
(unless (subtype t1 t2)
(tc-error "Expected ~a, but got ~a" t2 t1))
(ret expected)]
[_ (error "bad arguments to check-below")]))
(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
(tc-error "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-id #'id)]
[(tc-result: val-t) (tc-expr #'val)])
(unless (subtype val-t id-t)
(tc-error "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 "#%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 "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
(tc-error "internal error: with-handlers"))
ty)]
[stx
(syntax-property form 'typechecker:ignore-some)
(let ([ty (check-subforms/ignore form)])
(unless ty
(tc-error "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-id #'id)]
[(tc-result: val-t) (tc-expr #'val)])
(unless (subtype val-t id-t)
(tc-error "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 "do not use #%variable-reference")]
;; 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 "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
(cond [(type-annotation form) => (lambda (ann)
;(printf "annotated~n")
(tc-expr/check form ann))]
[else (internal-tc-expr form)])))
(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 "send: method ~a not understood by class ~a" s c)])]
[ret-ty (tc/funapp rcvr args (ret ftype) (map tc-expr (syntax->list args)))])
(if expected
(begin (check-below ret-ty expected) (ret expected))
ret-ty))]
[(tc-result: t) (int-err "non-symbol methods not yet supported: ~a" t)])]
[(tc-result: t) (tc-error "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)]))

View File

@ -0,0 +1,225 @@
#lang scheme/unit
(require "planet-requires.ss"
"signatures.ss"
"type-rep.ss" ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"lexical-env.ss" ;; maybe needs tests
"effect-rep.ss"
"mutated-vars.ss"
"subtype.ss"
(only-in "remove-intersect.ss"
[remove *remove]
restrict)
"union.ss"
"type-utils.ss"
"tc-utils.ss"
"type-comparison.ss"
syntax/kerncase
mzlib/trace
mzlib/plt-match)
;; necessary for creating (#%app void) in tc-if/onearm
(require (for-template scheme/base))
;; if typechecking
(import tc-expr^)
(export tc-if^)
;; combinators for typechecking in the context of effects
;; t/f tells us whether this is the true or the false branch of an if
;; neccessary for handling true/false effects
;; Boolean Expr listof[Effect] option[type] -> TC-Result
(define (tc-expr/eff t/f expr effs expected)
#;(printf "tc-expr/eff : ~a~n" (syntax-object->datum expr))
;; this flag represents whether the refinement proves that this expression cannot be executed
(let ([flag (box #f)])
;; this does the operation on the old type
;; type-op : (Type Type -> Type) Type -> _ Type -> Type
(define ((type-op f t) _ old)
(let ([new-t (f old t)])
;(printf "new-t ~a~n" new-t)
;; if this operation produces an uninhabitable type, then this expression can't be executed
(when (type-equal? new-t (Un))
;(printf "setting flag!~n")
(set-box! flag #t))
;; have to return something here, so that we can continue typechecking
new-t))
;; loop : listof[effect] -> tc-result
(let loop ([effs effs])
;; convenience macro for checking the rest of the list
(define-syntax check-rest
(syntax-rules ()
[(check-rest f v)
(with-update-type/lexical f v (loop (cdr effs)))]
[(check-rest f t v) (check-rest (type-op f t) v)]))
(if (null? effs)
;; base case
(let* ([reachable? (not (unbox flag))])
(cond
;; if flag is true, then we don't want to verify that this branch has the appropriate type
;; in particular, it might be (void)
[(and expected reachable?)
(tc-expr/check expr expected)]
;; this code is reachable, but we have no expected type
[reachable?
(tc-expr expr)]
;; otherwise, this code is unreachable
;; and the resulting type should be the empty type
[(check-unreachable-code?)
(tc-expr/check expr Univ)
(ret (Un))]
[else
(ret (Un))]))
;; recursive case
(match (car effs)
;; these effects have no consequence for the typechecking
[(True-Effect:)
(or t/f (set-box! flag #t))
(loop (cdr effs))]
[(False-Effect:)
(and t/f (set-box! flag #t))
(loop (cdr effs))]
;; restrict v to have a type that's a subtype of t
[(Restrict-Effect: t v)
(check-rest restrict t v)]
;; remove t from the type of v
[(Remove-Effect: t v) (check-rest *remove t v)]
;; just replace the type of v with (-val #f)
[(Var-False-Effect: v) (check-rest (lambda (_ old) (-val #f)) v)]
;; v cannot have type (-val #f)
[(Var-True-Effect: v) (check-rest *remove (-val #f) v)])))))
;; create a dummy else branch for typechecking
(define (tc/if-onearm tst body) (tc/if-twoarm tst body (syntax/loc body (#%app void))))
(define (tc/if-onearm/check tst body expected)
#;(unless (subtype -Void expected)
(tc-error "Single-armed if may return void, but void is not allowed in this context"))
(tc/if-twoarm/check tst body (syntax/loc body (#%app void)) expected))
;; the main function
(define (tc/if-twoarm tst thn els)
#;(printf "tc-if/twoarm~n")
;; check in the context of the effects, and return
(match-let* ([(tc-result: tst-ty tst-thn-eff tst-els-eff) (tc-expr tst)]
[(tc-result: thn-ty thn-thn-eff thn-els-eff) (tc-expr/eff #t thn tst-thn-eff #f)]
#;[_ (printf "v is ~a~n" v)]
#;[c (current-milliseconds)]
[(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff #f)])
#;(printf "v now is ~a~n" (ret els-ty els-thn-eff els-els-eff))
#;
(printf "els-ty ~a ~a~n"
els-ty c)
(match (list thn-thn-eff thn-els-eff els-thn-eff els-els-eff)
;; this is the case for `or'
;; the then branch has to be #t
;; the else branch has to be a simple predicate
;; FIXME - can something simpler be done by using demorgan's law?
;; note that demorgan's law doesn't hold for scheme `and' and `or' because they can produce arbitrary values
;; FIXME - mzscheme's or macro doesn't match this!
[(list (list (True-Effect:)) (list (True-Effect:)) (list (Restrict-Effect: t v)) (list (Remove-Effect: t v*)))
(=> unmatch)
#;(printf "or branch~n")
(match (list tst-thn-eff tst-els-eff)
;; check that the test was also a simple predicate
[(list (list (Restrict-Effect: s u)) (list (Remove-Effect: s u*)))
(if (and
;; check that all the predicates are for the for the same identifier
(free-identifier=? u u*)
(free-identifier=? v v*)
(free-identifier=? v u))
;; this is just a very simple or
(ret (Un (-val #t) els-ty)
;; the then and else effects are just the union of the two types
(list (make-Restrict-Effect (Un s t) v))
(list (make-Remove-Effect (Un s t) v)))
;; otherwise, something complicated is happening and we bail
(unmatch))]
;; similarly, bail here
[_ (unmatch)])]
;; this is the case for `and'
[(list _ _ (list (False-Effect:)) (list (False-Effect:)))
#;(printf "and branch~n")
(ret (Un (-val #f) thn-ty)
;; we change variable effects to type effects in the test,
;; because only the boolean result of the test is used
;; whereas, the actual value of the then branch is returned, not just the boolean result
(append (map var->type-eff tst-thn-eff) thn-thn-eff)
;; no else effects for and, because any branch could have been false
(list))]
;; otherwise this expression has no effects
[_
#;(printf "if base case:~a ~n" (syntax-object->datum tst))
#;(printf "els-ty ~a ~a~n"
els-ty c)
#;(printf "----------------------~nels-ty ~a ~nUn~a~n ~a~n"
els-ty (Un thn-ty els-ty) c)
(ret (Un thn-ty els-ty))])))
;; checking version
(define (tc/if-twoarm/check tst thn els expected)
;; check in the context of the effects, and return
(match-let* ([(tc-result: tst-ty tst-thn-eff tst-els-eff) (tc-expr tst)]
#;[_ (printf "got to here 0~n")]
[(tc-result: thn-ty thn-thn-eff thn-els-eff) (tc-expr/eff #t thn tst-thn-eff expected)]
#;[_ (printf "v is ~a~n" v)]
#;[c (current-milliseconds)]
#;[_ (printf "got to here 1~n")]
[(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff expected)]
#;[_ (printf "got to here 2~n")])
#;(printf "check: v now is ~a~n" (ret els-ty els-thn-eff els-els-eff))
#;(printf "els-ty ~a ~a~n"
els-ty c)
(match (list thn-thn-eff thn-els-eff els-thn-eff els-els-eff)
;; this is the case for `or'
;; the then branch has to be #t
;; the else branch has to be a simple predicate
;; FIXME - can something simpler be done by using demorgan's law?
;; note that demorgan's law doesn't hold for scheme `and' and `or' because they can produce arbitrary values
;; FIXME - mzscheme's or macro doesn't match this!
[(list (list (True-Effect:)) (list (True-Effect:)) (list (Restrict-Effect: t v)) (list (Remove-Effect: t v*)))
(=> unmatch)
;(printf "or branch~n")
(match (list tst-thn-eff tst-els-eff)
;; check that the test was also a simple predicate
[(list (list (Restrict-Effect: s u)) (list (Remove-Effect: s u*)))
(if (and
;; check that all the predicates are for the for the same identifier
(free-identifier=? u u*)
(free-identifier=? v v*)
(free-identifier=? v u))
;; this is just a very simple or
(let ([t (Un (-val #t) els-ty)])
(check-below t expected)
(ret t
;; the then and else effects are just the union of the two types
(list (make-Restrict-Effect (Un s t) v))
(list (make-Remove-Effect (Un s t) v))))
;; otherwise, something complicated is happening and we bail
(unmatch))]
;; similarly, bail here
[_ (unmatch)])]
;; this is the case for `and'
[(list _ _ (list (False-Effect:)) (list (False-Effect:)))
;(printf "and branch~n")
(let ([t (Un thn-ty (-val #f))])
(check-below t expected)
(ret t
;; we change variable effects to type effects in the test,
;; because only the boolean result of the test is used
;; whereas, the actual value of the then branch is returned, not just the boolean result
(append (map var->type-eff tst-thn-eff) thn-thn-eff)
;; no else effects for and, because any branch could have been false
(list)))]
;; otherwise this expression has no effects
[_
(let ([t (Un thn-ty els-ty)])
(check-below t expected)
(ret t))])))
;)

View File

@ -0,0 +1,196 @@
#lang scheme/unit
(require "signatures.ss"
(lib "trace.ss")
(except-in "type-rep.ss" make-arr) ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"type-environments.ss" ;; doesn't need tests
"lexical-env.ss" ;; maybe needs tests
"type-annotation.ss" ;; has tests
"utils.ss"
"type-utils.ss"
"effect-rep.ss"
"tc-utils.ss"
"resolve-type.ss"
(lib "plt-match.ss")
(only-in "type-effect-convenience.ss" [make-arr* make-arr]))
(require (for-template mzscheme "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))))
;; typecheck a single lambda, with argument list and body
;; fixme: abstract the two cases!
;; syntax-list[id] block listof[type] type option[type] -> arr
(define (tc/lambda-clause/check args body arg-tys ret-ty rest-ty)
(syntax-case args ()
[(args* ...)
(if (ormap (lambda (e) (not (type-annotation e))) (syntax->list #'(args* ...)))
(let* ([arg-list (syntax->list #'(args* ...))])
(unless (= (length arg-list) (length arg-tys))
(tc-error "Expected function with ~a arguments, but got function with ~a arguments" (length arg-tys) (length arg-list)))
(for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) arg-list)
(with-lexical-env/extend
arg-list arg-tys
(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 (= 1 (length arg-list)) (remove-var (car arg-list) thn els))
=> (lambda (thn/els) (make-arr arg-tys t #f (car thn/els) (cdr thn/els)))]
;; otherwise, the simple case
[else (make-arr arg-tys t)])]
[t (int-err "bad match - not a tc-result: ~a" t)])))
(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/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 (= 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" t)]))))]
[(args* ... . rest)
(let ([t (tc/lambda-clause args body)])
(check-below (make-Function (list t)) (make-Function (list (make-arr arg-tys ret-ty rest-ty))))
t)]))
;; 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" t)])))]
[(args ... . rest)
(let* ([arg-list (syntax->list #'(args ...))]
[arg-types (map get-type arg-list)]
[rest-type (get-type #'rest)])
(for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) (cons #'rest arg-list))
(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])
(if (pair? (syntax-e s))
(+ 1 (loop (cdr (syntax-e s))))
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: args ret rest _ _)))
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest)]
[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))
(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)
(match expected
[(Poly-names: ns (and expected* (Function: _)))
(with-syntax ()
(let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
(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))])
(tc/mono-lambda formals bodies expected*))])
;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
(ret (make-Poly literal-tvars ty))))]
[_ (tc-error "Expected a value of type ~a, but got a polymorphic function." 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)
#;(printf "formals: ~a~n" (syntax->datum formals))
(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)

View File

@ -0,0 +1,121 @@
#lang scheme/unit
(require "signatures.ss"
"type-effect-convenience.ss"
"lexical-env.ss"
"type-annotation.ss"
"type-alias-env.ss"
"type-env.ss"
"parse-type.ss"
"utils.ss"
syntax/free-vars
mzlib/trace
syntax/kerncase
(for-template
scheme/base
"internal-forms.ss"))
(require (only-in srfi/1 [member member1]))
(import tc-expr^)
(export tc-let^)
(define (do-check expr->type namess types form exprs body clauses expected)
;; just for error reporting
#;(define clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)]))
;; extend the lexical environment for checking the body
(with-lexical-env/extend
;; the list of lists of name
namess
;; the types
types
(for-each (lambda (stx e t) (check-type stx (expr->type e) t))
clauses
exprs
(map list->values-ty 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/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) (member1 n flat-names bound-identifier=?)) (free-vars (car exprs))))
;; then check this expression separately
(let ([t (tc-expr/t (car exprs))])
(with-lexical-env/extend
(list (car names))
(list (get-type/infer (car names) 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 tc-expr/t names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)]))))
(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 exprs)]
;; the annotated types of the name (possibly using the inferred types)
[types (map get-type/infer names inferred-types)]
;; the clauses for error reporting
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
(do-check (lambda (x) x) names types form inferred-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)

View File

@ -0,0 +1,252 @@
#lang scheme/base
(require (lib "struct.ss" "syntax")
(lib "etc.ss")
"type-rep.ss" ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"type-env.ss" ;; maybe needs tests
"type-utils.ss"
"parse-type.ss" ;; has tests
"type-environments.ss" ;; doesn't need tests
"type-name-env.ss" ;; maybe needs tests
"union.ss"
"tc-utils.ss"
"resolve-type.ss"
(lib "kerncase.ss" "syntax")
(lib "trace.ss")
(lib "kw.ss")
(lib "plt-match.ss"))
(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])
(let* ([name (syntax-e nm)]
[fld-types (append parent-field-types types)]
[sty (make-Struct name parent fld-types proc-ty)]
[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)))
;; 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])
;; 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)))
;; register the type name
(register-type-name nm (wrapper sty))
;; register the various function types
(register-type (or maker* maker) (wrapper (->* external-fld-types name)))
(register-types getters
(map (lambda (t) (wrapper (->* (list name) t))) external-fld-types/no-parent))
(when setters?
#;(printf "setters: ~a~n" (syntax-object->datum setters))
(register-types setters
(map (lambda (t) (wrapper (->* (list name t) -Void))) external-fld-types/no-parent)))
(register-type pred (make-pred-ty (wrapper name))))
;; 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))))
;; 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])
;; 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))
;; 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
(syntax-rules (:)
[(_ (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 ...))]))
;; This is going away!
#|
;; parent-nm is an identifier with the name of the defined type
;; variants is (list id id (list (cons id unparsed-type))) - first id is name of variant, second is name of maker,
;; list is name of field w/ type
;; top-pred is an identifier
;; produces void
(define (tc/define-type parent-nm top-pred variants)
;; the symbol and type variable used for parsing
(define parent-sym (syntax-e parent-nm))
(define parent-tvar (make-F parent-sym))
;; create the initial struct type, which contains type variables
(define (mk-initial-variant nm fld-tys-stx)
;; parse the types (recursiveness doesn't matter)
(define-values (fld-tys _) (FIXME parent-sym parent-tvar fld-tys-stx))
(make-Struct (syntax-e nm) #f fld-tys #f))
;; create the union type that is the total type
(define (mk-un-ty parent-sym variant-struct-tys)
(make-Mu parent-sym (apply Un variant-struct-tys)))
;; generate the names and call mk-variant
(define (mk-variant nm maker-name fld-names un-ty variant-struct-ty parent-nm)
;; construct the actual type of this variant
(define variant-ty (subst parent-nm un-ty variant-struct-ty))
;; the fields of this variant
(match-define (Struct: _ _ fld-types _) variant-ty)
;; register all the types (with custon maker name)
(register-struct-types nm variant-ty fld-names fld-types fld-types #f #:maker maker-name))
;; all the names
(define variant-names (map car variants))
(define variant-makers (map cadr variants))
(define variant-flds (map caddr variants))
;; create the initial variants, which don't have the parent substituted in
(define variant-struct-tys (map (lambda (n flds) (mk-initial-variant n (map car flds))) variant-names variant-flds))
;; just the names of each variant's fields
(define variant-fld-names (map (lambda (x) (map cdr x)) variant-flds))
;; the type of the parent
(define un-ty (mk-un-ty parent-sym variant-struct-tys))
;; register the types for the parent
(register-type top-pred (make-pred-ty un-ty))
(register-type-name parent-nm un-ty)
;; construct all the variants, and register the appropriate names
(for-each (lambda (nm mk fld-names sty) (mk-variant nm mk fld-names un-ty sty parent-sym))
variant-names variant-makers variant-fld-names variant-struct-tys))
|#

View File

@ -0,0 +1,245 @@
#lang scheme/unit
(require syntax/kerncase
mzlib/etc
mzlib/plt-match
"signatures.ss"
"tc-structs.ss"
"type-utils.ss"
"utils.ss" ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"internal-forms.ss" ;; doesn't need tests
"type-env.ss" ;; maybe needs tests
"parse-type.ss" ;; has tests
"tc-utils.ss" ;; doesn't need tests
"type-annotation.ss" ;; has tests
"type-name-env.ss" ;; maybe needs tests
"init-envs.ss"
"mutated-vars.ss"
"def-binding.ss"
"provide-handling.ss"
"type-alias-env.ss"
"type-contract.ss"
(only-in "prims.ss" :)
(for-template
(only-in "prims.ss" :)
"internal-forms.ss"
"tc-utils.ss"
(lib "contract.ss")
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] ...) #:maker m)) (#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:maker #'m)]
;; 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 ts vars))]
;; 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)]) (tc-expr #'expr)))
=> (match-lambda
[(tc-result: t)
(register-type (car vars) t)
(list (car vars) 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 (list->values-ty 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 (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)
;; 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)
(tc-toplevel/pass2 form))

View File

@ -0,0 +1,88 @@
(module tc-utils mzscheme
(provide (all-defined))
(require (lib "list.ss") (lib "etc.ss")
"syntax-traversal.ss")
;; 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))
;; 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))
(look-for-in-orig omodule emodule stx))
;; produce a type error, using the current syntax
(define (tc-error msg . rest)
(define cur-stx
(begin
;(printf "stx : ~a~n" (current-orig-stx))
(if (print-syntax?)
(current-orig-stx)
(locate-stx (current-orig-stx)))))
;(printf "Aliases: ~a~n" ((current-type-names)))
(raise-syntax-error 'typecheck (apply format msg rest) cur-stx cur-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 () '())))
;; error for unbound variables
(define (lookup-fail e) (tc-error "unbound identifier ~a" e))
;; 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))
(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))))
)

View File

@ -0,0 +1,54 @@
(module tool mzscheme
(require (lib "unit.ss")
(lib "class.ss")
(lib "tool.ss" "drscheme")
(lib "string-constant.ss" "string-constants")
(prefix r: "../typed-reader.ss"))
(provide tool@)
(define tool@
(unit
(import drscheme:tool^)
(export drscheme:tool-exports^)
(define mbl% (drscheme:language:module-based-language->language-mixin
(drscheme:language:simple-module-based-language->module-based-language-mixin
drscheme:language:simple-module-based-language%)))
(define planet-module '(planet "typed-scheme.ss" ("plt" "typed-scheme.plt" 3)))
(define (typed-scheme-language% cl%)
(class* cl% (drscheme:language:simple-module-based-language<%>)
(define/override (get-language-numbers)
'(1000 -401))
(define/override (get-language-name) "Typed Scheme")
(define/override (get-language-position)
(list (string-constant experimental-languages) "Typed Scheme"))
(define/override (get-module) planet-module)
(define/override (get-reader)
(lambda (src port)
(let ([v (r:read-syntax src port)])
(if (eof-object? v)
v
(namespace-syntax-introduce v)))))
(define/override (get-one-line-summary)
"Scheme with types!")
(define/override (get-language-url) "http://www.ccs.neu.edu/~samth/typed-scheme.html")
(define/override (enable-macro-stepper?) #t)
(define/override (use-namespace-require/copy?) #f)
(super-new [module (get-module)] [language-position (get-language-position)])))
(define (phase1) (void))
(define (phase2)
(drscheme:language-configuration:add-language
(make-object (typed-scheme-language%
((drscheme:language:get-default-mixin)
mbl%)))))))
)

View File

@ -0,0 +1,65 @@
#lang scheme/base
(require syntax/boundmap
"tc-utils.ss"
mzlib/trace
mzlib/plt-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)
(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)))))

View File

@ -0,0 +1,92 @@
#lang scheme/base
(require "type-rep.ss" "parse-type.ss" "tc-utils.ss" "subtype.ss" "utils.ss" "union.ss" "resolve-type.ss"
"type-env.ss")
(require (lib "plt-match.ss"))
(provide type-annotation
get-type
get-type/infer
type-label-symbol
type-ascrip-symbol
check-type)
(define type-label-symbol 'type-label)
(define type-ascrip-symbol 'type-ascription)
(define (print-size stx)
(syntax-case stx ()
[(a . b) (begin
(printf/log "Annotation Sexp Pair ~n")
(print-size #'a)
(print-size #'b))]
[_ (printf/log "Annotation Sexp ~n" )]))
;; get the type annotation of this syntax
;; syntax -> Maybe[Type]
(define (type-annotation stx)
(define (pt prop)
(print-size prop)
(if (syntax? prop)
(parse-type prop)
(parse-type/id stx prop)))
(cond
[(syntax-property stx type-label-symbol) => pt]
[(syntax-property stx type-ascrip-symbol) => pt]
[(and (identifier? stx) (lookup-type stx (lambda () #f)))
=>
(lambda (t)
(maybe-finish-register-type stx)
t)]
[else #f]))
(define (log/ann stx ty)
(printf/log "Required Annotated Variable: ~a ~a~n" (syntax-e stx) ty))
(define (log/extra stx ty ty2)
(printf/log "Extra Annotated Variable: ~a ~a ~a~n" (syntax-e stx) ty ty2))
(define (log/noann stx ty)
(printf/log "Unannotated Variable: ~a ~a~n" (syntax-e stx) ty))
;; get the type annotation of this identifier, otherwise error
;; identifier -> Type
(define (get-type stx)
(parameterize
([current-orig-stx stx])
(cond
[(type-annotation stx) => (lambda (x)
(log/ann stx x)
x)]
[(not (syntax-original? stx))
(tc-error "untyped var: ~a" (syntax-e stx))]
[else
(tc-error "no type information on variable ~a" (syntax-e stx))])))
;; get the type annotations on this list of identifiers
;; if not all identifiers have annotations, return the supplied inferred type
;; list[identifier] type -> list[type]
(define (get-type/infer stxs e-type)
(match (list stxs e-type)
[(list '() (Values: '())) (list)]
[(list (list stx ...) (Values: (list ty ...)))
(map (lambda (stx ty)
(cond [(type-annotation stx) => (lambda (ann) (check-type stx ty ann) (log/extra stx ty ann) ann)]
[else (log/noann stx ty) ty]))
stx ty)]
[(list (list stx) ty)
(cond [(type-annotation stx) => (lambda (ann)
(check-type stx ty ann)
(log/extra stx ty ann)
(list ann))]
[else (log/noann stx ty) (list ty)])]
[else (int-err "wrong type arity - get-type/infer ~a ~a" stxs e-type)]))
;; check that e-type is compatible with ty in context of stx
;; otherwise, error
;; syntax type type -> void
(define (check-type stx e-type ty)
(let ([stx* (current-orig-stx)])
(parameterize ([current-orig-stx stx])
(unless (subtype e-type ty)
;(printf "orig-stx: ~a" (syntax->datum stx*))
(tc-error "Body had type:~n~a~nVariable had type:~n~a~n" e-type ty)))))

View File

@ -0,0 +1,8 @@
(module type-comparison mzscheme
(require "type-rep.ss" "type-utils.ss")
(provide type-equal? tc-result-equal? type<? type-compare effects-equal?)
)

View File

@ -0,0 +1,131 @@
(module type-contract mzscheme
(provide type->contract define/fixup-contract? generate-contract-def change-contract-fixups)
(require
"type-rep.ss"
"parse-type.ss"
"utils.ss"
"type-name-env.ss"
"require-contract.ss"
"internal-forms.ss"
"tc-utils.ss"
"resolve-type.ss"
"type-utils.ss"
mzlib/list
(only "type-effect-convenience.ss" Any-Syntax))
(require
(lib "plt-match.ss")
(lib "struct.ss" "syntax")
(lib "stx.ss" "syntax")
(lib "trace.ss")
(only (lib "contract.ss") -> ->* case-> cons/c flat-rec-contract)
(lib "etc.ss")
(lib "struct.ss")
#;(lib "syntax-browser.ss" "macro-debugger"))
(require-for-template mzscheme (lib "contract.ss") (only scheme/class object%))
(define (define/fixup-contract? stx)
(syntax-property stx 'typechecker:contract-def))
(define (generate-contract-def stx)
(define prop (syntax-property stx 'typechecker:contract-def))
(define typ (parse-type prop))
(syntax-case stx (define-values)
[(_ (n) __)
(with-syntax ([cnt (type->contract typ (lambda () (tc-error/stx prop "Type ~a could not be converted to a contract." typ)))])
(syntax/loc stx (define-values (n) cnt)))]
[_ (int-err "should never happen - not a define-values: ~a" (syntax-object->datum stx))]))
(define (change-contract-fixups forms)
(map (lambda (e)
(if (not (define/fixup-contract? e))
e
(generate-contract-def e)))
(syntax->list forms)))
(define (type->contract ty fail)
(define vars (make-parameter '()))
(let/cc exit
(let t->c ([ty ty])
(match ty
[(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
[(Univ:) #'any/c]
;; we special-case lists:
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
#`(listof #,(t->c elem-ty))]
[(? (lambda (e) (eq? Any-Syntax e))) #'syntax?]
[(Base: sym)
(case sym
[(Number) #'number?]
[(Boolean) #'boolean?]
[(Keyword) #'keyword?]
[(Port) #'port?]
[(Path) #'path?]
[(String) #'string?]
[(Symbol) #'symbol?]
[(Bytes) #'bytes?]
[(Void) #'void?]
[(Syntax) #'syntax?]
[(Output-Port) #'output-port?]
[(Input-Port) #'input-port?]
[(Char) #'char?]
[(Namespace) #'namespace?]
[else (int-err "Base type ~a cannot be converted to contract" sym)])]
[(Union: elems)
(with-syntax
([cnts (map t->c elems)])
#;(printf "~a~n" (syntax-object->datum #'cnts))
#'(or/c . cnts))]
[(Function: arrs)
(let ()
(define (f a)
(define-values (dom* rngs* rst)
(match a
[(arr: dom (Values: rngs) #f _ _)
(values (map t->c dom) (map t->c rngs) #f)]
[(arr: dom rng #f _ _)
(values (map t->c dom) (list (t->c rng)) #f)]
[(arr: dom (Values: rngs) rst _ _)
(values (map t->c dom) (map t->c rngs) (t->c rst))]
[(arr: dom rng rst _ _)
(values (map t->c dom) (list (t->c rng)) (t->c rst))]))
(with-syntax
([(dom* ...) dom*]
[(rng* ...) rngs*]
[rst* rst])
(if rst
#'((dom* ...) (listof rst*) . ->* . (rng* ...))
#'((dom* ...) . ->* . (rng* ...)))))
(let ([l (map f arrs)])
(if (and (pair? l) (null? (cdr l)))
(car l)
#`(case-> #,@l))))]
[(Vector: t)
#`(vectorof #,(t->c t))]
[(Pair: t1 t2)
#`(cons/c #,(t->c t1) #,(t->c t2))]
[(Opaque: p? cert)
#`(flat-contract #,(cert p?))]
[(F: v) (cond [(assoc v (vars)) => cadr]
[else (int-err "unknown var: ~a" v)])]
[(Mu: n b)
(with-syntax ([(n*) (generate-temporaries (list n))])
(parameterize ([vars (cons (list n #'n*) (vars))])
#`(flat-rec-contract n* #,(t->c b))))]
[(Value: #f) #'false/c]
[(Instance: _) #'(is-a?/c object%)]
[(Class: _ _ _) #'(subclass?/c object%)]
[(Value: '()) #'null?]
[(Syntax: (Base: 'Symbol)) #'identifier?]
[(Syntax: t)
(if (equal? ty Any-Syntax)
#`syntax?
#`(syntax/c #,(t->c t)))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x #,v)))]
[else (exit (fail))]))))
)

View File

@ -0,0 +1,231 @@
(module type-effect-convenience scheme/base
(require "type-rep.ss"
"effect-rep.ss"
mzlib/plt-match
"type-comparison.ss"
"type-effect-printer.ss"
"union.ss"
"subtype.ss"
"type-utils.ss"
(lib "list.ss")
scheme/promise
(prefix-in 1: srfi/1)
(for-syntax scheme/base))
(provide (all-defined-out))
(define (-vet id) (make-Var-True-Effect id))
(define (-vef id) (make-Var-False-Effect id))
(define -rem make-Remove-Effect)
(define -rest make-Restrict-Effect)
(define (var->type-eff eff)
(match eff
[(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
[(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
[_ eff]))
(define ((add-var v) eff)
(match eff
[(Latent-Var-True-Effect:) (-vet v)]
[(Latent-Var-False-Effect:) (-vef v)]
[(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
[(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)]))
(define-syntax ->
(syntax-rules (:)
[(_ dom ... rng)
(->* (list dom ...) rng)]
[(_ dom ... rng : eff1 eff2)
(->* (list dom ...) : eff1 eff2)]))
(define-syntax ->*
(syntax-rules (:)
[(_ dom rng)
(make-Function (list (make-arr* dom rng)))]
[(_ dom rst rng)
(make-Function (list (make-arr* dom rng rst)))]
[(_ dom rng : eff1 eff2)
(make-Function (list (make-arr* dom rng #f eff1 eff2)))]
[(_ dom rst rng : eff1 eff2)
(make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
(define-syntax cl->
(syntax-rules (:)
[(_ [(dom ...) rng] ...)
(make-Function (list (make-arr* (list dom ...) rng) ...))]
[(_ [(dom ...) rng : eff1 eff2] ...)
(make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
[(_ [(dom ...) rng rst : eff1 eff2] ...)
(make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
(define (cl->* . args)
(define (funty-arities f)
(match f
[(Function: as) as]))
(make-Function (map car (map funty-arities args))))
(define make-arr*
(case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
[(dom rng rest) (make-arr dom rng rest (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest eff1 eff2)]))
(define (make-promise-ty t)
(make-Struct (string->uninterned-symbol "Promise") #f (list t) #f))
(define N (make-Base 'Number))
(define -Integer (make-Base 'Integer))
(define B (make-Base 'Boolean))
(define Sym (make-Base 'Symbol))
(define -Void (make-Base 'Void))
(define -Bytes (make-Base 'Bytes))
(define -Regexp (make-Base 'Regexp))
(define -PRegexp (make-Base 'PRegexp))
(define -Byte-Regexp (make-Base 'Byte-Regexp))
(define -Byte-PRegexp (make-Base 'Byte-PRegexp))
(define -String (make-Base 'String))
(define -Keyword (make-Base 'Keyword))
(define -Char (make-Base 'Char))
(define -Syntax make-Syntax)
(define -Prompt-Tag (make-Base 'Prompt-Tag))
(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set))
(define -Path (make-Base 'Path))
(define -Namespace (make-Base 'Namespace))
(define -Output-Port (make-Base 'Output-Port))
(define -Input-Port (make-Base 'Input-Port))
(define -HT make-Hashtable)
(define -Promise make-promise-ty)
(define Univ (make-Univ))
(define-syntax -v
(syntax-rules ()
[(_ x) (make-F 'x)]))
(define-syntax -poly
(syntax-rules ()
[(_ (vars ...) ty)
(let ([vars (-v vars)] ...)
(make-Poly (list 'vars ...) ty))]))
(define-syntax -mu
(syntax-rules ()
[(_ var ty)
(let ([var (-v var)])
(make-Mu 'var ty))]))
(define -values make-Values)
;; produce the appropriate type of a list of types
;; that is - if there is exactly one type, just produce it, otherwise produce a values-ty
;; list[type] -> type
(define (list->values-ty l)
(if (= 1 (length l)) (car l) (-values l)))
(define-syntax *Un
(syntax-rules ()
[(_ . args) (make-Union (list . args))]))
(define -pair make-Pair)
(define -base make-Base)
(define -struct make-Struct)
(define -val make-Value)
(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
(define -lst make-Listof)
(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
(define -Port (*Un -Input-Port -Output-Port))
(define (-lst* . args) (if (null? args)
(-val null)
(-pair (car args) (apply -lst* (cdr args)))))
#;(define NE (-mu x (Un N (make-Listof x))))
(define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
(define (Un/eff . args)
(apply Un (map tc-result-t args)))
(define -Param make-Param)
(define make-pred-ty
(case-lambda
[(in out t)
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
[(t) (make-pred-ty (list Univ) B t)]))
(define -Pathlike (*Un -Path -String))
(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
(define -Byte N)
(define (-Tuple l)
(foldr -pair (-val '()) l))
(define Any-Syntax
(-mu x
(-Syntax (*Un
(-lst x)
(-mu y (*Un x (-pair x y)))
(make-Vector x)
(make-Box x)
N
B
-String
Sym))))
(define Ident (-Syntax Sym))
;; DO NOT USE if t contains #f
(define (-opt t) (*Un (-val #f) t))
(define-syntax (make-env stx)
(syntax-case stx ()
[(_ e ...)
#`(list
#,@(map (lambda (e)
(syntax-case e ()
[(nm ty)
(identifier? #'nm)
#`(list #'nm ty)]
[(e ty extra-mods ...)
#'(list (let ([new-ns
(let* ([ns (make-empty-namespace)])
(namespace-attach-module (current-namespace)
'scheme/base
ns)
ns)])
(parameterize ([current-namespace new-ns])
(namespace-require 'extra-mods) ...
e))
ty)]))
(syntax->list #'(e ...))))]))
;; if t is of the form (Pair t* (Pair t* ... (Listof t*)))
;; return t*
;; otherwise, return t
;; generalize : Type -> Type
(define (generalize t)
(let/ec exit
(let loop ([t* t])
(match t*
[(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
[(Pair: t1 t2)
(let ([t-new (loop t2)])
(if (type-equal? (-lst t1) t-new)
t-new
(exit t)))]
[_ (exit t)]))))
)

View File

@ -0,0 +1,145 @@
(module type-effect-printer mzscheme
(require "type-rep.ss" "effect-rep.ss" "rep-utils.ss" "tc-utils.ss")
(require (lib "plt-match.ss"))
(require "planet-requires.ss")
;; do we attempt to find instantiations of polymorphic types to print?
;; FIXME - currently broken
(define print-poly-types? #f)
;; do we use simple type aliases in printing
(define print-aliases #t)
;; does t have a type name associated with it currently?
;; has-name : Type -> Maybe[Symbol]
(define (has-name? t)
(define ns ((current-type-names)))
(let/cc return
(unless print-aliases
(return #f))
(for-each
(lambda (pair)
(cond [(eq? t (cdr pair))
(return (car pair))]))
ns)
#f))
;; print out an effect
;; print-effect : Effect Port Boolean -> Void
(define (print-effect c port write?)
(define (fp . args) (apply fprintf port args))
(match c
[(Restrict-Effect: t v) (fp "(restrict ~a ~a)" t (syntax-e v))]
[(Remove-Effect: t v) (fp "(remove ~a ~a)" t (syntax-e v))]
[(Latent-Restrict-Effect: t) (fp "(restrict ~a)" t)]
[(Latent-Remove-Effect: t) (fp "(remove ~a)" t)]
[(Latent-Var-True-Effect:) (fp "(var #t)")]
[(Latent-Var-False-Effect:) (fp "(var #f)")]
[(True-Effect:) (fp "T")]
[(False-Effect:) (fp "F")]
[(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))]
[(Var-False-Effect: v) (fp "(var #f ~a)" (syntax-e v))]))
;; print out a type
;; print-type : Type Port Boolean -> Void
(define (print-type c port write?)
(define (fp . args) (apply fprintf port args))
(define (print-arr a)
(match a
[(top-arr:)
(fp "Procedure")]
[(arr: dom rng rest thn-eff els-eff)
(fp "(")
(for-each (lambda (t) (fp "~a " t)) dom)
(when rest
(fp "~a .. " rest))
(fp "-> ~a" rng)
(unless (and (null? thn-eff) (null? els-eff))
(fp " : ~a ~a" thn-eff els-eff))
(fp ")")]))
(define (tuple? t)
(match t
[(Pair: a (? tuple?)) #t]
[(Value: '()) #t]
[_ #f]))
(define (tuple-elems t)
(match t
[(Pair: a e) (cons a (tuple-elems e))]
[(Value: '()) null]))
;(fp "~a~n" (Type-seq c))
(match c
[(Univ:) (fp "Any")]
[(? has-name?) (fp "~a" (has-name? c))]
;; names are just the printed as the original syntax
[(Name: stx) (fp "[~a]" (syntax-e stx))]
[(App: rator rands stx)
(fp "~a" (cons rator rands))]
;; special cases for lists
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
(fp "(Listof ~a)" elem-ty)]
[(Mu: var (Union: (list (Pair: elem-ty (F: var)) (Value: '()))))
(fp "(Listof ~a)" elem-ty)]
[(Value: v) (cond [(or (symbol? v) (null? v))
(fp "'~a" v)]
[else (fp "~a" v)])]
[(? tuple? t)
(fp "~a" (cons 'List (tuple-elems t)))]
[(Base: n) (fp "~a" n)]
[(Opaque: pred _) (fp "(Opaque ~a)" (syntax-object->datum pred))]
[(Struct: 'Promise par (list fld) proc) (fp "(Promise ~a)" fld)]
[(Struct: nm par flds proc)
(fp "#(struct:~a ~a" nm flds)
(when proc
(fp " ~a" proc))
(fp ")")]
[(Function: arities)
(let ()
(match arities
[(list) (fp "(case-lambda)")]
[(list a) (print-arr a)]
[(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
[(arr: _ _ _ _ _) (print-arr c)]
[(Vector: e) (fp "(Vectorof ~a)" e)]
[(Box: e) (fp "(Box ~a)" e)]
[(Union: elems) (fp "~a" (cons 'U elems))]
[(Pair: l r) (fp "(Pair ~a ~a)" l r)]
[(F: nm) (fp "<~a>" nm)]
[(Values: (list v ...)) (fp "~a" (cons 'values v))]
[(Param: in out)
(if (equal? in out)
(fp "(Paramter ~a)" in)
(fp "(Parameter ~a ~a)" in out))]
[(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
#;
[(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
[(Poly-names: names body)
#;(fprintf (current-error-port) "POLY SEQ: ~a~n" (Type-seq body))
(fp "(All ~a ~a)" names body)]
#;
[(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)]
[(Mu: x (Syntax: (Union: (list
(Base: 'Number)
(Base: 'Boolean)
(Base: 'Symbol)
(Base: 'String)
(Mu: var (Union: (list (Value: '()) (Pair: (F: x) (F: var)))))
(Mu: y (Union: (list (F: x) (Pair: (F: x) (F: y)))))
(Vector: (F: x))
(Box: (F: x))))))
(fp "SyntaxObject")]
[(Mu-name: name body) (fp "(mu ~a ~a ~a)" (Type-seq c) name body)]
;; FIXME - this should not be used
#;
[(Scope: sc) (fp "(Scope ~a)" sc)]
#;
[(B: idx) (fp "(B ~a)" idx)]
[(Syntax: t) (fp "(Syntax ~a)" t)]
[(Instance: t) (fp "(Instance ~a)" t)]
[(Class: pf nf ms) (fp "(Class)")]
[else (fp "Unknown Type: ~a" (struct->vector c))]
))
(set-box! print-type* print-type)
(set-box! print-effect* print-effect)
)

View File

@ -0,0 +1,61 @@
#lang scheme/base
(require (lib "boundmap.ss" "syntax")
"tc-utils.ss")
(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)
(module-identifier-mapping-put! the-mapping id type))
;; add a single type to the mapping
;; identifier type -> void
(define (register-type/undefined id type)
(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))

View File

@ -0,0 +1,60 @@
(module type-environments mzscheme
(provide current-tvars
extend
lookup
make-empty-env
extend-env
extend/values
initial-tvar-env)
(require (lib "plt-match.ss")
(lib "list.ss")
"tc-utils.ss")
;; 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? '()))
;; 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))
)

View File

@ -0,0 +1,44 @@
#lang scheme/base
(require syntax/boundmap
mzlib/trace
"tc-utils.ss")
(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))

View File

@ -0,0 +1,434 @@
#lang scheme/base
(require (lib "plt-match.ss"))
(require (lib "etc.ss") (lib "list.ss"))
(require "planet-requires.ss" "rep-utils.ss" "effect-rep.ss" "tc-utils.ss"
"free-variance.ss")
(require (prefix-in 1: (lib "list.ss" "srfi" "1"))
(lib "trace.ss")
(for-syntax scheme/base))
(define name-table (make-hash-table 'weak))
;; 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-hash-table (list (cons i Covariant)))]
[#:fold-rhs #:base])
;; n is a Name
(dt F (n) [#:frees (make-immutable-hash-table (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*))))])
;; 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
(dt Struct (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)))])
;; dom : Listof[Type]
;; rng : Type
;; rest : Type
;; thn-eff : Effect
;; els-eff : Effect
;; arr is NOT a Type
(dt arr (dom rng rest thn-eff els-eff)
[#:frees (combine-frees (append (map flip-variances (map free-vars* dom))
(map free-vars* (append (list rng)
(if rest (list rest) null)
thn-eff
els-eff))))
(combine-frees (append (map flip-variances (map free-idxs* dom))
(map free-idxs* (append (list rng)
(if rest (list rest) null)
thn-eff
els-eff))))]
[#:fold-rhs (*arr (map type-rec-id dom)
(type-rec-id rng)
(and rest (type-rec-id rest))
(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) [#:frees (combine-frees (map free-vars* types))
(combine-frees (map free-idxs* types))]
[#:fold-rhs (*Values (map type-rec-id types))])
;; 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-table-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-table-put! ht (syntax-e #'kw) (list #'mtch
(syntax/loc cl (pats ...))
(lambda (tr er) #'expr)))]
[(kw pats ... expr)
(hash-table-put! ht (syntax-e #'kw) (list (mk-matcher (syntax-e #'kw))
(syntax/loc cl (pats ...))
(lambda (tr er) #'expr)))]))
(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 pat (quasisyntax/loc pats (#,match-ex . #,pats)))
(define cl (quasisyntax/loc match-ex (#,pat #,(body-f rid erid))))
cl)
(syntax-case stx ()
[(tc rec-id ty [kw pats ... es] ...)
#;(andmap (lambda (k) (keyword? (syntax-e k))) (syntax->list #'(kw ...)))
(syntax/loc stx (tc rec-id (lambda (e) (sub-eff rec-id e)) ty [kw pats ... es] ...))]
[(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-table-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<?)))]
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 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
(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<?)))]
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 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-table-put! 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-table-put! name-table v names)
v)))
;; the 'smart' destructor
(define (Poly-body* names t)
(match t
[(Poly: n scope)
(unless (= (length names) n)
(error "Wrong number of 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 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-table-get 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-table-get name-table t)])
(list syms (Poly-body* syms t))))
(list nps bp)))])))
;; unfold : Type -> Type
;; must be applied to a Mu
(define (unfold t)
(match t
[(Mu: sc) (instantiate t sc)]
[_ (int-err "unfold: requires Mu type, got ~a" t)]))
;; 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]))
;(trace subst subst-all)
(provide
unfold
Mu-name: Poly-names:
Type-seq Effect-seq
Mu-unsafe: Poly-unsafe:
Mu? Poly?
arr
Type? Effect?
Poly-n
free-vars*
type-equal? type-compare type<?
remove-dups
(rename-out [Mu:* Mu:]
[Poly:* Poly:]
[Mu* make-Mu]
[Poly* make-Poly]
[Mu-body* Mu-body]
[Poly-body* Poly-body]))
;(trace unfold)

View File

@ -0,0 +1,78 @@
#lang scheme/base
(require "type-rep.ss"
"effect-rep.ss"
"tc-utils.ss"
"rep-utils.ss"
"free-variance.ss"
mzlib/plt-match
(for-syntax scheme/base))
(provide fv fv/list
substitute
subst-all
subst
ret
instantiate-poly
tc-result:
tc-result-equal?
effects-equal?
tc-result-t)
;; substitute : Type Name Type -> Type
(define (substitute image name target)
(define (sb t) (substitute image name t))
(if (hash-table-get (free-vars* target) name #f)
(type-case sb target
[#:F name* (if (eq? name* name) image target)])
target))
;; substitute many variables
;; substitution = Listof[List[Name,Type]]
;; subst-all : substition Type -> Type
(define (subst-all s t)
(foldr (lambda (e acc) (substitute (cadr e) (car e) acc)) t s))
(define (instantiate-poly t types)
(match t
[(Poly: ns body)
(unless (= (length types) (length ns))
(int-err "instantiate-poly: wrong number of types: expected ~a, got ~a" (length ns) (length types)))
(subst-all (map list ns types) body)]
[_ (int-err "instantiate-many: requires Poly type, got ~a" t)]))
;; this structure represents the result of typechecking an expression
(define-struct tc-result (t thn els) #:inspector #f)
(define-match-expander tc-result:
(lambda (stx)
(syntax-case stx ()
[(form pt) #'(struct tc-result (pt _ _))]
[(form pt pe1 pe2) #'(struct tc-result (pt pe1 pe2))])))
;; convenience function for returning the result of typechecking an expression
(define ret
(case-lambda [(t) (make-tc-result t (list) (list))]
[(t thn els) (make-tc-result t thn els)]))
(define (subst v t e) (substitute t v e))
;; type comparison
;; equality - good
(define tc-result-equal? equal?)
(define (effects-equal? fs1 fs2) (andmap eq? fs1 fs2))
;; fv : Type -> Listof[Name]
(define (fv t) (hash-table-map (free-vars* t) (lambda (k v) k)))
;; fv/list : Listof[Type] -> Listof[Name]
(define (fv/list ts) (hash-table-map (combine-frees (map free-vars* ts)) (lambda (k v) k)))

View File

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

View File

@ -0,0 +1,106 @@
#lang scheme/base
(require "planet-requires.ss"
"type-rep.ss"
"effect-rep.ss"
"type-comparison.ss"
"resolve-type.ss"
"type-utils.ss")
(require mzlib/plt-match
mzlib/trace)
(provide unify1)
;; the types in the constraint list must be well-formed
(define (unify cl) (unify/acc cl '()))
(define (unify1 t1 t2) (unify (list (list t1 t2))))
(define (unify/acc constraint-list acc)
(parameterize ([match-equality-test type-equal?])
(match constraint-list
;; done!
[(list) acc]
;; equal constraints can be discarded
[(list (list t t) rest ...) (unify/acc rest acc)]
;; name resolution
[(list (list (Name: n) (Name: n*)) rest ...)
(if (free-identifier=? n n*)
(unify/acc rest acc)
#f)]
;; type application
[(list (list (App: r args _) (App: r* args* _)) rest ...)
(unify/acc (append (map list (cons r args) (cons r* args*)) rest) acc)]
;; unequal bound variables do not unify
[(list (list (B: _) (B: _)) rest ...) #f]
;; unify a variable (skipping the occurs check for now)
[(list (list (F: v) t) rest ...)
(unify/acc (map (lambda (p) (map (lambda (e) (subst v t e)) p)) rest)
(cons (list v t) acc))]
[(list (list t (F: v)) rest ...)
(unify/acc (map (lambda (p) (map (lambda (e) (subst v t e)) p)) rest)
(cons (list v t) acc))]
;; arrow types - just add a whole bunch of new constraints
[(list (list (Function: (list (arr: ts t t-rest t-thn-eff t-els-eff) ...))
(Function: (list (arr: ss s s-rest s-thn-eff s-els-eff) ...)))
rest ...)
#;(printf "arrow unification~n")
(let ()
(define (compatible-rest t-rest s-rest)
(andmap (lambda (x y) (or (and x y) (and (not x) (not y)))) ;; either both #f or both not #f
t-rest s-rest))
(define (flatten/zip x y) (map list (apply append x) (apply append y)))
(if (and (= (length ts) (length ss))
(compatible-rest t-rest s-rest)
(effects-equal? t-thn-eff s-thn-eff)
(effects-equal? t-els-eff s-els-eff))
(let ([ret-constraints (map list t s)]
;; remove the #f's before adding to the constraints
[rest-constraints (map list (filter values t-rest) (filter values s-rest))]
;; transform ((a b c) (d e)) ((1 2 3) (4 5)) into ((a 1) (b 2) (c 3) (d 4) (e 5))
[arg-constraints (flatten/zip ts ss)])
#;(printf "constraints ~a~n"(append ret-constraints rest-constraints arg-constraints))
(unify/acc (append arg-constraints rest-constraints ret-constraints rest) acc))
(begin #;(printf "failure!~n") #f)))]
;; aggregate types are simple
[(list (list (Vector: t) (Vector: s)) rest ...) (unify/acc (cons (list t s) rest) acc)]
[(list (list (Pair: t1 t2) (Pair: s1 s2)) rest ...)
(unify/acc (list* (list t1 s1) (list t2 s2) rest) acc)]
[(list (list (Hashtable: t1 t2) (Hashtable: s1 s2)) rest ...)
(unify/acc (list* (list t1 s1) (list t2 s2) rest) acc)]
[(list (list (Param: t1 t2) (Param: s1 s2)) rest ...)
(unify/acc (list* (list t1 s1) (list t2 s2) rest) acc)]
;; structs
[(list (list (Struct: nm p elems proc) (Struct: nm p elems* proc*)) rest ...)
(cond [(and proc proc*)
(unify/acc (append rest (map list elems elems*) (list (list proc proc*))) acc)]
[(or proc proc*) #f]
[else (unify/acc (append rest (map list elems elems*)) acc)])]
;; union types - oh no!
[(list (list (Union: l1) (Union: l2)) rest ...)
(and (= (length l1) (length l2))
(unify/acc (append (map list l1 l2) rest) acc))]
[(list (or (list (Union: _) _) (list _ (Union: _))) rest ...)
#;(printf "FIXME: union type ~n~a~n---------~n~a~n in unifier~n"
(caar constraint-list)
(cadar constraint-list))
#f]
;; mu types
[(list (list (Mu-unsafe: s) (Mu-unsafe: t)) rest ...)
(unify/acc (cons (list s t) rest) acc)]
[(list (list t (? Mu? s)) rest ...) (unify/acc (cons (list t (unfold s)) rest) acc)]
[(list (list (? Mu? s) t) rest ...) (unify/acc (cons (list (unfold s) t) rest) acc)]
#;[((or (($ mu _ _) _) (_ ($ mu _ _))) rest ...)
(printf "FIXME: mu types ~a in unifier~n" constraint-list)
#f]
;; polymorphic types - don't do that
[(list (or (list _ (? Poly?)) (list _ (? Poly?))) rest ...)
;(printf "FIXME: poly type in unifier~n")
#f]
;; nothing else can have type variables
[else #f]
)))
;(trace unify/acc)

View File

@ -0,0 +1,62 @@
(module union mzscheme
(require "type-rep.ss" "subtype.ss" "tc-utils.ss"
"type-effect-printer.ss" "rep-utils.ss"
"type-comparison.ss")
(require (lib "plt-match.ss") (lib "list.ss") (lib "trace.ss"))
(provide Un #;(rename *Un Un))
(define (make-union* set)
(match set
[(list t) t]
[_ (make-Union set)]))
(define empty-union (make-Union null))
(define (flat t)
(match t
[(Union: es) es]
[_ (list t)]))
#;(define (Values-types t) (match t [(Values: ts) ts]))
(define (remove-subtypes ts)
(let loop ([ts* ts] [result '()])
(cond [(null? ts*) (reverse result)]
[(ormap (lambda (t) (subtype (car ts*) t)) result) (loop (cdr ts*) result)]
[else (loop (cdr ts*) (cons (car ts*) result))])))
(define Un
(case-lambda
[() empty-union]
[args
;; a is a Type (not a union type)
;; b is a List[Type]
(define (union2 a b)
(define b* (make-union* b))
(cond
[(subtype a b*) (list b*)]
[(subtype b* a) (list a)]
[else (cons a b)]))
#;(union-count!)
(let ([types (remove-dups (sort (apply append (map flat args)) type<?))])
(cond
[(null? types) (make-union* null)]
[(null? (cdr types)) (car types)]
[(ormap Values? types)
(if (andmap Values? types)
(make-Values (apply map Un (map Values-types types)))
(int-err "Un: should not take the union of multiple values with some other type: ~a" types))]
[else (make-union* #;(remove-subtypes types) (foldr union2 null types))]))]))
#;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)
#;(define (*Un . args) (Un-intern args))
;(trace Un)
(define (u-maker args) (apply Un args))
;(trace u-maker)
(set-union-maker! u-maker)
)

View File

@ -0,0 +1,93 @@
(module unit-utils mzscheme
(require (lib "unit.ss"))
(require-for-syntax (lib "unit-exptime.ss")
(lib "list.ss" "srfi" "1")
(lib "match.ss"))
(provide define-values/link-units/infer)
(define-syntax (define-values/link-units/infer stx)
;; construct something we can put in the imports/exports clause from the datum
(define (datum->sig-elem d)
(if (car d)
(quasisyntax/loc (cdr d) (tag . #,(cdr d)))
(cdr d)))
;; identifier -> (list (listof imports) (listof exports))
(define (get-sigs id)
(define-values (imps exps) (unit-static-signatures id id))
(list imps exps))
;; flatten one level of a list
;; listof[listof[a]] -> listof[a]
(define (flatten l) (apply append l))
;; returns two lists of sig-elems
(define (get-all-sigs ids)
(define imps/exps (map get-sigs ids))
(define-values (imps exps) (unzip2 imps/exps))
(values (flatten imps) (flatten exps)))
;; construct the runtime code
;; takes 3 lists of identifiers and a syntax object for location info
(define (mk imports exports units stx)
(quasisyntax/loc stx
(begin (define-compound-unit/infer new-unit@
(import #,@imports)
(export #,@exports)
(link #,@units))
(define-values/invoke-unit/infer new-unit@))))
;; compares two signature datums for equality
(define (sig=? sig1 sig2)
(and (eq? (car sig1) (car sig2))
(or (symbol? (car sig1)) (not (car sig1)))
(bound-identifier=? (cdr sig1) (cdr sig2))))
;; is imp in the list of exports?
(define (imp-in-exps? imp exps)
(s:member imp exps sig=?))
;; produce the imports not satisfied by the exports, and all the exports
;; exports should not have duplicates
(define (imps/exps-from-units units)
(let-values ([(imps exps) (get-all-sigs units)])
(let* ([exps* (map datum->sig-elem exps)]
[imps* (map datum->sig-elem (filter (lambda (imp) (not (imp-in-exps? imp exps))) imps))])
(values imps* exps*))))
(syntax-case stx (import export)
;; here the exports are specified - they ought to be a subset of the allowable exports
[(_ (export . sigs) . units)
(let*-values ([(units) (syntax->list #'units)]
[(imps exps) (imps/exps-from-units units)])
(mk imps (syntax->list #'sigs) units stx))]
;; here we just export everything that's available
[(_ . units)
(andmap identifier? (syntax->list #'units))
(let*-values ([(units) (syntax->list #'units)]
[(imps exps) (imps/exps-from-units units)])
(mk imps exps units stx))]))
;; Tests
(define-signature x^ (x))
(define-signature y^ (y))
(define-signature z^ (z))
(define-unit y@
(import z^)
(export y^)
(define y (* 2 z)))
(define-unit x@
(import y^)
(export x^)
(define (x) (+ y 1)))
(define z 45)
(define-values/link-units/infer (export x^) x@ y@)
)

View File

@ -0,0 +1,121 @@
#lang scheme/base
(require (for-syntax scheme/base)
mzlib/plt-match
mzlib/struct)
(provide with-syntax* syntax-map start-timing do-time reverse-begin define-simple-syntax printf/log
with-logging-to-file log-file-name ==
print-type*
print-effect*
define-struct/printer
id
filter-multiple)
(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 (lib "file.ss") file-name-from-path))
(define-syntax (printf/log stx)
(if logging?
(syntax-case stx ()
[(_ fmt . args)
#'(when (log-file)
(apply 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 'truncate/replace)])
. 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)))))

View File

@ -0,0 +1,90 @@
(module typed-reader mzscheme
(require (lib "etc.ss"))
(require-for-template "private/prims.ss")
;; Provides raise-read-error and raise-read-eof-error
(require (lib "readerr.ss" "syntax"))
(define (skip-whitespace port)
;; Skips whitespace characters, sensitive to the current
;; readtable's definition of whitespace
(let ([ch (peek-char port)])
(unless (eof-object? ch)
;; Consult current readtable:
(let-values ([(like-ch/sym proc dispatch-proc)
(readtable-mapping (current-readtable) ch)])
;; If like-ch/sym is whitespace, then ch is whitespace
(when (and (char? like-ch/sym)
(char-whitespace? like-ch/sym))
(read-char port)
(skip-whitespace port))))))
(define (skip-comments read-one port src)
;; Recursive read, but skip comments and detect EOF
(let loop ()
(let ([v (read-one)])
(cond
[(special-comment? v) (loop)]
[(eof-object? v)
(let-values ([(l c p) (port-next-location port)])
(raise-read-eof-error "unexpected EOF in type annotation" src l c p 1))]
[else v]))))
(define (parse port read-one src)
(skip-whitespace port)
(let ([name (read-one)])
(begin0
(begin (skip-whitespace port)
(let ([next (read-one)])
(case (syntax-e next)
;; type annotation
[(:) (skip-whitespace port)
(syntax-property name 'type-label (syntax-object->datum (read-one)))]
[(::) (skip-whitespace port)
(datum->syntax-object name `(ann ,name : ,(read-one)))]
[(@) (let ([elems (let loop ([es '()])
(skip-whitespace port)
(if (equal? #\} (peek-char port))
(reverse es)
(loop (cons (read-one) es))))])
(datum->syntax-object name `(inst ,name : ,@elems)))]
;; arbitrary property annotation
[(PROP) (skip-whitespace port)
(let* ([prop-name (syntax-e (read-one))])
(skip-whitespace port)
(syntax-property name prop-name (read-one)))]
;; type annotation
[else (syntax-property name 'type-label (syntax-object->datum next))])))
(skip-whitespace port)
(let ([c (read-char port)])
#;(printf "char: ~a" c)
(unless (equal? #\} c)
(let-values ([(l c p) (port-next-location port)])
(raise-read-error (format "typed expression ~a not properly terminated" (syntax-object->datum name)) src l c p 1)))))))
(define parse-id-type
(case-lambda
[(ch port src line col pos)
;; `read-syntax' mode
(datum->syntax-object
#f
(parse port
(lambda () (read-syntax src port ))
src)
(let-values ([(l c p) (port-next-location port)])
(list src line col pos (and pos (- p pos)))))]))
(define readtable
(make-readtable #f #\{ 'dispatch-macro parse-id-type))
(define (*read inp)
(parameterize ([current-readtable readtable])
(read inp)))
(define (*read-syntax src port)
(parameterize ([current-readtable readtable])
(read-syntax src port)))
(provide (rename *read read) (rename *read-syntax read-syntax))
)

View File

@ -0,0 +1,392 @@
#lang scribble/doc
@begin[(require scribble/manual)
(require (for-label typed-scheme/lang/main))]
@begin[
(define (item* header . args) (apply item @bold[header]{: } args))
(define-syntax-rule (tmod forms ...) (schememod typed-scheme forms ...))
]
@title[#:tag "top"]{@bold{Typed Scheme}: Scheme with Static Types}
@(defmodulelang typed-scheme #:use-sources (typed-scheme/lang/main))
Typed Scheme is a Scheme-like language, with a type system that
supports common Scheme programming idioms. Explicit type declarations
are required --- that is, there is no type inference. The language
supports a number of features from previous work on type systems that
make it easier to type Scheme programs, as well as a novel idea dubbed
@italic{occurrence typing} for case discrimination.
Typed Scheme is also designed to integrate with the rest of your PLT
Scheme system. It is possible to convert a single module to Typed
Scheme, while leaving the rest of the program unchanged. The typed
module is protected from the untyped code base via
automatically-synthesized contracts.
Further information on Typed Scheme is available from
@link["http://www.ccs.neu.edu/home/samth/typed-scheme"]{the homepage}.
@section{Starting with Typed Scheme}
If you already know PLT Scheme, or even some other Scheme, it should be
easy to start using Typed Scheme.
@subsection{A First Function}
The following program defines the Fibonacci function in PLT Scheme:
@schememod[scheme
(define (fib n)
(cond [(= 0 n) 1]
[(= 1 n) 1]
[else (+ (fib (- n 1)) (fib (- n 2)))]))
]
This program defines the same program using Typed Scheme.
@schememod[typed-scheme
(: fib (Number -> Number))
(define (fib n)
(cond [(= 0 n) 1]
[(= 1 n) 1]
[else (+ (fib (- n 1)) (fib (- n 2)))]))
]
There are two differences between these programs:
@itemize{
@item*[@elem{The Language}]{@schememodname[scheme] has been replaced by @schememodname[typed-scheme].}
@item*[@elem{The Type Annotation}]{We have added a type annotation
for the @scheme[fib] function, using the @scheme[:] form.} }
In general, these are most of the changes that have to be made to a
PLT Scheme program to transform it into a Typed Scheme program.
@margin-note{Changes to uses of @scheme[require] may also be necessary
- these are described later.}
@subsection[#:tag "complex"]{Adding more complexity}
Other typed binding forms are also available. For example, we could have
rewritten our fibonacci program as follows:
@schememod[typed-scheme
(: fib (Number -> Number))
(define (fib n)
(let ([base? (or (= 0 n) (= 1 n))])
(if base? 1
(+ (fib (- n 1)) (fib (- n 2))))))
]
This program uses the @scheme[let] binding form, but no new type
annotations are required. Typed Scheme infers the type of
@scheme[base?].
We can also define mutually-recursive functions:
@schememod[typed-scheme
(: my-odd? (Number -> Boolean))
(define (my-odd? n)
(if (= 0 n) #f
(my-even? (- n 1))))
(: my-even? (Number -> Boolean))
(define (my-even? n)
(if (= 0 n) #t
(my-odd? (- n 1))))
(display (my-even? 12))
]
As expected, this program prints @schemeresult[#t].
@subsection{Defining New Datatypes}
If our program requires anything more than atomic data, we must define
new datatypes. In Typed Scheme, structures can be defined, similarly
to PLT Scheme structures. The following program defines a date
structure and a function that formats a date as a string, using PLT
Scheme's built-in @scheme[format] function.
@schememod[typed-scheme
(define-typed-struct Date ([day : Number] [month : String] [year : Number]))
(: format-date (Date -> String))
(define (format-date d)
(format "Today is day ~a of ~a in the year ~a"
(Date-day d) (Date-month d) (Date-year d)))
(display (format-date (make-Date 28 "November" 2006)))
]
Here we see the new built-in type @scheme[String] as well as a definition
of the new user-defined type @scheme[my-date]. To define
@scheme[my-date], we provide all the information usually found in a
@scheme[define-struct], but added type annotations to the fields using
the @scheme[define-typed-struct] form.
Then we can use the functions that this declaration creates, just as
we would have with @scheme[define-struct].
@subsection{Recursive Datatypes and Unions}
Many data structures involve multiple variants. In Typed Scheme, we
represent these using @italic{union types}, written @scheme[(U t1 t2 ...)].
@schememod[typed-scheme
(define-type-alias Tree (U leaf node))
(define-typed-struct leaf ([val : Number]))
(define-typed-struct node ([left : Tree] [right : Tree]))
(: tree-height (Tree -> Number))
(define (tree-height t)
(cond [(leaf? t) 1]
[else (max (tree-height (node-left t))
(tree-height (node-right t)))]))
(: tree-sum (Tree -> Number))
(define (tree-sum t)
(cond [(leaf? t) (leaf-val t)]
[else (+ (tree-sum (node-left t))
(tree-sum (node-right t)))]))
]
In this module, we have defined two new datatypes: @scheme[leaf] and
@scheme[node]. We've also defined the type alias @scheme[Tree] to be
@scheme[(U node leaf)], which represents a binary tree of numbers. In
essence, we are saying that the @scheme[tree-height] function accepts
a @scheme[Tree], which is either a @scheme[node] or a @scheme[leaf],
and produces a number.
In order to calculate interesting facts about trees, we have to take
them apart and get at their contents. But since accessors such as
@scheme[node-left] require a @scheme[node] as input, not a
@scheme[Tree], we have to determine which kind of input we
were passed.
For this purpose, we use the predicates that come with each defined
structure. For example, the @scheme[leaf?] predicate distinguishes
@scheme[leaf]s from all other Typed Scheme values. Therefore, in the
first branch of the @scheme[cond] clause in @scheme[tree-sum], we know
that @scheme[t] is a @scheme[leaf], and therefore we can get its value
with the @scheme[leaf-val] function.
In the else clauses of both functions, we know that @scheme[t] is not
a @scheme[leaf], and since the type of @scheme[t] was @scheme[Tree] by
process of elimination we can determine that @scheme[t] must be a
@scheme[node]. Therefore, we can use accessors such as
@scheme[node-left] and @scheme[node-right] with @scheme[t] as input.
@section{Polymorphism}
Virtually every Scheme program uses lists and sexpressions. Fortunately, Typed
Scheme can handle these as well. A simple list processing program can be
written like this:
@schememod[typed-scheme
(: sum-list ((Listof Number) -> Number))
(define (sum-list l)
(cond [(null? l) 0]
[else (+ (car l) (sum-list (cdr l)))]))
]
This looks similar to our earlier programs --- except for the type
of @scheme[l], which looks like a function application. In fact, it's
a use of the @italic{type constructor} @scheme[Listof], which takes
another type as its input, here @scheme[Number]. We can use
@scheme[Listof] to construct the type of any kind of list we might
want.
We can define our own type constructors as well. For example, here is
an analog of the @tt{Maybe} type constructor from Haskell:
@schememod[typed-scheme
(define-typed-struct Nothing ())
(define-typed-struct (a) Just ([v : a]))
(define-type-alias (Maybe a) (U Nothing (Just a)))
(: find (Number (Listof Number) -> (Maybe Number)))
(define (find v l)
(cond [(null? l) (make-Nothing)]
[(= v (car l)) (make-Just v)]
[else (find v (cdr l))]))
]
The first @scheme[define-typed-struct] defines @scheme[Nothing] to be
a structure with no contents.
The second definition
@schemeblock[
(define-typed-struct (a) Just ([v : a]))
]
creates a parameterized type, @scheme[Just], which is a structure with
one element, whose type is that of the type argument to
@scheme[Just]. Here the type parameters (only one, @scheme[a], in
this case) are written before the type name, and can be referred to in
the types of the fields.
The type alias definiton
@schemeblock[
(define-type-alias (Maybe a) (U Nothing (Just a)))
]
creates a parameterized alias --- @scheme[Maybe] is a potential
container for whatever type is supplied.
The @scheme[find] function takes a number @scheme[v] and list, and
produces @scheme[(make-Just v)] when the number is found in the list,
and @scheme[(make-Nothing)] otherwise. Therefore, it produces a
@scheme[(Maybe Number)], just as the annotation specified.
@section[#:tag "type-ref"]{Type Reference}
@subsubsub*section{Base Types}
These types represent primitive Scheme data.
@defidform[Number]{Any number}
@defidform[Boolean]{Either @scheme[#t] or @scheme[#f]}
@defidform[String]{A string}
@defidform[Keyword]{A PLT Scheme literal keyword}
@defidform[Symbol]{A symbol}
@defidform[Any]{Any value}
@subsubsub*section{Type Constructors}
The following constructors are parameteric in their type arguments.
@defform[(Listof t)]{Homogenous lists of @scheme[t]}
@defform[(Vectorof t)]{Homogenous vectors of @scheme[t]}
@defform[(Option t)]{Either @scheme[t] of @scheme[#f]}
@;{
@schemeblock[
(define: f : (Number -> Number) (lambda: ([x : Number]) 3))
]
}
@begin[
(require (for-syntax scheme/base))
(define-syntax (definfixform stx)
(syntax-case stx ()
[(_ dummy . rest) #'(begin (specform . rest))]))
#;
(define-syntax (definfixform stx)
(syntax-case stx ()
[(_ id spec desc ...)
#'(*defforms (quote-syntax id)
'()
'(spec)
(list (lambda (x) (schemeblock0 spec)))
'()
'()
(lambda () (list desc ...)))]))
]
@defform[(Pair s t)]{is the pair containing @scheme[s] as the @scheme[car]
and @scheme[t] as the @scheme[cdr]}
@defform[(-> dom ... rng)]{is the type of functions from the (possibly-empty)
sequence @scheme[dom ...] to the @scheme[rng] type.}
@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
types constructed with @scheme[->].}
@defform/none[(t t1 t2 ...)]{is the instantiation of the parametric type
@scheme[t] at types @scheme[t1 t2 ...]}
@defform[(All (v ...) t)]{is a parameterization of type @scheme[t], with
type variables @scheme[v ...]}
@defform[(values t ...)]{is the type of a sequence of multiple values, with
types @scheme[t ...]. This can only appear as the return type of a
function.}
@defform/none[v]{where @scheme[v] is a number, boolean or string, is the singleton type containing
only that value}
@defform/none[i]{where @scheme[i] is an identifier can be a reference to a type
name or a type variable}
@defform[(Rec n t)]{is a recursive type where @scheme[n] is bound to the
recursive type in the body @scheme[t]}
Other types cannot be written by the programmer, but are used
internally and may appear in error messages.
@defform/none[(struct:n (t ...))]{is the type of structures named
@scheme[n] with field types @scheme[t]. There may be multiple such
types with the same printed representation.}
@defform/none[<n>]{is the printed representation of a reference to the
type variable @scheme[n]}
@section[#:tag "special-forms"]{Special Form Reference}
Typed Scheme provides a variety of special forms above and beyond
those in PLT Scheme. They are used for annotating variables with types,
creating new types, and annotating expressions.
@subsection{Binding Forms}
@scheme[_loop], @scheme[_f], @scheme[_a], and @scheme[_v] are names, @scheme[_t] is a type.
@scheme[_e] is an expression and @scheme[_body] is a block.
@defform*[[(define: (f [v : t] ...) : t body)
(define: v : t e)]]{}
@defform[
(pdefine: (a ...) (f [v : t] ...) : t body)]{}
@defform*[[
(let: ([v : t e] ...) body)
(let: loop : t0 ([v : t e] ...) body)]]{where @scheme[_t0] is the type of the
result of @scheme[_loop] (and thus the result of the entire expression).}
@defform[
(letrec: ([v : t e] ...) body)]{}
@defform[
(let*: ([v : t e] ...) body)]{}
@defform*[[
(lambda: ([v : t] ...) body)
(lambda: ([v : t] ... . [v : t]) body)]]{}
@defform*[[
(plambda: (a ...) ([v : t] ...) body)
(plambda: (a ...) ([v : t] ... . [v : t]) body)]]{}
@defform[
(case-lambda: [formals body] ...)]{where @scheme[_formals] is like
the second element of a @scheme[lambda:]}
@defform[
(pcase-lambda: (a ...) [formals body] ...)]{where @scheme[_formals] is like
the third element of a @scheme[plambda:]}
@subsection{Structure Definitions}
@defform*[[
(define-typed-struct name ([f : t] ...))
(define-typed-struct (name parent) ([f : t] ...))
(define-typed-struct (v ...) name ([f : t] ...))
(define-typed-struct (v ...) (name parent) ([f : t] ...))]]
@subsection{Type Aliases}
@defform*[[(define-type-alias name t)
(define-type-alias (name v ...) t)]]{}
@subsection{Type Annotation}
@defform[
(: v t)
]
@litchar{#{v : t}} This is legal only for binding occurences of @scheme[_v].
@litchar{#{e :: t}} This is legal only in expression contexts.
@subsection{Require}
Here, @scheme[_m] is a module spec, @scheme[_pred] is an identifier
naming a predicate, and @scheme[_r] is an optionally-renamed identifier.
@defform*[[
(require/typed r t m)
(require/typed m [r t] ...)
]]{}
@defform[(require/opaque-type t pred m)]{}
@defform[(require-typed-struct name ([f : t] ...) m)]{}

View File

@ -0,0 +1,150 @@
#lang scheme/base
(require "private/prims.ss"
"private/init-envs.ss"
"private/extra-procs.ss"
"private/internal-forms.ss"
"private/base-env.ss"
(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-env.ss" "private/type-name-env.ss"
"private/type-alias-env.ss"
"private/utils.ss"
"private/internal-forms.ss"
"private/init-envs.ss"
"private/type-effect-convenience.ss"
"private/effect-rep.ss"
"private/rep-utils.ss"
"private/type-contract.ss"
"private/nest.ss"
syntax/kerncase
mzlib/list
mzlib/plt-match))
(provide
;; provides syntax such as define: and define-typed-struct
(all-from-out "private/prims.ss")
;; provides some pointless procedures - should be removed
(all-from-out "private/extra-procs.ss"))
(provide-tnames)
(provide-extra-tnames)
(provide (rename-out [module-begin #%module-begin]
[with-handlers: with-handlers]
[top-interaction #%top-interaction]
[#%plain-lambda lambda]
[#%plain-app #%app]
[require require]))
(define-for-syntax catch-errors? #f)
(define-syntax (module-begin stx)
(define module-name (syntax-property stx 'enclosing-module-name))
;(printf "BEGIN: ~a~n" (syntax->datum stx))
(with-logging-to-file
(log-file-name (syntax-src stx) module-name)
(syntax-case stx ()
[(mb forms ...)
(nest
([begin (set-box! typed-context? #t)
(start-timing module-name)]
[with-handlers
([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e))))
(lambda (e) (tc-error "Internal error: ~a" e))])]
[parameterize (;; this parameter is for parsing types
[current-tvars initial-tvar-env]
;; this parameter is just for printing types
;; this is a parameter to avoid dependency issues
[current-type-names
(lambda ()
(append
(type-name-env-map (lambda (id ty)
(cons (syntax-e id) ty)))
(type-alias-env-map (lambda (id ty)
(cons (syntax-e id) ty)))))]
;; reinitialize seen type variables
[type-name-references null])]
[begin (do-time "Initialized Envs")]
;; local-expand the module
;; pmb = #%plain-module-begin
[with-syntax ([new-mod
(local-expand #`(#%plain-module-begin
forms ...)
'module-begin
null
#;stop-list)])]
[with-syntax ([(pmb body2 ...) #'new-mod])]
[begin (do-time "Local Expand Done")]
[with-syntax ([after-code (parameterize ([orig-module-stx stx]
[expanded-module-stx #'new-mod])
(type-check #'(body2 ...)))]
[check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))]
[(transformed-body ...) (remove-provides #'(body2 ...))])]
[with-syntax ([(transformed-body ...) (change-contract-fixups #'(transformed-body ...))])])
(do-time "Typechecked")
(printf "checked ~a~n" module-name)
#;(printf "created ~a types~n" (count!))
#;(printf "tried to create ~a types~n" (all-count!))
#;(printf "created ~a union types~n" (union-count!))
;; reconstruct the module with the extra code
#'(#%module-begin transformed-body ... after-code check-syntax-help))])))
(define-syntax (top-interaction stx)
(syntax-case stx ()
[(_ . (module . rest))
(eq? 'module (syntax-e #'module))
#'(module . rest)]
[(_ . form)
(nest
([begin (set-box! typed-context? #t)]
[parameterize (;; this paramter is for parsing types
[current-tvars initial-tvar-env]
;; this parameter is just for printing types
;; this is a parameter to avoid dependency issues
[current-type-names
(lambda ()
(append
(type-name-env-map (lambda (id ty)
(cons (syntax-e id) ty)))
(type-alias-env-map (lambda (id ty)
(cons (syntax-e id) ty)))))])]
;(do-time "Initialized Envs")
;; local-expand the module
[let ([body2 (local-expand #'(#%top-interaction . form) 'top-level null)])]
[parameterize ([orig-module-stx #'form]
[expanded-module-stx body2])]
;; typecheck the body, and produce syntax-time code that registers types
[let ([type (tc-toplevel-form body2)])])
(kernel-syntax-case body2 #f
[(head . _)
(or (free-identifier=? #'head #'define-values)
(free-identifier=? #'head #'define-syntaxes)
(free-identifier=? #'head #'require)
(free-identifier=? #'head #'provide)
(free-identifier=? #'head #'begin)
(type-equal? -Void (tc-result-t type)))
body2]
;; construct code to print the type
[_
(nest
([with-syntax ([b body2]
[ty-str (match type
[(tc-result: t)
(format "- : ~a\n" t)]
[x (int-err "bad type result: ~a" x)])])])
#`(let ([v b] [type 'ty-str])
(begin0
v
(printf type))))]))]))