diff --git a/collects/tests/typed-scheme/fail/values-dots.ss b/collects/tests/typed-scheme/fail/values-dots.ss index 6c08fff5..f92743fa 100644 --- a/collects/tests/typed-scheme/fail/values-dots.ss +++ b/collects/tests/typed-scheme/fail/values-dots.ss @@ -7,8 +7,8 @@ (: map-with-funcs (All (b ...) ((b ... b -> b) ... b -> (b ... b -> (values b ... b))))) (define (map-with-funcs . fs) (lambda bs - (apply values* (map (lambda: ([f : (b ... b -> b)]) - (apply f bs)) fs)))) + (apply values (map (lambda: ([f : (b ... b -> b)]) + (apply f bs)) fs)))) (map-with-funcs (lambda () 1)) diff --git a/collects/tests/typed-scheme/succeed/nested-poly.ss b/collects/tests/typed-scheme/succeed/nested-poly.ss index 785ee9a5..ac8bb3cd 100644 --- a/collects/tests/typed-scheme/succeed/nested-poly.ss +++ b/collects/tests/typed-scheme/succeed/nested-poly.ss @@ -13,7 +13,7 @@ (B ... B -> (values A ... A)))))) (define (map-with-funcs . fs) (lambda as - (apply values* (map (lambda: ([f : (B ... B -> A)]) + (apply values (map (lambda: ([f : (B ... B -> A)]) (apply f as)) fs)))) diff --git a/collects/tests/typed-scheme/succeed/values-dots.ss b/collects/tests/typed-scheme/succeed/values-dots.ss index 0078526f..1c853f50 100644 --- a/collects/tests/typed-scheme/succeed/values-dots.ss +++ b/collects/tests/typed-scheme/succeed/values-dots.ss @@ -5,16 +5,16 @@ (call-with-values (lambda () (values 1 2)) (lambda: ([x : Number] [y : Number]) (+ x y))) -(#{call-with-values* @ Integer Integer Integer} (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y))) +(#{call-with-values @ Integer Integer Integer} (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y))) -(call-with-values* (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y))) +(call-with-values (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y))) (: map-with-funcs (All (b ...) ((b ... b -> b) ... b -> (b ... b -> (values b ... b))))) (define (map-with-funcs . fs) (lambda bs - (apply values* (map (lambda: ([f : (b ... b -> b)]) - (apply f bs)) fs)))) + (apply values (map (lambda: ([f : (b ... b -> b)]) + (apply f bs)) fs)))) (map-with-funcs + - * /) diff --git a/collects/tests/typed-scheme/unit-tests/all-tests.ss b/collects/tests/typed-scheme/unit-tests/all-tests.ss index aca0a4d1..1fe728d0 100644 --- a/collects/tests/typed-scheme/unit-tests/all-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/all-tests.ss @@ -12,7 +12,7 @@ "subst-tests.ss" "infer-tests.ss") -(require (private planet-requires infer infer-dummy)) +(require (utils planet-requires) (r:infer infer infer-dummy)) (require (schemeunit)) diff --git a/collects/tests/typed-scheme/unit-tests/infer-tests.ss b/collects/tests/typed-scheme/unit-tests/infer-tests.ss index f1d5e22b..aef624b7 100644 --- a/collects/tests/typed-scheme/unit-tests/infer-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/infer-tests.ss @@ -1,7 +1,10 @@ #lang scheme/base (require "test-utils.ss" (for-syntax scheme/base)) -(require (private planet-requires type-effect-convenience type-rep union infer type-utils) - (prefix-in table: (private tables))) +(require (utils planet-requires) + (rep type-rep) + (r:infer infer) + (private type-effect-convenience union type-utils) + (prefix-in table: (utils tables))) (require (schemeunit)) diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss index aa3882fd..fedf84fb 100644 --- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss @@ -1,8 +1,10 @@ #lang scheme/base (require "test-utils.ss" (for-syntax scheme/base)) -(require (private planet-requires type-comparison parse-type type-rep - tc-utils type-environments type-alias-env subtype - type-name-env init-envs union type-utils)) +(require (utils planet-requires tc-utils) + (env type-alias-env type-environments type-name-env init-envs) + (rep type-rep) + (private type-comparison parse-type subtype + union type-utils)) (require (rename-in (private type-effect-convenience) [-> t:->]) (except-in (private base-types) Un) diff --git a/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss index ca83402b..20da5c73 100644 --- a/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/remove-intersect-tests.ss @@ -1,6 +1,9 @@ #lang scheme/base (require "test-utils.ss" (for-syntax scheme/base)) -(require (private type-rep type-effect-convenience planet-requires remove-intersect subtype union infer)) +(require (rep type-rep) + (utils planet-requires) + (r:infer infer) + (private type-effect-convenience remove-intersect subtype union)) (require (schemeunit)) diff --git a/collects/tests/typed-scheme/unit-tests/subst-tests.ss b/collects/tests/typed-scheme/unit-tests/subst-tests.ss index 6c89d4ef..10a35fc9 100644 --- a/collects/tests/typed-scheme/unit-tests/subst-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/subst-tests.ss @@ -1,7 +1,9 @@ #lang scheme/base (require "test-utils.ss" (for-syntax scheme/base)) -(require (private planet-requires type-utils type-effect-convenience type-rep)) +(require (utils planet-requires) + (rep type-rep) + (private type-utils type-effect-convenience)) (require (schemeunit)) (define-syntax-rule (s img var tgt result) diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss index f4bc9912..83bb3e9a 100644 --- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss @@ -2,8 +2,12 @@ (require "test-utils.ss") -(require (private subtype type-rep type-effect-convenience - planet-requires init-envs type-environments union infer infer-dummy)) +(require (private subtype type-effect-convenience union) + (rep type-rep) + (utils planet-requires) + (env init-envs type-environments) + (r:infer infer infer-dummy)) + (require (schemeunit) (for-syntax scheme/base)) diff --git a/collects/tests/typed-scheme/unit-tests/test-utils.ss b/collects/tests/typed-scheme/unit-tests/test-utils.ss index f5c848fa..b160cacd 100644 --- a/collects/tests/typed-scheme/unit-tests/test-utils.ss +++ b/collects/tests/typed-scheme/unit-tests/test-utils.ss @@ -3,25 +3,12 @@ (require scheme/require-syntax scheme/match + typed-scheme/utils/utils (for-syntax scheme/base)) -(define-require-syntax private - (lambda (stx) - (syntax-case stx () - [(_ id ...) - (andmap identifier? (syntax->list #'(id ...))) - (with-syntax ([(id* ...) (map (lambda (id) (datum->syntax - id - (string->symbol - (string-append - "typed-scheme/private/" - (symbol->string (syntax-e id)))) - id id)) - (syntax->list #'(id ...)))]) - (syntax/loc stx (combine-in id* ...)))]))) - -(require (private planet-requires type-comparison utils type-utils)) +(require (utils planet-requires) (private type-comparison type-utils)) +(provide private typecheck (rename-out [infer r:infer]) utils env rep) (require (schemeunit)) (define (mk-suite ts) diff --git a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss index 6488d47b..899b8e1e 100644 --- a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss @@ -1,7 +1,8 @@ #lang scheme/base (require "test-utils.ss" (for-syntax scheme/base)) -(require (private planet-requires type-rep type-comparison type-effect-convenience union subtype)) +(require (utils planet-requires) (rep type-rep) + (private type-comparison type-effect-convenience union subtype)) (require (schemeunit)) (provide type-equal-tests) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index a5263dd3..fee35aa2 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -3,14 +3,16 @@ (require "test-utils.ss" (for-syntax scheme/base) (for-template scheme/base)) -(require (private base-env)) +(require (private base-env mutated-vars type-utils union prims type-effect-convenience type-annotation) + (typecheck typechecker) + (rep type-rep effect-rep) + (utils tc-utils planet-requires) + (env type-name-env type-environments init-envs)) -(require (private planet-requires typechecker - type-rep type-effect-convenience type-env - prims type-environments tc-utils union - type-name-env init-envs mutated-vars - effect-rep type-annotation type-utils) - (for-syntax (private tc-utils typechecker base-env type-env)) +(require (for-syntax (utils tc-utils) + (typecheck typechecker) + (env type-env) + (private base-env)) (for-template (private base-env base-types))) (require (schemeunit)) @@ -669,7 +671,7 @@ (tc-l #t (-val #t)) (tc-l "foo" -String) (tc-l foo (-val 'foo)) - (tc-l #:foo -Keyword) + (tc-l #:foo (-val '#:foo)) (tc-l #f (-val #f)) (tc-l #"foo" -Bytes) [tc-l () (-val null)] diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss new file mode 100644 index 00000000..4a03b910 --- /dev/null +++ b/collects/typed-scheme/env/init-envs.ss @@ -0,0 +1,81 @@ +#lang scheme/base +(provide (all-defined-out)) +(require "../utils/utils.ss") + +(require "type-env.ss" + "type-name-env.ss" + (rep type-rep effect-rep) + (for-template (rep type-rep effect-rep) + (private union) + mzlib/pconvert mzlib/shared scheme/base) + (private type-effect-convenience union) + "type-alias-env.ss" + mzlib/pconvert scheme/match mzlib/shared) + +(define (initialize-type-name-env initial-type-names) + (for-each (lambda (nm/ty) (register-resolved-type-alias (car nm/ty) (cadr nm/ty))) initial-type-names)) + +(define (initialize-type-env initial-env) + (for-each (lambda (nm/ty) (register-type (car nm/ty) (cadr nm/ty))) initial-env)) + +(define (converter v basic sub) + (define (gen-constructor sym) + (string->symbol (string-append "make-" (substring (symbol->string sym) 7)))) + (match v + [(Union: elems) `(make-Union (list ,@(map sub elems)))] + [(Name: stx) `(make-Name (quote-syntax ,stx))] + [(Struct: name parent flds proc poly? pred-id cert) + `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))] + [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))] + [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))] + [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))] + [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))] + [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))] + [(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) + `(,(gen-constructor tag) ,@(map sub vals))] + [(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) + `(,(gen-constructor tag) ,@(map sub vals))] + [_ (basic v)])) + +(define (bound-in-this-module id) + (let ([binding (identifier-binding id)]) + (if (and (list? binding) (module-path-index? (car binding))) + (let-values ([(mp base) (module-path-index-split (car binding))]) + (not mp)) + #f))) + +(define (tname-env-init-code) + (define (f id ty) + (if (bound-in-this-module id) + #`(register-type-name #'#,id #,(datum->syntax #'here (print-convert ty))) + #f)) + (parameterize ((current-print-convert-hook converter) + (show-sharing #f) + (booleans-as-true/false #f)) + (with-syntax ([registers (filter (lambda (x) x) (type-name-env-map f))]) + #'(begin (begin-for-syntax . registers))))) + +(define (talias-env-init-code) + (define (f id ty) + (if (bound-in-this-module id) + #`(register-resolved-type-alias #'#,id #,(datum->syntax #'here (print-convert ty))) + #f)) + (parameterize ((current-print-convert-hook converter) + (show-sharing #f) + (booleans-as-true/false #f)) + (with-syntax ([registers (filter (lambda (x) x) (type-alias-env-map f))]) + #'(begin (begin-for-syntax . registers))))) + +(define (env-init-code) + (define (f id ty) + (if (bound-in-this-module id) + #`(register-type #'#,id #,(datum->syntax #'here (print-convert ty))) + #f)) + (parameterize ((current-print-convert-hook converter) + (show-sharing #f) + (booleans-as-true/false #f)) + (with-syntax ([registers (filter (lambda (x) x) (type-env-map f))]) + #'(begin (begin-for-syntax . registers))))) + + + diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss new file mode 100644 index 00000000..63a1295b --- /dev/null +++ b/collects/typed-scheme/env/lexical-env.ss @@ -0,0 +1,62 @@ +#lang scheme/base + +(require (except-in "../utils/utils.ss" extend)) +(require "type-environments.ss" + (utils tc-utils) + "type-env.ss" + (private mutated-vars) + (private type-utils) + (private type-effect-convenience)) + +(provide (all-defined-out)) + +;; the current lexical environment +(define lexical-env (make-parameter (make-empty-env free-identifier=?))) + +;; run code in a new env +(define-syntax with-lexical-env + (syntax-rules () + [(_ e . b) (parameterize ([lexical-env e]) . b)])) + +;; run code in an extended env +(define-syntax with-lexical-env/extend + (syntax-rules () + [(_ is ts . b) (parameterize ([lexical-env (extend/values is ts (lexical-env))]) . b)])) + +;; find the type of identifier i, looking first in the lexical env, then in the top-level env +;; identifer -> Type +(define (lookup-type/lexical i) + (lookup (lexical-env) i + (lambda (i) (lookup-type + i (lambda () + (cond [(lookup (dotted-env) i (lambda _ #f)) + => + (lambda (a) + (-lst (substitute Univ (cdr a) (car a))))] + [else (lookup-fail (syntax-e i))])))))) + +;; refine the type of i in the lexical env +;; (identifier type -> type) identifier -> environment +(define (update-type/lexical f i) + ;; do the updating on the given env + ;; (identifier type -> type) identifier environment -> environment + (define (update f k env) + (parameterize + ([current-orig-stx k]) + (let* ([v (lookup-type/lexical k)] + [new-v (f k v)] + [new-env (extend env k new-v)]) + new-env))) + ;; check if i is ever the target of a set! + (if (is-var-mutated? i) + ;; if it is, we do nothing + (lexical-env) + ;; otherwise, refine the type + (update f i (lexical-env)))) + +;; convenience macro for typechecking in the context of an updated env +(define-syntax with-update-type/lexical + (syntax-rules () + [(_ f i . b) + (with-lexical-env (update-type/lexical f i) . b)])) + diff --git a/collects/typed-scheme/env/type-alias-env.ss b/collects/typed-scheme/env/type-alias-env.ss new file mode 100644 index 00000000..dd9183d3 --- /dev/null +++ b/collects/typed-scheme/env/type-alias-env.ss @@ -0,0 +1,68 @@ +#lang scheme/base + +(require (except-in "../utils/utils.ss" extend)) +(require syntax/boundmap + (utils tc-utils) + mzlib/trace + scheme/match) + +(provide register-type-alias + lookup-type-alias + resolve-type-aliases + register-resolved-type-alias + type-alias-env-map) + +(define-struct alias-def () #:inspector #f) +(define-struct (unresolved alias-def) (stx [in-process #:mutable]) #:inspector #f) +(define-struct (resolved alias-def) (ty) #:inspector #f) + +;; a mapping from id -> alias-def (where id is the name of the type) +(define the-mapping + (make-module-identifier-mapping)) + +(define (mapping-put! id v) (module-identifier-mapping-put! the-mapping id v)) + +;(trace mapping-put!) + +;; add a name to the mapping +;; identifier type-stx -> void +(define (register-type-alias id stx) + ;(printf "registering type ~a~n~a~n" (syntax-e id) id) + (mapping-put! id (make-unresolved stx #f))) + +(define (register-resolved-type-alias id ty) + #;(when (eq? 'Number (syntax-e id)) + (printf "registering type ~a ~a~n~a~n" id (syntax-e id) ty)) + (mapping-put! id (make-resolved ty))) + +(define (lookup-type-alias id parse-type [k (lambda () (tc-error "Unknown type alias: ~a" (syntax-e id)))]) + (let/ec return + (match (module-identifier-mapping-get the-mapping id (lambda () (return (k)))) + [(struct unresolved (stx #f)) + (resolve-type-alias id parse-type)] + [(struct unresolved (stx #t)) + (tc-error/stx stx "Recursive Type Alias Reference")] + [(struct resolved (t)) t]))) + +(define (resolve-type-alias id parse-type) + (define v (module-identifier-mapping-get the-mapping id)) + (match v + [(struct unresolved (stx _)) + (set-unresolved-in-process! v #t) + (let ([t (parse-type stx)]) + (mapping-put! id (make-resolved t)) + t)] + [(struct resolved (t)) + t])) + +(define (resolve-type-aliases parse-type) + (module-identifier-mapping-for-each the-mapping (lambda (id _) (resolve-type-alias id parse-type)))) + +;; map over the-mapping, producing a list +;; (id type -> T) -> listof[T] +(define (type-alias-env-map f) + (define sym (gensym)) + (filter (lambda (e) (not (eq? sym e))) + (module-identifier-mapping-map the-mapping (lambda (id t) (if (resolved? t) + (f id (resolved-ty t)) + sym))))) diff --git a/collects/typed-scheme/env/type-env.ss b/collects/typed-scheme/env/type-env.ss new file mode 100644 index 00000000..59eb3cad --- /dev/null +++ b/collects/typed-scheme/env/type-env.ss @@ -0,0 +1,65 @@ +#lang scheme/base + +(require (except-in "../utils/utils.ss" extend)) +(require syntax/boundmap + (utils tc-utils) + (private type-utils)) + +(provide register-type + finish-register-type + maybe-finish-register-type + register-type/undefined + lookup-type + register-types + check-all-registered-types + type-env-map) + +;; module-identifier-mapping from id -> type or Box[type] +;; where id is a variable, and type is the type of the variable +;; if the result is a box, then the type has not actually been defined, just registered +(define the-mapping (make-module-identifier-mapping)) + +;; add a single type to the mapping +;; identifier type -> void +(define (register-type id type) + ;(printf "register-type ~a~n" (syntax-e id)) + (module-identifier-mapping-put! the-mapping id type)) + +;; add a single type to the mapping +;; identifier type -> void +(define (register-type/undefined id type) + ;(printf "register-type/undef ~a~n" (syntax-e id)) + (module-identifier-mapping-put! the-mapping id (box type))) + +;; add a bunch of types to the mapping +;; listof[id] listof[type] -> void +(define (register-types ids types) + (for-each register-type ids types)) + +;; given an identifier, return the type associated with it +;; if none found, calls lookup-fail +;; identifier -> type +(define (lookup-type id [fail-handler (lambda () (lookup-fail (syntax-e id)))]) + (let ([v (module-identifier-mapping-get the-mapping id fail-handler)]) + (if (box? v) (unbox v) v))) + +(define (maybe-finish-register-type id) + (let ([v (module-identifier-mapping-get the-mapping id)]) + (if (box? v) + (register-type id (unbox v)) + #f))) + +(define (finish-register-type id) + (unless (maybe-finish-register-type id) + (int-err "finishing type that was already finished: ~a" (syntax-e id)))) + +(define (check-all-registered-types) + (module-identifier-mapping-for-each + the-mapping + (lambda (id e) + (when (box? e) (tc-error/stx id "Declaration for ~a provided, but with no definition" (syntax-e id)))))) + +;; map over the-mapping, producing a list +;; (id type -> T) -> listof[T] +(define (type-env-map f) + (module-identifier-mapping-map the-mapping f)) diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss new file mode 100644 index 00000000..0f159ec0 --- /dev/null +++ b/collects/typed-scheme/env/type-environments.ss @@ -0,0 +1,69 @@ +#lang scheme/base + +(provide current-tvars + extend + lookup + make-empty-env + extend-env + extend/values + dotted-env + initial-tvar-env + with-dotted-env/extend) + +(require (prefix-in r: "../utils/utils.ss")) +(require scheme/match + (r:utils tc-utils)) + +;; eq? has the type of equal?, and l is an alist (with conses!) +(define-struct env (eq? l)) + +;; the initial type variable environment - empty +;; this is used in the parsing of types +(define initial-tvar-env (make-env eq? '())) + +;; a parameter for the current type variables +(define current-tvars (make-parameter initial-tvar-env)) + +(define (make-empty-env p?) (make-env p? '())) + +;; the environment for types of ... variables +(define dotted-env (make-parameter (make-empty-env free-identifier=?))) + + + +;; extend that works on single arguments +(define (extend e k v) + (match e + [(struct env (f l)) (make-env f (cons (cons k v) l))] + [_ (int-err "extend: expected environment, got ~a" e)])) + +(define (extend-env ks vs e) + (match e + [(struct env (f l)) (make-env f (append (map cons ks vs) l))] + [_ (int-err "extend-env: expected environment, got ~a" e)])) + +(define (lookup e key fail) + (match e + [(struct env (f? l)) + (let loop ([l l]) + (cond [(null? l) (fail key)] + [(f? (caar l) key) (cdar l)] + [else (loop (cdr l))]))] + [_ (int-err "lookup: expected environment, got ~a" e)])) + + +;; takes two lists of sets to be added, which are either added one at a time, if the +;; elements are not lists, or all at once, if the elements are lists +(define (extend/values kss vss env) + (foldr (lambda (ks vs env) + (cond [(and (list? ks) (list? vs)) + (extend-env ks vs env)] + [(or (list? ks) (list? vs)) + (int-err "not both lists in extend/values: ~a ~a" ks vs)] + [else (extend-env (list ks) (list vs) env)])) + env kss vss)) + +;; run code in an extended dotted env +(define-syntax with-dotted-env/extend + (syntax-rules () + [(_ i t v . b) (parameterize ([dotted-env (extend/values (list i) (list (cons t v)) (dotted-env))]) . b)])) diff --git a/collects/typed-scheme/env/type-name-env.ss b/collects/typed-scheme/env/type-name-env.ss new file mode 100644 index 00000000..d6773f0e --- /dev/null +++ b/collects/typed-scheme/env/type-name-env.ss @@ -0,0 +1,44 @@ +#lang scheme/base +(require "../utils/utils.ss") + +(require syntax/boundmap + mzlib/trace + (utils tc-utils) + (private type-utils)) + +(provide register-type-name + lookup-type-name + register-type-names + type-name-env-map) + +;; a mapping from id -> type (where id is the name of the type) +(define the-mapping + (make-module-identifier-mapping)) + +(define (mapping-put! id v) (module-identifier-mapping-put! the-mapping id v)) +;(trace mapping-put!) + +;; add a name to the mapping +;; identifier Type -> void +(define (register-type-name id [type #t]) + ;(printf "registering type ~a~n~a~n" (syntax-e id) id) + (mapping-put! id type)) + +;; add a bunch of names to the mapping +;; listof[identifier] listof[type] -> void +(define (register-type-names ids types) + (for-each register-type-name ids types)) + +;; given an identifier, return the type associated with it +;; optional argument is failure continuation - default calls lookup-fail +;; identifier (-> error) -> type +(define (lookup-type-name id [k (lambda () (lookup-fail (syntax-e id)))]) + (begin0 + (module-identifier-mapping-get the-mapping id k) + (add-type-name-reference id))) + + +;; map over the-mapping, producing a list +;; (id type -> T) -> listof[T] +(define (type-name-env-map f) + (module-identifier-mapping-map the-mapping f)) diff --git a/collects/typed-scheme/infer/constraint-structs.ss b/collects/typed-scheme/infer/constraint-structs.ss new file mode 100644 index 00000000..d5c97034 --- /dev/null +++ b/collects/typed-scheme/infer/constraint-structs.ss @@ -0,0 +1,51 @@ +#lang scheme/base + +(require (except-in "../utils/utils.ss" extend)) +(require (rep type-rep) + scheme/contract) + +;; S, T types +;; X a var +(define-struct c (S X T) #:prefab) + +;; fixed : Listof[c] +;; rest : option[c] +(define-struct dcon (fixed rest) #:prefab) + +;; fixed : Listof[c] +;; rest : c +(define-struct dcon-exact (fixed rest) #:prefab) + +;; type : c +;; bound : var +(define-struct dcon-dotted (type bound) #:prefab) + +;; map : hash mapping variable to dcon or dcon-dotted +(define-struct dmap (map) #:prefab) + +;; maps is a list of pairs of +;; - functional maps from vars to c's +;; - dmaps (see dmap.ss) +;; we need a bunch of mappings for each cset to handle case-lambda +;; because case-lambda can generate multiple possible solutions, and we +;; don't want to rule them out too early +(define-struct cset (maps) #:prefab) + + +(define (hashof k/c v/c) + (flat-named-contract + (format "#" k/c v/c) + (lambda (h) + (define k/c? (if (flat-contract? k/c) (flat-contract-predicate k/c) k/c)) + (define v/c? (if (flat-contract? v/c) (flat-contract-predicate v/c) v/c)) + (and (hash? h) + (for/and ([(k v) h]) + (and (k/c? k) + (v/c? v))))))) + +(provide/contract (struct c ([S Type?] [X symbol?] [T Type?])) + (struct dcon ([fixed (listof c?)] [rest (or/c c? false/c)])) + (struct dcon-exact ([fixed (listof c?)] [rest c?])) + (struct dcon-dotted ([type c?] [bound symbol?])) + (struct dmap ([map (hashof symbol? (or/c dcon? dcon-exact? dcon-dotted?))])) + (struct cset ([maps (listof (cons/c (hashof symbol? c?) dmap?))]))) \ No newline at end of file diff --git a/collects/typed-scheme/infer/constraints.ss b/collects/typed-scheme/infer/constraints.ss new file mode 100644 index 00000000..3dff2c08 --- /dev/null +++ b/collects/typed-scheme/infer/constraints.ss @@ -0,0 +1,92 @@ +#lang scheme/unit + +(require (except-in "../utils/utils.ss" extend)) +(require (private type-effect-convenience type-utils union subtype) + (rep type-rep) + (utils tc-utils) + "signatures.ss" "constraint-structs.ss" + scheme/match) + +(import restrict^ dmap^) +(export constraints^) + + +(define-values (fail-sym exn:infer?) + (let ([sym (gensym)]) + (values sym (lambda (s) (eq? s sym))))) + +;; why does this have to be duplicated? +;; inference failure - masked before it gets to the user program +(define-syntaxes (fail!) + (syntax-rules () + [(_ s t) (raise fail-sym)])) + +;; Widest constraint possible +(define (no-constraint v) + (make-c (Un) v Univ)) + +(define (empty-cset X) + (make-cset (list (cons (for/hash ([x X]) (values x (no-constraint x))) + (make-dmap (make-immutable-hash null)))))) + + +(define (insert cs var S T) + (match cs + [(struct cset (maps)) + (make-cset (for/list ([(map dmap) (in-pairs maps)]) + (cons (hash-set map var (make-c S var T)) + dmap)))])) + +;; a stupid impl +(define (meet S T) + (let ([s* (restrict S T)]) + (if (and (subtype s* S) + (subtype s* T)) + s* + (Un)))) + +(define (join T U) (Un T U)) + + +(define (c-meet c1 c2 [var #f]) + (match* (c1 c2) + [((struct c (S X T)) (struct c (S* X* T*))) + (unless (or var (eq? X X*)) + (int-err "Non-matching vars in c-meet: ~a ~a" X X*)) + (let ([S (join S S*)] [T (meet T T*)]) + (unless (subtype S T) + (fail! S T)) + (make-c S (or var X) T))])) + +(define (subst-all/c sub -c) + (match -c + [(struct c (S X T)) + (make-c (subst-all sub S) + (F-n (subst-all sub (make-F X))) + (subst-all sub T))])) + +(define (cset-meet x y) + (match* (x y) + [((struct cset (maps1)) (struct cset (maps2))) + (let ([maps (filter values + (for*/list + ([(map1 dmap1) (in-pairs maps1)] + [(map2 dmap2) (in-pairs maps2)]) + (with-handlers ([exn:infer? (lambda (_) #f)]) + (cons + (hash-union map1 map2 (lambda (k v1 v2) (c-meet v1 v2))) + (dmap-meet dmap1 dmap2)))))]) + (when (null? maps) + (fail! maps1 maps2)) + (make-cset maps))] + [(_ _) (int-err "Got non-cset: ~a ~a" x y)])) + +(define (cset-meet* args) + (for/fold ([c (make-cset (list (cons (make-immutable-hash null) + (make-dmap (make-immutable-hash null)))))]) + ([a args]) + (cset-meet a c))) + +(define (cset-combine l) + (let ([mapss (map cset-maps l)]) + (make-cset (apply append mapss)))) diff --git a/collects/typed-scheme/infer/dmap.ss b/collects/typed-scheme/infer/dmap.ss new file mode 100644 index 00000000..95926680 --- /dev/null +++ b/collects/typed-scheme/infer/dmap.ss @@ -0,0 +1,66 @@ +#lang scheme/unit + +(require (except-in "../utils/utils.ss" extend)) +(require "signatures.ss" "constraint-structs.ss" + (utils tc-utils) + scheme/match) + +(import constraints^) +(export dmap^) + +;; dcon-meet : dcon dcon -> dcon +(define (dcon-meet dc1 dc2) + (match* (dc1 dc2) + [((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2)) + (struct dcon-exact (fixed2 rest2)))) + (unless (and rest2 (= (length fixed1) (length fixed2))) + (fail! fixed1 fixed2)) + (make-dcon-exact + (for/list ([c1 fixed1] + [c2 fixed2]) + (c-meet c1 c2 (c-X c1))) + (c-meet rest1 rest2 (c-X rest1)))] + [((struct dcon (fixed1 rest1)) (struct dcon-exact (fixed2 rest2))) + (dcon-meet dc2 dc1)] + [((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f))) + (unless (= (length fixed1) (length fixed2)) + (fail! fixed1 fixed2)) + (make-dcon + (for/list ([c1 fixed1] + [c2 fixed2]) + (c-meet c1 c2 (c-X c1))) + #f)] + [((struct dcon (fixed1 #f)) (struct dcon (fixed2 rest))) + (unless (>= (length fixed1) (length fixed2)) + (fail! fixed1 fixed2)) + (make-dcon + (for/list ([c1 fixed1] + [c2 (in-list-forever fixed2 rest)]) + (c-meet c1 c2 (c-X c1))) + #f)] + [((struct dcon (fixed1 rest)) (struct dcon (fixed2 #f))) + (dcon-meet dc2 dc1)] + [((struct dcon (fixed1 rest1)) (struct dcon (fixed2 rest2))) + (let-values ([(shorter longer srest lrest) + (if (< (length fixed1) (length fixed2)) + (values fixed1 fixed2 rest1 rest2) + (values fixed2 fixed1 rest2 rest1))]) + (make-dcon + (for/list ([c1 longer] + [c2 (in-list-forever shorter srest)]) + (c-meet c1 c2 (c-X c1))) + (c-meet lrest srest (c-X lrest))))] + [((struct dcon-dotted (c1 bound1)) (struct dcon-dotted (c2 bound2))) + (unless (eq? bound1 bound2) + (fail! bound1 bound2)) + (make-dcon-dotted (c-meet c1 c2 bound1) bound1)] + [((struct dcon _) (struct dcon-dotted _)) + (fail! dc1 dc2)] + [((struct dcon-dotted _) (struct dcon _)) + (fail! dc1 dc2)] + [(_ _) (int-err "Got non-dcons: ~a ~a" dc1 dc2)])) + +(define (dmap-meet dm1 dm2) + (make-dmap + (hash-union (dmap-map dm1) (dmap-map dm2) + (lambda (k dc1 dc2) (dcon-meet dc1 dc2))))) \ No newline at end of file diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss new file mode 100644 index 00000000..c640d363 --- /dev/null +++ b/collects/typed-scheme/infer/infer-unit.ss @@ -0,0 +1,491 @@ +#lang scheme/unit + +(require (except-in "../utils/utils.ss")) +(require (rep free-variance type-rep effect-rep rep-utils) + (private type-effect-convenience union subtype remove-intersect) + (utils tc-utils) + (env type-name-env) + (except-in (private type-utils) Dotted) + "constraint-structs.ss" + "signatures.ss" + (only-in (env type-environments) lookup current-tvars) + scheme/match + mzlib/etc + mzlib/trace + scheme/list) + +(import dmap^ constraints^ promote-demote^) +(export infer^) + +(define (empty-set) '()) + +(define current-seen (make-parameter (empty-set))) + +(define (seen-before s t) (cons (Type-seq s) (Type-seq t))) +(define (remember s t A) (cons (seen-before s t) A)) +(define (seen? s t) (member (seen-before s t) (current-seen))) + + +(define (dmap-constraint dmap dbound v) + (let ([dc (hash-ref dmap dbound #f)]) + (match dc + [(struct dcon (fixed #f)) + (if (eq? dbound v) + (no-constraint v) + (hash-ref fixed v (no-constraint v)))] + [(struct dcon (fixed rest)) + (if (eq? dbound v) + rest + (hash-ref fixed v (no-constraint v)))] + [(struct dcon-dotted (type bound)) + (if (eq? bound v) + type + (no-constraint v))] + [_ (no-constraint v)]))) + +(define (map/cset f cset) + (make-cset (for/list ([(cmap dmap) (in-pairs (cset-maps cset))]) + (f cmap dmap)))) + +(define (singleton-dmap dbound dcon) + (make-dmap (make-immutable-hash (list (cons dbound dcon))))) + +(define (hash-remove* hash keys) + (for/fold ([h hash]) ([k (in-list keys)]) (hash-remove h k))) + +(define (mover cset dbound vars f) + (map/cset + (lambda (cmap dmap) + (cons (hash-remove* cmap vars) + (dmap-meet + (singleton-dmap + dbound + (f cmap)) + dmap))) + cset)) + +(define (move-vars-to-dmap cset dbound vars) + (mover cset dbound vars + (lambda (cmap) + (make-dcon (for/list ([v vars]) + (hash-ref cmap v + (lambda () (int-err "No constraint for new var ~a" v)))) + #f)))) + +(define (move-rest-to-dmap cset dbound #:exact [exact? #f]) + (mover cset dbound (list dbound) + (lambda (cmap) + ((if exact? make-dcon-exact make-dcon) + null + (hash-ref cmap dbound + (lambda () (int-err "No constraint for bound ~a" dbound))))))) + +(define (move-vars+rest-to-dmap cset dbound vars #:exact [exact? #f]) + (map/cset + (lambda (cmap dmap) + (cons (hash-remove* cmap vars) + (dmap-meet + (singleton-dmap + dbound + ((if exact? make-dcon-exact make-dcon) + (for/list ([v vars]) + (hash-ref cmap v + (lambda () (int-err "No constraint for new var ~a" v)))) + (hash-ref cmap dbound + (lambda () (int-err "No constraint for bound ~a" dbound))))) + dmap))) + cset)) + +;; t and s must be *latent* effects +(define (cgen/eff V X t s) + (match* (t s) + [(e e) (empty-cset X)] + [((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: s)) + (cset-meet (cgen V X t s) (cgen V X s t))] + [((Latent-Remove-Effect: t) (Latent-Remove-Effect: s)) + (cset-meet (cgen V X t s) (cgen V X s t))] + [(_ _) (fail! t s)])) + +(define (cgen/eff/list V X ts ss) + (unless (>= (length ts) (length ss)) (fail! ts ss)) + (cset-meet* (for/list ([t ts] [s ss]) (cgen/eff V X t s)))) + +(define (cgen/arr V X t-arr s-arr) + (define (cg S T) (cgen V X S T)) + (match* (t-arr s-arr) + [((arr: ts t #f #f '() t-thn-eff t-els-eff) + (arr: ss s #f #f '() s-thn-eff s-els-eff)) + (cset-meet* + (list (cgen/list V X ss ts) + (cg t s) + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff)))] + [((arr: ts t t-rest #f '() t-thn-eff t-els-eff) + (arr: ss s s-rest #f '() s-thn-eff s-els-eff)) + (let ([arg-mapping + (cond [(and t-rest s-rest (<= (length ts) (length ss))) + (cgen/list V X (cons s-rest ss) (cons t-rest (extend ss ts t-rest)))] + [(and t-rest s-rest (>= (length ts) (length ss))) + (cgen/list V X (cons s-rest (extend ts ss s-rest)) (cons t-rest ts))] + [(and t-rest (not s-rest) (<= (length ts) (length ss))) + (cgen/list V X ss (extend ss ts t-rest))] + [(and s-rest (not t-rest) (>= (length ts) (length ss))) + (cgen/list V X (extend ts ss s-rest) ts)] + [else (fail! S T)])] + [ret-mapping (cg t s)]) + (cset-meet* + (list arg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff))))] + [((arr: ts t #f (cons dty dbound) '() t-thn-eff t-els-eff) + (arr: ss s #f #f '() s-thn-eff s-els-eff)) + (unless (memq dbound X) + (fail! S T)) + (unless (<= (length ts) (length ss)) + (fail! S T)) + (let* ([num-vars (- (length ss) (length ts))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound dty))] + [new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null t-thn-eff t-els-eff) s-arr)]) + (move-vars-to-dmap new-cset dbound vars))] + [((arr: ts t #f #f '() t-thn-eff t-els-eff) + (arr: ss s #f (cons dty dbound) '() s-thn-eff s-els-eff)) + (unless (memq dbound X) + (fail! S T)) + (unless (<= (length ss) (length ts)) + (fail! S T)) + (let* ([num-vars (- (length ts) (length ss))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound dty))] + [new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null s-thn-eff s-els-eff))]) + (move-vars-to-dmap new-cset dbound vars))] + [((arr: ts t #f (cons t-dty dbound) '() t-thn-eff t-els-eff) + (arr: ss s #f (cons s-dty dbound) '() s-thn-eff s-els-eff)) + (unless (= (length ts) (length ss)) + (fail! S T)) + ;; If we want to infer the dotted bound, then why is it in both types? + (when (memq dbound X) + (fail! S T)) + (let* ([arg-mapping (cgen/list V X ss ts)] + [darg-mapping (cgen V X s-dty t-dty)] + [ret-mapping (cg t s)]) + (cset-meet* + (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff))))] + [((arr: ts t #f (cons t-dty dbound) '() t-thn-eff t-els-eff) + (arr: ss s #f (cons s-dty dbound*) '() s-thn-eff s-els-eff)) + (unless (= (length ts) (length ss)) + (fail! S T)) + (let* ([arg-mapping (cgen/list V X ss ts)] + [darg-mapping (cgen V (cons dbound* X) s-dty t-dty)] + [ret-mapping (cg t s)]) + (cset-meet* + (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff))))] + [((arr: ts t t-rest #f '() t-thn-eff t-els-eff) + (arr: ss s #f (cons s-dty dbound) '() s-thn-eff s-els-eff)) + (unless (memq dbound X) + (fail! S T)) + (if (<= (length ts) (length ss)) + ;; the simple case + (let* ([arg-mapping (cgen/list V X ss (extend ss ts t-rest))] + [darg-mapping (move-rest-to-dmap (cgen V X s-dty t-rest) dbound)] + [ret-mapping (cg t s)]) + (cset-meet* (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff)))) + ;; the hard case + (let* ([num-vars (- (length ts) (length ss))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound s-dty))] + [new-cset (cgen/arr V (append vars X) t-arr + (make-arr (append ss new-tys) s #f (cons s-dty dbound) null s-thn-eff s-els-eff))]) + (move-vars+rest-to-dmap new-cset dbound vars)))] + ;; If dotted <: starred is correct, add it below. Not sure it is. + [((arr: ts t #f (cons t-dty dbound) '() t-thn-eff t-els-eff) + (arr: ss s s-rest #f '() s-thn-eff s-els-eff)) + (unless (memq dbound X) + (fail! S T)) + (cond [(< (length ts) (length ss)) + ;; the hard case + (let* ([num-vars (- (length ss) (length ts))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound t-dty))] + [arg-mapping (cgen/list V (append vars X) ss (append ts new-tys))] + [darg-mapping (cgen V X s-rest t-dty)] + [ret-mapping (cg t s)] + [new-cset + (cset-meet* (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff)))]) + (move-vars+rest-to-dmap new-cset dbound vars #:exact #t))] + [else + ;; the simple case + (let* ([arg-mapping (cgen/list V X (extend ts ss s-rest) ts)] + [darg-mapping (move-rest-to-dmap (cgen V X s-rest t-dty) dbound #:exact #t)] + [ret-mapping (cg t s)]) + (cset-meet* (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff))))])] + [(_ _) (fail! S T)])) + +;; determine constraints on the variables in X that would make T a supertype of S +;; the resulting constraints will not mention V +(define (cgen V X S T) + (define (cg S T) (cgen V X S T)) + (define empty (empty-cset X)) + (define (singleton S X T) + (insert empty X S T)) + (if (seen? S T) + empty + (parameterize ([match-equality-test type-equal?] + [current-seen (remember S T (current-seen))]) + (match* + (S T) + [(a a) empty] + [(_ (Univ:)) empty] + + [((F: (? (lambda (e) (memq e X)) v)) S) + (when (match S + [(F: v*) + (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))] + [_ #f]) + (fail! S T)) + (singleton (Un) v (var-demote S V))] + [(S (F: (? (lambda (e) (memq e X)) v))) + (when (match S + [(F: v*) + (just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))] + [_ #f]) + (fail! S T)) + (singleton (var-promote S V) v Univ)] + + ;; two unions with the same number of elements, so we just try to unify them pairwise + #;[((Union: l1) (Union: l2)) + (=> unmatch) + (unless (= (length l1) (length l2)) + (unmatch)) + (cgen-union V X l1 l2)] + + #;[((Poly: v1 b1) (Poly: v2 b2)) + (unless (= (length v1) (length v2)) + (fail! S T)) + (let ([b2* (subst-all (map list v2 v1) b2)]) + (cg b1 b2*))] + + #;[((PolyDots: (list v1 ... r1) b1) (PolyDots: (list v2 ... r2) b2)) + (unless (= (length v1) (length v2)) + (fail! S T)) + (let ([b2* (substitute-dotted v1 v1 v2 (subst-all (map list v2 v1) b2))]) + (cg b1 b2*))] + + [((Poly: v1 b1) T) + (cgen (append v1 V) X b1 T)] + + #;[((PolyDots: (list v1 ... r1) b1) T) + (let ([b1* (var-demote b1 (cons r1 v1))]) + (cg b1* T))] + + #; + [((Poly-unsafe: n b) (Poly-unsafe: n* b*)) + (unless (= n n*) + (fail! S T)) + (cg b b*)] + + + [((Union: es) S) (cset-meet* (cons empty (for/list ([e es]) (cg e S))))] + ;; we might want to use multiple csets here, but I don't think it makes a difference + [(S (Union: es)) (or + (for/or + ([e es]) + (with-handlers + ([exn:infer? (lambda _ #f)]) + (cg S e))) + (fail! S T))] + + [((Struct: nm p flds proc _ _ _) (Struct: nm p flds* proc* _ _ _)) + (let-values ([(flds flds*) + (cond [(and proc proc*) + (values (cons proc flds) (cons proc* flds*))] + [(or proc proc*) + (fail! S T)] + [else (values flds flds*)])]) + (cgen/list V X flds flds*))] + [((Name: n) (Name: n*)) + (if (free-identifier=? n n*) + null + (fail! S T))] + [((Pair: a b) (Pair: a* b*)) + (cset-meet (cg a a*) (cg b b*))] + ;; if we have two mu's, we rename them to have the same variable + ;; and then compare the bodies + [((Mu-unsafe: s) (Mu-unsafe: t)) + (cg s t)] + ;; other mu's just get unfolded + [(s (? Mu? t)) (cg s (unfold t))] + [((? Mu? s) t) (cg (unfold s) t)] + ;; type application + [((App: (Name: n) args _) + (App: (Name: n*) args* _)) + (unless (free-identifier=? n n*) + (fail! S T)) + (let ([x (instantiate-poly (lookup-type-name n) args)] + [y (instantiate-poly (lookup-type-name n) args*)]) + (cg x y))] + [((Values: ss) (Values: ts)) + (unless (= (length ss) (length ts)) + (fail! ss ts)) + (cgen/list V X ss ts)] + [((Values: ss) (ValuesDots: ts t-dty dbound)) + (unless (>= (length ss) (length ts)) + (fail! ss ts)) + (unless (memq dbound X) + (fail! S T)) + (let* ([num-vars (- (length ss) (length ts))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound t-dty))] + [new-cset (cgen/list V (append vars X) ss (append ts new-tys))]) + (move-vars-to-dmap new-cset dbound vars))] + [((ValuesDots: ss s-dty dbound) (Values: ts)) + (unless (>= (length ts) (length ss)) + (fail! ss ts)) + (unless (memq dbound X) + (fail! S T)) + (let* ([num-vars (- (length ts) (length ss))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound s-dty))] + [new-cset (cgen/list V (append vars X) (append ss new-tys) ts)]) + (move-vars-to-dmap new-cset dbound vars))] + [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound)) + (when (memq dbound X) (fail! ss ts)) + (cgen/list V X (cons s-dty ss) (cons t-dty ts))] + [((Vector: e) (Vector: e*)) + (cset-meet (cg e e*) (cg e* e))] + [((Box: e) (Box: e*)) + (cset-meet (cg e e*) (cg e* e))] + [((Hashtable: s1 s2) (Hashtable: t1 t2)) + ;; the key is covariant, the value is invariant + (cset-meet* (list (cg s1 t1) (cg t2 s2) (cg s2 t2)))] + [((Syntax: s1) (Syntax: s2)) + (cg s1 s2)] + ;; parameters are just like one-arg functions + [((Param: in1 out1) (Param: in2 out2)) + (cset-meet (cg in2 in1) (cg out1 out2))] + [((Function: (list t-arr ...)) + (Function: (list s-arr ...))) + (=> unmatch) + (cset-combine + (filter + values ;; only generate the successful csets + (for*/list + ([t-arr t-arr] [s-arr s-arr]) + (with-handlers ([exn:infer? (lambda (_) #f)]) + (cgen/arr V X t-arr s-arr)))))] + [(_ _) + (cond [(subtype S T) empty] + ;; or, nothing worked, and we fail + [else (fail! S T)])])))) + +(define (check-vars must-vars subst) + (and (for/and ([v must-vars]) + (assq v subst)) + subst)) + +(define (subst-gen C R must-vars) + (define (constraint->type v #:variable [variable #f]) + (match v + [(struct c (S X T)) + (let ([var (hash-ref (free-vars* R) (or variable X) Constant)]) + ;(printf "variance was: ~a~nR was ~a~nX was ~a~n" var R (or variable X)) + (evcase var + [Constant S] + [Covariant S] + [Contravariant T] + [Invariant S] + [Dotted T]))])) + (match (car (cset-maps C)) + [(cons cmap (struct dmap (dm))) + (check-vars + must-vars + (append + (for/list ([(k dc) dm]) + (match dc + [(struct dcon (fixed rest)) + (list k + (for/list ([f fixed]) + (constraint->type f #:variable k)) + (and rest (constraint->type rest)))] + [(struct dcon-exact (fixed rest)) + (list k + (for/list ([f fixed]) + (constraint->type f #:variable k)) + (constraint->type rest))])) + (for/list ([(k v) cmap]) + (list k (constraint->type v)))))])) + +(define (cgen/list V X S T) + (unless (= (length S) (length T)) + (fail! S T)) + (cset-meet* (for/list ([s S] [t T]) (cgen V X s t)))) + +;; X : variables to infer +;; S : actual argument types +;; T : formal argument types +;; R : result type +;; must-vars : variables that must be in the substitution +;; expected : boolean +;; returns a substitution +;; if R is #f, we don't care about the substituion +;; just return a boolean result +(define (infer X S T R must-vars [expected #f]) + (with-handlers ([exn:infer? (lambda _ #f)]) + (let ([cs (cgen/list null X S T)]) + (if (not expected) + (subst-gen cs R must-vars) + (cset-meet cs (cgen null X R expected)))))) + +;; like infer, but T-var is the vararg type: +(define (infer/vararg X S T T-var R must-vars [expected #f]) + (define new-T (extend S T T-var)) + (and ((length S) . >= . (length T)) + (infer X S new-T R must-vars expected))) + +;; like infer, but dotted-var is the bound on the ... +;; and T-dotted is the repeated type +(define (infer/dots X dotted-var S T T-dotted R must-vars [expected #f]) + (with-handlers ([exn:infer? (lambda _ #f)]) + (let* ([short-S (take S (length T))] + [rest-S (drop S (length T))] + [cs-short (cgen/list null (cons dotted-var X) short-S T)] + [new-vars (for/list ([i (in-range (length rest-S))]) (gensym dotted-var))] + [new-Ts (for/list ([v new-vars]) + (substitute (make-F v) dotted-var + (substitute-dots (map make-F new-vars) #f dotted-var T-dotted)))] + [cs-dotted (cgen/list null (append new-vars X) rest-S new-Ts)] + [cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)] + [cs (cset-meet cs-short cs-dotted*)]) + (if (not expected) + (subst-gen cs R must-vars) + (cset-meet cs (cgen null X R expected)))))) + +(define (infer/simple S T R) + (infer (fv/list T) S T R)) + +(define (i s t r) + (infer/simple (list s) (list t) r)) + +;(trace cgen/arr #;cgen #;cgen/list) diff --git a/collects/typed-scheme/infer/infer.ss b/collects/typed-scheme/infer/infer.ss new file mode 100644 index 00000000..208943a3 --- /dev/null +++ b/collects/typed-scheme/infer/infer.ss @@ -0,0 +1,12 @@ +#lang scheme/base + +(require (except-in "../utils/utils.ss" infer)) +(require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss" + "restrict.ss" "promote-demote.ss" + (only-in scheme/unit provide-signature-elements) + (utils unit-utils)) + +(provide-signature-elements restrict^ infer^) + +(define-values/link-units/infer + infer@ constraints@ dmap@ restrict@ promote-demote@) \ No newline at end of file diff --git a/collects/typed-scheme/infer/promote-demote.ss b/collects/typed-scheme/infer/promote-demote.ss new file mode 100644 index 00000000..87051229 --- /dev/null +++ b/collects/typed-scheme/infer/promote-demote.ss @@ -0,0 +1,92 @@ +#lang scheme/unit + +(require "../utils/utils.ss") +(require (rep type-rep) + (private type-effect-convenience union type-utils) + "signatures.ss" + scheme/list) + +(import) +(export promote-demote^) + +(define (V-in? V . ts) + (for/or ([e (append* (map fv ts))]) + (memq e V))) + +(define (var-promote T V) + (define (vp t) (var-promote t V)) + (define (inv t) (if (V-in? V t) Univ t)) + (type-case vp T + [#:F name (if (memq name V) Univ T)] + [#:Vector t (make-Vector (inv t))] + [#:Box t (make-Box (inv t))] + [#:Hashtable k v + (if (V-in? V v) + Univ + (make-Hashtable (vp k) v))] + [#:Param in out + (make-Param (var-demote in V) + (vp out))] + [#:arr dom rng rest drest kws thn els + (cond + [(apply V-in? V (append thn els)) + (make-arr null (Un) Univ #f null null)] + [(and drest (memq (cdr drest) V)) + (make-arr (for/list ([d dom]) (var-demote d V)) + (vp rng) + (var-demote (car drest) V) + #f + (for/list ([(kw kwt) (in-pairs kws)]) + (cons kw (var-demote kwt V))) + thn + els)] + [else + (make-arr (for/list ([d dom]) (var-demote d V)) + (vp rng) + (and rest (var-demote rest V)) + (and drest + (cons (var-demote (car drest) V) + (cdr drest))) + (for/list ([(kw kwt) (in-pairs kws)]) + (cons kw (var-demote kwt V))) + thn + els)])])) + +(define (var-demote T V) + (define (vd t) (var-demote t V)) + (define (inv t) (if (V-in? V t) (Un) t)) + (type-case vd T + [#:F name (if (memq name V) (Un) T)] + [#:Vector t (make-Vector (inv t))] + [#:Box t (make-Box (inv t))] + [#:Hashtable k v + (if (V-in? V v) + (Un) + (make-Hashtable (vd k) v))] + [#:Param in out + (make-Param (var-promote in V) + (vd out))] + [#:arr dom rng rest drest kws thn els + (cond + [(apply V-in? V (append thn els)) + (make-arr null (Un) Univ #f null null)] + [(and drest (memq (cdr drest) V)) + (make-arr (for/list ([d dom]) (var-promote d V)) + (vd rng) + (var-promote (car drest) V) + #f + (for/list ([(kw kwt) (in-pairs kws)]) + (cons kw (var-promote kwt V))) + thn + els)] + [else + (make-arr (for/list ([d dom]) (var-promote d V)) + (vd rng) + (and rest (var-promote rest V)) + (and drest + (cons (var-promote (car drest) V) + (cdr drest))) + (for/list ([(kw kwt) (in-pairs kws)]) + (cons kw (var-promote kwt V))) + thn + els)])])) diff --git a/collects/typed-scheme/infer/restrict.ss b/collects/typed-scheme/infer/restrict.ss new file mode 100644 index 00000000..e1365605 --- /dev/null +++ b/collects/typed-scheme/infer/restrict.ss @@ -0,0 +1,37 @@ +#lang scheme/unit + +(require "../utils/utils.ss") +(require (rep type-rep) + (private type-utils union remove-intersect subtype) + "signatures.ss" + scheme/match) + +(import infer^) +(export restrict^) + + +;; NEW IMPL +;; restrict t1 to be a subtype of t2 +(define (restrict t1 t2) + ;; we don't use union map directly, since that might produce too many elements + (define (union-map f l) + (match l + [(Union: es) + (let ([l (map f es)]) + ;(printf "l is ~a~n" l) + (apply Un l))])) + (cond + [(subtype t1 t2) t1] ;; already a subtype + [(match t2 + [(Poly: vars t) + (let ([subst (infer vars (list t1) (list t) t1 vars)]) + (and subst (restrict t1 (subst-all subst t1))))] + [_ #f])] + [(Union? t1) (union-map (lambda (e) (restrict e t2)) t1)] + [(Mu? t1) + (restrict (unfold t1) t2)] + [(Mu? t2) (restrict t1 (unfold t2))] + [(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1 + [(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty + [else t2] ;; t2 and t1 have a complex relationship, so we punt + )) \ No newline at end of file diff --git a/collects/typed-scheme/infer/signatures.ss b/collects/typed-scheme/infer/signatures.ss new file mode 100644 index 00000000..6db02b38 --- /dev/null +++ b/collects/typed-scheme/infer/signatures.ss @@ -0,0 +1,29 @@ +#lang scheme/base +(require scheme/unit) +(provide (all-defined-out)) + +(define-signature dmap^ + (dmap-meet)) + +(define-signature promote-demote^ + (var-promote var-demote)) + +(define-signature constraints^ + (exn:infer? + fail-sym + ;; inference failure - masked before it gets to the user program + (define-syntaxes (fail!) + (syntax-rules () + [(_ s t) (raise fail-sym)])) + cset-meet cset-meet* + no-constraint + empty-cset + insert + cset-combine + c-meet)) + +(define-signature restrict^ + (restrict)) + +(define-signature infer^ + (infer infer/vararg infer/dots)) diff --git a/collects/typed-scheme/no-check.ss b/collects/typed-scheme/no-check.ss new file mode 100644 index 00000000..470a7bed --- /dev/null +++ b/collects/typed-scheme/no-check.ss @@ -0,0 +1,5 @@ +#lang scheme/base + +(require "private/prims.ss") +(provide (all-from-out scheme/base) + (all-from-out "private/prims.ss")) \ No newline at end of file diff --git a/collects/typed-scheme/no-check/lang/reader.ss b/collects/typed-scheme/no-check/lang/reader.ss new file mode 100644 index 00000000..c35cbecc --- /dev/null +++ b/collects/typed-scheme/no-check/lang/reader.ss @@ -0,0 +1,13 @@ +#lang scheme/base +(require (prefix-in r: "../../typed-reader.ss") + (only-in syntax/module-reader wrap-read-all)) + +(define (*read in modpath line col pos) + (wrap-read-all 'typed-scheme/no-check in r:read modpath #f line col pos)) + +(define (*read-syntax src in modpath line col pos) + (wrap-read-all + 'typed-scheme/no-check in (lambda (in) (r:read-syntax src in)) + modpath src line col pos)) + +(provide (rename-out [*read read] [*read-syntax read-syntax])) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 59708588..6600a1f7 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -3,6 +3,7 @@ ;; these are libraries providing functions we add types to that are not in scheme/base (require "extra-procs.ss" + "../utils/utils.ss" (only-in scheme/list cons? take drop add-between last filter-map) (only-in rnrs/lists-6 fold-left) '#%paramz @@ -15,13 +16,12 @@ ;; these are all for constructing the types given to variables (require (for-syntax scheme/base - "init-envs.ss" - "effect-rep.ss" - (except-in "type-rep.ss" make-arr) + (env init-envs) + (except-in (rep effect-rep type-rep) make-arr) "type-effect-convenience.ss" (only-in "type-effect-convenience.ss" [make-arr* make-arr]) "union.ss" - "tc-structs.ss")) + (typecheck tc-structs))) (define-for-syntax (initialize-others) (d-s date @@ -57,6 +57,9 @@ [qq-append qq-append-ty] [id ty] ...)))])) +(define-for-syntax (one-of/c . args) + (apply Un (map -val args))) + (define-initial-env initial-env ;; make-promise @@ -145,9 +148,13 @@ [string-append (->* null -String -String)] [open-input-string (-> -String -Input-Port)] [open-output-file - (cl-> - [(-Pathlike) -Port] - [(-Pathlike Sym) -Port])] + (->key -Pathlike + #:mode (one-of/c 'binary 'text) #f + #:exists (one-of/c 'error 'append 'update 'can-update + 'replace 'truncate + 'must-truncate 'truncate/replace) + #f + -Output-Port)] [read (cl-> [(-Port) -Sexp] [() -Sexp])] @@ -205,9 +212,7 @@ [remove* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)] [((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))] - - [call-with-values (-poly (a b) (-> (-> a) (-> a b) b))] - + (error (make-Function (list (make-arr null (Un)) @@ -246,7 +251,6 @@ (- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))) (max (->* (list N) N N)) (min (->* (list N) N N)) - [values (make-Poly '(a) (-> (-v a) (-v a)))] [vector-ref (make-Poly (list 'a) ((make-Vector (-v a)) N . -> . (-v a)))] [build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (make-Vector a)))] @@ -467,7 +471,7 @@ [(-Bytes N) -Bytes] [(-Bytes N N) -Bytes])] [bytes-length (-> -Bytes N)] - [open-input-file (-> -Pathlike -Input-Port)] + [open-input-file (->key -Pathlike #:mode (Un (-val 'binary) (-val 'text)) #f -Input-Port)] [close-input-port (-> -Input-Port -Void)] [close-output-port (-> -Output-Port -Void)] [read-line (cl-> @@ -553,8 +557,11 @@ [syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a)) (-> (-Syntax Univ) Univ Univ)))] - [values* (-polydots (a) (null (a a) . ->... . (make-ValuesDots null a 'a)))] - [call-with-values* (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b))] + [values (-polydots (a) (null (a a) . ->... . (make-ValuesDots null a 'a)))] + [call-with-values (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b))] + + [eof (-val eof)] + [read-accept-reader (-Param B B)] ) (begin-for-syntax diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss index cc4bb42a..6058fd4b 100644 --- a/collects/typed-scheme/private/base-types.ss +++ b/collects/typed-scheme/private/base-types.ss @@ -1,9 +1,10 @@ #lang scheme/base +(require (except-in "../utils/utils.ss" extend)) (require (for-syntax scheme/base - "init-envs.ss" - (except-in "type-rep.ss" make-arr) + (env init-envs) + (except-in (rep type-rep) make-arr) "type-effect-convenience.ss" (only-in "type-effect-convenience.ss" [make-arr* make-arr]) "union.ss")) diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss index 83aa9c40..b5cd5378 100644 --- a/collects/typed-scheme/private/extra-procs.ss +++ b/collects/typed-scheme/private/extra-procs.ss @@ -1,5 +1,5 @@ #lang scheme/base -(provide assert call-with-values* values*) +(provide assert call-with-values* values* foo) (define (assert v) (unless v @@ -15,4 +15,7 @@ (car as) (map car bss)))) (define call-with-values* call-with-values) -(define values* values) \ No newline at end of file +(define values* values) + +(define (foo x #:bar [bar #f]) + bar) \ No newline at end of file diff --git a/collects/typed-scheme/private/mutated-vars.ss b/collects/typed-scheme/private/mutated-vars.ss index 6e7a2c2d..a362bd53 100644 --- a/collects/typed-scheme/private/mutated-vars.ss +++ b/collects/typed-scheme/private/mutated-vars.ss @@ -14,12 +14,11 @@ ;; syntax -> void (define (fmv/list lstx) (for-each find-mutated-vars (syntax->list lstx))) - ;(printf "called with ~a~n" (syntax->datum form)) + ;(when (and (pair? (syntax->datum form))) (printf "called with ~a~n" (syntax->datum form))) (kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal require/typed-internal) ;; what we care about: set! [(set! v e) (begin - ;(printf "mutated var found: ~a~n" (syntax-e #'v)) (module-identifier-mapping-put! table #'v #t))] [(define-values (var ...) expr) (find-mutated-vars #'expr)] @@ -28,15 +27,13 @@ [(begin0 . rest) (fmv/list #'rest)] [(#%plain-lambda _ . rest) (fmv/list #'rest)] [(case-lambda (_ . rest) ...) (for-each fmv/list (syntax->list #'(rest ...)))] - [(if e1 e2) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e2))] - [(if e1 e2 e3) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e1) (find-mutated-vars #'e3))] - [(with-continuation-mark e1 e2 e3) (begin (find-mutated-vars #'e1) - (find-mutated-vars #'e1) - (find-mutated-vars #'e3))] + [(if . es) (fmv/list #'es)] + [(with-continuation-mark . es) (fmv/list #'es)] [(let-values ([_ e] ...) . b) (begin (fmv/list #'(e ...)) (fmv/list #'b))] [(letrec-values ([_ e] ...) . b) (begin (fmv/list #'(e ...)) - (fmv/list #'b))] + (fmv/list #'b))] + [(#%expression e) (find-mutated-vars #'e)] ;; all the other forms don't have any expression subforms (like #%top) [_ (void)])) diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 2b92c493..07adfd9e 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -2,16 +2,15 @@ (provide parse-type parse-type/id) -(require (except-in "type-rep.ss" make-arr) +(require (except-in "../utils/utils.ss" extend)) +(require (except-in (rep type-rep) make-arr) "type-effect-convenience.ss" (only-in "type-effect-convenience.ss" [make-arr* make-arr]) - "tc-utils.ss" + (utils tc-utils) "union.ss" syntax/stx - (except-in "type-environments.ss") - "type-name-env.ss" - "type-alias-env.ss" - "type-utils.ss" + (env type-environments type-name-env type-alias-env) + "type-utils.ss" scheme/match) (define enable-mu-parsing (make-parameter #t)) @@ -213,7 +212,7 @@ ;(printf "found a type name ~a~n" #'id) (make-Name #'id)] [else - (tc-error/delayed "unbound type ~a" (syntax-e #'id)) + (tc-error/delayed "unbound type name ~a" (syntax-e #'id)) Univ])] [(All . rest) (eq? (syntax-e #'All) 'All) (tc-error "All: bad syntax")] diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss index ef3e7cc5..9068659c 100644 --- a/collects/typed-scheme/private/prims.ss +++ b/collects/typed-scheme/private/prims.ss @@ -22,20 +22,20 @@ This file defines two sorts of primitives. All of them are provided into any mod (provide (all-defined-out) (rename-out [define-typed-struct define-struct:])) +(require (except-in "../utils/utils.ss" extend)) (require (for-syntax scheme/base - "type-rep.ss" + (rep type-rep) mzlib/match "parse-type.ss" syntax/struct syntax/stx - "utils.ss" - "tc-utils.ss" - "type-name-env.ss" + (utils utils tc-utils) + (env type-name-env) "type-contract.ss")) (require "require-contract.ss" - "internal-forms.ss" + (typecheck internal-forms) (except-in mzlib/contract ->) (only-in mzlib/contract [-> c->]) mzlib/struct diff --git a/collects/typed-scheme/private/remove-intersect.ss b/collects/typed-scheme/private/remove-intersect.ss index f9b273e8..d244fb73 100644 --- a/collects/typed-scheme/private/remove-intersect.ss +++ b/collects/typed-scheme/private/remove-intersect.ss @@ -1,7 +1,8 @@ #lang scheme/base -(require "type-rep.ss" "union.ss" "subtype.ss" - "type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss" +(require (except-in "../utils/utils.ss" extend)) +(require (rep type-rep) + (private union subtype resolve-type type-effect-convenience type-utils) mzlib/plt-match mzlib/trace) (provide (rename-out [*remove remove]) overlap) diff --git a/collects/typed-scheme/private/resolve-type.ss b/collects/typed-scheme/private/resolve-type.ss index d68de692..6526a428 100644 --- a/collects/typed-scheme/private/resolve-type.ss +++ b/collects/typed-scheme/private/resolve-type.ss @@ -1,6 +1,7 @@ #lang scheme/base +(require "../utils/utils.ss") -(require "type-rep.ss" "type-name-env.ss" "tc-utils.ss" +(require (rep type-rep) (env type-name-env) (utils tc-utils) "type-utils.ss" mzlib/plt-match mzlib/trace) diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 398fe7b2..1db8c33b 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -1,12 +1,13 @@ #lang scheme/base +(require "../utils/utils.ss") -(require (except-in "type-rep.ss" sub-eff) "type-utils.ss" - "tc-utils.ss" - "effect-rep.ss" +(require (except-in (rep type-rep effect-rep) sub-eff) + (utils tc-utils) + "type-utils.ss" "type-comparison.ss" "resolve-type.ss" - "type-name-env.ss" - (only-in "infer-dummy.ss" unify) + (env type-name-env) + (only-in (infer infer-dummy) unify) mzlib/plt-match mzlib/trace) @@ -100,10 +101,13 @@ (match (list s t) ;; top for functions is above everything [(list _ (top-arr:)) A0] - [(list (arr: s1 s2 #f #f thn-eff els-eff) (arr: t1 t2 #f #f thn-eff els-eff)) - (let ([A1 (subtypes* A0 t1 s1)]) + [(list (arr: s1 s2 #f #f (list (cons kw s-kw-ty) ...) thn-eff els-eff) + (arr: t1 t2 #f #f (list (cons kw t-kw-ty) ...) thn-eff els-eff)) + (let* ([A1 (subtypes* A0 t1 s1)] + [A2 (subtypes* A1 t-kw-ty s-kw-ty)]) (subtype* A1 s2 t2))] - [(list (arr: s1 s2 s3 #f thn-eff els-eff) (arr: t1 t2 t3 #f thn-eff* els-eff*)) + [(list (arr: s1 s2 s3 #f (list (cons kw s-kw-ty) ...) thn-eff els-eff) + (arr: t1 t2 t3 #f (list (cons kw t-kw-ty) ...) thn-eff* els-eff*)) (unless (or (and (null? thn-eff*) (null? els-eff*)) (and (effects-equal? thn-eff thn-eff*) @@ -115,10 +119,11 @@ (andmap sub-eff els-eff els-eff*))) (fail! s t)) ;; either the effects have to be the same, or the supertype can't have effects - (let ([A (subtypes*/varargs A0 t1 s1 s3)]) + (let* ([A2 (subtypes*/varargs A0 t1 s1 s3)] + [A3 (subtypes* A2 t-kw-ty s-kw-ty)]) (if (not t3) - (subtype* A s2 t2) - (let ([A1 (subtype* A t3 s3)]) + (subtype* A3 s2 t2) + (let ([A1 (subtype* A3 t3 s3)]) (subtype* A1 s2 t2))))] [else (fail! s t)]))) diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss index 1a72e73b..bbb83034 100644 --- a/collects/typed-scheme/private/type-annotation.ss +++ b/collects/typed-scheme/private/type-annotation.ss @@ -1,7 +1,11 @@ #lang scheme/base -(require "type-rep.ss" "parse-type.ss" "tc-utils.ss" "subtype.ss" "utils.ss" - "type-env.ss" "type-effect-convenience.ss" "resolve-type.ss" "union.ss" +(require (except-in "../utils/utils.ss" extend)) +(require (rep type-rep) + (utils tc-utils) + (env type-env) + "parse-type.ss" "subtype.ss" + "type-effect-convenience.ss" "resolve-type.ss" "union.ss" scheme/match mzlib/trace) (provide type-annotation get-type diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss index 9ae26d54..13aa199c 100644 --- a/collects/typed-scheme/private/type-effect-convenience.ss +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -1,14 +1,16 @@ #lang scheme/base -(require "type-rep.ss" - "effect-rep.ss" +(require "../utils/utils.ss") + +(require (rep type-rep effect-rep) + (utils tc-utils) scheme/match "type-comparison.ss" "type-effect-printer.ss" "union.ss" "subtype.ss" "type-utils.ss" - "tc-utils.ss" scheme/promise + (for-syntax macro-debugger/stxclass/stxclass) (for-syntax scheme/base)) (provide (all-defined-out)) @@ -33,7 +35,7 @@ [(Latent-Remove-Effect: t) (make-Remove-Effect t v)] [(True-Effect:) eff] [(False-Effect:) eff] - [_ (error 'internal-tc-error "can't add var to effect ~a" eff)])) + [_ (int-err "can't add var ~a to effect ~a" v eff)])) (define-syntax (-> stx) (syntax-case* stx (:) (lambda (a b) (eq? (syntax-e a) (syntax-e b))) @@ -78,11 +80,26 @@ [(Function: as) as])) (make-Function (map car (map funty-arities args)))) +(define-syntax (->key stx) + (syntax-parse stx + [(_ ty:expr ... ((k:keyword kty:expr opt:boolean)) ...* rng) + #'(make-Function + (list + (make-arr* (list ty ...) + rng + #f + #f + (list (make-Keyword 'k kty opt) ...) + null + null)))])) + (define make-arr* - (case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))] - [(dom rng rest) (make-arr dom rng rest #f (list) (list))] - [(dom rng rest eff1 eff2) (make-arr dom rng rest #f eff1 eff2)] - [(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest eff1 eff2)])) + (case-lambda [(dom rng) (make-arr dom rng #f #f null (list) (list))] + [(dom rng rest) (make-arr dom rng rest #f null (list) (list))] + [(dom rng rest eff1 eff2) (make-arr dom rng rest #f null eff1 eff2)] + [(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest null eff1 eff2)] + [(dom rng rest drest kws eff1 eff2) + (make-arr dom rng rest drest (sort #:key Keyword-kw kws keyword frees +(define (combine-frees freess) + (define ht (make-hasheq)) + (define (combine-var v w) + (cond + [(eq? v w) v] + [(eq? v Dotted) w] + [(eq? w Dotted) v] + [(eq? v Constant) w] + [(eq? w Constant) v] + [else Invariant])) + (for* ([old-ht (in-list freess)] + [(sym var) (in-hash old-ht)]) + (let* ([sym-var (hash-ref ht sym (lambda () #f))]) + (if sym-var + (hash-set! ht sym (combine-var var sym-var)) + (hash-set! ht sym var)))) + ht) + +;; given a set of free variables, change bound to ... +;; (if bound wasn't free, this will add it as Dotted +;; appropriately so that things that expect to see +;; it as "free" will -- fixes the case where the +;; dotted pre-type base doesn't use the bound). +(define (fix-bound vs bound) + (define vs* (hash-map* (lambda (k v) v) vs)) + (hash-set! vs* bound Dotted) + vs*) + +;; frees -> frees +(define (flip-variances vs) + (hash-map* + (lambda (k v) + (evcase + v + [Covariant Contravariant] + [Contravariant Covariant] + [v v])) + vs)) + +(define (make-invariant vs) + (hash-map* + (lambda (k v) Invariant) + vs)) + +(define (hash-map* f ht) + (define new-ht (make-hasheq)) + (for ([(k v) (in-hash ht)]) + (hash-set! new-ht k (f k v))) + new-ht) + +(define (without-below n frees) + (define new-ht (make-hasheq)) + (for ([(k v) (in-hash frees)]) + (when (>= k n) (hash-set! new-ht k v))) + new-ht) + +(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table + fix-bound) + +(define-syntax (unless-in-table stx) + (syntax-case stx () + [(_ table val . body) + (quasisyntax/loc stx + (hash-ref table val #,(syntax/loc #'body (lambda () . body))))])) diff --git a/collects/typed-scheme/rep/interning.ss b/collects/typed-scheme/rep/interning.ss new file mode 100644 index 00000000..d9eb6ff4 --- /dev/null +++ b/collects/typed-scheme/rep/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 #;'weak)) make-name key)] + [(_ (*name arg ...) make-ht make-name key-expr) + (define *name + (let ([table (make-ht)]) + (lambda (arg ...) + #;(all-count!) + (let ([key key-expr]) + (hash-ref table key + (lambda () + (let ([new (make-name (count!) arg ...)]) + (hash-set! table key new) + new)))))))])) + +(define (make-count!) + + (let ([state 0]) + (lambda () (begin0 state (set! state (add1 state))))) + #; + (let ([ch (make-channel)]) + (thread (lambda () (let loop ([n 0]) (channel-put ch n) (loop (add1 n))))) + (lambda () (channel-get ch)))) + +(provide #;count! #;all-count! union-count!) + +(define count! (make-count!)) +(define union-count! (make-count!)) +(define all-count! (make-count!)) +(define id-count! (make-count!)) + + + +(define identifier-table (make-module-identifier-mapping)) + +(define (hash-id id) + (module-identifier-mapping-get + identifier-table + id + (lambda () (let ([c (id-count!)]) + (module-identifier-mapping-put! identifier-table id c) + c)))) diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss new file mode 100644 index 00000000..2f49dba9 --- /dev/null +++ b/collects/typed-scheme/rep/rep-utils.ss @@ -0,0 +1,162 @@ +#lang scheme/base +(require "../utils/utils.ss") + +(require mzlib/struct + mzlib/plt-match + syntax/boundmap + (utils planet-requires) + "free-variance.ss" + "interning.ss" + mzlib/etc + (for-syntax + scheme/base + syntax/struct + syntax/stx + (utils utils))) + +(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq) + + + +;; hash table for defining folds over types +(define-values-for-syntax (type-name-ht effect-name-ht) + (values (make-hasheq) (make-hasheq))) + +(provide (for-syntax type-name-ht effect-name-ht)) + + +;; all types are Type? +(define-struct/printer Type (seq) (lambda (a b c) ((unbox print-type*) a b c))) + +(define-struct/printer Effect (seq) (lambda (a b c) ((unbox print-effect*) a b c))) + + + + + +;; type/effect definition macro + +(define-for-syntax type-rec-id #'type-rec-id) +(define-for-syntax effect-rec-id #'effect-rec-id) +(define-for-syntax fold-target #'fold-target) + +(provide (for-syntax type-rec-id effect-rec-id fold-target)) + +(define-syntaxes (dt de) + (let () + (define (parse-opts opts stx) + (let loop ([provide? #t] [intern? #f] [frees #t] [fold-rhs #f] [opts opts]) + (cond + [(null? opts) (values provide? intern? frees fold-rhs)] + [(eq? '#:no-provide (syntax-e (stx-car opts))) + (loop #f intern? frees fold-rhs (cdr opts))] + [(eq? '#:no-frees (syntax-e (stx-car opts))) + (loop #f intern? #f fold-rhs (cdr opts))] + [(not (and (stx-pair? opts) (stx-pair? (stx-car opts)))) + (raise-syntax-error #f "bad options" stx)] + [(eq? '#:intern (syntax-e (stx-car (car opts)))) + (loop provide? (stx-car (stx-cdr (car opts))) frees fold-rhs (cdr opts))] + [(eq? '#:frees (syntax-e (stx-car (car opts)))) + (loop provide? intern? (stx-cdr (car opts)) fold-rhs (cdr opts))] + [(eq? '#:fold-rhs (syntax-e (stx-car (car opts)))) + (loop provide? intern? frees (stx-cdr (car opts)) (cdr opts))] + [else (raise-syntax-error #f "bad options" stx)]))) + (define (mk par ht-stx) + (lambda (stx) + (syntax-case stx () + [(dform nm flds . opts) + (let*-values ([(provide? intern? frees fold-rhs) (parse-opts (syntax->list #'opts) #'opts)] + [(kw) (string->keyword (symbol->string (syntax-e #'nm)))]) + (with-syntax* + ([ex (id #'nm #'nm ":")] + [kw-stx kw] + [parent par] + [(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)] + [(flds* ...) #'flds] + [*maker (id #'nm "*" #'nm)] + [**maker (id #'nm "**" #'nm)] + [ht-stx ht-stx] + [bfs-fold-rhs (cond [(and fold-rhs (eq? (syntax-e (stx-car fold-rhs)) '#:base)) + #`(lambda (tr er) #,fold-target)] + [(and fold-rhs (stx-pair? fold-rhs)) + (with-syntax ([fr (stx-car fold-rhs)]) + #'(lambda (tr er) + #'fr))] + [fold-rhs (raise-syntax-error fold-rhs "something went wrong")] + [else #'(lambda (type-rec-id effect-rec-id) #`(*maker (#,type-rec-id flds*) ...))])] + [provides (if provide? + #`(begin + (provide ex pred acc ...) + (provide (rename-out [*maker maker]))) + #'(begin))] + [intern (cond + [(syntax? intern?) + #`(defintern (**maker . flds) maker #,intern?)] + [(null? (syntax-e #'flds)) + #'(defintern (**maker . flds) maker #f)] + [(stx-null? (stx-cdr #'flds)) #'(defintern (**maker . flds) maker . flds)] + [else #'(defintern (**maker . flds) maker (list . flds))])] + [frees (cond + [(not frees) #'(begin)] + ;; we know that this has no free vars + [(and (pair? frees) (syntax? (car frees)) (not (syntax-e (car frees)))) + (syntax/loc stx + (define (*maker . flds) + (define v (**maker . flds)) + #;(printf "~a entered in #f case~n" '*maker) + (unless-in-table + var-table v + (hash-set! var-table v empty-hash-table) + (hash-set! index-table v empty-hash-table)) + v))] + ;; we provided an expression each for calculating the free vars and free idxs + ;; this should really be 2 expressions, one for each kind + [(and (pair? frees) (pair? (cdr frees))) + (quasisyntax/loc + stx + (define (*maker . flds) + (define v (**maker . flds)) + #;(printf "~a entered in expr case ~n~a~n~a ~n" '*maker '#,(car frees) '#,(cadr frees)) + #, + (quasisyntax/loc (car frees) + (unless-in-table + var-table v + (hash-set! var-table v #,(car frees)) + (hash-set! index-table v #,(cadr frees)))) + #;(printf "~a exited in expr case~n" '*maker) + v))] + [else + (let + ([combiner + (lambda (f flds) + (syntax-case flds () + [() #'empty-hash-table] + [(e) #`(#,f e)] + [(e ...) #`(combine-frees (list (#,f e) ...))]))]) + (quasisyntax/loc stx + (define (*maker . flds) + (define v (**maker . flds)) + #;(printf "~a entered in default case~n" '*maker) + (unless-in-table + var-table v + (define fvs #,(combiner #'free-vars* #'flds)) + (define fis #,(combiner #'free-idxs* #'flds)) + (hash-set! var-table v fvs) + (hash-set! index-table v fis)) + v)))])]) + #`(begin + (define-struct (nm parent) flds #:inspector #f) + (define-match-expander ex + (lambda (s) + (... + (syntax-case s () + [(__ . fs) + (with-syntax ([flds** (syntax/loc s (_ . fs))]) + (quasisyntax/loc s (struct nm flds**)))])))) + (begin-for-syntax + (hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx))) + intern + provides + frees)))]))) + (values (mk #'Type #'type-name-ht) (mk #'Effect #'effect-name-ht)))) + diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss new file mode 100644 index 00000000..9ced9791 --- /dev/null +++ b/collects/typed-scheme/rep/type-rep.ss @@ -0,0 +1,577 @@ +#lang scheme/base +(require "../utils/utils.ss") + +(require (utils planet-requires tc-utils) + "rep-utils.ss" "effect-rep.ss" "free-variance.ss" + mzlib/trace scheme/match + (for-syntax scheme/base)) + +(define name-table (make-weak-hasheq)) + +;; Name = Symbol + +;; Type is defined in rep-utils.ss + +;; t must be a Type +(dt Scope (t)) + +;; i is an nat +(dt B (i) + [#:frees empty-hash-table (make-immutable-hasheq (list (cons i Covariant)))] + [#:fold-rhs #:base]) + +;; n is a Name +(dt F (n) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base]) + +;; id is an Identifier +(dt Name (id) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base]) + +;; rator is a type +;; rands is a list of types +;; stx is the syntax of the pair of parens +(dt App (rator rands stx) + [#:intern (list rator rands)] + [#:frees (combine-frees (map free-vars* (cons rator rands))) + (combine-frees (map free-idxs* (cons rator rands)))] + [#:fold-rhs (*App (type-rec-id rator) + (map type-rec-id rands) + stx)]) + +;; left and right are Types +(dt Pair (left right)) + +;; elem is a Type +(dt Vector (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]) + +;; elem is a Type +(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]) + +;; name is a Symbol (not a Name) +(dt Base (name) [#:frees #f] [#:fold-rhs #:base]) + +;; body is a Scope +(dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))] + [#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))]) + +;; n is how many variables are bound here +;; body is a Scope +(dt Poly (n body) #:no-provide + [#:frees (free-vars* body) (without-below n (free-idxs* body))] + [#:fold-rhs (let ([body* (remove-scopes n body)]) + (*Poly n (add-scopes n (type-rec-id body*))))]) + +;; n is how many variables are bound here +;; there are n-1 'normal' vars and 1 ... var +;; body is a Scope +(dt PolyDots (n body) #:no-provide + [#:frees (free-vars* body) (without-below n (free-idxs* body))] + [#:fold-rhs (let ([body* (remove-scopes n body)]) + (*PolyDots n (add-scopes n (type-rec-id body*))))]) + +;; pred : identifier +;; cert : syntax certifier +(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base]) + +;; name : symbol +;; parent : Struct +;; flds : Listof[Type] +;; proc : Function Type +;; poly? : is this a polymorphic type? +;; pred-id : identifier for the predicate of the struct +;; cert : syntax certifier for pred-id +(dt Struct (name parent flds proc poly? pred-id cert) + [#:intern (list name parent flds proc)] + [#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds))) + (combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) flds)))] + [#:fold-rhs (*Struct name + (and parent (type-rec-id parent)) + (map type-rec-id flds) + (and proc (type-rec-id proc)) + poly? + pred-id + cert)]) + +;; kw : keyword? +;; ty : Type +;; required? : Boolean +(dt Keyword (kw ty required?) + [#:frees (free-vars* ty) + (free-idxs* ty)] + [#:fold-rhs (*Keyword kw (type-rec-id ty))]) + +;; dom : Listof[Type] +;; rng : Type +;; rest : Option[Type] +;; drest : Option[Cons[Type,Name or nat]] +;; kws : Listof[Keyword] +;; rest and drest NOT both true +;; thn-eff : Effect +;; els-eff : Effect +;; arr is NOT a Type +(dt arr (dom rng rest drest kws thn-eff els-eff) + [#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null) + (map Keyword-ty kws) + dom))) + (match drest + [(cons t (? symbol? bnd)) + (list (fix-bound (flip-variances (free-vars* t)) bnd))] + [(cons t bnd) (list (flip-variances (free-vars* t)))] + [_ null]) + (list (free-vars* rng)) + (map make-invariant + (map free-vars* (append thn-eff els-eff))))) + (combine-frees (append (map flip-variances (map free-idxs* (append (if rest (list rest) null) + (map Keyword-ty kws) + dom))) + (match drest + [(cons t (? number? bnd)) + (list (fix-bound (flip-variances (free-idxs* t)) bnd))] + [(cons t bnd) (list (flip-variances (free-idxs* t)))] + [_ null]) + (list (free-idxs* rng)) + (map make-invariant + (map free-idxs* (append thn-eff els-eff)))))] + [#:fold-rhs (*arr (map type-rec-id dom) + (type-rec-id rng) + (and rest (type-rec-id rest)) + (and drest (cons (type-rec-id (car drest)) (cdr drest))) + (for/list ([kw kws]) + (cons (Keyword-kw kw) (type-rec-id (Keyword-ty kw)) (Keyword-require? kw))) + (map effect-rec-id thn-eff) + (map effect-rec-id els-eff))]) + +;; top-arr is the supertype of all function types +(dt top-arr () + [#:frees #f] [#:fold-rhs #:base]) + +;; arities : Listof[arr] +(dt Function (arities) [#:frees (combine-frees (map free-vars* arities)) + (combine-frees (map free-idxs* arities))] + [#:fold-rhs (*Function (map type-rec-id arities))]) + +;; v : Scheme Value +(dt Value (v) [#:frees #f] [#:fold-rhs #:base]) + +;; elems : Listof[Type] +(dt Union (elems) [#:frees (combine-frees (map free-vars* elems)) + (combine-frees (map free-idxs* elems))] + [#:fold-rhs ((unbox union-maker) (map type-rec-id elems))]) + +(dt Univ () [#:frees #f] [#:fold-rhs #:base]) + +;; types : Listof[Type] +(dt Values (types) + #:no-provide + [#:frees (combine-frees (map free-vars* types)) + (combine-frees (map free-idxs* types))] + [#:fold-rhs (*Values (map type-rec-id types))]) + +(dt ValuesDots (types dty dbound) + [#:frees (combine-frees (map free-vars* (cons dty types))) + (combine-frees (map free-idxs* (cons dty types)))] + [#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)]) + +;; in : Type +;; out : Type +(dt Param (in out)) + +;; key : Type +;; value : Type +(dt Hashtable (key value)) + +;; t : Type +(dt Syntax (t)) + +;; pos-flds : (Listof Type) +;; name-flds : (Listof (Tuple Symbol Type Boolean)) +;; methods : (Listof (Tuple Symbol Function)) +(dt Class (pos-flds name-flds methods) + [#:frees (combine-frees + (map free-vars* (append pos-flds + (map cadr name-flds) + (map cadr methods)))) + (combine-frees + (map free-idxs* (append pos-flds + (map cadr name-flds) + (map cadr methods))))] + + [#:fold-rhs (match (list pos-flds name-flds methods) + [(list + pos-tys + (list (list init-names init-tys) ___) + (list (list mname mty) ___)) + (*Class + (map type-rec-id pos-tys) + (map list + init-names + (map type-rec-id init-tys)) + (map list mname (map type-rec-id mty)))])]) + +;; cls : Class +(dt Instance (cls)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Ugly hack - should use units + +(define union-maker (box #f)) + +(define (set-union-maker! v) (set-box! union-maker v)) + +(provide set-union-maker!) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; remove-dups: List[Type] -> List[Type] +;; removes duplicate types from a SORTED list +(define (remove-dups types) + (cond [(null? types) types] + [(null? (cdr types)) types] + [(type-equal? (car types) (cadr types)) (remove-dups (cdr types))] + [else (cons (car types) (remove-dups (cdr types)))])) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; type/effect fold + +(define-syntaxes (type-case effect-case) + (let () + (define (mk ht) + (lambda (stx) + (let ([ht (hash-copy ht)]) + (define (mk-matcher kw) + (datum->syntax stx (string->symbol (string-append (keyword->string kw) ":")))) + (define (add-clause cl) + (syntax-case cl () + [(kw #:matcher mtch pats ... expr) + (hash-set! ht (syntax-e #'kw) (list #'mtch + (syntax/loc cl (pats ...)) + (lambda (tr er) #'expr) + cl))] + [(kw pats ... expr) + (hash-set! ht (syntax-e #'kw) (list (mk-matcher (syntax-e #'kw)) + (syntax/loc cl (pats ...)) + (lambda (tr er) #'expr) + cl))])) + (define rid #'type-rec-id) + (define erid #'effect-rec-id) + (define (gen-clause k v) + (define match-ex (car v)) + (define pats (cadr v)) + (define body-f (caddr v)) + (define src (cadddr v)) + (define pat (quasisyntax/loc src (#,match-ex . #,pats))) + (define cl (quasisyntax/loc src (#,pat #,(body-f rid erid)))) + cl) + (syntax-case stx () + [(tc rec-id ty clauses ...) + (syntax-case #'(clauses ...) () + [([kw pats ... es] ...) #t] + [_ #f]) + (syntax/loc stx (tc rec-id (lambda (e) (sub-eff rec-id e)) ty clauses ...))] + [(tc rec-id e-rec-id ty clauses ...) + (begin + (map add-clause (syntax->list #'(clauses ...))) + (with-syntax ([old-rec-id type-rec-id]) + #`(let ([#,rid rec-id] + [#,erid e-rec-id] + [#,fold-target ty]) + ;; then generate the fold + #,(quasisyntax/loc stx + (match #,fold-target + #,@(hash-map ht gen-clause))))))])))) + (values (mk type-name-ht) (mk effect-name-ht)))) + +(provide type-case effect-case) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;; sub-eff : (Type -> Type) Eff -> Eff +(define (sub-eff sb eff) + (effect-case sb eff)) + +(define (add-scopes n t) + (if (zero? n) t + (add-scopes (sub1 n) (*Scope t)))) + +(define (remove-scopes n sc) + (if (zero? n) + sc + (match sc + [(Scope: sc*) (remove-scopes (sub1 n) sc*)] + [_ (int-err "Tried to remove too many scopes: ~a" sc)]))) + +;; abstract-many : Names Type -> Scope^n +;; where n is the length of names +(define (abstract-many names ty) + (define (nameTo name count type) + (let loop ([outer 0] [ty type]) + (define (sb t) (loop outer t)) + (type-case + sb ty + [#:F name* (if (eq? name name*) (*B (+ count outer)) ty)] + ;; necessary to avoid infinite loops + [#:Union elems (*Union (remove-dups (sort (map sb elems) type Type +;; where n is the length of types +;; all of the types MUST be Fs +(define (instantiate-many images sc) + (define (replace image count type) + (let loop ([outer 0] [ty type]) + (define (sb t) (loop outer t)) + (type-case + sb ty + [#:B idx (if (= (+ count outer) idx) + image + ty)] + ;; necessary to avoid infinite loops + [#:Union elems (*Union (remove-dups (sort (map sb elems) type void +(define (check-subforms/with-handlers form) + (define handler-tys '()) + (define body-ty #f) + (define (get-result-ty t) + (match t + [(Function: (list (arr: _ rngs #f _ '() _ _) ...)) (apply Un rngs)] + [_ (tc-error "Internal error in get-result-ty: not a function type: ~n~a" t)])) + (let loop ([form form]) + (parameterize ([current-orig-stx form]) + (kernel-syntax-case* form #f (#%app) + [stx + ;; if this needs to be checked + (syntax-property form 'typechecker:with-type) + ;; the form should be already ascribed the relevant type + (void + (tc-expr form))] + [stx + ;; this is a hander function + (syntax-property form 'typechecker:exn-handler) + (let ([t (tc-expr/t form)]) + (unless (subtype t (-> (Un) Univ)) + (tc-error "Exception handler must be a single-argument function, got ~n~a")) + (set! handler-tys (cons (get-result-ty t) handler-tys)))] + [stx + ;; this is the body of the with-handlers + (syntax-property form 'typechecker:exn-body) + (let ([t (tc-expr/t form)]) + (set! body-ty t))] + [(a . b) + (begin + (loop #'a) + (loop #'b))] + [_ (void)]))) + (ret (apply Un body-ty handler-tys))) + +(define (check-subforms/with-handlers/check form expected) + (let loop ([form form]) + (parameterize ([current-orig-stx form]) + (kernel-syntax-case* form #f () + [stx + ;; if this needs to be checked + (syntax-property form 'typechecker:with-type) + ;; the form should be already ascribed the relevant type + (tc-expr form)] + [stx + ;; this is a hander function + (syntax-property form 'typechecker:exn-handler) + (tc-expr/check form (-> (Un) expected))] + [stx + ;; this is the body of the with-handlers + (syntax-property form 'typechecker:exn-body) + (tc-expr/check form expected)] + [(a . b) + (begin + (loop #'a) + (loop #'b))] + [_ (void)]))) + (ret expected)) + +;; typecheck the expansion of a with-handlers form +;; syntax -> type +(define (check-subforms/ignore form) + (let loop ([form form]) + (kernel-syntax-case* form #f () + [stx + ;; if this needs to be checked + (syntax-property form 'typechecker:with-type) + ;; the form should be already ascribed the relevant type + (tc-expr form)] + [(a . b) + (loop #'a) + (loop #'b)] + [_ (void)]))) diff --git a/collects/typed-scheme/typecheck/def-binding.ss b/collects/typed-scheme/typecheck/def-binding.ss new file mode 100644 index 00000000..0b383b22 --- /dev/null +++ b/collects/typed-scheme/typecheck/def-binding.ss @@ -0,0 +1,11 @@ +#lang scheme/base + +(require scheme/contract) + +(define-struct binding (name) #:transparent) +(define-struct (def-binding binding) (ty) #:transparent) +(define-struct (def-stx-binding binding) () #:transparent) + +(provide/contract (struct binding ([name identifier?])) + (struct (def-binding binding) ([name identifier?] [ty any/c])) + (struct (def-stx-binding binding) ([name identifier?]))) diff --git a/collects/typed-scheme/typecheck/internal-forms.ss b/collects/typed-scheme/typecheck/internal-forms.ss new file mode 100644 index 00000000..b85dd96c --- /dev/null +++ b/collects/typed-scheme/typecheck/internal-forms.ss @@ -0,0 +1,14 @@ +#lang scheme/base + +(require (for-syntax scheme/base)) + +(define-syntax-rule (internal-forms nms ...) + (begin + (provide nms ...) + (define-syntax (nms stx) (raise-syntax-error 'typecheck "Internal typechecker form used out of context" stx)) ...)) + +(internal-forms require/typed-internal define-type-alias-internal + define-typed-struct-internal + define-typed-struct/exec-internal + assert-predicate-internal + :-internal) diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss new file mode 100644 index 00000000..4ca36a34 --- /dev/null +++ b/collects/typed-scheme/typecheck/provide-handling.ss @@ -0,0 +1,90 @@ +#lang scheme/base + +(require (except-in "../utils/utils.ss" extend)) +(require (only-in srfi/1/list s:member) + syntax/kerncase + mzlib/trace + (private type-contract) + (rep type-rep) + (utils tc-utils) + "def-binding.ss") + +(require (for-template scheme/base + scheme/contract)) + +(provide remove-provides provide? generate-prov) + +(define (provide? form) + (kernel-syntax-case form #f + [(#%provide . rest) form] + [_ #f])) + + +(define (remove-provides forms) + (filter (lambda (e) (not (provide? e))) (syntax->list forms))) + +(define ((generate-prov stx-defs val-defs) form) + (define (mem? i vd) + (cond [(s:member i vd (lambda (i j) (free-identifier=? i (binding-name j)))) => car] + [else #f])) + (define (lookup-id i vd) + (def-binding-ty (mem? i vd))) + (define (mk internal-id external-id) + (cond + [(mem? internal-id val-defs) + => + (lambda (b) + (with-syntax ([id internal-id] + [out-id external-id]) + (cond [(type->contract (def-binding-ty b) (lambda () #f)) + => + (lambda (cnt) + (with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))]) + #`(begin + (define/contract cnt-id #,cnt id) + (define-syntax export-id + (if (unbox typed-context?) + (make-rename-transformer #'id) + (make-rename-transformer #'cnt-id))) + (#%provide (rename export-id out-id)))))] + [else + (with-syntax ([(export-id) (generate-temporaries #'(id))]) + #`(begin + (define-syntax export-id + (if (unbox typed-context?) + (make-rename-transformer #'id) + (lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id))))) + (provide (rename-out [export-id out-id]))))])))] + [(mem? internal-id stx-defs) + => + (lambda (b) + (with-syntax ([id internal-id] + [out-id external-id]) + (with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))]) + #`(begin + (define-syntax export-id + (if (unbox typed-context?) + (make-rename-transformer #'id) + (lambda (stx) + (tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id))))) + (provide (rename-out [export-id out-id]))))))] + [(eq? (syntax-e internal-id) (syntax-e external-id)) + #`(provide #,internal-id)] + [else #`(provide (rename-out [#,internal-id #,external-id]))])) + (kernel-syntax-case form #f + [(#%provide form ...) + (map + (lambda (f) + (parameterize ([current-orig-stx f]) + (syntax-case* f (struct rename all-defined protect all-defined-except all-from all-from-except) + (lambda (a b) (eq? (syntax-e a) (syntax-e b))) + [id + (identifier? #'id) + (mk #'id #'id)] + [(rename in out) + (mk #'in #'out)] + [(protect . _) + (tc-error "provide: protect not supported by Typed Scheme")] + [_ (int-err "unknown provide form")]))) + (syntax->list #'(form ...)))] + [_ (int-err "non-provide form! ~a" (syntax->datum form))])) diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss new file mode 100644 index 00000000..572becfd --- /dev/null +++ b/collects/typed-scheme/typecheck/signatures.ss @@ -0,0 +1,28 @@ +#lang scheme/base +(require scheme/unit) +(provide (all-defined-out)) + +(define-signature typechecker^ + (type-check tc-toplevel-form)) + +(define-signature tc-expr^ + (tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t)) + +(define-signature check-subforms^ + (check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check)) + +(define-signature tc-if^ + (tc/if-onearm tc/if-twoarm tc/if-onearm/check tc/if-twoarm/check)) + +(define-signature tc-lambda^ + (tc/lambda tc/lambda/check tc/rec-lambda/check)) + +(define-signature tc-app^ + (tc/app tc/app/check tc/funapp)) + +(define-signature tc-let^ + (tc/let-values tc/letrec-values tc/let-values/check tc/letrec-values/check)) + +(define-signature tc-dots^ + (tc/dots)) + diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss new file mode 100644 index 00000000..3c04db14 --- /dev/null +++ b/collects/typed-scheme/typecheck/tc-app-unit.ss @@ -0,0 +1,734 @@ +#lang scheme/unit + +(require (only-in "../utils/utils.ss" debug in-syntax printf/log in-pairs rep utils private env [infer r:infer])) +(require "signatures.ss" + (rep type-rep effect-rep) + (utils tc-utils) + (private subtype type-utils union type-effect-convenience type-effect-printer resolve-type + type-annotation) + (r:infer infer) + (env type-environments) + (only-in srfi/1 alist-delete) + (only-in scheme/private/class-internal make-object do-make-object) + mzlib/trace mzlib/pretty syntax/kerncase scheme/match + (for-syntax scheme/base) + (for-template + "internal-forms.ss" scheme/base + (only-in scheme/private/class-internal make-object do-make-object))) +(require (r:infer constraint-structs)) + +(import tc-expr^ tc-lambda^ tc-dots^) +(export tc-app^) + +;; comparators that inform the type system +(define (comparator? i) + (or (free-identifier=? i #'eq?) + (free-identifier=? i #'equal?) + (free-identifier=? i #'eqv?) + (free-identifier=? i #'=) + (free-identifier=? i #'string=?))) + +;; typecheck eq? applications +;; identifier identifier expression expression expression +;; identifier expr expr expr expr -> tc-result +(define (tc/eq comparator v1 v2) + (define (e? i) (free-identifier=? i comparator)) + (define (do id val) + (define-syntax alt (syntax-rules () [(_ nm pred ...) + (and (e? #'nm) (or (pred val) ...))])) + (if (or (alt symbol=? symbol?) + (alt string=? string?) + (alt = number?) + (alt eq? boolean? keyword? symbol?) + (alt eqv? boolean? keyword? symbol? number?) + (alt equal? (lambda (x) #t))) + (values (list (make-Restrict-Effect (-val val) id)) + (list (make-Remove-Effect (-val val) id))) + (values (list) (list)))) + (match (list (tc-expr v1) (tc-expr v2)) + [(list (tc-result: id-t (list (Var-True-Effect: id1)) (list (Var-False-Effect: id2))) (tc-result: (Value: val))) + (do id1 val)] + [(list (tc-result: (Value: val)) (tc-result: id-t (list (Var-True-Effect: id1)) (list (Var-False-Effect: id2)))) + (do id1 val)] + [_ (values (list) (list))])) + + +;; typecheck an application: +;; arg-types: the types of the actual parameters +;; arg-effs: the effects of the arguments +;; dom-types: the types of the function's fixed arguments +;; rest-type: the type of the functions's rest parameter, or #f +;; latent-eff: the latent effect of the function +;; arg-stxs: the syntax for each actual parameter, for error reporting +;; [Type] [Type] Maybe[Type] [Syntax] -> (values Listof[Effect] Listof[Effect]) +(define (tc-args arg-types arg-thn-effs arg-els-effs dom-types rest-type latent-thn-eff latent-els-eff arg-stxs) + (define (var-true-effect-v e) (match e + [(Var-True-Effect: v) v])) + (define (var-false-effect-v e) (match e + [(Var-False-Effect: v) v])) + ;; special case for predicates: + (if (and (not (null? latent-thn-eff)) + (not (null? latent-els-eff)) + (not rest-type) + ;(printf "got to =~n") + (= (length arg-types) (length dom-types) 1) + ;(printf "got to var preds~n") + (= (length (car arg-thn-effs)) (length (car arg-els-effs)) 1) + (Var-True-Effect? (caar arg-thn-effs)) ;; thn-effs is a list for each arg + (Var-False-Effect? (caar arg-els-effs)) ;; same with els-effs + (free-identifier=? (var-true-effect-v (caar arg-thn-effs)) + (var-false-effect-v (caar arg-els-effs))) + (subtype (car arg-types) (car dom-types))) + ;; then this was a predicate application, so we construct the appropriate type effect + (values (map (add-var (var-true-effect-v (caar arg-thn-effs))) latent-thn-eff) + (map (add-var (var-true-effect-v (caar arg-thn-effs))) latent-els-eff)) + ;; otherwise, we just ignore the effects. + (let loop ([args arg-types] [doms dom-types] [stxs arg-stxs] [arg-count 1]) + (cond + [(and (null? args) (null? doms)) (values null null)] ;; here, we just return the empty effect + [(null? args) + (tc-error/delayed + "Insufficient arguments to function application, expected ~a, got ~a" + (length dom-types) (length arg-types)) + (values null null)] + [(and (null? doms) rest-type) + (if (subtype (car args) rest-type) + (loop (cdr args) doms (cdr stxs) (add1 arg-count)) + (begin + (tc-error/delayed #:stx (car stxs) + "Rest argument had wrong type, expected: ~a and got: ~a" + rest-type (car args)) + (values null null)))] + [(null? doms) + (tc-error/delayed "Too many arguments to function, expected ~a, got ~a" (length dom-types) (length arg-types)) + (values null null)] + [(subtype (car args) (car doms)) + (loop (cdr args) (cdr doms) (cdr stxs) (add1 arg-count))] + [else + (tc-error/delayed + #:stx (car stxs) + "Wrong function argument type, expected ~a, got ~a for argument ~a" + (car doms) (car args) arg-count) + (loop (cdr args) (cdr doms) (cdr stxs) (add1 arg-count))])))) + + +;(trace tc-args) + +(define (stringify-domain dom rst drst) + (let ([doms-string (if (null? dom) "" (string-append (stringify dom) " "))]) + (cond [drst + (format "~a~a ... ~a" doms-string (car drst) (cdr drst))] + [rst + (format "~a~a *" doms-string rst)] + [else (stringify dom)]))) + +(define (domain-mismatches ty doms rests drests arg-tys tail-ty tail-bound) + (cond + [(null? doms) + (int-err "How could doms be null: ~a ~a" ty)] + [(= 1 (length doms)) + (format "Domain: ~a~nArguments: ~a~n" + (stringify-domain (car doms) (car rests) (car drests)) + (stringify-domain arg-tys (if (not tail-bound) tail-ty #f) (if tail-bound (cons tail-ty tail-bound) #f)))] + [else + (format "Domains: ~a~nArguments: ~a~n" + (stringify (map stringify-domain doms rests drests) "~n\t") + (stringify-domain arg-tys (if (not tail-bound) tail-ty #f) (if tail-bound (cons tail-ty tail-bound) #f)))])) + +(define (do-apply-log subst fun arg) + (match* (fun arg) + [('star 'list) (printf/log "Polymorphic apply called with uniform rest arg, list argument\n")] + [('star 'dots) (printf/log "Polymorphic apply called with uniform rest arg, dotted argument\n")] + [('dots 'dots) (printf/log "Polymorphic apply called with non-uniform rest arg, dotted argument\n")]) + (log-result subst)) + +(define (tc/apply f args) + (define f-ty (tc-expr f)) + ;; produces the first n-1 elements of the list, and the last element + (define (split l) + (let loop ([l l] [acc '()]) + (if (null? (cdr l)) + (values (reverse acc) (car l)) + (loop (cdr l) (cons (car l) acc))))) + (define-values (fixed-args tail) (split (syntax->list args))) + + (match f-ty + [(tc-result: (Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ...))) + (when (null? doms) + (tc-error/expr #:return (ret (Un)) + "empty case-lambda given as argument to apply")) + (let ([arg-tys (map tc-expr/t fixed-args)]) + (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) + (cond [(null? doms*) + (let-values ([(tail-ty tail-bound) + (with-handlers ([exn:fail? (lambda _ (values (tc-expr/t tail) #f))]) + (tc/dots tail))]) + (tc-error/expr #:return (ret (Un)) + (string-append + "Bad arguments to function in apply:~n" + (domain-mismatches f-ty doms rests drests arg-tys tail-ty tail-bound))))] + [(and (car rests*) + (let-values ([(tail-ty tail-bound) + (with-handlers ([exn:fail? (lambda _ (values #f #f))]) + (tc/dots tail))]) + (and tail-ty + (subtype (apply -lst* arg-tys #:tail (make-Listof tail-ty)) + (apply -lst* (car doms*) #:tail (make-Listof (car rests*))))))) + (printf/log "Non-poly apply, ... arg\n") + (ret (car rngs*))] + [(and (car rests*) + (let ([tail-ty (with-handlers ([exn:fail? (lambda _ #f)]) + (tc-expr/t tail))]) + (and tail-ty + (subtype (apply -lst* arg-tys #:tail tail-ty) + (apply -lst* (car doms*) #:tail (make-Listof (car rests*))))))) + + (printf/log (if (memq (syntax->datum f) '(+ - * / max min)) + "Simple arithmetic non-poly apply\n" + "Simple non-poly apply\n")) + (ret (car rngs*))] + [(and (car drests*) + (let-values ([(tail-ty tail-bound) + (with-handlers ([exn:fail? (lambda _ (values #f #f))]) + (tc/dots tail))]) + (and tail-ty + (eq? (cdr (car drests*)) tail-bound) + (subtypes arg-tys (car doms*)) + (subtype tail-ty (car (car drests*)))))) + (printf/log "Non-poly apply, ... arg\n") + (ret (car rngs*))] + [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] + [(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ..1)))) + (let*-values ([(arg-tys) (map tc-expr/t fixed-args)] + [(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))]) + (tc/dots tail))]) + #;(for-each (lambda (x) (unless (not (Poly? x)) + (tc-error "Polymorphic argument of type ~a to polymorphic function in apply not allowed" x))) + (cons tail-ty arg-tys)) + (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) + (cond [(null? doms*) + (match f-ty + [(tc-result: (Poly-names: _ (Function: (list (arr: doms rngs rests drests '() _ _) ..1)))) + (tc-error/expr #:return (ret (Un)) + (string-append + "Bad arguments to polymorphic function in apply:~n" + (domain-mismatches f-ty doms rests drests arg-tys tail-ty tail-bound)))])] + ;; the actual work, when we have a * function and a list final argument + [(and (car rests*) + (not tail-bound) + (<= (length (car doms*)) + (length arg-tys)) + (infer/vararg vars + (cons tail-ty arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*) + (fv (car rngs*)))) + => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] + ;; actual work, when we have a * function and ... final arg + [(and (car rests*) + tail-bound + (<= (length (car doms*)) + (length arg-tys)) + (infer/vararg vars + (cons (make-Listof tail-ty) arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*) + (fv (car rngs*)))) + => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] + ;; ... function, ... arg + [(and (car drests*) + tail-bound + (eq? tail-bound (cdr (car drests*))) + (= (length (car doms*)) + (length arg-tys)) + (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))) + => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] + ;; if nothing matches, around the loop again + [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] + [(tc-result: (Poly: vars (Function: '()))) + (tc-error/expr #:return (ret (Un)) + "Function has no cases")] + [(tc-result: (PolyDots: (and vars (list fixed-vars ... dotted-var)) + (Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ..1)))) + (let*-values ([(arg-tys) (map tc-expr/t fixed-args)] + [(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))]) + (tc/dots tail))]) + (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) + (cond [(null? doms*) + (match f-ty + [(tc-result: (PolyDots-names: _ (Function: (list (arr: doms rngs rests drests '() _ _) ..1)))) + (tc-error/expr #:return (ret (Un)) + (string-append + "Bad arguments to polymorphic function in apply:~n" + (domain-mismatches f-ty doms rests drests arg-tys tail-ty tail-bound)))])] + ;; the actual work, when we have a * function and a list final argument + [(and (car rests*) + (not tail-bound) + (<= (length (car doms*)) + (length arg-tys)) + (infer/vararg vars + (cons tail-ty arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*) + (fv (car rngs*)))) + => (lambda (substitution) + (do-apply-log substitution 'star 'list) + (ret (subst-all substitution (car rngs*))))] + ;; actual work, when we have a * function and ... final arg + [(and (car rests*) + tail-bound + (<= (length (car doms*)) + (length arg-tys)) + (infer/vararg vars + (cons (make-Listof tail-ty) arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*) + (fv (car rngs*)))) + => (lambda (substitution) + (do-apply-log substitution 'star 'dots) + (ret (subst-all substitution (car rngs*))))] + ;; ... function, ... arg, same bound on ... + [(and (car drests*) + tail-bound + (eq? tail-bound (cdr (car drests*))) + (= (length (car doms*)) + (length arg-tys)) + (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))) + => (lambda (substitution) + (do-apply-log substitution 'dots 'dots) + (ret (subst-all substitution (car rngs*))))] + ;; ... function, ... arg, different bound on ... + [(and (car drests*) + tail-bound + (not (eq? tail-bound (cdr (car drests*)))) + (= (length (car doms*)) + (length arg-tys)) + (parameterize ([current-tvars (extend-env (list tail-bound (cdr (car drests*))) + (list (make-DottedBoth (make-F tail-bound)) + (make-DottedBoth (make-F (cdr (car drests*))))) + (current-tvars))]) + (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))) + => (lambda (substitution) + (define drest-bound (cdr (car drests*))) + (do-apply-log substitution 'dots 'dots) + (ret (substitute-dotted (cadr (assq drest-bound substitution)) + tail-bound + drest-bound + (subst-all (alist-delete drest-bound substitution eq?) + (car rngs*)))))] + ;; if nothing matches, around the loop again + [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] + [(tc-result: (PolyDots: vars (Function: '()))) + (tc-error/expr #:return (ret (Un)) + "Function has no cases")] + [(tc-result: f-ty) (tc-error/expr #:return (ret (Un)) + "Type of argument to apply is not a function type: ~n~a" f-ty)])) + + + +(define (log-result subst) + (define (dmap-length d) + (match d + [(struct dcon (fixed rest)) (length fixed)] + [(struct dcon-exact (fixed rest)) (length fixed)])) + (define (dmap-rest? d) + (match d + [(struct dcon (fixed rest)) rest] + [(struct dcon-exact (fixed rest)) rest])) + (if (list? subst) + (for ([s subst]) + (match s + [(list v (list imgs ...) starred) + (printf/log "Instantiated ... variable ~a with ~a types\n" v (length imgs))] + [_ (void)])) + (for* ([(cmap dmap) (in-pairs (cset-maps subst))] + [(k v) (dmap-map dmap)]) + (printf/log "Instantiated ... variable ~a with ~a types~a\n" k (dmap-length v) + (if (dmap-rest? v) + " and a starred type" + ""))))) + +(define-syntax (handle-clauses stx) + (syntax-case stx () + [(_ (lsts ... rngs) f-stx pred infer t argtypes expected) + (with-syntax ([(vars ... rng) (generate-temporaries #'(lsts ... rngs))]) + (syntax/loc stx + (or (for/or ([vars lsts] ... [rng rngs] + #:when (pred vars ... rng)) + (let ([substitution (infer vars ... rng)]) + (and substitution + (log-result substitution) + (or expected + (ret (subst-all substitution rng)))))) + (poly-fail t argtypes #:name (and (identifier? f-stx) f-stx)))))])) + +(define (poly-fail t argtypes #:name [name #f]) + (match t + [(or (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '() _ _) ...))) + (PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '() _ _) ...)))) + (let ([fcn-string (if name + (format "function ~a (over ~~a)" (syntax->datum name)) + "function over ~a")]) + (if (and (andmap null? msg-doms) + (null? argtypes)) + (tc-error/expr #:return (ret (Un)) + (string-append + "Could not infer types for applying polymorphic " + fcn-string + "\n") + (stringify msg-vars)) + (tc-error/expr #:return (ret (Un)) + (string-append + "Polymorphic " fcn-string " could not be applied to arguments:~n" + (domain-mismatches t msg-doms msg-rests msg-drests argtypes #f #f)) + (stringify msg-vars))))])) + + +(define (tc/funapp f-stx args-stx ftype0 argtys expected) + (match-let* ([(list (tc-result: argtypes arg-thn-effs arg-els-effs) ...) argtys]) + (let outer-loop ([ftype ftype0] + [argtypes argtypes] + [arg-thn-effs arg-thn-effs] + [arg-els-effs arg-els-effs] + [args args-stx]) + (match ftype + ;; procedural structs + [(tc-result: (and sty (Struct: _ _ _ (? Type? proc-ty) _ _ _)) thn-eff els-eff) + (outer-loop (ret proc-ty thn-eff els-eff) + (cons (tc-result-t ftype0) argtypes) + (cons (list) arg-thn-effs) + (cons (list) arg-els-effs) + #`(#,(syntax/loc f-stx dummy) #,@args))] + ;; mu types, etc + [(tc-result: (? needs-resolving? t) thn-eff els-eff) + (outer-loop (ret (resolve-once t) thn-eff els-eff) argtypes arg-thn-effs arg-els-effs args)] + ;; parameters + [(tc-result: (Param: in out)) + (match argtypes + [(list) (ret out)] + [(list t) + (if (subtype t in) + (ret -Void) + (tc-error/expr #:return (ret (Un)) + "Wrong argument to parameter - expected ~a and got ~a" in t))] + [_ (tc-error/expr #:return (ret (Un)) + "Wrong number of arguments to parameter - expected 0 or 1, got ~a" + (length argtypes))])] + ;; single clause functions + ;; FIXME - error on non-optional keywords + [(tc-result: (and t (Function: (list (arr: dom rng rest #f _ latent-thn-effs latent-els-effs)))) + thn-eff els-eff) + (let-values ([(thn-eff els-eff) + (tc-args argtypes arg-thn-effs arg-els-effs dom rest + latent-thn-effs latent-els-effs + (syntax->list args))]) + (ret rng thn-eff els-eff))] + ;; non-polymorphic case-lambda functions + [(tc-result: (and t (Function: (list (arr: doms rngs rests (and drests #f) '() latent-thn-effs latent-els-effs) ..1))) + thn-eff els-eff) + (let loop ([doms* doms] [rngs rngs] [rests* rests]) + (cond [(null? doms*) + (tc-error/expr + #:return (ret (Un)) + (string-append "No function domains matched in function application:\n" + (domain-mismatches t doms rests drests argtypes #f #f)))] + [(subtypes/varargs argtypes (car doms*) (car rests*)) + (when (car rests*) + (printf/log "Simple varargs function application (~a)\n" (syntax->datum f-stx))) + (ret (car rngs))] + [else (loop (cdr doms*) (cdr rngs) (cdr rests*))]))] + ;; simple polymorphic functions, no rest arguments + [(tc-result: (and t + (or (Poly: vars + (Function: (list (arr: doms rngs (and rests #f) (and drests #f) '() thn-effs els-effs) ...))) + (PolyDots: (list vars ... _) + (Function: (list (arr: doms rngs (and rests #f) (and drests #f) '() thn-effs els-effs) ...)))))) + (handle-clauses (doms rngs) f-stx + (lambda (dom _) (= (length dom) (length argtypes))) + (lambda (dom rng) (infer (fv/list (cons rng dom)) argtypes dom rng (fv rng) expected)) + t argtypes expected)] + ;; polymorphic varargs + [(tc-result: (and t + (or (Poly: vars (Function: (list (arr: doms rngs rests (and drests #f) '() thn-effs els-effs) ...))) + ;; we want to infer the dotted-var here as well, and we don't use these separately + ;; so we can just use "vars" instead of (list fixed-vars ... dotted-var) + (PolyDots: vars (Function: (list (arr: doms rngs rests (and drests #f) '() thn-effs els-effs) ...)))))) + (printf/log "Polymorphic varargs function application (~a)\n" (syntax->datum f-stx)) + (handle-clauses (doms rests rngs) f-stx + (lambda (dom rest rng) (<= (length dom) (length argtypes))) + (lambda (dom rest rng) (infer/vararg vars argtypes dom rest rng (fv rng) expected)) + t argtypes expected)] + ;; polymorphic ... type + [(tc-result: (and t (PolyDots: + (and vars (list fixed-vars ... dotted-var)) + (Function: (list (arr: doms rngs (and #f rests) (cons dtys dbounds) '() thn-effs els-effs) ...))))) + (printf/log "Polymorphic ... function application (~a)\n" (syntax->datum f-stx)) + (handle-clauses (doms dtys dbounds rngs) f-stx + (lambda (dom dty dbound rng) (and (<= (length dom) (length argtypes)) + (eq? dotted-var dbound))) + (lambda (dom dty dbound rng) (infer/dots fixed-vars dotted-var argtypes dom dty rng (fv rng) expected)) + t argtypes expected)] + ;; Union of function types works if we can apply all of them + [(tc-result: (Union: (list (and fs (Function: _)) ...)) e1 e2) + (match-let ([(list (tc-result: ts) ...) (map (lambda (f) (outer-loop + (ret f e1 e2) argtypes arg-thn-effs arg-els-effs args)) fs)]) + (ret (apply Un ts)))] + [(tc-result: f-ty _ _) (tc-error/expr #:return (ret (Un)) + "Cannot apply expression of type ~a, since it is not a function type" f-ty)])))) + +;(trace tc/funapp) + +(define (tc/app form) (tc/app/internal form #f)) + +(define (tc/app/check form expected) + (define t (tc/app/internal form expected)) + (check-below t expected) + (ret expected)) + +;; expr id -> type or #f +;; if there is a binding in stx of the form: +;; (let ([x (reverse name)]) e) +;; where x has a type annotation, return that annotation, otherwise #f +(define (find-annotation stx name) + (define (find s) (find-annotation s name)) + (define (match? b) + (kernel-syntax-case* b #f (reverse) + [[(v) (#%plain-app reverse n)] + (free-identifier=? name #'n) + (begin ;(printf "found annotation: ~a ~a~n~a~n" (syntax-e name) (syntax-e #'v) (type-annotation #'v)) + (type-annotation #'v))] + [_ #f])) + (kernel-syntax-case* + stx #f (reverse letrec-syntaxes+values) + [(let-values (binding ...) body) + (cond [(ormap match? (syntax->list #'(binding ...)))] + [else (find #'body)])] + [(#%plain-app e ...) (ormap find (syntax->list #'(e ...)))] + [(if e1 e2 e3) (ormap find (syntax->list #'(e1 e2 e3)))] + [(letrec-values ([(v ...) e] ...) b) + (ormap find (syntax->list #'(e ... b)))] + [(letrec-syntaxes+values _ ([(v ...) e] ...) b) + (ormap find (syntax->list #'(e ... b)))] + [(begin . es) + (ormap find (syntax->list #'es))] + [(#%plain-lambda (v ...) e) + (find #'e)] + [_ #f])) + + +(define (check-do-make-object cl pos-args names named-args) + (let* ([names (map syntax-e (syntax->list names))] + [name-assoc (map list names (syntax->list named-args))]) + (let loop ([t (tc-expr cl)]) + (match t + [(tc-result: (? Mu? t)) (loop (ret (unfold t)))] + [(tc-result: (and c (Class: pos-tys (list (and tnflds (list tnames _ _)) ...) _))) + (unless (= (length pos-tys) + (length (syntax->list pos-args))) + (tc-error/delayed "expected ~a positional arguments, but got ~a" + (length pos-tys) (length (syntax->list pos-args)))) + ;; use for, since they might be different lengths in error case + (for ([pa (in-syntax pos-args)] + [pt (in-list pos-tys)]) + (tc-expr/check pa pt)) + (for ([n names] + #:when (not (memq n tnames))) + (tc-error/delayed + "unknown named argument ~a for class~nlegal named arguments are ~a" + n (stringify tnames))) + (for-each (match-lambda + [(list tname tfty opt?) + (let ([s (cond [(assq tname name-assoc) => cadr] + [(not opt?) + (tc-error/delayed "value not provided for named init arg ~a" tname) + #f] + [else #f])]) + (if s + ;; this argument was present + (tc-expr/check s tfty) + ;; this argument wasn't provided, and was optional + #f))]) + tnflds) + (ret (make-Instance c))] + [(tc-result: t) + (tc-error/expr #:return (ret (Un)) "expected a class value for object creation, got: ~a" t)])))) + +(define (tc-keywords form arities kws kw-args pos-args expected) + (match arities + [(list (arr: dom rng rest #f ktys _ _)) + ;; assumes that everything is in sorted order + (let loop ([actual-kws kws] + [actuals (map tc-expr/t (syntax->list kw-args))] + [formals ktys]) + (match* (actual-kws formals) + [('() '()) + (void)] + [(_ '()) + (tc-error/expr #:return (ret (Un)) + "Unexpected keyword argument ~a" (car actual-kws))] + [('() (cons fst rst)) + (match fst + [(Keyword: k _ #t) + (tc-error/expr #:return (ret (Un)) + "Missing keyword argument ~a" k)] + [_ (loop actual-kws actuals rst)])] + [((cons k kws-rest) (cons (Keyword: k* t req?) form-rest)) + (cond [(eq? k k*) ;; we have a match + (unless (subtype (car actuals) t) + (tc-error/delayed + "Wrong function argument type, expected ~a, got ~a for keyword argument ~a" + t (car actuals) k)) + (loop kws-rest (cdr actuals) form-rest)] + [req? ;; this keyword argument was required + (tc-error/delayed "Missing keyword argument ~a" k*) + (loop kws-rest (cdr actuals) form-rest)] + [else ;; otherwise, ignore this formal param, and continue + (loop actual-kws actuals form-rest)])])) + (tc/funapp (car (syntax-e form)) kw-args (ret (make-Function arities)) (map tc-expr (syntax->list pos-args)) expected)] + [_ (int-err "case-lambda w/ keywords not supported")])) + + +(define (type->list t) + (match t + [(Pair: (Value: (? keyword? k)) b) (cons k (type->list b))] + [(Value: '()) null] + [_ (int-err "bad value in type->list: ~a" t)])) + +(define (tc/app/internal form expected) + (kernel-syntax-case* form #f + (values apply not list list* call-with-values do-make-object make-object cons + andmap ormap) ;; the special-cased functions + ;; special cases for classes + [(#%plain-app make-object cl . args) + (check-do-make-object #'cl #'args #'() #'())] + [(#%plain-app do-make-object cl (#%plain-app list . pos-args) (#%plain-app list (#%plain-app cons 'names named-args) ...)) + (check-do-make-object #'cl #'pos-args #'(names ...) #'(named-args ...))] + [(#%plain-app do-make-object . args) + (int-err "bad do-make-object : ~a" (syntax->datum #'args))] + ;; call-with-values + [(#%plain-app call-with-values prod con) + (match-let* ([(tc-result: prod-t) (tc-expr #'prod)]) + (define (values-ty->list t) + (match t + [(Values: ts) ts] + [_ (list t)])) + (match prod-t + [(Function: (list (arr: (list) vals _ #f '() _ _))) + (tc/funapp #'con #'prod (tc-expr #'con) (map ret (values-ty->list vals)) expected)] + [_ (tc-error/expr #:return (ret (Un)) + "First argument to call with values must be a function that can accept no arguments, got: ~a" + prod-t)]))] + ;; special cases for `values' + ;; special case the single-argument version to preserve the effects + [(#%plain-app values arg) (tc-expr #'arg)] + [(#%plain-app values . args) + (let ([tys (map tc-expr/t (syntax->list #'args))]) + (ret (-values tys)))] + ;; special case for `list' + [(#%plain-app list . args) + (let ([tys (map tc-expr/t (syntax->list #'args))]) + (ret (apply -lst* tys)))] + ;; special case for `list*' + [(#%plain-app list* . args) + (match-let* ([(list last tys-r ...) (reverse (map tc-expr/t (syntax->list #'args)))] + [tys (reverse tys-r)]) + (ret (foldr make-Pair last tys)))] + ;; in eq? cases, call tc/eq + [(#%plain-app eq? v1 v2) + (and (identifier? #'eq?) (comparator? #'eq?)) + (begin + ;; make sure the whole expression is type correct + (tc/funapp #'eq? #'(v1 v2) (tc-expr #'eq?) (map tc-expr (syntax->list #'(v1 v2))) expected) + ;; check thn and els with the eq? info + (let-values ([(thn-eff els-eff) (tc/eq #'eq? #'v1 #'v2)]) + (ret B thn-eff els-eff)))] + ;; special case for `not' + [(#%plain-app not arg) + (match (tc-expr #'arg) + ;; if arg was a predicate application, we swap the effects + [(tc-result: t thn-eff els-eff) + (ret B (map var->type-eff els-eff) (map var->type-eff thn-eff))])] + ;; special case for `apply' + [(#%plain-app apply f . args) (tc/apply #'f #'args)] + ;; special case for keywords + [(#%plain-app + (#%plain-app kpe kws num fn) + kw-list + (#%plain-app list . kw-arg-list) + . pos-args) + (eq? (syntax-e #'kpe) 'keyword-procedure-extract) + (match (tc-expr #'fn) + [(tc-result: (Function: arities)) + (tc-keywords form arities (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected)] + [t (tc-error/expr #:return (ret (Un)) + "Cannot apply expression of type ~a, since it is not a function type" t)])] + ;; even more special case for match + [(#%plain-app (letrec-values ([(lp) (#%plain-lambda args . body)]) lp*) . actuals) + (and expected (not (andmap type-annotation (syntax->list #'args))) (free-identifier=? #'lp #'lp*)) + (let-loop-check form #'lp #'actuals #'args #'body expected)] + ;; or/andmap of ... argument + [(#%plain-app or/andmap f arg) + (and + (identifier? #'or/andmap) + (or (free-identifier=? #'or/andmap #'ormap) + (free-identifier=? #'or/andmap #'andmap)) + (with-handlers ([exn:fail? (lambda _ #f)]) + (tc/dots #'arg) + #t)) + (let-values ([(ty bound) (tc/dots #'arg)]) + (parameterize ([current-tvars (extend-env (list bound) + (list (make-DottedBoth (make-F bound))) + (current-tvars))]) + (match-let* ([ft (tc-expr #'f)] + [(tc-result: t) (tc/funapp #'f #'(arg) ft (list (ret ty)) #f)]) + (ret (Un (-val #f) t)))))] + ;; default case + [(#%plain-app f args ...) + (tc/funapp #'f #'(args ...) (tc-expr #'f) (map tc-expr (syntax->list #'(args ...))) expected)])) + +(define (let-loop-check form lp actuals args body expected) + (kernel-syntax-case* #`(#,args #,body #,actuals) #f (null?) + [((val acc ...) + ((if (#%plain-app null? val*) thn els)) + (actual actuals ...)) + (and (free-identifier=? #'val #'val*) + (ormap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a)) + (syntax->list #'(acc ...)))) + (let* ([ts1 (generalize (tc-expr/t #'actual))] + [ann-ts (for/list ([a (in-syntax #'(acc ...))] + [ac (in-syntax #'(actuals ...))]) + (or (find-annotation #'(if (#%plain-app null? val*) thn els) a) + (generalize (tc-expr/t ac))))] + [ts (cons ts1 ann-ts)]) + ;; check that the actual arguments are ok here + (map tc-expr/check (syntax->list #'(actuals ...)) ann-ts) + ;; then check that the function typechecks with the inferred types + (tc/rec-lambda/check form args body lp ts expected) + (ret expected))] + ;; special case when argument needs inference + [_ + (let ([ts (map (compose generalize tc-expr/t) (syntax->list actuals))]) + (tc/rec-lambda/check form args body lp ts expected) + (ret expected))])) + +(define (matches? stx) + (let loop ([stx stx] [ress null] [acc*s null]) + (syntax-case stx (#%plain-app reverse) + [([(res) (#%plain-app reverse acc*)] . more) + (loop #'more (cons #'res ress) (cons #'acc* acc*s))] + [rest + (syntax->list #'rest) + (begin + ;(printf "ress: ~a~n" (map syntax-e ress)) + (list (reverse ress) (reverse acc*s) #'rest))] + [_ #f]))) + +;(trace tc/app/internal) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss new file mode 100644 index 00000000..c61bbd3d --- /dev/null +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -0,0 +1,331 @@ +#lang scheme/unit + + +(require (rename-in "../utils/utils.ss" [private r:private])) +(require syntax/kerncase + scheme/match + "signatures.ss" + (r:private type-utils type-effect-convenience union subtype parse-type type-annotation) + (rep type-rep effect-rep) + (utils tc-utils) + (env lexical-env) + (only-in (env type-environments) lookup current-tvars extend-env) + scheme/private/class-internal + (only-in srfi/1 split-at)) + +(require (for-template scheme/base scheme/private/class-internal)) + +(import tc-if^ tc-lambda^ tc-app^ tc-let^ check-subforms^) +(export tc-expr^) + + +;; return the type of a literal value +;; scheme-value -> type +(define (tc-literal v-stx) + ;; find the meet of the types of a list of expressions + ;; list[syntax] -> type + (define (types-of-literals es) + (apply Un (map tc-literal es))) + (define v (syntax-e v-stx)) + (cond + [(integer? v) -Integer] + [(number? v) N] + [(char? v) -Char] + [(boolean? v) (-val v)] + [(null? v) (-val null)] + [(symbol? v) (-val v)] + [(string? v) -String] + [(keyword? v) (-val v)] + [(bytes? v) -Bytes] + [(list? v) (-Tuple (map tc-literal v))] + [(vector? v) (make-Vector (types-of-literals (vector->list v)))] + [(pregexp? v) -PRegexp] + [(byte-pregexp? v) -Byte-PRegexp] + [(byte-regexp? v) -Byte-Regexp] + [(regexp? v) -Regexp] + [else Univ])) + + +(define (do-inst stx ty) + (define inst (syntax-property stx 'type-inst)) + (define (split-last l) + (let-values ([(all-but last-list) (split-at l (sub1 (length l)))]) + (values all-but (car last-list)))) + (cond [(not inst) ty] + [(not (or (Poly? ty) (PolyDots? ty))) + (tc-error/expr #:return (ret (Un)) "Cannot instantiate non-polymorphic type ~a" ty)] + + [(and (Poly? ty) + (not (= (length (syntax->list inst)) (Poly-n ty)))) + (tc-error/expr #:return (ret (Un)) + "Wrong number of type arguments to polymorphic type ~a:~nexpected: ~a~ngot: ~a" + ty (Poly-n ty) (length (syntax->list inst)))] + [(and (PolyDots? ty) (not (>= (length (syntax->list inst)) (sub1 (PolyDots-n ty))))) + ;; we can provide 0 arguments for the ... var + (tc-error/expr #:return (ret (Un)) + "Wrong number of type arguments to polymorphic type ~a:~nexpected at least: ~a~ngot: ~a" + ty (sub1 (PolyDots-n ty)) (length (syntax->list inst)))] + [(PolyDots? ty) + ;; In this case, we need to check the last thing. If it's a dotted var, then we need to + ;; use instantiate-poly-dotted, otherwise we do the normal thing. + (let-values ([(all-but-last last-stx) (split-last (syntax->list inst))]) + (match (syntax-e last-stx) + [(cons last-ty-stx (? identifier? last-id-stx)) + (unless (Dotted? (lookup (current-tvars) (syntax-e last-id-stx) (lambda _ #f))) + (tc-error/stx last-id-stx "~a is not a type variable bound with ..." (syntax-e last-id-stx))) + (let* ([last-id (syntax-e last-id-stx)] + [last-ty + (parameterize ([current-tvars (extend-env (list last-id) + (list (make-DottedBoth (make-F last-id))) + (current-tvars))]) + (parse-type last-ty-stx))]) + (instantiate-poly-dotted ty (map parse-type all-but-last) last-ty last-id))] + [_ + (instantiate-poly ty (map parse-type (syntax->list inst)))]))] + [else + (instantiate-poly ty (map parse-type (syntax->list inst)))])) + +;; typecheck an identifier +;; the identifier has variable effect +;; tc-id : identifier -> tc-result +(define (tc-id id) + (let* ([ty (lookup-type/lexical id)]) + (ret ty (list (make-Var-True-Effect id)) (list (make-Var-False-Effect id))))) + +;; typecheck an expression, but throw away the effect +;; tc-expr/t : Expr -> Type +(define (tc-expr/t e) (match (tc-expr e) + [(tc-result: t) t] + [t (int-err "tc-expr returned ~a, not a tc-result, for ~a" t (syntax->datum e))])) + +(define (tc-expr/check/t e t) + (match (tc-expr/check e t) + [(tc-result: t) t])) + +;; check-below : (/\ (Result Type -> Result) +;; (Type Type -> Type)) +(define (check-below tr1 expected) + (match (list tr1 expected) + [(list (tc-result: t1 te1 ee1) t2) + (unless (subtype t1 t2) + (tc-error/expr "Expected ~a, but got ~a" t2 t1)) + (ret expected)] + [(list t1 t2) + (unless (subtype t1 t2) + (tc-error/expr"Expected ~a, but got ~a" t2 t1)) + expected])) + +(define (tc-expr/check form expected) + (parameterize ([current-orig-stx form]) + ;(printf "form: ~a~n" (syntax-object->datum form)) + ;; the argument must be syntax + (unless (syntax? form) + (int-err "bad form input to tc-expr: ~a" form)) + (let (;; a local version of ret that does the checking + [ret + (lambda args + (define te (apply ret args)) + (check-below te expected) + (ret expected))]) + (kernel-syntax-case* form #f + (letrec-syntaxes+values find-method/who) ;; letrec-syntaxes+values is not in kernel-syntax-case literals + [stx + (syntax-property form 'typechecker:with-handlers) + (check-subforms/with-handlers/check form expected)] + [stx + (syntax-property form 'typechecker:ignore-some) + (let ([ty (check-subforms/ignore form)]) + (unless ty + (int-err "internal error: ignore-some")) + (check-below ty expected))] + ;; data + [(quote #f) (ret (-val #f) (list (make-False-Effect)) (list (make-False-Effect)))] + [(quote #t) (ret (-val #t) (list (make-True-Effect)) (list (make-True-Effect)))] + [(quote val) (ret (tc-literal #'val))] + ;; syntax + [(quote-syntax datum) (ret Any-Syntax)] + ;; mutation! + [(set! id val) + (match-let* ([(tc-result: id-t) (tc-expr #'id)] + [(tc-result: val-t) (tc-expr #'val)]) + (unless (subtype val-t id-t) + (tc-error/expr "Mutation only allowed with compatible types:~n~a is not a subtype of ~a" val-t id-t)) + (ret -Void))] + ;; top-level variable reference - occurs at top level + [(#%top . id) (check-below (tc-id #'id) expected)] + ;; weird + [(#%variable-reference . _) + (tc-error/expr #:return (ret expected) "#%variable-reference is not supported by Typed Scheme")] + ;; identifiers + [x (identifier? #'x) + (check-below (tc-id #'x) expected)] + ;; w-c-m + [(with-continuation-mark e1 e2 e3) + (begin (tc-expr/check #'e1 Univ) + (tc-expr/check #'e2 Univ) + (tc-expr/check #'e3 expected))] + ;; application + [(#%plain-app . _) (tc/app/check form expected)] + ;; #%expression + [(#%expression e) (tc-expr/check #'e expected)] + ;; syntax + ;; for now, we ignore the rhs of macros + [(letrec-syntaxes+values stxs vals . body) + (tc-expr/check (syntax/loc form (letrec-values vals . body)) expected)] + ;; begin + [(begin e . es) (tc-exprs/check (syntax->list #'(e . es)) expected)] + [(begin0 e . es) + (begin (tc-exprs/check (syntax->list #'es) Univ) + (tc-expr/check #'e expected))] + ;; if + [(if tst body) (tc/if-onearm/check #'tst #'body expected)] + [(if tst thn els) (tc/if-twoarm/check #'tst #'thn #'els expected)] + ;; lambda + [(#%plain-lambda formals . body) + (tc/lambda/check form #'(formals) #'(body) expected)] + [(case-lambda [formals . body] ...) + (tc/lambda/check form #'(formals ...) #'(body ...) expected)] + ;; send + [(let-values (((_) meth)) + (let-values (((_ _) (#%plain-app find-method/who _ rcvr _))) + (#%plain-app _ _ args ...))) + (tc/send #'rcvr #'meth #'(args ...) expected)] + ;; let + [(let-values ([(name ...) expr] ...) . body) + (tc/let-values/check #'((name ...) ...) #'(expr ...) #'body form expected)] + [(letrec-values ([(name ...) expr] ...) . body) + (tc/letrec-values/check #'((name ...) ...) #'(expr ...) #'body form expected)] + ;; other + [_ (tc-error/expr #:return (ret expected) "cannot typecheck unknown form : ~a~n" (syntax->datum form))] + )))) + +;; type check form in the current type environment +;; if there is a type error in form, or if it has the wrong annotation, error +;; otherwise, produce the type of form +;; syntax[expr] -> type +(define (tc-expr form) + ;; do the actual typechecking of form + ;; internal-tc-expr : syntax -> Type + (define (internal-tc-expr form) + (kernel-syntax-case* form #f + (letrec-syntaxes+values #%datum #%app lambda find-method/who) ;; letrec-syntaxes+values is not in kernel-syntax-case literals + ;; + [stx + (syntax-property form 'typechecker:with-handlers) + (let ([ty (check-subforms/with-handlers form)]) + (unless ty + (int-err "internal error: with-handlers")) + ty)] + [stx + (syntax-property form 'typechecker:ignore-some) + (let ([ty (check-subforms/ignore form)]) + (unless ty + (int-err "internal error: ignore-some")) + ty)] + + ;; data + [(quote #f) (ret (-val #f) (list (make-False-Effect)) (list (make-False-Effect)))] + [(quote #t) (ret (-val #t) (list (make-True-Effect)) (list (make-True-Effect)))] + + [(quote val) (ret (tc-literal #'val))] + ;; syntax + [(quote-syntax datum) (ret Any-Syntax)] + ;; w-c-m + [(with-continuation-mark e1 e2 e3) + (begin (tc-expr/check #'e1 Univ) + (tc-expr/check #'e2 Univ) + (tc-expr #'e3))] + ;; lambda + [(#%plain-lambda formals . body) + (tc/lambda form #'(formals) #'(body))] + [(case-lambda [formals . body] ...) + (tc/lambda form #'(formals ...) #'(body ...))] + ;; send + [(let-values (((_) meth)) + (let-values (((_ _) (#%plain-app find-method/who _ rcvr _))) + (#%plain-app _ _ args ...))) + (tc/send #'rcvr #'meth #'(args ...))] + ;; let + [(let-values ([(name ...) expr] ...) . body) + (tc/let-values #'((name ...) ...) #'(expr ...) #'body form)] + [(letrec-values ([(name ...) expr] ...) . body) + (tc/letrec-values #'((name ...) ...) #'(expr ...) #'body form)] + ;; mutation! + [(set! id val) + (match-let* ([(tc-result: id-t) (tc-expr #'id)] + [(tc-result: val-t) (tc-expr #'val)]) + (unless (subtype val-t id-t) + (tc-error/expr "Mutation only allowed with compatible types:~n~a is not a subtype of ~a" val-t id-t)) + (ret -Void))] + ;; top-level variable reference - occurs at top level + [(#%top . id) (tc-id #'id)] + ;; #%expression + [(#%expression e) (tc-expr #'e)] + ;; weird + [(#%variable-reference . _) + (tc-error/expr #:return (ret (Un)) "#%variable-reference is not supported by Typed Scheme")] + ;; identifiers + [x (identifier? #'x) (tc-id #'x)] + ;; application + [(#%plain-app . _) (tc/app form)] + ;; if + [(if tst body) (tc/if-twoarm #'tst #'body #'(#%app void))] + [(if tst thn els) (tc/if-twoarm #'tst #'thn #'els)] + + + + ;; syntax + ;; for now, we ignore the rhs of macros + [(letrec-syntaxes+values stxs vals . body) + (tc-expr (syntax/loc form (letrec-values vals . body)))] + + ;; begin + [(begin e . es) (tc-exprs (syntax->list #'(e . es)))] + [(begin0 e . es) + (begin (tc-exprs (syntax->list #'es)) + (tc-expr #'e))] + ;; other + [_ (tc-error/expr #:return (ret (Un)) "cannot typecheck unknown form : ~a~n" (syntax->datum form))])) + + (parameterize ([current-orig-stx form]) + ;(printf "form: ~a~n" (syntax->datum form)) + ;; the argument must be syntax + (unless (syntax? form) + (int-err "bad form input to tc-expr: ~a" form)) + ;; typecheck form + (let ([ty (cond [(type-ascription form) => (lambda (ann) + (tc-expr/check form ann))] + [else (internal-tc-expr form)])]) + (match ty + [(tc-result: t eff1 eff2) + (let ([ty* (do-inst form t)]) + (ret ty* eff1 eff2))])))) + +(define (tc/send rcvr method args [expected #f]) + (match (tc-expr rcvr) + [(tc-result: (Instance: (and c (Class: _ _ methods)))) + (match (tc-expr method) + [(tc-result: (Value: (? symbol? s))) + (let* ([ftype (cond [(assq s methods) => cadr] + [else (tc-error/expr "send: method ~a not understood by class ~a" s c)])] + [ret-ty (tc/funapp rcvr args (ret ftype) (map tc-expr (syntax->list args)) expected)]) + (if expected + (begin (check-below ret-ty expected) (ret expected)) + ret-ty))] + [(tc-result: t) (int-err "non-symbol methods not supported by Typed Scheme: ~a" t)])] + [(tc-result: t) (tc-error/expr #:return (or expected (Un)) "send: expected a class instance, got ~a" t)])) + +;; type-check a list of exprs, producing the type of the last one. +;; if the list is empty, the type is Void. +;; list[syntax[expr]] -> tc-result +(define (tc-exprs exprs) + (cond [(null? exprs) (ret -Void)] + [(null? (cdr exprs)) (tc-expr (car exprs))] + [else (tc-expr/check (car exprs) Univ) + (tc-exprs (cdr exprs))])) + +(define (tc-exprs/check exprs expected) + (cond [(null? exprs) (check-below (ret -Void) expected)] + [(null? (cdr exprs)) (tc-expr/check (car exprs) expected)] + [else (tc-expr/check (car exprs) Univ) + (tc-exprs/check (cdr exprs) expected)])) diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss new file mode 100644 index 00000000..962c480e --- /dev/null +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss @@ -0,0 +1,294 @@ +#lang scheme/unit + +(require (rename-in "../utils/utils.ss" [infer r:infer] [extend r:extend])) +(require "signatures.ss" + mzlib/trace + scheme/list + (except-in (rep type-rep effect-rep) make-arr) ;; doesn't need tests + (private type-effect-convenience type-annotation union type-utils) + (env type-environments lexical-env) + (utils tc-utils) + mzlib/plt-match + (only-in (private type-effect-convenience) [make-arr* make-arr])) +(require (for-template scheme/base "internal-forms.ss")) + +(import tc-expr^) +(export tc-lambda^) + +(define (remove-var id thns elss) + (let/ec exit + (define (fail) (exit #f)) + (define (rv e) + (match e + [(Var-True-Effect: v) (if (free-identifier=? v id) (make-Latent-Var-True-Effect) (fail))] + [(Var-False-Effect: v) (if (free-identifier=? v id) (make-Latent-Var-False-Effect) (fail))] + [(or (True-Effect:) (False-Effect:)) e] + [(Restrict-Effect: t v) (if (free-identifier=? v id) (make-Latent-Restrict-Effect t) (fail))] + [(Remove-Effect: t v) (if (free-identifier=? v id) (make-Latent-Remove-Effect t) (fail))])) + (cons (map rv thns) (map rv elss)))) + +(define (expected-str tys-len rest-ty drest arg-len rest) + (format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a" + tys-len + (if (= tys-len 1) "" "s") + (if (or rest-ty + drest) + " and a rest arg" + "") + arg-len + (if (= arg-len 1) "" "s") + (if rest " and a rest arg" ""))) + +;; listof[id] option[id] block listof[type] option[type] option[(cons type var)] type +(define (check-clause arg-list rest body arg-tys rest-ty drest ret-ty) + (let* ([arg-len (length arg-list)] + [tys-len (length arg-tys)] + [arg-types (if (andmap type-annotation arg-list) + (map get-type arg-list) + (cond + [(= arg-len tys-len) arg-tys] + [(< arg-len tys-len) (take arg-tys arg-len)] + [(> arg-len tys-len) (append arg-tys + (map (lambda _ (or rest-ty (Un))) + (drop arg-list tys-len)))]))]) + (define (check-body) + (with-lexical-env/extend + arg-list arg-types + (match (tc-exprs/check (syntax->list body) ret-ty) + [(tc-result: t thn els) + (cond + ;; this is T-AbsPred + ;; if this function takes only one argument, and all the effects are about that one argument + [(and (not rest-ty) (not drest) (= 1 (length arg-list)) (remove-var (car arg-list) thn els)) + => (lambda (thn/els) (make-arr arg-types t rest-ty drest (car thn/els) (cdr thn/els)))] + ;; otherwise, the simple case + [else (make-arr arg-types t rest-ty drest null null)])] + [t (int-err "bad match - not a tc-result: ~a ~a ~a" t ret-ty (syntax->datum body))]))) + #;(for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) arg-list) + (when (or (not (= arg-len tys-len)) + (and rest (and (not rest-ty) + (not drest)))) + (tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest))) + (cond + [(not rest) + (check-body)] + [drest + (with-dotted-env/extend + rest (car drest) (cdr drest) + (check-body))] + [(dotted? rest) + => + (lambda (b) + (let ([dty (get-type rest)]) + (with-dotted-env/extend + rest dty b + (check-body))))] + [else + (let ([rest-type (cond + [rest-ty rest-ty] + [(type-annotation rest) (get-type rest)] + [(< arg-len tys-len) (list-ref arg-tys arg-len)] + [else (Un)])]) + (with-lexical-env/extend + (list rest) (list (-lst rest-type)) + (check-body)))]))) + +;; typecheck a single lambda, with argument list and body +;; drest-ty and drest-bound are both false or not false +;; syntax-list[id] block listof[type] type option[type] option[(cons type var)] -> arr +(define (tc/lambda-clause/check args body arg-tys ret-ty rest-ty drest) + (syntax-case args () + [(args* ...) + (check-clause (syntax->list #'(args* ...)) #f body arg-tys rest-ty drest ret-ty)] + [(args* ... . rest) + (check-clause (syntax->list #'(args* ...)) #'rest body arg-tys rest-ty drest ret-ty)])) + +;; syntax-list[id] block -> arr +(define (tc/lambda-clause args body) + (syntax-case args () + [(args ...) + (let* ([arg-list (syntax->list #'(args ...))] + [arg-types (map get-type arg-list)]) + #;(for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) arg-list) + (with-lexical-env/extend + arg-list arg-types + (match (tc-exprs (syntax->list body)) + [(tc-result: t thn els) + (cond + ;; this is T-AbsPred + ;; if this function takes only one argument, and all the effects are about that one argument + [(and (= 1 (length arg-list)) (remove-var (car arg-list) thn els)) + => (lambda (thn/els) (make-arr arg-types t #f (car thn/els) (cdr thn/els)))] + ;; otherwise, the simple case + [else (make-arr arg-types t)])] + [t (int-err "bad match - not a tc-result: ~a no ret-ty" t)])))] + [(args ... . rest) + (let* ([arg-list (syntax->list #'(args ...))] + [arg-types (map get-type arg-list)]) + #;(for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) (cons #'rest arg-list)) + (cond + [(dotted? #'rest) + => + (lambda (bound) + (unless (Dotted? (lookup (current-tvars) bound + (lambda _ (tc-error/stx #'rest + "Bound on ... type (~a) was not in scope" bound)))) + (tc-error "Bound on ... type (~a) is not an appropriate type variable" bound)) + (let ([rest-type (parameterize ([current-tvars + (extend-env (list bound) + (list (make-DottedBoth (make-F bound))) + (current-tvars))]) + (get-type #'rest))]) + (with-lexical-env/extend + arg-list + arg-types + (parameterize ([dotted-env (extend-env (list #'rest) + (list (cons rest-type bound)) + (dotted-env))]) + (match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))]) + (make-arr-dots arg-types t rest-type bound))))))] + [else + (let ([rest-type (get-type #'rest)]) + (with-lexical-env/extend + (cons #'rest arg-list) + (cons (make-Listof rest-type) arg-types) + (match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))]) + (make-arr arg-types t rest-type))))]))])) + +;(trace tc-args) + +;; tc/mono-lambda : syntax-list syntax-list -> Funty +;; typecheck a sequence of case-lambda clauses +(define (tc/mono-lambda formals bodies expected) + (define (syntax-len s) + (cond [(syntax->list s) => length] + [else (let loop ([s s]) + (cond + [(pair? s) + (+ 1 (loop (cdr s)))] + [(pair? (syntax-e s)) + (+ 1 (loop (cdr (syntax-e s))))] + [else 1]))])) + (if (and expected + (= 1 (length (syntax->list formals)))) + ;; special case for not-case-lambda + (let loop ([expected expected]) + (match expected + [(Mu: _ _) (loop (unfold expected))] + [(Function: (list (arr: argss rets rests drests '() _ _) ...)) + (for ([args argss] [ret rets] [rest rests] [drest drests]) + (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest drest)) + expected] + [t (let ([t (tc/mono-lambda formals bodies #f)]) + (check-below t expected))])) + (let loop ([formals (syntax->list formals)] + [bodies (syntax->list bodies)] + [formals* null] + [bodies* null] + [nums-seen null]) + (cond + [(null? formals) + (make-Function (map tc/lambda-clause (reverse formals*) (reverse bodies*)))] + [(memv (syntax-len (car formals)) nums-seen) + ;; we check this clause, but it doesn't contribute to the overall type + (tc/lambda-clause (car formals) (car bodies)) + (loop (cdr formals) (cdr bodies) formals* bodies* nums-seen)] + [else + (loop (cdr formals) (cdr bodies) + (cons (car formals) formals*) + (cons (car bodies) bodies*) + (cons (syntax-len (car formals)) nums-seen))])))) + +(define (tc/lambda form formals bodies) + (tc/lambda/internal form formals bodies #f)) + +;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic +;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> Type +(define (tc/lambda/internal form formals bodies expected) + (if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected)) + (tc/plambda form formals bodies expected) + (ret (tc/mono-lambda formals bodies expected)))) + +(define (tc/lambda/check form formals bodies expected) + (tc/lambda/internal form formals bodies expected)) + +;; tc/plambda syntax syntax-list syntax-list type -> Poly +;; formals and bodies must by syntax-lists +(define (tc/plambda form formals bodies expected) + (define (maybe-loop form formals bodies expected) + (match expected + [(Function: _) (tc/mono-lambda formals bodies expected)] + [(or (Poly: _ _) (PolyDots: _ _)) + (tc/plambda form formals bodies expected)])) + (match expected + [(Poly-names: ns expected*) + (let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)]) + (when (and (pair? p) (eq? '... (car (last p)))) + (tc-error "Expected a polymorphic function without ..., but given function had ...")) + (or (and p (map syntax-e (syntax->list p))) + ns))] + [literal-tvars tvars] + [new-tvars (map make-F literal-tvars)] + [ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))]) + (maybe-loop form formals bodies expected*))]) + ;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty) + (ret expected))] + [(PolyDots-names: (list ns ... dvar) expected*) + (let-values + ([(tvars dotted) + (let ([p (syntax-property form 'typechecker:plambda)]) + (if p + (match (map syntax-e (syntax->list p)) + [(list var ... dvar '...) + (values var dvar)] + [_ (tc-error "Expected a polymorphic function with ..., but given function had no ...")]) + (values ns dvar)))]) + (let* ([literal-tvars tvars] + [new-tvars (map make-F literal-tvars)] + [ty (parameterize ([current-tvars (extend-env (cons dotted literal-tvars) + (cons (make-Dotted (make-F dotted)) + new-tvars) + (current-tvars))]) + (maybe-loop form formals bodies expected*))]) + (ret expected)))] + [#f + (match (map syntax-e (syntax->list (syntax-property form 'typechecker:plambda))) + [(list tvars ... dotted-var '...) + (let* ([literal-tvars tvars] + [new-tvars (map make-F literal-tvars)] + [ty (parameterize ([current-tvars (extend-env (cons dotted-var literal-tvars) + (cons (make-Dotted (make-F dotted-var)) new-tvars) + (current-tvars))]) + (tc/mono-lambda formals bodies #f))]) + (ret (make-PolyDots (append literal-tvars (list dotted-var)) ty)))] + [tvars + (let* ([literal-tvars tvars] + [new-tvars (map make-F literal-tvars)] + [ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))]) + (tc/mono-lambda formals bodies #f))]) + ;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty) + (ret (make-Poly literal-tvars ty)))])] + [_ + (unless (check-below (tc/plambda form formals bodies #f) expected) + (tc-error/expr #:return (ret expected) "Expected a value of type ~a, but got a polymorphic function." expected)) + (ret expected)])) + + +;; form : a syntax object for error reporting +;; formals : the formal arguments to the loop +;; body : a block containing the body of the loop +;; name : the name of the loop +;; args : the types of the actual arguments to the loop +;; ret : the expected return type of the whole expression +(define (tc/rec-lambda/check form formals body name args ret) + (with-lexical-env/extend + (syntax->list formals) args + (let ([t (->* args ret)]) + (with-lexical-env/extend + (list name) (list t) + (begin (tc-exprs/check (syntax->list body) ret) + (make-Function (list t))))))) + +;(trace tc/mono-lambda) + + diff --git a/collects/typed-scheme/typecheck/tc-let-unit.ss b/collects/typed-scheme/typecheck/tc-let-unit.ss new file mode 100644 index 00000000..9bf2bf3f --- /dev/null +++ b/collects/typed-scheme/typecheck/tc-let-unit.ss @@ -0,0 +1,141 @@ +#lang scheme/unit + +(require (rename-in "../utils/utils.ss" [infer r:infer])) +(require "signatures.ss" + (private type-effect-convenience type-annotation parse-type type-utils) + (env lexical-env type-alias-env type-env) + syntax/free-vars + mzlib/trace + scheme/match + syntax/kerncase + (for-template + scheme/base + "internal-forms.ss")) + +(require (only-in srfi/1/list s:member)) + + +(import tc-expr^) +(export tc-let^) + +(define (do-check expr->type namess types form exprs body clauses expected) + ;; extend the lexical environment for checking the body + (with-lexical-env/extend + ;; the list of lists of name + namess + ;; the types + types + (for-each expr->type + clauses + exprs + (map -values types)) + (if expected + (tc-exprs/check (syntax->list body) expected) + (tc-exprs (syntax->list body))))) + +#| +;; this is more abstract, but sucks + (define ((mk f) namess exprs body form) + (let* ([names (map syntax->list (syntax->list namess))] + [exprs (syntax->list exprs)]) + (f (lambda (e->t namess types exprs) (do-check e->t namess types form exprs body)) names exprs))) + + (define tc/letrec-values + (mk (lambda (do names exprs) + (let ([types (map (lambda (l) (map get-type l)) names)]) + (do tc-expr/t names types exprs))))) + + (define tc/let-values + (mk (lambda (do names exprs) + (let* (;; the types of the exprs + [inferred-types (map tc-expr/t exprs)] + ;; the annotated types of the name (possibly using the inferred types) + [types (map get-type/infer names inferred-types)]) + (do (lambda (x) x) names types inferred-types))))) + |# + +(define (tc/letrec-values/check namess exprs body form expected) + (tc/letrec-values/internal namess exprs body form expected)) + +(define (tc/letrec-values namess exprs body form) + (tc/letrec-values/internal namess exprs body form #f)) + +(define (tc-expr/maybe-expected/t e name) + (define expecteds + (map (lambda (stx) (lookup-type stx (lambda () #f))) name)) + (define mk (if (and (pair? expecteds) (null? (cdr expecteds))) + car + -values)) + (define tcr + (if + (andmap values expecteds) + (tc-expr/check e (mk expecteds)) + (tc-expr e))) + (match tcr + [(tc-result: t) t])) + +(define (tc/letrec-values/internal namess exprs body form expected) + (let* ([names (map syntax->list (syntax->list namess))] + [flat-names (apply append names)] + [exprs (syntax->list exprs)] + ;; the clauses for error reporting + [clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])]) + (for-each (lambda (names body) + (kernel-syntax-case* body #f (values :-internal define-type-alias-internal) + [(begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)) + (register-resolved-type-alias #'nm (parse-type #'ty))] + [(begin (quote-syntax (:-internal nm ty)) (#%plain-app values)) + (register-type/undefined #'nm (parse-type #'ty))] + [_ (void)])) + names + exprs) + (let loop ([names names] [exprs exprs] [flat-names flat-names] [clauses clauses]) + (cond + ;; after everything, check the body expressions + [(null? names) + (if expected (tc-exprs/check (syntax->list body) expected) (tc-exprs (syntax->list body)))] + ;; if none of the names bound in the letrec are free vars of this rhs + [(not (ormap (lambda (n) (s:member n flat-names bound-identifier=?)) (free-vars (car exprs)))) + ;; then check this expression separately + (with-lexical-env/extend + (list (car names)) + (list (get-type/infer (car names) (car exprs) (lambda (e) (tc-expr/maybe-expected/t e (car names))) tc-expr/check/t)) + (loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses)))] + [else + ;(for-each (lambda (vs) (for-each (lambda (v) (printf/log "Letrec Var: ~a~n" (syntax-e v))) vs)) names) + (do-check (lambda (stx e t) (tc-expr/check/t e t)) + names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)])))) + +;; this is so match can provide us with a syntax property to +;; say that this binding is only called in tail position +(define ((tc-expr-t/maybe-expected expected) e) + (kernel-syntax-case e #f + [(#%plain-lambda () _) + (and expected (syntax-property e 'typechecker:called-in-tail-position)) + (begin + (tc-expr/check e (-> expected)) + (-> expected))] + [_ (tc-expr/t e)])) + +(define (tc/let-values/internal namess exprs body form expected) + (let* (;; a list of each name clause + [names (map syntax->list (syntax->list namess))] + ;; all the trailing expressions - the ones actually bound to the names + [exprs (syntax->list exprs)] + ;; the types of the exprs + #;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)] + ;; the annotated types of the name (possibly using the inferred types) + [types (for/list ([name names] [e exprs]) (get-type/infer name e (tc-expr-t/maybe-expected expected) tc-expr/check/t))] + ;; the clauses for error reporting + [clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])]) + (do-check void names types form types body clauses expected))) + +(define (tc/let-values/check namess exprs body form expected) + (tc/let-values/internal namess exprs body form expected)) + +(define (tc/let-values namess exprs body form) + (tc/let-values/internal namess exprs body form #f)) + +;(trace tc/letrec-values/internal) + + diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss new file mode 100644 index 00000000..86233c0d --- /dev/null +++ b/collects/typed-scheme/typecheck/tc-structs.ss @@ -0,0 +1,210 @@ +#lang scheme/base + +(require (except-in "../utils/utils.ss" extend)) +(require (rep type-rep) + (private type-effect-convenience + type-utils parse-type + union resolve-type) + (env type-env type-environments type-name-env) + (utils tc-utils) + "def-binding.ss" + syntax/kerncase + syntax/struct + mzlib/trace + scheme/match + (for-syntax scheme/base)) + + +(require (for-template scheme/base + "internal-forms.ss")) + +(provide tc/struct tc/poly-struct names-of-struct tc/builtin-struct d-s) + +(define (names-of-struct stx) + (define (parent? stx) + (syntax-case stx () + [(a b) + (and (identifier? #'a) + (identifier? #'b)) + #t] + [a + (identifier? #'a) + #t] + [_ #f])) + (kernel-syntax-case* stx #f + (define-typed-struct-internal values) + [(#%define-values () (begin (quote-syntax (define-typed-struct-internal (ids ...) nm/par . rest)) (#%plain-app values))) + (and (andmap identifier? (syntax->list #'(ids ...))) + (parent? #'nm/par)) + (let-values ([(nm _1 _2 _3 _4) (parse-parent #'nm/par)]) + (list nm))] + [(#%define-values () (begin (quote-syntax (define-typed-struct-internal nm/par . rest)) (#%plain-app values))) + (let-values ([(nm _1 _2 _3 _4) (parse-parent #'nm/par)]) + (list nm))] + [(#%define-values () (begin (quote-syntax (define-typed-struct/exec-internal nm/par . rest)) (#%plain-app values))) + (let-values ([(nm _1 _2 _3 _4) (parse-parent #'nm/par)]) + (list nm))] + [_ (int-err "not define-typed-struct: ~a" (syntax->datum stx))])) + +;; parse name field of struct, determining whether a parent struct was specified +;; syntax -> (values identifier Option[Type](must be name) Option[Type](must be struct) List[Types] Symbol Type) +(define (parse-parent nm/par) + (syntax-case nm/par () + [nm (identifier? #'nm) (values #'nm #f #f (syntax-e #'nm) (make-F (syntax-e #'nm)))] + [(nm par) (let* ([parent0 (parse-type #'par)] + [parent (resolve-name parent0)]) + (values #'nm parent0 parent (syntax-e #'nm) (make-F (syntax-e #'nm))))] + [_ (int-err "not a parent: ~a" (syntax->datum nm/par))])) + +;; generate struct names given type name and field names +;; generate setters if setters? is true +;; all have syntax loc of name +;; identifier listof[identifier] boolean -> (values identifier identifier list[identifier] Option[list[identifier]]) +(define (struct-names nm flds setters?) + (define (split l) + (let loop ([l l] [getters '()] [setters '()]) + (if (null? l) + (values (reverse getters) (reverse setters)) + (loop (cddr l) (cons (car l) getters) (cons (cadr l) setters))))) + (match (build-struct-names nm flds #f (not setters?) nm) + [(list _ maker pred getters/setters ...) + (if setters? + (let-values ([(getters setters) (split getters/setters)]) + (values maker pred getters setters)) + (values maker pred getters/setters #f))])) + +;; gets the fields of the parent type, if they exist +;; Option[Struct-Ty] -> Listof[Type] +(define (get-parent-flds p) + (match p + [(Struct: _ _ flds _ _ _ _) flds] + [(Name: n) (get-parent-flds (lookup-type-name n))] + [#f null])) + + +;; construct all the various types for structs, and then register the approriate names +;; identifier listof[identifier] type listof[Type] listof[Type] boolean -> Type listof[Type] listof[Type] +(define (mk/register-sty nm flds parent parent-field-types types + #:wrapper [wrapper values] + #:type-wrapper [type-wrapper values] + #:mutable [setters? #f] + #:proc-ty [proc-ty #f] + #:maker [maker #f] + #:constructor-return [cret #f] + #:poly? [poly? #f]) + ;; create the approriate names that define-struct will bind + (define-values (maker pred getters setters) (struct-names nm flds setters?)) + (let* ([name (syntax-e nm)] + [fld-types (append parent-field-types types)] + [sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier))] + [external-fld-types/no-parent types] + [external-fld-types fld-types]) + (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters? + #:wrapper wrapper + #:type-wrapper type-wrapper + #:maker maker + #:constructor-return cret))) + +;; generate names, and register the approriate types give field types and structure type +;; optionally wrap things +;; identifier Type Listof[identifer] Listof[Type] Listof[Type] #:wrapper (Type -> Type) #:maker identifier +(define (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters? + #:wrapper [wrapper (lambda (x) x)] + #:type-wrapper [type-wrapper values] + #:maker [maker* #f] + #:constructor-return [cret #f]) + ;; create the approriate names that define-struct will bind + (define-values (maker pred getters setters) (struct-names nm flds setters?)) + ;; the type name that is used in all the types + (define name (type-wrapper (make-Name nm))) + ;; the list of names w/ types + (define bindings + (append + (list (cons (or maker* maker) + (wrapper (->* external-fld-types (if cret cret name)))) + (cons pred + (make-pred-ty (wrapper name)))) + (map (lambda (g t) (cons g (wrapper (->* (list name) t)))) getters external-fld-types/no-parent) + (if setters? + (map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent) + null))) + (register-type-name nm (wrapper sty)) + (for/list ([e bindings]) + (let ([nm (car e)] + [t (cdr e)]) + (register-type nm t) + (make-def-binding nm t)))) + +;; check and register types for a polymorphic define struct +;; tc/poly-struct : Listof[identifier] (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void +(define (tc/poly-struct vars nm/par flds tys) + ;; parent field types can't actually be determined here + (define-values (nm parent-name parent name name-tvar) (parse-parent nm/par)) + ;; create type variables for the new type parameters + (define tvars (map syntax-e vars)) + (define new-tvars (map make-F tvars)) + ;; parse the types + (define types + ;; add the type parameters of this structure to the tvar env + (parameterize ([current-tvars (extend-env tvars new-tvars (current-tvars))]) + ;; parse the field types + (map parse-type tys))) + ;; instantiate the parent if necessary, with new-tvars + (define concrete-parent + (if (Poly? parent) + (instantiate-poly parent new-tvars) + parent)) + ;; get the fields of the parent, if it exists + (define parent-field-types (get-parent-flds concrete-parent)) + ;; create the actual structure type, and the types of the fields + ;; that the outside world will see + ;; then register them + (mk/register-sty nm flds parent-name parent-field-types types + ;; wrap everything in the approriate forall + #:wrapper (lambda (t) (make-Poly tvars t)) + #:type-wrapper (lambda (t) (make-App t new-tvars #f)) + #:poly? #t)) + + +;; typecheck a non-polymophic struct and register the approriate types +;; tc/struct : (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void +(define (tc/struct nm/par flds tys [proc-ty #f] #:maker [maker #f] #:constructor-return [cret #f] #:mutable [mutable #f]) + ;; get the parent info and create some types and type variables + (define-values (nm parent-name parent name name-tvar) (parse-parent nm/par)) + ;; parse the field types, and determine if the type is recursive + (define types (map parse-type tys)) + (define proc-ty-parsed + (if proc-ty + (parse-type proc-ty) + #f)) + ;; create the actual structure type, and the types of the fields + ;; that the outside world will see + (mk/register-sty nm flds parent-name (get-parent-flds parent) types + ;; procedure + #:proc-ty proc-ty-parsed + #:maker maker + #:constructor-return (and cret (parse-type cret)) + #:mutable mutable)) + +;; register a struct type +;; convenience function for built-in structs +;; tc/builtin-struct : identifier identifier Listof[identifier] Listof[Type] Listof[Type] -> void +(define (tc/builtin-struct nm parent flds tys parent-tys) + (let ([parent* (if parent (make-Name parent) #f)]) + (mk/register-sty nm flds parent* parent-tys tys + #:mutable #t))) + +;; syntax for tc/builtin-struct +(define-syntax (d-s stx) + (syntax-case stx (:) + [(_ (nm par) ([fld : ty] ...) (par-ty ...)) + #'(tc/builtin-struct #'nm #'par + (list #'fld ...) + (list ty ...) + (list par-ty ...))] + [(_ nm ([fld : ty] ...) (par-ty ...)) + #'(tc/builtin-struct #'nm #f + (list #'fld ...) + (list ty ...) + (list par-ty ...))])) + diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss new file mode 100644 index 00000000..5f2d36f2 --- /dev/null +++ b/collects/typed-scheme/typecheck/tc-toplevel.ss @@ -0,0 +1,242 @@ +#lang scheme/unit + + +(require (rename-in "../utils/utils.ss" [infer r:infer])) +(require syntax/kerncase + mzlib/etc + scheme/match + "signatures.ss" + "tc-structs.ss" + (private type-utils type-effect-convenience parse-type type-annotation mutated-vars type-contract) + (env type-env init-envs type-name-env type-alias-env) + (utils tc-utils) + "provide-handling.ss" + "def-binding.ss" + (for-template + "internal-forms.ss" + mzlib/contract + scheme/base)) + +(import tc-expr^ check-subforms^) +(export typechecker^) + +(define (tc-toplevel/pass1 form) + ;(printf "form-top: ~a~n" form) + ;; first, find the mutated variables: + (find-mutated-vars form) + (parameterize ([current-orig-stx form]) + (kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal + define-typed-struct/exec-internal :-internal assert-predicate-internal + require/typed-internal values) + ;; forms that are handled in other ways + [stx + (or (syntax-property form 'typechecker:ignore) + (syntax-property form 'typechecker:ignore-some)) + (list)] + + ;; type aliases have already been handled by an earlier pass + [(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values))) + (list)] + + ;; require/typed + [(define-values () (begin (quote-syntax (require/typed-internal nm ty)) (#%plain-app values))) + (register-type #'nm (parse-type #'ty))] + + ;; define-typed-struct + [(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...))) (#%plain-app values))) + (tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))] + [(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...) #:mutable)) (#%plain-app values))) + (tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:mutable #t)] + [(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...) #:maker m #:constructor-return t)) + (#%plain-app values))) + (tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:maker #'m #:constructor-return #'t)] + ;; define-typed-struct w/ polymorphism + [(define-values () (begin (quote-syntax (define-typed-struct-internal (vars ...) nm ([fld : ty] ...))) (#%plain-app values))) + (tc/poly-struct (syntax->list #'(vars ...)) #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))] + + ;; executable structs - this is a big hack + [(define-values () (begin (quote-syntax (define-typed-struct/exec-internal nm ([fld : ty] ...) proc-ty)) (#%plain-app values))) + (tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #'proc-ty)] + + ;; predicate assertion - needed for define-type b/c or doesn't work + [(define-values () (begin (quote-syntax (assert-predicate-internal ty pred)) (#%plain-app values))) + (register-type #'pred (make-pred-ty (parse-type #'ty)))] + + ;; top-level type annotation + [(define-values () (begin (quote-syntax (:-internal id ty)) (#%plain-app values))) + (identifier? #'id) + (register-type/undefined #'id (parse-type #'ty))] + + + ;; values definitions + [(define-values (var ...) expr) + (let* ([vars (syntax->list #'(var ...))]) + (cond + ;; if all the variables have types, we stick them into the environment + [(andmap (lambda (s) (syntax-property s 'type-label)) vars) + (let ([ts (map get-type vars)]) + (for-each register-type vars ts) + (map make-def-binding vars ts))] + ;; if this already had an annotation, we just construct the binding reps + [(andmap (lambda (s) (lookup-type s (lambda () #f))) vars) + (for-each finish-register-type vars) + (map (lambda (s) (make-def-binding s (lookup-type s))) vars)] + ;; special case to infer types for top level defines - should handle the multiple values case here + [(and (= 1 (length vars)) + (with-handlers ([exn:fail? (lambda _ #f)]) + (save-errors!) + (begin0 (tc-expr #'expr) + (restore-errors!)))) + => (match-lambda + [(tc-result: t) + (register-type (car vars) t) + (list (make-def-binding (car vars) t))] + [t (int-err "~a is not a tc-result" t)])] + [else + (tc-error "Untyped definition : ~a" (map syntax-e vars))]))] + + ;; to handle the top-level, we have to recur into begins + [(begin . rest) + (apply append (filter list? (map tc-toplevel/pass1 (syntax->list #'rest))))] + + ;; define-syntaxes just get noted + [(define-syntaxes (var ...) . rest) + (andmap identifier? (syntax->list #'(var ...))) + (map make-def-stx-binding (syntax->list #'(var ...)))] + + ;; otherwise, do nothing in this pass + ;; handles expressions, provides, requires, etc and whatnot + [_ (list)]))) + + + + + +;; typecheck the expressions of a module-top-level form +;; no side-effects +;; syntax -> void +(define (tc-toplevel/pass2 form) + (parameterize ([current-orig-stx form]) + (kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal + require/typed-internal values) + ;; these forms we have been instructed to ignore + [stx + (syntax-property form 'typechecker:ignore) + (void)] + + ;; this is a form that we mostly ignore, but we check some interior parts + [stx + (syntax-property form 'typechecker:ignore-some) + (check-subforms/ignore form)] + + ;; these forms should always be ignored + [(#%require . _) (void)] + [(#%provide . _) (void)] + [(define-syntaxes . _) (void)] + [(define-values-for-syntax . _) (void)] + + ;; these forms are handled in pass1 + [(define-values () (begin (quote-syntax (require/typed-internal . rest)) (#%plain-app values))) + (void)] + [(define-values () (begin (quote-syntax (define-type-alias-internal . rest)) (#%plain-app values))) + (void)] + [(define-values () (begin (quote-syntax (define-typed-struct-internal . rest)) (#%plain-app values))) + (void)] + + ;; definitions just need to typecheck their bodies + [(define-values (var ...) expr) + (let* ([vars (syntax->list #'(var ...))] + [ts (map lookup-type vars)]) + (tc-expr/check #'expr (-values ts))) + (void)] + + ;; to handle the top-level, we have to recur into begins + [(begin) (void)] + [(begin . rest) + (let loop ([l (syntax->list #'rest)]) + (if (null? (cdr l)) + (tc-toplevel/pass2 (car l)) + (begin (tc-toplevel/pass2 (car l)) + (loop (cdr l)))))] + + ;; otherwise, the form was just an expression + [_ (tc-expr form)]))) + + + +;; new implementation of type-check +(define-syntax-rule (internal-syntax-pred nm) + (lambda (form) + (kernel-syntax-case* form #f + (nm values) + [(define-values () (begin (quote-syntax (nm . rest)) (#%plain-app values))) + #t] + [_ #f]))) + +(define (parse-def x) + (kernel-syntax-case x #f + [(define-values (nm ...) . rest) (syntax->list #'(nm ...))] + [_ #f])) + +(define (parse-syntax-def x) + (kernel-syntax-case x #f + [(define-syntaxes (nm ...) . rest) (syntax->list #'(nm ...))] + [_ #f])) + + +(define (add-type-name! names) + (for-each register-type-name names)) + +(define (parse-type-alias form) + (kernel-syntax-case* form #f + (define-type-alias-internal values) + [(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values))) + (values #'nm #'ty)] + [_ (int-err "not define-type-alias")])) + +(define (type-check forms0) + (begin-with-definitions + (define forms (syntax->list forms0)) + (define-values (type-aliases struct-defs stx-defs0 val-defs0 provs reqs) + (filter-multiple + forms + (internal-syntax-pred define-type-alias-internal) + (lambda (e) (or ((internal-syntax-pred define-typed-struct-internal) e) + ((internal-syntax-pred define-typed-struct/exec-internal) e))) + parse-syntax-def + parse-def + provide? + define/fixup-contract?)) + (for-each (compose register-type-alias parse-type-alias) type-aliases) + ;; add the struct names to the type table + (for-each (compose add-type-name! names-of-struct) struct-defs) + ;; resolve all the type aliases, and error if there are cycles + (resolve-type-aliases parse-type) + ;; do pass 1, and collect the defintions + (define defs (apply append (filter list? (map tc-toplevel/pass1 forms)))) + ;; separate the definitions into structures we'll handle for provides + (define stx-defs (filter def-stx-binding? defs)) + (define val-defs (filter def-binding? defs)) + ;; typecheck the expressions and the rhss of defintions + (for-each tc-toplevel/pass2 forms) + ;; check that declarations correspond to definitions + (check-all-registered-types) + ;; report delayed errors + (report-all-errors) + ;; compute the new provides + (with-syntax + ([((new-provs ...) ...) (map (generate-prov stx-defs val-defs) provs)]) + #`(begin + #,(env-init-code) + #,(tname-env-init-code) + #,(talias-env-init-code) + (begin new-provs ... ...))))) + +;; typecheck a top-level form +;; used only from #%top-interaction +;; syntax -> void +(define (tc-toplevel-form form) + (tc-toplevel/pass1 form) + (begin0 (tc-toplevel/pass2 form) + (report-all-errors))) + diff --git a/collects/typed-scheme/typecheck/typechecker.ss b/collects/typed-scheme/typecheck/typechecker.ss new file mode 100644 index 00000000..ed935ff9 --- /dev/null +++ b/collects/typed-scheme/typecheck/typechecker.ss @@ -0,0 +1,15 @@ +#lang scheme/base + +(require "../utils/utils.ss") +(require (utils unit-utils) + mzlib/trace + (only-in scheme/unit provide-signature-elements) + "signatures.ss" "tc-toplevel.ss" + "tc-if-unit.ss" "tc-lambda-unit.ss" "tc-app-unit.ss" + "tc-let-unit.ss" "tc-dots-unit.ss" + "tc-expr-unit.ss" "check-subforms-unit.ss") + +(provide-signature-elements typechecker^ tc-expr^) + +(define-values/link-units/infer + tc-toplevel@ tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@) diff --git a/collects/typed-scheme/typed-scheme.scrbl b/collects/typed-scheme/typed-scheme.scrbl index 95baadbf..afab39a1 100644 --- a/collects/typed-scheme/typed-scheme.scrbl +++ b/collects/typed-scheme/typed-scheme.scrbl @@ -436,13 +436,16 @@ The following base types are parameteric in their type arguments. @defform*[#:id -> #:literals (* ...) [(dom ... -> rng) (dom ... rest * -> rng) - (dom ... rest ... bound -> rng)]]{is the type of functions from the (possibly-empty) + (dom ... rest ... bound -> rng) + (dom -> rng : pred)]]{is the type of functions from the (possibly-empty) sequence @scheme[dom ...] to the @scheme[rng] type. The second form specifies a uniform rest argument of type @scheme[rest], and the third form specifies a non-uniform rest argument of type @scheme[rest] with bound @scheme[bound]. In the third form, the second occurrence of @scheme[...] is literal, and @scheme[bound] - must be an identifier denoting a type variable.} + must be an identifier denoting a type variable. In the fourth form, + there must be only one @scheme[dom] and @scheme[pred] is the type + checked by the predicate.} @defform[(U t ...)]{is the union of the types @scheme[t ...]} @defform[(case-lambda fun-ty ...)]{is a function that behaves like all of the @scheme[fun-ty]s. The @scheme[fun-ty]s must all be function diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss index 19c9c9cb..0bcfc701 100644 --- a/collects/typed-scheme/typed-scheme.ss +++ b/collects/typed-scheme/typed-scheme.ss @@ -1,22 +1,18 @@ #lang scheme/base -(require "private/base-env.ss" - "private/base-types.ss" +(require (rename-in "utils/utils.ss" [infer r:infer])) + +(require (private base-env base-types) (for-syntax scheme/base - "private/type-utils.ss" - "private/typechecker.ss" - "private/type-rep.ss" - "private/provide-handling.ss" - "private/type-environments.ss" - "private/tc-utils.ss" - "private/type-name-env.ss" - "private/type-alias-env.ss" - (except-in "private/utils.ss" extend) - (only-in "private/infer-dummy.ss" infer-param) - "private/infer.ss" - "private/type-effect-convenience.ss" - "private/type-contract.ss" + (private type-utils type-contract type-effect-convenience) + (typecheck typechecker provide-handling) + (env type-environments type-name-env type-alias-env) + (r:infer infer) + (utils tc-utils) + (rep type-rep) + (except-in (utils utils) infer extend) + (only-in (r:infer infer-dummy) infer-param) scheme/nest syntax/kerncase scheme/match)) @@ -31,7 +27,7 @@ (provide (rename-out [module-begin #%module-begin] [top-interaction #%top-interaction] [#%plain-lambda lambda] - [#%plain-app #%app] + [#%app #%app] [require require])) (define-for-syntax catch-errors? #f) diff --git a/collects/typed-scheme/utils/tc-utils.ss b/collects/typed-scheme/utils/tc-utils.ss new file mode 100644 index 00000000..132b2206 --- /dev/null +++ b/collects/typed-scheme/utils/tc-utils.ss @@ -0,0 +1,134 @@ +#lang scheme/base +(provide (all-defined-out)) +(require "syntax-traversal.ss" (for-syntax scheme/base) scheme/match) + +;; a parameter representing the original location of the syntax being currently checked +(define current-orig-stx (make-parameter #'here)) +(define orig-module-stx (make-parameter #f)) +(define expanded-module-stx (make-parameter #f)) + +(define (stringify l [between " "]) + (define (intersperse v l) + (cond [(null? l) null] + [(null? (cdr l)) l] + [else (cons (car l) (cons v (intersperse v (cdr l))))])) + (apply string-append (intersperse between (map (lambda (s) (format "~a" s)) l)))) + +;; helper function, not currently used +(define (find-origin stx) + (cond [(syntax-property stx 'origin) => (lambda (orig) + (let ([r (reverse orig)]) + (let loop ([r (reverse orig)]) + (if (null? r) #f + (if (syntax-source (car r)) (car r) + (loop (cdr r)))))))] + [else #f])) + +;; do we print the fully-expanded syntax in error messages? +(define print-syntax? (make-parameter #f)) + + +(define check-unreachable-code? (make-parameter #f)) + +(define (locate-stx stx) + (define omodule (orig-module-stx)) + (define emodule (expanded-module-stx)) + ;(printf "orig: ~a~n" (syntax-object->datum omodule)) + ;(printf "exp: ~a~n" (syntax-object->datum emodule)) + ;(printf "stx (locate): ~a~n" (syntax-object->datum stx)) + (if (and (not (print-syntax?)) omodule emodule stx) + (look-for-in-orig omodule emodule stx) + stx)) + +(define (raise-typecheck-error msg stxs) + (raise (make-exn:fail:syntax (string-append "typecheck: " msg) + (current-continuation-marks) + stxs))) + +(define delayed-errors null) + +(define-struct err (msg stx) #:prefab) + +(define-values (save-errors! restore-errors!) + (let ([v (box #f)]) + (values (lambda () (set-box! v delayed-errors)) + (lambda () (set! delayed-errors (unbox v)))))) + +(define (report-all-errors) + (define (reset!) (set! delayed-errors null)) + (match (reverse delayed-errors) + [(list) (void)] + [(list (struct err (msg stx))) + (reset!) + (raise-typecheck-error msg stx)] + [l + (let ([stxs + (for/list ([e l]) + (sync (thread (lambda () (raise-typecheck-error (err-msg e) (err-stx e))))) + (err-stx e))]) + (reset!) + (unless (null? stxs) + (raise-typecheck-error (format "Summary: ~a errors encountered" (length stxs)) (apply append stxs))))])) + +(define delay-errors? (make-parameter #f)) + +(define (tc-error/delayed msg #:stx [stx* (current-orig-stx)] . rest) + (let ([stx (locate-stx stx*)]) + (unless (syntax? stx) + (int-err "erroneous syntax was not a syntax object: ~a ~a" stx (syntax->datum stx*))) + (if (delay-errors?) + (set! delayed-errors (cons (make-err (apply format msg rest) (list stx)) delayed-errors)) + (raise-typecheck-error (apply format msg rest) (list stx))))) + +;; produce a type error, using the current syntax +(define (tc-error msg . rest) + (let ([stx (locate-stx (current-orig-stx))]) + ;; If this isn't original syntax, then we can get some pretty bogus error messages. Note + ;; that this is from a macro expansion, so that introduced vars and such don't confuse the user. + (cond + [(not (orig-module-stx)) + (raise-typecheck-error (apply format msg rest) (list stx))] + [(eq? (syntax-source (current-orig-stx)) (syntax-source (orig-module-stx))) + (raise-typecheck-error (apply format msg rest) (list stx))] + [else (raise-typecheck-error (apply format (string-append "Error in macro expansion -- " msg) rest) (list stx))]))) + +;; produce a type error, given a particular syntax +(define (tc-error/stx stx msg . rest) + (parameterize ([current-orig-stx stx]) + (apply tc-error msg rest))) + +;; check two identifiers to see if they have the same name +(define (symbolic-identifier=? a b) + (eq? (syntax-e a) (syntax-e b))) + +;; parameter for currently-defined type aliases +;; this is used only for printing type names +(define current-type-names (make-parameter (lambda () '()))) + +;; for reporting internal errors in the type checker +(define-struct (exn:fail:tc exn:fail) ()) + +;; raise an internal error - typechecker bug! +(define (int-err msg . args) + (raise (make-exn:fail:tc (string-append "Internal Typechecker Error: " + (apply format msg args) + (format "\nwhile typechecking\n~a" (syntax->datum (current-orig-stx)))) + (current-continuation-marks)))) + +(define-syntax (nyi stx) + (syntax-case stx () + [(_ str) + (quasisyntax/loc stx (int-err "~a: not yet implemented: ~a" str #,(syntax/loc stx (this-expression-file-name))))] + [(_) (syntax/loc stx (nyi ""))])) + + +;; are we currently expanding in a typed module (or top-level form)? +(define typed-context? (box #f)) + +;; what type names have been referred to in this module? +(define type-name-references (make-parameter '())) + +(define (add-type-name-reference t) + (type-name-references (cons t (type-name-references)))) + + diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss new file mode 100644 index 00000000..6ca8a6a9 --- /dev/null +++ b/collects/typed-scheme/utils/utils.ss @@ -0,0 +1,224 @@ +#lang scheme/base + +(require (for-syntax scheme/base) + mzlib/plt-match + scheme/require-syntax + mzlib/struct) + +(provide with-syntax* syntax-map start-timing do-time reverse-begin printf/log + with-logging-to-file log-file-name == + print-type* + print-effect* + define-struct/printer + id + filter-multiple + hash-union + in-pairs + in-list-forever + extend + debug + in-syntax + ;; require macros + rep utils typecheck infer env private) + +(define-syntax (define-requirer stx) + (syntax-case stx () + [(_ nm) + #`(... + (define-require-syntax nm + (lambda (stx) + (syntax-case stx () + [(_ id ...) + (andmap identifier? (syntax->list #'(id ...))) + (with-syntax ([(id* ...) + (map (lambda (id) + (datum->syntax + id + (string->symbol + (string-append + "typed-scheme/" + #,(symbol->string (syntax-e #'nm)) + "/" + (symbol->string (syntax-e id)))) + id id)) + (syntax->list #'(id ...)))]) + (syntax/loc stx (combine-in id* ...)))]))))])) + + +(define-requirer rep) +(define-requirer infer) +(define-requirer typecheck) +(define-requirer utils) +(define-requirer env) +(define-requirer private) + +(define-sequence-syntax in-syntax + (lambda () #'syntax->list) + (lambda (stx) + (syntax-case stx () + [[ids (_ arg)] + #'[ids (in-list (syntax->list arg))]]))) + +(define-syntax debug + (syntax-rules () + [(_ (f . args)) + (begin (printf "starting ~a~n" 'f) + (let ([l (list . args)]) + (printf "arguments are:~n") + (for/list ([arg 'args] + [val l]) + (printf "\t~a: ~a~n" arg val)) + (let ([e (apply f l)]) + (printf "result was ~a~n" e) + e)))] + [(_ . args) + (begin (printf "starting ~a~n" 'args) + (let ([e args]) + (printf "result was ~a~n" e) + e))])) + +(define-syntax (with-syntax* stx) + (syntax-case stx () + [(_ (cl) body ...) #'(with-syntax (cl) body ...)] + [(_ (cl cls ...) body ...) + #'(with-syntax (cl) (with-syntax* (cls ...) body ...))] + )) + +(define (filter-multiple l . fs) + (apply values + (map (lambda (f) (filter f l)) fs))) + +(define (syntax-map f stxl) + (map f (syntax->list stxl))) + +(define-syntax reverse-begin + (syntax-rules () [(_ h . forms) (begin0 (begin . forms) h)])) + +#; +(define-syntax define-simple-syntax + (syntax-rules () + [(dss (n . pattern) template) + (define-syntax n (syntax-rules () [(n . pattern) template]))])) + +(define log-file (make-parameter #f)) +(define-for-syntax logging? #f) + +(require (only-in mzlib/file file-name-from-path)) + +(define-syntax (printf/log stx) + (if logging? + (syntax-case stx () + [(_ fmt . args) + #'(when (log-file) + (fprintf (log-file) (string-append "~a: " fmt) + (file-name-from-path (object-name (log-file))) + . args))]) + #'(void))) + +(define (log-file-name src module-name) + (if (path? src) + (path-replace-suffix src ".log") + (format "~a.log" module-name))) + +(define-syntax (with-logging-to-file stx) + (syntax-case stx () + [(_ file . body) + (if logging? + #'(parameterize ([log-file (open-output-file file #:exists 'append)]) + . body) + #'(begin . body))])) + + +(define-for-syntax timing? #f) + +(define last-time (make-parameter #f)) +(define-syntaxes (start-timing do-time) + (if timing? + (values + (syntax-rules () + [(_ msg) + (begin + (when (last-time) + (error #f "Timing already started")) + (last-time (current-process-milliseconds)) + (printf "Starting ~a at ~a~n" msg (last-time)))]) + (syntax-rules () + [(_ msg) + (begin + (unless (last-time) + (start-timing msg)) + (let* ([t (current-process-milliseconds)] + [old (last-time)] + [diff (- t old)]) + (last-time t) + (printf "Timing ~a at ~a@~a~n" msg diff t)))])) + (values (lambda _ #'(void)) (lambda _ #'(void))))) + + +(define (symbol-append . args) + (string->symbol (apply string-append (map symbol->string args)))) + +(define-match-expander + == + (lambda (stx) + (syntax-case stx () + [(_ val) + #'(? (lambda (x) (equal? val x)))]))) + +(define-for-syntax printing? #t) + +(define print-type* (box (lambda _ (error "print-type* not yet defined")))) +(define print-effect* (box (lambda _ (error "print-effect* not yet defined")))) + +(define-syntax (define-struct/printer stx) + (syntax-case stx () + [(form name (flds ...) printer) + #`(define-struct/properties name (flds ...) + #,(if printing? #'([prop:custom-write printer]) #'()) + #f)])) + +(define (id kw . args) + (define (f v) + (cond [(string? v) v] + [(symbol? v) (symbol->string v)] + [(identifier? v) (symbol->string (syntax-e v))])) + (datum->syntax kw (string->symbol (apply string-append (map f args))))) + + +;; map map (key val val -> val) -> map +(define (hash-union h1 h2 f) + (for/fold ([h* h1]) + ([(k v2) h2]) + (let* ([v1 (hash-ref h1 k #f)] + [new-val (if v1 + (f k v1 v2) + v2)]) + (hash-set h* k new-val)))) + + +(define (in-pairs seq) + (make-do-sequence + (lambda () + (let-values ([(more? gen) (sequence-generate seq)]) + (values (lambda (e) (let ([e (gen)]) (values (car e) (cdr e)))) + (lambda (_) #t) + #t + (lambda (_) (more?)) + (lambda _ #t) + (lambda _ #t)))))) + +(define (in-list-forever seq val) + (make-do-sequence + (lambda () + (let-values ([(more? gen) (sequence-generate seq)]) + (values (lambda (e) (let ([e (if (more?) (gen) val)]) e)) + (lambda (_) #t) + #t + (lambda (_) #t) + (lambda _ #t) + (lambda _ #t)))))) + +;; Listof[A] Listof[B] B -> Listof[B] +;; pads out t to be as long as s +(define (extend s t extra) + (append t (build-list (- (length s) (length t)) (lambda _ extra)))) \ No newline at end of file