resolve conflicts

svn: r14598
This commit is contained in:
Sam Tobin-Hochstadt 2009-04-24 21:21:06 +00:00
parent b53fda9000
commit 1edf62a912
22 changed files with 160 additions and 154 deletions

View File

@ -29,6 +29,9 @@
`(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))]
[(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
[(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
[(Refinement: parent pred cert) `(make-Refinement ,(sub parent)
(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))]
[(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]

View File

@ -31,7 +31,7 @@
=>
(lambda (a)
(-lst (substitute Univ (cdr a) (car a))))]
[else (lookup-fail (syntax-e i))]))))))
[else (lookup-fail i)]))))))
;; refine the type of i in the lexical env
;; (identifier type -> type) identifier -> environment

View File

@ -39,7 +39,7 @@
;; given an identifier, return the type associated with it
;; if none found, calls lookup-fail
;; identifier -> type
(define (lookup-type id [fail-handler (lambda () (lookup-fail (syntax-e id)))])
(define (lookup-type id [fail-handler (lambda () (lookup-type-fail id))])
(let ([v (module-identifier-mapping-get the-mapping id fail-handler)])
(if (box? v) (unbox v) v)))

View File

@ -35,7 +35,7 @@
;; given an identifier, return the type associated with it
;; optional argument is failure continuation - default calls lookup-fail
;; identifier (-> error) -> type
(define (lookup-type-name id [k (lambda () (lookup-fail (syntax-e id)))])
(define (lookup-type-name id [k (lambda () (lookup-type-fail id))])
(begin0
(module-identifier-mapping-get the-mapping id k)
(add-type-name-reference id)))

View File

@ -243,6 +243,9 @@
[(a a) empty]
[(_ (Univ:)) empty]
[((Refinement: S _ _) T)
(cg S T)]
[((F: (? (lambda (e) (memq e X)) v)) S)
(when (match S
[(F: v*)

View File

@ -3,10 +3,11 @@
(require (except-in "../utils/utils.ss" infer))
(require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss"
"restrict.ss" "promote-demote.ss"
(only-in scheme/unit provide-signature-elements)
(only-in scheme/unit provide-signature-elements
define-values/invoke-unit/infer link)
(utils unit-utils))
(provide-signature-elements restrict^ infer^)
(define-values/link-units/infer
infer@ constraints@ dmap@ restrict@ promote-demote@)
(define-values/invoke-unit/infer
(link infer@ constraints@ dmap@ restrict@ promote-demote@))

View File

@ -418,11 +418,12 @@
[symbol->string (Sym . -> . -String)]
[vector-length (-poly (a) ((-vec a) . -> . -Integer))]
[call-with-input-file (-poly (a) (cl-> [(-String (-Port . -> . a)) a]
[(-String (-Port . -> . a) Sym) a]))]
[call-with-input-file (-poly (a) (-String (-Input-Port . -> . a) #:mode (Un (-val 'binary) (-val 'text)) #f . ->key . a))]
[call-with-output-file (-poly (a) (-String (-Output-Port . -> . a)
#:exists (one-of/c error 'append 'update 'replace 'truncate 'truncate/replace) #f
#:mode (Un (-val 'binary) (-val 'text)) #f
. ->key . a))]
[call-with-output-file (-poly (a) (cl-> [(-String (-Port . -> . a)) a]
[(-String (-Port . -> . a) Sym) a]))]
[current-output-port (-Param -Output-Port -Output-Port)]
[current-error-port (-Param -Output-Port -Output-Port)]
[current-input-port (-Param -Input-Port -Input-Port)]
@ -544,11 +545,29 @@
[list->string ((-lst -Char) . -> . -String)]
[string->list (-String . -> . (-lst -Char))]
[sort (-poly (a) ((-lst a) (a a . -> . B) . -> . (-lst a)))]
[find-system-path (Sym . -> . -Path)]
;; scheme/cmdline
[parse-command-line
(let ([mode-sym (one-of/c 'once-each 'once-any 'multi 'final 'help-labels)])
(-polydots (b a)
(cl->* (-Pathlike
(Un (-lst -String) (-vec -String))
(-lst (-pair mode-sym (-lst (-lst Univ))))
((list Univ) [a a] . ->... . b)
(-lst -String)
. -> . b))))]
;; scheme/list
[last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
. -> .
(Un (-pair a a) (-pair a (-val '())))))]
[remove-duplicates
(-poly (a)
(cl->*
((-lst a) . -> . (-lst a))
((-lst a) (a a . -> . Univ) . -> . (-lst a))))]
;; scheme/tcp
[tcp-listener? (make-pred-ty -TCP-Listener)]

View File

@ -8,7 +8,7 @@
(utils tc-utils stxclass-util)
syntax/stx
stxclass stxclass/util
(env type-environments type-name-env type-alias-env)
(env type-environments type-name-env type-alias-env lexical-env)
(prefix-in t: "base-types-extra.ss")
scheme/match
(for-template scheme/base "base-types-extra.ss"))
@ -296,6 +296,13 @@
(map list
(map syntax-e (syntax->list #'(mname ...)))
(map parse-type (syntax->list #'(mty ...)))))]
[(Refinement p?)
(and (eq? (syntax-e #'Refinement) 'Refinement)
(identifier? #'p?))
(match (lookup-type/lexical #'p?)
[(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
(make-Refinement dom #'p? (syntax-local-certifier))]
[t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
[(Instance t)
(eq? (syntax-e #'Instance) 'Instance)
(let ([v (parse-type #'t)])

View File

@ -343,7 +343,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(list #'struct-info
#'maker
#'pred
(list #'sel ...)
(reverse (list #'sel ...))
(list mut ...)
#f))))
#,(internal #'(define-typed-struct-internal nm ([fld : ty] ...) #:type-only))
@ -407,4 +407,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
[(_ [i:id t] ...)
(syntax/loc stx
(begin (: i t) ...
(provide i ...)))]))
(provide i ...)))]))
(define-syntax (declare-refinement stx)
(syntax-parse stx
[(_ p:id)
(quasisyntax/loc stx #,(internal #'(declare-refinement-internal p)))]))

View File

@ -62,6 +62,8 @@
#`(listof #,(t->c elem-ty))]
[(? (lambda (e) (eq? t:Any-Syntax e))) #'syntax?]
[(Base: sym cnt) cnt]
[(Refinement: par p? cert)
#`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
[(Union: elems)
(with-syntax
([cnts (map t->c elems)])
@ -100,7 +102,7 @@
[(Pair: t1 t2)
#`(cons/c #,(t->c t1) #,(t->c t2))]
[(Opaque: p? cert)
#`(flat-contract #,(cert p?))]
#`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
[(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
[else (int-err "unknown var: ~a" v)])]
[(Poly: vs (and b (Function: _)))
@ -122,7 +124,8 @@
[(Instance: _) #'(is-a?/c object%)]
[(Class: _ _ _) #'(subclass?/c object%)]
[(Value: '()) #'null?]
[(Struct: _ _ _ _ #f pred? cert) (cert pred?)]
[(Struct: _ _ _ _ #f pred? cert)
#`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))]
[(Syntax: (Base: 'Symbol _)) #'identifier?]
[(Syntax: t) #`(syntax/c #,(t->c t))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]

View File

@ -0,0 +1,20 @@
#lang scheme/base
(require (for-syntax scheme/base))
(provide make-typed-renaming get-alternate)
;; target : identifier
;; alternate : identifier
(define-struct typed-renaming (target alternate)
#:property prop:rename-transformer 0)
;; identifier -> identifier
;; get the alternate field of the renaming, if it exists
(define (get-alternate id)
(define-values (v new-id) (syntax-local-value/immediate id (lambda _ (values #f #f))))
(cond [(typed-renaming? v)
(typed-renaming-alternate v)]
[(rename-transformer? v)
(get-alternate (rename-transformer-target v))]
[else id]))

View File

@ -201,7 +201,7 @@
poly?
pred-id
cert)]
[#:key (gensym)])
[#:key #f #;(gensym)])
;; v : Scheme Value
@ -243,6 +243,17 @@
;; value : Type
(dt Hashtable ([key Type/c] [value Type/c]) [#:key 'hash])
;; parent : Type
;; pred : Identifier
;; cert : Certifier
(dt Refinement (parent pred cert)
[#:key (Type-key parent)]
[#:intern (list parent (hash-id pred))]
[#:fold-rhs (*Refinement (type-rec-id parent) pred cert)]
[#:frees (free-vars* parent)
(free-idxs* parent)])
;; t : Type
(dt Syntax ([t Type/c]) [#:key 'syntax])
@ -400,7 +411,7 @@
(map sb kws))]
[#:ValuesDots rs dty dbound
(*ValuesDots (map sb rs)
(sb dty)
(sb dty)
(if (eqv? dbound (+ count outer)) (F-n image) dbound))]
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
[#:PolyDots n body*

View File

@ -62,11 +62,11 @@ typed-scheme
There are two differences between these programs:
@itemize{
@itemize[
@item*[@elem{The Language}]{@schememodname[scheme] has been replaced by @schememodname[typed-scheme].}
@item*[@elem{The Type Annotation}]{We have added a type annotation
for the @scheme[fib] function, using the @scheme[:] form.} }
for the @scheme[fib] function, using the @scheme[:] form.} ]
In general, these are most of the changes that have to be made to a
PLT Scheme program to transform it into a Typed Scheme program.

View File

@ -87,7 +87,7 @@ The following base types are parameteric in their type arguments.
types @scheme[t ...]. This can only appear as the return type of a
function.}
@defform/none[v]{where @scheme[v] is a number, boolean or string, is the singleton type containing only that value}
@defform/none['sym]{where @scheme[sym] is a symbol, is the singleton type containing only that symbol}
@defform/none['val]{where @scheme[val] is a Scheme value, is the singleton type containing only that value}
@defform/none[i]{where @scheme[i] is an identifier can be a reference to a type
name or a type variable}
@defform[(Rec n t)]{is a recursive type where @scheme[n] is bound to the
@ -294,3 +294,18 @@ Other libraries can be used with Typed Scheme via
[check-version (-> (U Symbol (Listof Any)))])
(check-version)
]
@section{Typed Scheme Syntax Without Type Checking}
@defmodulelang[typed-scheme/no-check]
On occasions where the Typed Scheme syntax is useful, but actual
typechecking is not desired, the @schememodname[typed-scheme/no-check]
language is useful. It provides the same bindings and syntax as Typed
Scheme, but does no type checking.
Examples:
@schememod[typed-scheme/no-check
(: x Number)
(define x "not-a-number")]

View File

@ -11,4 +11,6 @@
define-typed-struct-internal
define-typed-struct/exec-internal
assert-predicate-internal
declare-refinement-internal
:-internal)

View File

@ -5,7 +5,7 @@
syntax/kerncase syntax/boundmap
(env type-name-env type-alias-env)
mzlib/trace
(private type-contract)
(private type-contract typed-renaming)
(rep type-rep)
(utils tc-utils)
"def-binding.ss")
@ -13,7 +13,8 @@
(require (for-template scheme/base
scheme/contract))
(provide remove-provides provide? generate-prov)
(provide remove-provides provide? generate-prov
get-alternate)
(define (provide? form)
(kernel-syntax-case form #f
@ -24,6 +25,12 @@
(define (remove-provides forms)
(filter (lambda (e) (not (provide? e))) (syntax->list forms)))
(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))))
(define (generate-prov stx-defs val-defs)
(define mapping (make-free-identifier-mapping))
(lambda (form)
@ -54,35 +61,35 @@
(define/contract cnt-id #,cnt id)
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer (syntax-property #'id
'not-free-identifier=? #t))
(make-rename-transformer (syntax-property #'cnt-id
'not-free-identifier=? #t))))
(renamer #'id #:alt #'cnt-id)
(renamer #'cnt-id)))
(#%provide (rename export-id out-id)))))]
[else
(with-syntax ([(export-id) (generate-temporaries #'(id))])
#`(begin
(with-syntax ([(export-id error-id) (generate-temporaries #'(id id))])
#`(begin
(define-syntax error-id
(lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id))))
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer (syntax-property #'id
'not-free-identifier=? #t))
(lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
(renamer #'id #:alt #'error-id)
(renamer #'error-id)))
(provide (rename-out [export-id out-id]))))])))]
[(mem? internal-id stx-defs)
=>
(lambda (b)
(with-syntax ([id internal-id]
[out-id external-id])
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
#`(begin
(with-syntax ([(export-id error-id) (generate-temporaries #'(id id))])
#`(begin
(define-syntax error-id
(lambda (stx)
(tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id))))
(define-syntax export-id
(if (unbox typed-context?)
(begin
(begin
(add-alias #'export-id #'id)
(make-rename-transformer (syntax-property #'id
'not-free-identifier=? #t)))
(lambda (stx)
(tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
(renamer #'id #:alt #'error-id))
(renamer #'error-id)))
(provide (rename-out [export-id out-id]))))))]
[(eq? (syntax-e internal-id) (syntax-e external-id))
#`(provide #,internal-id)]

View File

@ -576,7 +576,7 @@
[c:lv-clause
#:with (#%plain-app reverse n:id) #'c.e
#:with (v) #'(c.v ...)
#:when (free-identifier=? name #'v)
#:when (free-identifier=? name #'n)
(type-annotation #'v)]
[_ #f]))
(syntax-parse stx
@ -757,8 +757,8 @@
(match (tc-expr #'fn)
[(tc-result: (Function: arities))
(tc-keywords form arities (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected)]
[t (tc-error/expr #:return (ret (Un))
"Cannot apply expression of type ~a, since it is not a function type" t)])]
[(tc-result: t) (tc-error/expr #:return (ret (Un))
"Cannot apply expression of type ~a, since it is not a function type" t)])]
;; even more special case for match
[(#%plain-app (letrec-values ([(lp) (#%plain-lambda args . body)]) lp*) . actuals)
(and expected (not (andmap type-annotation (syntax->list #'args))) (free-identifier=? #'lp #'lp*))

View File

@ -136,7 +136,7 @@
(ret expected)]
[((? Type? t1) (? Type? t2))
(unless (subtype t1 t2)
(tc-error/expr"Expected ~a, but got ~a" t2 t1))
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
expected]))
(define (tc-expr/check form expected)

View File

@ -86,6 +86,7 @@
(define (mk/register-sty nm flds parent parent-field-types types
#:wrapper [wrapper values]
#:type-wrapper [type-wrapper values]
#:pred-wrapper [pred-wrapper values]
#:mutable [setters? #f]
#:proc-ty [proc-ty #f]
#:maker [maker* #f]
@ -104,6 +105,7 @@
(register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
#:wrapper wrapper
#:type-wrapper type-wrapper
#:pred-wrapper pred-wrapper
#:maker (or maker* maker)
#:constructor-return cret))))
@ -113,6 +115,7 @@
(define (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
#:wrapper [wrapper values]
#:type-wrapper [type-wrapper values]
#:pred-wrapper [pred-wrapper values]
#:maker [maker* #f]
#:constructor-return [cret #f])
;; create the approriate names that define-struct will bind
@ -125,7 +128,7 @@
(list (cons (or maker* maker)
(wrapper (->* external-fld-types (if cret cret name))))
(cons pred
(make-pred-ty (wrapper name))))
(make-pred-ty (pred-wrapper name))))
(map (lambda (g t) (cons g (wrapper (->* (list name) t)))) getters external-fld-types/no-parent)
(if setters?
(map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent)
@ -167,6 +170,7 @@
;; wrap everything in the approriate forall
#:wrapper (lambda (t) (make-Poly tvars t))
#:type-wrapper (lambda (t) (make-App t new-tvars #f))
#:pred-wrapper (lambda (t) (subst-all (for/list ([t tvars]) (list t Univ)) t))
#:poly? #t))

View File

@ -10,7 +10,7 @@
(rep type-rep)
(types utils convenience)
(private parse-type type-annotation type-contract)
(env type-env init-envs type-name-env type-alias-env)
(env type-env init-envs type-name-env type-alias-env lexical-env)
(utils tc-utils mutated-vars)
"provide-handling.ss"
"def-binding.ss"
@ -39,6 +39,17 @@
;; type aliases have already been handled by an earlier pass
[(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)))
(list)]
;; declare-refinement
[(define-values () (begin (quote-syntax (declare-refinement-internal pred)) (#%plain-app values)))
(match (lookup-type/lexical #'pred)
[(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
(register-type #'pred
(make-pred-ty (list dom)
rng
(make-Refinement dom #'pred (syntax-local-certifier))))
(list)]
[t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
;; require/typed
[(define-values () (begin (quote-syntax (require/typed-internal nm ty)) (#%plain-app values)))

View File

@ -3,8 +3,10 @@
(require "../utils/utils.ss")
(require (utils unit-utils)
mzlib/trace
(only-in scheme/unit provide-signature-elements)
"signatures.ss" "tc-toplevel.ss"
(only-in scheme/unit
provide-signature-elements
define-values/invoke-unit/infer link)
"signatures.ss" "tc-toplevel.ss"
"tc-new-if.ss" "tc-lambda-unit.ss" "tc-new-app-unit.ss"
"tc-let-unit.ss" "tc-dots-unit.ss"
"tc-expr-unit.ss" "check-subforms-unit.ss")

View File

@ -1,113 +1,6 @@
#lang scheme/base
(require scheme/unit
(for-syntax
scheme/base
(only-in srfi/1/list s:member delete-duplicates)
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)))
;; 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) (values (map car imps/exps) (map cadr 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 (sig-in-sigs? imp exps)
(for/or ([e exps]) (sig=? imp e)))
;; 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 (sig-in-sigs? imp exps))) imps))])
(values imps* exps*))))
(define (duplicates? sigs)
(for/or ([s sigs]
#:when
(> 1 (length (for/list ([s* sigs] #:when (free-identifier=? s s*)) s*))))
s))
(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)])
(cond [(duplicates? exps)
=>
(lambda (d)
(raise-syntax-error #f (format "multiple units export the signature ~a" d) stx))]
[else
(mk (delete-duplicates imps) exps units stx)]))]))
(require scheme/unit (for-syntax scheme/base))
;; 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@)
(define-signature y^ (y))
(define-unit x@ (import y^) (export))
(define-unit z@ (import y^) (export))
(define-values/link-units/infer x@ z@)
;(define-values/link-units/infer x@ y@)
|#