diff --git a/typed-racket-lib/typed-racket/base-env/base-env.rkt b/typed-racket-lib/typed-racket/base-env/base-env.rkt index afe4f5a3..58b198f5 100644 --- a/typed-racket-lib/typed-racket/base-env/base-env.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-env.rkt @@ -25,6 +25,7 @@ (only-in (types numeric-tower) [-Number N]) (only-in (rep type-rep) make-ClassTop + make-UnitTop make-Name make-ValuesDots make-MPairTop @@ -1159,6 +1160,9 @@ [object-info (-> (-object) (-values (list (Un (make-ClassTop) (-val #f)) -Boolean)))] ;; TODO: class-info (is this sound to allow?) +;; Section 7.8 (Unit Utilities) +[unit? (make-pred-ty (make-UnitTop))] + ;; Section 9.1 [exn:misc:match? (-> Univ B)] ;; this is a hack diff --git a/typed-racket-lib/typed-racket/base-env/base-special-env.rkt b/typed-racket-lib/typed-racket/base-env/base-special-env.rkt index 8f0d94a0..032984e9 100644 --- a/typed-racket-lib/typed-racket/base-env/base-special-env.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-special-env.rkt @@ -13,6 +13,7 @@ (rename-in (types abbrev numeric-tower union) [make-arr* make-arr]) (for-syntax racket/base syntax/parse (only-in racket/syntax syntax-local-eval))) +(provide make-template-identifier) (define (make-template-identifier what where) (let ([name (module-path-index-resolve (module-path-index-join where #f))]) diff --git a/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt b/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt index 6b04dc76..4fdbb90b 100644 --- a/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt @@ -16,7 +16,7 @@ ;; special type names that are not bound to particular types (define-other-types -> ->* case-> U Rec All Opaque Vector - Parameterof List List* Class Object Values AnyValues Instance Refinement + Parameterof List List* Class Object Unit Values AnyValues Instance Refinement pred Struct Struct-Type Prefab Top Bot Distinction) (provide (rename-out [All ∀] diff --git a/typed-racket-lib/typed-racket/base-env/base-types.rkt b/typed-racket-lib/typed-racket/base-env/base-types.rkt index 087a037f..71451a05 100644 --- a/typed-racket-lib/typed-racket/base-env/base-types.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-types.rkt @@ -126,6 +126,7 @@ [Continuation-Mark-KeyTop -Continuation-Mark-KeyTop] [Struct-TypeTop (make-StructTypeTop)] [ClassTop (make-ClassTop)] +[UnitTop (make-UnitTop)] [Keyword -Keyword] [Thread -Thread] [Resolved-Module-Path -Resolved-Module-Path] diff --git a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt index 1fd42875..43667d38 100644 --- a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt +++ b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt @@ -19,13 +19,15 @@ (provide require/opaque-type require-typed-struct-legacy require-typed-struct require/typed-legacy require/typed require/typed/provide - require-typed-struct/provide cast make-predicate define-predicate) + require-typed-struct/provide cast make-predicate define-predicate + require-typed-signature) (module forms racket/base (require (for-syntax racket/lazy-require racket/base)) (begin-for-syntax (lazy-require [(submod "..") - (require/opaque-type + (require/opaque-type + require-typed-signature require-typed-struct-legacy require-typed-struct require/typed-legacy require/typed require/typed/provide @@ -36,7 +38,8 @@ (with-syntax ([(names ...) (generate-temporaries #'(id ...))]) #'(begin (provide (rename-out [names id] ...)) (define-syntax (names stx) (id stx)) ...))])) - (def require/opaque-type + (def require/opaque-type + require-typed-signature require-typed-struct-legacy require-typed-struct require/typed-legacy require/typed require/typed/provide @@ -121,6 +124,11 @@ (~var constructor (opt-constructor legacy #'nm.nm))] #:with (constructor-parts ...) #'constructor.value)) + (define-syntax-class signature-clause + #:literals (:) + #:attributes (sig-name [var 1] [type 1]) + (pattern [#:signature sig-name:id ([var:id : type] ...)])) + (define-syntax-class opaque-clause ;#:literals (opaque) #:attributes (ty pred opt) @@ -135,6 +143,8 @@ #`(require/opaque-type oc.ty oc.pred #,lib . oc.opt)) (pattern (~var strc (struct-clause legacy)) #:attr spec #`(require-typed-struct strc.nm (strc.body ...) strc.constructor-parts ... #,lib)) + (pattern sig:signature-clause #:attr spec + #`(require-typed-signature sig.sig-name (sig.var ...) (sig.type ...) #,lib)) (pattern sc:simple-clause #:attr spec #`(require/typed #:internal sc.nm sc.ty #,lib))) @@ -442,3 +452,18 @@ [sel (nm -> ty)]) ...)))])) (values (rts #t) (rts #f)))) + +(define (require-typed-signature stx) + (syntax-parse stx + #:literals (:) + [(_ sig-name:id (var ...) (type ...) lib) + (quasisyntax/loc stx + (begin + (require (only-in lib sig-name)) + #,(internal (quasisyntax/loc stx + (define-signature-internal sig-name + #:parent-signature #f + ([var type] ...) + ;; infer parent relationships using the static information + ;; bound to this signature + #:check? #t)))))])) diff --git a/typed-racket-lib/typed-racket/base-env/signature-prims.rkt b/typed-racket-lib/typed-racket/base-env/signature-prims.rkt new file mode 100644 index 00000000..b225d440 --- /dev/null +++ b/typed-racket-lib/typed-racket/base-env/signature-prims.rkt @@ -0,0 +1,108 @@ +#lang racket/base + +;; This file implements unit signatures for typed racket + +(provide define-signature) + +(require "../utils/utils.rkt" + "colon.rkt" + (for-syntax syntax/parse + racket/base + racket/list + racket/syntax + syntax/kerncase + "../private/syntax-properties.rkt" + (typecheck internal-forms) + syntax/id-table + racket/dict + racket/unit-exptime + (utils tc-utils)) + (only-in racket/unit + [define-signature untyped-define-signature] + extends) + (for-label "colon.rkt") + (submod "../typecheck/internal-forms.rkt" forms) + (only-in "../../typed/racket/base.rkt" define-type)) + +(begin-for-syntax + (define-literal-set colon #:for-label (:)) + + ;; TODO: there should be a more extensible way of handling signatures + (define-syntax-class signature-forms + (pattern (form:def-sig-form ...))) + + (define-syntax-class def-sig-form + #:attributes (internal-form erased) + (pattern :sig-var-form + #:attr kind 'var) + ;; The define-type form is explicitly disallowed until I can figure out how + ;; to sensibly support them in signature definitions - dfeltey + (pattern :sig-type-form + #:fail-when #t "type definitions are not allowed within signature definitions" + #:attr kind 'type)) + + (define-syntax-class sig-var-form + #:literal-sets (colon) + (pattern [name:id : type] + #:with internal-form #'(name type) + #:with erased #'name)) + + ;; Preliminary support for type definitions in signatures + ;; The form is allowed in signature definitions, but currently + ;; fails on parsing. + ;; In the future supporting type definitions inside of signatures + ;; would be a worthwhile feature, but their implemention is not obvious + (define-syntax-class sig-type-form + #:literals (define-type) + (pattern (define-type t ty) + ;; These attributes are dummy values + #:attr internal-form #f + #:attr erased #f)) + + (define-splicing-syntax-class extends-form + #:literals (extends) + (pattern (~seq extends super:id) + #:with internal-form #'super + #:with extends-id #'super + #:attr form #'(extends super)) + (pattern (~seq) + #:with internal-form #'#f + #:with extends-id '() + #:attr form '()))) + + +;; process-signature-forms : (listof syntax?) -> (listof (pairof id id)) +;; Processes the raw syntax of signature forms and returns a list +;; of pairs representing names and types bound by the signature +(define-for-syntax (process-signature-forms forms) + (for/list ([form (in-list forms)]) + (syntax-parse form + [member:sig-var-form + (syntax-e #'member.internal-form)]))) + + +;; typed define-signature macro +;; This expands into the untyped define-signature syntax as well as an +;; internal form used by TR to register signatures in the signature environment +;; The `define-signature-internal` form specifies +;; - the `name` of the signature being defined +;; - it's parent-signature, or #f if this signature does not extend another signature +;; - the list of member variables contained in this signature along with their types +;; - and a boolean flag indicating whether the signature came from an instance of +;; require/typed in which case additional checking must occur when the internal +;; form is parsed +(define-syntax (define-signature stx) + (syntax-parse stx + [(_ sig-name:id super-form:extends-form forms:signature-forms) + (define members (process-signature-forms (syntax->list #'forms))) + (define erased-members (map car members)) + #`(begin + #,(ignore (quasisyntax/loc stx + (untyped-define-signature sig-name #,@(attribute super-form.form) + (#,@erased-members)))) + #,(internal (quasisyntax/loc stx + (define-signature-internal sig-name + #:parent-signature super-form.internal-form + (#,@members) + ;; no need to further check parent information + #:check? #f))))])) diff --git a/typed-racket-lib/typed-racket/base-env/unit-prims.rkt b/typed-racket-lib/typed-racket/base-env/unit-prims.rkt new file mode 100644 index 00000000..3aa63f8c --- /dev/null +++ b/typed-racket-lib/typed-racket/base-env/unit-prims.rkt @@ -0,0 +1,492 @@ +#lang racket/base + +;; Primitive forms for units/signatures + +(provide unit + define-unit + compound-unit + define-compound-unit + compound-unit/infer + define-compound-unit/infer + invoke-unit + invoke-unit/infer + define-values/invoke-unit + define-values/invoke-unit/infer + unit-from-context + define-unit-from-context) + + +(require "../utils/utils.rkt" + "colon.rkt" + (for-syntax syntax/parse + racket/base + racket/list + racket/match + racket/syntax + racket/sequence + syntax/context + syntax/flatten-begin + syntax/kerncase + "../private/syntax-properties.rkt" + (typecheck internal-forms) + syntax/id-table + racket/dict + racket/unit-exptime + syntax/strip-context + (utils tc-utils) + syntax/id-table + syntax/id-set) + (prefix-in untyped- (only-in racket/unit + define-signature + unit + invoke-unit + invoke-unit/infer + compound-unit + define-unit + define-compound-unit + define-values/invoke-unit + define-values/invoke-unit/infer + compound-unit/infer + define-compound-unit/infer + unit-from-context + define-unit-from-context)) + (only-in racket/unit + extends + import + export + init-depend + link + prefix + rename) + "base-types.rkt" + "base-types-extra.rkt" + (for-label "colon.rkt") + (for-template (rep type-rep)) + (submod "../typecheck/internal-forms.rkt" forms)) + +(begin-for-syntax + (define-literal-set colon #:for-label (:)) + + ;; process-definition-form handles all of the `define-` style unit macros + ;; such as define-unit, define-compound-unit, define-unit-from-context. but + ;; not the corresponding unit, compound-unit, etc forms + ;; Performs local expansion in order to apply a syntax property to the + ;; subexpression of the `define-*` form correpsonding to the body of the + ;; definition being created + ;; - eg for a define-unit form, a syntax property will be attached to the + ;; subexpression that creates the unit + (define (process-definition-form apply-property stx) + (define exp-stx (local-expand stx (syntax-local-context) (kernel-form-identifier-list))) + (syntax-parse exp-stx + #:literal-sets (kernel-literals) + [(begin e ...) + (quasisyntax/loc stx + (begin #,@(map (λ (e) (process-definition-form apply-property e)) + (syntax->list #'(e ...)))))] + [(define-values (name ...) rhs) + (quasisyntax/loc stx (define-values (name ...) #,(ignore (apply-property #'rhs))))] + ;; define-syntaxes that actually create the binding given in the + ;; `define-*` macro will fall through to this case, and should be left as-is + [_ exp-stx])) + + + (define-splicing-syntax-class init-depend-form + #:literals (init-depend) + (pattern (~and this-syntax (init-depend sig:id ...)) + #:attr form (list #'this-syntax) + #:with names #'(sig ...)) + (pattern (~seq) + #:attr form '() + #:with names #'())) + + ;; The `rename` attribute in the sig-spec syntax class is used to correctly + ;; map names of signature bound variables in unit bodies to their names in + ;; the fully expanded syntax. It applies prefixes and renamings from + ;; signature specifications to identifiers. + (define-syntax-class sig-spec + #:literals (prefix rename) + (pattern sig-id:id + #:attr rename (lambda (id) id) + #:with sig-name #'sig-id) + (pattern (prefix p:id sig:sig-spec) + #:attr rename (lambda (id) (format-id #'sig.sig-name + "~a~a" + #'p + ((attribute sig.rename) id))) + #:with sig-name #'sig.sig-name) + (pattern (rename sig:sig-spec (new:id old:id) ...) + #:attr rename + (lambda (id) + (define (lookup id) + (for/first ([old-id (in-syntax #'(old ...))] + [new-id (in-syntax #'(new ...))] + #:when (free-identifier=? id old-id)) + new-id)) + (define rn ((attribute sig.rename) id)) + (or (lookup rn) rn)) + #:with sig-name #'sig.sig-name))) + + +;; imports/members : identifier? -> syntax? +;; given an identifier bound to a signature +;; returns syntax containing the signature name and the names of each variable contained +;; in the signature, this is needed to typecheck define-values/invoke-unit forms +(define-for-syntax (imports/members sig-id) + (define-values (_1 imp-mem _2 _3) (signature-members sig-id sig-id)) + #`(#,sig-id #,@(map (lambda (id) + (local-expand + id + (syntax-local-context) + (kernel-form-identifier-list))) + imp-mem))) + +;; Given a list of signature specs +;; Processes each signature spec to determine the variables exported +;; and produces syntax containing the signature id and the exported variables +(define-for-syntax (process-dv-exports es) + (for/list ([e (in-list es)]) + (syntax-parse e + [s:sig-spec + (define sig-id #'s.sig-name) + (define renamer (attribute s.rename)) + (define-values (_1 ex-mem _2 _3) (signature-members sig-id sig-id)) + #`(#,sig-id #,@(map renamer ex-mem))]))) + +;; Typed macro for define-values/invoke-unit +;; This has to be handled specially because the types of +;; the defined values must be registered in the environment +(define-syntax (define-values/invoke-unit stx) + (syntax-parse stx + #:literals (import export) + [(_ unit-expr + (import isig:sig-spec ...) + (export esig:sig-spec ...)) + (define imports-stx (syntax->list #'(isig.sig-name ...))) + (define exports-stx (syntax->list #'(esig ...))) + (define/with-syntax temp (syntax-local-introduce (generate-temporary))) + #`(begin + #,(internal (quasisyntax/loc stx + (define-values/invoke-unit-internal + (#,@(map imports/members imports-stx)) + (#,@(process-dv-exports exports-stx))))) + (: temp (Unit (import isig.sig-name ...) + (export esig.sig-name ...) + (init-depend isig.sig-name ...) + AnyValues)) + (define temp unit-expr) + #,(ignore (quasisyntax/loc stx + (untyped-define-values/invoke-unit unit-expr + (import isig ...) + (export esig ...)))))])) +(begin-for-syntax + ;; flat signatures allow easy comparisons of whether one + ;; such flat-signature implements another + ;; - name is the identifier corresponding to the signatures name + ;; - implements is a free-id-set of this signature and all its ancestors + ;; flat-signatures enable a comparison of whether one signature implements + ;; another as a subset comparison on their contained sets of parent signatures + (struct flat-signature (name implements) #:transparent) + + ;; implements? : flat-signature? flat-signature? -> Boolean + ;; true iff signature sig1 implements signature sig2 + (define (implements? sig1 sig2) + (match* (sig1 sig2) + [((flat-signature name1 impls1) (flat-signature name2 impls2)) + (free-id-subset? impls2 impls1)])) + + ;; Given: a list of identifiers bound to static unit information + ;; Returns: two lists + ;; 1. A list of flat-signatures representing the signatures imported by + ;; the given units + ;; 2. A list of flat-signatures representing the signatures exported by + ;; the given units + (define (get-imports/exports unit-ids) + (define-values (imports exports) + (for/fold ([imports null] + [exports null]) + ([unit-id (in-list unit-ids)]) + (match-define-values ((list (cons _ new-imports) ...) + (list (cons _ new-exports) ...)) + (unit-static-signatures unit-id unit-id)) + (values (append imports new-imports) (append exports new-exports)))) + (values (map make-flat-signature imports) + (map make-flat-signature exports))) + + ;; Given the id of a signature, return a corresponding flat-signature + (define (make-flat-signature sig-name) + (flat-signature sig-name (get-signature-ancestors sig-name))) + + ;; Walk the chain of parent signatures to build a list, and convert it to + ;; a free-id-set + (define (get-signature-ancestors sig) + (immutable-free-id-set + (with-handlers ([exn:fail:syntax? (λ (e) null)]) + (let loop ([sig sig] [ancestors null]) + (define-values (parent _1 _2 _3) (signature-members sig sig)) + (if parent + (loop parent (cons sig ancestors)) + (cons sig ancestors)))))) + + ;; Calculate the set of inferred imports for a list of units + ;; The inferred imports are those which are not provided as + ;; exports from any of the units taking signature subtyping into account + (define (infer-imports unit-ids) + (define-values (imports exports) (get-imports/exports unit-ids)) + (define remaining-imports (remove* exports imports implements?)) + (map flat-signature-name remaining-imports)) + + ;; infer-exports returns all the exports from linked + ;; units rather than just those that are not also + ;; imported + (define (infer-exports unit-ids) + (define-values (imports exports) (get-imports/exports unit-ids)) + (map flat-signature-name exports)) + + (define-splicing-syntax-class maybe-exports + #:literals (export) + (pattern (~seq) + #:attr exports #f) + (pattern (export sig:id ...) + #:attr exports (syntax->list #'(sig ...)))) + + (define-syntax-class dviu/infer-unit-spec + #:literals (link) + (pattern unit-id:id + #:attr unit-ids (list #'unit-id)) + (pattern (link uid-inits:id ...) + #:attr unit-ids (syntax->list #'(uid-inits ...))))) + +;; Note: This may not correctly handle all use cases of +;; define-values/invoke-unit/infer +;; inferred imports and exports are handled in the following way +;; - the exports of ALL units being linked are added to the export list +;; to be registered in tc-toplevel, this appears to be how exports are treated +;; by the unit inference process +;; - inferred imports are those imports which are not provided by +;; any of the exports +;; This seems to correctly handle both recursive and non-recursive +;; linking patterns +(define-syntax (define-values/invoke-unit/infer stx) + (syntax-parse stx + [(_ exports:maybe-exports us:dviu/infer-unit-spec) + (define inferred-imports (infer-imports (attribute us.unit-ids))) + (define inferred-exports (or (attribute exports.exports) + (infer-exports (attribute us.unit-ids)))) + #`(begin + #,(internal (quasisyntax/loc stx + (define-values/invoke-unit-internal + (#,@(map imports/members inferred-imports)) + (#,@(process-dv-exports inferred-exports))))) + #,(ignore + (quasisyntax/loc stx (untyped-define-values/invoke-unit/infer #,@#'exports us))))])) + +(define-syntax (invoke-unit/infer stx) + (syntax-parse stx + [(_ . rest) + (ignore + (tr:unit:invoke-property + (quasisyntax/loc stx (untyped-invoke-unit/infer . rest)) 'infer))])) + +;; The typed invoke-unit macro must attach a syntax property to the expression +;; being invoked in order to reliably find it during typechecking. +;; Otherwise the expanded syntax may be confused for that of invoke-unit/infer +;; and be typechecked incorrectly +(define-syntax (invoke-unit stx) + (syntax-parse stx + [(invoke-unit expr . rest) + (ignore + (tr:unit:invoke-property + (quasisyntax/loc stx + (untyped-invoke-unit + #,(tr:unit:invoke:expr-property #'expr #t) + . rest)) #t))])) + +;; Trampolining macro that cooperates with the unit macro in order +;; to add information needed for typechecking units +;; Essentially head expands each expression in the body of a unit +;; - leaves define-syntaxes forms alone, to allow for macro definitions in unit bodies +;; - Inserts syntax into define-values forms that allow mapping the names of definitions +;; to their bodies during type checking +;; - Also specially handles type annotations in order to correctly associate variables +;; with their types +;; - All other expressions are marked as 'expr for typechecking +(define-syntax (add-tags stx) + (syntax-parse stx + [(_ e) + (define exp-e (local-expand #'e (syntax-local-context) (kernel-form-identifier-list))) + (syntax-parse exp-e + #:literals (begin define-values define-syntaxes :) + [(begin b ...) + #'(add-tags b ...)] + [(define-syntaxes (name:id ...) rhs:expr) + exp-e] + ;; Annotations must be handled specially + ;; Exported variables are renamed internally in units, which leads + ;; to them not being correctly associated with their type annotations + ;; This extra bit of inserted syntax allows the typechecker to + ;; properly associate all annotated variables with their types. + ;; The inserted lambda expression will be expanded to the internal + ;; name of the variable being annotated, this internal name + ;; can then be associated with the type annotation during typechecking + [(define-values () (colon-helper (: name:id type) rest ...)) + (quasisyntax/loc stx + (define-values () + #,(tr:unit:body-exp-def-type-property + #`(#%expression + (begin (void (lambda () name)) + (colon-helper (: name type) rest ...))) + 'def/type)))] + [(define-values (name:id ...) rhs) + (quasisyntax/loc stx + (define-values (name ...) + #,(tr:unit:body-exp-def-type-property + #'(#%expression + (begin + (void (lambda () name ... (void))) + rhs)) + 'def/type)))] + [_ + (tr:unit:body-exp-def-type-property exp-e 'expr)])] + [(_ e ...) + #'(begin (add-tags e) ...)])) + +(define-syntax (unit stx) + (syntax-parse stx + #:literals (import export) + [(unit imports exports init-depends:init-depend-form e ...) + (ignore + (tr:unit + (quasisyntax/loc stx + (untyped-unit + imports + exports + #,@(attribute init-depends.form) + (add-tags e ...)))))])) + +(define-syntax (define-unit stx) + (syntax-parse stx + #:literals (import export) + [(define-unit uid:id + imports + exports + init-depends:init-depend-form + e ...) + (process-definition-form + (λ (stx) (tr:unit stx)) + (quasisyntax/loc stx + (untyped-define-unit uid + imports + exports + #,@(attribute init-depends.form) + (add-tags e ...))))])) + +(begin-for-syntax + (define-syntax-class compound-imports + #:literals (import) + (pattern (import lb:link-binding ...) + #:attr import-tags (syntax->list #'(lb.link-id ...)))) + (define-syntax-class compound-links + #:literals (link) + (pattern (link ld:linkage-decl ...) + #:attr all-export-links (map syntax->list (syntax->list #'(ld.exported-keys ...))) + #:attr all-import-links (map syntax->list (syntax->list #'(ld.imported-keys ...))))) + (define-syntax-class linkage-decl + (pattern ((lb:link-binding ...) + unit-expr:expr + link-id:id ...) + #:attr exported-keys #'(lb.link-id ...) + #:with imported-keys #'(link-id ...))) + (define-syntax-class link-binding + (pattern (link-id:id : sig-id:id))) + + ;; build-compound-unit-prop : (listof id) (listof (listof id?)) (listof id?) + ;; -> (list (listof symbol?) + ;; (listof (listof symbol?)) + ;; (listof (listof symbol?))) + ;; Process the link bindings of a compound-unit form + ;; to return a syntax property used for typechecking compound-unit forms + ;; The return value is a list to be attached as a syntax property to compound-unit + ;; forms. + ;; The list contains 3 elements + ;; - The first element is a list of symbols corresponding to the link-ids of + ;; the compound-unit's imports + ;; - The second element is a list of lists of symbols, corresponding to the + ;; link-ids exported by units in the compound-unit's linking clause + ;; - The last element is also a list of lists of symbols, corresponding to the + ;; link-ids being imported by units in the compound-unit's linking clause + (define (build-compound-unit-prop import-tags all-import-links all-export-links) + (define table + (make-immutable-free-id-table + (for/list ([link (in-list (append import-tags (flatten all-export-links)))]) + (cons link (gensym (syntax-e link)))))) + (define imports-tags + (map (λ (id) (free-id-table-ref table id #f)) import-tags)) + (define units-exports + (map + (λ (lst) (map (λ (id) (free-id-table-ref table id #f)) lst)) + all-export-links)) + (define units-imports + (for/list ([unit-links (in-list all-import-links)]) + (for/list ([unit-link (in-list unit-links)]) + (free-id-table-ref table unit-link #f)))) + (list imports-tags units-exports units-imports))) + +(define-syntax (compound-unit stx) + (syntax-parse stx + [(_ imports:compound-imports + exports + links:compound-links) + (define import-tags (attribute imports.import-tags)) + (define all-import-links (attribute links.all-import-links)) + (define all-export-links (attribute links.all-export-links)) + (define prop (build-compound-unit-prop import-tags all-import-links all-export-links)) + (ignore (tr:unit:compound-property + (quasisyntax/loc stx (untyped-compound-unit imports exports links)) + prop))])) + +(define-syntax (define-compound-unit stx) + (syntax-parse stx + [(_ uid + imports:compound-imports + exports + links:compound-links) + (define import-tags (attribute imports.import-tags)) + (define all-import-links (attribute links.all-import-links)) + (define all-export-links (attribute links.all-export-links)) + (define prop (build-compound-unit-prop import-tags all-import-links all-export-links)) + (process-definition-form + (λ (stx) (tr:unit:compound-property stx prop)) + (quasisyntax/loc stx + (untyped-define-compound-unit uid imports exports links)))])) + +(define-syntax (compound-unit/infer stx) + (syntax-parse stx + #:literals (import export link) + [(_ . rest) + (ignore + (tr:unit:compound-property + (quasisyntax/loc stx + (untyped-compound-unit/infer . rest)) + 'infer))])) + +(define-syntax (define-compound-unit/infer stx) + (syntax-parse stx + [(_ . rest) + (process-definition-form + (λ (stx) (tr:unit:compound-property stx'infer)) + (quasisyntax/loc stx (untyped-define-compound-unit/infer . rest)))])) + +(define-syntax (unit-from-context stx) + (syntax-parse stx + [(_ . rest) + (ignore + (tr:unit:from-context + (quasisyntax/loc stx + (untyped-unit-from-context . rest))))])) + +(define-syntax (define-unit-from-context stx) + (syntax-parse stx + [(_ . rest) + (process-definition-form + (λ (stx) (tr:unit:from-context stx)) + (quasisyntax/loc stx (untyped-define-unit-from-context . rest)))])) diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt index 568538d6..7c9f66d9 100644 --- a/typed-racket-lib/typed-racket/env/init-envs.rkt +++ b/typed-racket-lib/typed-racket/env/init-envs.rkt @@ -8,11 +8,12 @@ "type-name-env.rkt" "type-alias-env.rkt" "mvar-env.rkt" + "signature-env.rkt" (rename-in racket/private/sort [sort raw-sort]) (rep type-rep object-rep filter-rep rep-utils free-variance) (for-syntax syntax/parse racket/base) (types abbrev union) - racket/dict racket/list + racket/dict racket/list racket/promise mzlib/pconvert racket/match) (provide ;; convenience form for defining an initial environment @@ -26,7 +27,8 @@ tvariance-env-init-code talias-env-init-code env-init-code - mvar-env-init-code) + mvar-env-init-code + signature-env-init-code) (define-syntax (define-initial-env stx) (syntax-parse stx @@ -118,6 +120,16 @@ (set-box! cache-box (dict-set (unbox cache-box) v (list name class-type)))) (if cache-box name class-type)])] + [(Signature: name extends mapping) + (define (serialize-mapping m) + (map (lambda (id/ty) + (define id (car id/ty)) + (define ty (force (cdr id/ty))) + `(cons (quote-syntax ,id) ,(sub ty))) + m)) + `(make-Signature (quote-syntax ,name) + (quote-syntax ,extends) + (list ,@(serialize-mapping mapping)))] [(arr: dom rng rest drest kws) `(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))] [(TypeFilter: t p) @@ -184,3 +196,8 @@ (make-init-code (λ (f) (dict-map mvar-env f)) (lambda (id v) (and v #`(register-mutated-var #'#,id))))) + +(define (signature-env-init-code) + (make-init-code + signature-env-map + (lambda (id sig) #`(register-signature! #'#,id #,(quote-type sig))))) diff --git a/typed-racket-lib/typed-racket/env/signature-env.rkt b/typed-racket-lib/typed-racket/env/signature-env.rkt new file mode 100644 index 00000000..23618960 --- /dev/null +++ b/typed-racket-lib/typed-racket/env/signature-env.rkt @@ -0,0 +1,69 @@ +#lang racket/base + +;; Environment for signature definitions +;; to track bindings and type definitions inside of signatures + +(provide register-signature! + finalize-signatures! + lookup-signature + signature-env-map + with-signature-env/extend) + +(require syntax/id-table + racket/match + racket/promise + (for-syntax syntax/parse racket/base) + "../utils/utils.rkt" + (utils tc-utils) + (rep type-rep)) + +;; initial signature environment +(define signature-env (make-parameter (make-immutable-free-id-table))) + +;; register-signature! : identifier? Signature? -> Void +;; adds a mapping from the given identifier to the given signature +;; in the signature environment +(define (register-signature! id sig) + (when (lookup-signature id) + (tc-error/fields "duplicate signature definition" + "identifier" (syntax-e id))) + (signature-env (free-id-table-set (signature-env) id sig))) + + +(define-syntax-rule (with-signature-env/extend ids sigs . b) + (let ([ids* ids] + [sigs* sigs]) + (define new-env + (for/fold ([env (signature-env)]) + ([id (in-list ids*)] + [sig (in-list sigs*)]) + (free-id-table-set env id sig))) + (parameterize ([signature-env new-env]) . b))) + +;; Iterate over the signature environment forcing the types of bindings +;; in each signature +(define (finalize-signatures!) + (signature-env + (make-immutable-free-id-table + (signature-env-map + (lambda (id sig) + (cons + id + (match sig + [(Signature: name extends mapping) + (make-Signature + name + extends + (map + (match-lambda [(cons id ty) (cons id (force ty))]) + mapping))] + [_ #f]))))))) + +;; lookup-signature : identifier? -> (or/c #f Signature?) +;; look up the signature corresponding to the given identifier +;; in the signature environment +(define (lookup-signature id) + (free-id-table-ref (signature-env) id #f)) + +(define (signature-env-map f) + (free-id-table-map (signature-env) f)) diff --git a/typed-racket-lib/typed-racket/env/signature-helper.rkt b/typed-racket-lib/typed-racket/env/signature-helper.rkt new file mode 100644 index 00000000..d7ac170f --- /dev/null +++ b/typed-racket-lib/typed-racket/env/signature-helper.rkt @@ -0,0 +1,157 @@ +#lang racket/base + +;; This module provides helper functions for typed signatures + +(require "../utils/utils.rkt" + syntax/id-set + (utils tc-utils) + (env signature-env) + (rep type-rep) + (private parse-type) + syntax/parse + racket/list + racket/match + racket/promise + racket/unit-exptime + (for-template racket/base + (submod "../typecheck/internal-forms.rkt" forms))) + +(provide parse-and-register-signature! signature->bindings signatures->bindings) + +;; parse-signature : Syntax -> Signature +;; parses the internal syntax of a signature form to build the internal representation +;; of a typed signature and registers the internal representation with the +;; Signature environment +;; The parsed syntax is created by uses of `define-signature-internal` which are +;; inserted by the typed version of the `define-signature` macro, this function +;; uses that syntax to created a Typed Representation of the signature to +;; place in the Signature environment +;; The parsed syntax contains the following fields: +;; - name is the name of the signature being defined +;; - the parent-signature is the name of the signature being extended or #f +;; if the signature defintion does not extend any signature +;; - a list of bindings, each of the form [name : Type], for each variable +;; in the signature +;; - The check field indicates that this syntax came from a use of require/typed +;; using the #:signature clause, and listed bindings muct be checked to ensure +;; they are consistent with the statically known signature variables +(define (parse-and-register-signature! form) + (syntax-parse form + #:literal-sets (kernel-literals) + #:literals (values define-signature-internal) + [(define-values () + (begin + (quote-syntax + (define-signature-internal name + #:parent-signature super + (binding ...) + #:check? check) #:local) + (#%plain-app values))) + (define raw-map (syntax->list #'(binding ...))) + (define check? (syntax->datum #'check)) + (define extends (get-extended-signature #'name #'super check? form)) + (define super-bindings (get-signature-mapping extends)) + (define new-bindings (map parse-signature-binding raw-map)) + (define pre-mapping (append super-bindings new-bindings)) + + ;; Make sure a require/typed signature has bindings listed + ;; that are consistent with its statically determined bindings + (when check? + (check-signature-bindings #'name (map car pre-mapping) form)) + + ;; require/typed signature bindings may not be in the correct order + ;; this fixes the ordering based on the static order determined + ;; by signature-members + (define mapping (if check? + (fix-order #'name pre-mapping) + pre-mapping)) + (define signature (make-Signature #'name extends mapping)) + (register-signature! #'name signature)])) + +;; check-signature-bindings : Identifier (Listof Identifier) -> Void +;; checks that the bindings of a signature identifier are consistent with +;; those listed in a require/typed clause +(define (check-signature-bindings name vars stx) + (match-define-values (_ inferred-vars inferred-defs _) (signature-members name name)) + (define (make-id-set set) (immutable-free-id-set set #:phase (add1 (syntax-local-phase-level)))) + (define inferred-vars-set (make-id-set inferred-vars)) + (define vars-set (make-id-set vars)) + (unless (empty? inferred-defs) + (tc-error/stx name "untyped signatures containing definitions are prohibited")) + (unless (free-id-set=? inferred-vars-set vars-set) + (tc-error/fields "required signature declares inconsistent members" + "expected members" (map syntax-e inferred-vars) + "received members" (map syntax-e vars) + #:stx stx))) + +;; get-extended-signature : Identifier Syntax Boolean -> (Option Signature) +;; Checks if the extended signature information must be inferred and looks +;; up the super signature in the environment +;; Raises an error if a super signature is inferred that is not in the +;; signature environment indicative of a signature that should be require/typed +;; but was not, a typed binding for the parent signature is necessary to correctly +;; check subtyping for units +(define (get-extended-signature name super check? stx) + (cond + [check? + (match-define-values (inferred-super _ _ _) (signature-members name name)) + (and inferred-super + (or (and (lookup-signature inferred-super) inferred-super) + (tc-error/fields "required signature extends an untyped signature" + "required signature" (syntax-e name) + "extended signature" (syntax-e inferred-super) + #:stx stx)))] + [(not (syntax->datum super)) #f] + ;; This case should probably be an error, because if the signature was not false + ;; the lookup may still silently fail which should not be allowed here + [else (or (and (lookup-signature super) super) + (tc-error/fields "signature definition extends untyped signature" + "in the definition of signature" (syntax-e name) + "which extends signature" (syntax-e super) + #:stx stx))])) + +;; parse-signature-binding : Syntax -> (list/c identifier? syntax?) +;; parses the binding forms inside of a define signature into the +;; form used by the Signature type representation +;; The call to `parse-type` is delayed to allow signatures and type aliases +;; to be mutually recursive, after aliases are registered in the environment +;; the promise will be forced to perform the actual type parsing +(define (parse-signature-binding binding-stx) + (syntax-parse binding-stx + [[name:id type] + (cons #'name (delay (parse-type #'type)))])) + +;; signature->bindings : identifier? -> (listof (cons/c identifier? type?)) +;; GIVEN: a signature name +;; RETURNS: the list of variables bound by that signature +;; inherited bindings come first +(define (signature->bindings sig-id) + (define sig (lookup-signature sig-id)) + (let loop ([sig (Signature-extends sig)] + [mapping (Signature-mapping sig)] + [bindings null]) + (if sig + (loop (Signature-extends (lookup-signature sig)) + (Signature-mapping (lookup-signature sig)) + (append mapping bindings)) + (append mapping bindings)))) + +;; (listof identifier?) -> (listof (cons/c identifier? type?)) +;; GIVEN: a list of signature names +;; RETURNS: the list of all bindings from those signatures +;; TODO: handle required renamings/prefix/only/except +(define (signatures->bindings ids) + (append-map signature->bindings ids)) + +;; get-signature-mapping : (Option Signature) -> (Listof (Cons Id Type)) +(define (get-signature-mapping sig) + (if sig (Signature-mapping (lookup-signature sig)) null)) + +;; fix-order : id (listof (cons/c id type?)) -> (listof (cons/c id type?) +;; Returns a reordered list of signature bindings to match the order given +;; by signature-members +(define (fix-order sig-id sig-bindings) + (match-define-values (_ members _ _) (signature-members sig-id sig-id)) + (map + (lambda (id) (assoc id sig-bindings free-transformer-identifier=?)) + members)) diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index 29f20350..60b985e5 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -5,13 +5,14 @@ (require "../utils/utils.rkt" (except-in (rep type-rep object-rep) make-arr) (rename-in (types abbrev union utils filter-ops resolve - classes prefab) + classes prefab signatures) [make-arr* make-arr]) (utils tc-utils stxclass-util literal-syntax-class) syntax/stx (prefix-in c: (contract-req)) syntax/parse racket/sequence (env tvar-env type-alias-env mvar-env - lexical-env index-env row-constraint-env) + lexical-env index-env row-constraint-env + signature-env) racket/dict racket/list racket/promise @@ -20,6 +21,7 @@ "parse-classes.rkt" (for-label (except-in racket/base case-lambda) + racket/unit "../base-env/colon.rkt" "../base-env/base-types-extra.rkt" ;; match on the `case-lambda` binding in the TR primitives @@ -79,6 +81,10 @@ (define-literal-syntax-class #:for-label cons) (define-literal-syntax-class #:for-label Class) (define-literal-syntax-class #:for-label Object) +(define-literal-syntax-class #:for-label Unit) +(define-literal-syntax-class #:for-label import) +(define-literal-syntax-class #:for-label export) +(define-literal-syntax-class #:for-label init-depend) (define-literal-syntax-class #:for-label Refinement) (define-literal-syntax-class #:for-label Instance) (define-literal-syntax-class #:for-label List) @@ -376,6 +382,42 @@ "given" v) (make-Instance (Un))) (make-Instance v)))] + [(:Unit^ (:import^ import:id ...) + (:export^ export:id ...) + (~optional (:init-depend^ init-depend:id ...) + #:defaults ([(init-depend 1) null])) + (~optional result + #:defaults ([result #f]))) + ;; Lookup an identifier in the signature environment + ;; Fail with a parse error, if the lookup returns #f + (define (id->sig id) + (or (lookup-signature id) + (parse-error #:stx id + #:delayed? #f + "Unknown signature used in Unit type" + "signature" (syntax-e id)))) + (define (import/export-error) + (parse-error #:stx stx + #:delayed? #f + "Unit types must import and export distinct signatures")) + (define (init-depend-error) + (parse-error + #:stx stx + #:delayed? #f + "Unit type initialization dependencies must be a subset of imports")) + (define imports + (check-imports/exports (stx-map id->sig #'(import ...)) import/export-error)) + (define exports + (check-imports/exports (stx-map id->sig #'(export ...)) import/export-error)) + (define init-depends + (check-init-depends/imports (stx-map id->sig #'(init-depend ...)) + imports + init-depend-error)) + (define res (attribute result)) + (make-Unit imports + exports + init-depends + (if res (parse-values-type res) (-values (list -Void))))] [(:List^ ts ...) (parse-list-type stx)] [(:List*^ ts ... t) diff --git a/typed-racket-lib/typed-racket/private/syntax-properties.rkt b/typed-racket-lib/typed-racket/private/syntax-properties.rkt index 15b03cca..a933a552 100644 --- a/typed-racket-lib/typed-racket/private/syntax-properties.rkt +++ b/typed-racket-lib/typed-racket/private/syntax-properties.rkt @@ -74,5 +74,10 @@ (tr:class:local-table tr:class:local-table) (tr:class:name-table tr:class:name-table) (tr:class:def tr:class:def) - ) + (tr:unit tr:unit #:mark) + (tr:unit:body-exp-def-type tr:unit:body-exp-def-type) + (tr:unit:invoke tr:unit:invoke) + (tr:unit:invoke:expr tr:unit:invoke:expr) + (tr:unit:compound tr:unit:compound) + (tr:unit:from-context tr:unit:from-context #:mark)) diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt index de0be4fa..cafa333b 100644 --- a/typed-racket-lib/typed-racket/private/type-contract.rkt +++ b/typed-racket-lib/typed-racket/private/type-contract.rkt @@ -396,6 +396,7 @@ [(Prompt-TagTop:) (only-untyped prompt-tag?/sc)] [(Continuation-Mark-KeyTop:) (only-untyped continuation-mark-key?/sc)] [(ClassTop:) (only-untyped class?/sc)] + [(UnitTop:) (only-untyped unit?/sc)] [(StructTypeTop:) (struct-type/sc null)] ;; TODO Figure out how this should work ;[(StructTop: s) (struct-top/sc s)] @@ -512,6 +513,25 @@ (if seal/sc (and/sc seal/sc sc-for-class) sc-for-class)] + [(Unit: imports exports init-depends results) + (define (traverse sigs) + (for/list ([sig (in-list sigs)]) + (define mapping + (map + (match-lambda + [(cons id type) (cons id (t->sc type))]) + (Signature-mapping sig))) + (signature-spec (Signature-name sig) (map car mapping) (map cdr mapping)))) + + (define imports-specs (traverse imports)) + (define exports-specs (traverse exports)) + (define init-depends-ids (map Signature-name init-depends)) + (match results + [(? AnyValues?) + (fail #:reason (~a "cannot generate contract for unit type" + " with unknown return values"))] + [(Values: (list (Result: rngs _ _) ...)) + (unit/sc imports-specs exports-specs init-depends-ids (map t->sc rngs))])] [(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred?) (cond [(dict-ref recursive-values nm #f)] diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt index 7ae70e1a..6d427648 100644 --- a/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -66,7 +66,8 @@ (not (Values? e)) (not (ValuesDots? e)) (not (AnyValues? e)) - (not (Result? e))))) + (not (Result? e)) + (not (Signature? e))))) ;; (or/c Type/c Values? Results?) ;; Anything that can be treated as a Values by sufficient expansion @@ -77,7 +78,8 @@ (not (arr? e)) (not (fld? e)) (not (ValuesDots? e)) - (not (AnyValues? e))))) + (not (AnyValues? e)) + (not (Signature? e))))) (define Type/c (flat-named-contract 'Type Type/c?)) (define Values/c (flat-named-contract 'Values Values/c?)) @@ -555,6 +557,35 @@ ;; cls : Class (def-type Instance ([cls Type/c]) [#:key 'instance]) +;; interp: +;; name is the id of the signature +;; extends is the extended signature or #f +;; mapping maps variables in a signature to their types +;; This is not a type because signatures are not values +(def-type Signature ([name identifier?] + [extends (or/c identifier? #f)] + [mapping (listof (cons/c identifier? (or/c promise? Type/c)))]) + [#:frees (lambda (f) null)] + [#:fold-rhs (*Signature name extends mapping)]) + +;; The supertype of all units, ie values recognized by the +;; predicate unit? +(def-type UnitTop () [#:fold-rhs #:base] [#:key 'unit]) + +;; interp: imports is the list of imported signatures +;; exports is the list of exported signatures +;; init-depends is the list of init-depend signatures +;; result is the type of the body of the unit +(def-type Unit ([imports (listof Signature?)] + [exports (listof Signature?)] + [init-depends (listof Signature?)] + [result SomeValues/c]) + [#:frees (lambda (f) (f result))] + [#:fold-rhs (*Unit (map type-rec-id imports) + (map type-rec-id exports) + (map type-rec-id init-depends) + (type-rec-id result))]) + ;; sequences ;; includes lists, vectors, etc ;; tys : sequence produces this set of values at each step diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt index 6f1549ab..77dee79c 100644 --- a/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt +++ b/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt @@ -6,7 +6,7 @@ (require "simple.rkt" "structural.rkt" (for-template racket/base racket/list racket/set racket/promise - racket/class racket/async-channel)) + racket/class racket/unit racket/async-channel)) (provide (all-defined-out)) (define identifier?/sc (flat/sc #'identifier?)) @@ -34,5 +34,6 @@ (define continuation-mark-key?/sc (flat/sc #'continuation-mark-key?)) (define class?/sc (flat/sc #'class?)) +(define unit?/sc (flat/sc #'unit?)) (define struct-type?/sc (flat/sc #'struct-type?)) diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/unit.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/unit.rkt new file mode 100644 index 00000000..b0006c55 --- /dev/null +++ b/typed-racket-lib/typed-racket/static-contracts/combinators/unit.rkt @@ -0,0 +1,109 @@ +#lang racket/base + +;; Static contracts for unit contracts + +(require "../structures.rkt" "../constraints.rkt" + racket/list racket/match + racket/dict + racket/contract + racket/syntax + (for-template racket/base racket/unit) + (for-syntax racket/base syntax/parse)) + + +(provide + (contract-out + [struct signature-spec ([name identifier?] + [members (listof identifier?)] + [scs (listof static-contract?)])] + [unit/sc (-> (listof signature-spec?) + (listof signature-spec?) + (listof identifier?) + (listof static-contract?) + static-contract?)])) + + +(struct signature-spec (name members scs) #:transparent) + +(struct unit-combinator combinator () + #:transparent + #:property prop:combinator-name "unit/sc" + #:methods gen:sc + [(define (sc-map v f) + (match v + [(unit-combinator unit-spec) + (unit-combinator (unit-spec-sc-map f unit-spec))])) + (define (sc-traverse v f) + (match v + [(unit-combinator unit-spec) + (unit-spec-sc-map f unit-spec) + (void)])) + (define (sc->contract v f) + (unit/sc->contract v f)) + (define (sc->constraints v f) + (merge-restricts* 'chaperone (map f (unit-spec->list (combinator-args v)))))]) + +(define unit-spec->list + (match-lambda + [(unit-spec imports exports init-depends invoke) + (flatten (append (filter-map signature-spec-scs imports) + (filter-map signature-spec-scs exports) + ;; init-depends do not show up because + ;; there are no contracts attached + (filter-map (lambda (x) x) invoke)))])) + +(struct unit-spec (imports exports init-depends invoke) + #:transparent + #:property prop:sequence unit-spec->list) + +(define (unit-spec-sc-map f seq) + (match seq + [(unit-spec imports exports init-depends invokes) + (unit-spec + (map (signature-spec-sc-map f) imports) + (map (signature-spec-sc-map f) exports) + ;; leave init-depends alone since they don't contain contracts + init-depends + (map (lambda (invoke) (and invoke (f invoke 'covariant))) invokes))])) + +(define ((signature-spec-sc-map f) seq) + (match seq + [(signature-spec name (list ids ...) (list scs ...)) + (signature-spec + name + ids + (map (lambda (sc) (and sc (f sc 'invariant))) scs))])) + + +(define (unit/sc->contract v f) + (match v + [(unit-combinator + (unit-spec (list imports ...) + (list exports ...) + (list deps ...) + (list invoke/scs ...))) + + (define (sig-spec->syntax sig-spec) + (match sig-spec + [(signature-spec name members scs) + (define member-stx + (map (lambda (id sc) #`(#,id #,(f sc))) members scs)) + #`(#,name #,@member-stx)])) + + (define (invokes->contract lst) + (cond + ;; just a single contract + [(= 1 (length lst)) + #`#,(f (first lst))] + ;; values contract + [else + #`(values #,@(map f lst))])) + + #`(unit/c + (import #,@(map sig-spec->syntax imports)) + (export #,@(map sig-spec->syntax exports)) + (init-depend #,@deps) + #,(invokes->contract invoke/scs))])) + +(define (unit/sc imports exports init-depends invoke) + (unit-combinator (unit-spec imports exports init-depends invoke))) diff --git a/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt new file mode 100644 index 00000000..4c77823e --- /dev/null +++ b/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt @@ -0,0 +1,753 @@ +#lang racket/unit + +;; This module provides a unit for type-checking units +;; The general strategy for typechecking all of the racket/unit forms +;; is to match the entire expanded syntax and parse out the relevant +;; pieces of information. +;; +;; Each typing rule knows the expected expansion of the form being checked +;; and specifically parses that syntax. This implementation is extremely +;; brittle and will require changes should the expansion of any of the unit +;; forms change. +;; +;; For unit forms the general idea is to parse expanded syntax to find information +;; related to: +;; - imports +;; - exports +;; - init-depend +;; - subexpressions that require typechecking +;; And use these pieces to typecheck the entire form +;; +;; For the `unit` form imports, exports, and init-depends are parsed to generate +;; the type of the expression and to typecheck the body of the unit since imported signatures +;; introduce bindings of variables to types, and exported variables must be defined +;; with subtypes of their expected types. +;; +;; The `invoke-unit` expansion is more complex and depends on whether or not +;; imports were specified. In the case of no imports, the strategy is simply to +;; find the expression being invoked and ensure it has the type of a unit with +;; no imports. When there are imports to an `invoke-unit` form, the syntax contains +;; local definitions of units defined using `unit-from-context`. These forms +;; are parsed to determine which imports were declared to check subtyping on the +;; invoked expression and to ensure that imports pulled from the current context +;; have the correct types. +;; +;; The `compound-unit` expansion contains information about the imports and exports +;; of each unit expression being linked. Additionally the typed `compound-unit` macro +;; attaches a syntax property that specifies the exact linking structure of the compound +;; unit. These pieces of information enable the calculation of init-depends for the entire +;; compound unit and to properly check subtyping on each linked expression. +;; +;; `unit-from-context` is handled similarly to `invoke-unit`, the expansion is exactly +;; that of a unit created using the `unit` form, but lacks the annotations that are placed +;; there by the typed `unit` macro. In this case the body of the unit is searched for +;; syntax corresponding to definitions which are checked against the declared exports +;; to ensure the form is well typed. +;; +;; The handling of the various `infer` forms (invoke-unit/infer compound-unit/infer) +;; is generally identical to the corresponding form lacking inference, however, in these +;; cases typechecking can be more lax. In particular, the unit implementation knows that +;; only valid unit expressions are used in these forms and so there is no need to typecheck +;; each unit subexpression unless it is needed to determine the result type. The +;; `compund-unit/infer` form, however, requires the cooperation of the unit implementation +;; to attach a syntax property that specified the init-depends of the compound unit, otherwise +;; this information is extremely difficult to obtain from the syntax alone. + +(require "../utils/utils.rkt" + syntax/id-set + racket/set + racket/dict + racket/format + racket/list + racket/match + racket/syntax + syntax/id-table + syntax/parse + syntax/stx + syntax/strip-context + racket/unit-exptime + "signatures.rkt" + (private parse-type syntax-properties type-annotation) + (only-in (base-env base-special-env) make-template-identifier) + (env lexical-env tvar-env global-env + signature-env signature-helper) + (types utils abbrev union subtype resolve generalize signatures) + (typecheck check-below internal-forms) + (utils tc-utils) + (rep type-rep) + (for-syntax racket/base racket/unit-exptime syntax/parse) + (for-template racket/base + racket/unsafe/undefined + (submod "internal-forms.rkt" forms))) + +(import tc-let^ tc-expr^) +(export check-unit^) + +;; Syntax class definitions +;; variable annotations are modified by the expansion of the typed unit +;; macro in order to allow annotations on exported variables, this +;; syntax class allows conversion back to the usual internal syntax +;; for type annotations which may be used by tc-letrec/values +(define-syntax-class unit-body-annotation + #:literal-sets (kernel-literals) + #:literals (void values :-internal cons) + (pattern + (#%expression + (begin + (#%plain-app void (#%plain-lambda () var-int)) + (begin + (quote-syntax + (:-internal var:id t) #:local) + (#%plain-app values)))) + #:attr name #'var + #:attr fixed-form (quasisyntax/loc this-syntax + (begin + (quote-syntax (:-internal var-int t) #:local) + (#%plain-app values))))) + +;; Syntax class matching the syntax of the rhs of definitions within unit bodies +;; The typed unit macro attaches the lambda to allow unit typechecking to associate +;; variable names with their definitions which are otherwise challenging to recover +(define-syntax-class unit-body-definition + #:literal-sets (kernel-literals) + #:literals (void) + (pattern + (#%expression + (begin + (#%plain-app void (#%plain-lambda () var:id ... (#%plain-app void))) + e)) + #:with vars #'(var ...) + #:with body #'e)) + +;; Process the syntax of annotations and definitions from a unit +;; produces two values representing the names and the exprs corresponding +;; to each definition or annotation +;; Note: +;; - definitions may produce multiple names via define-values +;; - annotations produce no names +(define (process-ann/def-for-letrec ann/defs) + (for/fold ([names #`()] + [exprs #`()]) + ([a/d (in-list ann/defs)]) + (syntax-parse a/d + [a:unit-body-annotation + (define name (attribute a.name)) + ;; TODO: + ;; Duplicate annotations from imports + ;; are not currently detected due to a bug + ;; in tc/letrec-values + ;; See Problem Report: 15145 + (define fixed (attribute a.fixed-form)) + (values #`(#,@names ()) #`(#,@exprs #,fixed))] + [d:unit-body-definition + (values #`(#,@names d.vars) #`(#,@exprs d.body))]))) + +;; A Sig-Info is a (sig-info identifier? (listof identifier?) (listof identifier?)) +;; name is the identifier corresponding to the signature this sig-info represents +;; externals is the list of external names for variables in the signature +;; internals is the list of internal names for variables in the signature +;; Note: +;; - external names are those attached to signatures stored in static information +;; and in the Siganture representation +;; - internal names are the internal renamings of those variables in fully expanded +;; unit syntax, this renaming is performed by the untyped unit macro +;; - All references within a unit body use the internal names +(struct sig-info (name externals internals) #:transparent) + +;; Process the various pieces of the fully expanded unit syntax to produce +;; sig-info structures for the unit's imports and exports, and a list of the +;; identifiers corresponding to init-depends of the unit +(define (process-unit-syntax import-sigs import-internal-ids import-tags + export-sigs export-temp-ids export-temp-internal-map + init-depend-tags) + ;; build a mapping of import-tags to import signatures + ;; since init-depends are referenced by the tags only in the expanded syntax + ;; this map is used to determine the actual signatures corresponding to the + ;; given signature tags of the init-depends + (define tag-map (make-immutable-free-id-table (map cons import-tags import-sigs))) + (define lookup-temp (λ (temp) (free-id-table-ref export-temp-internal-map temp #f))) + + (values (for/list ([sig-id (in-list import-sigs)] + [sig-internal-ids (in-list import-internal-ids)]) + (sig-info sig-id + (map car (Signature-mapping (lookup-signature sig-id))) + sig-internal-ids)) + ;; export-temp-ids is a flat list which must be processed + ;; sequentially to map them to the correct internal/external identifiers + (let-values ([(_ si) + (for/fold ([temp-ids export-temp-ids] + [sig-infos '()]) + ([sig (in-list export-sigs)]) + (define external-ids + (map car (Signature-mapping (lookup-signature sig)))) + (define len (length external-ids)) + (values (drop temp-ids len) + (cons (sig-info sig + external-ids + (map lookup-temp (take temp-ids len))) + sig-infos)))]) + (reverse si)) + (map (λ (x) (free-id-table-ref tag-map x #f)) init-depend-tags))) + +;; The following three syntax classes are used to parse specific pieces of +;; information from parts of the expansion of units + +;; Needed to parse out signature names, and signature-tags from the unit syntax +;; the tags are used to lookup init-depend signatures +(define-syntax-class sig-vector + #:literal-sets (kernel-literals) + #:literals (vector-immutable cons) + (pattern (#%plain-app + vector-immutable + (#%plain-app cons + (quote sig:id) + (#%plain-app vector-immutable sig-tag tag-rest ...)) + ...) + #:with sigs #'(sig ...) + #:with sig-tags #'(sig-tag ...))) + +(define-syntax-class init-depend-list + #:literal-sets (kernel-literals) + #:literals (list cons) + (pattern (#%plain-app list (#%plain-app cons _ sig-tag) ...) + #:with init-depend-tags #'(sig-tag ...))) + +(define-syntax-class export-table + #:literal-sets (kernel-literals) + #:literals (make-immutable-hash list cons vector-immutable check-not-unsafe-undefined unbox) + (pattern (#%plain-app + make-immutable-hash + (#%plain-app + list + (#%plain-app + cons + signature-tag:id + (#%plain-app + vector-immutable + (#%plain-lambda () + (#%plain-app check-not-unsafe-undefined (#%plain-app unbox export-temp-id) external-id)) + ...)) + ...)) + #:attr export-temp-ids (map syntax->list (syntax->list #'((export-temp-id ...) ...))))) + +;; This syntax class matches the whole expansion of unit forms +(define-syntax-class unit-expansion + #:literal-sets (kernel-literals) + #:attributes (body-stx + import-internal-ids + import-sigs + import-sig-tags + export-sigs + export-temp-ids + init-depend-tags) + (pattern (#%plain-app + make-unit:id + name:expr + import-vector:sig-vector + export-vector:sig-vector + list-dep:init-depend-list + (let-values (_ ...) + (let-values (_ ...) + (#%expression + (#%plain-lambda () + (let-values (((export-temp-id:id) _) ...) + (#%plain-app + values + (#%plain-lambda (import-table:id) + (let-values (((import:id ...) _) ...) + unit-body:expr)) + et:export-table + _ ...))))))) + #:attr import-sigs (syntax->list #'import-vector.sigs) + #:attr import-sig-tags (syntax->list #'import-vector.sig-tags) + #:attr export-sigs (syntax->list #'export-vector.sigs) + #:attr export-temp-ids (syntax->list #'(export-temp-id ...)) + #:attr init-depend-tags (syntax->list #'list-dep.init-depend-tags) + #:attr import-internal-ids (map syntax->list (syntax->list #'((import ...) ...))) + #:with body-stx #'unit-body)) + +;; Extract the identifiers referenced in unit-from-context and invoke-unit forms +;; in order to typecheck them in the current environment + (define (extract-definitions stx) + (trawl-for-property + stx + (lambda (stx) (syntax-parse stx [((int:id) ref:id) #t] [_ #f])) + (lambda (stx) (syntax-parse stx [((int:id) ref:id) #'ref])))) + +;; Syntax inside the expansion of units that allows recovering a mapping +;; from temp-ids of exports to their internal identifiers +(define-syntax-class export-temp-internal-map-elem + #:literal-sets (kernel-literals) + #:literals (set-box!) + (pattern (#%plain-app set-box! temp-id:id internal-id:id))) + +(define export-map-elem? + (syntax-parser [e:export-temp-internal-map-elem #t] + [_ #f])) +(define extract-export-map-elem + (syntax-parser [e:export-temp-internal-map-elem (cons #'e.temp-id #'e.internal-id)])) + +;; get a reference to the actual `invoke-unit/core` function to properly parse +;; the fully expanded syntax of `invoke-unit` forms +(define invoke-unit/core (make-template-identifier 'invoke-unit/core 'racket/unit)) + +;; Syntax class for all the various expansions of invoke-unit forms +;; This also includes the syntax for the invoke-unit/infer forms +(define-syntax-class invoke-unit-expansion + #:literal-sets (kernel-literals) + (pattern (#%plain-app iu/c unit-expr) + #:when (free-identifier=? #'iu/c invoke-unit/core) + #:attr units '() + #:attr expr #'unit-expr + #:attr imports '()) + (pattern + (let-values () + body:invoke-unit-linkings) + #:attr units (attribute body.units) + #:attr expr (attribute body.expr) + #:attr imports (attribute body.imports))) + +(define-syntax-class invoke-unit-linkings + #:literal-sets (kernel-literals) + (pattern + (let-values ([(u-temp:id) + (let-values ([(deps) _] + [(sig-provider) _] ... + [(temp) ie:invoked-expr]) + _ ...)]) + (#%plain-app iu/c (#%plain-app values _))) + #:when (free-identifier=? #'iu/c invoke-unit/core) + #:attr units '() + #:attr expr (if (tr:unit:invoke:expr-property #'ie) #'ie #'ie.invoke-expr) + #:attr imports '()) + (pattern + (let-values ([(temp-id) u:unit-expansion]) + rest:invoke-unit-linkings) + #:attr units (cons #'u (attribute rest.units)) + #:attr expr (attribute rest.expr) + #:attr imports (append (attribute u.export-sigs) (attribute rest.imports)))) + +;; This should be used ONLY when an invoke/infer is used with the link clause ... +(define-syntax-class invoked-expr + #:literal-sets (kernel-literals) + #:literals (values) + (pattern + (let-values ([(deps2:id) _] + [(local-unit-id:id) unit:id] ... + [(invoke-temp) invoke-unit]) + _ ...) + #:attr invoke-expr #'invoke-unit) + (pattern invoke-expr:expr)) + +;; Compound Unit syntax classes +(define-syntax-class compound-unit-expansion + #:literal-sets (kernel-literals) + #:literals (vector-immutable cons) + (pattern + (let-values ([(deps:id) _] + [(local-unit-name) unit-expr] ...) + (~seq (#%plain-app check-unit _ ...) + (#%plain-app check-sigs _ + (#%plain-app + vector-immutable + (#%plain-app cons (quote import-sig:id) _) ...) + (#%plain-app + vector-immutable + (#%plain-app cons (quote export-sig:id) _) ...) + _) + (let-values ([(fht) _] + [(rht) _]) + _ ...)) ... + (#%plain-app + make-unit:id + name:expr + import-vector:sig-vector + export-vector:sig-vector + deps-ref + internals)) + #:attr unit-exprs (syntax->list #'(unit-expr ...)) + #:attr unit-imports (map syntax->list (syntax->list #'((import-sig ...) ...))) + #:attr unit-exports (map syntax->list (syntax->list #'((export-sig ...) ...))) + #:attr compound-imports (syntax->list #'import-vector.sigs) + #:attr compound-exports (syntax->list #'export-vector.sigs))) + +;; A cu-expr-info represents an element of the link clause in +;; a compound-unit form +;; - expr : the unit expression being linked +;; - import-sigs : the Signatures specified as imports for this link-element +;; - import-links : the symbols that correspond to the link-bindings +;; imported by this unit +;; - export-sigs : the Signatures specified as exports for this link-element +;; - export-links : the symbols corresponding to the link-bindings exported +;; by this unit +(struct cu-expr-info (expr import-sigs import-links export-sigs export-links) + #:transparent) + +;; parse-compound-unit : Syntax -> (Values (Listof (Cons Symbol Id)) +;; (Listof Symbol) +;; (Listof Signature) +;; (Listof Signature) +;; (Listof cu-expr-info)) +;; Returns a mapping of link-ids to sig-ids, a list of imported sig ids +;; a list of exported link-ids +(define (parse-compound-unit stx) + (define (list->sigs l) (map lookup-signature l)) + (syntax-parse stx + [cu:compound-unit-expansion + (define link-binding-info (tr:unit:compound-property stx)) + (match-define (list cu-import-syms unit-export-syms unit-import-syms) + link-binding-info) + (define compound-imports (attribute cu.compound-imports)) + (define compound-exports (attribute cu.compound-exports)) + (define unit-exprs (attribute cu.unit-exprs)) + (define unit-imports (attribute cu.unit-imports)) + (define unit-exports (attribute cu.unit-exports)) + ;; Map signature ids to link binding symbols + (define mapping + (let () + (define link-syms (append cu-import-syms (flatten unit-export-syms))) + (define sig-ids (append compound-imports (flatten unit-exports))) + (map cons link-syms (map lookup-signature sig-ids)))) + (define cu-exprs + (for/list ([unit-expr (in-list unit-exprs)] + [import-sigs (in-list unit-imports)] + [import-links (in-list unit-import-syms)] + [export-sigs (in-list unit-exports)] + [export-links (in-list unit-export-syms)]) + (cu-expr-info unit-expr + (list->sigs import-sigs) import-links + (list->sigs export-sigs) export-links))) + (values + mapping + cu-import-syms + (list->sigs compound-imports) + (list->sigs compound-exports) + cu-exprs)])) + +;; Sig-Info -> (listof (pairof identifier? Type)) +;; GIVEN: signature information +;; RETURNS: a mapping from internal names to types +(define (make-local-type-mapping si) + (define sig (lookup-signature (sig-info-name si))) + (define internal-names (sig-info-internals si)) + (define sig-types + (map cdr (Signature-mapping sig))) + (map cons internal-names sig-types)) + +;; Syntax Option -> TCResults +;; Type-check a unit form +(define (check-unit form [expected #f]) + (define expected-type + (match expected + [(tc-result1: type) (resolve type)] + [_ #f])) + (match expected-type + [(? Unit? unit-type) + (ret (parse-and-check-unit form unit-type))] + [_ (ret (parse-and-check-unit form #f))])) + +;; Syntax Option -> TCResults + +(define (check-invoke-unit form [expected #f]) + (define expected-type + (match expected + [(tc-result1: type) (resolve type)] + [_ #f])) + (ret (parse-and-check-invoke form expected-type))) + +(define (check-compound-unit form [expected #f]) + (define infer? (eq? (tr:unit:compound-property form) 'infer)) + (define expected-type + (match expected + [(tc-result1: type) (resolve type)] + [_ #f])) + (if infer? + (ret (parse-and-check-compound/infer form expected-type)) + (ret (parse-and-check-compound form expected-type)))) + +(define (check-unit-from-context form [expected #f]) + (define expected-type + (match expected + [(tc-result1: type) (resolve type)] + [_ #f])) + (ret (parse-and-check-unit-from-context form expected-type))) + +(define (parse-and-check-unit-from-context form expected-type) + (syntax-parse form + [u:unit-expansion + (define export-sigs (map lookup-signature (attribute u.export-sigs))) + (define body-stx (attribute u.body-stx)) + (for ([sig (in-list export-sigs)]) + (define ids (extract-definitions body-stx)) + (define types (map cdr (Signature-mapping sig))) + (for ([type (in-list types)] + [id (in-list ids)]) + (define lexical-type (lookup-type/lexical id)) + (unless (subtype lexical-type type) + (tc-error/fields "type mismatch in unit-from-context export" + "expected" type + "given" lexical-type + "exported variable" (syntax-e id) + "exported-signature" (syntax-e (Signature-name sig)) + #:stx form + #:delayed #t)))) + (-unit null export-sigs null (-values (list -Void)))])) + +(define (parse-and-check-compound form expected-type) + (define-values (link-mapping + import-syms + import-sigs + export-sigs + cu-exprs) + (parse-compound-unit form)) + + (define (lookup-link-id id) (dict-ref link-mapping id #f)) + (define-values (check _ init-depends) + (for/fold ([check -Void] + [seen-init-depends import-syms] + [calculated-init-depends '()]) + ([form (in-list cu-exprs)]) + (match-define (cu-expr-info unit-expr-stx + import-sigs + import-links + export-sigs + export-links) + form) + (define unit-expected-type + (-unit import-sigs + export-sigs + (map lookup-link-id (set-intersect seen-init-depends import-links)) + ManyUniv)) + (define unit-expr-type (tc-expr/t unit-expr-stx)) + (check-below unit-expr-type unit-expected-type) + (define-values (body-type new-init-depends) + (match unit-expr-type + [(Unit: _ _ ini-deps ty) + ;; init-depends here are strictly subsets of the units imports + ;; but these may not exactly match with the provided links + ;; so all of the extended signatures must be traversed to find the right + ;; signatures for init-depends + (define extended-imports + (map cons import-links + (map (λ (l) (map Signature-name (flatten-sigs l))) import-sigs))) + (define init-depend-links + (for*/list ([sig-name (in-list (map Signature-name ini-deps))] + [(import-link import-family) (in-dict extended-imports)] + #:when (member sig-name import-family free-identifier=?)) + import-link)) + ;; new init-depends are the init-depends of this unit that + ;; overlap with the imports to the compound-unit + (values ty (set-intersect import-syms init-depend-links))] + ;; unit-expr was not actually a unit, but we want to delay the errors + [_ (values #f '())])) + (values body-type + ;; Add the exports to the list of seen-init-depends + (set-union seen-init-depends export-links) + ;; Add the new-init-depends to those already calculated + (set-union calculated-init-depends new-init-depends)))) + (if check + (-unit import-sigs + export-sigs + (map lookup-link-id init-depends) + check) + ;; Error case when one of the links was not a unit + -Bottom)) + +(define (parse-and-check-compound/infer form expected-type) + (define init-depend-refs (syntax-property form 'unit:inferred-init-depends)) + (syntax-parse form + [cu:compound-unit-expansion + (define unit-exprs (attribute cu.unit-exprs)) + (define compound-imports (map lookup-signature (attribute cu.compound-imports))) + (define compound-exports (map lookup-signature (attribute cu.compound-exports))) + (define import-vector (apply vector compound-imports)) + (define import-length (vector-length import-vector)) + (unless (and (list? init-depend-refs) + (andmap (λ (i) (and (exact-nonnegative-integer? i) (< i import-length))) + init-depend-refs)) + (int-err "malformed syntax property attached to compound-unit/infer form")) + (define compound-init-depends + (map (lambda (i) (vector-ref import-vector i)) init-depend-refs)) + (define resulting-unit-expr (last unit-exprs)) + (define final-unit-invoke-type (tc-expr/t resulting-unit-expr)) + ;; This type should always be a unit + (match-define (Unit: _ _ _ compound-invoke-type) final-unit-invoke-type) + (-unit compound-imports compound-exports compound-init-depends compound-invoke-type)])) + +(define (parse-and-check-invoke form expected-type) + (syntax-parse form + [iu:invoke-unit-expansion + (define infer? (eq? 'infer (tr:unit:invoke-property form))) + (define invoked-unit (attribute iu.expr)) + (define import-sigs (map lookup-signature (attribute iu.imports))) + (define linking-units (attribute iu.units)) + (define unit-expr-type (tc-expr/t invoked-unit)) + ;; TODO: Better error message/handling when the folling check-below "fails" + (unless infer? + (check-below unit-expr-type (-unit import-sigs null import-sigs ManyUniv))) + (for ([unit (in-list linking-units)] + [sig (in-list import-sigs)]) + (define ids (extract-definitions unit)) + (define types (map cdr (Signature-mapping sig))) + (for ([type (in-list types)] + [id (in-list ids)]) + (define lexical-type (lookup-type/lexical id)) + (unless (subtype lexical-type type) + (tc-error/fields "type mismatch in invoke-unit import" + "expected" type + "given" lexical-type + "imported variable" (syntax-e id) + "imported signature" (syntax-e (Signature-name sig)) + #:stx form + #:delayed? #t)))) + (cond + [(Unit? unit-expr-type) + (define result-type (Unit-result unit-expr-type)) + (match result-type + [(Values: (list (Result: t _ _) ...)) t] + [(AnyValues: f) ManyUniv] + [(ValuesDots: (list (Result: t _ _) ...) _ _) t])] + [else -Bottom])])) + +;; Parse and check unit syntax +(define (parse-and-check-unit form expected) + (syntax-parse form + [u:unit-expansion + ;; extract the unit body syntax + (define body-stx #'u.body-stx) + (define import-sigs (attribute u.import-sigs)) + (define import-internal-ids (attribute u.import-internal-ids)) + (define import-tags (attribute u.import-sig-tags)) + (define export-sigs (attribute u.export-sigs)) + (define export-temp-ids (attribute u.export-temp-ids)) + (define init-depend-tags (attribute u.init-depend-tags)) + (define export-temp-internal-map + (make-immutable-free-id-table + (trawl-for-property body-stx export-map-elem? extract-export-map-elem))) + (define-values (imports-info exports-info init-depends) + (process-unit-syntax import-sigs import-internal-ids import-tags + export-sigs export-temp-ids export-temp-internal-map + init-depend-tags)) + + ;; Get Signatures to build Unit type + (define import-signatures (map lookup-signature (map sig-info-name imports-info))) + (define export-signatures (map lookup-signature (map sig-info-name exports-info))) + (define init-depend-signatures (map lookup-signature init-depends)) + + (unless (distinct-signatures? import-signatures) + (tc-error/expr "unit expressions must import distinct signatures")) + ;; this check for exports may be unnecessary + ;; the unit macro seems to check it as well + (unless (distinct-signatures? export-signatures) + (tc-error/expr "unit expresssions must export distinct signatures")) + + (define local-sig-type-map + (apply append (map make-local-type-mapping imports-info))) + (define export-signature-type-map + (map (lambda (si) + (cons (sig-info-name si) (make-local-type-mapping si))) + exports-info)) + + ;; Thunk to pass to tc/letrec-values to check export subtyping + ;; These subtype checks can only be checked within the dynamic extent + ;; of the call to tc/letrec-values because they need to lookup + ;; variables in the type environment as modified by typechecking + (define (check-exports-thunk) + (for* ([sig-mapping (in-list export-signature-type-map)] + [sig (in-value (car sig-mapping))] + [mapping (in-value (cdr sig-mapping))] + [(id expected-type) (in-dict mapping)]) + (define id-lexical-type (lookup-type/lexical id)) + (unless (subtype id-lexical-type expected-type) + (tc-error/fields "type mismatch in unit export" + "expected" expected-type + "given" id-lexical-type + "exported variable" (syntax-e id) + "exported signature" (syntax-e sig) + #:delayed? #t)))) + + (define import-name-map + (append-map (lambda (si) (map cons (sig-info-externals si) (sig-info-internals si))) + imports-info)) + (define export-name-map + (append-map (lambda (si) (map cons (sig-info-externals si) (sig-info-internals si))) + exports-info)) + + (define body-forms + (trawl-for-property body-stx tr:unit:body-exp-def-type-property)) + + (define last-form + (or (and (not (empty? body-forms)) (last body-forms)))) + + ;; get expression forms, if the body was empty or ended with + ;; a definition insert a `(void)` expression to be typechecked + ;; This is necessary because we defer to tc/letrec-values for typechecking + ;; unit bodies, but a unit body may contain only definitions whereas letrec bodies + ;; cannot, in this case we insert dummy syntax representing a call to the void + ;; function in order to correctly type the body of the unit. + (define expression-forms + (let ([exprs + (filter + (lambda (stx) (eq? (tr:unit:body-exp-def-type-property stx) 'expr)) + body-forms)]) + (cond + [(or (not last-form) (eq? (tr:unit:body-exp-def-type-property last-form) 'def/type)) + (append exprs (list #'(#%plain-app void)))] + [else exprs]))) + + + + ;; Filter out the annotation and definition syntax from the unit body + ;; For the purposes of typechecking, annotations and definitions + ;; are essentially lifted to the top of the body and all expressions + ;; are placed at the end (possibly with the addition of a (void) expression + ;; as described above), since the types of definitions and annotations + ;; must scope over the entire body of the unit, this is valid for purposes + ;; of typechecking + (define annotation/definition-forms + (filter + (lambda (stx) (eq? (tr:unit:body-exp-def-type-property stx) 'def/type)) + body-forms)) + + (define-values (ann/def-names ann/def-exprs) + (process-ann/def-for-letrec annotation/definition-forms)) + + (define signature-annotations + (for/list ([(k v) (in-dict local-sig-type-map)]) + (cons k (-> v)))) + (define unit-type + (with-lexical-env/extend-types + (map car signature-annotations) + (map cdr signature-annotations) + ;; Typechecking a unit body is structurally similar to that of + ;; checking a let-body, so we resuse the machinary for checking + ;; let expressions + (define res (tc/letrec-values ann/def-names + ann/def-exprs + (quasisyntax/loc form (#,@expression-forms)) + #f + check-exports-thunk)) + (define invoke-type + (match res + [(tc-results: tps) (-values tps)])) + (-unit import-signatures + export-signatures + init-depend-signatures + invoke-type))) + unit-type])) + +;; Based on the function of the same name in check-class-unit.rkt +;; trawl-for-property : Syntax (Syntax -> Any) [(Syntax -> A)] -> (Listof A) +;; Search through the given syntax for pieces of syntax that satisfy +;; the accessor predicate, then apply the extractor function to all such syntaxes +(define (trawl-for-property form accessor [extractor values]) + (define (recur-on-all stx-list) + (apply append (map (λ (stx) (trawl-for-property stx accessor extractor)) stx-list))) + (syntax-parse form + #:literal-sets (kernel-literals) + [stx + #:when (accessor #'stx) + (list (extractor form))] + [_ + (define list? (syntax->list form)) + (if list? (recur-on-all list?) '())])) diff --git a/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt b/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt index 54bc20b6..85e1e0c4 100644 --- a/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt +++ b/typed-racket-lib/typed-racket/typecheck/internal-forms.rkt @@ -29,12 +29,16 @@ typed-require/struct predicate-assertion type-declaration + typed-define-signature + typed-define-values/invoke-unit typecheck-failure type-alias? new-subtype-def? typed-struct? - typed-struct/exec?) + typed-struct/exec? + typed-define-signature? + typed-define-values/invoke-unit?) (module forms racket/base (require (for-syntax racket/base)) @@ -59,7 +63,9 @@ assert-predicate-internal declare-refinement-internal :-internal - typecheck-fail-internal)) + typecheck-fail-internal + define-signature-internal + define-values/invoke-unit-internal)) (require (submod "." forms) (submod "." forms literal-set)) @@ -91,6 +97,11 @@ #:attr type-only (attribute options.type-only) #:attr maker (or (attribute options.maker) #'nm.nm))) +(define-syntax-class dviu-import/export + (pattern (sig-id:id member-id:id ...) + #:with sig #'sig-id + #:with members #'(member-id ...))) + ;;; Internal form syntax matching (define-literal-set internal-form-literals #:for-label @@ -145,7 +156,21 @@ [predicate-assertion (assert-predicate-internal type predicate)] [type-declaration - (:-internal id:identifier type)]) + (:-internal id:identifier type)] + ;; the check field indicates whether this signature is being + ;; required from an untyped context in which case the super + ;; value is ignored and information about parent signatures + ;; is inferred from static information bound to the signature + ;; identifier + [typed-define-signature + (define-signature-internal name #:parent-signature super (binding ...) #:check? check)] + ;; This should be a decent initial attempt at making + ;; define-values/invoke-unit work, the unit-expr is + ;; unnecessary at this point since it will be handled + ;; when expressions are typechecked + [typed-define-values/invoke-unit + (define-values/invoke-unit-internal (import:dviu-import/export ...) + (export:dviu-import/export ...))]) ;; Define separately outside of `define-internal-classes` since this form ;; is meant to appear in expression positions, so it doesn't make sense to use diff --git a/typed-racket-lib/typed-racket/typecheck/signatures.rkt b/typed-racket-lib/typed-racket/typecheck/signatures.rkt index 7fdf6191..37574242 100644 --- a/typed-racket-lib/typed-racket/typecheck/signatures.rkt +++ b/typed-racket-lib/typed-racket/typecheck/signatures.rkt @@ -22,6 +22,12 @@ (define-signature check-class^ ([cond-contracted check-class (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)])) +(define-signature check-unit^ + ([cond-contracted check-unit (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)] + [cond-contracted check-invoke-unit (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)] + [cond-contracted check-compound-unit (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)] + [cond-contracted check-unit-from-context (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)])) + (define-signature tc-if^ ([cond-contracted tc/if-twoarm ((syntax? syntax? syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)])) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt index 365218a3..8b761042 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt @@ -28,7 +28,7 @@ (only-in racket/private/class-internal find-method/who))) (import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-send^ check-subforms^ tc-literal^ - check-class^ tc-expression^) + check-class^ check-unit^ tc-expression^) (export tc-expr^) (define-literal-set tc-expr-literals #:for-label @@ -123,6 +123,15 @@ ;; a TR-annotated class [stx:tr:class^ (check-class form expected)] + ;; Unit forms + [stx:tr:unit^ + (check-unit form expected)] + [stx:tr:unit:invoke^ + (check-invoke-unit form expected)] + [stx:tr:unit:compound^ + (check-compound-unit form expected)] + [stx:tr:unit:from-context^ + (check-unit-from-context form expected)] [stx:exn-handlers^ (register-ignored! form) (check-subforms/with-handlers form expected) ] diff --git a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt index aebf1754..e7c266be 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt @@ -6,7 +6,8 @@ (only-in (types abbrev) (-> t:->) [->* t:->*]) (private type-annotation parse-type syntax-properties) (env lexical-env type-alias-helper mvar-env - global-env scoped-tvar-env) + global-env scoped-tvar-env + signature-env signature-helper) (rep filter-rep object-rep type-rep) syntax/free-vars (typecheck signatures tc-metafunctions tc-subst internal-forms tc-envops) @@ -37,7 +38,9 @@ ;; Checks that the body has the expected type when names are bound to the types spcified by results. ;; The exprs are also typechecked by using expr->type. ;; TODO: make this function sane. -(define/cond-contract (do-check expr->type namess expected-results exprs body expected) +;; The `check-thunk` argument serves the same purpose as in tc/letrec-values +(define/cond-contract (do-check expr->type namess expected-results exprs body expected + [check-thunk void]) ((syntax? tc-results/c . -> . any/c) (listof (listof identifier?)) (listof (listof tc-result?)) (listof syntax?) syntax? (or/c #f tc-results/c) @@ -94,6 +97,9 @@ (match results [(list (tc-result: ts fs os) ...) (expr->type expr (ret ts fs os))])) + ;; Perform additional context-dependent checking that needs to be done + ;; in the context of the letrec body + (check-thunk) ;; typecheck the body (tc-body/check body (and expected (erase-filter expected))))))) @@ -107,15 +113,23 @@ (define (regsiter-aliases-and-declarations names exprs) ;; Collect the declarations, which are represented as expressions. ;; We put them back into definitions to reuse the existing machinery - (define-values (type-aliases declarations) - (for/fold ([aliases '()] [declarations '()]) + (define-values (type-aliases declarations signature-forms) + (for/fold ([aliases '()] [declarations '()] [signature-forms '()]) ([body (in-list exprs)]) (syntax-parse #`(define-values () #,body) [t:type-alias - (values (cons #'t aliases) declarations)] + (values (cons #'t aliases) declarations signature-forms)] [t:type-declaration - (values aliases (cons (list #'t.id #'t.type) declarations))] - [_ (values aliases declarations)]))) + (values aliases (cons (list #'t.id #'t.type) declarations) signature-forms)] + [t:typed-define-signature + (values aliases declarations (cons #'t signature-forms))] + [_ (values aliases declarations signature-forms)]))) + + ;; add signature names to the signature environment, deferring type parsing + ;; until after aliases are registered to allow mutually recursive references + ;; between signatures and type aliases + (for/list ([sig-form (in-list (reverse signature-forms))]) + (parse-and-register-signature! sig-form)) (define-values (alias-names alias-map) (get-type-alias-info type-aliases)) (register-all-type-aliases alias-names alias-map) @@ -130,14 +144,22 @@ (for ([n (in-list names)] [b (in-list exprs)]) (syntax-case n () [(var) (add-scoped-tvars b (lookup-scoped-tvars #'var))] - [_ (void)]))) + [_ (void)])) -(define (tc/letrec-values namess exprs body [expected #f]) + ;; Finalize signatures, by parsing member types + (finalize-signatures!)) + +;; The `thunk` argument is run only for its side effects +;; It is used to perform additional context-dependent checking +;; within the context of a letrec body. +;; For example, it is used to typecheck units and ensure that exported +;; variables are exported at the correct types +(define (tc/letrec-values namess exprs body [expected #f] [check-thunk void]) (let* ([names (stx-map syntax->list namess)] [orig-flat-names (apply append names)] [exprs (syntax->list exprs)]) (regsiter-aliases-and-declarations names exprs) - + ;; First look at the clauses that do not bind the letrec names (define all-clauses (for/list ([name-lst names] [expr exprs]) @@ -153,19 +175,21 @@ ;; Check those and then check the rest in the extended environment (check-non-recursive-clauses - ordered-clauses - (lambda () - (cond - ;; after everything, check the body expressions - [(null? remaining-names) - (tc-body/check body (and expected (erase-filter expected)))] - [else - (define flat-names (apply append remaining-names)) - (do-check tc-expr/check - remaining-names - ;; types the user gave. - (map (λ (l) (map tc-result (map get-type l))) remaining-names) - remaining-exprs body expected)]))))) + ordered-clauses + (lambda () + (cond + ;; after everything, check the body expressions + [(null? remaining-names) + (check-thunk) + (tc-body/check body (and expected (erase-filter expected)))] + [else + (define flat-names (apply append remaining-names)) + (do-check tc-expr/check + remaining-names + ;; types the user gave. + (map (λ (l) (map tc-result (map get-type l))) remaining-names) + remaining-exprs body expected + check-thunk)]))))) ;; An lr-clause is a ;; (lr-clause (Listof Identifier) Syntax) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt index 76d8e4f7..a881b579 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt @@ -9,10 +9,13 @@ (private parse-type type-annotation syntax-properties type-contract) (env global-env init-envs type-name-env type-alias-env lexical-env env-req mvar-env scoped-tvar-env - type-alias-helper) + type-alias-helper signature-env signature-helper) (utils tc-utils redirect-contract) "provide-handling.rkt" "def-binding.rkt" "tc-structs.rkt" "typechecker.rkt" "internal-forms.rkt" + (typecheck provide-handling def-binding tc-structs + typechecker internal-forms + check-below) syntax/location racket/format (for-template @@ -115,6 +118,15 @@ [(define-values (lifted) expr) #:when (contract-lifted-property #'expr) (list)] + + ;; register types of variables defined by define-values/invoke-unit forms + [dviu:typed-define-values/invoke-unit + (for ([export-sig (in-list (syntax->list #'(dviu.export.sig ...)))] + [export-ids (in-list (syntax->list #'(dviu.export.members ...)))]) + (for ([id (in-list (syntax->list export-ids))] + [ty (in-list (map cdr (signature->bindings export-sig)))]) + (register-type-if-undefined id ty))) + (list)] ;; values definitions [(define-values (var ...) expr) @@ -208,9 +220,22 @@ (syntax-parse form #:literal-sets (kernel-literals) ;; need to special case this to avoid errors at top-level - [stx:tr:class^ + [(~or stx:tr:class^ + stx:tr:unit^ + stx:tr:unit:invoke^ + stx:tr:unit:compound^ + stx:tr:unit:from-context^) (tc-expr #'stx)] - + ;; Handle define-values/invoke-unit form typechecking, by making sure that + ;; inferred imports have the correct types + [dviu:typed-define-values/invoke-unit + (for ([import-sig (in-list (syntax->list #'(dviu.import.sig ...)))] + [import-ids (in-list (syntax->list #'(dviu.import.members ...)))]) + (for ([member (in-list (syntax->list import-ids))] + [expected-type (in-list (map cdr (signature->bindings import-sig)))]) + (define lexical-type (lookup-type/lexical member)) + (check-below lexical-type expected-type))) + 'no-type] ;; these forms we have been instructed to ignore [stx:ignore^ 'no-type] @@ -289,16 +314,23 @@ (define (type-check forms0) (define forms (syntax->list forms0)) (do-time "before form splitting") - (define-values (type-aliases struct-defs stx-defs0 val-defs0 provs) + (define-values (type-aliases struct-defs stx-defs0 val-defs0 provs signature-defs) (filter-multiple forms type-alias? (lambda (e) (or (typed-struct? e) (typed-struct/exec? e))) parse-syntax-def parse-def - provide?)) + provide? + typed-define-signature?)) (do-time "Form splitting done") + ;; Register signatures in the signature environment + ;; but defer type parsing to allow mutually recursive refernces + ;; between signatures and type aliases + (for ([sig-form signature-defs]) + (parse-and-register-signature! sig-form)) + (define-values (type-alias-names type-alias-map) (get-type-alias-info type-aliases)) @@ -313,6 +345,7 @@ (do-time "after adding type names") (register-all-type-aliases type-alias-names type-alias-map) + (finalize-signatures!) (do-time "starting struct handling") ;; Parse and register the structure types @@ -427,6 +460,7 @@ #,(tname-env-init-code) #,(tvariance-env-init-code) #,(mvar-env-init-code mvar-env) + #,(signature-env-init-code) #,(make-struct-table-code) #,@(for/list ([a (in-list aliases)]) (match-define (list from to) a) @@ -447,7 +481,7 @@ ;; appropriate-phase `require` statically in a module ;; that's non-dynamically depended on by ;; `typed/racket`. That makes for confusing non-local - ;; dependencies, though, so we do it here. + ;; dependencies, though, so we do it here. (require typed-racket/utils/redirect-contract) ;; We need a submodule for a for-syntax use of ;; `define-runtime-module-path`: diff --git a/typed-racket-lib/typed-racket/typecheck/typechecker.rkt b/typed-racket-lib/typed-racket/typecheck/typechecker.rkt index 3f37d516..57b6483e 100644 --- a/typed-racket-lib/typed-racket/typecheck/typechecker.rkt +++ b/typed-racket-lib/typed-racket/typecheck/typechecker.rkt @@ -10,11 +10,12 @@ "tc-literal.rkt" "tc-expression.rkt" "tc-send.rkt" "tc-expr-unit.rkt" "check-subforms-unit.rkt" - "check-class-unit.rkt") + "check-class-unit.rkt" + "check-unit-unit.rkt") (provide-signature-elements tc-expr^ check-subforms^ tc-literal^) (define-values/invoke-unit/infer (link tc-if@ tc-lambda@ tc-app-combined@ tc-let@ tc-expr@ tc-send@ check-subforms@ tc-apply@ tc-literal@ - check-class@ tc-expression@)) + check-class@ check-unit@ tc-expression@)) diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt index 563c38e8..816bce74 100644 --- a/typed-racket-lib/typed-racket/types/abbrev.rkt +++ b/typed-racket-lib/typed-racket/types/abbrev.rkt @@ -68,6 +68,8 @@ (define -inst make-Instance) (define (-prefab key . types) (make-Prefab (normalize-prefab-key key (length types)) types)) +(define -unit make-Unit) +(define -signature make-Signature) (define (-seq . args) (make-Sequence args)) diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt index 92a81d67..d05a1820 100644 --- a/typed-racket-lib/typed-racket/types/printer.rkt +++ b/typed-racket-lib/typed-racket/types/printer.rkt @@ -510,6 +510,14 @@ [(Instance: t) `(Instance ,(t->s t))] ; for cases like Error [(ClassTop:) 'ClassTop] [(? Class?) (class->sexp type)] + [(Unit: (list imports ...) (list exports ...) (list init-depends ...) body) + `(Unit + (import ,@(map t->s imports)) + (export ,@(map t->s exports)) + (init-depend ,@(map t->s init-depends)) + ,(t->s body))] + [(Signature: name extends mapping) + (syntax->datum name)] [(Result: t (or (NoFilter:) (FilterSet: (Top:) (Top:))) (or (NoObject:) (Empty:))) (type->sexp t)] [(Result: t fs (Empty:)) `(,(type->sexp t) : ,(filter->sexp fs))] [(Result: t fs lo) `(,(type->sexp t) : ,(filter->sexp fs) : ,(object->sexp lo))] diff --git a/typed-racket-lib/typed-racket/types/signatures.rkt b/typed-racket-lib/typed-racket/types/signatures.rkt new file mode 100644 index 00000000..8e4ee4ee --- /dev/null +++ b/typed-racket-lib/typed-racket/types/signatures.rkt @@ -0,0 +1,75 @@ +#lang racket/base + +;; This module provides helper functions for typed signatures needed for +;; checking subtyping and parsing unit types + +(require "../utils/utils.rkt" + (env signature-env) + (rep type-rep) + syntax/parse + syntax/id-set + racket/list + (only-in racket/set subset?) + (for-template racket/base + (typecheck internal-forms))) + +(provide check-sub-signatures? + distinct-signatures? + flatten-sigs + check-imports/exports + check-init-depends/imports) + +;; (listof Signature?) procedure? -> (listof Signature?) +;; given a list of imported/exported signatures +;; and a parse-error procedure, ensures that the signatures are +;; valid in that there are no overlapping signatures +;; Returns the given list or raises an error +(define (check-imports/exports sigs error-proc) + (unless (distinct-signatures? sigs) (error-proc)) + sigs) + +;; (listof Signature?) (listof Signature?) procedure? -> (listof Signature?) +;; Ensures that the init-depends signatures are a subset of the import signatures +;; an equal? based subset check is the right thing, since each init-depend +;; must be equal to an imported signature +(define (check-init-depends/imports init-depends imports error-proc) + (unless (subset? init-depends imports) (error-proc)) + init-depends) + +;; check-sub-signatures? : (listof Signature) (listof Signature) -> boolean? +;; checks that the first list of signatures can be used to implement the second +;; list of signatures +(define (check-sub-signatures? sub-sigs sup-sigs) + (define sub-exts (immutable-free-id-set (append-map signature-extensions sub-sigs))) + (define sup-exts (immutable-free-id-set (append-map signature-extensions sup-sigs))) + (free-id-subset? sup-exts sub-exts)) + +;; signature-extensions : (or/c #f identifier?) -> (listof identifier?) +;; returns the list (chain) of names of each signature that +;; the given signature extends including itself +;; returns '() when given #f +(define (signature-extensions sig*) + (let ([sig (and sig* (if (Signature? sig*) sig* (lookup-signature sig*)))]) + (if sig + (cons (Signature-name sig) + (signature-extensions (Signature-extends sig))) + null))) + +(define (flatten-sigs sig*) + (let ([sig (and sig* (if (Signature? sig*) sig* (lookup-signature sig*)))]) + (if sig + (cons sig (flatten-sigs (Signature-extends sig))) + null))) + + +;; : (listof Signature) -> boolean +;; returns true iff the list of signatures contains no duplicates under +;; extension +(define (distinct-signatures? sigs) + (define sig-ids (append-map signature-extensions sigs)) + (distinct-ids? sig-ids)) + +;; distinct-ids? : (listof id) -> boolean? +;; returns true iff the signature ids are all distinct +(define (distinct-ids? sigs) + (not (check-duplicates sigs free-identifier=?))) diff --git a/typed-racket-lib/typed-racket/types/structural.rkt b/typed-racket-lib/typed-racket/types/structural.rkt index 25ed42f3..27edf349 100644 --- a/typed-racket-lib/typed-racket/types/structural.rkt +++ b/typed-racket-lib/typed-racket/types/structural.rkt @@ -33,6 +33,7 @@ [ChannelTop ()] [Async-ChannelTop ()] [ClassTop ()] + [UnitTop ()] [Continuation-Mark-KeyTop ()] [Error ()] [HashtableTop ()] diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index 6bf66c57..bb7c8362 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -5,7 +5,7 @@ (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils early-return) (types utils resolve base-abbrev match-expanders - numeric-tower substitute current-seen prefab) + numeric-tower substitute current-seen prefab signatures) (for-syntax racket/base syntax/parse racket/sequence)) (lazy-require @@ -692,6 +692,17 @@ (or (and init-rest init-rest* (sub init-rest init-rest*)) (and (not init-rest) (not init-rest*))))] + [((? Unit?) (UnitTop:)) A0] + ;; For Unit types invoke-types are covariant + ;; imports and init-depends are covariant in that importing fewer + ;; signatures results in a subtype + ;; exports conversely are contravariant, subtypes export more signatures + [((Unit: imports exports init-depends t) (Unit: imports* exports* init-depends* t*)) + (and (check-sub-signatures? imports* imports) + (check-sub-signatures? exports exports*) + (check-sub-signatures? init-depends* init-depends) + (subtype-seq A0 + (subtype* t t*)))] ;; otherwise, not a subtype [(_ _) #f]))) (when (null? A) diff --git a/typed-racket-lib/typed/racket.rkt b/typed-racket-lib/typed/racket.rkt index 0e607a61..3d394075 100644 --- a/typed-racket-lib/typed/racket.rkt +++ b/typed-racket-lib/typed/racket.rkt @@ -2,11 +2,14 @@ (require typed/racket/base racket/require (subtract-in racket typed/racket/base racket/contract - typed/racket/class) + typed/racket/class + typed/racket/unit) typed/racket/class - (for-syntax racket/base)) + typed/racket/unit + (for-syntax racket/base)) (provide (all-from-out racket typed/racket/base - typed/racket/class) - (for-syntax (all-from-out racket/base)) + typed/racket/class + typed/racket/unit) + (for-syntax (all-from-out racket/base)) class) diff --git a/typed-racket-lib/typed/racket/unit.rkt b/typed-racket-lib/typed/racket/unit.rkt new file mode 100644 index 00000000..e36de3c6 --- /dev/null +++ b/typed-racket-lib/typed/racket/unit.rkt @@ -0,0 +1,33 @@ +#lang racket/base + +(require (except-in racket/unit + define-signature + unit + invoke-unit + invoke-unit/infer + compound-unit + define-unit + define-compound-unit + define-values/invoke-unit + define-values/invoke-unit/infer + compound-unit/infer + define-compound-unit/infer + unit-from-context + define-unit-from-context) + typed-racket/base-env/unit-prims + typed-racket/base-env/signature-prims) + +(provide define-signature + unit + invoke-unit + invoke-unit/infer + compound-unit + define-unit + define-compound-unit + define-values/invoke-unit + define-values/invoke-unit/infer + compound-unit/infer + define-compound-unit/infer + unit-from-context + define-unit-from-context + (all-from-out racket/unit)) diff --git a/typed-racket-test/fail/bad-ann-from-macro-in-unit.rkt b/typed-racket-test/fail/bad-ann-from-macro-in-unit.rkt new file mode 100644 index 00000000..db2a6a13 --- /dev/null +++ b/typed-racket-test/fail/bad-ann-from-macro-in-unit.rkt @@ -0,0 +1,16 @@ +#; +(exn-pred (regexp-quote "type mismatch\n expected: Integer\n given: String")) +#lang typed/racket + +(require (for-syntax syntax/parse)) + + +(unit (import) + (export) + (define-syntax (my-define stx) + (syntax-parse stx + [(_ name:id #:with-type type expr) + #'(begin + (: name type) + (define name expr))])) + (my-define bad #:with-type Integer "BAD")) diff --git a/typed-racket-test/fail/def-val-inv-unit-sig-mismatch.rkt b/typed-racket-test/fail/def-val-inv-unit-sig-mismatch.rkt new file mode 100644 index 00000000..c47b3a79 --- /dev/null +++ b/typed-racket-test/fail/def-val-inv-unit-sig-mismatch.rkt @@ -0,0 +1,7 @@ +#; +(exn-pred (regexp-quote "type mismatch\n expected: (Unit (import) (export x-sig) (init-depend) Any)\n given: (Unit (import) (export) (init-depend) Void)")) +#lang typed/racket + +(define-signature x-sig ([x : Integer])) + +(define-values/invoke-unit (unit (import) (export)) (import) (export x-sig)) diff --git a/typed-racket-test/fail/dviu-has-imports.rkt b/typed-racket-test/fail/dviu-has-imports.rkt new file mode 100644 index 00000000..281cfac5 --- /dev/null +++ b/typed-racket-test/fail/dviu-has-imports.rkt @@ -0,0 +1,7 @@ +#; +(exn-pred (regexp-quote "type mismatch\n expected: (Unit (import) (export) (init-depend) Any)\n given: (Unit (import x-sig) (export) (init-depend) Integer)")) + +#lang typed/racket + +(define-signature x-sig ([x : Integer])) +(define-values/invoke-unit (unit (import x-sig) (export) x) (import) (export)) diff --git a/typed-racket-test/fail/dviu-infer-deps-bad.rkt b/typed-racket-test/fail/dviu-infer-deps-bad.rkt new file mode 100644 index 00000000..a00cffe3 --- /dev/null +++ b/typed-racket-test/fail/dviu-infer-deps-bad.rkt @@ -0,0 +1,19 @@ +#; +(exn-pred #rx"unit depends on initialization of later unit") +#lang typed/racket + +;; This program errors at compile time, but the check is from +;; the untyped implementation of define-values/invoke-unit/infer + +(define-signature s^ ([a : Integer])) +(define-signature t^ ([b : Integer])) +(define-unit u@ + (import s^) + (export t^) + (init-depend s^) + (define b a)) +(define-unit v@ + (import) + (export s^) + (define a 2)) +(define-values/invoke-unit/infer (export) (link u@ v@)) diff --git a/typed-racket-test/fail/dviu-infer-fact-no-link.rkt b/typed-racket-test/fail/dviu-infer-fact-no-link.rkt new file mode 100644 index 00000000..fd53f6cf --- /dev/null +++ b/typed-racket-test/fail/dviu-infer-fact-no-link.rkt @@ -0,0 +1,22 @@ +#; +(exn-pred #rx"define-values/invoke-unit: unit argument expects an untagged import with signature fact\\^") +#lang typed/racket + +(define-signature fact^ ([fact : (-> Natural Natural)])) + + +(define-unit fact@ + (import (prefix i: fact^)) + (export fact^) + (: fact (-> Natural Natural)) + (define (fact n) + (if (= 0 n) + 1 + (* n (i:fact (sub1 n)))))) + +;; without link this should fail +;; see the corresponging successful test +;; dviu-infer-fact.rkt in the succeed directory +(define-values/invoke-unit/infer fact@) + +(fact 5) diff --git a/typed-racket-test/fail/dviu-not-a-unit.rkt b/typed-racket-test/fail/dviu-not-a-unit.rkt new file mode 100644 index 00000000..685b1651 --- /dev/null +++ b/typed-racket-test/fail/dviu-not-a-unit.rkt @@ -0,0 +1,5 @@ +#; +(exn:pred #rx"type mismatch") +#lang typed/racket + +(define-values/invoke-unit 1 (import) (export)) diff --git a/typed-racket-test/fail/dviu-not-subtype.rkt b/typed-racket-test/fail/dviu-not-subtype.rkt new file mode 100644 index 00000000..613eb104 --- /dev/null +++ b/typed-racket-test/fail/dviu-not-subtype.rkt @@ -0,0 +1,10 @@ +#; +(exn-pred #rx"type mismatch") +#lang typed/racket + +(define-signature x-sig ([x : Integer])) +(define-signature x-sub extends x-sig ([xx : Integer])) + +(define u (unit (import) (export x-sig) (define x 1))) + +(define-values/invoke-unit u (import) (export x-sub)) diff --git a/typed-racket-test/fail/extend-untyped-signature.rkt b/typed-racket-test/fail/extend-untyped-signature.rkt new file mode 100644 index 00000000..c36fe3bb --- /dev/null +++ b/typed-racket-test/fail/extend-untyped-signature.rkt @@ -0,0 +1,13 @@ +#; +(exn-pred #rx"signature definition extends untyped signature") +#lang racket + +(module ut1 racket + (provide a^) + (define-signature a^ (a))) + +(module t1 typed/racket + (require (submod ".." ut1)) + (define-signature a-sub^ extends a^ ()) + (unit (import a-sub^) (export) a)) + \ No newline at end of file diff --git a/typed-racket-test/fail/signature-escape.rkt b/typed-racket-test/fail/signature-escape.rkt new file mode 100644 index 00000000..119ddc0c --- /dev/null +++ b/typed-racket-test/fail/signature-escape.rkt @@ -0,0 +1,18 @@ +#; +(exn-pred (regexp-quote "type mismatch\n expected: (Unit (import bad^) (export) (init-depend bad^) AnyValues)\n given: (Unit (import bad^) (export) (init-depend) Void)\n in: (invoke-unit bad (import bad^))")) +#lang typed/racket + +;; The full error message for this prorgam is +;; Type Checker: type mismatch +;; expected: (Unit (import bad^) (export) (init-depend bad^) AnyValues) +;; given: (Unit (import bad^) (export) (init-depend) Void) +;; in: (invoke-unit bad (import bad^)) + + +(define-signature bad^ ()) +(define bad + (let () + (define-signature bad^ ()) + (unit (import bad^) (export)))) + +(invoke-unit bad (import bad^)) diff --git a/typed-racket-test/fail/unit-contract-missing-init-depends.rkt b/typed-racket-test/fail/unit-contract-missing-init-depends.rkt new file mode 100644 index 00000000..99274b5a --- /dev/null +++ b/typed-racket-test/fail/unit-contract-missing-init-depends.rkt @@ -0,0 +1,20 @@ +#; +(exn-pred #rx"contract does not list initialization dependency a\\^") + +#lang racket + +(module untyped racket + (provide (all-defined-out)) + (define-signature a^ (a)) + (define-unit u + (import a^) + (export) + (init-depend a^) + a)) + +(module typed typed/racket + (require/typed (submod ".." untyped) + [#:signature a^ ([a : Any])] + [u (Unit (import a^) (export) Any)])) + +(require 'typed) diff --git a/typed-racket-test/fail/unit-ctc-init-depends.rkt b/typed-racket-test/fail/unit-ctc-init-depends.rkt new file mode 100644 index 00000000..07e16620 --- /dev/null +++ b/typed-racket-test/fail/unit-ctc-init-depends.rkt @@ -0,0 +1,24 @@ +#; +(exn-pred #rx"x@: broke its own contract;\n contract does not list initialization dependency x\\^") +#lang racket + + +(module untyped racket + (provide x^ x@) + (define-signature x^ (x)) + (define x@ + (unit + (import x^) + (export) + (init-depend x^) + x))) + +(module typed typed/racket + (require/typed (submod ".." untyped) + [#:signature x^ ([x : Integer])] + [x@ (Unit (import x^) + (export) + Integer)])) + +(require 'typed) + diff --git a/typed-racket-test/fail/unit-import-wrong-type.rkt b/typed-racket-test/fail/unit-import-wrong-type.rkt new file mode 100644 index 00000000..252c1b88 --- /dev/null +++ b/typed-racket-test/fail/unit-import-wrong-type.rkt @@ -0,0 +1,13 @@ +#; +(exn-pred #rx"Type Checker: type mismatch\n expected: Integer\n given: String") +#lang typed/racket/base +(require typed/racket/unit) + + +(define-signature x^ ([x : String])) + +(unit (import x^) + (export ) + (: y Integer) + (define y x) + y) diff --git a/typed-racket-test/fail/unit-typed-untyped-1.rkt b/typed-racket-test/fail/unit-typed-untyped-1.rkt new file mode 100644 index 00000000..7a75ab5b --- /dev/null +++ b/typed-racket-test/fail/unit-typed-untyped-1.rkt @@ -0,0 +1,14 @@ +#; +(exn-pred #rx"u: broke its own contract\n promised: Integer") +#lang racket + +(module untyped racket + (provide u) + (define u (unit (import) (export) "not an integer"))) + +(module typed typed/racket + (require/typed (submod ".." untyped) + [u (Unit (import) (export) Integer)]) + (invoke-unit u)) + +(require 'typed) diff --git a/typed-racket-test/fail/unit-typed-untyped-2.rkt b/typed-racket-test/fail/unit-typed-untyped-2.rkt new file mode 100644 index 00000000..962155b4 --- /dev/null +++ b/typed-racket-test/fail/unit-typed-untyped-2.rkt @@ -0,0 +1,19 @@ +#; +(exn-pred #rx"u: contract violation\n expected: Integer") +#lang racket + +(module typed typed/racket + (provide (all-defined-out)) + (define-signature x^ ([x : Integer])) + (define-signature y^ ([y : (-> Integer Integer)])) + + (define u + (unit (import x^) (export y^) (define (y n) x)))) + +(module untyped racket + (require (submod ".." typed)) + (define x 11) + (define-values/invoke-unit u (import x^) (export y^)) + (y "not an integer")) + +(require 'untyped) diff --git a/typed-racket-test/succeed/define-values-invoke-unit-subtyping.rkt b/typed-racket-test/succeed/define-values-invoke-unit-subtyping.rkt new file mode 100644 index 00000000..027cd4cd --- /dev/null +++ b/typed-racket-test/succeed/define-values-invoke-unit-subtyping.rkt @@ -0,0 +1,11 @@ +#lang typed/racket + +(define-signature a1^ ([a1 : Integer])) +(define-signature a2^ extends a1^ ([a2 : Integer])) +(define-signature b^ ([b : Integer])) + +(define-unit u1 (import) (export a2^) (define a1 6) (define a2 7)) +(define-unit u2 (import a1^) (export b^) (define b (+ a1 11))) + + +(define-values/invoke-unit/infer (export) (link u1 u2)) \ No newline at end of file diff --git a/typed-racket-test/succeed/dviu-infer-deps-ok.rkt b/typed-racket-test/succeed/dviu-infer-deps-ok.rkt new file mode 100644 index 00000000..471b47ac --- /dev/null +++ b/typed-racket-test/succeed/dviu-infer-deps-ok.rkt @@ -0,0 +1,14 @@ +#lang typed/racket + +(define-signature s^ ([a : Integer])) +(define-signature t^ ([b : Integer])) +(define-unit u@ + (import s^) + (export t^) + (init-depend s^) + (define b a)) +(define-unit v@ + (import) + (export s^) + (define a 2)) +(define-values/invoke-unit/infer (export) (link v@ u@)) diff --git a/typed-racket-test/succeed/dviu-infer-fact.rkt b/typed-racket-test/succeed/dviu-infer-fact.rkt new file mode 100644 index 00000000..bd910245 --- /dev/null +++ b/typed-racket-test/succeed/dviu-infer-fact.rkt @@ -0,0 +1,20 @@ +#lang typed/racket + +(define-signature fact^ ([fact : (-> Natural Natural)])) + + +(define-unit fact@ + (import (prefix i: fact^)) + (export fact^) + (: fact (-> Natural Natural)) + (define (fact n) + (if (= 0 n) + 1 + (* n (i:fact (sub1 n)))))) + +;; without link this should fail +;; see the corresponding test for failure: +;; dviu-infer-fact-no-link.rkt in the fail directory +(define-values/invoke-unit/infer (link fact@)) + +(fact 5) diff --git a/typed-racket-test/succeed/dviu-unit-from-context.rkt b/typed-racket-test/succeed/dviu-unit-from-context.rkt new file mode 100644 index 00000000..4350d015 --- /dev/null +++ b/typed-racket-test/succeed/dviu-unit-from-context.rkt @@ -0,0 +1,10 @@ +#lang typed/racket + +(define-signature yz-sig ([y : Integer] [z : Integer])) +(define y 1) +(define z 10) +(define-values/invoke-unit (unit-from-context yz-sig) + (import) + (export (prefix x: yz-sig))) +(+ x:y x:z) + diff --git a/typed-racket-test/succeed/macro-in-unit.rkt b/typed-racket-test/succeed/macro-in-unit.rkt new file mode 100644 index 00000000..4a297a71 --- /dev/null +++ b/typed-racket-test/succeed/macro-in-unit.rkt @@ -0,0 +1,27 @@ +#lang typed/racket + + +(require (for-syntax syntax/parse)) + +(define-signature x^ ([x : Integer] [y : String] [z : (-> Symbol)])) + +(unit (import) + (export x^) + (define-syntax (my-define stx) + (syntax-parse stx + [(_ name:id expr:exact-integer) + #'(begin + (: name Integer) + (define name expr))] + [(_ name:id expr:str) + #'(begin + (: name String) + (define name expr))] + [(_ name:id #:with-type type expr) + #'(begin + (: name type) + (define name expr))])) + (my-define x 17) + (my-define a "hello") + (my-define y "a string") + (my-define z #:with-type (-> Symbol) (λ () (string->symbol y)))) diff --git a/typed-racket-test/succeed/simple-unit-scope.rkt b/typed-racket-test/succeed/simple-unit-scope.rkt new file mode 100644 index 00000000..86d4da11 --- /dev/null +++ b/typed-racket-test/succeed/simple-unit-scope.rkt @@ -0,0 +1,7 @@ +#lang typed/racket + +(define-signature y^ ([y : Integer])) + +(let ((y 1)) + (unit (import) (export y^) + (define y 2))) diff --git a/typed-racket-test/succeed/unit-3x-2.rkt b/typed-racket-test/succeed/unit-3x-2.rkt new file mode 100644 index 00000000..63237c34 --- /dev/null +++ b/typed-racket-test/succeed/unit-3x-2.rkt @@ -0,0 +1,67 @@ +#lang typed/racket + +(define-signature is-3x-sig ([is-3x : (-> Natural Boolean)])) +(define-signature is-3x+1-sig ([is-3x+1 : (-> Natural Boolean)])) +(define-signature is-3x+2-sig ([is-3x+2 : (-> Natural Boolean)])) + +(define is-3x-unit + (unit + (import is-3x+2-sig) + (export is-3x-sig) + (: is-3x (-> Natural Boolean)) + (define (is-3x x) + (or (= 0 x) (is-3x+2 (sub1 x)))))) + +(define is-3x+2-unit + (unit + (import is-3x+1-sig) + (export is-3x+2-sig) + (: is-3x+2 (-> Natural Boolean)) + (define (is-3x+2 x) + (and (> x 0) (is-3x+1 (sub1 x)))))) + +(define is-3x+1-unit + (unit + (import is-3x-sig) + (export is-3x+1-sig) + (: is-3x+1 (-> Natural Boolean)) + (define (is-3x+1 x) + (and (> x 0) (is-3x (sub1 x)))))) + +(define 3x-compound1 + (compound-unit (import (IS-3X : is-3x-sig)) + (export IS-3X+1 IS-3X+2) + (link (((IS-3X+1 : is-3x+1-sig)) is-3x+1-unit IS-3X) + (((IS-3X+2 : is-3x+2-sig)) is-3x+2-unit IS-3X+1)))) + +(define 3x-compound2 + (compound-unit (import) + (export IS-3X) + (link (((IS-3X : is-3x-sig)) is-3x-unit IS-3X+2) + (((IS-3X+1 : is-3x+1-sig) + (IS-3X+2 : is-3x+2-sig)) 3x-compound1 IS-3X)))) + +(define 3x-run-unit + (unit + (import is-3x-sig is-3x+1-sig is-3x+2-sig) + (export) + (list (is-3x 1) + (is-3x 3) + (is-3x+1 5) + (is-3x+1 7) + (is-3x+2 4) + (is-3x+2 8)))) + +(define 3x-compound3 + (compound-unit (import) + (export IS-3X IS-3X+1 IS-3X+2) + (link (((IS-3X : is-3x-sig)) 3x-compound2) + (((IS-3X+1 : is-3x+1-sig) + (IS-3X+2 : is-3x+2-sig)) 3x-compound1 IS-3X) + (() 3x-run-unit IS-3X IS-3X+1 IS-3X+2)))) + + +(define-values/invoke-unit 3x-compound3 (import) (export is-3x-sig is-3x+1-sig (rename is-3x+2-sig (y is-3x+2)))) +(list (y 8) + (is-3x+1 7) + (is-3x 6)) diff --git a/typed-racket-test/succeed/unit-3x.rkt b/typed-racket-test/succeed/unit-3x.rkt new file mode 100644 index 00000000..22986b48 --- /dev/null +++ b/typed-racket-test/succeed/unit-3x.rkt @@ -0,0 +1,71 @@ +#lang typed/racket + +(define-signature is-3x-sig ([is-3x : (-> Natural Boolean)])) +(define-signature is-3x+1-sig ([is-3x+1 : (-> Natural Boolean)])) +(define-signature is-3x+2-sig ([is-3x+2 : (-> Natural Boolean)])) + +(define is-3x-unit + (unit + (import is-3x+2-sig) + (export is-3x-sig) + (: is-3x (-> Natural Boolean)) + (define (is-3x x) + (or (= 0 x) (is-3x+2 (sub1 x)))))) + +(define is-3x+2-unit + (unit + (import is-3x+1-sig) + (export is-3x+2-sig) + (: is-3x+2 (-> Natural Boolean)) + (define (is-3x+2 x) + (and (> x 0) (is-3x+1 (sub1 x)))))) + +(define is-3x+1-unit + (unit + (import is-3x-sig) + (export is-3x+1-sig) + (: is-3x+1 (-> Natural Boolean)) + (define (is-3x+1 x) + (and (> x 0) (is-3x (sub1 x)))))) + +(define 3x-compound1 + (compound-unit (import (IS-3X : is-3x-sig)) + (export IS-3X+1 IS-3X+2) + (link (((IS-3X+1 : is-3x+1-sig)) is-3x+1-unit IS-3X) + (((IS-3X+2 : is-3x+2-sig)) is-3x+2-unit IS-3X+1)))) + +(define 3x-compound2 + (compound-unit (import) + (export IS-3X) + (link (((IS-3X : is-3x-sig)) is-3x-unit IS-3X+2) + (((IS-3X+1 : is-3x+1-sig) + (IS-3X+2 : is-3x+2-sig)) 3x-compound1 IS-3X)))) + +(define 3x-run-unit + (unit + (import is-3x-sig is-3x+1-sig is-3x+2-sig) + (export) + (list (is-3x 1) + (is-3x 3) + (is-3x+1 5) + (is-3x+1 7) + (is-3x+2 4) + (is-3x+2 8)))) + +(define 3x-compound3 + (compound-unit (import) + (export IS-3X IS-3X+1 IS-3X+2) + (link (((IS-3X : is-3x-sig)) 3x-compound2) + (((IS-3X+1 : is-3x+1-sig) + (IS-3X+2 : is-3x+2-sig)) 3x-compound1 IS-3X) + (() 3x-run-unit IS-3X IS-3X+1 IS-3X+2)))) + +(invoke-unit 3x-compound3) + +(define-values/invoke-unit 3x-compound3 (import) (export is-3x-sig is-3x+1-sig is-3x+2-sig)) + +(list (is-3x+2 8) + (is-3x+1 7) + (is-3x 6)) + + diff --git a/typed-racket-test/succeed/unit-typed-untyped-compound-1.rkt b/typed-racket-test/succeed/unit-typed-untyped-compound-1.rkt new file mode 100644 index 00000000..86406d47 --- /dev/null +++ b/typed-racket-test/succeed/unit-typed-untyped-compound-1.rkt @@ -0,0 +1,20 @@ +#lang racket + +(module typed typed/racket + (provide (all-defined-out)) + (define-signature x^ ([x : Integer])) + (define u (unit (import x^) (export) (lambda ([n : Integer]) (+ n x))))) + +(module untyped racket + (require (submod ".." typed)) + (define v (unit (import) (export x^) (define x 11))) + (define w (compound-unit + (import) + (export) + (link (([X : x^]) v) + (() u X)))) + + (define f (invoke-unit w)) + (f 6)) + +(require 'untyped) diff --git a/typed-racket-test/succeed/unit-typed-untyped-compound-2.rkt b/typed-racket-test/succeed/unit-typed-untyped-compound-2.rkt new file mode 100644 index 00000000..055794bd --- /dev/null +++ b/typed-racket-test/succeed/unit-typed-untyped-compound-2.rkt @@ -0,0 +1,22 @@ +#lang racket + +(module untyped racket + (provide (all-defined-out)) + (define-signature x^ (x)) + (define u (unit (import x^) (export) (lambda (n) (+ n x))))) + +(module typed typed/racket + (require/typed (submod ".." untyped) + [#:signature x^ ([x : Integer])] + [u (Unit (import x^) (export) (-> Integer Integer))]) + (define v (unit (import) (export x^) (define x 11))) + (define w (compound-unit + (import) + (export) + (link (([X : x^]) v) + (() u X)))) + + (define f (invoke-unit w)) + (f 6)) + +(require 'typed) diff --git a/typed-racket-test/succeed/unit-typed-untyped-values.rkt b/typed-racket-test/succeed/unit-typed-untyped-values.rkt new file mode 100644 index 00000000..ad6c665a --- /dev/null +++ b/typed-racket-test/succeed/unit-typed-untyped-values.rkt @@ -0,0 +1,17 @@ +#lang racket + +(module typed typed/racket + (provide (all-defined-out)) + (define u + (unit (import) + (export) + (values (lambda ([x : String]) x) + (lambda ([n : Integer]) (sqr n)))))) + +(module untyped racket + (require (submod ".." typed)) + (define-values (f g) (invoke-unit u)) + (f "string") + (g 5)) + +(require 'untyped) diff --git a/typed-racket-test/succeed/units-no-sigs.rkt b/typed-racket-test/succeed/units-no-sigs.rkt new file mode 100644 index 00000000..00c3b8ee --- /dev/null +++ b/typed-racket-test/succeed/units-no-sigs.rkt @@ -0,0 +1,33 @@ +#lang typed/racket + +(define-signature yz-sig ([y : Integer] [z : Integer])) + +(let ((y 1) + (z 10)) + (define u (unit (import) (export yz-sig) + (define y 2) + (define z 3))) + (define u1 (unit (import) (export) + y)) + (define u2 (unit (import (only yz-sig z)) (export) + y)) + (define u3 (unit (import (except yz-sig y)) (export) + y)) + (define u4 (unit (import (prefix s: yz-sig)) (export) + y)) + (define u5 (unit (import (rename yz-sig (r y))) (export) + y)) + (define u6 (unit (import yz-sig) (export) + y)) + (: l (-> (Unit (import yz-sig) (export) Integer) Integer)) + (define (l x) + (invoke-unit + (compound-unit (import) (export) + (link (((YZ : yz-sig)) u) + (() x YZ))))) + (invoke-unit u1) + (l u2) + (l u3) + (l u4) + (l u5) + (l u6)) diff --git a/typed-racket-test/unit-tests/all-tests.rkt b/typed-racket-test/unit-tests/all-tests.rkt index ccf64642..91b0a2ff 100644 --- a/typed-racket-test/unit-tests/all-tests.rkt +++ b/typed-racket-test/unit-tests/all-tests.rkt @@ -44,4 +44,5 @@ "rep-tests.rkt" "prims-tests.rkt" "tooltip-tests.rkt" - "prefab-tests.rkt") + "prefab-tests.rkt" + "typed-units-tests.rkt") diff --git a/typed-racket-test/unit-tests/contract-tests.rkt b/typed-racket-test/unit-tests/contract-tests.rkt index 71d6dba6..e416d313 100644 --- a/typed-racket-test/unit-tests/contract-tests.rkt +++ b/typed-racket-test/unit-tests/contract-tests.rkt @@ -246,7 +246,19 @@ (t (-class #:method ([m (-polydots (x) (->... (list) (x x) -Void))]))) (t (-class #:method ([m (-polyrow (x) (list null null null null) (-> (-class #:row (-v x)) -Void))]))) - + + ;; units + ;; These tests do not have sufficient coverage because more + ;; coverage requires a proper set up of the signature environment. + ;; Further coverage of unit contract compilations occurs in + ;; integration tests. + (t-sc (-unit null null null (-values (list -Integer))) + (unit/sc null null null (list integer/sc))) + (t-sc (-unit null null null (-values (list -Integer -Number))) + (unit/sc null null null (list integer/sc number/sc))) + (t-sc (-unit null null null (-values (list))) + (unit/sc null null null null)) + ;; typed/untyped interaction tests (t-int (-poly (a) (-> a a)) (λ (f) (f 1)) diff --git a/typed-racket-test/unit-tests/parse-type-tests.rkt b/typed-racket-test/unit-tests/parse-type-tests.rkt index 7fbe1ba0..881ab828 100644 --- a/typed-racket-test/unit-tests/parse-type-tests.rkt +++ b/typed-racket-test/unit-tests/parse-type-tests.rkt @@ -21,6 +21,7 @@ (only-in (base-env case-lambda) case-lambda) (prefix-in un: (only-in racket/class init init-field field augment)) (only-in typed/racket/class init init-field field augment) + (only-in racket/unit import export init-depend) rackunit) @@ -381,6 +382,26 @@ ((Class #:row-var r (init y)) -> (Class #:row-var r)))] [FAIL (All (r #:row (init x y z) (field f) m n) ((Class #:row-var r a b c) -> (Class #:row-var r)))] + + ;; parsing tests for Unit types + ;; These are only simple tests because checking types + ;; with signatures requires interaction with the Signature + ;; environment. Additionally, more complex tests of Unit + ;; type parsing happens in unit-tests and integrations tests as well + [(Unit (import) (export) (init-depend) String) + (make-Unit null null null (-values (list -String)))] + [(Unit (import) (export) String) + (make-Unit null null null (-values (list -String)))] + [(Unit (import) (export) (init-depend)) + (make-Unit null null null (-values (list -Void)))] + [(Unit (import) (export)) + (make-Unit null null null (-values (list -Void)))] + [UnitTop (make-UnitTop)] + [FAIL (Unit (export) String)] + [FAIL (Unit (import) String)] + [FAIL (Unit (init-depend) String)] + [FAIL (Unit (import bad) (export) String)] + [FAIL (Unit (import) (export bad) String)] )) ;; FIXME - add tests for parse-values-type, parse-tc-results diff --git a/typed-racket-test/unit-tests/static-contract-conversion-tests.rkt b/typed-racket-test/unit-tests/static-contract-conversion-tests.rkt index eeb87090..5deb5ca9 100644 --- a/typed-racket-test/unit-tests/static-contract-conversion-tests.rkt +++ b/typed-racket-test/unit-tests/static-contract-conversion-tests.rkt @@ -48,7 +48,6 @@ (with-check-info (['static sc]) (fail-check "Type was incorrectly converted to contract"))))])) - (define tests (test-suite "Conversion Tests" (t/sc (-Number . -> . -Number)) @@ -70,4 +69,11 @@ (t/sc (-mu a (-box a))) (t/sc (-mu sexp (Un -Null -Symbol (-pair sexp sexp) (-vec sexp) (-box sexp)))) (t/sc (-mu a (-> a a))) - (t/sc (-seq -Symbol)))) + (t/sc (-seq -Symbol)) + ;; These tests for unit static contracts are insufficient, but + ;; in order to test Unit types the signature environment must be + ;; set up correctly. More complex cases of compilation to unit/c + ;; contracts are tested by integration tests. + (t/sc (-unit null null null (-values (list -String)))) + (t/sc (-unit null null null (-values (list -Symbol -String)))) + (t/fail (-unit null null null ManyUniv)))) diff --git a/typed-racket-test/unit-tests/type-printer-tests.rkt b/typed-racket-test/unit-tests/type-printer-tests.rkt index 4af5eb9f..86346fb3 100644 --- a/typed-racket-test/unit-tests/type-printer-tests.rkt +++ b/typed-racket-test/unit-tests/type-printer-tests.rkt @@ -137,7 +137,38 @@ (check-prints-as? (cl->* (->opt -Pathlike [-String] -Void) (->optkey Univ [-String] #:rest -String #:x -String #t -Void)) (string-append "(case-> (->* (Path-String) (String) Void) " - "(->* (Any #:x String) (String) #:rest String Void))"))) + "(->* (Any #:x String) (String) #:rest String Void))")) + (check-prints-as? (make-Unit null null null -String) + "(Unit (import) (export) (init-depend) String)") + ;; Setup for slightly more complex unit printing test + (let* ([a^ (make-Signature #'a^ #f null)] + [a-sub^ (make-Signature #'a-sub^ a^ (list (cons #'a -String)))] + [b^ (make-Signature #'b^ #f (list (cons #'b -Integer)))] + [c^ (make-Signature #'c^ #f (list (cons #'c -Symbol)))] + [d^ (make-Signature #'d^ #f (list (cons #'d -String)))]) + (check-prints-as? (make-Unit (list a^) null null -String) + "(Unit (import a^) (export) (init-depend) String)") + (check-prints-as? (make-Unit (list a^) (list b^) null -String) + "(Unit (import a^) (export b^) (init-depend) String)") + (check-prints-as? (make-Unit (list a^) (list b^) (list a^) -String) + "(Unit (import a^) (export b^) (init-depend a^) String)") + (check-prints-as? (make-Unit (list a-sub^) null null -String) + "(Unit (import a-sub^) (export) (init-depend) String)") + (check-prints-as? (make-Unit (list a-sub^) null (list a-sub^) -String) + "(Unit (import a-sub^) (export) (init-depend a-sub^) String)") + (check-prints-as? (make-Unit null (list a-sub^) null -String) + "(Unit (import) (export a-sub^) (init-depend) String)") + (check-prints-as? (make-Unit (list a^ b^) (list c^ d^) null -String) + "(Unit (import a^ b^) (export c^ d^) (init-depend) String)") + (check-prints-as? (make-Unit (list a^ b^) null null -String) + "(Unit (import a^ b^) (export) (init-depend) String)") + (check-prints-as? (make-Unit null (list c^ d^) null -String) + "(Unit (import) (export c^ d^) (init-depend) String)") + (check-prints-as? (make-Unit (list a^ b^) (list c^ d^) (list b^) -String) + "(Unit (import a^ b^) (export c^ d^) (init-depend b^) String)") + (check-prints-as? (make-Unit (list a^ b^) (list c^ d^) (list b^ a^) -String) + "(Unit (import a^ b^) (export c^ d^) (init-depend b^ a^) String)")) + (check-prints-as? (make-UnitTop) "UnitTop")) (test-suite "Pretty printing tests" (check-pretty-prints-as? (-val 3) "3") diff --git a/typed-racket-test/unit-tests/typed-units-tests.rkt b/typed-racket-test/unit-tests/typed-units-tests.rkt new file mode 100644 index 00000000..779b7293 --- /dev/null +++ b/typed-racket-test/unit-tests/typed-units-tests.rkt @@ -0,0 +1,775 @@ +#lang racket/base + +;; Unit tests for typed units + +(require (submod "typecheck-tests.rkt" test-helpers) + (except-in "test-utils.rkt" private) + (for-syntax racket/base + typed-racket/tc-setup + typed-racket/utils/tc-utils)) + +(provide tests) +(gen-test-main) + +(begin-for-syntax + ;; for checking the printing of type aliases + (current-type-names (init-current-type-names))) + +;; see typecheck-tests.rkt for rationale on imports +(require rackunit + typed/racket/unit + (except-in typed-racket/utils/utils private) + (except-in (base-env extra-procs prims class-prims + base-types base-types-extra) + define lambda λ case-lambda) + (prefix-in tr: (only-in (base-env prims) define lambda λ case-lambda)) + (for-syntax (rep type-rep filter-rep object-rep) + (rename-in (types abbrev union numeric-tower filter-ops utils) + [Un t:Un] + [-> t:->]))) + +(define tests + (test-suite + "unit typechecking tests" + ;; simple tests that annotations work appropriately + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (unit + (import) + (export a^) + (: a Natural) + (define a 5)) + (void)) + -Void] + [tc-err + (let () + (define-signature a^ ([a : Integer])) + (unit + (import) + (export a^) + (: a String) + (define a 5)) + (error ""))] + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (unit + (import) + (export a^) + (: a Integer) + (define a 5) + (: b String) + (define b "foo")) + (void)) + -Void] + [tc-err + (let () + (define-signature a^ ([a : Integer])) + (unit + (import) + (export a^) + (: a Integer) + (define a 5) + (: b String) + (define b 5)e) + (error ""))] + + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (define-type-alias Foo (Unit (import a^) (export) Integer)) + (define a 17) + (: u (Unit (import a^) (export) Integer)) + (define u (unit (import a^) (export) a)) + (invoke-unit u (import a^))) + -Integer] + + [tc-e + (let () + (define-type-alias Foo (U Integer (Unit (import a^) (export) Foo))) + (define-signature a^ ([a : Foo])) + (: u Foo) + (define u (unit (import a^) (export) a)) + (define a 11) + (invoke-unit (assert u unit?) (import a^)) + (void)) + -Void] + + #| + This should typecheck, but doesn't because fact has no type annotation + + (define-signature fact^ + ([fact : (-> Integer Integer)])) + + + + (define-unit fact@ + (import (prefix i: fact^)) + (export fact^) + (define (fact n) + (if (< n 1) + 1 + (* n (i:fact (sub1 n))))) + fact) + |# + [tc-e + (let () + (define-signature a^ ()) + (define-signature b^ ()) + + (define-unit u + (import a^) + (export)) + + (define-unit v + (import) + (export a^ b^) + 5) + + (define-compound-unit/infer w + (import) + (export) + (link (() u A) + (([A : a^] [B : b^]) v))) + + (define-compound-unit/infer w2 + (import [A : a^]) + (export) + (link (() u A))) + + (define-compound-unit/infer w3 + (import) + (export) + (link u v)) + + (define-compound-unit/infer w4 + (import a^) + (export) + (link u)) + (void)) + -Void] + + [tc-err + (let () + (unit (import) + (export) + (+ 1 "bad")) + (error ""))] + + ;; factorial with units + [tc-e + (let () + (define-signature fact^ ([fact : (-> Integer Natural)])) + + (define-unit fact@ + (import (prefix i: fact^)) + (export fact^) + (: fact (-> Integer Natural)) + (define (fact n) + (if (<= n 1) 1 (* n (i:fact (sub1 n))))) + fact) + + (define-compound-unit/infer fact-c@ + (import) + (export) + (link fact@)) + + (define factorial (invoke-unit fact-c@)) + + (factorial 5)) + -Nat] + + ;; factorial + invoke-unit/infer + [tc-e + (let () + (define-signature fact^ ([fact : (-> Integer Natural)])) + (define-unit fact@ + (import (prefix i: fact^)) + (export fact^) + (: fact (-> Integer Natural)) + (define (fact n) + (if (<= n 1) 1 (* n (i:fact (sub1 n))))) + fact) + (define fact (invoke-unit/infer fact@)) + (fact 5)) + -Nat] + [tc-e + (let () + (define a 11) + (let () + (define-signature a^ ([a : Integer])) + (define-unit u + (import a^) + (export) + (: x Integer) + (define x a) + x) + (invoke-unit/infer u))) + -Integer] + + ;; Make sure scoping doesn't break the typed unit expansion/typechecking + [tc-e + (let () + (define-signature x^ ([x : Number])) + (define u + (unit + (import x^) + (export) + (unit (import x^) (export) x))) + (void)) + -Void] + [tc-e + (let () + (define-signature x^ ([x : Number])) + (unit + (import) + (export x^) + (define x^ "FOOBAR") + (define x 5)) + (void)) + -Void] + + [tc-e + (let () + (define-signature x^ ([x : (-> Integer Integer)])) + (unit + (import x^) + (export) + (define-signature x^ ([y : (-> Natural Real)])) + (unit + (import) + (export x^) + (define y x)) + (void)) + (void)) + -Void] + + ;; Tests adapted from racket-tests/tests/units/test-unit.rkt + [tc-e + (begin (invoke-unit (unit (import) (export) 12)) (void)) + -Void] + + [tc-e + (let () + (define-signature x-sig ([x : Integer])) + (define-signature y-sig ([y : Integer])) + (define-signature z-sig ([z : Integer])) + (define-signature empty-sig ()) + + (invoke-unit + (compound-unit (import) (export) + (link (((X : x-sig) (Y : y-sig)) (unit (import empty-sig z-sig) + (export y-sig x-sig) + (define x 1) + (define y 2)) + Z E) + (((Z : z-sig) (E : empty-sig)) (unit (import x-sig y-sig) + (export empty-sig z-sig) + (define z 3) + 3) X Y))))) + -PosByte] + + [tc-e + (let () + (define-signature x-sig ([x : Integer])) + (define-signature xy-sig ([x : Integer] [y : Integer])) + (define-signature b-sig ([b : Integer])) + + (let ((un (compound-unit (import) (export S U) + (link (((S : x-sig)) (unit (import) (export x-sig) (define x 10))) + (((U : xy-sig)) (unit (import) (export xy-sig) (define x 11) (define y 12))))))) + (invoke-unit + (compound-unit (import) (export) + (link (((S : x-sig) (U : xy-sig)) un) + (((B : b-sig)) (unit (import x-sig) (export b-sig) (define b x)) S) + (() (unit (import b-sig xy-sig) (export) (list b x y)) B U))))) + (void)) + -Void] + + [tc-e + (let () + (define-signature even-sig ([even : (-> Integer Boolean)])) + (define-signature odd-sig ([odd : (-> Integer Boolean)])) + + (define even-unit + (unit (import odd-sig) + (export even-sig) + (: even (-> Integer Boolean)) + (define (even x) + (or (= 0 x) (odd (sub1 x)))))) + + (define odd-unit + (unit (import even-sig) + (export odd-sig) + (: odd (-> Integer Boolean)) + (define (odd x) + (and (> x 0) (even (sub1 x)))) + (define x (odd 11)) + x)) + + (define run-unit + (compound-unit (import) + (export) + (link (((EVEN : even-sig)) even-unit ODD) + (((ODD : odd-sig)) odd-unit EVEN)))) + + (invoke-unit run-unit)) + -Boolean] + + [tc-e + (let () + (define-signature x-sig ([x : Integer])) + (define-signature yz-sig ([y : Integer] [z : Integer])) + (invoke-unit + (compound-unit + (import) + (export) + (link (((T : yz-sig)) + (unit (import x-sig) (export yz-sig) + (define-values (y a) (values 1 2)) + (define-values (b z) (values y a))) + S) + (((S : x-sig)) + (unit (import yz-sig) (export x-sig) (define x 3) (+ y z)) T))))) + -Integer] + + [tc-e + (let () + (define-signature x-sig ([x : Integer])) + (invoke-unit + (unit + (import) + (export x-sig) + (define-syntax (y stx) + (syntax-case stx () + ((_ x) #'(define x 1)))) + (y x) + x))) + -One] + + [tc-e + (let () + (define-signature fact-sig ([fact : (-> Natural Natural)] [n : Natural])) + (invoke-unit + (compound-unit (import) (export) + (link (((F : fact-sig)) (unit (import (except (rename fact-sig (f-in fact)) n)) + (export (rename fact-sig (f-out fact))) + (define n 1) + (: f-out (-> Natural Natural)) + (define (f-out x) (if (= 0 x) + 1 + (* x (f-in (sub1 x)))))) + F) + (() (unit (import (only fact-sig fact)) (export) + (define n 2) + (fact 4)) + F))))) + -Nat] + + [tc-e + (let () + (define-signature x-sig ([x : Integer])) + (invoke-unit + (compound-unit (import) (export) + (link (((S : x-sig)) (unit (import) (export x-sig) (define x 1))) + (() (unit (import (prefix s: x-sig)) (export) s:x) S))))) + -Integer] + + [tc-e + (let () + (define-signature x-sig ([x : Integer])) + (define-signature xy-sig ([x : Integer] [y : Integer])) + (define-signature yz-sig ([y : Integer] [z : Integer])) + (define-signature sx ([x : Integer])) + (define-signature sy ([y : Integer])) + (define-signature sz ([z : Integer])) + (invoke-unit + (compound-unit (import) (export) + (link (((S : x-sig) (T : yz-sig) (U : xy-sig)) + (unit (import) (export (rename x-sig (s:x x)) + (rename yz-sig (t:y y) (t:z z)) + (prefix u: xy-sig)) + (define x 1) (define y 2) (define z 3) + (define s:x x) (define t:y y) (define t:z z) (define u:x x) (define u:y y))) + (((SX : sx)) (unit (import (prefix s: x-sig)) (export sx) (define x s:x)) S) + (((SY : sy)) (unit (import (prefix u: xy-sig)) (export sy) (define y u:y)) U) + (((SZ : sz)) (unit (import (prefix t: yz-sig)) (export sz) (define z t:z)) T) + (() (unit (import sx sy sz) (export) (+ x y z)) SX SY SZ))))) + -Integer] + + [tc-e + (let () + (define-signature b-sig ([b : Integer])) + (let ([b : String "WRONG b"]) + (define u1 (unit (import) (export b-sig) (define b 2))) + (define u2 (unit (import b-sig) (export) b)) + (invoke-unit (compound-unit (import) (export) + (link (((B : b-sig)) u1) + (() u2 B)))))) + -Integer] + + ;; subtyping tests + [tc-e + (let () + (define-signature x-sig ([x : Integer])) + (define-signature y-sig ([y : Integer])) + (define-signature x-sub extends x-sig ([xx : Integer])) + (define-signature y-sub extends y-sig ([yy : Integer])) + + (define u1 (unit (import x-sig) (export y-sub) (define y (add1 x)) (define yy 2) (+ x y yy))) + (define u2 (unit (import y-sig) (export x-sub) (define x 3) (define xx 44))) + + (invoke-unit + (compound-unit (import) (export) + (link (((S1 : x-sig)) u2 S2) + (((S2 : y-sig)) u1 S1))))) + -Integer] + ;; Make sure let expressions order the signature processing correctly + [tc-e + (let () + (let () + (define-signature y-sig ([y : Integer])) + (define-signature y-sub extends y-sig ([yy : String])) + (unit (import) (export y-sub) (define y 1) (define yy "yy is a string")) + (void))) + -Void] + + ;; check that invoke-unit and invoke-unit/infer both work correctly + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (define-signature aa^ extends a^ ([aa : String])) + + (define-unit u (import a^) (export) a) + (define a 1) + (define aa "One") + (invoke-unit/infer u)) + -Integer] + + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (define-signature aa^ extends a^ ([aa : String])) + + (define-unit u (import a^) (export) a) + (define a 1) + (define aa "One") + (invoke-unit u (import aa^))) + -Integer] + + ;; Sanity checking combinations of compound-unit and invoke-unit + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (define u@ (unit (import) (export a^) (define a 5))) + (invoke-unit + (compound-unit + (import) + (export) + (link (((a^1 : a^)) u@) + (() + (unit + (import a^) + (export) + (values a)) + a^1))) (import))) + -Integer] + + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (define-unit u@ (import) (export a^) (define a 5)) + (invoke-unit + (compound-unit + (import) + (export) + (link (((a^1 : a^)) u@) + (() + (unit + (import a^) + (export) + (values a)) + a^1))) (import))) + -Integer] + + ;; make sure that invoke-unit/infer works when there is a link clause + [tc-e + (let () + (define-signature a^ ([a : Integer])) + + (define-unit u (import) (export a^) (define a 5)) + (define-unit v (import a^) (export) a) + + (invoke-unit/infer (link u v))) + -Integer] + + ;; unit-from-context and define-unit-from-context tests + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (define a 17) + (define-unit u (import a^) (export) a) + (define-unit-from-context v a^) + (define w (compound-unit/infer (import) (export) (link v u))) + (invoke-unit w)) + -Integer] + + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (define a 17) + (define-unit u (import a^) (export) a) + (define-unit-from-context v a^) + (invoke-unit/infer (link v u))) + -Integer] + + [tc-e + (let () + (define-signature a^ ([a : Integer])) + (define a 17) + (define u (unit-from-context a^)) + (define v (unit (import a^) (export) a)) + (invoke-unit + (compound-unit + (import) + (export) + (link (([A : a^]) u) + (() v A))) + (import))) + -Integer] + + ;; Make sure body annotations for exports are checked + [tc-err + (let () + (define-signature a^ ([a : Integer])) + (unit + (import) + (export a^) + (: a String) + (define a 5)) + (error ""))] + ;; and for non-exports as well + [tc-err + (let () + (define-signature a^ ([a : Integer])) + (unit + (import) + (export a^) + (: b String) + (define b 12) + (define a 5)) + (error ""))] + + ;; init-depends type errors with compound-unit/define-compound-unit + [tc-err + (let () + (define-signature a ()) + (define-signature aa extends a ()) + (define-unit u1 + (import ) + (export aa)) + (define-unit u2 + (import a) + (export) + (init-depend a)) + (define-unit u3 + (import) + (export aa)) + (compound-unit + (import [A1 : a]) + (export) + (link + (([A2 : a]) u1 ) + (() u2 A) + (([A : aa]) u3))) + (error ""))] + + [tc-err + (let () + (define-signature a ()) + (define-unit u1 + (import ) + (export a)) + (define-unit u2 + (import a) + (export) + (init-depend a)) + (define-unit u3 + (import) + (export a)) + (compound-unit + (import [A1 : a]) + (export) + (link + (([A2 : a]) u1 ) + (() u2 A) + (([A : a]) u3))) + (error ""))] + + [tc-err + (let () + (define-signature a ()) + (define-signature aa extends a ()) + (define-unit u1 + (import ) + (export aa)) + (define-unit u2 + (import aa) + (export)) + (define-unit u3 + (import) + (export)) + (compound-unit + (import) + (export) + (link + (([A : a]) u1 ) + (() u2 A))) + (error ""))] + + [tc-err + (let () + (define-signature a ()) + (define-unit u1 + (import ) + (export a)) + (define-unit u2 + (import a) + (export) + (init-depend a)) + (define-unit u3 + (import) + (export a)) + (define-compound-unit w + (import [A1 : a]) + (export) + (link + (([A2 : a]) u1 ) + (() u2 A) + (([A : a]) u3))) + (error ""))] + + ;; inference + [tc-err + (let () + (invoke-unit/infer 1) + (error ""))] + + [tc-err + (let () + (compound-unit (import) (export) (link (() 1))) + (error ""))] + + [tc-err + (let () + (define-signature x-sig ([x : Integer])) + (compound-unit (import) (export) + (link (() (unit (import x-sig) (export))))) + (error ""))] + + [tc-err + (let () + (define-signature x-sig ([x : Integer])) + (compound-unit (import) (export) + (link (([X : x-sig]) (unit (import) (export))))) + (error ""))] + + [tc-err + (let () + (invoke-unit 1) + (error ""))] + + [tc-err + (let () + (define-signature x-sig ([x : Integer])) + (invoke-unit (unit (import x-sig) (export) x)) + (error ""))] + + [tc-err + (let () + (define-signature x^ ([x : String])) + (unit (import x^) (export) + (: y Integer) + (define y x) + y) + (error ""))] + + ;; Type mismatch in unit body + [tc-err + (let () + (unit (import) (export) + (: x String) + (define x 5)) + (error ""))] + [tc-err + (let () + (define-signature a^ ([a : String])) + (unit (import) (export a^) (define a 5)) + (error ""))] + [tc-err + (let () + (define-signature a^ ([a : Integer])) + (define a "foo") + (invoke-unit (unit (import a^) (export) a) (import a^)) + (error ""))] + [tc-err + (let () + (define-signature a^ ([a : Integer])) + (unit + (import a^) + (export) + (: x String) + (define x a)) + (error ""))] + ;; units can only import/export distinct sets of signatures + [tc-err + (let () + (define-signature a^ ()) + (define-signature b^ extends a^ ()) + (define-siganture c^ extends a^ ()) + (unit (import b^ c^) (export)) + (error ""))] + + ;; invoking a unit which imports a locally defined signature is a type error + ;; even if it is invoked with an import of the same name + [tc-err + (let () + (define-signature bad^ ()) + (define bad + (let () + (define-signature bad^ ()) + (unit (import bad^) (export)))) + (invoke-unit bad (import bad^)) + (error ""))] + + ;; This tests that the linking clauses in compound-unit forms + ;; are correctly satisfied + ;; This is fairly subtle, and the type mismatch error + ;; message doesn't make it obvious why it fails to typecheck + [tc-err + (let () + (define-signature a^ ()) + + (define-unit a1 + (import) + (export a^)) + + (define-unit a2 + (import) + (export a^)) + + (define-unit u + (import a^) + (export) + (init-depend a^)) + + (define-compound-unit w + (import) + (export) + (link + (([A1 : a^]) a1) + (() u A2) + (([A2 : a^]) a2))) + (error ""))])) + diff --git a/typed-racket-test/xfail/fact-unit.rkt b/typed-racket-test/xfail/fact-unit.rkt new file mode 100644 index 00000000..6a8f01c7 --- /dev/null +++ b/typed-racket-test/xfail/fact-unit.rkt @@ -0,0 +1,18 @@ +#lang typed/racket + +;; It would be nice if this program could typecheck, but because the types +;; of unannotated exports are not added to the type environment the type +;; the fact function is not inferred correctly. Adding a type annotation +;; to fact allows this program to run. + +(define-signature fact^ + ([fact : (-> Integer Integer)])) + +(define-unit fact@ + (import (prefix i: fact^)) + (export fact^) + (define (fact n) + (if (< n 1) + 1 + (* n (i:fact (sub1 n))))) + fact) \ No newline at end of file