diff --git a/collects/typed-scheme/info.ss b/collects/typed-scheme/info.ss new file mode 100644 index 0000000000..e59bcb1832 --- /dev/null +++ b/collects/typed-scheme/info.ss @@ -0,0 +1,4 @@ +#lang setup/infotab + +(define name "Typed Scheme") +(define scribblings '(("typed-scheme.scrbl"))) diff --git a/collects/typed-scheme/lang/main.ss b/collects/typed-scheme/lang/main.ss new file mode 100644 index 0000000000..a31d5925a6 --- /dev/null +++ b/collects/typed-scheme/lang/main.ss @@ -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)) diff --git a/collects/typed-scheme/lang/minimal.ss b/collects/typed-scheme/lang/minimal.ss new file mode 100644 index 0000000000..c732931f44 --- /dev/null +++ b/collects/typed-scheme/lang/minimal.ss @@ -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) ...))))))])) + \ No newline at end of file diff --git a/collects/typed-scheme/lang/reader.ss b/collects/typed-scheme/lang/reader.ss new file mode 100644 index 0000000000..8794ba5907 --- /dev/null +++ b/collects/typed-scheme/lang/reader.ss @@ -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]))) + diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss new file mode 100644 index 0000000000..514259e871 --- /dev/null +++ b/collects/typed-scheme/private/base-env.ss @@ -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) + diff --git a/collects/typed-scheme/private/check-subforms-unit.ss b/collects/typed-scheme/private/check-subforms-unit.ss new file mode 100644 index 0000000000..79298be97c --- /dev/null +++ b/collects/typed-scheme/private/check-subforms-unit.ss @@ -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)]))) \ No newline at end of file diff --git a/collects/typed-scheme/private/def-binding.ss b/collects/typed-scheme/private/def-binding.ss new file mode 100644 index 0000000000..41d3136105 --- /dev/null +++ b/collects/typed-scheme/private/def-binding.ss @@ -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) \ No newline at end of file diff --git a/collects/typed-scheme/private/defstruct-unit.ss b/collects/typed-scheme/private/defstruct-unit.ss new file mode 100644 index 0000000000..fa4e6b29de --- /dev/null +++ b/collects/typed-scheme/private/defstruct-unit.ss @@ -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) ...))])) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/effect-rep.ss b/collects/typed-scheme/private/effect-rep.ss new file mode 100644 index 0000000000..e33977f9b6 --- /dev/null +++ b/collects/typed-scheme/private/effect-rep.ss @@ -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 diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss new file mode 100644 index 0000000000..cd8af3b267 --- /dev/null +++ b/collects/typed-scheme/private/extra-procs.ss @@ -0,0 +1,9 @@ +(module extra-procs mzscheme + (provide assert) + + (define (assert v) + (unless v + (error "Assertion failed - value was #f")) + v) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/free-variance.ss b/collects/typed-scheme/private/free-variance.ss new file mode 100644 index 0000000000..8bf8664d06 --- /dev/null +++ b/collects/typed-scheme/private/free-variance.ss @@ -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))))])) \ No newline at end of file diff --git a/collects/typed-scheme/private/infer.ss b/collects/typed-scheme/private/infer.ss new file mode 100644 index 0000000000..c1f1c6f407 --- /dev/null +++ b/collects/typed-scheme/private/infer.ss @@ -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) + + + + diff --git a/collects/typed-scheme/private/init-envs.ss b/collects/typed-scheme/private/init-envs.ss new file mode 100644 index 0000000000..957efd1ae0 --- /dev/null +++ b/collects/typed-scheme/private/init-envs.ss @@ -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))))) + + + + + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/internal-forms.ss b/collects/typed-scheme/private/internal-forms.ss new file mode 100644 index 0000000000..b1808af506 --- /dev/null +++ b/collects/typed-scheme/private/internal-forms.ss @@ -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) + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/interning.ss b/collects/typed-scheme/private/interning.ss new file mode 100644 index 0000000000..130a46a874 --- /dev/null +++ b/collects/typed-scheme/private/interning.ss @@ -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)))) \ No newline at end of file diff --git a/collects/typed-scheme/private/lexical-env.ss b/collects/typed-scheme/private/lexical-env.ss new file mode 100644 index 0000000000..ffea848ebb --- /dev/null +++ b/collects/typed-scheme/private/lexical-env.ss @@ -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)])) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/mutated-vars.ss b/collects/typed-scheme/private/mutated-vars.ss new file mode 100644 index 0000000000..b55ce41c3e --- /dev/null +++ b/collects/typed-scheme/private/mutated-vars.ss @@ -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?) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/nest.ss b/collects/typed-scheme/private/nest.ss new file mode 100644 index 0000000000..1cccc99ed0 --- /dev/null +++ b/collects/typed-scheme/private/nest.ss @@ -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 ...))])) diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss new file mode 100644 index 0000000000..f4e16dd98e --- /dev/null +++ b/collects/typed-scheme/private/parse-type.ss @@ -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))]))) + diff --git a/collects/typed-scheme/private/planet-requires.ss b/collects/typed-scheme/private/planet-requires.ss new file mode 100644 index 0000000000..0c21dc6017 --- /dev/null +++ b/collects/typed-scheme/private/planet-requires.ss @@ -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")) \ No newline at end of file diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss new file mode 100644 index 0000000000..29bb988ab1 --- /dev/null +++ b/collects/typed-scheme/private/prims.ss @@ -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 ...)))))]))])) + + + diff --git a/collects/typed-scheme/private/provide-handling.ss b/collects/typed-scheme/private/provide-handling.ss new file mode 100644 index 0000000000..e9fcc99e75 --- /dev/null +++ b/collects/typed-scheme/private/provide-handling.ss @@ -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))])) \ No newline at end of file diff --git a/collects/typed-scheme/private/remove-intersect.ss b/collects/typed-scheme/private/remove-intersect.ss new file mode 100644 index 0000000000..6765e21574 --- /dev/null +++ b/collects/typed-scheme/private/remove-intersect.ss @@ -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) + + diff --git a/collects/typed-scheme/private/rep-utils.ss b/collects/typed-scheme/private/rep-utils.ss new file mode 100644 index 0000000000..19939a6358 --- /dev/null +++ b/collects/typed-scheme/private/rep-utils.ss @@ -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)))) + + + + + diff --git a/collects/typed-scheme/private/require-contract.ss b/collects/typed-scheme/private/require-contract.ss new file mode 100644 index 0000000000..c6157919ef --- /dev/null +++ b/collects/typed-scheme/private/require-contract.ss @@ -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) +|# diff --git a/collects/typed-scheme/private/resolve-type.ss b/collects/typed-scheme/private/resolve-type.ss new file mode 100644 index 0000000000..b07bf88d92 --- /dev/null +++ b/collects/typed-scheme/private/resolve-type.ss @@ -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) + +|# \ No newline at end of file diff --git a/collects/typed-scheme/private/signatures.ss b/collects/typed-scheme/private/signatures.ss new file mode 100644 index 0000000000..19812bf322 --- /dev/null +++ b/collects/typed-scheme/private/signatures.ss @@ -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 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)) + + diff --git a/collects/typed-scheme/private/syntax-traversal.ss b/collects/typed-scheme/private/syntax-traversal.ss new file mode 100644 index 0000000000..e2cfe31685 --- /dev/null +++ b/collects/typed-scheme/private/syntax-traversal.ss @@ -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) + diff --git a/collects/typed-scheme/private/tables.ss b/collects/typed-scheme/private/tables.ss new file mode 100644 index 0000000000..6d52dd436e --- /dev/null +++ b/collects/typed-scheme/private/tables.ss @@ -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)) + + diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss new file mode 100644 index 0000000000..21c33a2b9b --- /dev/null +++ b/collects/typed-scheme/private/tc-app-unit.ss @@ -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) diff --git a/collects/typed-scheme/private/tc-expr-unit.ss b/collects/typed-scheme/private/tc-expr-unit.ss new file mode 100644 index 0000000000..528d6513a8 --- /dev/null +++ b/collects/typed-scheme/private/tc-expr-unit.ss @@ -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)])) \ No newline at end of file diff --git a/collects/typed-scheme/private/tc-if-unit.ss b/collects/typed-scheme/private/tc-if-unit.ss new file mode 100644 index 0000000000..cf9064803a --- /dev/null +++ b/collects/typed-scheme/private/tc-if-unit.ss @@ -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))]))) + + + +;) \ No newline at end of file diff --git a/collects/typed-scheme/private/tc-lambda-unit.ss b/collects/typed-scheme/private/tc-lambda-unit.ss new file mode 100644 index 0000000000..deeb33b997 --- /dev/null +++ b/collects/typed-scheme/private/tc-lambda-unit.ss @@ -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) + + diff --git a/collects/typed-scheme/private/tc-let-unit.ss b/collects/typed-scheme/private/tc-let-unit.ss new file mode 100644 index 0000000000..8a137fc785 --- /dev/null +++ b/collects/typed-scheme/private/tc-let-unit.ss @@ -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) + + diff --git a/collects/typed-scheme/private/tc-structs.ss b/collects/typed-scheme/private/tc-structs.ss new file mode 100644 index 0000000000..8237507ddd --- /dev/null +++ b/collects/typed-scheme/private/tc-structs.ss @@ -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)) + + + +|# \ No newline at end of file diff --git a/collects/typed-scheme/private/tc-toplevel.ss b/collects/typed-scheme/private/tc-toplevel.ss new file mode 100644 index 0000000000..496df7905b --- /dev/null +++ b/collects/typed-scheme/private/tc-toplevel.ss @@ -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)) + + + diff --git a/collects/typed-scheme/private/tc-utils.ss b/collects/typed-scheme/private/tc-utils.ss new file mode 100644 index 0000000000..9b60c143af --- /dev/null +++ b/collects/typed-scheme/private/tc-utils.ss @@ -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)))) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/tool.ss b/collects/typed-scheme/private/tool.ss new file mode 100644 index 0000000000..4071ff7f19 --- /dev/null +++ b/collects/typed-scheme/private/tool.ss @@ -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%))))))) + ) + + + + + diff --git a/collects/typed-scheme/private/type-alias-env.ss b/collects/typed-scheme/private/type-alias-env.ss new file mode 100644 index 0000000000..33d6d82ef1 --- /dev/null +++ b/collects/typed-scheme/private/type-alias-env.ss @@ -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))))) diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss new file mode 100644 index 0000000000..3b61281ab7 --- /dev/null +++ b/collects/typed-scheme/private/type-annotation.ss @@ -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))))) diff --git a/collects/typed-scheme/private/type-comparison.ss b/collects/typed-scheme/private/type-comparison.ss new file mode 100644 index 0000000000..b421fd8625 --- /dev/null +++ b/collects/typed-scheme/private/type-comparison.ss @@ -0,0 +1,8 @@ +(module type-comparison mzscheme + (require "type-rep.ss" "type-utils.ss") + + (provide type-equal? tc-result-equal? typecontract 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))])))) + + ) diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss new file mode 100644 index 0000000000..d12f0cbd58 --- /dev/null +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -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)])))) + + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss new file mode 100644 index 0000000000..9424048944 --- /dev/null +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -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) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/type-env.ss b/collects/typed-scheme/private/type-env.ss new file mode 100644 index 0000000000..c42d110d04 --- /dev/null +++ b/collects/typed-scheme/private/type-env.ss @@ -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)) diff --git a/collects/typed-scheme/private/type-environments.ss b/collects/typed-scheme/private/type-environments.ss new file mode 100644 index 0000000000..54d5b008b2 --- /dev/null +++ b/collects/typed-scheme/private/type-environments.ss @@ -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)) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/type-name-env.ss b/collects/typed-scheme/private/type-name-env.ss new file mode 100644 index 0000000000..3031f28ada --- /dev/null +++ b/collects/typed-scheme/private/type-name-env.ss @@ -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)) + + diff --git a/collects/typed-scheme/private/type-rep.ss b/collects/typed-scheme/private/type-rep.ss new file mode 100644 index 0000000000..0c7c274930 --- /dev/null +++ b/collects/typed-scheme/private/type-rep.ss @@ -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 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 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 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))) diff --git a/collects/typed-scheme/private/typechecker.ss b/collects/typed-scheme/private/typechecker.ss new file mode 100644 index 0000000000..5b48745b83 --- /dev/null +++ b/collects/typed-scheme/private/typechecker.ss @@ -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@) diff --git a/collects/typed-scheme/private/unify.ss b/collects/typed-scheme/private/unify.ss new file mode 100644 index 0000000000..71eeb582f0 --- /dev/null +++ b/collects/typed-scheme/private/unify.ss @@ -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) + diff --git a/collects/typed-scheme/private/union.ss b/collects/typed-scheme/private/union.ss new file mode 100644 index 0000000000..a58d59fb75 --- /dev/null +++ b/collects/typed-scheme/private/union.ss @@ -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)) typesig-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@) + + ) \ No newline at end of file diff --git a/collects/typed-scheme/private/utils.ss b/collects/typed-scheme/private/utils.ss new file mode 100644 index 0000000000..01a9317d61 --- /dev/null +++ b/collects/typed-scheme/private/utils.ss @@ -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))))) + + diff --git a/collects/typed-scheme/typed-reader.ss b/collects/typed-scheme/typed-reader.ss new file mode 100644 index 0000000000..1bf7835585 --- /dev/null +++ b/collects/typed-scheme/typed-reader.ss @@ -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)) + ) diff --git a/collects/typed-scheme/typed-scheme.scrbl b/collects/typed-scheme/typed-scheme.scrbl new file mode 100644 index 0000000000..c534db2bb3 --- /dev/null +++ b/collects/typed-scheme/typed-scheme.scrbl @@ -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[]{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)]{} diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss new file mode 100644 index 0000000000..4a85636203 --- /dev/null +++ b/collects/typed-scheme/typed-scheme.ss @@ -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))))]))])) + + +