Switch to #lang everywhere.
Fix up requires to use srfi-1 less, and in a uniform way. svn: r9030
This commit is contained in:
Sam Tobin-Hochstadt
parent
afa5e930fe
commit
b0f41af021
|
|
@ -1,14 +1,14 @@
|
|||
(module reader scheme/base
|
||||
(require (prefix-in r: "../typed-reader.ss")
|
||||
(only-in syntax/module-reader wrap-read-all))
|
||||
|
||||
(define (*read in)
|
||||
(wrap-read-all 'typed-scheme in r:read))
|
||||
|
||||
(define (*read-syntax src in)
|
||||
(wrap-read-all 'typed-scheme
|
||||
in
|
||||
(lambda (in)
|
||||
(r:read-syntax src in))))
|
||||
|
||||
(provide (rename-out [*read read] [*read-syntax read-syntax])))
|
||||
#lang scheme/base
|
||||
(require (prefix-in r: "../typed-reader.ss")
|
||||
(only-in syntax/module-reader wrap-read-all))
|
||||
|
||||
(define (*read in)
|
||||
(wrap-read-all 'typed-scheme in r:read))
|
||||
|
||||
(define (*read-syntax src in)
|
||||
(wrap-read-all 'typed-scheme
|
||||
in
|
||||
(lambda (in)
|
||||
(r:read-syntax src in))))
|
||||
|
||||
(provide (rename-out [*read read] [*read-syntax read-syntax]))
|
||||
|
|
|
|||
|
|
@ -1,11 +1,9 @@
|
|||
#lang scheme/unit
|
||||
|
||||
(require (prefix-in 1: srfi/1)
|
||||
syntax/kerncase
|
||||
(require syntax/kerncase
|
||||
syntax/struct
|
||||
syntax/stx
|
||||
mzlib/etc
|
||||
mzlib/plt-match
|
||||
scheme/match
|
||||
"type-contract.ss"
|
||||
"signatures.ss"
|
||||
"tc-structs.ss"
|
||||
|
|
|
|||
|
|
@ -1,22 +1,21 @@
|
|||
(module defstruct-unit mzscheme
|
||||
(require (lib "struct.ss") (lib "unit.ss"))
|
||||
(provide (all-defined))
|
||||
|
||||
(define-syntax defstructs/sig/unit
|
||||
(syntax-rules (define-struct/properties)
|
||||
[(_ signame unitname (imps ...)
|
||||
def
|
||||
(define-struct/properties nm1 (flds1 ...) props #f)
|
||||
(define-struct/properties (nm par) (flds ...) () #f) ...)
|
||||
(begin
|
||||
(define-signature signame
|
||||
((struct nm1 (flds1 ...))
|
||||
(struct nm (flds ...)) ...))
|
||||
(define-unit unitname
|
||||
(import imps ...)
|
||||
(export signame)
|
||||
def
|
||||
(define-struct/properties nm1 (flds1 ...) props #f)
|
||||
(define-struct (nm par) (flds ...) #f) ...))]))
|
||||
|
||||
)
|
||||
#lang scheme/base
|
||||
(require (lib "struct.ss") (lib "unit.ss"))
|
||||
(provide #;(all-defined))
|
||||
|
||||
(define-syntax defstructs/sig/unit
|
||||
(syntax-rules (define-struct/properties)
|
||||
[(_ signame unitname (imps ...)
|
||||
def
|
||||
(define-struct/properties nm1 (flds1 ...) props #f)
|
||||
(define-struct/properties (nm par) (flds ...) () #f) ...)
|
||||
(begin
|
||||
(define-signature signame
|
||||
((struct nm1 (flds1 ...))
|
||||
(struct nm (flds ...)) ...))
|
||||
(define-unit unitname
|
||||
(import imps ...)
|
||||
(export signame)
|
||||
def
|
||||
(define-struct/properties nm1 (flds1 ...) props #f)
|
||||
(define-struct (nm par) (flds ...) #f) ...))]))
|
||||
|
||||
|
|
|
|||
|
|
@ -1,9 +1,7 @@
|
|||
(module extra-procs mzscheme
|
||||
(provide assert)
|
||||
|
||||
(define (assert v)
|
||||
(unless v
|
||||
(error "Assertion failed - value was #f"))
|
||||
v)
|
||||
#lang scheme/base
|
||||
(provide assert)
|
||||
|
||||
)
|
||||
(define (assert v)
|
||||
(unless v
|
||||
(error "Assertion failed - value was #f"))
|
||||
v)
|
||||
|
|
|
|||
|
|
@ -1,76 +1,73 @@
|
|||
(module init-envs mzscheme
|
||||
(provide (all-defined))
|
||||
|
||||
(require "type-env.ss" "type-rep.ss" "type-name-env.ss" "union.ss" "effect-rep.ss" (lib "shared.ss")
|
||||
"type-effect-convenience.ss" "type-alias-env.ss"
|
||||
"type-alias-env.ss")
|
||||
(require (lib "pconvert.ss") (lib "plt-match.ss") (lib "list.ss"))
|
||||
(require-for-template (lib "pconvert.ss"))
|
||||
(require-for-template (lib "shared.ss"))
|
||||
(require-for-template mzscheme "type-rep.ss" "union.ss" "effect-rep.ss" (lib "shared.ss"))
|
||||
|
||||
(define (initialize-type-name-env initial-type-names)
|
||||
(for-each (lambda (nm/ty) (register-resolved-type-alias (car nm/ty) (cadr nm/ty))) initial-type-names))
|
||||
#lang scheme/base
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define (initialize-type-env initial-env)
|
||||
(for-each (lambda (nm/ty) (register-type (car nm/ty) (cadr nm/ty))) initial-env))
|
||||
|
||||
(define (converter v basic sub)
|
||||
(define (gen-constructor sym)
|
||||
(string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
|
||||
(match v
|
||||
[(Union: elems) `(make-Union (list ,@(map sub elems)))]
|
||||
[(Name: stx) `(make-Name (quote-syntax ,stx))]
|
||||
[(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
|
||||
[(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
|
||||
[(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
|
||||
[(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
|
||||
[(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals)))
|
||||
`(,(gen-constructor tag) ,@(map sub vals))]
|
||||
[(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals)))
|
||||
`(,(gen-constructor tag) ,@(map sub vals))]
|
||||
[_ (basic v)]))
|
||||
|
||||
(define (bound-in-this-module id)
|
||||
(let ([binding (identifier-binding id)])
|
||||
(if (and (list? binding) (module-path-index? (car binding)))
|
||||
(let-values ([(mp base) (module-path-index-split (car binding))])
|
||||
(not mp))
|
||||
#f)))
|
||||
|
||||
(define (tname-env-init-code)
|
||||
(define (f id ty)
|
||||
(if (bound-in-this-module id)
|
||||
#`(register-type-name #'#,id #,(datum->syntax-object #'here (print-convert ty)))
|
||||
#f))
|
||||
(parameterize ((current-print-convert-hook converter)
|
||||
(show-sharing #f)
|
||||
(booleans-as-true/false #f))
|
||||
(with-syntax ([registers (filter (lambda (x) x) (type-name-env-map f))])
|
||||
#'(begin (begin-for-syntax . registers)))))
|
||||
|
||||
(define (talias-env-init-code)
|
||||
(define (f id ty)
|
||||
(if (bound-in-this-module id)
|
||||
#`(register-resolved-type-alias #'#,id #,(datum->syntax-object #'here (print-convert ty)))
|
||||
#f))
|
||||
(parameterize ((current-print-convert-hook converter)
|
||||
(show-sharing #f)
|
||||
(booleans-as-true/false #f))
|
||||
(with-syntax ([registers (filter (lambda (x) x) (type-alias-env-map f))])
|
||||
#'(begin (begin-for-syntax . registers)))))
|
||||
|
||||
(define (env-init-code)
|
||||
(define (f id ty)
|
||||
(if (bound-in-this-module id)
|
||||
#`(register-type #'#,id #,(datum->syntax-object #'here (print-convert ty)))
|
||||
#f))
|
||||
(parameterize ((current-print-convert-hook converter)
|
||||
(show-sharing #f)
|
||||
(booleans-as-true/false #f))
|
||||
(with-syntax ([registers (filter (lambda (x) x) (type-env-map f))])
|
||||
#'(begin (begin-for-syntax . registers)))))
|
||||
(require "type-env.ss" "type-rep.ss" "type-name-env.ss" "union.ss" "effect-rep.ss"
|
||||
"type-effect-convenience.ss" "type-alias-env.ss"
|
||||
"type-alias-env.ss")
|
||||
(require mzlib/pconvert scheme/match mzlib/shared
|
||||
(for-template mzlib/pconvert mzlib/shared scheme/base "type-rep.ss" "union.ss" "effect-rep.ss"))
|
||||
|
||||
(define (initialize-type-name-env initial-type-names)
|
||||
(for-each (lambda (nm/ty) (register-resolved-type-alias (car nm/ty) (cadr nm/ty))) initial-type-names))
|
||||
|
||||
(define (initialize-type-env initial-env)
|
||||
(for-each (lambda (nm/ty) (register-type (car nm/ty) (cadr nm/ty))) initial-env))
|
||||
|
||||
(define (converter v basic sub)
|
||||
(define (gen-constructor sym)
|
||||
(string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
|
||||
(match v
|
||||
[(Union: elems) `(make-Union (list ,@(map sub elems)))]
|
||||
[(Name: stx) `(make-Name (quote-syntax ,stx))]
|
||||
[(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
|
||||
[(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
|
||||
[(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
|
||||
[(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
|
||||
[(? Type? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals)))
|
||||
`(,(gen-constructor tag) ,@(map sub vals))]
|
||||
[(? Effect? (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals)))
|
||||
`(,(gen-constructor tag) ,@(map sub vals))]
|
||||
[_ (basic v)]))
|
||||
|
||||
(define (bound-in-this-module id)
|
||||
(let ([binding (identifier-binding id)])
|
||||
(if (and (list? binding) (module-path-index? (car binding)))
|
||||
(let-values ([(mp base) (module-path-index-split (car binding))])
|
||||
(not mp))
|
||||
#f)))
|
||||
|
||||
(define (tname-env-init-code)
|
||||
(define (f id ty)
|
||||
(if (bound-in-this-module id)
|
||||
#`(register-type-name #'#,id #,(datum->syntax #'here (print-convert ty)))
|
||||
#f))
|
||||
(parameterize ((current-print-convert-hook converter)
|
||||
(show-sharing #f)
|
||||
(booleans-as-true/false #f))
|
||||
(with-syntax ([registers (filter (lambda (x) x) (type-name-env-map f))])
|
||||
#'(begin (begin-for-syntax . registers)))))
|
||||
|
||||
(define (talias-env-init-code)
|
||||
(define (f id ty)
|
||||
(if (bound-in-this-module id)
|
||||
#`(register-resolved-type-alias #'#,id #,(datum->syntax #'here (print-convert ty)))
|
||||
#f))
|
||||
(parameterize ((current-print-convert-hook converter)
|
||||
(show-sharing #f)
|
||||
(booleans-as-true/false #f))
|
||||
(with-syntax ([registers (filter (lambda (x) x) (type-alias-env-map f))])
|
||||
#'(begin (begin-for-syntax . registers)))))
|
||||
|
||||
(define (env-init-code)
|
||||
(define (f id ty)
|
||||
(if (bound-in-this-module id)
|
||||
#`(register-type #'#,id #,(datum->syntax #'here (print-convert ty)))
|
||||
#f))
|
||||
(parameterize ((current-print-convert-hook converter)
|
||||
(show-sharing #f)
|
||||
(booleans-as-true/false #f))
|
||||
(with-syntax ([registers (filter (lambda (x) x) (type-env-map f))])
|
||||
#'(begin (begin-for-syntax . registers)))))
|
||||
|
||||
|
||||
|
||||
)
|
||||
|
|
|
|||
|
|
@ -1,15 +1,14 @@
|
|||
(module internal-forms mzscheme
|
||||
|
||||
(define-syntax internal-forms
|
||||
(syntax-rules ()
|
||||
[(_ nms ...)
|
||||
(begin
|
||||
(provide nms ...)
|
||||
(define-syntax (nms stx) (raise-syntax-error 'typecheck "Internal typechecker form used out of context" stx)) ...)]))
|
||||
|
||||
(internal-forms require/typed-internal define-type-alias-internal
|
||||
define-typed-struct-internal
|
||||
define-typed-struct/exec-internal
|
||||
assert-predicate-internal
|
||||
:-internal)
|
||||
)
|
||||
#lang scheme/base
|
||||
|
||||
(require (for-syntax scheme/base))
|
||||
|
||||
(define-syntax-rule (internal-forms nms ...)
|
||||
(begin
|
||||
(provide nms ...)
|
||||
(define-syntax (nms stx) (raise-syntax-error 'typecheck "Internal typechecker form used out of context" stx)) ...))
|
||||
|
||||
(internal-forms require/typed-internal define-type-alias-internal
|
||||
define-typed-struct-internal
|
||||
define-typed-struct/exec-internal
|
||||
assert-predicate-internal
|
||||
:-internal)
|
||||
|
|
|
|||
|
|
@ -1,51 +1,50 @@
|
|||
(module lexical-env mzscheme
|
||||
|
||||
(require "type-environments.ss" "tc-utils.ss" "type-env.ss" "mutated-vars.ss")
|
||||
|
||||
(provide (all-defined))
|
||||
|
||||
;; the current lexical environment
|
||||
(define lexical-env (make-parameter (make-empty-env module-identifier=?)))
|
||||
|
||||
;; run code in a new env
|
||||
(define-syntax with-lexical-env
|
||||
(syntax-rules ()
|
||||
[(_ e . b) (parameterize ([lexical-env e]) . b)]))
|
||||
|
||||
;; run code in an extended env
|
||||
(define-syntax with-lexical-env/extend
|
||||
(syntax-rules ()
|
||||
[(_ is ts . b) (parameterize ([lexical-env (extend/values is ts (lexical-env))]) . b)]))
|
||||
#lang scheme/base
|
||||
|
||||
;; find the type of identifier i, looking first in the lexical env, then in the top-level env
|
||||
;; identifer -> Type
|
||||
(define (lookup-type/lexical i)
|
||||
(lookup (lexical-env) i
|
||||
(lambda (i) (lookup-type i))))
|
||||
|
||||
;; refine the type of i in the lexical env
|
||||
;; (identifier type -> type) identifier -> environment
|
||||
(define (update-type/lexical f i)
|
||||
;; do the updating on the given env
|
||||
;; (identifier type -> type) identifier environment -> environment
|
||||
(define (update f k env)
|
||||
(parameterize
|
||||
([current-orig-stx k])
|
||||
(let* ([v (lookup-type/lexical k)]
|
||||
[new-v (f k v)]
|
||||
[new-env (extend env k new-v)])
|
||||
new-env)))
|
||||
;; check if i is ever the target of a set!
|
||||
(if (is-var-mutated? i)
|
||||
;; if it is, we do nothing
|
||||
(lexical-env)
|
||||
;; otherwise, refine the type
|
||||
(update f i (lexical-env))))
|
||||
|
||||
;; convenience macro for typechecking in the context of an updated env
|
||||
(define-syntax with-update-type/lexical
|
||||
(syntax-rules ()
|
||||
[(_ f i . b)
|
||||
(with-lexical-env (update-type/lexical f i) . b)]))
|
||||
(require "type-environments.ss" "tc-utils.ss" "type-env.ss" "mutated-vars.ss")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
;; the current lexical environment
|
||||
(define lexical-env (make-parameter (make-empty-env free-identifier=?)))
|
||||
|
||||
;; run code in a new env
|
||||
(define-syntax with-lexical-env
|
||||
(syntax-rules ()
|
||||
[(_ e . b) (parameterize ([lexical-env e]) . b)]))
|
||||
|
||||
;; run code in an extended env
|
||||
(define-syntax with-lexical-env/extend
|
||||
(syntax-rules ()
|
||||
[(_ is ts . b) (parameterize ([lexical-env (extend/values is ts (lexical-env))]) . b)]))
|
||||
|
||||
;; find the type of identifier i, looking first in the lexical env, then in the top-level env
|
||||
;; identifer -> Type
|
||||
(define (lookup-type/lexical i)
|
||||
(lookup (lexical-env) i
|
||||
(lambda (i) (lookup-type i))))
|
||||
|
||||
;; refine the type of i in the lexical env
|
||||
;; (identifier type -> type) identifier -> environment
|
||||
(define (update-type/lexical f i)
|
||||
;; do the updating on the given env
|
||||
;; (identifier type -> type) identifier environment -> environment
|
||||
(define (update f k env)
|
||||
(parameterize
|
||||
([current-orig-stx k])
|
||||
(let* ([v (lookup-type/lexical k)]
|
||||
[new-v (f k v)]
|
||||
[new-env (extend env k new-v)])
|
||||
new-env)))
|
||||
;; check if i is ever the target of a set!
|
||||
(if (is-var-mutated? i)
|
||||
;; if it is, we do nothing
|
||||
(lexical-env)
|
||||
;; otherwise, refine the type
|
||||
(update f i (lexical-env))))
|
||||
|
||||
;; convenience macro for typechecking in the context of an updated env
|
||||
(define-syntax with-update-type/lexical
|
||||
(syntax-rules ()
|
||||
[(_ f i . b)
|
||||
(with-lexical-env (update-type/lexical f i) . b)]))
|
||||
|
||||
)
|
||||
|
|
|
|||
|
|
@ -1,52 +1,50 @@
|
|||
(module mutated-vars mzscheme
|
||||
|
||||
(require-for-template mzscheme)
|
||||
(require (lib "boundmap.ss" "syntax")
|
||||
(lib "kerncase.ss" "syntax")
|
||||
(lib "trace.ss"))
|
||||
|
||||
;; mapping telling whether an identifer is mutated
|
||||
;; maps id -> boolean
|
||||
(define table (make-module-identifier-mapping))
|
||||
|
||||
;; find and add to mapping all the set!'ed variables in form
|
||||
#lang scheme/base
|
||||
|
||||
(require (for-template scheme/base)
|
||||
syntax/boundmap syntax/kerncase
|
||||
mzlib/trace)
|
||||
|
||||
;; mapping telling whether an identifer is mutated
|
||||
;; maps id -> boolean
|
||||
(define table (make-module-identifier-mapping))
|
||||
|
||||
;; find and add to mapping all the set!'ed variables in form
|
||||
;; syntax -> void
|
||||
(define (find-mutated-vars form)
|
||||
;; syntax -> void
|
||||
(define (find-mutated-vars form)
|
||||
;; syntax -> void
|
||||
(define (fmv/list lstx)
|
||||
(for-each find-mutated-vars (syntax->list lstx)))
|
||||
;(printf "called with ~a~n" (syntax-object->datum form))
|
||||
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal require/typed-internal #%app lambda)
|
||||
;; what we care about: set!
|
||||
[(set! v e)
|
||||
(begin
|
||||
;(printf "mutated var found: ~a~n" (syntax-e #'v))
|
||||
(module-identifier-mapping-put! table #'v #t))]
|
||||
[(define-values (var ...) expr)
|
||||
(find-mutated-vars #'expr)]
|
||||
[(#%app . rest) (fmv/list #'rest)]
|
||||
[(begin . rest) (fmv/list #'rest)]
|
||||
[(begin0 . rest) (fmv/list #'rest)]
|
||||
[(lambda _ . rest) (fmv/list #'rest)]
|
||||
[(case-lambda (_ . rest) ...) (for-each fmv/list (syntax->list #'(rest ...)))]
|
||||
[(if e1 e2) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e2))]
|
||||
[(if e1 e2 e3) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e1) (find-mutated-vars #'e3))]
|
||||
[(with-continuation-mark e1 e2 e3) (begin (find-mutated-vars #'e1)
|
||||
(find-mutated-vars #'e1)
|
||||
(find-mutated-vars #'e3))]
|
||||
[(let-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
|
||||
(fmv/list #'b))]
|
||||
[(letrec-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
|
||||
(fmv/list #'b))]
|
||||
;; all the other forms don't have any expression subforms (like #%top)
|
||||
[_ (void)]))
|
||||
|
||||
;(trace find-mutated-vars)
|
||||
|
||||
;; checks to see if a particular variable is ever set!'d
|
||||
;; is-var-mutated? : identifier -> boolean
|
||||
(define (is-var-mutated? id) (module-identifier-mapping-get table id (lambda _ #f)))
|
||||
|
||||
(provide find-mutated-vars is-var-mutated?)
|
||||
|
||||
)
|
||||
(define (fmv/list lstx)
|
||||
(for-each find-mutated-vars (syntax->list lstx)))
|
||||
;(printf "called with ~a~n" (syntax-object->datum form))
|
||||
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal require/typed-internal #%app lambda)
|
||||
;; what we care about: set!
|
||||
[(set! v e)
|
||||
(begin
|
||||
;(printf "mutated var found: ~a~n" (syntax-e #'v))
|
||||
(module-identifier-mapping-put! table #'v #t))]
|
||||
[(define-values (var ...) expr)
|
||||
(find-mutated-vars #'expr)]
|
||||
[(#%app . rest) (fmv/list #'rest)]
|
||||
[(begin . rest) (fmv/list #'rest)]
|
||||
[(begin0 . rest) (fmv/list #'rest)]
|
||||
[(lambda _ . rest) (fmv/list #'rest)]
|
||||
[(case-lambda (_ . rest) ...) (for-each fmv/list (syntax->list #'(rest ...)))]
|
||||
[(if e1 e2) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e2))]
|
||||
[(if e1 e2 e3) (begin (find-mutated-vars #'e1) (find-mutated-vars #'e1) (find-mutated-vars #'e3))]
|
||||
[(with-continuation-mark e1 e2 e3) (begin (find-mutated-vars #'e1)
|
||||
(find-mutated-vars #'e1)
|
||||
(find-mutated-vars #'e3))]
|
||||
[(let-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
|
||||
(fmv/list #'b))]
|
||||
[(letrec-values ([_ e] ...) . b) (begin (fmv/list #'(e ...))
|
||||
(fmv/list #'b))]
|
||||
;; all the other forms don't have any expression subforms (like #%top)
|
||||
[_ (void)]))
|
||||
|
||||
;(trace find-mutated-vars)
|
||||
|
||||
;; checks to see if a particular variable is ever set!'d
|
||||
;; is-var-mutated? : identifier -> boolean
|
||||
(define (is-var-mutated? id) (module-identifier-mapping-get table id (lambda _ #f)))
|
||||
|
||||
(provide find-mutated-vars is-var-mutated?)
|
||||
|
||||
|
|
|
|||
|
|
@ -7,14 +7,12 @@
|
|||
(only-in "type-effect-convenience.ss" [make-arr* make-arr])
|
||||
"tc-utils.ss"
|
||||
"union.ss"
|
||||
(lib "stx.ss" "syntax")
|
||||
syntax/stx
|
||||
(except-in "type-environments.ss")
|
||||
"type-name-env.ss"
|
||||
"type-alias-env.ss"
|
||||
"type-utils.ss"
|
||||
(only-in (lib "list.ss") foldl foldr)
|
||||
#;(except-in (lib "list.ss" "srfi" "1") unfold remove)
|
||||
(lib "plt-match.ss"))
|
||||
scheme/match)
|
||||
|
||||
(define enable-mu-parsing (make-parameter #t))
|
||||
|
||||
|
|
|
|||
|
|
@ -1,12 +1,7 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require (only-in (lib "1.ss" "srfi") [assoc assoc*])
|
||||
(prefix-in 1: (lib "1.ss" "srfi"))
|
||||
(lib "kerncase.ss" "syntax")
|
||||
(lib "struct.ss" "syntax")
|
||||
(lib "stx.ss" "syntax")
|
||||
(lib "etc.ss")
|
||||
(except-in (lib "list.ss") remove)
|
||||
(require (only-in srfi/1/list s:member)
|
||||
syntax/kerncase syntax/struct syntax/stx
|
||||
mzlib/trace
|
||||
"type-contract.ss"
|
||||
"signatures.ss"
|
||||
|
|
@ -30,8 +25,7 @@
|
|||
"init-envs.ss"
|
||||
"effect-rep.ss"
|
||||
"mutated-vars.ss"
|
||||
"def-binding.ss"
|
||||
(lib "plt-match.ss"))
|
||||
"def-binding.ss")
|
||||
|
||||
(require (for-template scheme/base
|
||||
scheme/contract))
|
||||
|
|
@ -49,7 +43,7 @@
|
|||
|
||||
(define ((generate-prov stx-defs val-defs) form)
|
||||
(define (mem? i vd)
|
||||
(cond [(1:member i vd (lambda (i j) (free-identifier=? i (binding-name j)))) => car]
|
||||
(cond [(s:member i vd (lambda (i j) (free-identifier=? i (binding-name j)))) => car]
|
||||
[else #f]))
|
||||
(define (lookup-id i vd)
|
||||
(def-binding-ty (mem? i vd)))
|
||||
|
|
|
|||
|
|
@ -19,22 +19,3 @@
|
|||
[(require/contract nm cnt lib)
|
||||
#`(begin (require (only-in lib [nm tmp]))
|
||||
(define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen #'#,stx)))]))
|
||||
#|
|
||||
(module a mzscheme
|
||||
(provide x)
|
||||
(define (x a) 'hi))
|
||||
|
||||
(module z mzscheme
|
||||
(require require-contract)
|
||||
|
||||
(require (lib "contract.ss"))
|
||||
|
||||
(define-struct b (X Y))
|
||||
|
||||
(require/contract x (b? . -> . b?) a )
|
||||
|
||||
(x 'no)
|
||||
)
|
||||
|
||||
(require z)
|
||||
|#
|
||||
|
|
|
|||
|
|
@ -1,42 +1,41 @@
|
|||
(module signatures mzscheme
|
||||
(require (lib "unit.ss"))
|
||||
(provide (all-defined))
|
||||
|
||||
;; cycle 1
|
||||
|
||||
(define-signature type-printer^
|
||||
(print-type has-name print-effect)) ;; done
|
||||
|
||||
(define-signature infer^
|
||||
(unify1 fv fv/list unfold)) ;; done
|
||||
|
||||
(define-signature subst^
|
||||
(subst subst-all)) ;; done
|
||||
|
||||
(define-signature type-equal^
|
||||
(type-equal? type-compare type<? rename tc-result-equal?)) ;; done
|
||||
|
||||
;; cycle 2
|
||||
|
||||
(define-signature typechecker^
|
||||
(type-check tc-toplevel-form))
|
||||
|
||||
(define-signature tc-expr^
|
||||
(tc-expr tc-expr/check check-below tc-literal tc-exprs tc-exprs/check tc-expr/t #;check-expr))
|
||||
|
||||
(define-signature check-subforms^
|
||||
(check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check))
|
||||
|
||||
(define-signature tc-if^
|
||||
(tc/if-onearm tc/if-twoarm tc/if-onearm/check tc/if-twoarm/check))
|
||||
|
||||
(define-signature tc-lambda^
|
||||
(tc/lambda tc/lambda/check tc/rec-lambda/check))
|
||||
|
||||
(define-signature tc-app^
|
||||
(tc/app tc/app/check tc/funapp))
|
||||
|
||||
(define-signature tc-let^
|
||||
(tc/let-values tc/letrec-values tc/let-values/check tc/letrec-values/check))
|
||||
|
||||
)
|
||||
#lang scheme/base
|
||||
(require scheme/unit)
|
||||
(provide (all-defined-out))
|
||||
|
||||
;; cycle 1
|
||||
|
||||
(define-signature type-printer^
|
||||
(print-type has-name print-effect)) ;; done
|
||||
|
||||
(define-signature infer^
|
||||
(unify1 fv fv/list unfold)) ;; done
|
||||
|
||||
(define-signature subst^
|
||||
(subst subst-all)) ;; done
|
||||
|
||||
(define-signature type-equal^
|
||||
(type-equal? type-compare type<? rename tc-result-equal?)) ;; done
|
||||
|
||||
;; cycle 2
|
||||
|
||||
(define-signature typechecker^
|
||||
(type-check tc-toplevel-form))
|
||||
|
||||
(define-signature tc-expr^
|
||||
(tc-expr tc-expr/check check-below tc-literal tc-exprs tc-exprs/check tc-expr/t #;check-expr))
|
||||
|
||||
(define-signature check-subforms^
|
||||
(check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check))
|
||||
|
||||
(define-signature tc-if^
|
||||
(tc/if-onearm tc/if-twoarm tc/if-onearm/check tc/if-twoarm/check))
|
||||
|
||||
(define-signature tc-lambda^
|
||||
(tc/lambda tc/lambda/check tc/rec-lambda/check))
|
||||
|
||||
(define-signature tc-app^
|
||||
(tc/app tc/app/check tc/funapp))
|
||||
|
||||
(define-signature tc-let^
|
||||
(tc/let-values tc/letrec-values tc/let-values/check tc/letrec-values/check))
|
||||
|
||||
|
|
|
|||
|
|
@ -1,9 +1,6 @@
|
|||
#lang scheme/unit
|
||||
|
||||
(require "signatures.ss"
|
||||
(lib "plt-match.ss")
|
||||
(lib "list.ss")
|
||||
(prefix-in 1: srfi/1)
|
||||
"type-rep.ss"
|
||||
"effect-rep.ss"
|
||||
"tc-utils.ss"
|
||||
|
|
@ -17,14 +14,10 @@
|
|||
"type-annotation.ss"
|
||||
"resolve-type.ss"
|
||||
(only-in scheme/private/class-internal make-object do-make-object)
|
||||
(lib "pretty.ss")
|
||||
(lib "trace.ss")
|
||||
(lib "kerncase.ss" "syntax"))
|
||||
|
||||
(require (for-template (lib "plt-match.ss") "internal-forms.ss" scheme/base
|
||||
(only-in scheme/private/class-internal make-object do-make-object)))
|
||||
(require (for-syntax (lib "plt-match.ss") "internal-forms.ss"))
|
||||
|
||||
mzlib/trace mzlib/pretty syntax/kerncase scheme/match
|
||||
(for-template
|
||||
"internal-forms.ss" scheme/base
|
||||
(only-in scheme/private/class-internal make-object do-make-object)))
|
||||
|
||||
(import tc-expr^ tc-lambda^)
|
||||
(export tc-app^)
|
||||
|
|
|
|||
|
|
@ -1,12 +1,10 @@
|
|||
#lang scheme/unit
|
||||
|
||||
|
||||
(require (prefix-in 1: srfi/1)
|
||||
syntax/kerncase
|
||||
(require syntax/kerncase
|
||||
syntax/struct
|
||||
syntax/stx
|
||||
mzlib/etc
|
||||
mzlib/plt-match
|
||||
scheme/match
|
||||
"type-contract.ss"
|
||||
"signatures.ss"
|
||||
"tc-structs.ss"
|
||||
|
|
@ -30,7 +28,6 @@
|
|||
"init-envs.ss"
|
||||
"effect-rep.ss"
|
||||
"mutated-vars.ss"
|
||||
(lib "plt-match.ss")
|
||||
scheme/private/class-internal)
|
||||
|
||||
(require (for-template scheme/base scheme/private/class-internal))
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@
|
|||
"resolve-type.ss"
|
||||
(lib "plt-match.ss")
|
||||
(only-in "type-effect-convenience.ss" [make-arr* make-arr]))
|
||||
(require (for-template mzscheme "internal-forms.ss"))
|
||||
(require (for-template scheme/base "internal-forms.ss"))
|
||||
|
||||
(import tc-expr^)
|
||||
(export tc-lambda^)
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@
|
|||
scheme/base
|
||||
"internal-forms.ss"))
|
||||
|
||||
(require (only-in srfi/1 [member member1]))
|
||||
(require (only-in srfi/1/list s:member))
|
||||
|
||||
|
||||
(import tc-expr^)
|
||||
|
|
@ -86,7 +86,7 @@
|
|||
[(null? names)
|
||||
(if expected (tc-exprs/check (syntax->list body) expected) (tc-exprs (syntax->list body)))]
|
||||
;; if none of the names bound in the letrec are free vars of this rhs
|
||||
[(not (ormap (lambda (n) (member1 n flat-names bound-identifier=?)) (free-vars (car exprs))))
|
||||
[(not (ormap (lambda (n) (s:member n flat-names bound-identifier=?)) (free-vars (car exprs))))
|
||||
;; then check this expression separately
|
||||
(let ([t (tc-expr/t (car exprs))])
|
||||
(with-lexical-env/extend
|
||||
|
|
|
|||
|
|
@ -1,88 +1,86 @@
|
|||
(module tc-utils mzscheme
|
||||
(provide (all-defined))
|
||||
(require (lib "list.ss") (lib "etc.ss")
|
||||
"syntax-traversal.ss")
|
||||
#lang scheme/base
|
||||
(provide (all-defined-out))
|
||||
(require "syntax-traversal.ss" (for-syntax scheme/base))
|
||||
|
||||
;; a parameter representing the original location of the syntax being currently checked
|
||||
(define current-orig-stx (make-parameter #'here))
|
||||
(define orig-module-stx (make-parameter #f))
|
||||
(define expanded-module-stx (make-parameter #f))
|
||||
|
||||
;; helper function, not currently used
|
||||
(define (find-origin stx)
|
||||
(cond [(syntax-property stx 'origin) => (lambda (orig)
|
||||
(let ([r (reverse orig)])
|
||||
(let loop ([r (reverse orig)])
|
||||
(if (null? r) #f
|
||||
(if (syntax-source (car r)) (car r)
|
||||
(loop (cdr r)))))))]
|
||||
[else #f]))
|
||||
|
||||
;; do we print the fully-expanded syntax in error messages?
|
||||
(define print-syntax? (make-parameter #f))
|
||||
|
||||
|
||||
(define check-unreachable-code? (make-parameter #f))
|
||||
|
||||
(define (locate-stx stx)
|
||||
(define omodule (orig-module-stx))
|
||||
(define emodule (expanded-module-stx))
|
||||
;(printf "orig: ~a~n" (syntax-object->datum omodule))
|
||||
;(printf "exp: ~a~n" (syntax-object->datum emodule))
|
||||
;(printf "stx (locate): ~a~n" (syntax-object->datum stx))
|
||||
(look-for-in-orig omodule emodule stx))
|
||||
|
||||
;; produce a type error, using the current syntax
|
||||
(define (tc-error msg . rest)
|
||||
(define cur-stx
|
||||
(begin
|
||||
;(printf "stx : ~a~n" (current-orig-stx))
|
||||
(if (print-syntax?)
|
||||
(current-orig-stx)
|
||||
(locate-stx (current-orig-stx)))))
|
||||
|
||||
;(printf "Aliases: ~a~n" ((current-type-names)))
|
||||
(raise-syntax-error 'typecheck (apply format msg rest) cur-stx cur-stx))
|
||||
|
||||
;; produce a type error, given a particular syntax
|
||||
(define (tc-error/stx stx msg . rest)
|
||||
(parameterize ([current-orig-stx stx])
|
||||
(apply tc-error msg rest)))
|
||||
|
||||
;; check two identifiers to see if they have the same name
|
||||
(define (symbolic-identifier=? a b)
|
||||
(eq? (syntax-e a) (syntax-e b)))
|
||||
|
||||
;; parameter for currently-defined type aliases
|
||||
;; this is used only for printing type names
|
||||
(define current-type-names (make-parameter (lambda () '())))
|
||||
|
||||
;; error for unbound variables
|
||||
(define (lookup-fail e) (tc-error "unbound identifier ~a" e))
|
||||
;; a parameter representing the original location of the syntax being currently checked
|
||||
(define current-orig-stx (make-parameter #'here))
|
||||
(define orig-module-stx (make-parameter #f))
|
||||
(define expanded-module-stx (make-parameter #f))
|
||||
|
||||
;; helper function, not currently used
|
||||
(define (find-origin stx)
|
||||
(cond [(syntax-property stx 'origin) => (lambda (orig)
|
||||
(let ([r (reverse orig)])
|
||||
(let loop ([r (reverse orig)])
|
||||
(if (null? r) #f
|
||||
(if (syntax-source (car r)) (car r)
|
||||
(loop (cdr r)))))))]
|
||||
[else #f]))
|
||||
|
||||
;; do we print the fully-expanded syntax in error messages?
|
||||
(define print-syntax? (make-parameter #f))
|
||||
|
||||
|
||||
;; for reporting internal errors in the type checker
|
||||
(define-struct (exn:fail:tc exn:fail) ())
|
||||
|
||||
;; raise an internal error - typechecker bug!
|
||||
(define (int-err msg . args)
|
||||
(raise (make-exn:fail:tc (string-append "Internal Typechecker Error: " (apply format msg args))
|
||||
(current-continuation-marks))))
|
||||
|
||||
(define-syntax (nyi stx)
|
||||
(syntax-case stx ()
|
||||
[(_ str)
|
||||
(quasisyntax/loc stx (int-err "~a: not yet implemented: ~a" str #,(syntax/loc stx (this-expression-file-name))))]
|
||||
[(_) (syntax/loc stx (nyi ""))]))
|
||||
(define check-unreachable-code? (make-parameter #f))
|
||||
|
||||
(define (locate-stx stx)
|
||||
(define omodule (orig-module-stx))
|
||||
(define emodule (expanded-module-stx))
|
||||
;(printf "orig: ~a~n" (syntax-object->datum omodule))
|
||||
;(printf "exp: ~a~n" (syntax-object->datum emodule))
|
||||
;(printf "stx (locate): ~a~n" (syntax-object->datum stx))
|
||||
(look-for-in-orig omodule emodule stx))
|
||||
|
||||
;; produce a type error, using the current syntax
|
||||
(define (tc-error msg . rest)
|
||||
(define cur-stx
|
||||
(begin
|
||||
;(printf "stx : ~a~n" (current-orig-stx))
|
||||
(if (print-syntax?)
|
||||
(current-orig-stx)
|
||||
(locate-stx (current-orig-stx)))))
|
||||
|
||||
;; are we currently expanding in a typed module (or top-level form)?
|
||||
(define typed-context? (box #f))
|
||||
|
||||
;; what type names have been referred to in this module?
|
||||
(define type-name-references (make-parameter '()))
|
||||
|
||||
(define (add-type-name-reference t)
|
||||
(type-name-references (cons t (type-name-references))))
|
||||
|
||||
)
|
||||
;(printf "Aliases: ~a~n" ((current-type-names)))
|
||||
(raise-syntax-error 'typecheck (apply format msg rest) cur-stx cur-stx))
|
||||
|
||||
;; produce a type error, given a particular syntax
|
||||
(define (tc-error/stx stx msg . rest)
|
||||
(parameterize ([current-orig-stx stx])
|
||||
(apply tc-error msg rest)))
|
||||
|
||||
;; check two identifiers to see if they have the same name
|
||||
(define (symbolic-identifier=? a b)
|
||||
(eq? (syntax-e a) (syntax-e b)))
|
||||
|
||||
;; parameter for currently-defined type aliases
|
||||
;; this is used only for printing type names
|
||||
(define current-type-names (make-parameter (lambda () '())))
|
||||
|
||||
;; error for unbound variables
|
||||
(define (lookup-fail e) (tc-error "unbound identifier ~a" e))
|
||||
|
||||
|
||||
;; for reporting internal errors in the type checker
|
||||
(define-struct (exn:fail:tc exn:fail) ())
|
||||
|
||||
;; raise an internal error - typechecker bug!
|
||||
(define (int-err msg . args)
|
||||
(raise (make-exn:fail:tc (string-append "Internal Typechecker Error: " (apply format msg args))
|
||||
(current-continuation-marks))))
|
||||
|
||||
(define-syntax (nyi stx)
|
||||
(syntax-case stx ()
|
||||
[(_ str)
|
||||
(quasisyntax/loc stx (int-err "~a: not yet implemented: ~a" str #,(syntax/loc stx (this-expression-file-name))))]
|
||||
[(_) (syntax/loc stx (nyi ""))]))
|
||||
|
||||
|
||||
;; are we currently expanding in a typed module (or top-level form)?
|
||||
(define typed-context? (box #f))
|
||||
|
||||
;; what type names have been referred to in this module?
|
||||
(define type-name-references (make-parameter '()))
|
||||
|
||||
(define (add-type-name-reference t)
|
||||
(type-name-references (cons t (type-name-references))))
|
||||
|
||||
|
|
|
|||
|
|
@ -1,8 +1,3 @@
|
|||
(module type-comparison mzscheme
|
||||
(require "type-rep.ss" "type-utils.ss")
|
||||
|
||||
(provide type-equal? tc-result-equal? type<? type-compare effects-equal?)
|
||||
|
||||
|
||||
|
||||
)
|
||||
#lang scheme/base
|
||||
(require "type-rep.ss" "type-utils.ss")
|
||||
(provide type-equal? tc-result-equal? type<? type-compare effects-equal?)
|
||||
|
|
|
|||
|
|
@ -1,132 +1,123 @@
|
|||
(module type-contract mzscheme
|
||||
|
||||
(provide type->contract define/fixup-contract? generate-contract-def change-contract-fixups)
|
||||
|
||||
(require
|
||||
"type-rep.ss"
|
||||
"parse-type.ss"
|
||||
"utils.ss"
|
||||
"type-name-env.ss"
|
||||
"require-contract.ss"
|
||||
"internal-forms.ss"
|
||||
"tc-utils.ss"
|
||||
"resolve-type.ss"
|
||||
"type-utils.ss"
|
||||
mzlib/list
|
||||
(only "type-effect-convenience.ss" Any-Syntax))
|
||||
|
||||
(require
|
||||
(lib "plt-match.ss")
|
||||
(lib "struct.ss" "syntax")
|
||||
(lib "stx.ss" "syntax")
|
||||
(lib "trace.ss")
|
||||
(only (lib "contract.ss") -> ->* case-> cons/c flat-rec-contract)
|
||||
(lib "etc.ss")
|
||||
(lib "struct.ss")
|
||||
#;(lib "syntax-browser.ss" "macro-debugger"))
|
||||
|
||||
(require-for-template mzscheme (lib "contract.ss") (only scheme/class object%))
|
||||
|
||||
(define (define/fixup-contract? stx)
|
||||
(syntax-property stx 'typechecker:contract-def))
|
||||
|
||||
(define (generate-contract-def stx)
|
||||
(define prop (syntax-property stx 'typechecker:contract-def))
|
||||
(define typ (parse-type prop))
|
||||
(syntax-case stx (define-values)
|
||||
[(_ (n) __)
|
||||
(with-syntax ([cnt (type->contract typ (lambda () (tc-error/stx prop "Type ~a could not be converted to a contract." typ)))])
|
||||
(syntax/loc stx (define-values (n) cnt)))]
|
||||
[_ (int-err "should never happen - not a define-values: ~a" (syntax-object->datum stx))]))
|
||||
|
||||
(define (change-contract-fixups forms)
|
||||
(map (lambda (e)
|
||||
(if (not (define/fixup-contract? e))
|
||||
e
|
||||
(generate-contract-def e)))
|
||||
(syntax->list forms)))
|
||||
|
||||
|
||||
(define (type->contract ty fail)
|
||||
(define vars (make-parameter '()))
|
||||
(let/cc exit
|
||||
(let t->c ([ty ty])
|
||||
(match ty
|
||||
[(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
|
||||
[(Univ:) #'any/c]
|
||||
;; we special-case lists:
|
||||
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
|
||||
#`(listof #,(t->c elem-ty))]
|
||||
[(? (lambda (e) (eq? Any-Syntax e))) #'syntax?]
|
||||
[(Base: sym)
|
||||
(case sym
|
||||
[(Number) #'number?]
|
||||
[(Boolean) #'boolean?]
|
||||
[(Keyword) #'keyword?]
|
||||
[(Port) #'port?]
|
||||
[(Path) #'path?]
|
||||
[(String) #'string?]
|
||||
[(Symbol) #'symbol?]
|
||||
[(Bytes) #'bytes?]
|
||||
[(Void) #'void?]
|
||||
[(Syntax) #'syntax?]
|
||||
[(Output-Port) #'output-port?]
|
||||
[(Input-Port) #'input-port?]
|
||||
[(Char) #'char?]
|
||||
[(Namespace) #'namespace?]
|
||||
[(Integer) #'integer?]
|
||||
[else (int-err "Base type ~a cannot be converted to contract" sym)])]
|
||||
[(Union: elems)
|
||||
(with-syntax
|
||||
([cnts (map t->c elems)])
|
||||
#;(printf "~a~n" (syntax-object->datum #'cnts))
|
||||
#'(or/c . cnts))]
|
||||
[(Function: arrs)
|
||||
(let ()
|
||||
(define (f a)
|
||||
(define-values (dom* rngs* rst)
|
||||
(match a
|
||||
[(arr: dom (Values: rngs) #f _ _)
|
||||
(values (map t->c dom) (map t->c rngs) #f)]
|
||||
[(arr: dom rng #f _ _)
|
||||
(values (map t->c dom) (list (t->c rng)) #f)]
|
||||
[(arr: dom (Values: rngs) rst _ _)
|
||||
(values (map t->c dom) (map t->c rngs) (t->c rst))]
|
||||
[(arr: dom rng rst _ _)
|
||||
(values (map t->c dom) (list (t->c rng)) (t->c rst))]))
|
||||
(with-syntax
|
||||
([(dom* ...) dom*]
|
||||
[(rng* ...) rngs*]
|
||||
[rst* rst])
|
||||
(if rst
|
||||
#'((dom* ...) (listof rst*) . ->* . (rng* ...))
|
||||
#'((dom* ...) . ->* . (rng* ...)))))
|
||||
(let ([l (map f arrs)])
|
||||
(if (and (pair? l) (null? (cdr l)))
|
||||
(car l)
|
||||
#`(case-> #,@l))))]
|
||||
[(Vector: t)
|
||||
#`(vectorof #,(t->c t))]
|
||||
[(Pair: t1 t2)
|
||||
#`(cons/c #,(t->c t1) #,(t->c t2))]
|
||||
[(Opaque: p? cert)
|
||||
#`(flat-contract #,(cert p?))]
|
||||
[(F: v) (cond [(assoc v (vars)) => cadr]
|
||||
[else (int-err "unknown var: ~a" v)])]
|
||||
[(Mu: n b)
|
||||
(with-syntax ([(n*) (generate-temporaries (list n))])
|
||||
(parameterize ([vars (cons (list n #'n*) (vars))])
|
||||
#`(flat-rec-contract n* #,(t->c b))))]
|
||||
[(Value: #f) #'false/c]
|
||||
[(Instance: _) #'(is-a?/c object%)]
|
||||
[(Class: _ _ _) #'(subclass?/c object%)]
|
||||
[(Value: '()) #'null?]
|
||||
[(Syntax: (Base: 'Symbol)) #'identifier?]
|
||||
[(Syntax: t)
|
||||
(if (equal? ty Any-Syntax)
|
||||
#`syntax?
|
||||
#`(syntax/c #,(t->c t)))]
|
||||
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x #,v)))]
|
||||
[else (exit (fail))]))))
|
||||
|
||||
)
|
||||
#lang scheme/base
|
||||
|
||||
(provide type->contract define/fixup-contract? generate-contract-def change-contract-fixups)
|
||||
|
||||
(require
|
||||
"type-rep.ss"
|
||||
"parse-type.ss"
|
||||
"utils.ss"
|
||||
"type-name-env.ss"
|
||||
"require-contract.ss"
|
||||
"internal-forms.ss"
|
||||
"tc-utils.ss"
|
||||
"resolve-type.ss"
|
||||
"type-utils.ss"
|
||||
(only-in "type-effect-convenience.ss" Any-Syntax)
|
||||
scheme/match
|
||||
syntax/struct
|
||||
syntax/stx
|
||||
mzlib/trace
|
||||
(only-in scheme/contract -> ->* case-> cons/c flat-rec-contract)
|
||||
(for-template scheme/base scheme/contract (only-in scheme/class object%)))
|
||||
|
||||
(define (define/fixup-contract? stx)
|
||||
(syntax-property stx 'typechecker:contract-def))
|
||||
|
||||
(define (generate-contract-def stx)
|
||||
(define prop (syntax-property stx 'typechecker:contract-def))
|
||||
(define typ (parse-type prop))
|
||||
(syntax-case stx (define-values)
|
||||
[(_ (n) __)
|
||||
(with-syntax ([cnt (type->contract typ (lambda () (tc-error/stx prop "Type ~a could not be converted to a contract." typ)))])
|
||||
(syntax/loc stx (define-values (n) cnt)))]
|
||||
[_ (int-err "should never happen - not a define-values: ~a" (syntax->datum stx))]))
|
||||
|
||||
(define (change-contract-fixups forms)
|
||||
(map (lambda (e)
|
||||
(if (not (define/fixup-contract? e))
|
||||
e
|
||||
(generate-contract-def e)))
|
||||
(syntax->list forms)))
|
||||
|
||||
|
||||
(define (type->contract ty fail)
|
||||
(define vars (make-parameter '()))
|
||||
(let/cc exit
|
||||
(let t->c ([ty ty])
|
||||
(match ty
|
||||
[(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
|
||||
[(Univ:) #'any/c]
|
||||
;; we special-case lists:
|
||||
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
|
||||
#`(listof #,(t->c elem-ty))]
|
||||
[(? (lambda (e) (eq? Any-Syntax e))) #'syntax?]
|
||||
[(Base: sym)
|
||||
(case sym
|
||||
[(Number) #'number?]
|
||||
[(Boolean) #'boolean?]
|
||||
[(Keyword) #'keyword?]
|
||||
[(Port) #'port?]
|
||||
[(Path) #'path?]
|
||||
[(String) #'string?]
|
||||
[(Symbol) #'symbol?]
|
||||
[(Bytes) #'bytes?]
|
||||
[(Void) #'void?]
|
||||
[(Syntax) #'syntax?]
|
||||
[(Output-Port) #'output-port?]
|
||||
[(Input-Port) #'input-port?]
|
||||
[(Char) #'char?]
|
||||
[(Namespace) #'namespace?]
|
||||
[(Integer) #'integer?]
|
||||
[else (int-err "Base type ~a cannot be converted to contract" sym)])]
|
||||
[(Union: elems)
|
||||
(with-syntax
|
||||
([cnts (map t->c elems)])
|
||||
#;(printf "~a~n" (syntax-object->datum #'cnts))
|
||||
#'(or/c . cnts))]
|
||||
[(Function: arrs)
|
||||
(let ()
|
||||
(define (f a)
|
||||
(define-values (dom* rngs* rst)
|
||||
(match a
|
||||
[(arr: dom (Values: rngs) #f _ _)
|
||||
(values (map t->c dom) (map t->c rngs) #f)]
|
||||
[(arr: dom rng #f _ _)
|
||||
(values (map t->c dom) (list (t->c rng)) #f)]
|
||||
[(arr: dom (Values: rngs) rst _ _)
|
||||
(values (map t->c dom) (map t->c rngs) (t->c rst))]
|
||||
[(arr: dom rng rst _ _)
|
||||
(values (map t->c dom) (list (t->c rng)) (t->c rst))]))
|
||||
(with-syntax
|
||||
([(dom* ...) dom*]
|
||||
[(rng* ...) rngs*]
|
||||
[rst* rst])
|
||||
(if rst
|
||||
#'((dom* ...) (listof rst*) . ->* . (rng* ...))
|
||||
#'((dom* ...) . ->* . (rng* ...)))))
|
||||
(let ([l (map f arrs)])
|
||||
(if (and (pair? l) (null? (cdr l)))
|
||||
(car l)
|
||||
#`(case-> #,@l))))]
|
||||
[(Vector: t)
|
||||
#`(vectorof #,(t->c t))]
|
||||
[(Pair: t1 t2)
|
||||
#`(cons/c #,(t->c t1) #,(t->c t2))]
|
||||
[(Opaque: p? cert)
|
||||
#`(flat-contract #,(cert p?))]
|
||||
[(F: v) (cond [(assoc v (vars)) => cadr]
|
||||
[else (int-err "unknown var: ~a" v)])]
|
||||
[(Mu: n b)
|
||||
(with-syntax ([(n*) (generate-temporaries (list n))])
|
||||
(parameterize ([vars (cons (list n #'n*) (vars))])
|
||||
#`(flat-rec-contract n* #,(t->c b))))]
|
||||
[(Value: #f) #'false/c]
|
||||
[(Instance: _) #'(is-a?/c object%)]
|
||||
[(Class: _ _ _) #'(subclass?/c object%)]
|
||||
[(Value: '()) #'null?]
|
||||
[(Syntax: (Base: 'Symbol)) #'identifier?]
|
||||
[(Syntax: t)
|
||||
(if (equal? ty Any-Syntax)
|
||||
#`syntax?
|
||||
#`(syntax/c #,(t->c t)))]
|
||||
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x #,v)))]
|
||||
[else (exit (fail))]))))
|
||||
|
|
|
|||
|
|
@ -1,231 +1,227 @@
|
|||
(module type-effect-convenience scheme/base
|
||||
|
||||
(require "type-rep.ss"
|
||||
"effect-rep.ss"
|
||||
mzlib/plt-match
|
||||
"type-comparison.ss"
|
||||
"type-effect-printer.ss"
|
||||
"union.ss"
|
||||
"subtype.ss"
|
||||
"type-utils.ss"
|
||||
(lib "list.ss")
|
||||
scheme/promise
|
||||
(prefix-in 1: srfi/1)
|
||||
(for-syntax scheme/base))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
||||
(define (-vet id) (make-Var-True-Effect id))
|
||||
(define (-vef id) (make-Var-False-Effect id))
|
||||
|
||||
(define -rem make-Remove-Effect)
|
||||
(define -rest make-Restrict-Effect)
|
||||
|
||||
(define (var->type-eff eff)
|
||||
(match eff
|
||||
[(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
|
||||
[(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
|
||||
[_ eff]))
|
||||
|
||||
(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)]
|
||||
[(True-Effect:) eff]
|
||||
[(False-Effect:) eff]
|
||||
[_ (error 'internal-tc-error "can't add var to effect ~a" eff)]))
|
||||
|
||||
(define-syntax ->
|
||||
(syntax-rules (:)
|
||||
[(_ dom ... rng)
|
||||
(->* (list dom ...) rng)]
|
||||
[(_ dom ... rng : eff1 eff2)
|
||||
(->* (list dom ...) : eff1 eff2)]))
|
||||
(define-syntax ->*
|
||||
(syntax-rules (:)
|
||||
[(_ dom rng)
|
||||
(make-Function (list (make-arr* dom rng)))]
|
||||
[(_ dom rst rng)
|
||||
(make-Function (list (make-arr* dom rng rst)))]
|
||||
[(_ dom rng : eff1 eff2)
|
||||
(make-Function (list (make-arr* dom rng #f eff1 eff2)))]
|
||||
[(_ dom rst rng : eff1 eff2)
|
||||
(make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
|
||||
(define-syntax cl->
|
||||
(syntax-rules (:)
|
||||
[(_ [(dom ...) rng] ...)
|
||||
(make-Function (list (make-arr* (list dom ...) rng) ...))]
|
||||
[(_ [(dom ...) rng : eff1 eff2] ...)
|
||||
(make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
|
||||
[(_ [(dom ...) rng rst : eff1 eff2] ...)
|
||||
(make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
|
||||
(define (cl->* . args)
|
||||
(define (funty-arities f)
|
||||
(match f
|
||||
[(Function: as) as]))
|
||||
(make-Function (map car (map funty-arities args))))
|
||||
|
||||
(define make-arr*
|
||||
(case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
|
||||
[(dom rng rest) (make-arr dom rng rest (list) (list))]
|
||||
[(dom rng rest eff1 eff2) (make-arr dom rng rest eff1 eff2)]))
|
||||
|
||||
(define (make-promise-ty t)
|
||||
(make-Struct (string->uninterned-symbol "Promise") #f (list t) #f))
|
||||
|
||||
(define N (make-Base 'Number))
|
||||
(define -Integer (make-Base 'Integer))
|
||||
(define B (make-Base 'Boolean))
|
||||
(define Sym (make-Base 'Symbol))
|
||||
(define -Void (make-Base 'Void))
|
||||
(define -Bytes (make-Base 'Bytes))
|
||||
(define -Regexp (make-Base 'Regexp))
|
||||
(define -PRegexp (make-Base 'PRegexp))
|
||||
(define -Byte-Regexp (make-Base 'Byte-Regexp))
|
||||
(define -Byte-PRegexp (make-Base 'Byte-PRegexp))
|
||||
(define -String (make-Base 'String))
|
||||
(define -Keyword (make-Base 'Keyword))
|
||||
(define -Char (make-Base 'Char))
|
||||
(define -Syntax make-Syntax)
|
||||
(define -Prompt-Tag (make-Base 'Prompt-Tag))
|
||||
(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set))
|
||||
(define -Path (make-Base 'Path))
|
||||
(define -Namespace (make-Base 'Namespace))
|
||||
(define -Output-Port (make-Base 'Output-Port))
|
||||
(define -Input-Port (make-Base 'Input-Port))
|
||||
|
||||
(define -HT make-Hashtable)
|
||||
(define -Promise make-promise-ty)
|
||||
#lang scheme/base
|
||||
(require "type-rep.ss"
|
||||
"effect-rep.ss"
|
||||
scheme/match
|
||||
"type-comparison.ss"
|
||||
"type-effect-printer.ss"
|
||||
"union.ss"
|
||||
"subtype.ss"
|
||||
"type-utils.ss"
|
||||
scheme/promise
|
||||
(for-syntax scheme/base))
|
||||
|
||||
(define Univ (make-Univ))
|
||||
|
||||
(define-syntax -v
|
||||
(syntax-rules ()
|
||||
[(_ x) (make-F 'x)]))
|
||||
|
||||
(define-syntax -poly
|
||||
(syntax-rules ()
|
||||
[(_ (vars ...) ty)
|
||||
(let ([vars (-v vars)] ...)
|
||||
(make-Poly (list 'vars ...) ty))]))
|
||||
|
||||
(define-syntax -mu
|
||||
(syntax-rules ()
|
||||
[(_ var ty)
|
||||
(let ([var (-v var)])
|
||||
(make-Mu 'var ty))]))
|
||||
|
||||
|
||||
(define -values make-Values)
|
||||
|
||||
;; produce the appropriate type of a list of types
|
||||
;; that is - if there is exactly one type, just produce it, otherwise produce a values-ty
|
||||
;; list[type] -> type
|
||||
(define (list->values-ty l)
|
||||
(if (= 1 (length l)) (car l) (-values l)))
|
||||
|
||||
(define-syntax *Un
|
||||
(syntax-rules ()
|
||||
[(_ . args) (make-Union (list . args))]))
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
||||
(define -pair make-Pair)
|
||||
(define -base make-Base)
|
||||
|
||||
(define -struct make-Struct)
|
||||
(define -val make-Value)
|
||||
|
||||
(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
|
||||
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
|
||||
|
||||
(define -lst make-Listof)
|
||||
(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
|
||||
(define -Port (*Un -Input-Port -Output-Port))
|
||||
|
||||
(define (-lst* . args) (if (null? args)
|
||||
(-val null)
|
||||
(-pair (car args) (apply -lst* (cdr args)))))
|
||||
|
||||
|
||||
#;(define NE (-mu x (Un N (make-Listof x))))
|
||||
(define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
|
||||
|
||||
(define (Un/eff . args)
|
||||
(apply Un (map tc-result-t args)))
|
||||
(define (-vet id) (make-Var-True-Effect id))
|
||||
(define (-vef id) (make-Var-False-Effect id))
|
||||
|
||||
(define -Param make-Param)
|
||||
|
||||
(define make-pred-ty
|
||||
(case-lambda
|
||||
[(in out t)
|
||||
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
|
||||
[(t) (make-pred-ty (list Univ) B t)]))
|
||||
(define -rem make-Remove-Effect)
|
||||
(define -rest make-Restrict-Effect)
|
||||
|
||||
(define (var->type-eff eff)
|
||||
(match eff
|
||||
[(Var-True-Effect: v) (make-Remove-Effect (make-Value #f) v)]
|
||||
[(Var-False-Effect: v) (make-Restrict-Effect (make-Value #f) v)]
|
||||
[_ eff]))
|
||||
|
||||
(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)]
|
||||
[(True-Effect:) eff]
|
||||
[(False-Effect:) eff]
|
||||
[_ (error 'internal-tc-error "can't add var to effect ~a" eff)]))
|
||||
|
||||
(define-syntax ->
|
||||
(syntax-rules (:)
|
||||
[(_ dom ... rng)
|
||||
(->* (list dom ...) rng)]
|
||||
[(_ dom ... rng : eff1 eff2)
|
||||
(->* (list dom ...) : eff1 eff2)]))
|
||||
(define-syntax ->*
|
||||
(syntax-rules (:)
|
||||
[(_ dom rng)
|
||||
(make-Function (list (make-arr* dom rng)))]
|
||||
[(_ dom rst rng)
|
||||
(make-Function (list (make-arr* dom rng rst)))]
|
||||
[(_ dom rng : eff1 eff2)
|
||||
(make-Function (list (make-arr* dom rng #f eff1 eff2)))]
|
||||
[(_ dom rst rng : eff1 eff2)
|
||||
(make-Function (list (make-arr* dom rng rst eff1 eff2)))]))
|
||||
(define-syntax cl->
|
||||
(syntax-rules (:)
|
||||
[(_ [(dom ...) rng] ...)
|
||||
(make-Function (list (make-arr* (list dom ...) rng) ...))]
|
||||
[(_ [(dom ...) rng : eff1 eff2] ...)
|
||||
(make-Function (list (make-arr* (list dom ...) rng #f eff1 eff2) ...))]
|
||||
[(_ [(dom ...) rng rst : eff1 eff2] ...)
|
||||
(make-Function (list (make-arr* (list dom ...) rng rst eff1 eff2) ...))]))
|
||||
(define (cl->* . args)
|
||||
(define (funty-arities f)
|
||||
(match f
|
||||
[(Function: as) as]))
|
||||
(make-Function (map car (map funty-arities args))))
|
||||
|
||||
(define make-arr*
|
||||
(case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
|
||||
[(dom rng rest) (make-arr dom rng rest (list) (list))]
|
||||
[(dom rng rest eff1 eff2) (make-arr dom rng rest eff1 eff2)]))
|
||||
|
||||
(define (make-promise-ty t)
|
||||
(make-Struct (string->uninterned-symbol "Promise") #f (list t) #f))
|
||||
|
||||
(define N (make-Base 'Number))
|
||||
(define -Integer (make-Base 'Integer))
|
||||
(define B (make-Base 'Boolean))
|
||||
(define Sym (make-Base 'Symbol))
|
||||
(define -Void (make-Base 'Void))
|
||||
(define -Bytes (make-Base 'Bytes))
|
||||
(define -Regexp (make-Base 'Regexp))
|
||||
(define -PRegexp (make-Base 'PRegexp))
|
||||
(define -Byte-Regexp (make-Base 'Byte-Regexp))
|
||||
(define -Byte-PRegexp (make-Base 'Byte-PRegexp))
|
||||
(define -String (make-Base 'String))
|
||||
(define -Keyword (make-Base 'Keyword))
|
||||
(define -Char (make-Base 'Char))
|
||||
(define -Syntax make-Syntax)
|
||||
(define -Prompt-Tag (make-Base 'Prompt-Tag))
|
||||
(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set))
|
||||
(define -Path (make-Base 'Path))
|
||||
(define -Namespace (make-Base 'Namespace))
|
||||
(define -Output-Port (make-Base 'Output-Port))
|
||||
(define -Input-Port (make-Base 'Input-Port))
|
||||
|
||||
(define -HT make-Hashtable)
|
||||
(define -Promise make-promise-ty)
|
||||
|
||||
(define Univ (make-Univ))
|
||||
|
||||
(define-syntax -v
|
||||
(syntax-rules ()
|
||||
[(_ x) (make-F 'x)]))
|
||||
|
||||
(define-syntax -poly
|
||||
(syntax-rules ()
|
||||
[(_ (vars ...) ty)
|
||||
(let ([vars (-v vars)] ...)
|
||||
(make-Poly (list 'vars ...) ty))]))
|
||||
|
||||
(define-syntax -mu
|
||||
(syntax-rules ()
|
||||
[(_ var ty)
|
||||
(let ([var (-v var)])
|
||||
(make-Mu 'var ty))]))
|
||||
|
||||
|
||||
(define -values make-Values)
|
||||
|
||||
;; produce the appropriate type of a list of types
|
||||
;; that is - if there is exactly one type, just produce it, otherwise produce a values-ty
|
||||
;; list[type] -> type
|
||||
(define (list->values-ty l)
|
||||
(if (= 1 (length l)) (car l) (-values l)))
|
||||
|
||||
(define-syntax *Un
|
||||
(syntax-rules ()
|
||||
[(_ . args) (make-Union (list . args))]))
|
||||
|
||||
|
||||
(define -pair make-Pair)
|
||||
(define -base make-Base)
|
||||
|
||||
(define -struct make-Struct)
|
||||
(define -val make-Value)
|
||||
|
||||
(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec))))
|
||||
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
|
||||
|
||||
(define -lst make-Listof)
|
||||
(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
|
||||
(define -Port (*Un -Input-Port -Output-Port))
|
||||
|
||||
(define (-lst* . args) (if (null? args)
|
||||
(-val null)
|
||||
(-pair (car args) (apply -lst* (cdr args)))))
|
||||
|
||||
|
||||
#;(define NE (-mu x (Un N (make-Listof x))))
|
||||
(define -NE (-mu x (*Un N (-pair x (-pair Sym (-pair x (-val null)))))))
|
||||
|
||||
(define (Un/eff . args)
|
||||
(apply Un (map tc-result-t args)))
|
||||
|
||||
(define -Param make-Param)
|
||||
|
||||
(define make-pred-ty
|
||||
(case-lambda
|
||||
[(in out t)
|
||||
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
|
||||
[(t) (make-pred-ty (list Univ) B t)]))
|
||||
|
||||
(define -Pathlike (*Un -Path -String))
|
||||
(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
|
||||
(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
|
||||
(define -Byte N)
|
||||
|
||||
(define (-Tuple l)
|
||||
(foldr -pair (-val '()) l))
|
||||
|
||||
(define Any-Syntax
|
||||
(-mu x
|
||||
(-Syntax (*Un
|
||||
(-lst x)
|
||||
(-mu y (*Un x (-pair x y)))
|
||||
(make-Vector x)
|
||||
(make-Box x)
|
||||
N
|
||||
B
|
||||
-String
|
||||
Sym))))
|
||||
|
||||
(define Ident (-Syntax Sym))
|
||||
|
||||
;; DO NOT USE if t contains #f
|
||||
(define (-opt t) (*Un (-val #f) t))
|
||||
|
||||
(define-syntax (make-env stx)
|
||||
(syntax-case stx ()
|
||||
[(_ e ...)
|
||||
#`(list
|
||||
#,@(map (lambda (e)
|
||||
(syntax-case e ()
|
||||
[(nm ty)
|
||||
(identifier? #'nm)
|
||||
#`(list #'nm ty)]
|
||||
[(e ty extra-mods ...)
|
||||
#'(list (let ([new-ns
|
||||
(let* ([ns (make-empty-namespace)])
|
||||
(namespace-attach-module (current-namespace)
|
||||
'scheme/base
|
||||
ns)
|
||||
ns)])
|
||||
(parameterize ([current-namespace new-ns])
|
||||
(namespace-require 'extra-mods) ...
|
||||
e))
|
||||
ty)]))
|
||||
(syntax->list #'(e ...))))]))
|
||||
|
||||
;; if t is of the form (Pair t* (Pair t* ... (Listof t*)))
|
||||
;; return t*
|
||||
;; otherwise, return t
|
||||
;; generalize : Type -> Type
|
||||
(define (generalize t)
|
||||
(let/ec exit
|
||||
(let loop ([t* t])
|
||||
(match t*
|
||||
[(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
|
||||
[(Pair: t1 t2)
|
||||
(let ([t-new (loop t2)])
|
||||
(if (type-equal? (-lst t1) t-new)
|
||||
t-new
|
||||
(exit t)))]
|
||||
[_ (exit t)]))))
|
||||
|
||||
(define -Pathlike (*Un -Path -String))
|
||||
(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
|
||||
(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
|
||||
(define -Byte N)
|
||||
|
||||
(define (-Tuple l)
|
||||
(foldr -pair (-val '()) l))
|
||||
|
||||
(define Any-Syntax
|
||||
(-mu x
|
||||
(-Syntax (*Un
|
||||
(-lst x)
|
||||
(-mu y (*Un x (-pair x y)))
|
||||
(make-Vector x)
|
||||
(make-Box x)
|
||||
N
|
||||
B
|
||||
-String
|
||||
Sym))))
|
||||
|
||||
(define Ident (-Syntax Sym))
|
||||
|
||||
;; DO NOT USE if t contains #f
|
||||
(define (-opt t) (*Un (-val #f) t))
|
||||
|
||||
(define-syntax (make-env stx)
|
||||
(syntax-case stx ()
|
||||
[(_ e ...)
|
||||
#`(list
|
||||
#,@(map (lambda (e)
|
||||
(syntax-case e ()
|
||||
[(nm ty)
|
||||
(identifier? #'nm)
|
||||
#`(list #'nm ty)]
|
||||
[(e ty extra-mods ...)
|
||||
#'(list (let ([new-ns
|
||||
(let* ([ns (make-empty-namespace)])
|
||||
(namespace-attach-module (current-namespace)
|
||||
'scheme/base
|
||||
ns)
|
||||
ns)])
|
||||
(parameterize ([current-namespace new-ns])
|
||||
(namespace-require 'extra-mods) ...
|
||||
e))
|
||||
ty)]))
|
||||
(syntax->list #'(e ...))))]))
|
||||
|
||||
;; if t is of the form (Pair t* (Pair t* ... (Listof t*)))
|
||||
;; return t*
|
||||
;; otherwise, return t
|
||||
;; generalize : Type -> Type
|
||||
(define (generalize t)
|
||||
(let/ec exit
|
||||
(let loop ([t* t])
|
||||
(match t*
|
||||
[(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
|
||||
[(Pair: t1 t2)
|
||||
(let ([t-new (loop t2)])
|
||||
(if (type-equal? (-lst t1) t-new)
|
||||
t-new
|
||||
(exit t)))]
|
||||
[_ (exit t)]))))
|
||||
|
||||
|
||||
)
|
||||
|
|
|
|||
|
|
@ -1,145 +1,141 @@
|
|||
(module type-effect-printer mzscheme
|
||||
(require "type-rep.ss" "effect-rep.ss" "rep-utils.ss" "tc-utils.ss")
|
||||
(require (lib "plt-match.ss"))
|
||||
(require "planet-requires.ss")
|
||||
|
||||
;; do we attempt to find instantiations of polymorphic types to print?
|
||||
;; FIXME - currently broken
|
||||
(define print-poly-types? #f)
|
||||
;; do we use simple type aliases in printing
|
||||
(define print-aliases #t)
|
||||
#lang scheme/base
|
||||
(require "type-rep.ss" "effect-rep.ss" "rep-utils.ss" "tc-utils.ss" "planet-requires.ss" scheme/match)
|
||||
|
||||
;; does t have a type name associated with it currently?
|
||||
;; has-name : Type -> Maybe[Symbol]
|
||||
(define (has-name? t)
|
||||
(define ns ((current-type-names)))
|
||||
(let/cc return
|
||||
(unless print-aliases
|
||||
(return #f))
|
||||
(for-each
|
||||
(lambda (pair)
|
||||
(cond [(eq? t (cdr pair))
|
||||
(return (car pair))]))
|
||||
ns)
|
||||
#f))
|
||||
|
||||
;; print out an effect
|
||||
;; print-effect : Effect Port Boolean -> Void
|
||||
(define (print-effect c port write?)
|
||||
(define (fp . args) (apply fprintf port args))
|
||||
(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)")]
|
||||
[(True-Effect:) (fp "T")]
|
||||
[(False-Effect:) (fp "F")]
|
||||
[(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))]
|
||||
[(Var-False-Effect: v) (fp "(var #f ~a)" (syntax-e v))]))
|
||||
|
||||
|
||||
;; print out a type
|
||||
;; print-type : Type Port Boolean -> Void
|
||||
(define (print-type c port write?)
|
||||
(define (fp . args) (apply fprintf port args))
|
||||
(define (print-arr a)
|
||||
(match a
|
||||
[(top-arr:)
|
||||
(fp "Procedure")]
|
||||
[(arr: dom rng rest thn-eff els-eff)
|
||||
(fp "(")
|
||||
(for-each (lambda (t) (fp "~a " t)) dom)
|
||||
(when rest
|
||||
(fp "~a .. " rest))
|
||||
(fp "-> ~a" rng)
|
||||
(unless (and (null? thn-eff) (null? els-eff))
|
||||
(fp " : ~a ~a" thn-eff els-eff))
|
||||
(fp ")")]))
|
||||
(define (tuple? t)
|
||||
(match t
|
||||
[(Pair: a (? tuple?)) #t]
|
||||
[(Value: '()) #t]
|
||||
[_ #f]))
|
||||
(define (tuple-elems t)
|
||||
(match t
|
||||
[(Pair: a e) (cons a (tuple-elems e))]
|
||||
[(Value: '()) null]))
|
||||
;(fp "~a~n" (Type-seq c))
|
||||
(match c
|
||||
[(Univ:) (fp "Any")]
|
||||
[(? has-name?) (fp "~a" (has-name? c))]
|
||||
;; names are just the printed as the original syntax
|
||||
[(Name: stx) (fp "[~a]" (syntax-e stx))]
|
||||
[(App: rator rands stx)
|
||||
(fp "~a" (cons rator rands))]
|
||||
;; special cases for lists
|
||||
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
|
||||
(fp "(Listof ~a)" elem-ty)]
|
||||
[(Mu: var (Union: (list (Pair: elem-ty (F: var)) (Value: '()))))
|
||||
(fp "(Listof ~a)" elem-ty)]
|
||||
[(Value: v) (cond [(or (symbol? v) (null? v))
|
||||
(fp "'~a" v)]
|
||||
[else (fp "~a" v)])]
|
||||
[(? tuple? t)
|
||||
(fp "~a" (cons 'List (tuple-elems t)))]
|
||||
[(Base: n) (fp "~a" n)]
|
||||
[(Opaque: pred _) (fp "(Opaque ~a)" (syntax-object->datum pred))]
|
||||
[(Struct: 'Promise par (list fld) proc) (fp "(Promise ~a)" fld)]
|
||||
[(Struct: nm par flds proc)
|
||||
(fp "#(struct:~a ~a" nm flds)
|
||||
(when proc
|
||||
(fp " ~a" proc))
|
||||
(fp ")")]
|
||||
[(Function: arities)
|
||||
(let ()
|
||||
(match arities
|
||||
[(list) (fp "(case-lambda)")]
|
||||
[(list a) (print-arr a)]
|
||||
[(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
|
||||
[(arr: _ _ _ _ _) (print-arr c)]
|
||||
[(Vector: e) (fp "(Vectorof ~a)" e)]
|
||||
[(Box: e) (fp "(Box ~a)" e)]
|
||||
[(Union: elems) (fp "~a" (cons 'U elems))]
|
||||
[(Pair: l r) (fp "(Pair ~a ~a)" l r)]
|
||||
[(F: nm) (fp "<~a>" nm)]
|
||||
[(Values: (list v ...)) (fp "~a" (cons 'values v))]
|
||||
[(Param: in out)
|
||||
(if (equal? in out)
|
||||
(fp "(Paramter ~a)" in)
|
||||
(fp "(Parameter ~a ~a)" in out))]
|
||||
[(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
|
||||
#;
|
||||
[(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
|
||||
[(Poly-names: names body)
|
||||
#;(fprintf (current-error-port) "POLY SEQ: ~a~n" (Type-seq body))
|
||||
(fp "(All ~a ~a)" names body)]
|
||||
#;
|
||||
[(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)]
|
||||
[(Mu: x (Syntax: (Union: (list
|
||||
(Base: 'Number)
|
||||
(Base: 'Boolean)
|
||||
(Base: 'Symbol)
|
||||
(Base: 'String)
|
||||
(Mu: var (Union: (list (Value: '()) (Pair: (F: x) (F: var)))))
|
||||
(Mu: y (Union: (list (F: x) (Pair: (F: x) (F: y)))))
|
||||
(Vector: (F: x))
|
||||
(Box: (F: x))))))
|
||||
(fp "SyntaxObject")]
|
||||
[(Mu-name: name body) (fp "(mu ~a ~a ~a)" (Type-seq c) name body)]
|
||||
;; FIXME - this should not be used
|
||||
#;
|
||||
[(Scope: sc) (fp "(Scope ~a)" sc)]
|
||||
#;
|
||||
[(B: idx) (fp "(B ~a)" idx)]
|
||||
[(Syntax: t) (fp "(Syntax ~a)" t)]
|
||||
[(Instance: t) (fp "(Instance ~a)" t)]
|
||||
[(Class: pf nf ms) (fp "(Class)")]
|
||||
[else (fp "Unknown Type: ~a" (struct->vector c))]
|
||||
))
|
||||
|
||||
(set-box! print-type* print-type)
|
||||
(set-box! print-effect* print-effect)
|
||||
|
||||
)
|
||||
;; do we attempt to find instantiations of polymorphic types to print?
|
||||
;; FIXME - currently broken
|
||||
(define print-poly-types? #f)
|
||||
;; do we use simple type aliases in printing
|
||||
(define print-aliases #t)
|
||||
|
||||
;; does t have a type name associated with it currently?
|
||||
;; has-name : Type -> Maybe[Symbol]
|
||||
(define (has-name? t)
|
||||
(define ns ((current-type-names)))
|
||||
(let/cc return
|
||||
(unless print-aliases
|
||||
(return #f))
|
||||
(for-each
|
||||
(lambda (pair)
|
||||
(cond [(eq? t (cdr pair))
|
||||
(return (car pair))]))
|
||||
ns)
|
||||
#f))
|
||||
|
||||
;; print out an effect
|
||||
;; print-effect : Effect Port Boolean -> Void
|
||||
(define (print-effect c port write?)
|
||||
(define (fp . args) (apply fprintf port args))
|
||||
(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)")]
|
||||
[(True-Effect:) (fp "T")]
|
||||
[(False-Effect:) (fp "F")]
|
||||
[(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))]
|
||||
[(Var-False-Effect: v) (fp "(var #f ~a)" (syntax-e v))]))
|
||||
|
||||
|
||||
;; print out a type
|
||||
;; print-type : Type Port Boolean -> Void
|
||||
(define (print-type c port write?)
|
||||
(define (fp . args) (apply fprintf port args))
|
||||
(define (print-arr a)
|
||||
(match a
|
||||
[(top-arr:)
|
||||
(fp "Procedure")]
|
||||
[(arr: dom rng rest thn-eff els-eff)
|
||||
(fp "(")
|
||||
(for-each (lambda (t) (fp "~a " t)) dom)
|
||||
(when rest
|
||||
(fp "~a .. " rest))
|
||||
(fp "-> ~a" rng)
|
||||
(unless (and (null? thn-eff) (null? els-eff))
|
||||
(fp " : ~a ~a" thn-eff els-eff))
|
||||
(fp ")")]))
|
||||
(define (tuple? t)
|
||||
(match t
|
||||
[(Pair: a (? tuple?)) #t]
|
||||
[(Value: '()) #t]
|
||||
[_ #f]))
|
||||
(define (tuple-elems t)
|
||||
(match t
|
||||
[(Pair: a e) (cons a (tuple-elems e))]
|
||||
[(Value: '()) null]))
|
||||
;(fp "~a~n" (Type-seq c))
|
||||
(match c
|
||||
[(Univ:) (fp "Any")]
|
||||
[(? has-name?) (fp "~a" (has-name? c))]
|
||||
;; names are just the printed as the original syntax
|
||||
[(Name: stx) (fp "[~a]" (syntax-e stx))]
|
||||
[(App: rator rands stx)
|
||||
(fp "~a" (cons rator rands))]
|
||||
;; special cases for lists
|
||||
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
|
||||
(fp "(Listof ~a)" elem-ty)]
|
||||
[(Mu: var (Union: (list (Pair: elem-ty (F: var)) (Value: '()))))
|
||||
(fp "(Listof ~a)" elem-ty)]
|
||||
[(Value: v) (cond [(or (symbol? v) (null? v))
|
||||
(fp "'~a" v)]
|
||||
[else (fp "~a" v)])]
|
||||
[(? tuple? t)
|
||||
(fp "~a" (cons 'List (tuple-elems t)))]
|
||||
[(Base: n) (fp "~a" n)]
|
||||
[(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))]
|
||||
[(Struct: 'Promise par (list fld) proc) (fp "(Promise ~a)" fld)]
|
||||
[(Struct: nm par flds proc)
|
||||
(fp "#(struct:~a ~a" nm flds)
|
||||
(when proc
|
||||
(fp " ~a" proc))
|
||||
(fp ")")]
|
||||
[(Function: arities)
|
||||
(let ()
|
||||
(match arities
|
||||
[(list) (fp "(case-lambda)")]
|
||||
[(list a) (print-arr a)]
|
||||
[(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))]
|
||||
[(arr: _ _ _ _ _) (print-arr c)]
|
||||
[(Vector: e) (fp "(Vectorof ~a)" e)]
|
||||
[(Box: e) (fp "(Box ~a)" e)]
|
||||
[(Union: elems) (fp "~a" (cons 'U elems))]
|
||||
[(Pair: l r) (fp "(Pair ~a ~a)" l r)]
|
||||
[(F: nm) (fp "<~a>" nm)]
|
||||
[(Values: (list v ...)) (fp "~a" (cons 'values v))]
|
||||
[(Param: in out)
|
||||
(if (equal? in out)
|
||||
(fp "(Paramter ~a)" in)
|
||||
(fp "(Parameter ~a ~a)" in out))]
|
||||
[(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
|
||||
#;
|
||||
[(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
|
||||
[(Poly-names: names body)
|
||||
#;(fprintf (current-error-port) "POLY SEQ: ~a~n" (Type-seq body))
|
||||
(fp "(All ~a ~a)" names body)]
|
||||
#;
|
||||
[(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)]
|
||||
[(Mu: x (Syntax: (Union: (list
|
||||
(Base: 'Number)
|
||||
(Base: 'Boolean)
|
||||
(Base: 'Symbol)
|
||||
(Base: 'String)
|
||||
(Mu: var (Union: (list (Value: '()) (Pair: (F: x) (F: var)))))
|
||||
(Mu: y (Union: (list (F: x) (Pair: (F: x) (F: y)))))
|
||||
(Vector: (F: x))
|
||||
(Box: (F: x))))))
|
||||
(fp "SyntaxObject")]
|
||||
[(Mu-name: name body) (fp "(mu ~a ~a ~a)" (Type-seq c) name body)]
|
||||
;; FIXME - this should not be used
|
||||
#;
|
||||
[(Scope: sc) (fp "(Scope ~a)" sc)]
|
||||
#;
|
||||
[(B: idx) (fp "(B ~a)" idx)]
|
||||
[(Syntax: t) (fp "(Syntax ~a)" t)]
|
||||
[(Instance: t) (fp "(Instance ~a)" t)]
|
||||
[(Class: pf nf ms) (fp "(Class)")]
|
||||
[else (fp "Unknown Type: ~a" (struct->vector c))]
|
||||
))
|
||||
|
||||
(set-box! print-type* print-type)
|
||||
(set-box! print-effect* print-effect)
|
||||
|
|
|
|||
|
|
@ -1,60 +1,58 @@
|
|||
(module type-environments mzscheme
|
||||
|
||||
(provide current-tvars
|
||||
extend
|
||||
lookup
|
||||
make-empty-env
|
||||
extend-env
|
||||
extend/values
|
||||
initial-tvar-env)
|
||||
|
||||
(require (lib "plt-match.ss")
|
||||
(lib "list.ss")
|
||||
"tc-utils.ss")
|
||||
|
||||
;; eq? has the type of equal?, and l is an alist (with conses!)
|
||||
(define-struct env (eq? l))
|
||||
|
||||
;; the initial type variable environment - empty
|
||||
;; this is used in the parsing of types
|
||||
(define initial-tvar-env (make-env eq? '()))
|
||||
#lang scheme/base
|
||||
|
||||
;; a parameter for the current type variables
|
||||
(define current-tvars (make-parameter initial-tvar-env))
|
||||
|
||||
(define (make-empty-env p?) (make-env p? '()))
|
||||
|
||||
(provide current-tvars
|
||||
extend
|
||||
lookup
|
||||
make-empty-env
|
||||
extend-env
|
||||
extend/values
|
||||
initial-tvar-env)
|
||||
|
||||
;; extend that works on single arguments
|
||||
(define (extend e k v)
|
||||
(match e
|
||||
[(struct env (f l)) (make-env f (cons (cons k v) l))]
|
||||
[_ (int-err "extend: expected environment, got ~a" e)]))
|
||||
|
||||
(define (extend-env ks vs e)
|
||||
(match e
|
||||
[(struct env (f l)) (make-env f (append (map cons ks vs) l))]
|
||||
[_ (int-err "extend-env: expected environment, got ~a" e)]))
|
||||
|
||||
(define (lookup e key fail)
|
||||
(match e
|
||||
[(struct env (f? l))
|
||||
(let loop ([l l])
|
||||
(cond [(null? l) (fail key)]
|
||||
[(f? (caar l) key) (cdar l)]
|
||||
[else (loop (cdr l))]))]
|
||||
[_ (int-err "lookup: expected environment, got ~a" e)]))
|
||||
|
||||
|
||||
;; takes two lists of sets to be added, which are either added one at a time, if the
|
||||
;; elements are not lists, or all at once, if the elements are lists
|
||||
(define (extend/values kss vss env)
|
||||
(foldr (lambda (ks vs env)
|
||||
(cond [(and (list? ks) (list? vs))
|
||||
(extend-env ks vs env)]
|
||||
[(or (list? ks) (list? vs))
|
||||
(int-err "not both lists in extend/values: ~a ~a" ks vs)]
|
||||
[else (extend-env (list ks) (list vs) env)]))
|
||||
env kss vss))
|
||||
(require scheme/match
|
||||
"tc-utils.ss")
|
||||
|
||||
;; eq? has the type of equal?, and l is an alist (with conses!)
|
||||
(define-struct env (eq? l))
|
||||
|
||||
;; the initial type variable environment - empty
|
||||
;; this is used in the parsing of types
|
||||
(define initial-tvar-env (make-env eq? '()))
|
||||
|
||||
;; a parameter for the current type variables
|
||||
(define current-tvars (make-parameter initial-tvar-env))
|
||||
|
||||
(define (make-empty-env p?) (make-env p? '()))
|
||||
|
||||
|
||||
;; extend that works on single arguments
|
||||
(define (extend e k v)
|
||||
(match e
|
||||
[(struct env (f l)) (make-env f (cons (cons k v) l))]
|
||||
[_ (int-err "extend: expected environment, got ~a" e)]))
|
||||
|
||||
(define (extend-env ks vs e)
|
||||
(match e
|
||||
[(struct env (f l)) (make-env f (append (map cons ks vs) l))]
|
||||
[_ (int-err "extend-env: expected environment, got ~a" e)]))
|
||||
|
||||
(define (lookup e key fail)
|
||||
(match e
|
||||
[(struct env (f? l))
|
||||
(let loop ([l l])
|
||||
(cond [(null? l) (fail key)]
|
||||
[(f? (caar l) key) (cdar l)]
|
||||
[else (loop (cdr l))]))]
|
||||
[_ (int-err "lookup: expected environment, got ~a" e)]))
|
||||
|
||||
|
||||
;; takes two lists of sets to be added, which are either added one at a time, if the
|
||||
;; elements are not lists, or all at once, if the elements are lists
|
||||
(define (extend/values kss vss env)
|
||||
(foldr (lambda (ks vs env)
|
||||
(cond [(and (list? ks) (list? vs))
|
||||
(extend-env ks vs env)]
|
||||
[(or (list? ks) (list? vs))
|
||||
(int-err "not both lists in extend/values: ~a ~a" ks vs)]
|
||||
[else (extend-env (list ks) (list vs) env)]))
|
||||
env kss vss))
|
||||
|
||||
)
|
||||
|
|
|
|||
|
|
@ -1,11 +1,8 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require (lib "plt-match.ss"))
|
||||
(require (lib "etc.ss") (lib "list.ss"))
|
||||
(require "planet-requires.ss" "rep-utils.ss" "effect-rep.ss" "tc-utils.ss"
|
||||
"free-variance.ss")
|
||||
(require (prefix-in 1: (lib "list.ss" "srfi" "1"))
|
||||
(lib "trace.ss")
|
||||
"free-variance.ss"
|
||||
mzlib/trace scheme/match
|
||||
(for-syntax scheme/base))
|
||||
|
||||
(define name-table (make-hash-table 'weak))
|
||||
|
|
|
|||
|
|
@ -1,62 +1,61 @@
|
|||
(module union mzscheme
|
||||
|
||||
(require "type-rep.ss" "subtype.ss" "tc-utils.ss"
|
||||
"type-effect-printer.ss" "rep-utils.ss"
|
||||
"type-comparison.ss")
|
||||
(require (lib "plt-match.ss") (lib "list.ss") (lib "trace.ss"))
|
||||
|
||||
(provide Un #;(rename *Un Un))
|
||||
|
||||
(define (make-union* set)
|
||||
(match set
|
||||
[(list t) t]
|
||||
[_ (make-Union set)]))
|
||||
|
||||
(define empty-union (make-Union null))
|
||||
|
||||
(define (flat t)
|
||||
(match t
|
||||
[(Union: es) es]
|
||||
[_ (list t)]))
|
||||
#;(define (Values-types t) (match t [(Values: ts) ts]))
|
||||
(define (remove-subtypes ts)
|
||||
(let loop ([ts* ts] [result '()])
|
||||
(cond [(null? ts*) (reverse result)]
|
||||
[(ormap (lambda (t) (subtype (car ts*) t)) result) (loop (cdr ts*) result)]
|
||||
[else (loop (cdr ts*) (cons (car ts*) result))])))
|
||||
|
||||
(define Un
|
||||
(case-lambda
|
||||
[() empty-union]
|
||||
[args
|
||||
;; a is a Type (not a union type)
|
||||
;; b is a List[Type]
|
||||
(define (union2 a b)
|
||||
(define b* (make-union* b))
|
||||
(cond
|
||||
[(subtype a b*) (list b*)]
|
||||
[(subtype b* a) (list a)]
|
||||
[else (cons a b)]))
|
||||
#;(union-count!)
|
||||
(let ([types (remove-dups (sort (apply append (map flat args)) type<?))])
|
||||
(cond
|
||||
[(null? types) (make-union* null)]
|
||||
[(null? (cdr types)) (car types)]
|
||||
[(ormap Values? types)
|
||||
(if (andmap Values? types)
|
||||
(make-Values (apply map Un (map Values-types types)))
|
||||
(int-err "Un: should not take the union of multiple values with some other type: ~a" types))]
|
||||
[else (make-union* #;(remove-subtypes types) (foldr union2 null types))]))]))
|
||||
|
||||
#;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)
|
||||
|
||||
#;(define (*Un . args) (Un-intern args))
|
||||
|
||||
;(trace Un)
|
||||
|
||||
(define (u-maker args) (apply Un args))
|
||||
|
||||
;(trace u-maker)
|
||||
(set-union-maker! u-maker)
|
||||
|
||||
)
|
||||
#lang scheme/base
|
||||
|
||||
(require "type-rep.ss" "subtype.ss" "tc-utils.ss"
|
||||
"type-effect-printer.ss" "rep-utils.ss"
|
||||
"type-comparison.ss"
|
||||
scheme/match mzlib/trace)
|
||||
|
||||
(provide Un #;(rename *Un Un))
|
||||
|
||||
(define (make-union* set)
|
||||
(match set
|
||||
[(list t) t]
|
||||
[_ (make-Union set)]))
|
||||
|
||||
(define empty-union (make-Union null))
|
||||
|
||||
(define (flat t)
|
||||
(match t
|
||||
[(Union: es) es]
|
||||
[_ (list t)]))
|
||||
#;(define (Values-types t) (match t [(Values: ts) ts]))
|
||||
(define (remove-subtypes ts)
|
||||
(let loop ([ts* ts] [result '()])
|
||||
(cond [(null? ts*) (reverse result)]
|
||||
[(ormap (lambda (t) (subtype (car ts*) t)) result) (loop (cdr ts*) result)]
|
||||
[else (loop (cdr ts*) (cons (car ts*) result))])))
|
||||
|
||||
(define Un
|
||||
(case-lambda
|
||||
[() empty-union]
|
||||
[args
|
||||
;; a is a Type (not a union type)
|
||||
;; b is a List[Type]
|
||||
(define (union2 a b)
|
||||
(define b* (make-union* b))
|
||||
(cond
|
||||
[(subtype a b*) (list b*)]
|
||||
[(subtype b* a) (list a)]
|
||||
[else (cons a b)]))
|
||||
#;(union-count!)
|
||||
(let ([types (remove-dups (sort (apply append (map flat args)) type<?))])
|
||||
(cond
|
||||
[(null? types) (make-union* null)]
|
||||
[(null? (cdr types)) (car types)]
|
||||
[(ormap Values? types)
|
||||
(if (andmap Values? types)
|
||||
(make-Values (apply map Un (map Values-types types)))
|
||||
(int-err "Un: should not take the union of multiple values with some other type: ~a" types))]
|
||||
[else (make-union* #;(remove-subtypes types) (foldr union2 null types))]))]))
|
||||
|
||||
#;(defintern (Un-intern args) (lambda (_ args) (apply Un args)) args)
|
||||
|
||||
#;(define (*Un . args) (Un-intern args))
|
||||
|
||||
;(trace Un)
|
||||
|
||||
(define (u-maker args) (apply Un args))
|
||||
|
||||
;(trace u-maker)
|
||||
(set-union-maker! u-maker)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,93 +1,96 @@
|
|||
(module unit-utils mzscheme
|
||||
(require (lib "unit.ss"))
|
||||
(require-for-syntax (lib "unit-exptime.ss")
|
||||
(lib "list.ss" "srfi" "1")
|
||||
(lib "match.ss"))
|
||||
|
||||
(provide define-values/link-units/infer)
|
||||
#lang scheme/base
|
||||
|
||||
(define-syntax (define-values/link-units/infer stx)
|
||||
;; construct something we can put in the imports/exports clause from the datum
|
||||
(define (datum->sig-elem d)
|
||||
(if (car d)
|
||||
(quasisyntax/loc (cdr d) (tag . #,(cdr d)))
|
||||
(cdr d)))
|
||||
|
||||
;; identifier -> (list (listof imports) (listof exports))
|
||||
(define (get-sigs id)
|
||||
(define-values (imps exps) (unit-static-signatures id id))
|
||||
(list imps exps))
|
||||
|
||||
;; flatten one level of a list
|
||||
;; listof[listof[a]] -> listof[a]
|
||||
(define (flatten l) (apply append l))
|
||||
|
||||
;; returns two lists of sig-elems
|
||||
(define (get-all-sigs ids)
|
||||
(define imps/exps (map get-sigs ids))
|
||||
(define-values (imps exps) (unzip2 imps/exps))
|
||||
(values (flatten imps) (flatten exps)))
|
||||
|
||||
;; construct the runtime code
|
||||
;; takes 3 lists of identifiers and a syntax object for location info
|
||||
(define (mk imports exports units stx)
|
||||
(quasisyntax/loc stx
|
||||
(begin (define-compound-unit/infer new-unit@
|
||||
(import #,@imports)
|
||||
(export #,@exports)
|
||||
(link #,@units))
|
||||
(define-values/invoke-unit/infer new-unit@))))
|
||||
|
||||
;; compares two signature datums for equality
|
||||
(define (sig=? sig1 sig2)
|
||||
(and (eq? (car sig1) (car sig2))
|
||||
(or (symbol? (car sig1)) (not (car sig1)))
|
||||
(bound-identifier=? (cdr sig1) (cdr sig2))))
|
||||
|
||||
;; is imp in the list of exports?
|
||||
(define (imp-in-exps? imp exps)
|
||||
(s:member imp exps sig=?))
|
||||
|
||||
;; produce the imports not satisfied by the exports, and all the exports
|
||||
;; exports should not have duplicates
|
||||
(define (imps/exps-from-units units)
|
||||
(let-values ([(imps exps) (get-all-sigs units)])
|
||||
(let* ([exps* (map datum->sig-elem exps)]
|
||||
[imps* (map datum->sig-elem (filter (lambda (imp) (not (imp-in-exps? imp exps))) imps))])
|
||||
(values imps* exps*))))
|
||||
|
||||
(syntax-case stx (import export)
|
||||
;; here the exports are specified - they ought to be a subset of the allowable exports
|
||||
[(_ (export . sigs) . units)
|
||||
(let*-values ([(units) (syntax->list #'units)]
|
||||
[(imps exps) (imps/exps-from-units units)])
|
||||
(mk imps (syntax->list #'sigs) units stx))]
|
||||
;; here we just export everything that's available
|
||||
[(_ . units)
|
||||
(andmap identifier? (syntax->list #'units))
|
||||
(let*-values ([(units) (syntax->list #'units)]
|
||||
[(imps exps) (imps/exps-from-units units)])
|
||||
(mk imps exps units stx))]))
|
||||
(require scheme/unit
|
||||
(for-syntax
|
||||
scheme/base
|
||||
(only-in srfi/1/list s:member)
|
||||
scheme/unit-exptime
|
||||
scheme/match))
|
||||
|
||||
(provide define-values/link-units/infer)
|
||||
|
||||
(define-syntax (define-values/link-units/infer stx)
|
||||
;; construct something we can put in the imports/exports clause from the datum
|
||||
(define (datum->sig-elem d)
|
||||
(if (car d)
|
||||
(quasisyntax/loc (cdr d) (tag . #,(cdr d)))
|
||||
(cdr d)))
|
||||
|
||||
|
||||
;; Tests
|
||||
;; identifier -> (list (listof imports) (listof exports))
|
||||
(define (get-sigs id)
|
||||
(define-values (imps exps) (unit-static-signatures id id))
|
||||
(list imps exps))
|
||||
|
||||
(define-signature x^ (x))
|
||||
(define-signature y^ (y))
|
||||
(define-signature z^ (z))
|
||||
;; flatten one level of a list
|
||||
;; listof[listof[a]] -> listof[a]
|
||||
(define (flatten l) (apply append l))
|
||||
|
||||
(define-unit y@
|
||||
(import z^)
|
||||
(export y^)
|
||||
(define y (* 2 z)))
|
||||
;; returns two lists of sig-elems
|
||||
(define (get-all-sigs ids)
|
||||
(define imps/exps (map get-sigs ids))
|
||||
(define-values (imps exps) (values (map car imps/exps) (map cadr imps/exps)))
|
||||
(values (flatten imps) (flatten exps)))
|
||||
|
||||
(define-unit x@
|
||||
(import y^)
|
||||
(export x^)
|
||||
(define (x) (+ y 1)))
|
||||
;; construct the runtime code
|
||||
;; takes 3 lists of identifiers and a syntax object for location info
|
||||
(define (mk imports exports units stx)
|
||||
(quasisyntax/loc stx
|
||||
(begin (define-compound-unit/infer new-unit@
|
||||
(import #,@imports)
|
||||
(export #,@exports)
|
||||
(link #,@units))
|
||||
(define-values/invoke-unit/infer new-unit@))))
|
||||
|
||||
(define z 45)
|
||||
|
||||
(define-values/link-units/infer (export x^) x@ y@)
|
||||
;; compares two signature datums for equality
|
||||
(define (sig=? sig1 sig2)
|
||||
(and (eq? (car sig1) (car sig2))
|
||||
(or (symbol? (car sig1)) (not (car sig1)))
|
||||
(bound-identifier=? (cdr sig1) (cdr sig2))))
|
||||
|
||||
)
|
||||
;; is imp in the list of exports?
|
||||
(define (imp-in-exps? imp exps)
|
||||
(s:member imp exps sig=?))
|
||||
|
||||
;; produce the imports not satisfied by the exports, and all the exports
|
||||
;; exports should not have duplicates
|
||||
(define (imps/exps-from-units units)
|
||||
(let-values ([(imps exps) (get-all-sigs units)])
|
||||
(let* ([exps* (map datum->sig-elem exps)]
|
||||
[imps* (map datum->sig-elem (filter (lambda (imp) (not (imp-in-exps? imp exps))) imps))])
|
||||
(values imps* exps*))))
|
||||
|
||||
(syntax-case stx (import export)
|
||||
;; here the exports are specified - they ought to be a subset of the allowable exports
|
||||
[(_ (export . sigs) . units)
|
||||
(let*-values ([(units) (syntax->list #'units)]
|
||||
[(imps exps) (imps/exps-from-units units)])
|
||||
(mk imps (syntax->list #'sigs) units stx))]
|
||||
;; here we just export everything that's available
|
||||
[(_ . units)
|
||||
(andmap identifier? (syntax->list #'units))
|
||||
(let*-values ([(units) (syntax->list #'units)]
|
||||
[(imps exps) (imps/exps-from-units units)])
|
||||
(mk imps exps units stx))]))
|
||||
|
||||
|
||||
;; Tests
|
||||
|
||||
(define-signature x^ (x))
|
||||
(define-signature y^ (y))
|
||||
(define-signature z^ (z))
|
||||
|
||||
(define-unit y@
|
||||
(import z^)
|
||||
(export y^)
|
||||
(define y (* 2 z)))
|
||||
|
||||
(define-unit x@
|
||||
(import y^)
|
||||
(export x^)
|
||||
(define (x) (+ y 1)))
|
||||
|
||||
(define z 45)
|
||||
|
||||
(define-values/link-units/infer (export x^) x@ y@)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1,90 +1,88 @@
|
|||
(module typed-reader mzscheme
|
||||
(require (lib "etc.ss"))
|
||||
|
||||
(require-for-template "private/prims.ss")
|
||||
|
||||
;; Provides raise-read-error and raise-read-eof-error
|
||||
(require (lib "readerr.ss" "syntax"))
|
||||
|
||||
(define (skip-whitespace port)
|
||||
;; Skips whitespace characters, sensitive to the current
|
||||
;; readtable's definition of whitespace
|
||||
(let ([ch (peek-char port)])
|
||||
(unless (eof-object? ch)
|
||||
;; Consult current readtable:
|
||||
(let-values ([(like-ch/sym proc dispatch-proc)
|
||||
(readtable-mapping (current-readtable) ch)])
|
||||
;; If like-ch/sym is whitespace, then ch is whitespace
|
||||
(when (and (char? like-ch/sym)
|
||||
(char-whitespace? like-ch/sym))
|
||||
(read-char port)
|
||||
(skip-whitespace port))))))
|
||||
|
||||
(define (skip-comments read-one port src)
|
||||
;; Recursive read, but skip comments and detect EOF
|
||||
(let loop ()
|
||||
(let ([v (read-one)])
|
||||
(cond
|
||||
[(special-comment? v) (loop)]
|
||||
[(eof-object? v)
|
||||
(let-values ([(l c p) (port-next-location port)])
|
||||
(raise-read-eof-error "unexpected EOF in type annotation" src l c p 1))]
|
||||
[else v]))))
|
||||
#lang scheme/base
|
||||
|
||||
(define (parse port read-one src)
|
||||
(skip-whitespace port)
|
||||
(let ([name (read-one)])
|
||||
(begin0
|
||||
(begin (skip-whitespace port)
|
||||
(let ([next (read-one)])
|
||||
(case (syntax-e next)
|
||||
;; type annotation
|
||||
[(:) (skip-whitespace port)
|
||||
(syntax-property name 'type-label (syntax-object->datum (read-one)))]
|
||||
[(::) (skip-whitespace port)
|
||||
(datum->syntax-object name `(ann ,name : ,(read-one)))]
|
||||
[(@) (let ([elems (let loop ([es '()])
|
||||
(skip-whitespace port)
|
||||
(if (equal? #\} (peek-char port))
|
||||
(reverse es)
|
||||
(loop (cons (read-one) es))))])
|
||||
(datum->syntax-object name `(inst ,name : ,@elems)))]
|
||||
;; arbitrary property annotation
|
||||
[(PROP) (skip-whitespace port)
|
||||
(let* ([prop-name (syntax-e (read-one))])
|
||||
(skip-whitespace port)
|
||||
(syntax-property name prop-name (read-one)))]
|
||||
;; type annotation
|
||||
[else (syntax-property name 'type-label (syntax-object->datum next))])))
|
||||
(skip-whitespace port)
|
||||
(let ([c (read-char port)])
|
||||
#;(printf "char: ~a" c)
|
||||
(unless (equal? #\} c)
|
||||
(let-values ([(l c p) (port-next-location port)])
|
||||
(raise-read-error (format "typed expression ~a not properly terminated" (syntax-object->datum name)) src l c p 1)))))))
|
||||
|
||||
(define parse-id-type
|
||||
(case-lambda
|
||||
[(ch port src line col pos)
|
||||
;; `read-syntax' mode
|
||||
(datum->syntax-object
|
||||
#f
|
||||
(parse port
|
||||
(lambda () (read-syntax src port ))
|
||||
src)
|
||||
(let-values ([(l c p) (port-next-location port)])
|
||||
(list src line col pos (and pos (- p pos)))))]))
|
||||
(require (for-template "private/prims.ss"))
|
||||
|
||||
(define readtable
|
||||
(make-readtable #f #\{ 'dispatch-macro parse-id-type))
|
||||
|
||||
(define (*read inp)
|
||||
(parameterize ([current-readtable readtable])
|
||||
(read inp)))
|
||||
|
||||
(define (*read-syntax src port)
|
||||
(parameterize ([current-readtable readtable])
|
||||
(read-syntax src port)))
|
||||
|
||||
(provide (rename *read read) (rename *read-syntax read-syntax))
|
||||
)
|
||||
;; Provides raise-read-error and raise-read-eof-error
|
||||
(require syntax/readerr)
|
||||
|
||||
(define (skip-whitespace port)
|
||||
;; Skips whitespace characters, sensitive to the current
|
||||
;; readtable's definition of whitespace
|
||||
(let ([ch (peek-char port)])
|
||||
(unless (eof-object? ch)
|
||||
;; Consult current readtable:
|
||||
(let-values ([(like-ch/sym proc dispatch-proc)
|
||||
(readtable-mapping (current-readtable) ch)])
|
||||
;; If like-ch/sym is whitespace, then ch is whitespace
|
||||
(when (and (char? like-ch/sym)
|
||||
(char-whitespace? like-ch/sym))
|
||||
(read-char port)
|
||||
(skip-whitespace port))))))
|
||||
|
||||
(define (skip-comments read-one port src)
|
||||
;; Recursive read, but skip comments and detect EOF
|
||||
(let loop ()
|
||||
(let ([v (read-one)])
|
||||
(cond
|
||||
[(special-comment? v) (loop)]
|
||||
[(eof-object? v)
|
||||
(let-values ([(l c p) (port-next-location port)])
|
||||
(raise-read-eof-error "unexpected EOF in type annotation" src l c p 1))]
|
||||
[else v]))))
|
||||
|
||||
(define (parse port read-one src)
|
||||
(skip-whitespace port)
|
||||
(let ([name (read-one)])
|
||||
(begin0
|
||||
(begin (skip-whitespace port)
|
||||
(let ([next (read-one)])
|
||||
(case (syntax-e next)
|
||||
;; type annotation
|
||||
[(:) (skip-whitespace port)
|
||||
(syntax-property name 'type-label (syntax->datum (read-one)))]
|
||||
[(::) (skip-whitespace port)
|
||||
(datum->syntax name `(ann ,name : ,(read-one)))]
|
||||
[(@) (let ([elems (let loop ([es '()])
|
||||
(skip-whitespace port)
|
||||
(if (equal? #\} (peek-char port))
|
||||
(reverse es)
|
||||
(loop (cons (read-one) es))))])
|
||||
(datum->syntax name `(inst ,name : ,@elems)))]
|
||||
;; arbitrary property annotation
|
||||
[(PROP) (skip-whitespace port)
|
||||
(let* ([prop-name (syntax-e (read-one))])
|
||||
(skip-whitespace port)
|
||||
(syntax-property name prop-name (read-one)))]
|
||||
;; type annotation
|
||||
[else (syntax-property name 'type-label (syntax->datum next))])))
|
||||
(skip-whitespace port)
|
||||
(let ([c (read-char port)])
|
||||
#;(printf "char: ~a" c)
|
||||
(unless (equal? #\} c)
|
||||
(let-values ([(l c p) (port-next-location port)])
|
||||
(raise-read-error (format "typed expression ~a not properly terminated" (syntax->datum name)) src l c p 1)))))))
|
||||
|
||||
(define parse-id-type
|
||||
(case-lambda
|
||||
[(ch port src line col pos)
|
||||
;; `read-syntax' mode
|
||||
(datum->syntax
|
||||
#f
|
||||
(parse port
|
||||
(lambda () (read-syntax src port ))
|
||||
src)
|
||||
(let-values ([(l c p) (port-next-location port)])
|
||||
(list src line col pos (and pos (- p pos)))))]))
|
||||
|
||||
(define readtable
|
||||
(make-readtable #f #\{ 'dispatch-macro parse-id-type))
|
||||
|
||||
(define (*read inp)
|
||||
(parameterize ([current-readtable readtable])
|
||||
(read inp)))
|
||||
|
||||
(define (*read-syntax src port)
|
||||
(parameterize ([current-readtable readtable])
|
||||
(read-syntax src port)))
|
||||
|
||||
(provide (rename-out [*read read] [*read-syntax read-syntax]))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user