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

Remove some old debugging printfs in soon-to-be-dead code.

Browse Source 
Fix some requires.
Start implementing metafunctions.
Strengthen contracts on filter-sets.
Rename N B Sym.

svn: r13988

original commit: 6c30e2d9e7c9d983f97092ad3aad8268e0560cb5
This commit is contained in:
Sam Tobin-Hochstadt 2009-03-06 19:50:42 +00:00
parent bc1da3d537
commit c6ccbfc76d
11 changed files with 131 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -9,7 +9,8 @@
(only-in '#%kernel [apply kernel:apply])
scheme/promise
(only-in string-constants/private/only-once maybe-print-message)
(only-in scheme/match/runtime match:error))
(only-in scheme/match/runtime match:error)
(for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])))
[raise (Univ . -> . (Un))]

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

@ -25,8 +25,8 @@
(define-for-syntax (initialize-others)
(d-s date
([second : N] [minute : N] [hour : N] [day : N] [month : N]
[year : N] [weekday : N] [year-day : N] [dst? : B] [time-zone-offset : N])
([second : -Number] [minute : -Number] [hour : -Number] [day : -Number] [month : -Number]
[year : -Number] [weekday : -Number] [year-day : -Number] [dst? : -Boolean] [time-zone-offset : -Number])
())
(d-s exn ([message : -String] [continuation-marks : Univ]) ())
(d-s (exn:fail exn) () (-String -Cont-Mark-Set))
@ -65,7 +65,7 @@
;; make-promise
(-poly (a) (-> (-> a) (-Promise a)))
;; language
Sym
-Symbol
;; qq-append
(-poly (a b)
(cl->*

6
collects/typed-scheme/private/base-types.ss
View File

@ -1,10 +1,10 @@
#lang s-exp "type-env-lang.ss"
[Number N]
[Number -Number]
[Integer -Integer]
[Void -Void]
[Boolean B]
[Symbol Sym]
[Boolean -Boolean]
[Symbol -Symbol]
[String -String]
[Any Univ]
[Port -Port]

1
collects/typed-scheme/private/env-lang.ss
View File

@ -31,6 +31,7 @@
(provide #%module-begin
require
(all-from-out scheme/base)
types rep private utils
(for-syntax
(types-out convenience union)
(all-from-out scheme/base)))

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

@ -3,6 +3,20 @@
(require scheme/match scheme/contract)
(require "rep-utils.ss" "free-variance.ss")
(define Filter/c
(flat-named-contract
'Filter
(λ (e)
(and (Filter? e) (not (FilterSet? e))))))
(define LatentFilter/c
(flat-named-contract
'LatentFilter
(λ (e)
(and (LatentFilter? e) (not (LFilterSet? e))))))
(provide Filter/c LatentFilter/c index/c)
(df Bot () [#:fold-rhs #:base])
(df TypeFilter ([t Type?] [p (listof PathElem?)] [v identifier?])
@ -17,11 +31,22 @@
(combine-frees (map free-idxs* (cons t p)))]
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
(df FilterSet ([thn (listof (and/c Filter? (not/c FilterSet?)))]
[els (listof (and/c Filter? (not/c FilterSet?)))])
(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))])
[#: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)
(list/c)]
[else (listof Filter/c)])]
[e (cond [(ormap Bot? e)
(list/c Bot?)]
[(ormap Bot? t)
(list/c)]
[else (listof Filter/c)])])
()
[result FilterSet?])])
(define index/c (or/c natural-number/c keyword?))
@ -35,8 +60,19 @@
[#: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)])
(dlf LFilterSet ([thn (listof (and/c LatentFilter? (not/c LFilterSet?)))]
[els (listof (and/c LatentFilter? (not/c LFilterSet?)))])
(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))])
[#: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)
(list/c)]
[else (listof LatentFilter/c)])]
[e (cond [(ormap LBot? e)
(list/c LBot?)]
[(ormap LBot? t)
(list/c)]
[else (listof LatentFilter/c)])])
()
[result LFilterSet?])])

2
collects/typed-scheme/rep/rep-utils.ss
View File

@ -95,7 +95,7 @@
[provides (if #'no-provide?
#'(begin)
#`(begin
(provide ex pred acc ...)
(provide #;nm ex pred acc ...)
(p/c (rename *maker maker *maker-cnt))))]
[intern
(let ([mk (lambda (int)

2
collects/typed-scheme/typecheck/signatures.ss
View File

@ -2,7 +2,7 @@
(require scheme/unit scheme/contract "../utils/utils.ss")
(require (rep type-rep)
(utils unit-utils)
(private type-utils))
(types utils))
(provide (all-defined-out))
(define-signature typechecker^

62
collects/typed-scheme/typecheck/tc-metafunctions.ss Normal file
View File

@ -0,0 +1,62 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (rename-in (types subtype convenience remove-intersect)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(rep type-rep)
scheme/contract scheme/match
stxclass/util
(for-syntax scheme/base))
;; 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)]
[(memq (make-LBot) l2)
(make-LFilterSet null (list (make-LBot)))]
[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)]))
(define/contract (abstract-filter x idx fs)
(-> identifier? index/c FilterSet? LFilterSet?)
(match fs
[(FilterSet: f+ f-)
(lcombine
(apply append (for/list ([f f+]) (abo x idx f)))
(apply append (for/list ([f f-]) (abo x idx f))))]))
(define/contract (abo x idx f)
(-> identifier? index/c Filter/c (or/c '() (list/c LatentFilter/c)))
(define-match-expander =x
(lambda (stx) #'(? (lambda (id) (free-identifier=? id x)))))
(match f
[(Bot:) (list (make-LBot))]
[(TypeFilter: t p (=x)) (list (make-LTypeFilter t p))]
[(NotTypeFilter: t p (=x)) (list (make-LNotTypeFilter t p))]
[_ null]))
(define/contract (apply-filter lfs t o)
(-> LFilterSet? Type/c Object?)
(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))))]))
(define/contract (apo lf s o)
(-> LatentFilter/c Type/c Object? (or/c '() (list/c Filter/c)))
(match* (lf s o)
[((LBot:) _ _) (list (make-Bot))]
[((LNotTypeFilter: (? (lambda (t) (subtype s t))) (list) _) _ _) (list (make-Bot))]
[((LTypeFilter: (? (lambda (t) (not (overlap s t)))) (list) _) _ _) (list (make-Bot))]
[(_ _ (Empty:)) null]
[((LTypeFilter: t pi* _) _ (Path: pi x)) (make-TypeFilter t (append pi* pi) x)]
[((LNotTypeFilter: t pi* _) _ (Path: pi x)) (make-NotTypeFilter t (append pi* pi) x)]))

5
collects/typed-scheme/typecheck/tc-toplevel.ss
View File

@ -8,9 +8,10 @@
"signatures.ss"
"tc-structs.ss"
(rep type-rep)
(private type-utils type-effect-convenience parse-type type-annotation mutated-vars type-contract)
(types utils convenience)
(private parse-type type-annotation type-contract)
(env type-env init-envs type-name-env type-alias-env)
(utils tc-utils)
(utils tc-utils mutated-vars)
"provide-handling.ss"
"def-binding.ss"
(for-template

5
collects/typed-scheme/typed-scheme.ss
View File

@ -2,10 +2,11 @@
(require (rename-in "utils/utils.ss" [infer r:infer]))
(require (private #;base-env base-types)
(require (private base-types)
(for-syntax
scheme/base
(private type-utils type-contract type-effect-convenience)
(private type-contract)
(types utils convenience)
(typecheck typechecker provide-handling)
(env type-environments type-name-env type-alias-env)
(r:infer infer)

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

@ -66,10 +66,10 @@
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
(define N (make-Base 'Number #'number?))
(define -Number (make-Base 'Number #'number?))
(define -Integer (make-Base 'Integer #'exact-integer?))
(define B (make-Base 'Boolean #'boolean?))
(define Sym (make-Base 'Symbol #'symbol?))
(define -Boolean (make-Base 'Boolean #'boolean?))
(define -Symbol (make-Base 'Symbol #'symbol?))
(define -Void (make-Base 'Void #'void?))
(define -Bytes (make-Base 'Bytes #'bytes?))
(define -Regexp (make-Base 'Regexp #'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?))))
@ -99,24 +99,24 @@
(define Any-Syntax
(-mu x
(-Syntax (*Un
N
B
Sym
-Number
-Boolean
-Symbol
-String
-Keyword
(-mu y (*Un (-val '()) (-pair x (*Un x y))))
(make-Vector x)
(make-Box x)))))
(define Ident (-Syntax Sym))
(define Ident (-Syntax -Symbol))
(define -Sexp (-mu x (*Un (-val null) N B Sym -String (-pair x x))))
(define -Sexp (-mu x (*Un (-val null) -Number -Boolean -Symbol -String (-pair x x))))
(define -Port (*Un -Output-Port -Input-Port))
(define -Pathlike (*Un -String -Path))
(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
(define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String))
(define -Byte N)
(define -Byte -Number)
(define -no-lfilter (make-LFilterSet null null))
(define -no-filter (make-FilterSet null null))
@ -249,7 +249,7 @@
(case-lambda
[(in out t)
(->* in out : (-LFS (list (-filter t)) (list (-not-filter t))))]
[(t) (make-pred-ty (list Univ) B t)]))
[(t) (make-pred-ty (list Univ) -Boolean t)]))
(define (opt-fn args opt-args result)