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

start removing names

Browse Source 
original commit: df1572231ea34907db23f7c930a19bea7e4e6249
This commit is contained in:
Sam Tobin-Hochstadt 2010-04-19 17:52:10 -04:00
commit b797c59d21
25 changed files with 198 additions and 156 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
collects/tests/typed-scheme/fail/with-type-bug.ss Normal file
View File

@ -0,0 +1,5 @@
#;
(exn-pred exn:fail:contract?)
#lang scheme
(require (prefix-in T: typed/scheme))
((T:with-type #:result (T:Integer T:-> T:Integer) add1) 1/2)

12
collects/tests/typed-scheme/succeed/provide-poly-struct.ss Normal file
View File

@ -0,0 +1,12 @@
#lang scheme/load
(module m typed-scheme
(define-struct: (A) x ([v : A]))
(provide make-x x-v))
(module n scheme
(require 'm)
(x-v (make-x 1)))
(require 'm)
(require 'n)

1
collects/tests/typed-scheme/succeed/sequences.ss
View File

@ -7,3 +7,4 @@
(ann (for ([z (open-input-string "foobar")]) (add1 z)) Void)
(ann (for ([z (in-list (list 1 2 3))]) (add1 z)) Void)
(ann (for ([z (in-vector (vector 1 2 3))]) (add1 z)) Void)

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

@ -112,10 +112,11 @@
[(-values (list -Number)) (-values (list Univ))]
[(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a) null)) . -> . (-lst a)))
((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))) null)) . -> . (-lst (-pair -Number (-v a))))]
[(-poly (a) ((-struct 'bar #f (list -Number a) null) . -> . (-lst a)))
((-struct 'bar #f (list -Number (-pair -Number (-v a))) null) . -> . (-lst (-pair -Number (-v a))))]
[(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a) null #'values)) . -> . (-lst a)))
((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values))
. -> . (-lst (-pair -Number (-v a))))]
[(-poly (a) ((-struct 'bar #f (list -Number a) null #'values) . -> . (-lst a)))
((-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values) . -> . (-lst (-pair -Number (-v a))))]
[(-poly (a) (a . -> . (make-Listof a))) ((-v b) . -> . (make-Listof (-v b)))]
[(-poly (a) (a . -> . (make-Listof a))) ((-pair -Number (-v b)) . -> . (make-Listof (-pair -Number (-v b))))]

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

@ -37,10 +37,14 @@
[(-mu x (Un -Number -Symbol x)) (-mu y (Un -Number -Symbol y))]
;; found bug
[FAIL (Un (-mu heap-node
(-struct 'heap-node #f (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))) null))
(-struct 'heap-node #f
(list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty)))
null #'values))
(-base 'heap-empty))
(Un (-mu heap-node
(-struct 'heap-node #f (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))) null))
(-struct 'heap-node #f
(list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty)))
null #'values))
(-base 'heap-empty))]))
(define-go

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

@ -11,6 +11,8 @@
(rep type-rep filter-rep object-rep)
(rename-in (types utils union convenience abbrev)
[Un t:Un]
[true-lfilter -true-lfilter]
pecheck-tests.ss
[true-filter -true-filter]
[-> t:->])
(utils tc-utils utils)
@ -138,10 +140,10 @@
(tc-e/t 3 -Pos)
(tc-e/t "foo" -String)
(tc-e (+ 3 4) -Pos)
[tc-e/t (lambda: () 3) (t:-> -Pos : -true-filter)]
[tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : -true-filter)]
[tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : -true-filter)]
[tc-e/t (lambda () 3) (t:-> -Pos : -true-filter)]
[tc-e/t (lambda: () 3) (t:-> -Pos : -true-lfilter)]
[tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : -true-lfilter)]
[tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : -true-lfilter)]
[tc-e/t (lambda () 3) (t:-> -Pos : -true-lfilter)]
[tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list -true-filter -true-filter))]
[tc-e (cons 3 4) (-pair -Pos -Pos)]
[tc-e (cons 3 (ann '() : (Listof Integer))) (make-Listof -Integer)]
@ -479,11 +481,12 @@
[tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (number? z))])
(lambda: ([x : Any]) (if (p? x) 11 12)))
(t:-> Univ -Pos : -true-filter)]
(t:-> Univ -Pos : -true-lfilter)]
[tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (number? z))])
(lambda: ([x : Any]) (if (p? x) x 12)))
(make-pred-ty Univ Univ (-val #f) 0 null)]
(t:-> Univ Univ : (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f)))) : (make-LPath null 0))]
; (make-pred-ty Univ Univ (-val #f) 0 null)]
[tc-e/t (let* ([z (ann 1 : Any)]
[p? (lambda: ([x : Any]) (not (number? z)))])
(lambda: ([x : Any]) (if (p? x) x 12)))
@ -491,7 +494,7 @@
[tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) (not (number? z)))])
(lambda: ([x : Any]) (if (p? x) x 12)))
(t:-> Univ -Pos : -true-filter)]
(t:-> Univ -Pos : -true-lfilter)]
[tc-e/t (let* ([z 1]
[p? (lambda: ([x : Any]) z)])
(lambda: ([x : Any]) (if (p? x) x 12)))
@ -660,7 +663,7 @@
;; instantiating dotted terms
[tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer)
(-Integer B -Integer . t:-> . -Pos : -true-filter)]
(-Integer B -Integer . t:-> . -Pos : -true-lfilter)]
[tc-e/t (inst (plambda: (a ...) [xs : (a ... a -> Integer) ... a] 3) Integer Boolean Integer)
((-Integer B -Integer . t:-> . -Integer)
(-Integer B -Integer . t:-> . -Integer)
@ -725,13 +728,13 @@
(lambda: ([y : (a ... a -> Number)])
(apply y zs))
ys)))
(-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))]
(-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-lfilter))]
[tc-e/t (plambda: (a ...) [ys : (a ... a -> Number) *]
(lambda: [zs : a ... a]
(map (lambda: ([y : (a ... a -> Number)])
(apply y zs))
ys)))
(-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))]
(-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-lfilter))]
[tc-e/t (lambda: ((x : (All (t) t)))
((inst (inst x (All (t) (t -> t)))

11
collects/typed-scheme/env/init-envs.ss vendored
View File

@ -1,10 +1,10 @@
#lang scheme/base
(provide (all-defined-out))
(require "../utils/utils.ss")
(require "type-env.ss"
(require "../utils/utils.ss"
"type-env.ss"
"type-name-env.ss"
"type-alias-env.ss"
unstable/struct
(rep type-rep object-rep filter-rep rep-utils)
(for-template (rep type-rep object-rep filter-rep)
(types union)
@ -25,11 +25,12 @@
[(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))]
[(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt))]
[(Name: stx) `(make-Name (quote-syntax ,stx))]
[(Struct: name parent flds proc poly? pred-id cert acc-ids)
[(Struct: name parent flds proc poly? pred-id cert acc-ids maker-id)
`(make-Struct ,(sub name) ,(sub parent)
,(sub flds) ,(sub proc) ,(sub poly?)
(quote-syntax ,pred-id) (syntax-local-certifier)
(list ,@(for/list ([a acc-ids]) `(quote-syntax ,a))))]
(list ,@(for/list ([a acc-ids]) `(quote-syntax ,a)))
(quote-syntax ,maker-id))]
[(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
[(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
[(Refinement: parent pred cert) `(make-Refinement ,(sub parent)

2
collects/typed-scheme/infer/infer-unit.ss
View File

@ -330,7 +330,7 @@
(cg S e)))
(fail! S T))]
[((Struct: nm p flds proc _ _ _ _) (Struct: nm p flds* proc* _ _ _ _))
[((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*))]

18
collects/typed-scheme/module-info.ss Normal file
View File

@ -0,0 +1,18 @@
#lang scheme/base
(require typed-scheme/typed-reader)
(provide module-info configure)
(define ((module-info arg) key default)
(case key
[(configure-runtime) `(#(typed-scheme/module-info configure ()))]
[else default]))
;; options currently always empty
(define (configure options)
(namespace-require 'scheme/base)
(eval '(begin
(require (for-syntax typed-scheme/utils/tc-utils scheme/base))
(begin-for-syntax (set-box! typed-context? #t)))
(current-namespace))
(current-readtable readtable))

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

@ -651,7 +651,9 @@
;; unsafe
[unsafe-vector-ref (-poly (a) ((-vec a) -Nat . -> . a))]
[unsafe-vector*-ref (-poly (a) ((-vec a) -Nat . -> . a))]
[unsafe-vector-length (-poly (a) ((-vec a) . -> . -Nat))]
[unsafe-vector*-length (-poly (a) ((-vec a) . -> . -Nat))]
[unsafe-car (-poly (a b)
(cl->*
(->acc (list (-pair a b)) a (list -car))))]

38
collects/typed-scheme/private/type-contract.ss
View File

@ -160,25 +160,33 @@
#;#'class?
#'(class/c (name fcn-cnt) ... (init [by-name-init by-name-cnt] ...)))]
[(Value: '()) #'null?]
[(Struct: nm par flds proc poly? pred? cert acc-ids)
[(Struct: nm par flds proc poly? pred? cert acc-ids maker-id)
(cond
[(assf (λ (t) (type-equal? t ty)) structs-seen)
=>
(lambda (pr)
(cdr pr))]
cdr]
[proc (exit (fail))]
[poly?
(with-syntax* ([(x rec) (generate-temporaries '(x rec))]
[(fld-cnts ...)
(for/list ([fty flds]
[f-acc acc-ids])
#`(#,(t->c fty #:seen (cons (cons ty #'rec) structs-seen))
(#,f-acc x)))])
#`(flat-rec-contract
rec
'#,(syntax-e pred?)
(lambda (x) (and fld-cnts ...))))]
[else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])]
[poly?
(with-syntax* ([(rec blame val) (generate-temporaries '(rec blame val))]
[maker maker-id]
[cnt-name nm]
[(fld-cnts ...)
(for/list ([fty flds]
[f-acc acc-ids])
#`(((contract-projection
#,(t->c fty #:seen (cons (cons ty #'(recursive-contract rec)) structs-seen)))
blame)
(#,f-acc val)))])
#`(letrec ([rec
(make-contract
#:name 'cnt-name
#:first-order #,pred?
#:projection
(lambda (blame)
(lambda (val)
(maker fld-cnts ...))))])
rec))]
[else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])]
[(Syntax: (Base: 'Symbol _)) #'identifier?]
[(Syntax: t) #`(syntax/c #,(t->c t))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]

62
collects/typed-scheme/rep/filter-rep.ss
View File

@ -14,26 +14,22 @@
'FilterSet
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
(provide Filter/c FilterSet/c)
#;(define LatentFilter/c
(flat-named-contract
'LatentFilter
(λ (e)
(and (LatentFilter? e) (not (LFilterSet? e))))))
(provide Filter/c FilterSet/c); LatentFilter/c LatentFilterSet/c index/c)
(define name-ref/c (or/c identifier? integer?))
(define (hash-name v) (if (identifier? v) (hash-id v) v))
(df Bot () [#:fold-rhs #:base])
(df Top () [#:fold-rhs #:base])
(df TypeFilter ([t Type?] [p (listof PathElem?)] [v identifier?])
[#:intern (list t p (hash-id v))]
(df TypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
[#:intern (list t p (hash-name v))]
[#:frees (combine-frees (map free-vars* (cons t p)))
(combine-frees (map free-idxs* (cons t p)))]
[#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
(df NotTypeFilter ([t Type?] [p (listof PathElem?)] [v identifier?])
[#:intern (list t p (hash-id v))]
(df NotTypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
[#:intern (list t p (hash-name v))]
[#:frees (combine-frees (map free-vars* (cons t p)))
(combine-frees (map free-idxs* (cons t p)))]
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
@ -69,49 +65,5 @@
;; should only be used for parsing type annotations and expected types
(df NoFilter () [#:fold-rhs #:base])
#|
(define index/c (or/c natural-number/c keyword?))
(dlf LBot () [#:fold-rhs #:base])
(dlf LTypeFilter ([t Type?] [p (listof PathElem?)] [idx index/c])
[#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))]
[#:fold-rhs (*LTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
(dlf LNotTypeFilter ([t Type?] [p (listof PathElem?)] [idx index/c])
[#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))]
[#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
;; implication
(dlf LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-listof LatentFilter/c)])
[#:frees (combine-frees (map free-vars* (append a c)))
(combine-frees (map free-idxs* (append a c)))])
(dlf LFilterSet (thn els)
[#:frees (combine-frees (map free-vars* (append thn els)))
(combine-frees (map free-idxs* (append thn els)))]
[#:fold-rhs (*LFilterSet (map latentfilter-rec-id thn) (map latentfilter-rec-id els))]
[#:contract (->d ([t (cond [(ormap LBot? t)
(list/c LBot?)]
[(ormap LBot? e)
(flat-named-contract "e was LBot" (list/c))]
[else (listof LatentFilter/c)])]
[e (cond [(ormap LBot? e)
(list/c LBot?)]
[(ormap LBot? t)
(flat-named-contract "t was LBot" (list/c))]
[else (listof LatentFilter/c)])])
(#:syntax [stx #f])
[result LFilterSet?])])
(define LatentFilterSet/c
(flat-named-contract
'LatentFilterSet
(λ (e) (or (LFilterSet? e)))))
|#
(define (filter-equal? a b) (= (Rep-seq a) (Rep-seq b)))
(provide filter-equal?)

38
collects/typed-scheme/rep/type-rep.ss
View File

@ -150,11 +150,9 @@
[rng (or/c Values? ValuesDots?)]
[rest (or/c #f Type/c)]
[drest (or/c #f (cons/c Type/c (or/c natural-number/c symbol?)))]
[kws (listof Keyword?)]
;; order is: fixed, rest/drest, keywords
[names (listof identifier?)])
[kws (listof Keyword?)])
#:no-provide
[#:intern (list dom rng rest drest kws (map hash-id names))]
[#:intern (list dom rng rest drest kws)]
[#:frees (combine-frees
(append (map (compose flip-variances free-vars*)
(append (if rest (list rest) null)
@ -183,8 +181,7 @@
(type-rec-id rng)
(and rest (type-rec-id rest))
(and drest (cons (type-rec-id (car drest)) (cdr drest)))
(map type-rec-id kws)
names)])
(map type-rec-id kws))])
;; top-arr is the supertype of all function types
(dt top-arr () [#:fold-rhs #:base])
@ -201,7 +198,7 @@
;; name : symbol
;; parent : Struct
;; flds : Listof[Type]
;; flds : Listof[Cons[Type,Bool]] type and mutability
;; proc : Function Type
;; poly? : is this a polymorphic type?
;; pred-id : identifier for the predicate of the struct
@ -209,22 +206,34 @@
(dt Struct ([name symbol?]
[parent (or/c #f Struct? Name?)]
[flds (listof Type/c)]
#;
[flds (listof (cons/c Type/c boolean?))]
[proc (or/c #f Function?)]
[poly? boolean?]
[pred-id identifier?]
[cert procedure?]
[acc-ids (listof identifier?)])
[acc-ids (listof identifier?)]
[maker-id identifier?])
[#: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)))]
[#:frees (combine-frees (map free-vars* (append (if proc (list proc) null)
(if parent (list parent) null)
flds #;(map car flds))))
(combine-frees (map free-idxs* (append (if proc (list proc) null)
(if parent (list parent) null)
flds #;(map car flds))))]
[#:fold-rhs (*Struct name
(and parent (type-rec-id parent))
(map type-rec-id flds)
#;
(for/list ([(t m?) (in-pairs (in-list flds))])
(cons (type-rec-id t) m?))
(and proc (type-rec-id proc))
poly?
pred-id
cert
acc-ids)]
acc-ids
maker-id)]
[#:key #f])
;; A structure type descriptor
@ -401,7 +410,7 @@
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions
[#:arr dom rng rest drest kws names
[#:arr dom rng rest drest kws
(*arr (map sb dom)
(sb rng)
(if rest (sb rest) #f)
@ -447,7 +456,7 @@
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions
[#:arr dom rng rest drest kws names
[#:arr dom rng rest drest kws
(*arr (map sb dom)
(sb rng)
(if rest (sb rest) #f)
@ -455,8 +464,7 @@
(cons (sb (car drest))
(if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
#f)
(map sb kws)
names)]
(map sb kws))]
[#:ValuesDots rs dty dbound
(*ValuesDots (map sb rs)
(sb dty)

10
collects/typed-scheme/scribblings/begin.scrbl
View File

@ -36,22 +36,22 @@ form from @schememodname[scheme]---when porting a program from
@schememodname[scheme] to @schememodname[typed/scheme], uses of
@scheme[define-struct] should be changed to @scheme[define-struct:].
@schemeblock[(: mag (pt -> Real))]
@schemeblock[(: mag (pt -> Number))]
This declares that @scheme[mag] has the type @scheme[(pt -> Real)].
This declares that @scheme[mag] has the type @scheme[(pt -> Number)].
@;{@scheme[mag] must be defined at the top-level of the module containing
the declaration.}
The type @scheme[(pt -> Real)] is a function type, that is, the type
The type @scheme[(pt -> Number)] is a function type, that is, the type
of a procedure. The input type, or domain, is a single argument of
type @scheme[pt], which refers to an instance of the @scheme[pt]
structure. The @scheme[->] both indicates that this is a function
type and separates the domain from the range, or output type, in this
case @scheme[Real].
case @scheme[Number].
@schemeblock[
(define (mag p)
(sqrt (sqr (pt-x p)) (sqr (pt-y p))))
(sqrt (+ (sqr (pt-x p)) (sqr (pt-y p)))))
]
This definition is unchanged from the untyped version of the code.

6
collects/typed-scheme/scribblings/quick.scrbl
View File

@ -28,9 +28,9 @@ language:
typed/scheme
(define-struct: pt ([x : Real] [y : Real]))
(: mag (pt -> Real))
(: mag (pt -> Number))
(define (mag p)
(sqrt (sqr (pt-x p)) (sqr (pt-y p))))
(sqrt (+ (sqr (pt-x p)) (sqr (pt-y p)))))
]
)
@ -40,7 +40,7 @@ scheme
(code:contract mag : pt -> number)
(define (mag p)
(sqrt (sqr (pt-x p)) (sqr (pt-y p))))
(sqrt (+ (sqr (pt-x p)) (sqr (pt-y p)))))
]
Here is the same program, in @schememodname[typed/scheme]:

2
collects/typed-scheme/typecheck/tc-app.ss
View File

@ -696,7 +696,7 @@
(lambda (dom rng rest a) (infer/vararg vars argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected))))
t argtys expected)]
;; procedural structs
[((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _))) _)
[((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _ _))) _)
(tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) (ret proc-ty) (cons ftype0 argtys) expected)]
;; parameters are functions too
[((tc-result1: (Param: in out)) (list)) (ret out)]

13
collects/typed-scheme/typecheck/tc-envops.ss
View File

@ -11,7 +11,7 @@
(types resolve)
(only-in (env type-environments lexical-env) env? update-type/lexical env-map env-props replace-props)
scheme/contract scheme/match
mzlib/trace unstable/debug
mzlib/trace unstable/debug unstable/struct
(typecheck tc-metafunctions)
(for-syntax scheme/base))
@ -42,12 +42,15 @@
(make-Syntax (update t (make-NotTypeFilter u rst x)))]
;; struct ops
[((Struct: nm par flds proc poly pred cert acc-ids)
[((Struct: nm par flds proc poly pred cert acc-ids maker-id)
(TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-TypeFilter u rst x)))) proc poly pred cert acc-ids)]
[((Struct: nm par flds proc poly pred cert acc-ids)
(make-Struct nm par
(replace-nth flds idx
(lambda (e) (update e (make-TypeFilter u rst x))))
proc poly pred cert acc-ids maker-id)]
[((Struct: nm par flds proc poly pred cert acc-ids maker-id)
(NotTypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert acc-ids)]
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert acc-ids maker-id)]
;; otherwise
[(t (TypeFilter: u (list) _))

4
collects/typed-scheme/typecheck/tc-structs.ss
View File

@ -76,7 +76,7 @@
;; Option[Struct-Ty] -> Listof[Type]
(define (get-parent-flds p)
(match p
[(Struct: _ _ flds _ _ _ _ _) flds]
[(Struct: _ _ flds _ _ _ _ _ _) flds]
[(Name: n) (get-parent-flds (lookup-type-name n))]
[#f null]))
@ -99,7 +99,7 @@
(define-values (struct-type-id 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) getters)]
[sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier) getters (or maker* maker))]
[external-fld-types/no-parent types]
[external-fld-types fld-types])
(if type-only

2
collects/typed-scheme/typed-reader.ss
View File

@ -83,4 +83,4 @@
(parameterize ([current-readtable readtable])
(read-syntax src port)))
(provide (rename-out [*read read] [*read-syntax read-syntax]))
(provide readtable (rename-out [*read read] [*read-syntax read-syntax]))

8
collects/typed-scheme/types/abbrev.ss
View File

@ -76,7 +76,7 @@
(define make-promise-ty
(let ([s (string->uninterned-symbol "Promise")])
(lambda (t)
(make-Struct s #f (list t) #f #f #'promise? values (list #'values)))))
(make-Struct s #f (list t) #f #f #'promise? values (list #'values) #'values))))
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
@ -271,8 +271,8 @@
(define (make-arr-dots dom rng dty dbound)
(make-arr* dom rng #:drest (cons dty dbound)))
(define (-struct name parent flds accs [proc #f] [poly #f] [pred #'dummy] [cert values])
(make-Struct name parent flds proc poly pred cert accs))
(define (-struct name parent flds accs constructor [proc #f] [poly #f] [pred #'dummy] [cert values])
(make-Struct name parent flds proc poly pred cert accs constructor))
(d/c (-filter t i [p null])
(c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c)
@ -362,6 +362,8 @@
(define true-filter (-FS -top -bot))
(define false-filter (-FS -bot -top))
(define true-lfilter (-FS -top -bot))
(define false-lfilter (-FS -bot -top))
(define (opt-fn args opt-args result)
(apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])

4
collects/typed-scheme/types/printer.ss
View File

@ -145,8 +145,8 @@
(fp "~a" (cons 'List (tuple-elems t)))]
[(Base: n cnt) (fp "~a" n)]
[(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))]
[(Struct: 'Promise par (list fld) proc _ _ _ _) (fp "(Promise ~a)" fld)]
[(Struct: nm par flds proc _ _ _ _)
[(Struct: 'Promise par (list fld) proc _ _ _ _ _) (fp "(Promise ~a)" fld)]
[(Struct: nm par flds proc _ _ _ _ _)
(fp "#(struct:~a ~a" nm flds)
(when proc
(fp " ~a" proc))

16
collects/typed-scheme/types/remove-intersect.ss
View File

@ -50,18 +50,18 @@
[(or (list (Pair: _ _) _)
(list _ (Pair: _ _)))
#f]
[(or (list (Value: '()) (Struct: n _ flds _ _ _ _ _))
(list (Struct: n _ flds _ _ _ _ _) (Value: '())))
[(or (list (Value: '()) (Struct: n _ flds _ _ _ _ _ _))
(list (Struct: n _ flds _ _ _ _ _ _) (Value: '())))
#f]
[(list (Struct: n _ flds _ _ _ _ _)
(Struct: n _ flds* _ _ _ _ _))
[(list (Struct: n _ flds _ _ _ _ _ _)
(Struct: n _ flds* _ _ _ _ _ _))
(for/and ([f flds] [f* flds*]) (overlap f f*))]
;; n and n* must be different, so there's no overlap
[(list (Struct: n #f flds _ _ _ _ _)
(Struct: n* #f flds* _ _ _ _ _))
[(list (Struct: n #f flds _ _ _ _ _ _)
(Struct: n* #f flds* _ _ _ _ _ _))
#f]
[(list (Struct: n p flds _ _ _ _ _)
(Struct: n* p* flds* _ _ _ _ _))
[(list (Struct: n p flds _ _ _ _ _ _)
(Struct: n* p* flds* _ _ _ _ _ _))
(and (= (length flds) (length flds*)) (for/and ([f flds] [f* flds*]) (overlap f f*)))]
[else #t])])))

40
collects/typed-scheme/types/subtype.ss
View File

@ -5,7 +5,7 @@
(types utils comparison resolve abbrev)
(env type-name-env)
(only-in (infer infer-dummy) unify)
scheme/match unstable/match unstable/debug
scheme/match unstable/match
mzlib/trace (rename-in scheme/contract
[-> c->]
[->* c->*])
@ -186,10 +186,11 @@
(match arrs
[(list (and a1 (arr: dom1 rng1 #f #f '() names)) (arr: dom rng #f #f '()) ...)
(cond
[(null? dom) a1]
[(not (apply = (length dom1) (map length dom))) #f]
[(not (foldl type-equal? rng1 rng)) #f]
[else (make-arr (apply map (lambda args (make-Union (sort args type<?))) (cons dom1 dom)) rng1 #f #f '() names)])]
[(null? dom) (make-arr dom1 rng1 #f #f '() names)]
[(not (apply = (length dom1) (map length dom))) #f]
[(not (for/and ([rng2 (in-list rng)]) (type-equal? rng1 rng2)))
#f]
[else (make-arr (apply map (lambda args (make-Union (sort args type<?))) (cons dom1 dom)) rng1 #f #f '() names)])]
[_ #f]))
@ -198,7 +199,8 @@
;; potentially raises exn:subtype, when the algorithm fails
;; is s a subtype of t, taking into account constraints A
(define (subtype* A s t)
(parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))]
(define =t (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b))))
(parameterize ([match-equality-test =t]
[current-seen A])
(let ([ks (Type-key s)] [kt (Type-key t)])
(cond
@ -223,26 +225,26 @@
[((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
;; now we encode the numeric hierarchy - bletch
[((Base: 'Integer _) (Base: 'Number _)) A0]
[((Base: 'Flonum _) (== -Real type-equal?)) A0]
[((Base: 'Integer _) (== -Real type-equal?)) A0]
[((Base: 'Flonum _) (== -Real =t)) A0]
[((Base: 'Integer _) (== -Real =t)) A0]
[((Base: 'Flonum _) (Base: 'Number _)) A0]
[((Base: 'Exact-Rational _) (Base: 'Number _)) A0]
[((Base: 'Integer _) (Base: 'Exact-Rational _)) A0]
[((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0]
[((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0]
[((Base: 'Exact-Positive-Integer _) (== -Nat type-equal?)) A0]
[((Base: 'Exact-Positive-Integer _) (== -Nat =t)) A0]
[((Base: 'Exact-Positive-Integer _) (Base: 'Integer _)) A0]
[((== -Nat type-equal?) (Base: 'Number _)) A0]
[((== -Nat type-equal?) (Base: 'Exact-Rational _)) A0]
[((== -Nat type-equal?) (Base: 'Integer _)) A0]
[((== -Nat =t) (Base: 'Number _)) A0]
[((== -Nat =t) (Base: 'Exact-Rational _)) A0]
[((== -Nat =t) (Base: 'Integer _)) A0]
;; values are subtypes of their "type"
[((Value: (? exact-integer? n)) (Base: 'Integer _)) A0]
[((Value: (and n (? number?) (? exact?) (? rational?))) (Base: 'Exact-Rational _)) A0]
[((Value: (? exact-nonnegative-integer? n)) (== -Nat type-equal?)) A0]
[((Value: (? exact-nonnegative-integer? n)) (== -Nat =t)) A0]
[((Value: (? exact-positive-integer? n)) (Base: 'Exact-Positive-Integer _)) A0]
[((Value: (? inexact-real? n)) (Base: 'Flonum _)) A0]
[((Value: (? real? n)) (== -Real type-equal?)) A0]
[((Value: (? real? n)) (== -Real =t)) A0]
[((Value: (? number? n)) (Base: 'Number _)) A0]
[((Value: (? keyword?)) (Base: 'Keyword _)) A0]
@ -304,22 +306,22 @@
[(s (Union: es)) (or (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)
(fail! s t))]
;; subtyping on immutable structs is covariant
[((Struct: nm _ flds #f _ _ _ _) (Struct: nm _ flds* #f _ _ _ _))
[((Struct: nm _ flds #f _ _ _ _ _) (Struct: nm _ flds* #f _ _ _ _ _))
(subtypes* A0 flds flds*)]
[((Struct: nm _ flds proc _ _ _ _) (Struct: nm _ flds* proc* _ _ _ _))
[((Struct: nm _ flds proc _ _ _ _ _) (Struct: nm _ flds* proc* _ _ _ _ _))
(subtypes* A0 (cons proc flds) (cons proc* flds*))]
[((Struct: _ _ _ _ _ _ _ _) (StructTop: (? (lambda (s2) (type-equal? s2 s)))))
[((Struct: _ _ _ _ _ _ _ _ _) (StructTop: (? (lambda (s2) (type-equal? s2 s)))))
A0]
[((Box: _) (BoxTop:)) A0]
[((Vector: _) (VectorTop:)) A0]
[((MPair: _ _) (MPairTop:)) A0]
[((Hashtable: _ _) (HashtableTop:)) A0]
;; subtyping on structs follows the declared hierarchy
[((Struct: nm (? Type? parent) flds proc _ _ _ _) other)
[((Struct: nm (? Type? parent) flds proc _ _ _ _ _) other)
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
(subtype* A0 parent other)]
;; Promises are covariant
[((Struct: 'Promise _ (list t) _ _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _ _)) (subtype* A0 t t*)]
[((Struct: 'Promise _ (list t) _ _ _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _ _ _)) (subtype* A0 t t*)]
;; subtyping on values is pointwise
[((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
;; trivial case for Result

10
collects/typed/scheme/base/lang/reader.ss
View File

@ -4,5 +4,15 @@ typed/scheme/base
#:read r:read
#:read-syntax r:read-syntax
#:info make-info
#:module-info make-module-info
(define (make-info key default use-default)
(case key
[else (use-default key default)]))
(define make-module-info
`#(typed-scheme/module-info module-info ()))
(require (prefix-in r: typed-scheme/typed-reader))

10
collects/typed/scheme/lang/reader.ss
View File

@ -4,5 +4,15 @@ typed/scheme
#:read r:read
#:read-syntax r:read-syntax
#:info make-info
#:module-info make-module-info
(define (make-info key default use-default)
(case key
[else (use-default key default)]))
(define make-module-info
`#(typed-scheme/module-info module-info ()))
(require (prefix-in r: typed-scheme/typed-reader))