svn merge -r11644:11643 .

Yeah, these trunk merges will eventually come back.

svn: r11655
This commit is contained in:
Stevie Strickland 2008-09-11 22:21:45 +00:00
parent cfb01a1828
commit ae2d69720c
75 changed files with 374 additions and 559 deletions

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@ -1,6 +1,6 @@
#lang scheme
(require "test-utils.ss")
(require (utils planet-requires))
(require (private planet-requires))
(require (schemeunit))
(provide module-tests)

View File

@ -1,10 +1,8 @@
#lang scheme/base
(require "test-utils.ss" (for-syntax scheme/base))
(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 (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 (rename-in (private type-effect-convenience) [-> t:->])
(except-in (private base-types) Un)

View File

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

View File

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

View File

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

View File

@ -3,12 +3,25 @@
(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)

View File

@ -1,10 +1,8 @@
#lang scheme/base
(require "test-utils.ss"
(for-syntax scheme/base))
(require (private type-annotation type-effect-convenience parse-type)
(env type-environments type-name-env init-envs)
(utils planet-requires tc-utils)
(rep type-rep))
(require (private planet-requires type-annotation tc-utils type-rep type-effect-convenience type-environments
parse-type init-envs type-name-env))
(require (schemeunit))

View File

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

View File

@ -3,16 +3,14 @@
(require "test-utils.ss"
(for-syntax scheme/base)
(for-template scheme/base))
(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 base-env))
(require (for-syntax (utils tc-utils)
(typecheck typechecker)
(env type-env)
(private base-env))
(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))
(for-template (private base-env base-types)))
(require (schemeunit))
@ -671,7 +669,7 @@
(tc-l #t (-val #t))
(tc-l "foo" -String)
(tc-l foo (-val 'foo))
(tc-l #:foo (-val '#:foo))
(tc-l #:foo -Keyword)
(tc-l #f (-val #f))
(tc-l #"foo" -Bytes)
[tc-l () (-val null)]

View File

@ -1,8 +0,0 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (rep type-rep) (utils tc-utils))
(define infer-param (make-parameter (lambda e (int-err "infer not initialized"))))
(define (unify X S T) ((infer-param) X S T (make-Univ) null))
(provide unify infer-param)

View File

@ -1,29 +0,0 @@
#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))

View File

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

View File

@ -1,13 +0,0 @@
#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]))

View File

@ -3,7 +3,6 @@
;; 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
@ -16,12 +15,13 @@
;; these are all for constructing the types given to variables
(require (for-syntax
scheme/base
(env init-envs)
(except-in (rep effect-rep type-rep) make-arr)
"init-envs.ss"
"effect-rep.ss"
(except-in "type-rep.ss" make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"
(typecheck tc-structs)))
"tc-structs.ss"))
(define-for-syntax (initialize-others)
(d-s date
@ -57,9 +57,6 @@
[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
@ -148,13 +145,9 @@
[string-append (->* null -String -String)]
[open-input-string (-> -String -Input-Port)]
[open-output-file
(->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)]
(cl->
[(-Pathlike) -Port]
[(-Pathlike Sym) -Port])]
[read (cl->
[(-Port) -Sexp]
[() -Sexp])]
@ -212,7 +205,9 @@
[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))
@ -251,6 +246,7 @@
(- (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)))]
@ -471,7 +467,7 @@
[(-Bytes N) -Bytes]
[(-Bytes N N) -Bytes])]
[bytes-length (-> -Bytes N)]
[open-input-file (->key -Pathlike #:mode (Un (-val 'binary) (-val 'text)) #f -Input-Port)]
[open-input-file (-> -Pathlike -Input-Port)]
[close-input-port (-> -Input-Port -Void)]
[close-output-port (-> -Output-Port -Void)]
[read-line (cl->
@ -557,11 +553,8 @@
[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))]
[eof (-val eof)]
[read-accept-reader (-Param 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))]
)
(begin-for-syntax

View File

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

View File

@ -1,12 +1,15 @@
#lang scheme/unit
(require (except-in "../utils/utils.ss" extend))
(require syntax/kerncase
scheme/match
"signatures.ss"
(private type-utils type-effect-convenience union subtype)
(utils tc-utils)
(rep type-rep))
"type-utils.ss"
"type-rep.ss" ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"union.ss"
"subtype.ss" ;; has tests
"tc-utils.ss" ;; doesn't need tests
)
(import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-expr^)
(export check-subforms^)
@ -18,7 +21,7 @@
(define body-ty #f)
(define (get-result-ty t)
(match t
[(Function: (list (arr: _ rngs #f _ '() _ _) ...)) (apply Un rngs)]
[(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])

View File

@ -1,7 +1,6 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require (rep type-rep)
(require "type-rep.ss"
scheme/contract)
;; S, T types

View File

@ -1,9 +1,8 @@
#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)
(require "type-effect-convenience.ss" "type-rep.ss"
"type-utils.ss" "union.ss" "tc-utils.ss"
"subtype.ss" "utils.ss"
"signatures.ss" "constraint-structs.ss"
scheme/match)

View File

@ -1,8 +1,6 @@
#lang scheme/unit
(require (except-in "../utils/utils.ss" extend))
(require "signatures.ss" "constraint-structs.ss"
(utils tc-utils)
(require "signatures.ss" "utils.ss" "tc-utils.ss" "constraint-structs.ss"
scheme/match)
(import constraints^)

View File

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

View File

@ -1,8 +1,7 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (for-syntax scheme/base)
(utils tc-utils)
"tc-utils.ss"
mzlib/etc)
;; this file contains support for calculating the free variables/indexes of types
@ -28,8 +27,8 @@
(define var-table (make-weak-hasheq))
;; maps Type to List[Cons[Symbol,Variance]]
(define (free-idxs* t) (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" (syntax-e t)))))
(define (free-vars* t) (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" (syntax-e t)))))
(define (free-idxs* t) (hash-ref index-table t (lambda _ (error "type not in index-table" (syntax-e t)))))
(define (free-vars* t) (hash-ref var-table t (lambda _ (error "type not in var-table" (syntax-e t)))))
(define empty-hash-table (make-immutable-hasheq null))

View File

@ -0,0 +1,7 @@
#lang scheme/base
(require "type-rep.ss")
(define infer-param (make-parameter (lambda e (error 'infer "not initialized"))))
(define (unify X S T) ((infer-param) X S T (make-Univ) null))
(provide unify infer-param)

View File

@ -1,14 +1,12 @@
#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)
(require "type-effect-convenience.ss" "type-rep.ss" "effect-rep.ss" "rep-utils.ss"
"free-variance.ss"
(except-in "type-utils.ss" Dotted)
"union.ss" "tc-utils.ss" "type-name-env.ss"
"subtype.ss" "remove-intersect.ss" "signatures.ss" "utils.ss"
"constraint-structs.ss"
"signatures.ss"
(only-in (env type-environments) lookup current-tvars)
(only-in "type-environments.ss" lookup current-tvars)
scheme/match
mzlib/etc
mzlib/trace
@ -113,15 +111,15 @@
(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))
[((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))
[((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)))]
@ -137,8 +135,8 @@
(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))
[((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))
@ -148,10 +146,10 @@
(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)])
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f 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))
[((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))
@ -161,10 +159,10 @@
(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))])
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f 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))
[((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?
@ -177,8 +175,8 @@
(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))
[((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)]
@ -188,8 +186,8 @@
(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))
[((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))
@ -207,11 +205,11 @@
[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))])
(make-arr (append ss new-tys) s #f (cons s-dty dbound) 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))
[((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))

View File

@ -1,10 +1,9 @@
#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))
"unit-utils.ss")
(provide-signature-elements restrict^ infer^)

View File

@ -1,16 +1,11 @@
#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)
(require "type-env.ss" "type-rep.ss" "type-name-env.ss" "union.ss" "effect-rep.ss"
"type-effect-convenience.ss" "type-alias-env.ss"
"type-alias-env.ss")
(require mzlib/pconvert scheme/match mzlib/shared
(for-template mzlib/pconvert mzlib/shared scheme/base "type-rep.ss" "union.ss" "effect-rep.ss"))
(define (initialize-type-name-env initial-type-names)
(for-each (lambda (nm/ty) (register-resolved-type-alias (car nm/ty) (cadr nm/ty))) initial-type-names))

View File

@ -1,12 +1,6 @@
#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))
(require "type-environments.ss" "tc-utils.ss" "type-env.ss" "mutated-vars.ss" "type-utils.ss" "type-effect-convenience.ss")
(provide (all-defined-out))

View File

@ -14,11 +14,12 @@
;; syntax -> void
(define (fmv/list lstx)
(for-each find-mutated-vars (syntax->list lstx)))
;(when (and (pair? (syntax->datum form))) (printf "called with ~a~n" (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)]
@ -27,13 +28,15 @@
[(begin0 . rest) (fmv/list #'rest)]
[(#%plain-lambda _ . rest) (fmv/list #'rest)]
[(case-lambda (_ . rest) ...) (for-each fmv/list (syntax->list #'(rest ...)))]
[(if . es) (fmv/list #'es)]
[(with-continuation-mark . es) (fmv/list #'es)]
[(if e1 e2) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e2))]
[(if e1 e2 e3) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e1) (find-mutated-vars #'e3))]
[(with-continuation-mark e1 e2 e3) (begin (find-mutated-vars #'e1)
(find-mutated-vars #'e1)
(find-mutated-vars #'e3))]
[(let-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
(fmv/list #'b))]
[(letrec-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
(fmv/list #'b))]
[(#%expression e) (find-mutated-vars #'e)]
(fmv/list #'b))]
;; all the other forms don't have any expression subforms (like #%top)
[_ (void)]))

View File

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

View File

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

View File

@ -1,9 +1,8 @@
#lang scheme/unit
(require "../utils/utils.ss")
(require (rep type-rep)
(private type-effect-convenience union type-utils)
"signatures.ss"
(require "type-effect-convenience.ss" "type-rep.ss"
"type-utils.ss" "union.ss"
"signatures.ss"
scheme/list)
(import)
@ -27,7 +26,7 @@
[#:Param in out
(make-Param (var-demote in V)
(vp out))]
[#:arr dom rng rest drest kws thn els
[#:arr dom rng rest drest thn els
(cond
[(apply V-in? V (append thn els))
(make-arr null (Un) Univ #f null null)]
@ -36,8 +35,6 @@
(vp rng)
(var-demote (car drest) V)
#f
(for/list ([(kw kwt) (in-pairs kws)])
(cons kw (var-demote kwt V)))
thn
els)]
[else
@ -47,8 +44,6 @@
(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)])]))
@ -66,7 +61,7 @@
[#:Param in out
(make-Param (var-promote in V)
(vd out))]
[#:arr dom rng rest drest kws thn els
[#:arr dom rng rest drest thn els
(cond
[(apply V-in? V (append thn els))
(make-arr null (Un) Univ #f null null)]
@ -75,8 +70,6 @@
(vd rng)
(var-promote (car drest) V)
#f
(for/list ([(kw kwt) (in-pairs kws)])
(cons kw (var-promote kwt V)))
thn
els)]
[else
@ -86,7 +79,5 @@
(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)])]))

View File

@ -1,12 +1,11 @@
#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)
"type-contract.ss"
"type-rep.ss"
"tc-utils.ss"
"def-binding.ss")
(require (for-template scheme/base

View File

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

View File

@ -1,18 +1,18 @@
#lang scheme/base
(require "../utils/utils.ss")
(require mzlib/struct
mzlib/plt-match
syntax/boundmap
(utils planet-requires)
"planet-requires.ss"
"free-variance.ss"
"utils.ss"
"interning.ss"
mzlib/etc
(for-syntax
scheme/base
syntax/struct
syntax/stx
(utils utils)))
"utils.ss"))
(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq)
@ -150,9 +150,7 @@
(lambda (s)
(...
(syntax-case s ()
[(__ . fs)
(with-syntax ([flds** (syntax/loc s (_ . fs))])
(quasisyntax/loc s (struct nm flds**)))]))))
[(__ . fs) (quasisyntax/loc s (struct nm #, (syntax/loc #'fs (_ . fs))))]))))
(begin-for-syntax
(hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx)))
intern

View File

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

View File

@ -1,8 +1,8 @@
#lang scheme/unit
(require "../utils/utils.ss")
(require (rep type-rep)
(private type-utils union remove-intersect subtype)
(require "type-rep.ss"
"type-utils.ss" "union.ss"
"subtype.ss" "remove-intersect.ss"
"signatures.ss"
scheme/match)

View File

@ -2,11 +2,41 @@
(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))
;; cycle 2
(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))
(tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t #;check-expr))
(define-signature check-subforms^
(check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check))

View File

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

View File

@ -1,13 +1,19 @@
#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)
"type-rep.ss"
"effect-rep.ss"
"tc-utils.ss"
"subtype.ss"
"infer.ss"
(only-in "utils.ss" debug in-syntax printf/log in-pairs)
"union.ss"
"type-utils.ss"
"type-effect-convenience.ss"
"type-effect-printer.ss"
"type-annotation.ss"
"resolve-type.ss"
"type-environments.ss"
(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
@ -15,7 +21,7 @@
(for-template
"internal-forms.ss" scheme/base
(only-in scheme/private/class-internal make-object do-make-object)))
(require (r:infer constraint-structs))
(require "constraint-structs.ss")
(import tc-expr^ tc-lambda^ tc-dots^)
(export tc-app^)
@ -153,7 +159,7 @@
(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) ...)))
[(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"))
@ -198,7 +204,7 @@
(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))))
[(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))])
@ -208,7 +214,7 @@
(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-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"
@ -253,14 +259,14 @@
(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))))
(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-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"
@ -372,8 +378,8 @@
(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 '() _ _) ...))))
[(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")])
@ -423,8 +429,7 @@
"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))))
[(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
@ -432,7 +437,7 @@
(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)))
[(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*)
@ -448,19 +453,19 @@
;; 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) ...)))
(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) ...))))))
(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) ...)))
(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) ...))))))
(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)))
@ -469,7 +474,7 @@
;; 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) ...)))))
(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))
@ -561,47 +566,6 @@
[(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
@ -621,7 +585,7 @@
[(Values: ts) ts]
[_ (list t)]))
(match prod-t
[(Function: (list (arr: (list) vals _ #f '() _ _)))
[(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"
@ -657,23 +621,11 @@
[(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)])]
[(#%plain-app apply f . args) (tc/apply #'f #'args)]
;; 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)]
(let-loop-check #'form #'lp #'actuals #'args #'body expected)]
;; or/andmap of ... argument
[(#%plain-app or/andmap f arg)
(and

View File

@ -1,11 +1,10 @@
#lang scheme/unit
(require (except-in "../utils/utils.ss" extend))
(require "signatures.ss"
(utils tc-utils)
(env type-environments)
(private type-utils)
(rep type-rep)
"tc-utils.ss"
"type-environments.ss"
"type-utils.ss"
"type-rep.ss"
syntax/kerncase
scheme/match)

View File

@ -1,15 +1,21 @@
#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)
"type-utils.ss"
"utils.ss" ;; doesn't need tests
"type-rep.ss" ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"union.ss"
"subtype.ss" ;; has tests
"parse-type.ss" ;; has tests
"tc-utils.ss" ;; doesn't need tests
"lexical-env.ss" ;; maybe needs tests
"type-annotation.ss" ;; has tests
"effect-rep.ss"
(only-in "type-environments.ss" lookup current-tvars extend-env)
scheme/private/class-internal
(only-in srfi/1 split-at))
@ -35,7 +41,7 @@
[(null? v) (-val null)]
[(symbol? v) (-val v)]
[(string? v) -String]
[(keyword? v) (-val v)]
[(keyword? v) -Keyword]
[(bytes? v) -Bytes]
[(list? v) (-Tuple (map tc-literal v))]
[(vector? v) (make-Vector (types-of-literals (vector->list v)))]
@ -95,8 +101,7 @@
;; 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))]))
[(tc-result: t) t]))
(define (tc-expr/check/t e t)
(match (tc-expr/check e t)

View File

@ -1,15 +1,20 @@
#lang scheme/unit
(require (rename-in "../utils/utils.ss" [infer r:infer]))
(require (utils planet-requires)
(require "planet-requires.ss"
"signatures.ss"
(rep type-rep effect-rep)
(private type-effect-convenience subtype union type-utils type-comparison mutated-vars)
(env lexical-env)
(only-in (private remove-intersect)
"type-rep.ss" ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"lexical-env.ss" ;; maybe needs tests
"effect-rep.ss"
"mutated-vars.ss"
"subtype.ss"
(only-in "remove-intersect.ss"
[remove *remove])
(r:infer infer)
(utils tc-utils)
"infer.ss"
"union.ss"
"type-utils.ss"
"tc-utils.ss"
"type-comparison.ss"
syntax/kerncase
mzlib/trace
mzlib/plt-match)

View File

@ -1,15 +1,20 @@
#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)
(except-in "type-rep.ss" make-arr) ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"type-environments.ss" ;; doesn't need tests
"lexical-env.ss" ;; maybe needs tests
"type-annotation.ss" ;; has tests
(except-in "utils.ss" extend)
"type-utils.ss"
"effect-rep.ss"
"tc-utils.ss"
"union.ss"
mzlib/plt-match
(only-in (private type-effect-convenience) [make-arr* make-arr]))
(only-in "type-effect-convenience.ss" [make-arr* make-arr]))
(require (for-template scheme/base "internal-forms.ss"))
(import tc-expr^)
@ -175,7 +180,7 @@
(let loop ([expected expected])
(match expected
[(Mu: _ _) (loop (unfold expected))]
[(Function: (list (arr: argss rets rests drests '() _ _) ...))
[(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]

View File

@ -1,9 +1,14 @@
#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)
"type-effect-convenience.ss"
"lexical-env.ss"
"type-annotation.ss"
"type-alias-env.ss"
"type-env.ss"
"parse-type.ss"
"utils.ss"
"type-utils.ss"
syntax/free-vars
mzlib/trace
scheme/match

View File

@ -1,12 +1,15 @@
#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)
(require "type-rep.ss" ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"type-env.ss" ;; maybe needs tests
"type-utils.ss"
"parse-type.ss" ;; has tests
"type-environments.ss" ;; doesn't need tests
"type-name-env.ss" ;; maybe needs tests
"union.ss"
"tc-utils.ss"
"resolve-type.ss"
"def-binding.ss"
syntax/kerncase
syntax/struct

View File

@ -1,17 +1,26 @@
#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"
"type-utils.ss"
"utils.ss" ;; doesn't need tests
"type-effect-convenience.ss" ;; maybe needs tests
"internal-forms.ss" ;; doesn't need tests
"type-env.ss" ;; maybe needs tests
"parse-type.ss" ;; has tests
"tc-utils.ss" ;; doesn't need tests
"type-annotation.ss" ;; has tests
"type-name-env.ss" ;; maybe needs tests
"init-envs.ss"
"mutated-vars.ss"
"def-binding.ss"
"provide-handling.ss"
"type-alias-env.ss"
"type-contract.ss"
(for-template
"internal-forms.ss"
mzlib/contract

View File

@ -70,12 +70,12 @@
(unless (null? stxs)
(raise-typecheck-error (format "Summary: ~a errors encountered" (length stxs)) (apply append stxs))))]))
(define delay-errors? (make-parameter #f))
(define delay-errors? (make-parameter #t))
(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*)))
(error "syntax was not syntax" 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)))))

View File

@ -1,8 +1,7 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require syntax/boundmap
(utils tc-utils)
"tc-utils.ss"
mzlib/trace
scheme/match)

View File

@ -1,11 +1,7 @@
#lang scheme/base
(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"
(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"
scheme/match mzlib/trace)
(provide type-annotation
get-type

View File

@ -1,4 +1,3 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (rep type-rep) "type-utils.ss")
(require "type-rep.ss" "type-utils.ss")
(provide type-equal? tc-result-equal? type<? type-compare effects-equal?)

View File

@ -2,14 +2,14 @@
(provide type->contract define/fixup-contract? generate-contract-def change-contract-fixups)
(require (except-in "../utils/utils.ss" extend))
(require
(rep type-rep)
(typecheck internal-forms)
(utils tc-utils)
(env type-name-env)
"type-rep.ss"
"parse-type.ss"
"utils.ss"
"type-name-env.ss"
"require-contract.ss"
"internal-forms.ss"
"tc-utils.ss"
"resolve-type.ss"
"type-utils.ss"
(only-in "type-effect-convenience.ss" Any-Syntax)
@ -80,13 +80,13 @@
(define (f a)
(define-values (dom* rngs* rst)
(match a
[(arr: dom (Values: rngs) #f #f '() _ _)
[(arr: dom (Values: rngs) #f #f _ _)
(values (map t->c dom) (map t->c rngs) #f)]
[(arr: dom rng #f #f '() _ _)
[(arr: dom rng #f #f _ _)
(values (map t->c dom) (list (t->c rng)) #f)]
[(arr: dom (Values: rngs) rst #f '() _ _)
[(arr: dom (Values: rngs) rst #f _ _)
(values (map t->c dom) (map t->c rngs) (t->c rst))]
[(arr: dom rng rst #f '() _ _)
[(arr: dom rng rst #f _ _)
(values (map t->c dom) (list (t->c rng)) (t->c rst))]))
(with-syntax
([(dom* ...) dom*]

View File

@ -1,16 +1,14 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (rep type-rep effect-rep)
(utils tc-utils)
(require "type-rep.ss"
"effect-rep.ss"
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))
@ -35,7 +33,7 @@
[(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
[(True-Effect:) eff]
[(False-Effect:) eff]
[_ (int-err "can't add var ~a to effect ~a" v eff)]))
[_ (error 'internal-tc-error "can't add var to effect ~a" eff)]))
(define-syntax (-> stx)
(syntax-case* stx (:) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
@ -80,26 +78,11 @@
[(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 #f null (list) (list))]
[(dom rng rest) (make-arr dom rng rest #f null (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest #f null eff1 eff2)]
[(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest null eff1 eff2)]
[(dom rng rest drest kws eff1 eff2)
(make-arr dom rng rest drest (sort #:key Keyword-kw kws keyword<?) eff1 eff2)]))
(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)]))
(define (make-arr-dots dom rng dty dbound)
(make-arr* dom rng #f (cons dty dbound) null null))

View File

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

View File

@ -1,9 +1,7 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require syntax/boundmap
(utils tc-utils)
(private type-utils))
"tc-utils.ss" "type-utils.ss")
(provide register-type
finish-register-type

View File

@ -10,9 +10,8 @@
initial-tvar-env
with-dotted-env/extend)
(require (prefix-in r: "../utils/utils.ss"))
(require scheme/match
(r:utils tc-utils))
"tc-utils.ss")
;; eq? has the type of equal?, and l is an alist (with conses!)
(define-struct env (eq? l))

View File

@ -1,10 +1,9 @@
#lang scheme/base
(require "../utils/utils.ss")
(require syntax/boundmap
mzlib/trace
(utils tc-utils)
(private type-utils))
"tc-utils.ss"
"type-utils.ss")
(provide register-type-name
lookup-type-name

View File

@ -1,8 +1,7 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (utils planet-requires tc-utils)
"rep-utils.ss" "effect-rep.ss" "free-variance.ss"
(require "planet-requires.ss" "rep-utils.ss" "effect-rep.ss" "tc-utils.ss"
"free-variance.ss"
mzlib/trace scheme/match
(for-syntax scheme/base))
@ -91,27 +90,16 @@
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)))
(dt arr (dom rng rest drest thn-eff els-eff)
[#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null) dom)))
(match drest
[(cons t (? symbol? bnd))
(list (fix-bound (flip-variances (free-vars* t)) bnd))]
@ -120,9 +108,7 @@
(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)))
(combine-frees (append (map flip-variances (map free-idxs* (append (if rest (list rest) null) dom)))
(match drest
[(cons t (? number? bnd))
(list (fix-bound (flip-variances (free-idxs* t)) bnd))]
@ -135,8 +121,6 @@
(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))])
@ -264,11 +248,9 @@
(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 ty [kw pats ... es] ...)
#;(andmap (lambda (k) (keyword? (syntax-e k))) (syntax->list #'(kw ...)))
(syntax/loc stx (tc rec-id (lambda (e) (sub-eff rec-id e)) ty [kw pats ... es] ...))]
[(tc rec-id e-rec-id ty clauses ...)
(begin
(map add-clause (syntax->list #'(clauses ...)))
@ -314,7 +296,7 @@
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions
[#:arr dom rng rest drest kws thn-eff els-eff
[#:arr dom rng rest drest thn-eff els-eff
(*arr (map sb dom)
(sb rng)
(if rest (sb rest) #f)
@ -322,8 +304,6 @@
(cons (sb (car drest))
(if (eq? (cdr drest) name) (+ count outer) (cdr drest)))
#f)
(for/list ([kw kws])
(cons (car kw) (sb (cdr kw))))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff))]
[#:ValuesDots tys dty dbound
@ -360,7 +340,7 @@
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions
[#:arr dom rng rest drest kws thn-eff els-eff
[#:arr dom rng rest drest thn-eff els-eff
(*arr (map sb dom)
(sb rng)
(if rest (sb rest) #f)
@ -368,8 +348,6 @@
(cons (sb (car drest))
(if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
#f)
(for/list ([kw kws])
(cons (car kw) (sb (cdr kw))))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff))]
[#:ValuesDots tys dty dbound
@ -423,7 +401,7 @@
(match t
[(Poly: n scope)
(unless (= (length names) n)
(int-err "Wrong number of names: expected ~a got ~a" n (length names)))
(error "Wrong number of names"))
(instantiate-many (map *F names) scope)]))
;; the 'smart' constructor
@ -438,7 +416,7 @@
(match t
[(PolyDots: n scope)
(unless (= (length names) n)
(int-err "Wrong number of names: expected ~a got ~a" n (length names)))
(error "Wrong number of names"))
(instantiate-many (map *F names) scope)]))
(print-struct #t)

View File

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

View File

@ -1,7 +1,6 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (utils unit-utils)
(require "unit-utils.ss"
mzlib/trace
(only-in scheme/unit provide-signature-elements)
"signatures.ss" "tc-toplevel.ss"

View File

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

View File

@ -2,7 +2,6 @@
(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
@ -17,40 +16,7 @@
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)
in-syntax)
(define-sequence-syntax in-syntax
(lambda () #'syntax->list)

View File

@ -1,18 +1,22 @@
#lang scheme/base
(require (rename-in "utils/utils.ss" [infer r:infer]))
(require (private base-env base-types)
(require "private/base-env.ss"
"private/base-types.ss"
(for-syntax
scheme/base
(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)
"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"
scheme/nest
syntax/kerncase
scheme/match))
@ -27,7 +31,7 @@
(provide (rename-out [module-begin #%module-begin]
[top-interaction #%top-interaction]
[#%plain-lambda lambda]
[#%app #%app]
[#%plain-app #%app]
[require require]))
(define-for-syntax catch-errors? #f)