a new branch of the whole tree
svn: r18648 original commit: d4e0c16d55c167dbef9eefac8b4820fbada0f6b1
This commit is contained in:
Sam Tobin-Hochstadt
parent
8e2865524c
commit
af7254875a
|
|
@ -9,8 +9,9 @@
|
|||
base-env-indexing)
|
||||
(typecheck typechecker)
|
||||
(rep type-rep filter-rep object-rep)
|
||||
(rename-in (types utils union convenience)
|
||||
(rename-in (types utils union convenience abbrev)
|
||||
[Un t:Un]
|
||||
[true-filter -true-filter]
|
||||
[-> t:->])
|
||||
(utils tc-utils utils)
|
||||
unstable/mutated-vars
|
||||
|
|
@ -137,11 +138,11 @@
|
|||
(tc-e/t 3 -Pos)
|
||||
(tc-e/t "foo" -String)
|
||||
(tc-e (+ 3 4) -Pos)
|
||||
[tc-e/t (lambda: () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))]
|
||||
[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 (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)]
|
||||
[tc-e (void) -Void]
|
||||
|
|
@ -474,15 +475,15 @@
|
|||
(t:-> Univ N)]
|
||||
[tc-e/t (let ([p? (lambda: ([x : Any]) (not (number? x)))])
|
||||
(lambda: ([x : Any]) (if (p? x) 12 (add1 x))))
|
||||
(t:-> Univ N : (-LFS null (list (make-LTypeFilter -Number null 0))))]
|
||||
(t:-> Univ N : (-FS -top (-filter -Number #'x)))]
|
||||
[tc-e/t (let* ([z 1]
|
||||
[p? (lambda: ([x : Any]) (number? z))])
|
||||
(lambda: ([x : Any]) (if (p? x) 11 12)))
|
||||
(t:-> Univ -Pos : (-LFS null (list (make-LBot))))]
|
||||
(t:-> Univ -Pos : -true-filter)]
|
||||
[tc-e/t (let* ([z 1]
|
||||
[p? (lambda: ([x : Any]) (number? z))])
|
||||
(lambda: ([x : Any]) (if (p? x) x 12)))
|
||||
(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)))
|
||||
|
|
@ -490,7 +491,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 : (-LFS null (list (make-LBot))))]
|
||||
(t:-> Univ -Pos : -true-filter)]
|
||||
[tc-e/t (let* ([z 1]
|
||||
[p? (lambda: ([x : Any]) z)])
|
||||
(lambda: ([x : Any]) (if (p? x) x 12)))
|
||||
|
|
@ -650,19 +651,21 @@
|
|||
;; instantiating non-dotted terms
|
||||
[tc-e/t (inst (plambda: (a) ([x : a]) x) Integer)
|
||||
(make-Function (list (make-arr* (list -Integer) -Integer
|
||||
#:filters (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f))))
|
||||
#:object (make-LPath null 0))))]
|
||||
#:names (list #'x)
|
||||
#:filters (-FS (-not-filter (-val #f) #'x)
|
||||
(-filter (-val #f) #'x))
|
||||
#:object (make-Path null #'x))))]
|
||||
[tc-e/t (inst (plambda: (a) [x : a *] (apply list x)) Integer)
|
||||
((list) -Integer . ->* . (-lst -Integer))]
|
||||
|
||||
;; instantiating dotted terms
|
||||
[tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer)
|
||||
(-Integer B -Integer . t:-> . -Pos : (-LFS null (list (make-LBot))))]
|
||||
(-Integer B -Integer . t:-> . -Pos : -true-filter)]
|
||||
[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)
|
||||
(-Integer B -Integer . t:-> . -Integer)
|
||||
. t:-> . -Pos : (-LFS null (list (make-LBot))))]
|
||||
. t:-> . -Pos : -true-filter)]
|
||||
|
||||
[tc-e/t (plambda: (z x y ...) () (inst map z x y ... y))
|
||||
(-polydots (z x y) (t:-> (cl->*
|
||||
|
|
@ -722,13 +725,13 @@
|
|||
(lambda: ([y : (a ... a -> Number)])
|
||||
(apply y zs))
|
||||
ys)))
|
||||
(-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : (-LFS null (list (make-LBot)))))]
|
||||
(-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))]
|
||||
[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)) : (-LFS null (list (make-LBot)))))]
|
||||
(-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))]
|
||||
|
||||
[tc-e/t (lambda: ((x : (All (t) t)))
|
||||
((inst (inst x (All (t) (t -> t)))
|
||||
|
|
@ -779,16 +782,16 @@
|
|||
[user : Number]
|
||||
[gc : Number])
|
||||
'whatever))
|
||||
#:ret (ret (-val 'whatever) (-FS (list) (list (make-Bot))))]
|
||||
#:ret (ret (-val 'whatever) -true-filter)]
|
||||
[tc-e (let: ([l : (Listof Any) (list 1 2 3)])
|
||||
(if (andmap number? l)
|
||||
(+ 1 (car l))
|
||||
7))
|
||||
-Number]
|
||||
(tc-e (or (string->number "7") 7)
|
||||
#:ret (ret -Number (-FS (list) (list (make-Bot)))))
|
||||
#:ret (ret -Number -true-filter))
|
||||
[tc-e (let ([x 1]) (if x x (add1 x)))
|
||||
#:ret (ret -Pos (-FS (list) (list (make-Bot))))]
|
||||
#:ret (ret -Pos -true-filter)]
|
||||
[tc-e (let: ([x : (U (Vectorof Number) String) (vector 1 2 3)])
|
||||
(if (vector? x) (vector-ref x 0) (string-length x)))
|
||||
-Number]
|
||||
|
|
|
|||
13
collects/typed-scheme/env/init-envs.ss
vendored
13
collects/typed-scheme/env/init-envs.ss
vendored
|
|
@ -38,8 +38,17 @@
|
|||
[(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))]
|
||||
[(? (lambda (e) (or (LatentFilter? e)
|
||||
(LatentObject? e)
|
||||
[(arr: dom rng rest drest kws names)
|
||||
`(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws)
|
||||
(list ,@(for/list ([i names]) `(quote-syntax ,i))))]
|
||||
[(TypeFilter: t p i)
|
||||
`(make-TypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))]
|
||||
[(NotTypeFilter: t p i)
|
||||
`(make-NotTypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))]
|
||||
[(Path: p i)
|
||||
`(make-Path ,(sub p) (quote-syntax ,i))]
|
||||
[(? (lambda (e) (or (Filter? e)
|
||||
(Object? e)
|
||||
(PathElem? e)))
|
||||
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
|
||||
`(,(gen-constructor tag) ,@(map sub vals))]
|
||||
|
|
|
|||
2
collects/typed-scheme/env/lexical-env.ss
vendored
2
collects/typed-scheme/env/lexical-env.ss
vendored
|
|
@ -4,7 +4,7 @@
|
|||
"type-environments.ss"
|
||||
"type-env.ss"
|
||||
unstable/mutated-vars
|
||||
(only-in scheme/contract ->* -> or/c any/c)
|
||||
(only-in scheme/contract ->* -> or/c any/c listof cons/c)
|
||||
(utils tc-utils)
|
||||
(only-in (rep type-rep) Type/c)
|
||||
(typecheck tc-metafunctions)
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
|
||||
(require scheme/contract
|
||||
(prefix-in r: "../utils/utils.ss")
|
||||
scheme/match (r:rep filter-rep rep-utils) unstable/struct
|
||||
scheme/match (r:rep filter-rep rep-utils type-rep) unstable/struct
|
||||
(except-in (r:utils tc-utils) make-env)
|
||||
(r:typecheck tc-metafunctions))
|
||||
|
||||
|
|
@ -49,7 +49,7 @@
|
|||
;; the environment for types of ... variables
|
||||
(define dotted-env (make-parameter (make-empty-env free-identifier=?)))
|
||||
|
||||
(define/contract (env-map f e)
|
||||
(r:d/c (env-map f e)
|
||||
((pair? . -> . pair?) env? . -> . env?)
|
||||
(make env (env-eq? e) (map f (env-l e)) (env-props e)))
|
||||
|
||||
|
|
@ -95,4 +95,4 @@
|
|||
(syntax-rules ()
|
||||
[(_ i t v . b) (parameterize ([dotted-env (extend/values (list i) (list (cons t v)) (dotted-env))]) . b)]))
|
||||
|
||||
(provide/contract [make-empty-env ((-> any/c any/c any/c) . -> . env?)])
|
||||
(r:p/c [make-empty-env ((-> any/c any/c any/c) . -> . env?)])
|
||||
|
|
|
|||
|
|
@ -1,14 +1,17 @@
|
|||
#lang scheme/unit
|
||||
|
||||
(require "../utils/utils.ss"
|
||||
(rep free-variance type-rep filter-rep rep-utils)
|
||||
(types convenience union subtype remove-intersect resolve)
|
||||
(except-in (utils tc-utils) make-env)
|
||||
(env type-name-env)
|
||||
(except-in (types utils) Dotted)
|
||||
(require scheme/require
|
||||
(except-in
|
||||
(path-up
|
||||
"utils/utils.ss" "utils/tc-utils.ss"
|
||||
"rep/free-variance.ss" "rep/type-rep.ss" "rep/filter-rep.ss" "rep/rep-utils.ss"
|
||||
"types/convenience.ss" "types/union.ss" "types/subtype.ss" "types/remove-intersect.ss" "types/resolve.ss"
|
||||
"env/type-name-env.ss")
|
||||
make-env)
|
||||
(except-in (path-up "types/utils.ss") Dotted)
|
||||
(only-in (path-up "env/type-environments.ss") lookup current-tvars)
|
||||
"constraint-structs.ss"
|
||||
"signatures.ss"
|
||||
(only-in (env type-environments) lookup current-tvars)
|
||||
"signatures.ss"
|
||||
scheme/match
|
||||
mzlib/etc
|
||||
mzlib/trace
|
||||
|
|
@ -101,11 +104,13 @@
|
|||
(define (cgen/filter V X t s)
|
||||
(match* (t s)
|
||||
[(e e) (empty-cset X)]
|
||||
;; FIXME - is there something to be said about LBot?
|
||||
[((LTypeFilter: t p i) (LTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))]
|
||||
[((LNotTypeFilter: t p i) (LNotTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))]
|
||||
[(e (Top:)) (empty-cset X)]
|
||||
;; FIXME - is there something to be said about the logical ones?
|
||||
[((TypeFilter: t p i) (TypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))]
|
||||
[((NotTypeFilter: t p i) (NotTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))]
|
||||
[(_ _) (fail! t s)]))
|
||||
|
||||
#;
|
||||
(define (cgen/filters V X ts ss)
|
||||
(cond
|
||||
[(null? ss) (empty-cset X)]
|
||||
|
|
@ -119,14 +124,14 @@
|
|||
(define (cgen/filter-set V X t s)
|
||||
(match* (t s)
|
||||
[(e e) (empty-cset X)]
|
||||
[((LFilterSet: t+ t-) (LFilterSet: s+ s-))
|
||||
(cset-meet (cgen/filters V X t+ s+) (cgen/filters V X t- s-))]
|
||||
[((FilterSet: t+ t-) (FilterSet: s+ s-))
|
||||
(cset-meet (cgen/filter V X t+ s+) (cgen/filter V X t- s-))]
|
||||
[(_ _) (fail! t s)]))
|
||||
|
||||
(define (cgen/object V X t s)
|
||||
(match* (t s)
|
||||
[(e e) (empty-cset X)]
|
||||
[(e (LEmpty:)) (empty-cset X)]
|
||||
[(e (Empty:)) (empty-cset X)]
|
||||
;; FIXME - do something here
|
||||
[(_ _) (fail! t s)]))
|
||||
|
||||
|
|
@ -153,8 +158,8 @@
|
|||
[ret-mapping (cg t s)])
|
||||
(cset-meet*
|
||||
(list arg-mapping ret-mapping)))]
|
||||
[((arr: ts t #f (cons dty dbound) '())
|
||||
(arr: ss s #f #f '()))
|
||||
[((arr: ts t #f (cons dty dbound) '() names)
|
||||
(arr: ss s #f #f '() names*))
|
||||
(unless (memq dbound X)
|
||||
(fail! S T))
|
||||
(unless (<= (length ts) (length ss))
|
||||
|
|
@ -164,10 +169,11 @@
|
|||
(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) s-arr)])
|
||||
[new-names (generate-temporaries new-tys)]
|
||||
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null (append names new-names)) s-arr)])
|
||||
(move-vars-to-dmap new-cset dbound vars))]
|
||||
[((arr: ts t #f #f '())
|
||||
(arr: ss s #f (cons dty dbound) '()))
|
||||
(arr: ss s #f (cons dty dbound) '() names*))
|
||||
(unless (memq dbound X)
|
||||
(fail! S T))
|
||||
(unless (<= (length ss) (length ts))
|
||||
|
|
@ -177,7 +183,8 @@
|
|||
(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))])
|
||||
[new-names (generate-temporaries new-tys)]
|
||||
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null (append names* new-names)))])
|
||||
(move-vars-to-dmap new-cset dbound vars))]
|
||||
[((arr: ts t #f (cons t-dty dbound) '())
|
||||
(arr: ss s #f (cons s-dty dbound) '()))
|
||||
|
|
@ -201,7 +208,7 @@
|
|||
(cset-meet*
|
||||
(list arg-mapping darg-mapping ret-mapping)))]
|
||||
[((arr: ts t t-rest #f '())
|
||||
(arr: ss s #f (cons s-dty dbound) '()))
|
||||
(arr: ss s #f (cons s-dty dbound) '() names*))
|
||||
(unless (memq dbound X)
|
||||
(fail! S T))
|
||||
(if (<= (length ts) (length ss))
|
||||
|
|
@ -216,8 +223,9 @@
|
|||
(gensym dbound))]
|
||||
[new-tys (for/list ([var vars])
|
||||
(substitute (make-F var) dbound s-dty))]
|
||||
[new-names (generate-temporaries new-tys)]
|
||||
[new-cset (cgen/arr V (append vars X) t-arr
|
||||
(make-arr (append ss new-tys) s #f (cons s-dty dbound) null))])
|
||||
(make-arr (append ss new-tys) s #f (cons s-dty dbound) null (append names* new-names)))])
|
||||
(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) '())
|
||||
|
|
@ -506,4 +514,4 @@
|
|||
(define (i s t r)
|
||||
(infer/simple (list s) (list t) r))
|
||||
|
||||
;(trace subst-gen cgen)
|
||||
;(trace cgen cgen/arr)
|
||||
|
|
|
|||
|
|
@ -30,9 +30,9 @@
|
|||
Univ
|
||||
(make-Hashtable (vp k) v))]
|
||||
[#:Param in out
|
||||
(make-Param (var-demote in V)
|
||||
(vp out))]
|
||||
[#:arr dom rng rest drest kws
|
||||
(make-Param (var-demote in V)
|
||||
(vp out))]
|
||||
[#:arr dom rng rest drest kws names
|
||||
(cond
|
||||
[(apply V-in? V (get-filters rng))
|
||||
(make-top-arr)]
|
||||
|
|
@ -41,7 +41,8 @@
|
|||
(vp rng)
|
||||
(var-demote (car drest) V)
|
||||
#f
|
||||
(for/list ([k kws]) (var-demote k V)))]
|
||||
(for/list ([k kws]) (var-demote k V))
|
||||
names)]
|
||||
[else
|
||||
(make-arr (for/list ([d dom]) (var-demote d V))
|
||||
(vp rng)
|
||||
|
|
@ -49,7 +50,8 @@
|
|||
(and drest
|
||||
(cons (var-demote (car drest) V)
|
||||
(cdr drest)))
|
||||
(for/list ([k kws]) (var-demote k V)))])]))
|
||||
(for/list ([k kws]) (var-demote k V))
|
||||
names)])]))
|
||||
|
||||
(define (var-demote T V)
|
||||
(define (vd t) (var-demote t V))
|
||||
|
|
@ -63,9 +65,9 @@
|
|||
(Un)
|
||||
(make-Hashtable (vd k) v))]
|
||||
[#:Param in out
|
||||
(make-Param (var-promote in V)
|
||||
(vd out))]
|
||||
[#:arr dom rng rest drest kws
|
||||
(make-Param (var-promote in V)
|
||||
(vd out))]
|
||||
[#:arr dom rng rest drest kws names
|
||||
(cond
|
||||
[(apply V-in? V (get-filters rng))
|
||||
(make-top-arr)]
|
||||
|
|
@ -74,7 +76,8 @@
|
|||
(vd rng)
|
||||
(var-promote (car drest) V)
|
||||
#f
|
||||
(for/list ([k kws]) (var-demote k V)))]
|
||||
(for/list ([k kws]) (var-demote k V))
|
||||
names)]
|
||||
[else
|
||||
(make-arr (for/list ([d dom]) (var-promote d V))
|
||||
(vd rng)
|
||||
|
|
@ -82,4 +85,5 @@
|
|||
(and drest
|
||||
(cons (var-promote (car drest) V)
|
||||
(cdr drest)))
|
||||
(for/list ([k kws]) (var-demote k V)))])]))
|
||||
(for/list ([k kws]) (var-demote k V))
|
||||
names)])]))
|
||||
|
|
|
|||
|
|
@ -8,6 +8,7 @@
|
|||
(all-defined-out)
|
||||
(all-from-out "private/prims.ss"))
|
||||
|
||||
|
||||
(define-syntax (require/typed stx)
|
||||
(define-syntax-class opt-rename
|
||||
#:attributes (nm spec)
|
||||
|
|
|
|||
|
|
@ -41,15 +41,16 @@
|
|||
;; numeric predicates
|
||||
[zero? (make-pred-ty (list N) B -Zero)]
|
||||
[number? (make-pred-ty N)]
|
||||
[integer? (Univ . -> . B : (-LFS (list (-filter (Un -Integer -Flonum))) (list (-not-filter -Integer))))]
|
||||
[integer? (asym-pred (x) Univ B (-FS (-filter (Un -Integer -Flonum) x)
|
||||
(-not-filter -Integer x)))]
|
||||
[exact-integer? (make-pred-ty -Integer)]
|
||||
[real? (make-pred-ty -Real)]
|
||||
[inexact-real? (make-pred-ty -Flonum)]
|
||||
[complex? (make-pred-ty N)]
|
||||
[rational? (make-pred-ty -Real)]
|
||||
[exact? (N . -> . B : (-LFS (list) (list (-not-filter -ExactRational))))]
|
||||
[inexact? (N . -> . B : (-LFS (list) (list (-not-filter -Flonum))))]
|
||||
[fixnum? (Univ . -> . B : (-LFS (list (-filter -Integer)) null))]
|
||||
[exact? (asym-pred (x) N B (-FS -top (-not-filter -ExactRational x)))]
|
||||
[inexact? (asym-pred (x) N B (-FS -top (-not-filter -Flonum x)))]
|
||||
[fixnum? (asym-pred (x) Univ B (-FS (-filter -Integer x) -top))]
|
||||
[positive? (-> -Real B)]
|
||||
[negative? (-> -Real B)]
|
||||
[exact-positive-integer? (make-pred-ty -Pos)]
|
||||
|
|
@ -185,7 +186,6 @@
|
|||
[unsafe-fllog fl-unop]
|
||||
[unsafe-flexp fl-unop]
|
||||
[unsafe-flsqrt fl-unop]
|
||||
[unsafe-fx->fl (-Integer . -> . -Flonum)]
|
||||
|
||||
[unsafe-fx+ fx-op]
|
||||
[unsafe-fx- fx-intop]
|
||||
|
|
@ -262,7 +262,6 @@
|
|||
[fllog fl-unop]
|
||||
[flexp fl-unop]
|
||||
[flsqrt fl-unop]
|
||||
[->fl (-Integer . -> . -Flonum)]
|
||||
|
||||
;; safe flvector ops
|
||||
|
||||
|
|
|
|||
|
|
@ -704,40 +704,3 @@
|
|||
|
||||
|
||||
;; mutable pairs
|
||||
|
||||
|
||||
;; Byte and String Output (Section 12.3 of the Reference)
|
||||
[write-char (cl-> [(-Char) -Void]
|
||||
[(-Char -Output-Port) -Void])]
|
||||
[write-byte (cl-> [(-Nat) -Void]
|
||||
[(-Nat -Output-Port) -Void])]
|
||||
[newline (cl-> [() -Void]
|
||||
[(-Output-Port) -Void])]
|
||||
[write-string (cl-> [(-String) -Nat]
|
||||
[(-String -Output-Port) -Nat]
|
||||
[(-String -Output-Port -Nat) -Nat]
|
||||
[(-String -Output-Port -Nat -Nat) -Nat])]
|
||||
[write-bytes (cl-> [(-Bytes) -Nat]
|
||||
[(-Bytes -Output-Port) -Nat]
|
||||
[(-Bytes -Output-Port -Nat) -Nat]
|
||||
[(-Bytes -Output-Port -Nat -Nat) -Nat])]
|
||||
[write-bytes-avail (cl-> [(-Bytes) -Nat]
|
||||
[(-Bytes -Output-Port) -Nat]
|
||||
[(-Bytes -Output-Port -Nat) -Nat]
|
||||
[(-Bytes -Output-Port -Nat -Nat) -Nat])]
|
||||
[write-bytes-avail* (cl-> [(-Bytes) (-opt -Nat)]
|
||||
[(-Bytes -Output-Port) (-opt -Nat)]
|
||||
[(-Bytes -Output-Port -Nat) (-opt -Nat)]
|
||||
[(-Bytes -Output-Port -Nat -Nat) (-opt -Nat)])]
|
||||
[write-bytes-avail/enable-break (cl-> [(-Bytes) -Nat]
|
||||
[(-Bytes -Output-Port) -Nat]
|
||||
[(-Bytes -Output-Port -Nat) -Nat]
|
||||
[(-Bytes -Output-Port -Nat -Nat) -Nat])]
|
||||
[write-special (cl-> [(Univ) -Boolean]
|
||||
[(Univ -Output-Port) -Boolean])]
|
||||
;; Need event type before we can include these
|
||||
;;write-special-avail*
|
||||
;;write-bytes-avail-evt
|
||||
;;write-special-evt
|
||||
[port-writes-atomic? (-Output-Port . -> . -Boolean)]
|
||||
[port-writes-special? (-Output-Port . -> . -Boolean)]
|
||||
|
|
|
|||
|
|
@ -68,7 +68,7 @@
|
|||
(define-values (dom* opt-dom* rngs* rst)
|
||||
(match a
|
||||
;; functions with no filters or objects
|
||||
[(arr: dom (Values: (list (Result: rngs (LFilterSet: '() '()) (LEmpty:)) ...)) rst #f kws)
|
||||
[(arr: dom (Values: (list (Result: rngs (FilterSet: (Top:) (Top:)) (Empty:)) ...)) rst #f kws)
|
||||
(let-values ([(mand-kws opt-kws) (partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws)]
|
||||
[(conv) (match-lambda [(Keyword: kw kty _) (list kw (t->c/neg kty))])])
|
||||
(values (append (map t->c/neg dom) (append-map conv mand-kws))
|
||||
|
|
|
|||
|
|
@ -9,15 +9,22 @@
|
|||
(λ (e)
|
||||
(and (Filter? e) (not (NoFilter? e)) (not (FilterSet? e))))))
|
||||
|
||||
(define LatentFilter/c
|
||||
(define FilterSet/c
|
||||
(flat-named-contract
|
||||
'FilterSet
|
||||
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
|
||||
|
||||
|
||||
#;(define LatentFilter/c
|
||||
(flat-named-contract
|
||||
'LatentFilter
|
||||
(λ (e)
|
||||
(and (LatentFilter? e) (not (LFilterSet? e))))))
|
||||
|
||||
(provide Filter/c LatentFilter/c FilterSet/c LatentFilterSet/c index/c)
|
||||
(provide Filter/c FilterSet/c); LatentFilter/c LatentFilterSet/c index/c)
|
||||
|
||||
(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))]
|
||||
|
|
@ -32,24 +39,29 @@
|
|||
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
|
||||
|
||||
;; implication
|
||||
(df ImpFilter ([a (non-empty-listof Filter/c)] [c (non-empty-listof Filter/c)])
|
||||
[#:frees (combine-frees (map free-vars* (append a c)))
|
||||
(combine-frees (map free-idxs* (append a c)))])
|
||||
(df ImpFilter ([a Filter/c] [c Filter/c]))
|
||||
|
||||
(df AndFilter ([fs (non-empty-listof Filter/c)])
|
||||
[#:fold-rhs (*AndFilter (map filter-rec-id fs))]
|
||||
[#:frees (combine-frees (map free-vars* fs))
|
||||
(combine-frees (map free-idxs* fs))])
|
||||
|
||||
(df OrFilter ([fs (non-empty-listof Filter/c)])
|
||||
[#:fold-rhs (*OrFilter (map filter-rec-id fs))]
|
||||
[#:frees (combine-frees (map free-vars* fs))
|
||||
(combine-frees (map free-idxs* fs))])
|
||||
|
||||
(df FilterSet (thn els)
|
||||
[#:frees (combine-frees (map free-vars* (append thn els)))
|
||||
(combine-frees (map free-idxs* (append thn els)))]
|
||||
[#:fold-rhs (*FilterSet (map filter-rec-id thn) (map filter-rec-id els))]
|
||||
[#:contract (->d ([t (cond [(ormap Bot? t)
|
||||
(list/c Bot?)]
|
||||
[(ormap Bot? e)
|
||||
(flat-named-contract "e was Bot" (list/c))]
|
||||
[else (listof Filter/c)])]
|
||||
[e (cond [(ormap Bot? e)
|
||||
(list/c Bot?)]
|
||||
[(ormap Bot? t)
|
||||
(flat-named-contract "t was Bot" (list/c))]
|
||||
[else (listof Filter/c)])])
|
||||
[#:contract (->d ([t (cond [(Bot? t)
|
||||
Bot?]
|
||||
[(Bot? e)
|
||||
Top?]
|
||||
[else Filter/c])]
|
||||
[e (cond [(Bot? e)
|
||||
Bot?]
|
||||
[(Bot? t)
|
||||
Top?]
|
||||
[else Filter/c])])
|
||||
(#:syntax [stx #f])
|
||||
[result FilterSet?])])
|
||||
|
||||
|
|
@ -57,6 +69,7 @@
|
|||
;; 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])
|
||||
|
|
@ -69,6 +82,8 @@
|
|||
[#: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)))
|
||||
|
|
@ -92,15 +107,11 @@
|
|||
(#:syntax [stx #f])
|
||||
[result LFilterSet?])])
|
||||
|
||||
(define FilterSet/c
|
||||
(flat-named-contract
|
||||
'FilterSet
|
||||
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
|
||||
|
||||
(define LatentFilterSet/c
|
||||
(flat-named-contract
|
||||
'LatentFilterSet
|
||||
(λ (e) (or (LFilterSet? e)))))
|
||||
|#
|
||||
|
||||
(define filter-equal? eq?)
|
||||
(define (filter-equal? a b) (= (Rep-seq a) (Rep-seq b)))
|
||||
(provide filter-equal?)
|
||||
|
|
@ -1,6 +1,7 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require scheme/match scheme/contract "rep-utils.ss" "free-variance.ss" "filter-rep.ss")
|
||||
(provide object-equal?)
|
||||
|
||||
(dpe CarPE () [#:fold-rhs #:base])
|
||||
(dpe CdrPE () [#:fold-rhs #:base])
|
||||
|
|
@ -16,12 +17,16 @@
|
|||
[#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
|
||||
[#:fold-rhs (*Path (map pathelem-rec-id p) v)])
|
||||
|
||||
;; represents no info about the filters of this expression
|
||||
;; represents no info about the object of this expression
|
||||
;; should only be used for parsing type annotations and expected types
|
||||
(do NoObject () [#:fold-rhs #:base])
|
||||
|
||||
(define (object-equal? o1 o2) (= (Rep-seq o1) (Rep-seq o2)))
|
||||
|
||||
#|
|
||||
(dlo LEmpty () [#:fold-rhs #:base])
|
||||
|
||||
(dlo LPath ([p (listof PathElem?)] [idx index/c])
|
||||
[#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
|
||||
[#:fold-rhs (*LPath (map pathelem-rec-id p) idx)])
|
||||
|#
|
||||
|
|
@ -5,7 +5,7 @@
|
|||
"rep-utils.ss" "object-rep.ss" "filter-rep.ss" "free-variance.ss"
|
||||
mzlib/trace scheme/match
|
||||
scheme/contract
|
||||
(for-syntax scheme/base))
|
||||
(for-syntax scheme/base syntax/parse))
|
||||
|
||||
(define name-table (make-weak-hasheq))
|
||||
|
||||
|
|
@ -132,9 +132,9 @@
|
|||
[#:frees (λ (f) (f ty))]
|
||||
[#:fold-rhs (*Keyword kw (type-rec-id ty) required?)])
|
||||
|
||||
(dt Result ([t Type/c] [f LFilterSet?] [o LatentObject?])
|
||||
(dt Result ([t Type/c] [f FilterSet?] [o Object?])
|
||||
[#:frees (λ (frees) (combine-frees (map frees (list t f o))))]
|
||||
[#:fold-rhs (*Result (type-rec-id t) (latentfilter-rec-id f) (latentobject-rec-id o))])
|
||||
[#:fold-rhs (*Result (type-rec-id t) (filter-rec-id f) (object-rec-id o))])
|
||||
|
||||
;; types : Listof[Type]
|
||||
(dt Values ([rs (listof Result?)])
|
||||
|
|
@ -150,7 +150,11 @@
|
|||
[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?)])
|
||||
[kws (listof Keyword?)]
|
||||
;; order is: fixed, rest/drest, keywords
|
||||
[names (listof identifier?)])
|
||||
#:no-provide
|
||||
[#:intern (list dom rng rest drest kws (map hash-id names))]
|
||||
[#:frees (combine-frees
|
||||
(append (map (compose flip-variances free-vars*)
|
||||
(append (if rest (list rest) null)
|
||||
|
|
@ -179,7 +183,8 @@
|
|||
(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))])
|
||||
(map type-rec-id kws)
|
||||
names)])
|
||||
|
||||
;; top-arr is the supertype of all function types
|
||||
(dt top-arr () [#:fold-rhs #:base])
|
||||
|
|
@ -396,7 +401,7 @@
|
|||
;; necessary to avoid infinite loops
|
||||
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
|
||||
;; functions
|
||||
[#:arr dom rng rest drest kws
|
||||
[#:arr dom rng rest drest kws names
|
||||
(*arr (map sb dom)
|
||||
(sb rng)
|
||||
(if rest (sb rest) #f)
|
||||
|
|
@ -404,7 +409,8 @@
|
|||
(cons (sb (car drest))
|
||||
(if (eq? (cdr drest) name) (+ count outer) (cdr drest)))
|
||||
#f)
|
||||
(map sb kws))]
|
||||
(map sb kws)
|
||||
names)]
|
||||
[#:ValuesDots rs dty dbound
|
||||
(*ValuesDots (map sb rs)
|
||||
(sb dty)
|
||||
|
|
@ -441,7 +447,7 @@
|
|||
;; necessary to avoid infinite loops
|
||||
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
|
||||
;; functions
|
||||
[#:arr dom rng rest drest kws
|
||||
[#:arr dom rng rest drest kws names
|
||||
(*arr (map sb dom)
|
||||
(sb rng)
|
||||
(if rest (sb rest) #f)
|
||||
|
|
@ -449,7 +455,8 @@
|
|||
(cons (sb (car drest))
|
||||
(if (eqv? (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
|
||||
#f)
|
||||
(map sb kws))]
|
||||
(map sb kws)
|
||||
names)]
|
||||
[#:ValuesDots rs dty dbound
|
||||
(*ValuesDots (map sb rs)
|
||||
(sb dty)
|
||||
|
|
@ -604,6 +611,13 @@
|
|||
(list syms (PolyDots-body* syms t))))
|
||||
(list nps bp)))])))
|
||||
|
||||
(define-match-expander arr:*
|
||||
(lambda (stx)
|
||||
(syntax-parse stx
|
||||
[(_ dom rng rest drest kws names)
|
||||
(syntax/loc stx (arr: dom rng rest drest kws names))]
|
||||
[(_ dom rng rest drest kws)
|
||||
(syntax/loc stx (arr: dom rng rest drest kws _))])))
|
||||
;(trace subst subst-all)
|
||||
|
||||
(provide
|
||||
|
|
@ -614,6 +628,7 @@
|
|||
PolyDots-unsafe:
|
||||
Mu? Poly? PolyDots?
|
||||
arr
|
||||
arr?
|
||||
Type? Filter? LatentFilter? Object? LatentObject?
|
||||
Type/c
|
||||
Poly-n
|
||||
|
|
@ -631,7 +646,9 @@
|
|||
[PolyDots* make-PolyDots]
|
||||
[Mu-body* Mu-body]
|
||||
[Poly-body* Poly-body]
|
||||
[PolyDots-body* PolyDots-body]))
|
||||
[PolyDots-body* PolyDots-body]
|
||||
[*arr make-arr]
|
||||
[arr:* arr:]))
|
||||
|
||||
(p/c [type-equal? (Rep? Rep? . -> . boolean?)])
|
||||
|
||||
|
|
|
|||
|
|
@ -52,36 +52,24 @@
|
|||
(alt equal? equal?-able)))
|
||||
(match* ((single-value v1) (single-value v2))
|
||||
[((tc-result1: t _ o) (tc-result1: (Value: (? ok? val))))
|
||||
(ret -Boolean (apply-filter (make-LFilterSet (list (make-LTypeFilter (-val val) null 0)) (list (make-LNotTypeFilter (-val val) null 0))) t o))]
|
||||
(ret -Boolean
|
||||
(-FS (-filter-at (-val val) o)
|
||||
(-not-filter-at (-val val) o)))]
|
||||
[((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o))
|
||||
(ret -Boolean (apply-filter (make-LFilterSet (list (make-LTypeFilter (-val val) null 0)) (list (make-LNotTypeFilter (-val val) null 0))) t o))]
|
||||
(ret -Boolean
|
||||
(-FS (-filter-at (-val val) o)
|
||||
(-not-filter-at (-val val) o)))]
|
||||
[((tc-result1: t _ o)
|
||||
(and (? (lambda _ (free-identifier=? #'member comparator)))
|
||||
(tc-result1: (app untuple (list (and ts (Value: _)) ...)))))
|
||||
(or (and (? (lambda _ (free-identifier=? #'member comparator)))
|
||||
(tc-result1: (app untuple (list (and ts (Value: _)) ...))))
|
||||
(and (? (lambda _ (free-identifier=? #'memv comparator)))
|
||||
(tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...))))
|
||||
(and (? (lambda _ (free-identifier=? #'memq comparator)))
|
||||
(tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...))))))
|
||||
(let ([ty (apply Un ts)])
|
||||
(ret (Un (-val #f) t)
|
||||
(apply-filter
|
||||
(make-LFilterSet (list (make-LTypeFilter ty null 0))
|
||||
(list (make-LNotTypeFilter ty null 0)))
|
||||
t o)))]
|
||||
[((tc-result1: t _ o)
|
||||
(and (? (lambda _ (free-identifier=? #'memv comparator)))
|
||||
(tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...)))))
|
||||
(let ([ty (apply Un ts)])
|
||||
(ret (Un (-val #f) t)
|
||||
(apply-filter
|
||||
(make-LFilterSet (list (make-LTypeFilter ty null 0))
|
||||
(list (make-LNotTypeFilter ty null 0)))
|
||||
t o)))]
|
||||
[((tc-result1: t _ o)
|
||||
(and (? (lambda _ (free-identifier=? #'memq comparator)))
|
||||
(tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...)))))
|
||||
(let ([ty (apply Un ts)])
|
||||
(ret (Un (-val #f) t)
|
||||
(apply-filter
|
||||
(make-LFilterSet (list (make-LTypeFilter ty null 0))
|
||||
(list (make-LNotTypeFilter ty null 0)))
|
||||
t o)))]
|
||||
(-FS (-filter-at ty o)
|
||||
(-not-filter-at ty o))))]
|
||||
[(_ _) (ret -Boolean)]))
|
||||
|
||||
|
||||
|
|
@ -609,7 +597,7 @@
|
|||
(= (length d)
|
||||
(length (syntax->list #'args))))
|
||||
dom)
|
||||
(Values: (list (Result: v (LFilterSet: '() '()) (LEmpty:))))
|
||||
(Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:))))
|
||||
#f #f (list (Keyword: _ _ #f) ...)))))))
|
||||
;(printf "f dom: ~a ~a~n" (syntax->datum #'f) dom)
|
||||
(let ([arg-tys (map (lambda (a t) (tc-expr/check a (ret t)))
|
||||
|
|
@ -740,10 +728,13 @@
|
|||
|
||||
;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results?
|
||||
(define (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t])
|
||||
;(printf "got to here 0~a~n" args-stx)
|
||||
(match* (ftype0 argtys)
|
||||
;; we check that all kw args are optional
|
||||
[((arr: dom (Values: (list (Result: t-r lf-r lo-r) ...)) rest #f (list (Keyword: _ _ #f) ...))
|
||||
[((arr: dom (Values: (list (Result: t-r f-r o-r) ...)) rest #f (list (Keyword: _ _ #f) ...)
|
||||
names)
|
||||
(list (tc-result1: t-a phi-a o-a) ...))
|
||||
;(printf "got to here 1~a~n" args-stx)
|
||||
(when check?
|
||||
(cond [(and (not rest) (not (= (length dom) (length t-a))))
|
||||
(tc-error/expr #:return (ret t-r)
|
||||
|
|
@ -751,26 +742,27 @@
|
|||
[(and rest (< (length t-a) (length dom)))
|
||||
(tc-error/expr #:return (ret t-r)
|
||||
"Wrong number of arguments, expected at least ~a and got ~a" (length dom) (length t-a))])
|
||||
(for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))] [a (syntax->list args-stx)] [arg-t (in-list t-a)])
|
||||
(for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))]
|
||||
[a (in-list (syntax->list args-stx))]
|
||||
[arg-t (in-list t-a)])
|
||||
(parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
|
||||
(let* (;; Listof[Listof[LFilterSet]]
|
||||
[lfs-f (for/list ([lf lf-r])
|
||||
(for/list ([i (in-indexes dom)])
|
||||
(split-lfilters lf i)))]
|
||||
;; Listof[FilterSet]
|
||||
[f-r (for/list ([lfs lfs-f])
|
||||
(merge-filter-sets
|
||||
(for/list ([lf lfs] [t t-a] [o o-a])
|
||||
(apply-filter lf t o))))]
|
||||
;; Listof[Object]
|
||||
[o-r (for/list ([lo lo-r])
|
||||
(match lo
|
||||
[(LPath: pi* i)
|
||||
(match (object-index o-a i)
|
||||
[(Path: pi x) (make-Path (append pi* pi) x)]
|
||||
[_ (make-Empty)])]
|
||||
[_ (make-Empty)]))])
|
||||
(ret t-r f-r o-r))]
|
||||
;(printf "got to here 2 ~a ~a ~a ~n" dom names o-a)
|
||||
(let-values ([(names o-a)
|
||||
(for/lists (n o) ([d (in-list dom)]
|
||||
[nm (in-list names)]
|
||||
[oa (in-list o-a)])
|
||||
(values nm oa))])
|
||||
;(printf "got to here 3~a~n" args-stx)
|
||||
(let* (;; Listof[FilterSet]
|
||||
[f-r (for/list ([f f-r])
|
||||
(apply-filter f names o-a))]
|
||||
;; Listof[Object]
|
||||
[o-r (for/list ([o o-r])
|
||||
(apply-object o names o-a))]
|
||||
;; Listof[Type]
|
||||
[t-r (for/list ([t t-r])
|
||||
(apply-type t names o-a))])
|
||||
(ret t-r f-r o-r)))]
|
||||
[((arr: _ _ _ drest '()) _)
|
||||
(int-err "funapp with drest args NYI")]
|
||||
[((arr: _ _ _ _ kws) _)
|
||||
|
|
|
|||
|
|
@ -15,8 +15,6 @@
|
|||
(typecheck tc-metafunctions)
|
||||
(for-syntax scheme/base))
|
||||
|
||||
(provide env+)
|
||||
|
||||
(define (replace-nth l i f)
|
||||
(cond [(null? l) (error 'replace-nth "list not long enough" l i f)]
|
||||
[(zero? i) (cons (f (car l)) (cdr l))]
|
||||
|
|
@ -75,3 +73,5 @@
|
|||
(set-box! flag #f))
|
||||
new-t))
|
||||
x Γ)])))
|
||||
|
||||
(p/c [env+ (env? (listof Filter/c) (box/c #t). -> . env?)])
|
||||
|
|
@ -135,8 +135,8 @@
|
|||
(define (tc-id id)
|
||||
(let* ([ty (lookup-type/lexical id)])
|
||||
(ret ty
|
||||
(make-FilterSet (list (make-NotTypeFilter (-val #f) null id))
|
||||
(list (make-TypeFilter (-val #f) null id)))
|
||||
(make-FilterSet (make-NotTypeFilter (-val #f) null id)
|
||||
(make-TypeFilter (-val #f) null id))
|
||||
(make-Path null id))))
|
||||
|
||||
;; typecheck an expression, but throw away the effect
|
||||
|
|
@ -174,7 +174,7 @@
|
|||
(if (= (length ts) (length ts2))
|
||||
(ret ts2 fs os)
|
||||
(ret ts2))]
|
||||
[((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
|
||||
[((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
|
||||
(cond
|
||||
[(not (subtype t1 t2))
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1)])
|
||||
|
|
@ -183,6 +183,9 @@
|
|||
(cond
|
||||
[(not (subtype t1 t2))
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1)]
|
||||
[(and (not (filter-equal? f1 f2))
|
||||
(object-equal? o1 o2))
|
||||
(tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
|
||||
[(not (and (equal? f1 f2) (equal? o1 o2)))
|
||||
(tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))])
|
||||
expected]
|
||||
|
|
@ -254,6 +257,7 @@
|
|||
(add-typeof-expr form t)
|
||||
t)]))))
|
||||
|
||||
#;
|
||||
(define (tc-or e1 e2 or-part [expected #f])
|
||||
(match (single-value e1)
|
||||
[(tc-result1: t1 (and f1 (FilterSet: fs+ fs-)) o1)
|
||||
|
|
@ -345,14 +349,7 @@
|
|||
[(let-values (((_) meth))
|
||||
(let-values (((_ _) (#%plain-app find-method/who _ rcvr _)))
|
||||
(#%plain-app _ _ args ...)))
|
||||
(tc/send #'rcvr #'meth #'(args ...) expected)]
|
||||
;; or
|
||||
[(let-values ([(or-part) e1]) (if op1 op2 e2))
|
||||
(and
|
||||
(identifier? #'op1) (identifier? #'op2)
|
||||
(free-identifier=? #'or-part #'op1)
|
||||
(free-identifier=? #'or-part #'op2))
|
||||
(tc-or #'e1 #'e2 #'or-part expected)]
|
||||
(tc/send #'rcvr #'meth #'(args ...) expected)]
|
||||
;; let
|
||||
[(let-values ([(name ...) expr] ...) . body)
|
||||
(tc/let-values #'((name ...) ...) #'(expr ...) #'body form expected)]
|
||||
|
|
@ -415,12 +412,6 @@
|
|||
(let-values (((_ _) (#%plain-app find-method/who _ rcvr _)))
|
||||
(#%plain-app _ _ args ...)))
|
||||
(tc/send #'rcvr #'meth #'(args ...))]
|
||||
;; or
|
||||
[(let-values ([(or-part) e1]) (if op1 op2 e2))
|
||||
(and (identifier? #'op1) (identifier? #'op2)
|
||||
(free-identifier=? #'or-part #'op1)
|
||||
(free-identifier=? #'or-part #'op2))
|
||||
(tc-or #'e1 #'e2 #'or-part)]
|
||||
;; let
|
||||
[(let-values ([(name ...) expr] ...) . body)
|
||||
(tc/let-values #'((name ...) ...) #'(expr ...) #'body form)]
|
||||
|
|
|
|||
|
|
@ -4,14 +4,14 @@
|
|||
(require (rename-in "../utils/utils.ss" [infer r:infer]))
|
||||
(require "signatures.ss"
|
||||
(rep type-rep filter-rep object-rep)
|
||||
(rename-in (types convenience subtype union utils comparison remove-intersect)
|
||||
(rename-in (types convenience subtype union utils comparison remove-intersect abbrev)
|
||||
[remove *remove])
|
||||
(env lexical-env type-environments)
|
||||
(r:infer infer)
|
||||
(utils tc-utils)
|
||||
(typecheck tc-envops tc-metafunctions)
|
||||
syntax/kerncase
|
||||
mzlib/trace
|
||||
mzlib/trace unstable/debug
|
||||
scheme/match)
|
||||
|
||||
;; if typechecking
|
||||
|
|
@ -43,18 +43,27 @@
|
|||
[(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
|
||||
(let*-values ([(flag+ flag-) (values (box #t) (box #t))]
|
||||
[(derived-imps+ derived-atoms+)
|
||||
(combine-props fs+ (env-props (lexical-env)))])
|
||||
(match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+ flag+) (tc thn (unbox flag+)))]
|
||||
[(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))])
|
||||
(combine-props (list fs+) (env-props (lexical-env)))])
|
||||
(match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) (list fs+) flag+) (tc thn (unbox flag+)))]
|
||||
[(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) (list fs-) flag-) (tc els (unbox flag-)))])
|
||||
;; if we have the same number of values in both cases
|
||||
(cond [(= (length ts) (length us))
|
||||
(let ([r
|
||||
(combine-results
|
||||
(for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3])
|
||||
(combine-filter f1 f2 f3 t u o2 o3)))])
|
||||
(if expected
|
||||
(check-below r expected)
|
||||
r))]
|
||||
(let ([r (combine-results
|
||||
(for/list ([f2 fs2] [f3 fs3] [t2 ts] [t3 us] [o2 os2] [o3 os3])
|
||||
(let ([filter
|
||||
(match* (f2 f3)
|
||||
[((NoFilter:) _)
|
||||
(-FS -top -top)]
|
||||
[(_ (NoFilter:))
|
||||
(-FS -top -top)]
|
||||
[((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
|
||||
(-FS (-or (-and fs+ f2+) (-and fs- f3+))
|
||||
(-or (-and fs+ f2-) (-and fs- f3-)))])]
|
||||
[type (Un t2 t3)]
|
||||
[object (if (object-equal? o2 o3) o2 (make-Empty))])
|
||||
;(printf "result filter is: ~a\n" filter)
|
||||
(ret type filter object))))])
|
||||
(if expected (check-below r expected) r))]
|
||||
;; special case if one of the branches is unreachable
|
||||
[(and (= 1 (length us)) (type-equal? (car us) (Un)))
|
||||
(if expected (check-below (ret ts fs2 os2) expected) (ret ts fs2 os2))]
|
||||
|
|
@ -63,7 +72,7 @@
|
|||
;; otherwise, error
|
||||
[else
|
||||
(tc-error/expr #:return (ret (or expected Err))
|
||||
"Expected the same number of values from both branches of if expression, but got ~a and ~a"
|
||||
"Expected the same number of values from both branches of `if' expression, but got ~a and ~a"
|
||||
(length ts) (length us))])))]
|
||||
[(tc-results: t _ _)
|
||||
(tc-error/expr #:return (ret (or expected Err))
|
||||
|
|
|
|||
|
|
@ -14,7 +14,8 @@
|
|||
(types abbrev utils)
|
||||
(env type-environments lexical-env)
|
||||
(utils tc-utils)
|
||||
mzlib/plt-match)
|
||||
unstable/debug
|
||||
scheme/match)
|
||||
(require (for-template scheme/base "internal-forms.ss"))
|
||||
|
||||
(import tc-expr^)
|
||||
|
|
@ -32,9 +33,7 @@
|
|||
[(struct lam-result ((list (list arg-ids arg-tys) ...) (list (list kw kw-id kw-ty req?) ...) rest drest body))
|
||||
(make-arr
|
||||
arg-tys
|
||||
(abstract-filters (append (for/list ([i (in-naturals)] [_ arg-ids]) i) kw)
|
||||
(append arg-ids kw-id)
|
||||
body)
|
||||
(abstract-filters body)
|
||||
#:kws (map make-Keyword kw kw-ty req?)
|
||||
#:rest rest
|
||||
#:drest drest)]))
|
||||
|
|
@ -200,7 +199,7 @@
|
|||
[(tc-result1: (Function: (list (arr: argss rets rests drests '()) ...)))
|
||||
(for/list ([args argss] [ret rets] [rest rests] [drest drests])
|
||||
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies))
|
||||
args (values->tc-results ret (formals->list (car (syntax->list formals)))) rest drest))]
|
||||
args (values->tc-results ret) rest drest))]
|
||||
[_ (go (syntax->list formals) (syntax->list bodies) null null null)]))]
|
||||
;; otherwise
|
||||
[else (go (syntax->list formals) (syntax->list bodies) null null null)]))
|
||||
|
|
|
|||
|
|
@ -5,14 +5,18 @@
|
|||
[-> -->]
|
||||
[->* -->*]
|
||||
[one-of/c -one-of/c])
|
||||
(rep type-rep filter-rep) scheme/list
|
||||
(rep type-rep filter-rep rep-utils) scheme/list
|
||||
scheme/contract scheme/match unstable/match
|
||||
(for-syntax scheme/base))
|
||||
|
||||
(provide combine-filter apply-filter abstract-filter abstract-filters combine-props
|
||||
split-lfilters merge-filter-sets values->tc-results tc-results->values)
|
||||
;(provide (all-defined-out))
|
||||
|
||||
(define-syntax-rule (d/c/p (name . args) c . body)
|
||||
(begin (d/c (name . args) c . body)
|
||||
(p/c [name c])))
|
||||
|
||||
;; this implements the sequence invariant described on the first page relating to Bot
|
||||
#;
|
||||
(define (lcombine l1 l2)
|
||||
(cond [(memq (make-LBot) l1)
|
||||
(make-LFilterSet (list (make-LBot)) null)]
|
||||
|
|
@ -21,31 +25,25 @@
|
|||
[else (make-LFilterSet l1 l2)]))
|
||||
|
||||
(define (combine l1 l2)
|
||||
(cond [(memq (make-Bot) l1)
|
||||
(make-FilterSet (list (make-Bot)) null)]
|
||||
[(memq (make-Bot) l2)
|
||||
(make-FilterSet null (list (make-Bot)))]
|
||||
[else (make-FilterSet l1 l2)]))
|
||||
(match* (l1 l2)
|
||||
[(_ (Bot:)) (-FS -top -bot)]
|
||||
[((Bot:) _) (-FS -bot -top)]
|
||||
[(_ _) (-FS l1 l2)]))
|
||||
|
||||
(d/c (abstract-filters keys ids results)
|
||||
((listof index/c) (listof identifier?) tc-results? . -> . (or/c Values? ValuesDots?))
|
||||
(define (mk l [drest #f])
|
||||
(if drest (make-ValuesDots l (car drest) (cdr drest)) (make-Values l)))
|
||||
(d/c/p (abstract-filters results)
|
||||
(tc-results? . -> . (or/c Values? ValuesDots?))
|
||||
(match results
|
||||
[(tc-results: ts fs os dty dbound)
|
||||
(make-ValuesDots
|
||||
(for/list ([t ts]
|
||||
[f fs]
|
||||
[o os])
|
||||
(make-Result t (abstract-filter ids keys f) (abstract-object ids keys o)))
|
||||
(for/list ([t ts] [f fs] [o os])
|
||||
(make-Result t f o))
|
||||
dty dbound)]
|
||||
[(tc-results: ts fs os)
|
||||
(make-Values
|
||||
(for/list ([t ts]
|
||||
[f fs]
|
||||
[o os])
|
||||
(make-Result t (abstract-filter ids keys f) (abstract-object ids keys o))))]))
|
||||
(for/list ([t ts] [f fs] [o os])
|
||||
(make-Result t f o)))]))
|
||||
|
||||
#;
|
||||
(define/contract (abstract-object ids keys o)
|
||||
(-> (listof identifier?) (listof index/c) Object? LatentObject?)
|
||||
(define (lookup y)
|
||||
|
|
@ -57,15 +55,17 @@
|
|||
[(Path: p (lookup: idx)) (make-LPath p idx)]
|
||||
[_ (make-LEmpty)]))
|
||||
|
||||
#;
|
||||
(d/c (abstract-filter ids keys fs)
|
||||
(-> (listof identifier?) (listof index/c) FilterSet/c LatentFilterSet/c)
|
||||
(match fs
|
||||
[(FilterSet: f+ f-)
|
||||
(lcombine
|
||||
(combine
|
||||
(apply append (for/list ([f f+]) (abo ids keys f)))
|
||||
(apply append (for/list ([f f-]) (abo ids keys f))))]
|
||||
[(NoFilter:) (lcombine null null)]))
|
||||
[(NoFilter:) (combine -top -top)]))
|
||||
|
||||
#;
|
||||
(d/c (abo xs idxs f)
|
||||
((listof identifier?) (listof index/c) Filter/c . -> . (or/c null? (list/c LatentFilter/c)))
|
||||
(define (lookup y)
|
||||
|
|
@ -91,32 +91,116 @@
|
|||
(define (merge-filter-sets fs)
|
||||
(match fs
|
||||
[(list (FilterSet: f+ f-) ...)
|
||||
(make-FilterSet (remove-duplicates (apply append f+)) (remove-duplicates (apply append f-)))]))
|
||||
(make-FilterSet (make-AndFilter f+) (make-AndFilter f-))]))
|
||||
|
||||
(d/c (apply-filter lfs t o)
|
||||
(-> LatentFilterSet/c Type/c Object? FilterSet/c)
|
||||
(match lfs
|
||||
[(LFilterSet: lf+ lf-)
|
||||
(combine
|
||||
(apply append (for/list ([lf lf+]) (apo lf t o)))
|
||||
(apply append (for/list ([lf lf-]) (apo lf t o))))]))
|
||||
(d/c/p (apply-filter fs ids os [polarity #t])
|
||||
(->* (FilterSet/c (listof identifier?) (listof Object?)) (boolean?) FilterSet/c)
|
||||
(match fs
|
||||
[(FilterSet: f+ f-)
|
||||
(combine (subst-filter* f+ ids os polarity)
|
||||
(subst-filter* f- ids os polarity))]))
|
||||
|
||||
(d/c (apo lf s o)
|
||||
(-> LatentFilter/c Type/c Object? (or/c '() (list/c Filter/c)))
|
||||
(match* (lf s o)
|
||||
[((ImpFilter: as cs) _ _)
|
||||
(match* [(for/list ([a as]) (apo a s o))
|
||||
(for/list ([c cs]) (apo c s o))]
|
||||
[((list (list a*) ...)
|
||||
(list (list c*) ...)) (list (make-ImpFilter a* c*))]
|
||||
[(_ _) null])]
|
||||
[((LBot:) _ _) (list (make-Bot))]
|
||||
[((LNotTypeFilter: (? (lambda (t) (subtype s t)) t) (list) _) _ _) (list (make-Bot))]
|
||||
[((LTypeFilter: (? (lambda (t) (not (overlap s t))) t) (list) _) _ _) (list (make-Bot))]
|
||||
[(_ _ (Empty:)) null]
|
||||
[((LTypeFilter: t pi* _) _ (Path: pi x)) (list (make-TypeFilter t (append pi* pi) x))]
|
||||
[((LNotTypeFilter: t pi* _) _ (Path: pi x)) (list (make-NotTypeFilter t (append pi* pi) x))]))
|
||||
(d/c/p (apply-type t ids os [polarity #t])
|
||||
(->* (Type/c (listof identifier?) (listof Object?)) (boolean?) Type/c)
|
||||
(for/fold ([t t]) ([i (in-list ids)] [o (in-list os)])
|
||||
(subst-type t i o polarity)))
|
||||
|
||||
(d/c/p (apply-object t ids os [polarity #t])
|
||||
(->* (Object? (listof identifier?) (listof Object?)) (boolean?) Object?)
|
||||
(for/fold ([t t]) ([i (in-list ids)] [o (in-list os)])
|
||||
(subst-object t i o polarity)))
|
||||
|
||||
(define (subst-filter* f ids os polarity)
|
||||
(-> Filter/c (listof identifier?) (listof Object?) boolean? Filter/c)
|
||||
(for/fold ([f f]) ([i (in-list ids)] [o (in-list os)])
|
||||
(subst-filter f i o polarity)))
|
||||
|
||||
(d/c/p (subst-filter-set fs id o polarity)
|
||||
(-> FilterSet? identifier? Object? boolean? FilterSet?)
|
||||
(match fs
|
||||
[(FilterSet: f+ f-)
|
||||
(combine (subst-filter f+ id o polarity)
|
||||
(subst-filter f- id o polarity))]))
|
||||
|
||||
(define (subst-type t id o polarity)
|
||||
(define (st t) (subst-type t id o polarity))
|
||||
(d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs id o polarity))
|
||||
(type-case (#:Type st
|
||||
#:Filter sf
|
||||
#:Object (lambda (f) (subst-object f id o polarity)))
|
||||
t))
|
||||
|
||||
(define (subst-object t id o polarity)
|
||||
(match t
|
||||
[(NoObject:) t]
|
||||
[(Empty:) t]
|
||||
[(Path: p i)
|
||||
(if (free-identifier=? i id)
|
||||
(match o
|
||||
[(Empty:) (make-Empty)]
|
||||
;; the result is not from an annotation, so it isn't a NoObject
|
||||
[(NoObject:) (make-Empty)]
|
||||
[(Path: p* i*) (make-Path (append p p*) i*)])
|
||||
t)]))
|
||||
|
||||
;; this is the substitution metafunction
|
||||
(d/c/p (subst-filter f id o polarity)
|
||||
(-> Filter/c identifier? Object? boolean? Filter/c)
|
||||
(define (ap f) (subst-filter f o polarity))
|
||||
(define (tf-matcher t p i id o polarity maker)
|
||||
(match o
|
||||
[(or (Empty:) (NoObject:)) (if polarity -top -bot)]
|
||||
[(Path: p* i*)
|
||||
(cond [(free-identifier=? i id)
|
||||
(maker
|
||||
(subst-type t id o polarity)
|
||||
(append p p*)
|
||||
i*)]
|
||||
[(id-free-in? id t) (if polarity -top -bot)]
|
||||
[else f])]))
|
||||
(match f
|
||||
[(ImpFilter: ant consq)
|
||||
(make-ImpFilter (subst-filter ant id o (not polarity)) (ap consq))]
|
||||
[(AndFilter: fs) (make-AndFilter (map ap fs))]
|
||||
[(OrFilter: fs) (make-OrFilter (map ap fs))]
|
||||
[(Bot:) -bot]
|
||||
[(Top:) -top]
|
||||
[(TypeFilter: t p i)
|
||||
(tf-matcher t p i id o polarity make-TypeFilter)]
|
||||
[(NotTypeFilter: t p i)
|
||||
(tf-matcher t p i id o polarity make-NotTypeFilter)]))
|
||||
|
||||
(define (id-free-in? id type)
|
||||
(let/ec
|
||||
return
|
||||
(define (for-object o)
|
||||
(object-case (#:Type for-type)
|
||||
o
|
||||
[#:Path p i
|
||||
(if (free-identifier=? i id)
|
||||
(return #t)
|
||||
o)]))
|
||||
(define (for-filter o)
|
||||
(filter-case (#:Type for-type
|
||||
#:Filter for-filter)
|
||||
o
|
||||
[#:NotTypeFilter t p i
|
||||
(if (free-identifier=? i id)
|
||||
(return #t)
|
||||
o)]
|
||||
[#:TypeFilter t p i
|
||||
(if (free-identifier=? i id)
|
||||
(return #t)
|
||||
o)]))
|
||||
(define (for-type t)
|
||||
(type-case (#:Type for-type
|
||||
#:Filter for-filter
|
||||
#:Object for-object)
|
||||
t))
|
||||
(for-type type)))
|
||||
|
||||
#|
|
||||
#;
|
||||
(define/contract (split-lfilters lf idx)
|
||||
(LatentFilterSet/c index/c . -> . LatentFilterSet/c)
|
||||
(define (idx= lf)
|
||||
|
|
@ -133,6 +217,7 @@
|
|||
(define-match-expander F-FS:
|
||||
(lambda (stx) #'(FilterSet: (list (Bot:)) _)))
|
||||
|
||||
#;
|
||||
(d/c (combine-filter f1 f2 f3 t2 t3 o2 o3)
|
||||
(FilterSet/c FilterSet/c FilterSet/c Type? Type? Object? Object? . -> . tc-results?)
|
||||
(define (mk f) (ret (Un t2 t3) f (make-Empty)))
|
||||
|
|
@ -163,56 +248,28 @@
|
|||
[(_ _ _)
|
||||
;; could intersect f2 and f3 here
|
||||
(mk (make-FilterSet null null))]))
|
||||
|#
|
||||
|
||||
;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
|
||||
(define (values->tc-results tc formals)
|
||||
(d/c/p (values->tc-results tc)
|
||||
((or/c Values? ValuesDots?) . -> . tc-results?)
|
||||
(match tc
|
||||
[(ValuesDots: (list (Result: ts lfs los) ...) dty dbound)
|
||||
(ret ts
|
||||
(for/list ([lf lfs])
|
||||
(or
|
||||
(and (null? formals)
|
||||
(match lf
|
||||
[(LFilterSet: lf+ lf-)
|
||||
(combine (if (memq (make-LBot) lf+) (list (make-Bot)) (list))
|
||||
(if (memq (make-LBot) lf-) (list (make-Bot)) (list)))]))
|
||||
(merge-filter-sets
|
||||
(for/list ([x formals] [i (in-naturals)])
|
||||
(apply-filter (split-lfilters lf i) Univ (make-Path null x))))))
|
||||
(for/list ([lo los])
|
||||
(or
|
||||
(for/or ([x formals] [i (in-naturals)])
|
||||
(match lo
|
||||
[(LEmpty:) #f]
|
||||
[(LPath: p (== i)) (make-Path p x)]))
|
||||
(make-Empty)))
|
||||
dty dbound)]
|
||||
[(Values: (list (Result: ts lfs los) ...))
|
||||
(ret ts
|
||||
(for/list ([lf lfs])
|
||||
(or
|
||||
(and (null? formals)
|
||||
(match lf
|
||||
[(LFilterSet: lf+ lf-)
|
||||
(combine (if (memq (make-LBot) lf+) (list (make-Bot)) (list))
|
||||
(if (memq (make-LBot) lf-) (list (make-Bot)) (list)))]))
|
||||
(merge-filter-sets
|
||||
(for/list ([x formals] [i (in-naturals)])
|
||||
(apply-filter (split-lfilters lf i) Univ (make-Path null x))))))
|
||||
(for/list ([lo los])
|
||||
(or
|
||||
(for/or ([x formals] [i (in-naturals)])
|
||||
(match lo
|
||||
[(LEmpty:) #f]
|
||||
[(LPath: p (== i)) (make-Path p x)]))
|
||||
(make-Empty))))]))
|
||||
[(ValuesDots: (list (Result: ts fs os) ...) dty dbound)
|
||||
(ret ts fs os dty dbound)]
|
||||
[(Values: (list (Result: ts fs os) ...))
|
||||
(ret ts fs os)]))
|
||||
|
||||
(define (tc-results->values tc)
|
||||
(match tc
|
||||
[(tc-results: ts) (-values ts)]))
|
||||
|
||||
(provide combine-props tc-results->values subst-object subst-type)
|
||||
|
||||
(define (combine-props new-props old-props)
|
||||
(define-values (new-imps new-atoms) (partition ImpFilter? new-props))
|
||||
(define-values (new-atoms new-formulas)
|
||||
(partition (lambda (e) (or (TypeFilter? e) (NotTypeFilter? e))) new-props))
|
||||
(values new-formulas new-atoms)
|
||||
#;#;
|
||||
(define-values (derived-imps derived-atoms)
|
||||
(for/fold
|
||||
([derived-imps null]
|
||||
|
|
|
|||
|
|
@ -143,9 +143,7 @@
|
|||
(for/list ([g (in-list getters)] [t (in-list external-fld-types/no-parent)] [i (in-naturals)])
|
||||
(let ([func (if setters?
|
||||
(->* (list name) t)
|
||||
(make-Function
|
||||
(list (make-arr* (list name) t
|
||||
#:object (make-LPath (list (make-StructPE name i)) 0)))))])
|
||||
(->acc (list name) t (list (make-StructPE name i))))])
|
||||
(cons g (wrapper func))))
|
||||
(if setters?
|
||||
(map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent)
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@
|
|||
[with-handlers
|
||||
([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e))))
|
||||
(lambda (e) (tc-error "Internal error: ~a" e))])]
|
||||
[parameterize (;; disable fancy printing
|
||||
[parameterize (;; enable fancy printing?
|
||||
[custom-printer #t]
|
||||
;; a cheat to avoid units
|
||||
[infer-param infer]
|
||||
|
|
@ -99,7 +99,9 @@
|
|||
[(_ . form)
|
||||
(nest
|
||||
([begin (set-box! typed-context? #t)]
|
||||
[parameterize (;; a cheat to avoid units
|
||||
[parameterize (;; disable fancy printing
|
||||
[custom-printer #t]
|
||||
;; a cheat to avoid units
|
||||
[infer-param infer]
|
||||
;; this paramter is for parsing types
|
||||
[current-tvars initial-tvar-env]
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@
|
|||
scheme/match
|
||||
scheme/promise
|
||||
scheme/flonum
|
||||
unstable/syntax
|
||||
(prefix-in c: scheme/contract)
|
||||
(for-syntax scheme/base syntax/parse)
|
||||
(for-template scheme/base scheme/contract scheme/promise scheme/tcp scheme/flonum))
|
||||
|
|
@ -26,8 +27,6 @@
|
|||
(define -Param make-Param)
|
||||
(define -box make-Box)
|
||||
(define -vec make-Vector)
|
||||
(define -LFS make-LFilterSet)
|
||||
(define-syntax -FS (make-rename-transformer #'make-FilterSet))
|
||||
|
||||
(define-syntax *Un
|
||||
(syntax-rules ()
|
||||
|
|
@ -62,8 +61,8 @@
|
|||
#'(app untuple (? values elem-pats))])))
|
||||
|
||||
|
||||
(d/c (-result t [f -no-lfilter] [o -no-lobj])
|
||||
(c:->* (Type/c) (LFilterSet? LatentObject?) Result?)
|
||||
(d/c (-result t [f -no-filter] [o -no-obj])
|
||||
(c:->* (Type/c) (FilterSet? Object?) Result?)
|
||||
(make-Result t f o))
|
||||
|
||||
(d/c (-values args)
|
||||
|
|
@ -115,11 +114,19 @@
|
|||
(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
|
||||
(define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String))
|
||||
|
||||
(define -no-lfilter (make-LFilterSet null null))
|
||||
(define -no-filter (make-FilterSet null null))
|
||||
(define -no-lobj (make-LEmpty))
|
||||
(define -top (make-Top))
|
||||
(define -bot (make-Bot))
|
||||
(define -no-filter (make-FilterSet -top -top))
|
||||
(define -no-obj (make-Empty))
|
||||
|
||||
|
||||
(d/c (-FS + -)
|
||||
(c:-> Filter/c Filter/c FilterSet?)
|
||||
(match* (+ -)
|
||||
[((Bot:) _) (make-FilterSet -bot -top)]
|
||||
[(_ (Bot:)) (make-FilterSet -top -bot)]
|
||||
[(+ -) (make-FilterSet + -)]))
|
||||
|
||||
(define -car (make-CarPE))
|
||||
(define -cdr (make-CdrPE))
|
||||
(define -syntax-e (make-SyntaxPE))
|
||||
|
|
@ -173,20 +180,26 @@
|
|||
|
||||
(define top-func (make-Function (list (make-top-arr))))
|
||||
|
||||
(d/c (make-arr* dom rng
|
||||
(d/c (make-arr* dom rng
|
||||
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
|
||||
#:filters [filters -no-lfilter] #:object [obj -no-lobj])
|
||||
#:filters [filters -no-filter] #:object [obj -no-obj]
|
||||
#:names [names (append
|
||||
(generate-temporaries dom)
|
||||
(if (or drest rest) (list (generate-temporary)) null)
|
||||
(generate-temporaries kws))])
|
||||
(c:->* ((listof Type/c) (or/c Values? ValuesDots? Type/c))
|
||||
(#:rest (or/c #f Type/c)
|
||||
#:drest (or/c #f (cons/c Type/c symbol?))
|
||||
#:kws (listof Keyword?)
|
||||
#:filters LFilterSet?
|
||||
#:object LatentObject?)
|
||||
#:filters FilterSet?
|
||||
#:object Object?
|
||||
#:names (listof identifier?))
|
||||
arr?)
|
||||
(make-arr dom (if (or (Values? rng) (ValuesDots? rng))
|
||||
rng
|
||||
(make-Values (list (-result rng filters obj))))
|
||||
rest drest (sort #:key Keyword-kw kws keyword<?)))
|
||||
rest drest (sort #:key Keyword-kw kws keyword<?)
|
||||
names))
|
||||
|
||||
(define-syntax (->* stx)
|
||||
(define-syntax-class c
|
||||
|
|
@ -228,10 +241,12 @@
|
|||
(make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))]))
|
||||
|
||||
(define (->acc dom rng path)
|
||||
(define x (generate-temporary 'x))
|
||||
(make-Function (list (make-arr* dom rng
|
||||
#:filters (-LFS (list (-not-filter (-val #f) path))
|
||||
(list (-filter (-val #f) path)))
|
||||
#:object (make-LPath path 0)))))
|
||||
#:names (list x)
|
||||
#:filters (-FS (-not-filter (-val #f) x path)
|
||||
(-filter (-val #f) x path))
|
||||
#:object (make-Path path x)))))
|
||||
|
||||
(define (cl->* . args)
|
||||
(define (funty-arities f)
|
||||
|
|
@ -259,12 +274,70 @@
|
|||
(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 (-filter t [p null] [i 0])
|
||||
(make-LTypeFilter t p i))
|
||||
(d/c (-filter t i [p null])
|
||||
(c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c)
|
||||
(make-TypeFilter t p i))
|
||||
|
||||
(define (-not-filter t [p null] [i 0])
|
||||
(make-LNotTypeFilter t p i))
|
||||
(define (-filter-at t o)
|
||||
(match o
|
||||
[(Path: p i) (-filter t i p)]
|
||||
[_ -top]))
|
||||
(define (-not-filter-at t o)
|
||||
(match o
|
||||
[(Path: p i) (-not-filter t i p)]
|
||||
[_ -top]))
|
||||
|
||||
(define (opposite? f1 f2)
|
||||
(match* (f1 f2)
|
||||
[((TypeFilter: t1 p1 i1)
|
||||
(NotTypeFilter: t2 p1 i2))
|
||||
(and (type-equal? t1 t2)
|
||||
(free-identifier=? i1 i2))]
|
||||
[((NotTypeFilter: t2 p1 i2)
|
||||
(TypeFilter: t1 p1 i1))
|
||||
(and (type-equal? t1 t2)
|
||||
(free-identifier=? i1 i2))]
|
||||
[(_ _) #f]))
|
||||
|
||||
(define (-or . args)
|
||||
(let loop ([fs args] [result null])
|
||||
(if (null? fs)
|
||||
(match result
|
||||
[(list) -bot]
|
||||
[(list f) f]
|
||||
[(list f1 f2) (opposite? f1 f2) -top]
|
||||
[_ (make-OrFilter result)])
|
||||
(match (car fs)
|
||||
[(and t (Top:)) t]
|
||||
[(OrFilter: fs*) (loop (cdr fs) (append fs* result))]
|
||||
[(Bot:) (loop (cdr fs) result)]
|
||||
[t (loop (cdr fs) (cons t result))]))))
|
||||
|
||||
(define (-and . args)
|
||||
(let loop ([fs args] [result null])
|
||||
(if (null? fs)
|
||||
(match result
|
||||
[(list) -top]
|
||||
[(list f) f]
|
||||
;; don't think this is useful here
|
||||
#;[(list f1 f2) (opposite? f1 f2) -bot]
|
||||
[_ (make-AndFilter result)])
|
||||
(match (car fs)
|
||||
[(and t (Bot:)) t]
|
||||
[(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
|
||||
[(Top:) (loop (cdr fs) result)]
|
||||
[t (loop (cdr fs) (cons t result))]))))
|
||||
|
||||
(d/c (-not-filter t i [p null])
|
||||
(c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c)
|
||||
(make-NotTypeFilter t p i))
|
||||
|
||||
(define-syntax-rule (with-names (vars ...) . e)
|
||||
(let-values ([(vars ...) (apply values (generate-temporaries '(vars ...)))])
|
||||
. e))
|
||||
|
||||
(define-syntax-rule (asym-pred (var) dom rng filter)
|
||||
(with-names (var) (make-Function (list (make-arr* (list dom) rng #:names (list var) #:filters filter)))))
|
||||
|
||||
(d/c make-pred-ty
|
||||
(case-> (c:-> Type/c Type/c)
|
||||
|
|
@ -273,15 +346,22 @@
|
|||
(c:-> (listof Type/c) Type/c Type/c integer? (listof PathElem?) Type/c))
|
||||
(case-lambda
|
||||
[(in out t n p)
|
||||
(->* in out : (-LFS (list (-filter t p n)) (list (-not-filter t p n))))]
|
||||
(define xs (generate-temporaries in))
|
||||
(make-Function
|
||||
(list
|
||||
(make-arr*
|
||||
in out
|
||||
#:names xs
|
||||
#:filters (-FS (-filter t (list-ref xs n) p) (-not-filter t (list-ref xs n) p)))))]
|
||||
[(in out t n)
|
||||
(->* in out : (-LFS (list (-filter t null n)) (list (-not-filter t null n))))]
|
||||
(make-pred-ty in out t n null)]
|
||||
[(in out t)
|
||||
(make-pred-ty in out t 0)]
|
||||
[(t) (make-pred-ty (list Univ) -Boolean t 0)]))
|
||||
(make-pred-ty in out t 0 null)]
|
||||
[(t)
|
||||
(make-pred-ty (list Univ) -Boolean t 0 null)]))
|
||||
|
||||
(define true-filter (-FS (list) (list (make-Bot))))
|
||||
(define false-filter (-FS (list (make-Bot)) (list)))
|
||||
(define true-filter (-FS -top -bot))
|
||||
(define false-filter (-FS -bot -top))
|
||||
|
||||
(define (opt-fn args opt-args result)
|
||||
(apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])
|
||||
|
|
|
|||
|
|
@ -29,40 +29,20 @@
|
|||
ns)
|
||||
#f))
|
||||
|
||||
;; print out an effect
|
||||
;; print-effect : Effect Port Boolean -> Void
|
||||
(define (print-latentfilter c port write?)
|
||||
(define (fp . args) (apply fprintf port args))
|
||||
(match c
|
||||
[(LFilterSet: thn els) (fp "(")
|
||||
(if (null? thn)
|
||||
(fp "LTop")
|
||||
(for ([i thn]) (fp "~a " i)))
|
||||
(fp "|")
|
||||
(if (null? els)
|
||||
(fp "LTop")
|
||||
(for ([i els]) (fp " ~a" i)))
|
||||
(fp")")]
|
||||
[(LNotTypeFilter: type path 0) (fp "(! ~a @ ~a)" type path)]
|
||||
[(LTypeFilter: type path 0) (fp "(~a @ ~a)" type path)]
|
||||
[(LNotTypeFilter: type path idx) (fp "(! ~a @ ~a ~a)" type path idx)]
|
||||
[(LTypeFilter: type path idx) (fp "(~a @ ~a ~a)" type path idx)]
|
||||
[(LBot:) (fp "LBot")]
|
||||
[(LImpFilter: a c) (fp "(LImpFilter ~a ~a)" a c)]
|
||||
[else (fp "(Unknown Latent Filter: ~a)" (struct->vector c))]))
|
||||
|
||||
(define (print-filter c port write?)
|
||||
(define (fp . args) (apply fprintf port args))
|
||||
(match c
|
||||
[(FilterSet: thn els) (fp "(")
|
||||
(for ([i thn]) (fp "~a " i)) (fp "|")
|
||||
(for ([i els]) (fp " ~a" i))
|
||||
(fp")")]
|
||||
[(FilterSet: thn els) (fp "(~a | ~a)" thn els)]
|
||||
[(NoFilter:) (fp "-")]
|
||||
[(NotTypeFilter: type (list) id) (fp "(! ~a @ ~a)" type (syntax-e id))]
|
||||
[(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))]
|
||||
[(TypeFilter: type (list) id) (fp "(~a @ ~a)" type (syntax-e id))]
|
||||
[(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path (syntax-e id))]
|
||||
[(Bot:) (fp "Bot")]
|
||||
[(Top:) (fp "Top")]
|
||||
[(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)]
|
||||
[(AndFilter: a) (fp "(AndFilter") (for ([a0 a]) (fp " ~a" a0)) (fp ")")]
|
||||
[(OrFilter: a) (fp "(OrFilter") (for ([a0 a]) (fp " ~a" a0)) (fp ")")]
|
||||
[else (fp "(Unknown Filter: ~a)" (struct->vector c))]))
|
||||
|
||||
(define (print-pathelem c port write?)
|
||||
|
|
@ -73,12 +53,6 @@
|
|||
[(StructPE: t i) (fp "(~a ~a)" t i)]
|
||||
[else (fp "(Unknown Path Element: ~a)" (struct->vector c))]))
|
||||
|
||||
(define (print-latentobject c port write?)
|
||||
(define (fp . args) (apply fprintf port args))
|
||||
(match c
|
||||
[(LEmpty:) (fp "")]
|
||||
[(LPath: pes i) (fp "~a" (append pes (list i)))]))
|
||||
|
||||
(define (print-object c port write?)
|
||||
(define (fp . args) (apply fprintf port args))
|
||||
(match c
|
||||
|
|
@ -114,17 +88,17 @@
|
|||
(fp "~a ...~a~a "
|
||||
(car drest) (if (special-dots-printing?) "" " ") (cdr drest)))
|
||||
(match rng
|
||||
[(Values: (list (Result: t (LFilterSet: (list) (list)) (LEmpty:))))
|
||||
[(Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:))))
|
||||
(fp "-> ~a" t)]
|
||||
[(Values: (list (Result: t
|
||||
(LFilterSet: (list (LTypeFilter: ft pth 0))
|
||||
(list (LNotTypeFilter: ft pth 0)))
|
||||
(LEmpty:))))
|
||||
(FilterSet: (TypeFilter: ft pth id)
|
||||
(NotTypeFilter: ft pth id))
|
||||
(Empty:))))
|
||||
(if (null? pth)
|
||||
(fp "-> ~a : ~a" t ft)
|
||||
(begin (fp "-> ~a : ~a @" t ft)
|
||||
(for ([pe pth]) (fp " ~a" pe))))]
|
||||
[(Values: (list (Result: t fs (LEmpty:))))
|
||||
[(Values: (list (Result: t fs (Empty:))))
|
||||
(fp/filter "-> ~a : ~a" t fs)]
|
||||
[(Values: (list (Result: t lf lo)))
|
||||
(fp/filter "-> ~a : ~a ~a" t lf lo)]
|
||||
|
|
@ -141,11 +115,16 @@
|
|||
(match t
|
||||
[(Pair: a e) (cons a (tuple-elems e))]
|
||||
[(Value: '()) null]))
|
||||
(match c
|
||||
(match c
|
||||
;; if we know how it was written, print that
|
||||
[(? Rep-stx a)
|
||||
(fp "~a" (syntax->datum (Rep-stx a)))]
|
||||
[(Univ:) (fp "Any")]
|
||||
;; special case number until something better happens
|
||||
;;[(Base: 'Number _) (fp "Number")]
|
||||
[(? has-name?) (fp "~a" (has-name? c))]
|
||||
[(? has-name?)
|
||||
#;(printf "has a name\n")
|
||||
(fp "~a" (has-name? c))]
|
||||
[(StructTop: st) (fp "~a" st)]
|
||||
[(BoxTop:) (fp "Box")]
|
||||
[(VectorTop:) (fp "Vector")]
|
||||
|
|
@ -183,7 +162,7 @@
|
|||
(lambda (e) (fp " ") (print-arr e))
|
||||
b)
|
||||
(fp ")")]))]
|
||||
[(arr: _ _ _ _ _) (print-arr c)]
|
||||
[(arr: _ _ _ _ _) (fp "(arr ") (print-arr c) (fp ")")]
|
||||
[(Vector: e) (fp "(Vectorof ~a)" e)]
|
||||
[(Box: e) (fp "(Boxof ~a)" e)]
|
||||
[(Union: elems) (fp "~a" (cons 'U elems))]
|
||||
|
|
@ -227,8 +206,8 @@
|
|||
[(Syntax: t) (fp "(Syntaxof ~a)" t)]
|
||||
[(Instance: t) (fp "(Instance ~a)" t)]
|
||||
[(Class: pf nf ms) (fp "(Class)")]
|
||||
[(Result: t (LFilterSet: (list) (list)) (LEmpty:)) (fp "~a" t)]
|
||||
[(Result: t fs (LEmpty:)) (fp "(~a : ~a)" t fs)]
|
||||
[(Result: t (FilterSet: (Top:) (Top:)) (Empty:)) (fp "~a" t)]
|
||||
[(Result: t fs (Empty:)) (fp "(~a : ~a)" t fs)]
|
||||
[(Result: t fs lo) (fp "(~a : ~a : ~a)" t fs lo)]
|
||||
[(Refinement: parent p? _)
|
||||
(fp "(Refinement ~a ~a)" parent (syntax-e p?))]
|
||||
|
|
@ -238,7 +217,7 @@
|
|||
|
||||
(set-box! print-type* print-type)
|
||||
(set-box! print-filter* print-filter)
|
||||
(set-box! print-latentfilter* print-latentfilter)
|
||||
;(set-box! print-latentfilter* print-latentfilter)
|
||||
(set-box! print-object* print-object)
|
||||
(set-box! print-latentobject* print-latentobject)
|
||||
;(set-box! print-latentobject* print-latentobject)
|
||||
(set-box! print-pathelem* print-pathelem)
|
||||
|
|
|
|||
|
|
@ -184,14 +184,12 @@
|
|||
(d/c (combine-arrs arrs)
|
||||
(c-> (listof arr?) (or/c #f arr?))
|
||||
(match arrs
|
||||
[(list (arr: dom1 rng1 #f #f '()) (arr: dom rng #f #f '()) ...)
|
||||
[(list (and a1 (arr: dom1 rng1 #f #f '() names)) (arr: dom rng #f #f '()) ...)
|
||||
(cond
|
||||
[(null? dom) (make-arr dom1 rng1 #f #f '())]
|
||||
((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 '())])]
|
||||
[(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)])]
|
||||
[_ #f]))
|
||||
|
||||
|
||||
|
|
@ -328,7 +326,7 @@
|
|||
[((Result: t f o) (Result: t* f o))
|
||||
(subtype* A0 t t*)]
|
||||
;; we can ignore interesting results
|
||||
[((Result: t f o) (Result: t* (LFilterSet: (list) (list)) (LEmpty:)))
|
||||
[((Result: t f o) (Result: t* (FilterSet: (Top:) (Top:)) (Empty:)))
|
||||
(subtype* A0 t t*)]
|
||||
;; subtyping on other stuff
|
||||
[((Syntax: t) (Syntax: t*))
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@
|
|||
target
|
||||
[#:Union tys (Un (map sb tys))]
|
||||
[#:F name* (if (eq? name* name) image target)]
|
||||
[#:arr dom rng rest drest kws
|
||||
[#:arr dom rng rest drest kws names
|
||||
(begin
|
||||
(when (and (pair? drest)
|
||||
(eq? name (cdr drest))
|
||||
|
|
@ -53,7 +53,8 @@
|
|||
(sb rng)
|
||||
(and rest (sb rest))
|
||||
(and drest (cons (sb (car drest)) (cdr drest)))
|
||||
(map sb kws)))]
|
||||
(map sb kws)
|
||||
names))]
|
||||
[#:ValuesDots types dty dbound
|
||||
(begin
|
||||
(when (eq? name dbound)
|
||||
|
|
@ -76,10 +77,10 @@
|
|||
(for/list ([img images])
|
||||
(make-Result
|
||||
(substitute img name expanded)
|
||||
(make-LFilterSet null null)
|
||||
(make-LEmpty))))))
|
||||
(make-FilterSet (make-Top) (make-Top))
|
||||
(make-Empty))))))
|
||||
(make-ValuesDots (map sb types) (sb dty) dbound))]
|
||||
[#:arr dom rng rest drest kws
|
||||
[#:arr dom rng rest drest kws names
|
||||
(if (and (pair? drest)
|
||||
(eq? name (cdr drest)))
|
||||
(make-arr (append
|
||||
|
|
@ -90,12 +91,14 @@
|
|||
(sb rng)
|
||||
rimage
|
||||
#f
|
||||
(map sb kws))
|
||||
(map sb kws)
|
||||
names)
|
||||
(make-arr (map sb dom)
|
||||
(sb rng)
|
||||
(and rest (sb rest))
|
||||
(and drest (cons (sb (car drest)) (cdr drest)))
|
||||
(map sb kws)))])
|
||||
(map sb kws)
|
||||
names))])
|
||||
target))
|
||||
|
||||
;; implements sd from the formalism
|
||||
|
|
@ -113,14 +116,15 @@
|
|||
(if (eq? name* name)
|
||||
image
|
||||
target)]
|
||||
[#:arr dom rng rest drest kws
|
||||
[#:arr dom rng rest drest kws names
|
||||
(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))))
|
||||
(map sb kws))])
|
||||
(map sb kws)
|
||||
names)])
|
||||
target))
|
||||
|
||||
;; substitute many variables
|
||||
|
|
@ -210,7 +214,7 @@
|
|||
;; convenience function for returning the result of typechecking an expression
|
||||
(define ret
|
||||
(case-lambda [(t)
|
||||
(let ([mk (lambda (t) (make-FilterSet null null))])
|
||||
(let ([mk (lambda (t) (make-FilterSet (make-Top) (make-Top)))])
|
||||
(make-tc-results
|
||||
(cond [(Type? t)
|
||||
(list (make-tc-result t (mk t) (make-Empty)))]
|
||||
|
|
|
|||
|
|
@ -161,7 +161,7 @@ at least theoretically.
|
|||
|
||||
|
||||
;; turn contracts on and off - off by default for performance.
|
||||
(define-for-syntax enable-contracts? #f)
|
||||
(define-for-syntax enable-contracts? #t)
|
||||
(provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c)
|
||||
|
||||
;; these are versions of the contract forms conditionalized by `enable-contracts?'
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@
|
|||
[draw-text (String Number Number -> Void)])))
|
||||
(dt Color% (Class () () ([red (-> Number)])))
|
||||
|
||||
(dt Snip% (Class () () ()))
|
||||
(dt Snip% (Class () () ([get-count (-> Integer)])))
|
||||
|
||||
(dt Text% (Class ()
|
||||
()
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user