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

changed the ->d contracts to ->i contracts

Browse Source 
original commit: d419e8c12a554d660a65198dd102bc03e01c93a8
This commit is contained in:
Robby Findler 2010-09-09 14:16:56 -05:00
commit 780c2159b8
11 changed files with 225 additions and 205 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

69
collects/typed-scheme/core.rkt Normal file
View File

@ -0,0 +1,69 @@
#lang racket/base
(require (rename-in "utils/utils.rkt" [infer r:infer])
(for-syntax racket/base)
(for-template racket/base)
(private with-types type-contract)
(except-in syntax/parse id)
racket/match unstable/syntax unstable/match
(optimizer optimizer)
(types utils convenience)
(typecheck typechecker provide-handling tc-toplevel)
(env type-name-env type-alias-env)
(r:infer infer)
(rep type-rep)
(except-in (utils utils tc-utils) infer)
(only-in (r:infer infer-dummy) infer-param)
"tc-setup.rkt")
(provide mb-core ti-core wt-core)
(define (mb-core stx)
(syntax-parse stx
[(mb (~optional (~and #:optimize (~bind [opt? #'#t]))) forms ...)
(let ([pmb-form (syntax/loc stx (#%plain-module-begin forms ...))])
(parameterize ([optimize? (or (optimize?) (attribute opt?))])
(tc-setup
stx pmb-form 'module-begin new-mod tc-module after-code
(with-syntax*
(;; pmb = #%plain-module-begin
[(pmb . body2) new-mod]
;; add in syntax property on useless expression to draw check-syntax arrows
[check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))]
;; perform the provide transformation from [Culpepper 07]
[transformed-body (remove-provides #'body2)]
;; add the real definitions of contracts on requires
[transformed-body (change-contract-fixups #'transformed-body)]
;; potentially optimize the code based on the type information
[(optimized-body ...)
;; do we optimize?
(if (optimize?)
(begin0 (map optimize-top (syntax->list #'transformed-body))
(do-time "Optimized"))
#'transformed-body)])
;; reconstruct the module with the extra code
;; use the regular %#module-begin from `racket/base' for top-level printing
#`(#%module-begin optimized-body ... #,after-code check-syntax-help)))))]))
(define (ti-core stx)
(syntax-parse stx
[(_ . ((~datum module) . rest))
#'(module . rest)]
[(_ . form)
(tc-setup
stx #'form 'top-level body2 tc-toplevel-form type
(syntax-parse body2
;; any of these do not produce an expression to be printed
[(head:invis-kw . _) body2]
[_ (let ([ty-str (match type
;; don't print results of type void
[(tc-result1: (== -Void type-equal?)) #f]
[(tc-result1: t f o)
(format "- : ~a\n" t)]
[(tc-results: t)
(format "- : ~a\n" (cons 'Values t))]
[x (int-err "bad type result: ~a" x)])])
(if ty-str
#`(let ([type '#,ty-str])
(begin0 #,body2 (display type)))
body2))]))]))

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

@ -640,6 +640,8 @@
[exit (-> (Un))]
[collect-garbage (-> -Void)]
[current-memory-use (-> -Nat)]
[dump-memory-stats (-> Univ)]
[module->namespace (-> (-mu x (-lst (Un -Symbol -String -Nat x (-val #f)))) -Namespace)]
[current-namespace (-Param -Namespace -Namespace)]

32
collects/typed-scheme/private/prims.rkt
View File

@ -30,31 +30,31 @@ This file defines two sorts of primitives. All of them are provided into any mod
(require "../utils/utils.rkt"
racket/base
mzlib/etc
(for-syntax
"../utils/require-contract.rkt"
"colon.rkt"
"../typecheck/internal-forms.rkt"
(rename-in racket/contract [-> c->])
mzlib/struct
"base-types.rkt"
"base-types-extra.rkt"
(for-syntax
syntax/parse
syntax/private/util
scheme/base
(rep type-rep)
mzlib/match
"parse-type.rkt" "annotate-classes.rkt"
scheme/struct-info
syntax/struct
syntax/stx
scheme/struct-info
(private internal)
(except-in (utils utils tc-utils))
(env type-name-env)
"../rep/type-rep.rkt"
"parse-type.rkt"
"annotate-classes.rkt"
"internal.rkt"
"../utils/utils.rkt"
"../utils/tc-utils.rkt"
"../env/type-name-env.rkt"
"type-contract.rkt"
"for-clauses.rkt"))
(require (utils require-contract)
"colon.rkt"
(typecheck internal-forms)
(except-in mzlib/contract ->)
(only-in mzlib/contract [-> c->])
mzlib/struct
"base-types.rkt"
"base-types-extra.rkt")
(define-for-syntax (ignore stx) (syntax-property stx 'typechecker:ignore #t))

188
collects/typed-scheme/private/with-types.rkt
View File

@ -1,11 +1,14 @@
#lang racket/base
(require racket/require racket/contract/regions racket/contract/base
(require racket/require
(for-template
(except-in racket/base for for*)
"prims.rkt"
(prefix-in c: (combine-in racket/contract/regions racket/contract/base)))
"base-env.rkt" "base-special-env.rkt" "base-env-numeric.rkt"
"base-env-indexing.rkt" "extra-procs.rkt" "prims.rkt"
(for-syntax
scheme/base syntax/parse racket/block racket/match
unstable/sequence unstable/debug "base-types-extra.rkt"
syntax/parse racket/block racket/match
unstable/sequence unstable/debug "base-types-extra.rkt"
(except-in (path-up "env/type-name-env.rkt"
"env/type-alias-env.rkt"
"infer/infer-dummy.rkt"
@ -21,98 +24,97 @@
"types/convenience.rkt"
"types/abbrev.rkt")
->)
(except-in (path-up "utils/utils.rkt") infer)))
(except-in (path-up "utils/utils.rkt") infer))
(provide with-type)
(provide wt-core)
(define-for-syntax (with-type-helper stx body fvids fvtys exids extys resty expr? ctx)
(block
(define old-context (unbox typed-context?))
(define ((no-contract t [stx stx]))
(tc-error/stx stx "Type ~a could not be converted to a contract." t))
(set-box! typed-context? #t)
(define fv-types (for/list ([t (in-list (syntax->list fvtys))])
(parse-type t)))
(define fv-cnts (for/list ([t (in-list fv-types)]
[stx (in-list (syntax->list fvtys))])
(type->contract t #:typed-side #f (no-contract t))))
(define ex-types (for/list ([t (syntax->list extys)])
(parse-type t)))
(define ex-cnts (for/list ([t (in-list ex-types)]
[stx (in-list (syntax->list extys))])
(type->contract t #:typed-side #t (no-contract t))))
(define region-tc-result
(and expr? (parse-tc-results resty)))
(define region-cnts
(if region-tc-result
(match region-tc-result
[(tc-result1: t)
(list (type->contract t #:typed-side #t (no-contract t #'region-ty-stx)))]
[(tc-results: ts)
(for/list ([t (in-list ts)])
(type->contract
t #:typed-side #t
(no-contract t #'region-ty-stx)))])
null))
(for ([i (in-list (syntax->list fvids))]
[ty (in-list fv-types)])
(register-type i ty))
(define expanded-body
(if expr?
(with-syntax ([body body])
(local-expand #'(let () . body) ctx null))
(with-syntax ([(body ...) body]
[(id ...) exids]
[(ty ...) extys])
(local-expand #'(let () (begin (: id ty) ... body ... (values id ...))) ctx null))))
(parameterize (;; disable fancy printing?
[custom-printer #t]
;; a cheat to avoid units
[infer-param infer]
;; do we report multiple errors
[delay-errors? #t]
;; this parameter is just for printing types
;; this is a parameter to avoid dependency issues
[current-type-names
(lambda ()
(append
(type-name-env-map (lambda (id ty)
(cons (syntax-e id) ty)))
(type-alias-env-map (lambda (id ty)
(cons (syntax-e id) ty)))))]
;; reinitialize seen type variables
[type-name-references null]
;; for error reporting
[orig-module-stx stx]
[expanded-module-stx expanded-body])
(tc-expr/check expanded-body (if expr? region-tc-result (ret ex-types))))
(report-all-errors)
(set-box! typed-context? old-context)
;; then clear the new entries from the env ht
(for ([i (in-list (syntax->list fvids))])
(unregister-type i))
(with-syntax ([(fv.id ...) fvids]
[(cnt ...) fv-cnts]
[(ex-id ...) exids]
[(ex-cnt ...) ex-cnts]
[(region-cnt ...) region-cnts]
[body expanded-body]
[check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))])
(if expr?
(quasisyntax/loc stx
(begin check-syntax-help
(with-contract typed-region
#:results (region-cnt ...)
#:freevars ([fv.id cnt] ...)
body)))
(syntax/loc stx
(begin
(define-values () (begin check-syntax-help (values)))
(with-contract typed-region
([ex-id ex-cnt] ...)
(define-values (ex-id ...) body))))))))
(define (with-type-helper stx body fvids fvtys exids extys resty expr? ctx)
(define old-context (unbox typed-context?))
(define ((no-contract t [stx stx]))
(tc-error/stx stx "Type ~a could not be converted to a contract." t))
(set-box! typed-context? #t)
(define fv-types (for/list ([t (in-list (syntax->list fvtys))])
(parse-type t)))
(define fv-cnts (for/list ([t (in-list fv-types)]
[stx (in-list (syntax->list fvtys))])
(type->contract t #:typed-side #f (no-contract t))))
(define ex-types (for/list ([t (syntax->list extys)])
(parse-type t)))
(define ex-cnts (for/list ([t (in-list ex-types)]
[stx (in-list (syntax->list extys))])
(type->contract t #:typed-side #t (no-contract t))))
(define region-tc-result
(and expr? (parse-tc-results resty)))
(define region-cnts
(if region-tc-result
(match region-tc-result
[(tc-result1: t)
(list (type->contract t #:typed-side #t (no-contract t #'region-ty-stx)))]
[(tc-results: ts)
(for/list ([t (in-list ts)])
(type->contract
t #:typed-side #t
(no-contract t #'region-ty-stx)))])
null))
(for ([i (in-list (syntax->list fvids))]
[ty (in-list fv-types)])
(register-type i ty))
(define expanded-body
(if expr?
(with-syntax ([body body])
(local-expand #'(let () . body) ctx null))
(with-syntax ([(body ...) body]
[(id ...) exids]
[(ty ...) extys])
(local-expand #'(let () (begin (: id ty) ... body ... (values id ...))) ctx null))))
(parameterize (;; disable fancy printing?
[custom-printer #t]
;; a cheat to avoid units
[infer-param infer]
;; do we report multiple errors
[delay-errors? #t]
;; this parameter is just for printing types
;; this is a parameter to avoid dependency issues
[current-type-names
(lambda ()
(append
(type-name-env-map (lambda (id ty)
(cons (syntax-e id) ty)))
(type-alias-env-map (lambda (id ty)
(cons (syntax-e id) ty)))))]
;; reinitialize seen type variables
[type-name-references null]
;; for error reporting
[orig-module-stx stx]
[expanded-module-stx expanded-body])
(tc-expr/check expanded-body (if expr? region-tc-result (ret ex-types))))
(report-all-errors)
(set-box! typed-context? old-context)
;; then clear the new entries from the env ht
(for ([i (in-list (syntax->list fvids))])
(unregister-type i))
(with-syntax ([(fv.id ...) fvids]
[(cnt ...) fv-cnts]
[(ex-id ...) exids]
[(ex-cnt ...) ex-cnts]
[(region-cnt ...) region-cnts]
[body expanded-body]
[check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))])
(if expr?
(quasisyntax/loc stx
(begin check-syntax-help
(c:with-contract typed-region
#:results (region-cnt ...)
#:freevars ([fv.id cnt] ...)
body)))
(syntax/loc stx
(begin
(define-values () (begin check-syntax-help (values)))
(c:with-contract typed-region
([ex-id ex-cnt] ...)
(define-values (ex-id ...) body)))))))
(define-syntax (with-type stx)
(define (wt-core stx)
(define-syntax-class typed-id
#:description "[id type]"
[pattern (id ty)])

4
collects/typed-scheme/rep/filter-rep.rkt
View File

@ -46,10 +46,10 @@
(combine-frees (map free-idxs* fs))])
(df FilterSet (thn els)
[#:contract (->d ([t any/c]
[#:contract (->i ([t any/c]
[e any/c])
(#:syntax [stx #f])
#:pre-cond
#:pre-cond (t e)
(and (cond [(Bot? t) #t]
[(Bot? e) (Top? t)]
[else (Filter/c-predicate? t)])

8
collects/typed-scheme/rep/type-rep.rkt
View File

@ -149,8 +149,8 @@
;; n is how many variables are bound here
;; body is a Scope
(dt Poly (n body) #:no-provide
[#:contract (->d ([n natural-number/c]
[body (scope-depth n)])
[#:contract (->i ([n natural-number/c]
[body (n) (scope-depth n)])
(#:syntax [stx (or/c #f syntax?)])
[result Poly?])]
[#:frees (λ (f) (f body))]
@ -162,8 +162,8 @@
;; there are n-1 'normal' vars and 1 ... var
;; body is a Scope
(dt PolyDots (n body) #:no-provide
[#:contract (->d ([n natural-number/c]
[body (scope-depth n)])
[#:contract (->i ([n natural-number/c]
[body (n) (scope-depth n)])
(#:syntax [stx (or/c #f syntax?)])
[result PolyDots?])]
[#:key (Type-key body)]

12
collects/typed-scheme/typecheck/def-export.rkt
View File

@ -1,16 +1,10 @@
#lang racket/base
(require racket/require
(for-syntax syntax/parse racket/base
(path-up "utils/tc-utils.rkt" "private/typed-renaming.rkt" "env/type-name-env.rkt")))
(require racket/require (for-template "renamer.rkt") "renamer.rkt"
(for-syntax syntax/parse racket/base "renamer.rkt"
(path-up "utils/tc-utils.rkt" "env/type-name-env.rkt")))
(provide def-export)
(define-for-syntax (renamer id #:alt [alt #f])
(if alt
(make-typed-renaming (syntax-property id 'not-free-identifier=? #t) alt)
(make-rename-transformer (syntax-property id 'not-free-identifier=? #t))))
(define-syntax (def-export stx)
(syntax-parse stx
[(def-export export-id:identifier id:identifier cnt-id:identifier)

9
collects/typed-scheme/typecheck/renamer.rkt Normal file
View File

@ -0,0 +1,9 @@
#lang racket/base
(require "../private/typed-renaming.rkt")
(provide renamer)
(define (renamer id #:alt [alt #f])
(if alt
(make-typed-renaming (syntax-property id 'not-free-identifier=? #t) alt)
(make-rename-transformer (syntax-property id 'not-free-identifier=? #t))))

71
collects/typed-scheme/typed-scheme.rkt
View File

@ -1,21 +1,6 @@
#lang racket/base
(require (rename-in "utils/utils.rkt" [infer r:infer])
(private with-types)
(for-syntax
(except-in syntax/parse id)
racket/match unstable/syntax racket/base unstable/match
(private type-contract)
(optimizer optimizer)
(types utils convenience)
(typecheck typechecker provide-handling tc-toplevel)
(env type-name-env type-alias-env)
(r:infer infer)
(utils tc-utils)
(rep type-rep)
(except-in (utils utils) infer)
(only-in (r:infer infer-dummy) infer-param)
"tc-setup.rkt"))
(require (for-syntax racket/base "typecheck/renamer.rkt"))
(provide (rename-out [module-begin #%module-begin]
[top-interaction #%top-interaction]
@ -25,54 +10,16 @@
with-type)
(define-syntax (module-begin stx)
(syntax-parse stx
[(mb (~optional (~and #:optimize (~bind [opt? #'#t]))) forms ...)
(let ([pmb-form (syntax/loc stx (#%plain-module-begin forms ...))])
(parameterize ([optimize? (or (optimize?) (attribute opt?))])
(tc-setup
stx pmb-form 'module-begin new-mod tc-module after-code
(with-syntax*
(;; pmb = #%plain-module-begin
[(pmb . body2) new-mod]
;; add in syntax property on useless expression to draw check-syntax arrows
[check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))]
;; perform the provide transformation from [Culpepper 07]
[transformed-body (remove-provides #'body2)]
;; add the real definitions of contracts on requires
[transformed-body (change-contract-fixups #'transformed-body)]
;; potentially optimize the code based on the type information
[(optimized-body ...)
;; do we optimize?
(if (optimize?)
(begin0 (map optimize-top (syntax->list #'transformed-body))
(do-time "Optimized"))
#'transformed-body)])
;; reconstruct the module with the extra code
;; use the regular %#module-begin from `racket/base' for top-level printing
#`(#%module-begin optimized-body ... #,after-code check-syntax-help)))))]))
(dynamic-require 'typed-scheme/private/base-env #f)
(dynamic-require 'typed-scheme/private/base-env-numeric #f)
(dynamic-require 'typed-scheme/private/base-env-indexing #f)
((dynamic-require 'typed-scheme/core 'mb-core) stx))
(define-syntax (top-interaction stx)
(syntax-parse stx
[(_ . ((~datum module) . rest))
#'(module . rest)]
[(_ . form)
(tc-setup
stx #'form 'top-level body2 tc-toplevel-form type
(syntax-parse body2
;; any of these do not produce an expression to be printed
[(head:invis-kw . _) body2]
[_ (let ([ty-str (match type
;; don't print results of type void
[(tc-result1: (== -Void type-equal?)) #f]
[(tc-result1: t f o)
(format "- : ~a\n" t)]
[(tc-results: t)
(format "- : ~a\n" (cons 'Values t))]
[x (int-err "bad type result: ~a" x)])])
(if ty-str
#`(let ([type '#,ty-str])
(begin0 #,body2 (display type)))
body2))]))]))
((dynamic-require 'typed-scheme/core 'ti-core) stx))
(define-syntax (with-type stx)
((dynamic-require 'typed-scheme/core 'wt-core) stx))

16
collects/typed-scheme/types/utils.rkt
View File

@ -137,16 +137,16 @@
(p/c
[ret
(->d ([t (or/c Type/c (listof Type/c))])
([f (if (list? t)
(listof FilterSet/c)
FilterSet/c)]
[o (if (list? t)
(listof Object?)
Object?)]
(->i ([t (or/c Type/c (listof Type/c))])
([f (t) (if (list? t)
(listof FilterSet/c)
FilterSet/c)]
[o (t) (if (list? t)
(listof Object?)
Object?)]
[dty Type/c]
[dbound symbol?])
[_ tc-results?])])
[res tc-results?])])
(define (combine-results tcs)
(match tcs

19
collects/typed-scheme/utils/tc-utils.rkt
View File

@ -6,10 +6,8 @@ don't depend on any other portion of the system
|#
(provide (all-defined-out))
(require "syntax-traversal.rkt"
"utils.rkt" racket/dict
syntax/parse (for-syntax scheme/base syntax/parse) scheme/match unstable/debug
(for-syntax unstable/syntax))
(require "syntax-traversal.rkt" racket/dict
syntax/parse (for-syntax scheme/base syntax/parse) scheme/match)
;; a parameter representing the original location of the syntax being currently checked
(define current-orig-stx (make-parameter #'here))
@ -138,13 +136,12 @@ don't depend on any other portion of the system
;; raise an internal error - typechecker bug!
(define (int-err msg . args)
(parameterize ([custom-printer #t])
(raise (make-exn:fail:tc (string-append "Internal Typechecker Error: "
(apply format msg args)
(format "\nwhile typechecking\n~aoriginally\n~a"
(syntax->datum (current-orig-stx))
(syntax->datum (locate-stx (current-orig-stx)))))
(current-continuation-marks)))))
(raise (make-exn:fail:tc (string-append "Internal Typechecker Error: "
(apply format msg args)
(format "\nwhile typechecking\n~aoriginally\n~a"
(syntax->datum (current-orig-stx))
(syntax->datum (locate-stx (current-orig-stx)))))
(current-continuation-marks))))
(define-syntax (nyi stx)
(syntax-case stx ()