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

checkpoint

Browse Source 
svn: r12954

original commit: ed48078523c1282d0df9f2133cfca50102f8849b
This commit is contained in:
Sam Tobin-Hochstadt 2008-12-30 19:47:21 +00:00
commit 76b262cb20
7 changed files with 33 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -100,9 +100,9 @@
(define (cgen/eff V X t s)
(match* (t s)
[(e e) (empty-cset X)]
[((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: s))
[((Latent-Restrict-Effect: t k) (Latent-Restrict-Effect: s k))
(cset-meet (cgen V X t s) (cgen V X s t))]
[((Latent-Remove-Effect: t) (Latent-Remove-Effect: s))
[((Latent-Remove-Effect: t k) (Latent-Remove-Effect: s k))
(cset-meet (cgen V X t s) (cgen V X s t))]
[(_ _) (fail! t s)]))

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

@ -107,8 +107,8 @@
[filter (-poly (a b) (cl->*
((a . -> . B
:
(list (make-Latent-Restrict-Effect b))
(list (make-Latent-Remove-Effect b)))
(list (make-Latent-Restrict-Effect b 0))
(list (make-Latent-Remove-Effect b 0)))
(-lst a)
. -> .
(-lst b))

10
collects/typed-scheme/private/subtype.ss
View File

@ -81,15 +81,15 @@
(ormap (lambda (e) (arr-subtype*/no-fail A e s)) ts))
(define (sub-eff e1 e2)
(match (list e1 e2)
[(list e e) #t]
[(list (Latent-Restrict-Effect: t) (Latent-Restrict-Effect: t*))
(match* (e1 e2)
[(e e) #t]
[((Latent-Restrict-Effect: t k) (Latent-Restrict-Effect: t* k))
(and (subtype t t*)
(subtype t* t))]
[(list (Latent-Remove-Effect: t) (Latent-Remove-Effect: t*))
[((Latent-Remove-Effect: t k) (Latent-Remove-Effect: t* k))
(and (subtype t t*)
(subtype t* t))]
[else #f]))
[(_ _) #f]))
;(trace sub-eff)

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

@ -38,10 +38,10 @@
(define ((add-var v) eff)
(match eff
[(Latent-Var-True-Effect:) (-vet v)]
[(Latent-Var-False-Effect:) (-vef v)]
[(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
[(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
[(Latent-Var-True-Effect: k) (-vet v)]
[(Latent-Var-False-Effect: k) (-vef v)]
[(Latent-Restrict-Effect: t k) (make-Restrict-Effect t v)]
[(Latent-Remove-Effect: t k) (make-Remove-Effect t v)]
[(True-Effect:) eff]
[(False-Effect:) eff]
[_ (int-err "can't add var ~a to effect ~a" v eff)]))
@ -208,7 +208,7 @@
(define make-pred-ty
(case-lambda
[(in out t)
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
(->* in out : (list (make-Latent-Restrict-Effect t 0)) (list (make-Latent-Remove-Effect t 0)))]
[(t) (make-pred-ty (list Univ) B t)]))
(define -Pathlike (*Un -Path -String))

13
collects/typed-scheme/private/type-effect-printer.ss
View File

@ -32,10 +32,10 @@
(match c
[(Restrict-Effect: t v) (fp "(restrict ~a ~a)" t (syntax-e v))]
[(Remove-Effect: t v) (fp "(remove ~a ~a)" t (syntax-e v))]
[(Latent-Restrict-Effect: t) (fp "(restrict ~a)" t)]
[(Latent-Remove-Effect: t) (fp "(remove ~a)" t)]
[(Latent-Var-True-Effect:) (fp "(var #t)")]
[(Latent-Var-False-Effect:) (fp "(var #f)")]
[(Latent-Restrict-Effect: t k) (fp "(restrict ~a ~a)" t k)]
[(Latent-Remove-Effect: t k) (fp "(remove ~a ~a)" t k)]
[(Latent-Var-True-Effect: k) (fp "(var #t ~a)" k)]
[(Latent-Var-False-Effect: k) (fp "(var #f ~a)" k)]
[(True-Effect:) (fp "T")]
[(False-Effect:) (fp "F")]
[(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))]
@ -64,9 +64,10 @@
(when drest
(fp "~a ... ~a " (car drest) (cdr drest)))
(fp "-> ~a" rng)
(match* (thn-eff els-eff)
(match* (thn-eff els-eff)
[((list) (list)) (void)]
[((list (Latent-Restrict-Effect: t)) (list (Latent-Remove-Effect: t))) (fp " : ~a" t)]
[((list (Latent-Restrict-Effect: t 0)) (list (Latent-Remove-Effect: t 0))) (fp " : ~a" t)]
[((list (Latent-Restrict-Effect: t k)) (list (Latent-Remove-Effect: t k))) (fp " : ~a_~a" t k)]
[(_ _) (fp " : ~a ~a" thn-eff els-eff)])
(fp ")")]))
(define (tuple? t)

14
collects/typed-scheme/rep/effect-rep.ss
View File

@ -27,13 +27,19 @@
[#:fold-rhs (*Remove-Effect (type-rec-id t) v)])
;; t is a Type
(de Latent-Restrict-Effect (t))
;; k is a nat
(de Latent-Restrict-Effect (t k) [#:frees (free-vars* t) (free-idxs* t)]
[#:fold-rhs (*Latent-Restrict-Effect (type-rec-id t) k)])
;; t is a Type
(de Latent-Remove-Effect (t))
;; k is a nat
(de Latent-Remove-Effect (t k) [#:frees (free-vars* t) (free-idxs* t)]
[#:fold-rhs (*Latent-Remove-Effect (type-rec-id t) k)])
(de Latent-Var-True-Effect () [#:frees #f] [#:fold-rhs #:base])
;; k is a nat
(de Latent-Var-True-Effect (k) [#:frees #f] [#:fold-rhs #:base])
(de Latent-Var-False-Effect () [#:frees #f] [#:fold-rhs #:base])
;; k is a nat
(de Latent-Var-False-Effect (k) [#:frees #f] [#:fold-rhs #:base])
;; could also have latent true/false effects, but seems pointless

2
collects/typed-scheme/ts-guide.scrbl
View File

@ -14,6 +14,8 @@
@author["Sam Tobin-Hochstadt"]
@section-index["typechecking"]
Typed Scheme is a Scheme-like language, with a type system that
supports common Scheme programming idioms. Explicit type declarations
are required --- that is, there is no type inference. The language