Skip to content

WIP: add type-out provide-spec #301

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

@begin[(require "../utils.rkt" scribble/example racket/sandbox)
(require (for-label (only-meta-in 0 [except-in typed/racket])
(only-in racket/contract contract-out)
(only-in racket/base)))]

@(define the-eval (make-base-eval))
Expand Down Expand Up @@ -514,9 +515,6 @@ for function types.
(: var4 : String -> Integer)]
}

@defform[(provide: [v t] ...)]{This declares that the @racket[v]s have
the types @racket[t], and also provides all of the @racket[v]s.}

@defform/none[#{v : t}]{ This declares that the variable @racket[v] has type
@racket[t]. This is legal only for binding occurrences of @racket[_v].

Expand Down Expand Up @@ -677,6 +675,41 @@ Uses outside of a module top-level raise an error.
(sync (alarm-evt (+ 100 (current-inexact-milliseconds))))]
}

@section{Provide}

@defform[(provide: [v t] ...)]{This declares that the @racket[v]s have
the types @racket[t], and also provides all of the @racket[v]s.}

@defform/subs[
#:literals (rename struct type)
(type-out type-out-spec ...)
([type-out-spec
(id t)
(rename orig-id id t)
(struct maybe-type-vars id/super ((id : t) ...)
struct-option)]
[maybe-type-vars code:blank
(v ...)]
[id/super id
(id super-id)]
[struct-option (code:line)
#:omit-constructor])]{
A @racket[_provide-spec] similar to @racket[contract-out] for use in @racket[provide]
(currently only for the same phase level as the enclosing @racket[provide] form).

The basic @racket[(id t)] form applies the type annotation @racket[t] to the identifier
@racket[id] and exports @racket[id].
This has the same effect as the sequence @racket[(begin (: id t) (provide id))].

The @racket[rename] form assigns @racket[orig-id] the type @racket[t] and exports
@racket[orig-id] under the name @racket[id].
Within the module only @racket[orig-id] is visible, but clients may only use @racket[id].

The @racket[struct] form describes the name and public fields of an existing structure type.
When the @racket[#:omit-constructor] option is given, the constructor name is not exported.
}


@section{Other Forms}

@defidform[with-handlers]{
Expand Down
104 changes: 104 additions & 0 deletions typed-racket-lib/typed-racket/base-env/prims.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -30,10 +30,12 @@ the typed racket language.
|#



(provide (except-out (all-defined-out) -let-internal define-for-variants
def-redirect
define-for*-variants with-handlers: define-for/acc:-variants
base-for/flvector: base-for/vector -lambda -define -do -let
provide-typed-vars
-let* -let*-values -let-values -let/cc -let/ec -letrec -letrec-values)
(all-from-out "top-interaction.rkt")
(all-from-out "case-lambda.rkt")
Expand Down Expand Up @@ -123,11 +125,16 @@ the typed racket language.
(for-syntax
racket/lazy-require
syntax/parse/pre
racket/struct-info
syntax/stx
racket/list
racket/provide-transform
racket/syntax
racket/base
(only-in racket/string string-prefix? string-split)
(only-in "../typecheck/tc-structs.rkt" name-of-struct)
(only-in "../typecheck/internal-forms.rkt" internal)
(only-in "../typecheck/find-annotation.rkt" find-annotation)
"annotate-classes.rkt"
"../utils/literal-syntax-class.rkt"
"../private/parse-classes.rkt"
Expand Down Expand Up @@ -636,6 +643,103 @@ the typed racket language.
(begin (: i* t) ...
(provide (rename-out [i* i] ...))))]))

(begin-for-syntax
(define-syntax-class (type-out-spec stx)
#:attributes (type-decl* provide-spec*)
#:datum-literals (rename struct type :) ;; 2016-02-03 'type' is unused for now
(pattern [n:id t]
#:attr type-decl* (syntax/loc stx (: n t))
#:attr provide-spec* (syntax/loc stx n))
(pattern [rename old-n:id new-n:id t]
#:attr type-decl* (syntax/loc stx (: old-n t))
#:attr provide-spec* (syntax/loc stx (rename-out (old-n new-n))))
(pattern [struct (~optional (~seq (v*:id ...)))
(~or n:id (n:id parent:id) (~seq n:id parent:id))
((f*:id : t*) ...)
(~optional (~and #:omit-constructor omit?))]
#:attr type-decl*
;; Make type annotations for each struct field accessor
;; Also:
;; - check that supertype information is correct
;; - check that all struct fields have an annotation (including super fields)
(let*-values ([(struct-info)
(or
(syntax-local-value #'n (lambda () #f))
(raise-syntax-error 'type-out "unknown struct type. (Make sure struct definitions come before their use in a type-out form)" stx (syntax-e #'n)))]
[(_struct-type constr _n? all-acc* _mut* super)
(apply values (extract-struct-info struct-info))]
[(acc*) ;; Reverse, filter superclass accessors, remove sentinel
(let ([n-str (symbol->string (syntax-e #'n))])
(for/fold ([out* '()])
([acc (in-list all-acc*)])
(if (and acc
(string-prefix? (symbol->string (syntax-e acc)) n-str))
(cons acc out*)
out*)))])
;; check parent, if given
(when (and (attribute parent)
(or (boolean? super) (not (free-identifier=? super #'parent))))
(raise-syntax-error
'type-out
(format "struct type ~a is not a subtype of ~a" (syntax-e #'n) (syntax-e #'parent))
stx))
;; match known accessors with field information
(let* ([f+t* (map syntax-e (syntax->list #'((f* . t*) ...)))]
[_check-dup ;; Check for duplicate field annotations
(for/fold ([prev #f])
([f+t (in-list f+t*)])
(when (and prev (free-identifier=? prev (car f+t)))
(raise-syntax-error 'type-out "duplicate annotation for struct field" (car f+t) stx))
(car f+t))]
[n-len (+ 1 (string-length (symbol->string (syntax-e #'n))))] ;; To infer field names
[acc+type*
(for/list ([acc (in-list acc*)])
(define acc-id
(format-id stx "~a" (substring (symbol->string (syntax-e acc)) n-len)))
(define f+t
(if (null? f+t*)
#f
(begin0 (car f+t*) (set! f+t* (cdr f+t*)))))
(unless f+t
(raise-syntax-error 'type-out "missing annotation for struct field" stx (syntax-e acc-id)))
(unless (free-identifier=? acc-id (car f+t))
(raise-syntax-error 'type-out (format "expected annotation for struct field '~a'" (syntax-e acc-id)) stx (cons (syntax-e (car f+t)) (syntax-e (cdr f+t)))))
(quasisyntax/loc stx (ann #,acc (-> n #,(cdr f+t)))))])
(unless (null? f+t*)
(raise-syntax-error 'type-out "struct field does not exist (supertype fields cannot be annotated in type-out)" stx (map (lambda (f+t) (syntax-e (car f+t))) f+t*)))
(quasisyntax/loc stx (let () #,@acc+type* (void)))))
#:attr provide-spec*
(if (attribute omit?)
(with-syntax ([constr (cadr (extract-struct-info (syntax-local-value #'n)))])
(if (free-identifier=? #'constr #'n)
;; Type is only constructor
(syntax/loc stx (except-out (struct-out n) constr))
;; We have 2 constructors (can't tell when struct name is not a constructor)
(syntax/loc stx (except-out (struct-out n) n constr))))
(syntax/loc stx (struct-out n))))))

(define-syntax provide-typed-vars
(make-provide-transformer
(λ (stx modes)
(for*/list ([provide-clause (in-list (syntax->list stx))]
[export (in-list (expand-export provide-clause modes))])
export))))

(define-syntax type-out
(make-provide-pre-transformer
(lambda (stx modes)
(syntax-parse stx
[(_ (~var e* (type-out-spec stx)) ...)
;; Move type declarations to the toplevel
(with-syntax ([(t* ...) #'(e*.type-decl* ...)])
(syntax-local-lift-module-end-declaration
(syntax-property ;; Mark, so we can lift to beginning of module later
(quasisyntax/loc stx (begin t* ...))
tr:type-out:type-annotation-property #t)))
;; Collect a flat list of provide specs & expand
(with-syntax ([(spec* ...) #'(e*.provide-spec* ...)])
(syntax/loc stx (provide-typed-vars spec* ...)))]))))

(define-syntax (declare-refinement stx)
(syntax-parse stx
[(_ p:id)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,7 @@
(tr:class:local-table tr:class:local-table)
(tr:class:name-table tr:class:name-table)
(tr:class:def tr:class:def)
(tr:type-out:type-annotation tr:type-out:type-annotation)
(tr:unit tr:unit #:mark)
(tr:unit:body-exp-def-type tr:unit:body-exp-def-type)
(tr:unit:invoke tr:unit:invoke)
Expand Down
13 changes: 12 additions & 1 deletion typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -315,11 +315,22 @@
(~datum prefix-all-defined) (~datum prefix-all-defined-except)
(~datum expand)))))

;; Move type declarations introduced by 'type-out' to the beginning
;; of a list of forms.
;; Maintain relative ordering of lifted declarations and of other declarations.
;; Exists because typechecking depends on the ordering of annotations vs. defs,
;; and there is no `syntax-local-lift-module-begin-declaration` function.
;; (-> (Listof Syntax) (Listof Syntax))
(define (lift-type-out-declarations form*)
(define (is-type-out-decl? form)
(syntax-property form tr:type-out:type-annotation-property))
(call-with-values (lambda () (partition is-type-out-decl? form*)) append))

;; actually do the work on a module
;; produces prelude and post-lude syntax objects
;; syntax-list -> (values syntax syntax)
(define (type-check forms0)
(define forms (syntax->list forms0))
(define forms (lift-type-out-declarations (syntax->list forms0)))
(do-time "before form splitting")
(define-values (type-aliases struct-defs stx-defs0 val-defs0 provs signature-defs)
(filter-multiple
Expand Down
1 change: 1 addition & 0 deletions typed-racket-test/unit-tests/all-tests.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -44,4 +44,5 @@
"prims-tests.rkt"
"tooltip-tests.rkt"
"prefab-tests.rkt"
"type-out-tests.rkt"
"typed-units-tests.rkt")
Loading