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

Reorg to separate out files.

Browse Source 
svn: r11857
This commit is contained in:
Sam Tobin-Hochstadt 2008-09-24 19:56:48 +00:00
parent 9b6a8d2e5a
commit 15e7be91f5
7 changed files with 593 additions and 558 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/typed-scheme/main.ss
View File

@ -1,10 +1,12 @@
#lang s-exp "minimal.ss" #lang s-exp "minimal.ss"
(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app) (providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app)
(except "private/prims.ss")) (except "private/prims.ss"))
(basics #%module-begin (basics #%module-begin
#%top-interaction #%top-interaction
lambda lambda
#%app)) #%app))
(require "private/base-env.ss" "private/base-special-env.ss")
(provide (rename-out [with-handlers: with-handlers])) (provide (rename-out [with-handlers: with-handlers]))

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

@ -5,7 +5,7 @@
(require (for-syntax scheme/base)) (require (for-syntax scheme/base))
(define-for-syntax ts-mod "typed-scheme.ss") (define-for-syntax ts-mod 'typed-scheme/typed-scheme)
(define-syntax (providing stx) (define-syntax (providing stx)
(syntax-case stx (libs from basics except) (syntax-case stx (libs from basics except)

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

@ -1,154 +1,72 @@
#lang scheme/base #lang s-exp "env-lang.ss"
;; these are libraries providing functions we add types to that are not in scheme/base
(require (require
"extra-procs.ss"
"../utils/utils.ss"
(only-in scheme/list cons? take drop add-between last filter-map) (only-in scheme/list cons? take drop add-between last filter-map)
(only-in rnrs/lists-6 fold-left) (only-in rnrs/lists-6 fold-left)
'#%paramz '#%paramz
(only-in scheme/match/runtime match:error)
scheme/promise scheme/promise
string-constants/string-constant) (only-in scheme/match/runtime match:error))
[raise (Univ . -> . (Un))]
(car (-poly (a b) (cl-> [((-pair a b)) a]
;; these are all for constructing the types given to variables [((make-Listof a)) a])))
(require (for-syntax [first (-poly (a b) (cl-> [((-pair a b)) a]
scheme/base [((make-Listof a)) a]))]
(env init-envs) [second (-poly (a b c)
(except-in (rep effect-rep type-rep) make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"
(typecheck tc-structs)))
(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])
())
(d-s exn ([message : -String] [continuation-marks : Univ]) ())
(d-s (exn:fail exn) () (-String Univ))
(d-s (exn:fail:read exn:fail) ([srclocs : (-lst Univ)]) (-String Univ))
)
(provide (for-syntax initial-env initialize-others))
(define-syntax (define-initial-env stx)
(syntax-case stx ()
[(_ initial-env make-promise-ty language-ty qq-append-ty [id ty] ...)
(with-syntax ([(_ make-promise . _)
(local-expand #'(delay 3)
'expression
null)]
[language
(local-expand #'(this-language)
'expression
null)]
[(_ qq-append . _)
(local-expand #'`(,@'() 1)
'expression
null)])
#`(define-for-syntax initial-env
(make-env
[make-promise make-promise-ty]
[language language-ty]
[qq-append qq-append-ty]
[id ty] ...)))]))
(define-for-syntax (one-of/c . args)
(apply Un (map -val args)))
(define-initial-env initial-env
;; make-promise
(-poly (a) (-> (-> a) (-Promise a)))
;; language
Sym
;; qq-append
(-poly (a b)
(cl->*
(-> (-lst a) (-val '()) (-lst a))
(-> (-lst a) (-lst b) (-lst (*Un a b)))))
#|;; language
[(expand '(this-language))
Sym
string-constants/string-constant]
;; make-promise
[(cadr (syntax->list (expand '(delay 3))))
(-poly (a) (-> (-> a) (-Promise a)))
scheme/promise]
;; qq-append
[(cadr (syntax->list (expand '`(,@'() 1))))
(-poly (a b)
(cl->*
(-> (-lst a) (-val '()) (-lst a))
(-> (-lst a) (-lst b) (-lst (*Un a b)))))]
|#
[raise (Univ . -> . (Un))]
(car (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v a)]
[((make-Listof (-v a))) (-v a)])))
[first (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v a)]
[((make-Listof (-v a))) (-v a)]))]
[second (-poly (a b c)
(cl-> (cl->
[((-pair a (-pair b c))) b] [((-pair a (-pair b c))) b]
[((-lst a)) a]))] [((-lst a)) a]))]
[third (-poly (a b c d) [third (-poly (a b c d)
(cl-> (cl->
[((-pair a (-pair b (-pair c d)))) c] [((-pair a (-pair b (-pair c d)))) c]
[((-lst a)) a]))] [((-lst a)) a]))]
[fourth (-poly (a) ((-lst a) . -> . a))] [fourth (-poly (a) ((-lst a) . -> . a))]
[fifth (-poly (a) ((-lst a) . -> . a))] [fifth (-poly (a) ((-lst a) . -> . a))]
[sixth (-poly (a) ((-lst a) . -> . a))] [sixth (-poly (a) ((-lst a) . -> . a))]
[rest (-poly (a) ((-lst a) . -> . (-lst a)))] [rest (-poly (a) ((-lst a) . -> . (-lst a)))]
(cadr (cadr
(-poly (a b c) (-poly (a b c)
(cl-> (cl->
[((-pair a (-pair b c))) b] [((-pair a (-pair b c))) b]
[((-lst a)) a]))) [((-lst a)) a])))
(caddr (-poly (a) (-> (-lst a) a))) (caddr (-poly (a) (-> (-lst a) a)))
(cadddr (-poly (a) (-> (-lst a) a))) (cadddr (-poly (a) (-> (-lst a) a)))
(cdr (make-Poly (list 'a 'b) (cl-> [((-pair (-v a) (-v b))) (-v b)] (cdr (-poly (a b) (cl-> [((-pair a b)) b]
[((make-Listof (-v a))) (make-Listof (-v a))]))) [((make-Listof a)) (make-Listof a)])))
(cddr (make-Poly (list 'a) (-> (make-Listof (-v a)) (make-Listof (-v a))))) (cddr (-poly (a) (-> (make-Listof a) (make-Listof a))))
(cdddr (make-Poly (list 'a) (-> (make-Listof (-v a)) (make-Listof (-v a))))) (cdddr (-poly (a) (-> (make-Listof a) (make-Listof a))))
(cons (-poly (a b) (cons (-poly (a b)
(cl-> [(a (-lst a)) (-lst a)] (cl-> [(a (-lst a)) (-lst a)]
[(a b) (-pair a b)]))) [(a b) (-pair a b)])))
[*cons (-poly (a b) (cl-> [*cons (-poly (a b) (cl->
[(a b) (-pair a b)] [(a b) (-pair a b)]
[(a (-lst a)) (-lst a)]))] [(a (-lst a)) (-lst a)]))]
[*list? (make-pred-ty (-lst Univ))] [*list? (make-pred-ty (-lst Univ))]
(null? (make-pred-ty (-val null))) (null? (make-pred-ty (-val null)))
(eof-object? (make-pred-ty (-val eof))) (eof-object? (make-pred-ty (-val eof)))
[null (-val null)] [null (-val null)]
(number? (make-pred-ty N)) (number? (make-pred-ty N))
[char? (make-pred-ty -Char)] [char? (make-pred-ty -Char)]
(integer? (make-pred-ty -Integer)) (integer? (make-pred-ty -Integer))
(boolean? (make-pred-ty B)) (boolean? (make-pred-ty B))
(add1 (cl->* (add1 (cl->*
(-> -Integer -Integer) (-> -Integer -Integer)
(-> N N))) (-> N N)))
(sub1 (cl->* (sub1 (cl->*
#;(-> -Integer -Integer) #;(-> -Integer -Integer)
(-> N N))) (-> N N)))
(eq? (-> Univ Univ B)) (eq? (-> Univ Univ B))
(eqv? (-> Univ Univ B)) (eqv? (-> Univ Univ B))
(equal? (-> Univ Univ B)) (equal? (-> Univ Univ B))
(even? (-> N B)) (even? (-> N B))
[assert (-poly (a) (-> (*Un a (-val #f)) a))] [assert (-poly (a) (-> (*Un a (-val #f)) a))]
[gensym (cl-> [(Sym) Sym] [gensym (cl-> [(Sym) Sym]
[() Sym])] [() Sym])]
[string-append (->* null -String -String)] [string-append (->* null -String -String)]
[open-input-string (-> -String -Input-Port)] [open-input-string (-> -String -Input-Port)]
[open-output-file [open-output-file
(->key -Pathlike (->key -Pathlike
#:mode (one-of/c 'binary 'text) #f #:mode (one-of/c 'binary 'text) #f
#:exists (one-of/c 'error 'append 'update 'can-update #:exists (one-of/c 'error 'append 'update 'can-update
@ -156,43 +74,43 @@
'must-truncate 'truncate/replace) 'must-truncate 'truncate/replace)
#f #f
-Output-Port)] -Output-Port)]
[read (cl-> [read (cl->
[(-Port) -Sexp] [(-Port) -Sexp]
[() -Sexp])] [() -Sexp])]
[ormap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))] [ormap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))]
[andmap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))] [andmap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))]
[newline (cl-> [() -Void] [newline (cl-> [() -Void]
[(-Port) -Void])] [(-Port) -Void])]
[not (-> Univ B)] [not (-> Univ B)]
[floor (-> N N)] [floor (-> N N)]
[box (-poly (a) (a . -> . (make-Box a)))] [box (-poly (a) (a . -> . (-box a)))]
[unbox (-poly (a) ((make-Box a) . -> . a))] [unbox (-poly (a) ((-box a) . -> . a))]
[set-box! (-poly (a) ((make-Box a) a . -> . -Void))] [set-box! (-poly (a) ((-box a) a . -> . -Void))]
[box? (make-pred-ty (make-Box Univ))] [box? (make-pred-ty (-box Univ))]
[cons? (make-pred-ty (-pair Univ Univ))] [cons? (make-pred-ty (-pair Univ Univ))]
[pair? (make-pred-ty (-pair Univ Univ)) #;(-poly (a b) (make-pred-ty (-pair a b)))] [pair? (make-pred-ty (-pair Univ Univ)) #;(-poly (a b) (make-pred-ty (-pair a b)))]
[empty? (make-pred-ty (-val null))] [empty? (make-pred-ty (-val null))]
[empty (-val null)] [empty (-val null)]
[string? (make-pred-ty -String)] [string? (make-pred-ty -String)]
[string (->* '() -Char -String)] [string (->* '() -Char -String)]
[symbol? (make-pred-ty Sym)] [symbol? (make-pred-ty Sym)]
[list? (make-pred-ty (-lst Univ))] [list? (make-pred-ty (-lst Univ))]
[list (-poly (a) (->* '() a (-lst a)))] [list (-poly (a) (->* '() a (-lst a)))]
[procedure? (make-pred-ty (make-Function (list (make-top-arr))))] [procedure? (make-pred-ty (make-Function (list (make-top-arr))))]
[map (-polydots (c a b) ((list ((list a) (b b) . ->... . c) (-lst a)) [map (-polydots (c a b) ((list ((list a) (b b) . ->... . c) (-lst a))
((-lst b) b) . ->... .(-lst c)))] ((-lst b) b) . ->... .(-lst c)))]
[for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a)) [for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a))
((-lst b) b) . ->... . -Void))] ((-lst b) b) . ->... . -Void))]
[fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a)) [fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
((-lst b) b) . ->... . c))] ((-lst b) b) . ->... . c))]
[fold-right (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a)) [fold-right (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
((-lst b) b) . ->... . c))] ((-lst b) b) . ->... . c))]
[foldl [foldl
(-poly (a b c) (-poly (a b c)
(cl-> [((a b . -> . b) b (make-Listof a)) b] (cl-> [((a b . -> . b) b (make-Listof a)) b]
[((a b c . -> . c) c (make-Listof a) (make-Listof b)) c]))] [((a b c . -> . c) c (make-Listof a) (make-Listof b)) c]))]
[foldr (-poly (a b c) ((a b . -> . b) b (-lst a) . -> . b))] [foldr (-poly (a b c) ((a b . -> . b) b (-lst a) . -> . b))]
[filter (-poly (a b) (cl->* [filter (-poly (a b) (cl->*
((a . -> . B ((a . -> . B
: :
(list (make-Latent-Restrict-Effect b)) (list (make-Latent-Restrict-Effect b))
@ -201,20 +119,20 @@
. -> . . -> .
(-lst b)) (-lst b))
((a . -> . B) (-lst a) . -> . (-lst a))))] ((a . -> . B) (-lst a) . -> . (-lst a))))]
[filter-map (-polydots (c a b) [filter-map (-polydots (c a b)
((list ((list
((list a) (b b) . ->... . (-opt c)) ((list a) (b b) . ->... . (-opt c))
(-lst a)) (-lst a))
((-lst b) b) . ->... . (-lst c)))] ((-lst b) b) . ->... . (-lst c)))]
[take (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] [take (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
[drop (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] [drop (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
[last (-poly (a) ((-lst a) . -> . a))] [last (-poly (a) ((-lst a) . -> . a))]
[add-between (-poly (a b) ((-lst a) b . -> . (-lst (Un a b))))] [add-between (-poly (a b) ((-lst a) b . -> . (-lst (Un a b))))]
[remove* (-poly (a b) [remove* (-poly (a b)
(cl-> [((-lst a) (-lst a)) (-lst a)] (cl-> [((-lst a) (-lst a)) (-lst a)]
[((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))] [((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))]
(error (error
(make-Function (list (make-Function (list
(make-arr null (Un)) (make-arr null (Un))
(make-arr (list Sym -String) (Un) Univ) (make-arr (list Sym -String) (Un) Univ)
@ -222,142 +140,142 @@
(make-arr (list Sym) (Un))))) (make-arr (list Sym) (Un)))))
[namespace-variable-value [namespace-variable-value
(cl-> (cl->
[(Sym) Univ] [(Sym) Univ]
[(Sym B -Namespace (-> Univ)) Univ])] [(Sym B -Namespace (-> Univ)) Univ])]
(match:error (Univ . -> . (Un))) (match:error (Univ . -> . (Un)))
(display (display
(cl-> (cl->
[(Univ) -Void] [(Univ) -Void]
[(Univ -Port) -Void])) [(Univ -Port) -Void]))
[void (->* '() Univ -Void)] [void (->* '() Univ -Void)]
[void? (make-pred-ty -Void)] [void? (make-pred-ty -Void)]
[printf (->* (list -String) Univ -Void)] [printf (->* (list -String) Univ -Void)]
[fprintf (->* (list -Output-Port -String) Univ -Void)] [fprintf (->* (list -Output-Port -String) Univ -Void)]
[format (->* (list -String) Univ -String)] [format (->* (list -String) Univ -String)]
(fst (make-Poly (list 'a 'b) (-> (-pair (-v a) (-v b)) (-v a)))) (fst (-poly (a b) (-> (-pair a b) a)))
(snd (make-Poly (list 'a 'b) (-> (-pair (-v a) (-v b)) (-v b)))) (snd (-poly (a b) (-> (-pair a b) b)))
(= (->* (list N N) N B)) (= (->* (list N N) N B))
(>= (->* (list N N) N B)) (>= (->* (list N N) N B))
(< (->* (list N N) N B)) (< (->* (list N N) N B))
(<= (->* (list N N) N B)) (<= (->* (list N N) N B))
[> (->* (list N) N B)] [> (->* (list N) N B)]
(zero? (N . -> . B)) (zero? (N . -> . B))
(* (cl->* (->* '() -Integer -Integer) (->* '() N N))) (* (cl->* (->* '() -Integer -Integer) (->* '() N N)))
(/ (cl->* (->* (list N) N N))) (/ (cl->* (->* (list N) N N)))
(+ (cl->* (->* '() -Integer -Integer) (->* '() N N))) (+ (cl->* (->* '() -Integer -Integer) (->* '() N N)))
(- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))) (- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N)))
(max (->* (list N) N N)) (max (->* (list N) N N))
(min (->* (list N) N N)) (min (->* (list N) N N))
[vector-ref [vector-ref
(make-Poly (list 'a) ((make-Vector (-v a)) N . -> . (-v a)))] (-poly (a) ((-vec a) N . -> . a))]
[build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (make-Vector a)))] [build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (-vec a)))]
[build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))] [build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))]
[reverse (make-Poly '(a) (-> (make-Listof (-v a)) (make-Listof (-v a))))] [reverse (-poly (a) (-> (make-Listof a) (make-Listof a)))]
[append (-poly (a) (->* (list) (-lst a) (-lst a)))] [append (-poly (a) (->* (list) (-lst a) (-lst a)))]
[length (make-Poly '(a) (-> (make-Listof (-v a)) -Integer))] [length (-poly (a) (-> (make-Listof a) -Integer))]
[memq (make-Poly (list 'a) (-> (-v a) (make-Listof (-v a)) (-opt (make-Listof (-v a)))))] [memq (-poly (a) (-> a (make-Listof a) (-opt (make-Listof a))))]
[memv (make-Poly (list 'a) (-> (-v a) (make-Listof (-v a)) (-opt (make-Listof (-v a)))))] [memv (-poly (a) (-> a (make-Listof a) (-opt (make-Listof a))))]
[memf (-poly (a) ((a . -> . B) (-lst a) . -> . (-opt (-lst a))))] [memf (-poly (a) ((a . -> . B) (-lst a) . -> . (-opt (-lst a))))]
[member [member
(-poly (a) (a (-lst a) . -> . (-opt (-lst a))))] (-poly (a) (a (-lst a) . -> . (-opt (-lst a))))]
[findf (-poly (a) ((a . -> . B) (-lst a) . -> . (-opt a)))] [findf (-poly (a) ((a . -> . B) (-lst a) . -> . (-opt a)))]
[string<? (->* (list -String -String) -String B)] [string<? (->* (list -String -String) -String B)]
[string>? (->* (list -String -String) -String B)] [string>? (->* (list -String -String) -String B)]
[string=? (->* (list -String -String) -String B)] [string=? (->* (list -String -String) -String B)]
[char=? (->* (list -Char -Char) -Char B)] [char=? (->* (list -Char -Char) -Char B)]
[char<=? (->* (list -Char -Char) -Char B)] [char<=? (->* (list -Char -Char) -Char B)]
[char>=? (->* (list -Char -Char) -Char B)] [char>=? (->* (list -Char -Char) -Char B)]
[char<? (->* (list -Char -Char) -Char B)] [char<? (->* (list -Char -Char) -Char B)]
[char>? (->* (list -Char -Char) -Char B)] [char>? (->* (list -Char -Char) -Char B)]
[char-ci=? (->* (list -Char -Char) -Char B)] [char-ci=? (->* (list -Char -Char) -Char B)]
[char-ci<=? (->* (list -Char -Char) -Char B)] [char-ci<=? (->* (list -Char -Char) -Char B)]
[char-ci>=? (->* (list -Char -Char) -Char B)] [char-ci>=? (->* (list -Char -Char) -Char B)]
[char-ci>? (->* (list -Char -Char) -Char B)] [char-ci>? (->* (list -Char -Char) -Char B)]
[char-ci<? (->* (list -Char -Char) -Char B)] [char-ci<? (->* (list -Char -Char) -Char B)]
[string<=? (->* (list -String -String) -String B)] [string<=? (->* (list -String -String) -String B)]
[string>=? (->* (list -String -String) -String B)] [string>=? (->* (list -String -String) -String B)]
[string-ci<? (->* (list -String -String) -String B)] [string-ci<? (->* (list -String -String) -String B)]
[string-ci>? (->* (list -String -String) -String B)] [string-ci>? (->* (list -String -String) -String B)]
[string-ci=? (->* (list -String -String) -String B)] [string-ci=? (->* (list -String -String) -String B)]
[string-ci<=? (->* (list -String -String) -String B)] [string-ci<=? (->* (list -String -String) -String B)]
[string-ci>=? (->* (list -String -String) -String B)] [string-ci>=? (->* (list -String -String) -String B)]
[string-upcase (-> -String -String)] [string-upcase (-> -String -String)]
[string-downcase (-> -String -String)] [string-downcase (-> -String -String)]
[string-titlecase (-> -String -String)] [string-titlecase (-> -String -String)]
[string-foldcase (-> -String -String)] [string-foldcase (-> -String -String)]
[string-normalize-nfd (-> -String -String)] [string-normalize-nfd (-> -String -String)]
[string-normalize-nfkd (-> -String -String)] [string-normalize-nfkd (-> -String -String)]
[string-normalize-nfc (-> -String -String)] [string-normalize-nfc (-> -String -String)]
[string-normalize-nfkc (-> -String -String)] [string-normalize-nfkc (-> -String -String)]
[string-ref (-> -String N -Char)] [string-ref (-> -String N -Char)]
[substring (cl->* [substring (cl->*
(-> -String N -String) (-> -String N -String)
(-> -String N N -String))] (-> -String N N -String))]
[string->path (-> -String -Path)] [string->path (-> -String -Path)]
[file-exists? (-> -Pathlike B)] [file-exists? (-> -Pathlike B)]
[assq (-poly (a) (-> Univ (-lst (-pair Univ a)) a))] [assq (-poly (a) (-> Univ (-lst (-pair Univ a)) a))]
[build-path ((list -Pathlike*) -Pathlike* . ->* . -Path)] [build-path ((list -Pathlike*) -Pathlike* . ->* . -Path)]
[string->number (-> -String (-opt N))] [string->number (-> -String (-opt N))]
[with-input-from-file [with-input-from-file
(-poly (a) (-poly (a)
(cl-> (cl->
[(-Pathlike (-> a)) a] [(-Pathlike (-> a)) a]
[(-Pathlike (-> a) Sym) a]))] [(-Pathlike (-> a) Sym) a]))]
[with-output-to-file [with-output-to-file
(-poly (a) (-poly (a)
(cl-> (cl->
[(-Pathlike (-> a)) a] [(-Pathlike (-> a)) a]
[(-Pathlike (-> a) Sym) a]))] [(-Pathlike (-> a) Sym) a]))]
[random (cl-> [random (cl->
[(-Integer) -Integer] [(-Integer) -Integer]
[() -Integer])] [() -Integer])]
[assoc (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))] [assoc (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[assf (-poly (a b) [assf (-poly (a b)
((a . -> . B) (-lst (-pair a b)) . -> . (-opt (-pair a b))))] ((a . -> . B) (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[list-ref (-poly (a) ((-lst a) -Integer . -> . a))] [list-ref (-poly (a) ((-lst a) -Integer . -> . a))]
[positive? (-> N B)] [positive? (-> N B)]
[negative? (-> N B)] [negative? (-> N B)]
[odd? (-> N B)] [odd? (-> N B)]
[even? (-> N B)] [even? (-> N B)]
[apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))] [apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))] [call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))] [call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
[quotient (-Integer -Integer . -> . -Integer)] [quotient (-Integer -Integer . -> . -Integer)]
[remainder (-Integer -Integer . -> . -Integer)] [remainder (-Integer -Integer . -> . -Integer)]
[quotient/remainder (-Integer -Integer . -> . (-values (list -Integer -Integer)))] [quotient/remainder (-Integer -Integer . -> . (-values (list -Integer -Integer)))]
;; parameter stuff ;; parameter stuff
[parameterization-key Sym] [parameterization-key Sym]
[extend-parameterization (-poly (a b) (-> Univ (-Param a b) a Univ))] [extend-parameterization (-poly (a b) (-> Univ (-Param a b) a Univ))]
[continuation-mark-set-first (-> (-opt -Cont-Mark-Set) Univ Univ)] [continuation-mark-set-first (-> (-opt -Cont-Mark-Set) Univ Univ)]
[make-parameter (-poly (a b) (cl-> [(a) (-Param a a)] [make-parameter (-poly (a b) (cl-> [(a) (-Param a a)]
[(b (a . -> . b)) (-Param a b)]))] [(b (a . -> . b)) (-Param a b)]))]
[current-directory (-Param -Pathlike -Path)] [current-directory (-Param -Pathlike -Path)]
[current-namespace (-Param -Namespace -Namespace)] [current-namespace (-Param -Namespace -Namespace)]
[print-struct (-Param B B)] [print-struct (-Param B B)]
[read-decimal-as-inexact (-Param B B)] [read-decimal-as-inexact (-Param B B)]
[current-command-line-arguments (-Param (make-Vector -String) (make-Vector -String))] [current-command-line-arguments (-Param (-vec -String) (-vec -String))]
;; regexp stuff ;; regexp stuff
[regexp-match [regexp-match
(cl-> (cl->
[((*Un -String -Regexp) -String) (-opt (-lst (-opt -String)))] [((*Un -String -Regexp) -String) (-opt (-lst (-opt -String)))]
[(-Pattern -String) (-opt (-lst (-opt (*Un -Bytes -String))))] [(-Pattern -String) (-opt (-lst (-opt (*Un -Bytes -String))))]
@ -373,142 +291,142 @@
[(-Pattern (*Un -Input-Port -Bytes) N (-opt N) (-opt -Output-Port)) (-lst (-opt -Bytes))])] [(-Pattern (*Un -Input-Port -Bytes) N (-opt N) (-opt -Output-Port)) (-lst (-opt -Bytes))])]
[number->string (N . -> . -String)] [number->string (N . -> . -String)]
[current-milliseconds (-> -Integer)] [current-milliseconds (-> -Integer)]
[modulo (cl->* (-Integer -Integer . -> . -Integer))] [modulo (cl->* (-Integer -Integer . -> . -Integer))]
;; errors ;; errors
[raise-type-error [raise-type-error
(cl-> (cl->
[(Sym -String Univ) (Un)] [(Sym -String Univ) (Un)]
[(Sym -String N (-lst Univ)) (Un)])] [(Sym -String N (-lst Univ)) (Un)])]
;; this is a hack ;; this is a hack
[match:error ((list) Univ . ->* . (Un))] [match:error ((list) Univ . ->* . (Un))]
[vector-set! (-poly (a) (-> (make-Vector a) N a -Void))] [vector-set! (-poly (a) (-> (-vec a) N a -Void))]
[vector->list (-poly (a) (-> (make-Vector a) (-lst a)))] [vector->list (-poly (a) (-> (-vec a) (-lst a)))]
[list->vector (-poly (a) (-> (-lst a) (make-Vector a)))] [list->vector (-poly (a) (-> (-lst a) (-vec a)))]
[exact? (N . -> . B)] [exact? (N . -> . B)]
[inexact? (N . -> . B)] [inexact? (N . -> . B)]
[expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))] [expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))]
[vector (-poly (a) (->* (list) a (make-Vector a)))] [vector (-poly (a) (->* (list) a (-vec a)))]
[real? (Univ . -> . B)] [real? (Univ . -> . B)]
[real-part (N . -> . N)] [real-part (N . -> . N)]
[imag-part (N . -> . N)] [imag-part (N . -> . N)]
[magnitude (N . -> . N)] [magnitude (N . -> . N)]
[angle (N . -> . N)] [angle (N . -> . N)]
[numerator (N . -> . -Integer)] [numerator (N . -> . -Integer)]
[denominator (N . -> . -Integer)] [denominator (N . -> . -Integer)]
[exact->inexact (N . -> . N)] [exact->inexact (N . -> . N)]
[inexact->exact (N . -> . N)] [inexact->exact (N . -> . N)]
[make-string [make-string
(cl-> (cl->
[(N) -String] [(N) -String]
[(N -Char) -String])] [(N -Char) -String])]
[arithmetic-shift (-Integer -Integer . -> . -Integer)] [arithmetic-shift (-Integer -Integer . -> . -Integer)]
[abs (N . -> . N)] [abs (N . -> . N)]
[substring (cl-> [(-String N) -String] [substring (cl-> [(-String N) -String]
[(-String N N) -String])] [(-String N N) -String])]
[string-length (-String . -> . N)] [string-length (-String . -> . N)]
[string-set! (-String N -Char . -> . -Void)] [string-set! (-String N -Char . -> . -Void)]
[make-vector [make-vector
(-poly (a) (-poly (a)
(cl-> (cl->
[(N) (make-Vector N)] [(N) (-vec N)]
[(N a) (make-Vector a)]))] [(N a) (-vec a)]))]
[file-exists? (-Pathlike . -> . B)] [file-exists? (-Pathlike . -> . B)]
[string->symbol (-String . -> . Sym)] [string->symbol (-String . -> . Sym)]
[symbol->string (Sym . -> . -String)] [symbol->string (Sym . -> . -String)]
[vector-length (-poly (a) ((make-Vector a) . -> . N))] [vector-length (-poly (a) ((-vec a) . -> . N))]
[call-with-input-file (-poly (a) [call-with-input-file (-poly (a)
(cl-> (cl->
[(-String (-Port . -> . a)) a] [(-String (-Port . -> . a)) a]
[(-String (-Port . -> . a) Sym) a]))] [(-String (-Port . -> . a) Sym) a]))]
[call-with-output-file (-poly (a) [call-with-output-file (-poly (a)
(cl-> (cl->
[(-String (-Port . -> . a)) a] [(-String (-Port . -> . a)) a]
[(-String (-Port . -> . a) Sym) a]))] [(-String (-Port . -> . a) Sym) a]))]
[current-output-port (-Param -Output-Port -Output-Port)] [current-output-port (-Param -Output-Port -Output-Port)]
[current-error-port (-Param -Output-Port -Output-Port)] [current-error-port (-Param -Output-Port -Output-Port)]
[current-input-port (-Param -Input-Port -Input-Port)] [current-input-port (-Param -Input-Port -Input-Port)]
[round (N . -> . N)] [round (N . -> . N)]
[seconds->date (N . -> . (make-Name #'date))] [seconds->date (N . -> . (make-Name #'date))]
[current-seconds (-> N)] [current-seconds (-> N)]
[sqrt (-> N N)] [sqrt (-> N N)]
[path->string (-> -Path -String)] [path->string (-> -Path -String)]
[link-exists? (-> -Pathlike B)] [link-exists? (-> -Pathlike B)]
[directory-exists? (-> -Pathlike B)] [directory-exists? (-> -Pathlike B)]
[file-exists? (-> -Pathlike B)] [file-exists? (-> -Pathlike B)]
[directory-list (cl-> [() (-lst -Path)] [directory-list (cl-> [() (-lst -Path)]
[(-Path) (-lst -Path)])] [(-Path) (-lst -Path)])]
[make-hash (-poly (a b) (-> (-HT a b)))] [make-hash (-poly (a b) (-> (-HT a b)))]
[make-hasheq (-poly (a b) (-> (-HT a b)))] [make-hasheq (-poly (a b) (-> (-HT a b)))]
[make-weak-hash (-poly (a b) (-> (-HT a b)))] [make-weak-hash (-poly (a b) (-> (-HT a b)))]
[make-weak-hasheq (-poly (a b) (-> (-HT a b)))] [make-weak-hasheq (-poly (a b) (-> (-HT a b)))]
[hash-set! (-poly (a b) ((-HT a b) a b . -> . -Void))] [hash-set! (-poly (a b) ((-HT a b) a b . -> . -Void))]
[hash-map (-poly (a b c) ((-HT a b) (a b . -> . c) . -> . (-lst c)))] [hash-map (-poly (a b c) ((-HT a b) (a b . -> . c) . -> . (-lst c)))]
[hash-ref (-poly (a b c) [hash-ref (-poly (a b c)
(cl-> (cl->
(((-HT a b) a) b) (((-HT a b) a) b)
(((-HT a b) a (-> c)) (*Un b c)) (((-HT a b) a (-> c)) (*Un b c))
(((-HT a b) a c) (*Un b c))))] (((-HT a b) a c) (*Un b c))))]
#;[hash-table-index (-poly (a b) ((-HT a b) a b . -> . -Void))] #;[hash-table-index (-poly (a b) ((-HT a b) a b . -> . -Void))]
[bytes (->* (list) N -Bytes)] [bytes (->* (list) N -Bytes)]
[bytes-ref (-> -Bytes N N)] [bytes-ref (-> -Bytes N N)]
[bytes-append (->* (list -Bytes) -Bytes -Bytes)] [bytes-append (->* (list -Bytes) -Bytes -Bytes)]
[subbytes (cl-> [subbytes (cl->
[(-Bytes N) -Bytes] [(-Bytes N) -Bytes]
[(-Bytes N N) -Bytes])] [(-Bytes N N) -Bytes])]
[bytes-length (-> -Bytes N)] [bytes-length (-> -Bytes N)]
[open-input-file (->key -Pathlike #:mode (Un (-val 'binary) (-val 'text)) #f -Input-Port)] [open-input-file (->key -Pathlike #:mode (Un (-val 'binary) (-val 'text)) #f -Input-Port)]
[close-input-port (-> -Input-Port -Void)] [close-input-port (-> -Input-Port -Void)]
[close-output-port (-> -Output-Port -Void)] [close-output-port (-> -Output-Port -Void)]
[read-line (cl-> [read-line (cl->
[() -String] [() -String]
[(-Input-Port) -String] [(-Input-Port) -String]
[(-Input-Port Sym) -String])] [(-Input-Port Sym) -String])]
[copy-file (-> -Pathlike -Pathlike -Void)] [copy-file (-> -Pathlike -Pathlike -Void)]
[bytes->string/utf-8 (-> -Bytes -String)] [bytes->string/utf-8 (-> -Bytes -String)]
[force (-poly (a) (-> (-Promise a) a))] [force (-poly (a) (-> (-Promise a) a))]
[bytes<? (->* (list -Bytes) -Bytes B)] [bytes<? (->* (list -Bytes) -Bytes B)]
[regexp-replace* [regexp-replace*
(cl->* (cl->*
(-Pattern (*Un -Bytes -String) (*Un -Bytes -String) . -> . -Bytes) (-Pattern (*Un -Bytes -String) (*Un -Bytes -String) . -> . -Bytes)
(-Pattern -String -String . -> . -String))] (-Pattern -String -String . -> . -String))]
[peek-char [peek-char
(cl->* (cl->*
[-> -Char] [-> -Char]
[-Input-Port . -> . -Char] [-Input-Port . -> . -Char]
[-Input-Port N . -> . -Char] [-Input-Port N . -> . -Char]
[N . -> . -Char])] [N . -> . -Char])]
[peek-byte [peek-byte
(cl->* (cl->*
[-> -Byte] [-> -Byte]
[-Input-Port . -> . -Byte] [-Input-Port . -> . -Byte]
[-Input-Port N . -> . -Byte] [-Input-Port N . -> . -Byte]
[N . -> . -Byte])] [N . -> . -Byte])]
[make-pipe [make-pipe
(cl->* (cl->*
[-> (-values (list -Input-Port -Output-Port))] [-> (-values (list -Input-Port -Output-Port))]
[N . -> . (-values (list -Input-Port -Output-Port))])] [N . -> . (-values (list -Input-Port -Output-Port))])]
[open-output-bytes [open-output-bytes
(cl->* (cl->*
[-> -Output-Port] [-> -Output-Port]
[Univ . -> . -Output-Port])] [Univ . -> . -Output-Port])]
[get-output-bytes [get-output-bytes
(cl->* (cl->*
[-Output-Port . -> . -Bytes] [-Output-Port . -> . -Bytes]
[-Output-Port Univ . -> . -Bytes] [-Output-Port Univ . -> . -Bytes]
@ -516,59 +434,50 @@
[-Output-Port Univ N N . -> . -Bytes] [-Output-Port Univ N N . -> . -Bytes]
[-Output-Port N . -> . -Bytes] [-Output-Port N . -> . -Bytes]
[-Output-Port N N . -> . -Bytes])] [-Output-Port N N . -> . -Bytes])]
#;[exn:fail? (-> Univ B)] #;[exn:fail? (-> Univ B)]
#;[exn:fail:read? (-> Univ B)] #;[exn:fail:read? (-> Univ B)]
[write (-> -Sexp -Void)] [write (-> -Sexp -Void)]
[open-output-string (-> -Output-Port)] [open-output-string (-> -Output-Port)]
;; FIXME - wrong ;; FIXME - wrong
[get-output-string (-> -Output-Port -String)] [get-output-string (-> -Output-Port -String)]
[make-directory (-> -Path -Void)] [make-directory (-> -Path -Void)]
[hash-for-each (-poly (a b c) [hash-for-each (-poly (a b c)
(-> (-HT a b) (-> a b c) -Void))] (-> (-HT a b) (-> a b c) -Void))]
[delete-file (-> -Pathlike -Void)] [delete-file (-> -Pathlike -Void)]
[make-namespace (cl->* (-> -Namespace) [make-namespace (cl->* (-> -Namespace)
(-> (*Un (-val 'empty) (-val 'initial)) -Namespace))] (-> (*Un (-val 'empty) (-val 'initial)) -Namespace))]
[make-base-namespace (-> -Namespace)] [make-base-namespace (-> -Namespace)]
[eval (-> -Sexp Univ)] [eval (-> -Sexp Univ)]
[exit (-> (Un))] [exit (-> (Un))]
[module->namespace (-> -Sexp -Namespace)] [module->namespace (-> -Sexp -Namespace)]
[current-namespace (-Param -Namespace -Namespace)] [current-namespace (-Param -Namespace -Namespace)]
;; syntax operations ;; syntax operations
[expand (-> (-Syntax Univ) (-Syntax Univ))] [expand (-> (-Syntax Univ) (-Syntax Univ))]
[expand-once (-> (-Syntax Univ) (-Syntax Univ))] [expand-once (-> (-Syntax Univ) (-Syntax Univ))]
[syntax-source (-poly (a) (-> (-Syntax a) Univ))] [syntax-source (-poly (a) (-> (-Syntax a) Univ))]
[syntax-position (-poly (a) (-> (-Syntax a) (-opt N)))] [syntax-position (-poly (a) (-> (-Syntax a) (-opt N)))]
[datum->syntax (cl->* [datum->syntax (cl->*
(-> (-opt (-Syntax Univ)) Sym (-Syntax Sym)) (-> (-opt (-Syntax Univ)) Sym (-Syntax Sym))
(-> (-opt (-Syntax Univ)) Univ (-Syntax Univ)))] (-> (-opt (-Syntax Univ)) Univ (-Syntax Univ)))]
[syntax->datum (-poly (a) (-> (-Syntax a) Univ))] [syntax->datum (-poly (a) (-> (-Syntax a) Univ))]
[syntax-e (-poly (a) (-> (-Syntax a) a))] [syntax-e (-poly (a) (-> (-Syntax a) a))]
[syntax-original? (-poly (a) (-> (-Syntax a) B))] [syntax-original? (-poly (a) (-> (-Syntax a) B))]
[identifier? (make-pred-ty (-Syntax Sym))] [identifier? (make-pred-ty (-Syntax Sym))]
[syntax? (make-pred-ty (-Syntax Univ))] [syntax? (make-pred-ty (-Syntax Univ))]
[syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a)) [syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a))
(-> (-Syntax Univ) Univ Univ)))] (-> (-Syntax Univ) Univ Univ)))]
[values (-polydots (a) (null (a a) . ->... . (make-ValuesDots null a 'a)))] [values (-polydots (a) (null (a a) . ->... . (make-ValuesDots null a 'a)))]
[call-with-values (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b))] [call-with-values (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b))]
[eof (-val eof)]
[read-accept-reader (-Param B B)]
)
(begin-for-syntax
#;(printf "running base-env~n")
(initialize-type-env initial-env)
(initialize-others))
[eof (-val eof)]
[read-accept-reader (-Param B B)]

83
collects/typed-scheme/private/base-special-env.ss Normal file
View File

@ -0,0 +1,83 @@
#lang scheme/base
;; these are libraries providing functions we add types to that are not in scheme/base
(require
"extra-procs.ss"
"../utils/utils.ss"
(only-in scheme/list cons? take drop add-between last filter-map)
(only-in rnrs/lists-6 fold-left)
'#%paramz
(only-in scheme/match/runtime match:error)
scheme/promise
string-constants/string-constant)
;; these are all for constructing the types given to variables
(require (for-syntax
scheme/base
(env init-envs)
(except-in (rep effect-rep type-rep) make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"
(typecheck tc-structs)))
(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])
())
(d-s exn ([message : -String] [continuation-marks : Univ]) ())
(d-s (exn:fail exn) () (-String Univ))
(d-s (exn:fail:read exn:fail) ([srclocs : (-lst Univ)]) (-String Univ))
)
(provide (for-syntax initial-env/special-case initialize-others initialize-type-env)
define-initial-env)
(define-syntax (define-initial-env stx)
(syntax-case stx ()
[(_ initial-env make-promise-ty language-ty qq-append-ty [id ty] ...)
(with-syntax ([(_ make-promise . _)
(local-expand #'(delay 3)
'expression
null)]
[language
(local-expand #'(this-language)
'expression
null)]
[(_ qq-append . _)
(local-expand #'`(,@'() 1)
'expression
null)])
#`(define-for-syntax initial-env
(make-env
[make-promise make-promise-ty]
[language language-ty]
[qq-append qq-append-ty]
[id ty] ...)))]))
(define-initial-env initial-env/special-case
;; make-promise
(-poly (a) (-> (-> a) (-Promise a)))
;; language
Sym
;; qq-append
(-poly (a b)
(cl->*
(-> (-lst a) (-val '()) (-lst a))
(-> (-lst a) (-lst b) (-lst (*Un a b))))))
(begin-for-syntax
(initialize-type-env initial-env/special-case)
(initialize-others))

34
collects/typed-scheme/private/env-lang.ss Normal file
View File

@ -0,0 +1,34 @@
#lang scheme/base
(require "../utils/utils.ss")
(require (for-syntax (private type-effect-convenience)
(env init-envs)
scheme/base
(except-in (rep effect-rep type-rep) make-arr)
"type-effect-convenience.ss"
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
"union.ss"))
(define-syntax (#%module-begin stx)
(syntax-case stx (require)
[(mb (require . args) [id ty] ...)
(begin
(unless (andmap identifier? (syntax->list #'(id ...)))
(raise-syntax-error #f "not all ids"))
#'(#%plain-module-begin
(begin
(require . args)
(define-for-syntax e
(make-env [id ty] ...))
(begin-for-syntax
(initialize-type-env e)))))]
[(mb . rest)
#'(mb (require) . rest)]))
(provide #%module-begin
require
(all-from-out scheme/base)
(for-syntax
(all-from-out scheme/base
"type-effect-convenience.ss"
"union.ss")))

9
collects/typed-scheme/private/type-effect-convenience.ss
View File

@ -13,7 +13,12 @@
(for-syntax macro-debugger/stxclass/stxclass) (for-syntax macro-debugger/stxclass/stxclass)
(for-syntax scheme/base)) (for-syntax scheme/base))
(provide (all-defined-out)) (provide (all-defined-out)
;; these should all eventually go away
make-Name make-ValuesDots make-Function make-top-arr make-Latent-Restrict-Effect make-Latent-Remove-Effect)
(define (one-of/c . args)
(apply Un (map -val args)))
(define (-vet id) (make-Var-True-Effect id)) (define (-vet id) (make-Var-True-Effect id))
(define (-vef id) (make-Var-False-Effect id)) (define (-vef id) (make-Var-False-Effect id))
@ -206,6 +211,8 @@
(define (-Tuple l) (define (-Tuple l)
(foldr -pair (-val '()) l)) (foldr -pair (-val '()) l))
(define -box make-Box)
(define -vec make-Vector)
(define Any-Syntax (define Any-Syntax
(-mu x (-mu x

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

@ -2,7 +2,7 @@
(require (rename-in "utils/utils.ss" [infer r:infer])) (require (rename-in "utils/utils.ss" [infer r:infer]))
(require (private base-env base-types) (require (private #;base-env base-types)
(for-syntax (for-syntax
scheme/base scheme/base
(private type-utils type-contract type-effect-convenience) (private type-utils type-contract type-effect-convenience)