From 1edf62a912ac0468c2a995043c58826607d645dc Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 24 Apr 2009 21:21:06 +0000 Subject: [PATCH] resolve conflicts svn: r14598 --- collects/typed-scheme/env/init-envs.ss | 3 + collects/typed-scheme/env/lexical-env.ss | 2 +- collects/typed-scheme/env/type-env.ss | 2 +- collects/typed-scheme/env/type-name-env.ss | 2 +- collects/typed-scheme/infer/infer-unit.ss | 3 + collects/typed-scheme/infer/infer.ss | 7 +- collects/typed-scheme/private/base-env.ss | 27 ++++- collects/typed-scheme/private/parse-type.ss | 9 +- collects/typed-scheme/private/prims.ss | 9 +- .../typed-scheme/private/type-contract.ss | 7 +- .../typed-scheme/private/typed-renaming.ss | 20 ++++ collects/typed-scheme/rep/type-rep.ss | 15 ++- collects/typed-scheme/ts-guide.scrbl | 4 +- collects/typed-scheme/ts-reference.scrbl | 17 ++- .../typed-scheme/typecheck/internal-forms.ss | 2 + .../typecheck/provide-handling.ss | 43 ++++--- .../typed-scheme/typecheck/tc-app-unit.ss | 6 +- .../typed-scheme/typecheck/tc-expr-unit.ss | 2 +- collects/typed-scheme/typecheck/tc-structs.ss | 6 +- .../typed-scheme/typecheck/tc-toplevel.ss | 13 ++- .../typed-scheme/typecheck/typechecker.ss | 6 +- collects/typed-scheme/utils/unit-utils.ss | 109 +----------------- 22 files changed, 160 insertions(+), 154 deletions(-) create mode 100644 collects/typed-scheme/private/typed-renaming.ss diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss index dc5dc33090..396c94c4e4 100644 --- a/collects/typed-scheme/env/init-envs.ss +++ b/collects/typed-scheme/env/init-envs.ss @@ -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))] diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss index 9998ad3c99..07f8134c09 100644 --- a/collects/typed-scheme/env/lexical-env.ss +++ b/collects/typed-scheme/env/lexical-env.ss @@ -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 diff --git a/collects/typed-scheme/env/type-env.ss b/collects/typed-scheme/env/type-env.ss index dda31d6679..444aeebd73 100644 --- a/collects/typed-scheme/env/type-env.ss +++ b/collects/typed-scheme/env/type-env.ss @@ -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))) diff --git a/collects/typed-scheme/env/type-name-env.ss b/collects/typed-scheme/env/type-name-env.ss index 4c35e9d694..7c41a3dec4 100644 --- a/collects/typed-scheme/env/type-name-env.ss +++ b/collects/typed-scheme/env/type-name-env.ss @@ -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))) diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss index ea3648b095..18ff9b6548 100644 --- a/collects/typed-scheme/infer/infer-unit.ss +++ b/collects/typed-scheme/infer/infer-unit.ss @@ -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*) diff --git a/collects/typed-scheme/infer/infer.ss b/collects/typed-scheme/infer/infer.ss index b8c3788381..c660783ed0 100644 --- a/collects/typed-scheme/infer/infer.ss +++ b/collects/typed-scheme/infer/infer.ss @@ -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@)) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 2ce9716030..3b6ce0806f 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -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)] diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 0f8be85bb6..ef555e6cc6 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -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)]) diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss index 696c9c63cc..a5ec8287d1 100644 --- a/collects/typed-scheme/private/prims.ss +++ b/collects/typed-scheme/private/prims.ss @@ -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 ...)))])) \ No newline at end of file + (provide i ...)))])) + +(define-syntax (declare-refinement stx) + (syntax-parse stx + [(_ p:id) + (quasisyntax/loc stx #,(internal #'(declare-refinement-internal p)))])) \ No newline at end of file diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index 930437b763..87377316e5 100644 --- a/collects/typed-scheme/private/type-contract.ss +++ b/collects/typed-scheme/private/type-contract.ss @@ -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)))] diff --git a/collects/typed-scheme/private/typed-renaming.ss b/collects/typed-scheme/private/typed-renaming.ss new file mode 100644 index 0000000000..39f6bfaf72 --- /dev/null +++ b/collects/typed-scheme/private/typed-renaming.ss @@ -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])) diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index bfd1605f45..754884c03f 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -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* diff --git a/collects/typed-scheme/ts-guide.scrbl b/collects/typed-scheme/ts-guide.scrbl index 079a86fb02..d3af990ca0 100644 --- a/collects/typed-scheme/ts-guide.scrbl +++ b/collects/typed-scheme/ts-guide.scrbl @@ -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. diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl index c2982e2546..d2911b682b 100644 --- a/collects/typed-scheme/ts-reference.scrbl +++ b/collects/typed-scheme/ts-reference.scrbl @@ -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")] \ No newline at end of file diff --git a/collects/typed-scheme/typecheck/internal-forms.ss b/collects/typed-scheme/typecheck/internal-forms.ss index b85dd96c1e..a0ce6e9cb0 100644 --- a/collects/typed-scheme/typecheck/internal-forms.ss +++ b/collects/typed-scheme/typecheck/internal-forms.ss @@ -11,4 +11,6 @@ define-typed-struct-internal define-typed-struct/exec-internal assert-predicate-internal + declare-refinement-internal :-internal) + diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss index 66b3576a13..c214937592 100644 --- a/collects/typed-scheme/typecheck/provide-handling.ss +++ b/collects/typed-scheme/typecheck/provide-handling.ss @@ -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)] diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss index 61b4f54be6..63db7660b9 100644 --- a/collects/typed-scheme/typecheck/tc-app-unit.ss +++ b/collects/typed-scheme/typecheck/tc-app-unit.ss @@ -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*)) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index 328e373b6a..9640ef5a90 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -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) diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss index 4c6b019b4c..395a82bdc2 100644 --- a/collects/typed-scheme/typecheck/tc-structs.ss +++ b/collects/typed-scheme/typecheck/tc-structs.ss @@ -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)) diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss index fce1a1a30e..e881e3e48a 100644 --- a/collects/typed-scheme/typecheck/tc-toplevel.ss +++ b/collects/typed-scheme/typecheck/tc-toplevel.ss @@ -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))) diff --git a/collects/typed-scheme/typecheck/typechecker.ss b/collects/typed-scheme/typecheck/typechecker.ss index 2f41a66a9e..bfa104fe82 100644 --- a/collects/typed-scheme/typecheck/typechecker.ss +++ b/collects/typed-scheme/typecheck/typechecker.ss @@ -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") diff --git a/collects/typed-scheme/utils/unit-utils.ss b/collects/typed-scheme/utils/unit-utils.ss index 728edcd193..77b19a08ca 100644 --- a/collects/typed-scheme/utils/unit-utils.ss +++ b/collects/typed-scheme/utils/unit-utils.ss @@ -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@) -|#