diff --git a/collects/typed-scheme/infer/signatures.ss b/collects/typed-scheme/infer/signatures.ss index 6db02b38dc..a3b85665f3 100644 --- a/collects/typed-scheme/infer/signatures.ss +++ b/collects/typed-scheme/infer/signatures.ss @@ -1,29 +1,42 @@ #lang scheme/base -(require scheme/unit) +(require scheme/unit scheme/contract "constraint-structs.ss" "../utils/utils.ss") +(require (rep type-rep) (utils unit-utils)) (provide (all-defined-out)) (define-signature dmap^ - (dmap-meet)) + ([cnt dmap-meet (dmap? dmap? . -> . dmap?)])) (define-signature promote-demote^ - (var-promote var-demote)) + ([cnt var-promote (Type? (listof symbol?) . -> . Type?)] + [cnt var-demote (Type? (listof symbol?) . -> . Type?)])) (define-signature constraints^ - (exn:infer? - fail-sym + ([cnt exn:infer? (any/c . -> . boolean?)] + [cnt fail-sym symbol?] ;; inference failure - masked before it gets to the user program (define-syntaxes (fail!) (syntax-rules () [(_ s t) (raise fail-sym)])) - cset-meet cset-meet* + [cnt cset-meet (cset? cset? . -> . cset?)] + [cnt cset-meet* ((listof cset?) . -> . cset?)] no-constraint - empty-cset - insert - cset-combine - c-meet)) + [cnt empty-cset ((listof symbol?) . -> . cset?)] + [cnt insert (cset? symbol? Type? Type? . -> . cset?)] + [cnt cset-combine ((listof cset?) . -> . cset?)] + [cnt c-meet ((c? c?) (symbol?) . ->* . c?)])) (define-signature restrict^ - (restrict)) + ([cnt restrict (Type? Type? . -> . Type?)])) (define-signature infer^ - (infer infer/vararg infer/dots)) + ([cnt infer (((listof symbol?) (listof Type?) (listof Type?) Type? (listof symbol?)) ((or/c #f Type?)) . ->* . any)] + [cnt infer/vararg (((listof symbol?) + (listof Type?) + (listof Type?) + Type? Type? + (listof symbol?)) + ((or/c #f Type?)) . ->* . any)] + [cnt infer/dots (((listof symbol?) + symbol? + (listof Type?) (listof Type?) Type? Type? (listof symbol?)) + (#:expected (or/c #f Type?)) . ->* . any)])) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 1eeec0cfd0..4034d2ed70 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -46,7 +46,8 @@ [null (-val null)] [number? (make-pred-ty N)] [char? (make-pred-ty -Char)] -[integer? (make-pred-ty -Integer)] +[integer? (Univ . -> . B : (list (make-Latent-Restrict-Effect N)) (list (make-Latent-Remove-Effect -Integer)))] +[exact-integer? (make-pred-ty -Integer)] [boolean? (make-pred-ty B)] [add1 (cl->* (-> -Integer -Integer) (-> N N))] diff --git a/collects/typed-scheme/private/base-types-extra.ss b/collects/typed-scheme/private/base-types-extra.ss index db633260bf..b31f182fe5 100644 --- a/collects/typed-scheme/private/base-types-extra.ss +++ b/collects/typed-scheme/private/base-types-extra.ss @@ -11,9 +11,12 @@ ;; special types names that are not bound to particular types (define-other-types - -> U mu Un All Opaque Vectorof - Parameter Tuple Class Values) + -> U mu All Opaque + Parameter Tuple Class Values Instance + pred) (provide (rename-out [All ∀] + [U Un] + [Tuple List] [mu Rec])) diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss index 296bd88f3b..0cbae61e0b 100644 --- a/collects/typed-scheme/private/base-types.ss +++ b/collects/typed-scheme/private/base-types.ss @@ -12,20 +12,21 @@ [Regexp -Regexp] [PRegexp -PRegexp] [Char -Char] -[Option (-poly (a) (-opt a))] -[List (-lst Univ)] -[Listof -Listof] [Namespace -Namespace] [Input-Port -Input-Port] [Output-Port -Output-Port] [Bytes -Bytes] +#;[List (-lst Univ)] [EOF (-val eof)] +[Syntax Any-Syntax] +[Identifier Ident] +[Procedure top-func] [Keyword -Keyword] +[Listof -Listof] +[Vectorof (-poly (a) (make-Vector a))] +[Option (-poly (a) (-opt a))] [HashTable (-poly (a b) (-HT a b))] [Promise (-poly (a) (-Promise a))] [Pair (-poly (a b) (-pair a b))] [Boxof (-poly (a) (make-Box a))] -[Syntax Any-Syntax] -[Identifier Ident] -[Procedure top-func] diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 551dc14b7a..6c38ec5fac 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -1,17 +1,21 @@ #lang scheme/base -(provide parse-type parse-type/id) +(provide parse-type parse-type/id parse-type*) -(require (except-in "../utils/utils.ss" extend)) +(require (except-in "../utils/utils.ss" extend id)) (require (except-in (rep type-rep) make-arr) "type-effect-convenience.ss" (only-in "type-effect-convenience.ss" [make-arr* make-arr]) (utils tc-utils) "union.ss" syntax/stx + stxclass stxclass/util (env type-environments type-name-env type-alias-env) "type-utils.ss" - scheme/match) + (prefix-in t: "base-types-extra.ss") + scheme/match + "stxclass-util.ss" + (for-template scheme/base "base-types-extra.ss")) (define enable-mu-parsing (make-parameter #t)) @@ -23,8 +27,238 @@ (define (stx-cadr stx) (stx-car (stx-cdr stx))) -(define (parse-type stx) +(define-syntax-class star + (pattern star:id + #:when (eq? '* #'star.datum))) + +(define-syntax-class ddd + (pattern ddd:id + #:when (eq? '... #'ddd.datum))) + +(define-syntax-class tvar + #:description "type variable" + (pattern v:id + #:with val (lookup (current-tvars) #'v.datum (lambda (_) #f)) + #:with name #'v.datum + #:with datum #'v.datum + #:when #'val)) + +(define-syntax-class dotted-tvar + #:description "type variable bound with ..." + (pattern v:tvar + #:when (Dotted? #'v.val) + #:with t (Dotted-t #'v.val) + #:with val #'v.val + #:with name #'v.datum + #:with datum #'v.datum)) + +(define-syntax-class dotted-both-tvar + #:transparent + (pattern v:dotted-tvar + #:when (DottedBoth? #'v.val) + #:with t (Dotted-t #'v.val) + #:with val #'v.val + #:with name #'v.datum + #:with datum #'v.datum)) + + +(define-syntax-class (type/tvars syms var-tys) + (pattern ty + #:with t (parameterize ([current-tvars (extend-env syms + var-tys + (current-tvars))]) + (parse-type* #'ty)))) + +(define-syntax-class (type/tvar sym var-ty) + (pattern ty + #:declare ty (type/tvars (list sym) (list var-ty)) + #:with t #'ty.t)) + + +(define-syntax-class fun-ty + #:literals (t:-> :) + #:description "function type" + ;; FIXME - shouldn't have to use syntax->datum + (pattern (dom*:type t:-> rng:type : pred:type) + #:when (add-type-name-reference #'t:->) + #:with t (make-pred-ty (list #'dom*.t) #'rng.t #'pred.t) + #:with (dom ...) (list #'dom*)) + (pattern (dom:type ... rest:type _:star t:-> rng:type) + #:when (add-type-name-reference #'t:->) + #:with t (->* (syntax->datum #'(dom.t ...)) #'rest.t #'rng.t)) + (pattern (dom:type ... rest _:ddd bound:dotted-tvar t:-> rng:type) + #:with rest.t (parse/get #'rest t (type/tvar #'bound.name (make-DottedBoth (make-F #'bound.name)))) + #:when (add-type-name-reference #'t:->) + #:with t + (let ([var #'bound.val]) + (make-Function + (list + (make-arr-dots (syntax->datum #'(dom.t ...)) + #'rng.t + #'rest.t + #'bound.name))))) + (pattern (dom:type ... t:-> rng:type) + #:when (add-type-name-reference #'t:->) + #:with t (->* (syntax->datum #'(dom.t ...)) #'rng.t))) + +(define-syntax-class fun-ty/one + (pattern f:fun-ty + #:with arr (match #'f.t [(Function: (list a)) a]))) + + +(define-syntax-class values-ty + #:literals (values) + (pattern (values ts:type ... rest _:ddd bound:dotted-tvar) + #:with rest.t (parse/get #'rest t (type/tvar #'bound.name (make-DottedBoth (make-F #'bound.name)))) + #:with t + (make-ValuesDots (syntax->datum #'(ts.t ...)) + #'rest.t + #'bound.name)) + (pattern (values ts:type ...) + #:with t (-values (syntax->datum #'(ts.t ...))))) + +(define-syntax-class type-name + (pattern i:id + #:when (lookup-type-name #'i (lambda () #f)) + #:with t #'(make-Name #'i) + #:when (add-type-name-reference #'i))) + +(define-syntax-class type-alias + (pattern i:id + #:with t (lookup-type-alias #'i parse-type* (lambda () #f)) + #:when #'t + #:when (add-type-name-reference #'i))) + +(define-syntax-class all-type + #:literals (t:All) + (pattern (t:All (v:id ... v-last:id _:ddd) b) + #:with b.t (parse/get #'b t (type/tvars (cons #'v-last.datum (syntax->datum #'(v ...))) + (cons (make-Dotted (make-F #'v-last.datum)) + (map make-F (syntax->datum #'(v ...)))))) + #:when (add-type-name-reference #'All) + #:with t (make-PolyDots (syntax->datum #'(v ... v-last)) #'b.t)) + (pattern (t:All (v:id ...) b) + #:with b.t (parse/get #'b t (type/tvars (syntax->datum #'(v ...)) (map make-F (syntax->datum #'(v ...))))) + #:when (add-type-name-reference #'All) + #:with t (make-Poly (syntax->datum #'(v ...)) #'b.t))) + +(define-syntax-class type-app + (pattern (i arg:type args:type ...) + #:when (identifier? #'i) + #:declare i type + #:with t + (let loop + ([rator #'i.t] [args (syntax->datum #'(arg.t args.t ...))]) + (match rator + [(Name: _) + ;; FIXME - need orig stx + (make-App rator args #'here)] + [(Poly: ns _) + (if (not (= (length args) (length ns))) + (begin + (tc-error/delayed "Wrong number of arguments to type ~a, expected ~a but got ~a" rator (length ns) (length args)) + (instantiate-poly rator (map (lambda _ Err) ns))) + (instantiate-poly rator args))] + [(Mu: _ _) (loop (unfold rator) args)] + [(Error:) Err] + [_ (tc-error/delayed "Type ~a cannot be applied, arguments were: ~a" rator args) + Err])))) + +(define-syntax-class not-kw-id + (pattern i:id + #:when (not (for/or ([e (syntax->list + #'(quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance + t:-> t:All))]) + (free-identifier=? e #'i))) + #:when (not (memq #'i.datum '(* ...))) + #:with datum #'i.datum)) + +(define-syntax-class type + #:literals (quote t:pred t:Tuple case-lambda t:U t:Rec t:Opaque t:Parameter t:Class t:Instance) + (pattern ty + #:declare ty (3d Type?) + #:with t #'ty.datum) + (pattern i:dotted-both-tvar + #:with t #'i.t) + #; + (pattern i:dotted-tvar + #:when (tc-error/stx #'i "Type variable ~a must be used with ..." #'i.datum) + #:with t Err) + (pattern i:tvar + #:when (not (Dotted? #'i.val)) + #:with t #'i.val) + (pattern i:type-alias + #:with t #'i.t) + (pattern i:type-name + #:with t #'i.t) + #; + (pattern i:not-kw-id + #:with t Err + #:when (tc-error/stx #'i "Unbound type name ~a" #'i.datum) + ) + (pattern ty:all-type + #:with t #'ty.t) + (pattern (t:Rec x:id b) + #:when (enable-mu-parsing) + #:with b.t (parse/get #'b t (type/tvar #'x.datum (make-F #'x.datum))) + #:when (add-type-name-reference #'t:Rec) + #:with t (if (memq #'x.datum (fv #'b.t)) + (make-Mu #'x.datum #'b.t) + #'b.t)) + (pattern (t:pred ty:type) + #:when (add-type-name-reference #'t:pred) + #:with t (make-pred-ty #'ty.t)) + (pattern (t:Parameter ty:type) + #:when (add-type-name-reference #'t:Paramter) + #:with t (-Param #'ty.t #'ty.t)) + (pattern (t:Parameter t1:type t2:type) + #:when (add-type-name-reference #'t:Paramter) + #:with t (-Param #'t1.t #'t2.t)) + (pattern (t:Opaque p?:id) + #:when (add-type-name-reference #'t:Opaque) + #:with t (make-Opaque #'p? (syntax-local-certifier))) + (pattern (t:U ty:type ...) + #:with t (apply Un (syntax->datum #'(ty.t ...)))) + (pattern (t:Tuple ty:type ...) + #:with t (-Tuple (syntax->datum #'(ty.t ...)))) + (pattern fty:fun-ty + #:with t #'fty.t) + (pattern vt:values-ty + #:with t #'vt.t) + (pattern (fst:type . rst:type) + #:with t (-pair #'fst.t #'rst.t)) + (pattern (quote v:atom) + #:with t (-val #'v.datum)) + (pattern (case-lambda f:fun-ty/one ...) + #:with t (make-Function (syntax->datum #'(f.arr ...)))) + + (pattern (t:Class (pos-args:type ...) ([fname:id fty:type ((rest:boolean) #:opt) ...*] ...) ([mname:id mty:type] ...)) + #:with t + (make-Class + (syntax->datum #'(pos-args.t ...)) + (syntax->datum #'([fname.datum fty.t rest.datum] ...)) + (syntax->datum #'([mname.datum mty.t] ...)))) + + (pattern (t:Instance ty:type) + #:with t + (if (not (or (Mu? #'ty.t) (Class? #'ty.t) (Union? #'ty.t) (Error? #'ty.t))) + (begin (tc-error/delayed "Argument to Instance must be a class type, got ~a" #'ty.t) + (make-Instance Err)) + (make-Instance #'ty.t))) + + (pattern tapp:type-app + #:with t #'tapp.t) + + (pattern v:atom + #:when (not (symbol? #'v.datum)) + #:with t (-val #'v.datum))) + +(define (parse-type* stx) (parameterize ([current-orig-stx stx]) + (parse/get stx t type))) + +(define (parse-type stx) + (parameterize ([current-orig-stx stx]) (syntax-case* stx () symbolic-identifier=? [t diff --git a/collects/typed-scheme/private/require-contract.ss b/collects/typed-scheme/private/require-contract.ss index c718b42fc0..73570ff2b7 100644 --- a/collects/typed-scheme/private/require-contract.ss +++ b/collects/typed-scheme/private/require-contract.ss @@ -25,7 +25,7 @@ [(require/contract nm cnt lib) (identifier? #'nm) #`(begin (require (only-in lib [nm tmp])) - (define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))] + (define-ignored nm (contract cnt tmp '(interface for #,(syntax->datum #'nm)) 'never-happen (quote-syntax nm))))] [(require/contract (orig-nm nm) cnt lib) #`(begin (require (only-in lib [orig-nm tmp])) (define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))])) diff --git a/collects/typed-scheme/private/stxclass-util.ss b/collects/typed-scheme/private/stxclass-util.ss new file mode 100644 index 0000000000..c0abe348fe --- /dev/null +++ b/collects/typed-scheme/private/stxclass-util.ss @@ -0,0 +1,33 @@ +#lang scheme/base + +(require stxclass (for-syntax stxclass scheme/base stxclass/util)) + +(provide (all-defined-out)) + +(define-syntax (parse/get stx) + (syntax-parse stx + [(_ arg:expr attr:id pat) + (let* ([i (generate-temporary)] + [get-i (datum->syntax + i + (string->symbol + (string-append (symbol->string (syntax-e i)) + "." + (symbol->string #'attr.datum))))]) + (quasisyntax/loc stx + (syntax-parse arg + [#,i #:declare #,i pat #'#,get-i])))])) + +(define (atom? v) + (or (number? v) (string? v) (boolean? v) (symbol? v) (keyword? v) (char? v) (bytes? v) (regexp? v))) + +(define-syntax-class (3d pred) + (pattern s + #:with datum (syntax-e #'s) + #:when (pred #'datum))) + +(define-pred-stxclass atom atom?) +(define-pred-stxclass byte-pregexp byte-pregexp?) +(define-pred-stxclass byte-regexp byte-regexp?) +(define-pred-stxclass regexp regexp?) +(define-pred-stxclass bytes bytes?) \ No newline at end of file diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 7263ca8618..d0d6629bc7 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -81,15 +81,15 @@ (ormap (lambda (e) (arr-subtype*/no-fail A e s)) ts)) (define (sub-eff e1 e2) - (match (list e1 e2) - [(list e e) #t] - [(list (Latent-Restrict-Effect: t) (Latent-Restrict-Effect: t*)) + (match* (e1 e2) + [(e e) #t] + [((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: t*)) (and (subtype t t*) (subtype t* t))] - [(list (Latent-Remove-Effect: t) (Latent-Remove-Effect: t*)) + [((Latent-Remove-Effect: t) (Latent-Remove-Effect: t*)) (and (subtype t t*) (subtype t* t))] - [else #f])) + [(_ _) #f])) ;(trace sub-eff) diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss index 1279c4ea02..69c91f5196 100644 --- a/collects/typed-scheme/private/type-effect-convenience.ss +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -119,7 +119,7 @@ (make-Struct s #f (list t) #f #f #'promise? values)))) (define N (make-Base 'Number #'number?)) -(define -Integer (make-Base 'Integer #'integer?)) +(define -Integer (make-Base 'Integer #'exact-integer?)) (define B (make-Base 'Boolean #'boolean?)) (define Sym (make-Base 'Symbol #'symbol?)) (define -Void (make-Base 'Void #'void?)) diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss index 37f248c391..b5852df8d3 100644 --- a/collects/typed-scheme/private/type-effect-printer.ss +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -64,9 +64,10 @@ (when drest (fp "~a ... ~a " (car drest) (cdr drest))) (fp "-> ~a" rng) - (match* (thn-eff els-eff) + (match* (thn-eff els-eff) [((list) (list)) (void)] [((list (Latent-Restrict-Effect: t)) (list (Latent-Remove-Effect: t))) (fp " : ~a" t)] + [((list (Latent-Restrict-Effect: t)) (list (Latent-Remove-Effect: t))) (fp " : ~a" t)] [(_ _) (fp " : ~a ~a" thn-eff els-eff)]) (fp ")")])) (define (tuple? t) diff --git a/collects/typed-scheme/rep/effect-rep.ss b/collects/typed-scheme/rep/effect-rep.ss index 892c889584..96f8768c9b 100644 --- a/collects/typed-scheme/rep/effect-rep.ss +++ b/collects/typed-scheme/rep/effect-rep.ss @@ -27,10 +27,12 @@ [#:fold-rhs (*Remove-Effect (type-rec-id t) v)]) ;; t is a Type -(de Latent-Restrict-Effect (t)) +(de Latent-Restrict-Effect (t) [#:frees (free-vars* t) (free-idxs* t)] + [#:fold-rhs (*Latent-Restrict-Effect (type-rec-id t))]) ;; t is a Type -(de Latent-Remove-Effect (t)) +(de Latent-Remove-Effect (t) [#:frees (free-vars* t) (free-idxs* t)] + [#:fold-rhs (*Latent-Remove-Effect (type-rec-id t))]) (de Latent-Var-True-Effect () [#:frees #f] [#:fold-rhs #:base]) diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss index 8e4124b37e..14e39c96a9 100644 --- a/collects/typed-scheme/rep/rep-utils.ss +++ b/collects/typed-scheme/rep/rep-utils.ss @@ -11,7 +11,7 @@ scheme/base syntax/struct syntax/stx - (utils utils))) + (utils utils))) (provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq) diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl index 57f96451dc..1d1af93d61 100644 --- a/collects/typed-scheme/ts-reference.scrbl +++ b/collects/typed-scheme/ts-reference.scrbl @@ -19,25 +19,33 @@ @section[#:tag "type-ref"]{Type Reference} @subsubsub*section{Base Types} -These types represent primitive Scheme data. -@defidform[Number]{A @gtech{number}} -@defidform[Integer]{An @gtech{integer}} -@defidform[Boolean]{Either @scheme[#t] or @scheme[#f]} -@defidform[String]{A @gtech{string}} -@defidform[Keyword]{A literal @gtech{keyword}} -@defidform[Symbol]{A @gtech{symbol}} -@defidform[Void]{@|void-const|} -@defidform[Port]{A @gtech{port}} -@defidform[Path]{A @rtech{path}} -@defidform[Char]{A @gtech{character}} +@deftogether[( +@defidform[Number] +@defidform[Integer] +@defidform[Boolean] +@defidform[String] +@defidform[Keyword] +@defidform[Symbol] +@defidform[Void] +@defidform[Input-Port] +@defidform[Output-Port] +@defidform[Path] +@defidform[Regexp] +@defidform[PRegexp] +@defidform[Syntax] +@defidform[Bytes] +@defidform[Namespace] +@defidform[EOF] +@defidform[Char])]{ +These types represent primitive Scheme data.} -@defidform[Any]{Any value} +@defidform[Any]{Any Scheme value. All other types are subtypes of @scheme[Any].} The following base types are parameteric in their type arguments. -@defform[(Listof t)]{Homogenous @gtech{lists} of @scheme[t]} -@defform[(Boxof t)]{A @gtech{box} of @scheme[t]} -@defform[(Vectorof t)]{Homogenous @gtech{vectors} of @scheme[t]} +@defform[(Listof t)]{Homogenous @rtech{lists} of @scheme[t]} +@defform[(Boxof t)]{A @rtech{box} of @scheme[t]} +@defform[(Vectorof t)]{Homogenous @rtech{vectors} of @scheme[t]} @defform[(Option t)]{Either @scheme[t] of @scheme[#f]} @defform*[[(Parameter t) (Parameter s t)]]{A @rtech{parameter} of @scheme[t]. If two type arguments are supplied, @@ -100,46 +108,60 @@ creating new types, and annotating expressions. @scheme[_loop], @scheme[_f], @scheme[_a], and @scheme[_v] are names, @scheme[_t] is a type. @scheme[_e] is an expression and @scheme[_body] is a block. +@defform*[[ + (let: ([v : t e] ...) . body) + (let: loop : t0 ([v : t e] ...) . body)]]{ +Local bindings, like @scheme[let], each with +associated types. In the second form, @scheme[_t0] is the type of the +result of @scheme[_loop] (and thus the result of the entire + expression as well as the final + expression in @scheme[body]).} +@deftogether[[ +@defform[(letrec: ([v : t e] ...) . body)] +@defform[(let*: ([v : t e] ...) . body)]]]{Type-annotated versions of +@scheme[letrec] and @scheme[let*].} + +@subsection{Anonymous Functions} + +@defform/subs[(lambda: formals . body) +([formals ([v : t] ...) + ([v : t] ... . [v : t])])]{ +A function of the formal arguments @scheme[v], where each formal +argument has the associated type. If a rest argument is present, then +it has type @scheme[(Listof t)].} +@defform[(λ: formals . body)]{ +An alias for the same form using @scheme[lambda:].} +@defform[(plambda: (a ...) formals . body)]{ +A polymorphic function, abstracted over the type variables +@scheme[a]. The type variables @scheme[a] are bound in both the types +of the formal, and in any type expressions in the @scheme[body].} +@defform[(case-lambda: [formals body] ...)]{ +A function of multiple arities. Note that each @scheme[formals] must have a +different arity.} +@defform[(pcase-lambda: (a ...) [formals body] ...)]{ +A polymorphic function of multiple arities.} + +@subsection{Definitions} + @defform*[[(define: v : t e) - (define: (f [v : t] ...) : t . body) - (define: (a ...) (f [v : t] ...) : t . body)]]{ + (define: (f . formals) : t . body) + (define: (a ...) (f . formals) : t . body)]]{ These forms define variables, with annotated types. The first form defines @scheme[v] with type @scheme[t] and value @scheme[e]. The second and third forms defines a function @scheme[f] with appropriate types. In most cases, use of @scheme[:] is preferred to use of @scheme[define:].} -@defform*[[ - (let: ([v : t e] ...) . body) - (let: loop : t0 ([v : t e] ...) . body)]]{where @scheme[_t0] is the type of the - result of @scheme[_loop] (and thus the result of the entire expression).} -@defform[ - (letrec: ([v : t e] ...) . body)]{} -@defform[ - (let*: ([v : t e] ...) . body)]{} -@defform*[[ - (lambda: ([v : t] ...) . body) - (lambda: ([v : t] ... . [v : t]) . body)]]{} -@defform*[[ - (plambda: (a ...) ([v : t] ...) . body) - (plambda: (a ...) ([v : t] ... . [v : t]) . body)]]{} -@defform[ - (case-lambda: [formals body] ...)]{where @scheme[_formals] is like - the second element of a @scheme[lambda:]} -@defform[ - (pcase-lambda: (a ...) [formals body] ...)]{where @scheme[_formals] is like - the second element of a @scheme[lambda:].} @subsection{Structure Definitions} -@defform*[[ -(define-struct: name ([f : t] ...)) -(define-struct: (name parent) ([f : t] ...)) -(define-struct: (v ...) name ([f : t] ...)) -(define-struct: (v ...) (name parent) ([f : t] ...))]]{ +@defform/subs[ +(define-struct: maybe-type-vars name-spec ([f : t] ...)) +([maybe-type-vars code:blank (v ...)] + [name-spec name (name parent)])]{ Defines a @rtech{structure} with the name @scheme[name], where the - fields @scheme[f] have types @scheme[t]. The second and fourth forms - define @scheme[name] to be a substructure of @scheme[parent]. The - last two forms define structures that are polymorphic in the type + fields @scheme[f] have types @scheme[t]. When @scheme[parent], the +structure is a substructure of @scheme[parent]. When +@scheme[maybe-type-vars] is present, the structure is polymorphic in the type variables @scheme[v].} @subsection{Type Aliases} @@ -172,7 +194,7 @@ This is legal only in expression contexts.} appropriate number of type variables. This is legal only in expression contexts.} -@litchar|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)]. +@schemevarfont|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)]. @subsection{Require} @@ -183,7 +205,16 @@ naming a predicate, and @scheme[_r] is an optionally-renamed identifier. (require/typed r t m) (require/typed m [r t] ...) ]]{The first form requires @scheme[r] from module @scheme[m], giving -it type @scheme[t]. The second form generalizes this to multiple identifiers.} +it type @scheme[t]. The second form generalizes this to multiple +identifiers. + +In both cases, the identifiers are protected with @rtech{contracts} which +enforce the type @scheme[t]. If this contract fails, the module +@scheme[m] is blamed. + +Some types, notably polymorphic types constructed with @scheme[All], +cannot be converted to contracts and raise a static error when used in +a @scheme[require/typed] form.} @defform[(require/opaque-type t pred m)]{ This defines a new type @scheme[t]. @scheme[pred], imported from @@ -191,4 +222,23 @@ module @scheme[m], is a predicate for this type. The type is defined as precisely those values to which @scheme[pred] produces @scheme[#t]. @scheme[pred] must have type @scheme[(Any -> Boolean)].} -@defform[(require-typed-struct name ([f : t] ...) m)]{} +@defform*[[(require-typed-struct name ([f : t] ...) m) + (require-typed-struct (name parent) ([f : t] ...) m)]]{ +Requires all the functions associated with the structure @scheme[name] from the module @scheme[m], +with the appropriate types. The structure predicate has the +appropriate Typed Scheme filter type so that it may be used as a +predicate in @scheme[if] expressions in Typed Scheme. + +In the second form, @scheme[parent] must already be a structure type +known to Typed Scheme, either via @scheme[define-struct:] or +@scheme[require-typed-struct]. +} + +@defform/subs[(do: : u ([id : t init-expr step-expr-maybe] ...) + (stop?-expr finish-expr ...) + expr ...+) + ([step-expr-maybe code:blank + step-expr])]{ +Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and +the final body @scheme[expr] having the type @scheme[u]. +} diff --git a/collects/typed-scheme/typecheck/check-subforms-unit.ss b/collects/typed-scheme/typecheck/check-subforms-unit.ss index e37c6f3719..3dd9208d83 100644 --- a/collects/typed-scheme/typecheck/check-subforms-unit.ss +++ b/collects/typed-scheme/typecheck/check-subforms-unit.ss @@ -12,7 +12,7 @@ (export check-subforms^) ;; find the subexpressions that need to be typechecked in an ignored form -;; syntax -> void +;; syntax -> any (define (check-subforms/with-handlers form) (define handler-tys '()) (define body-ty #f) @@ -48,6 +48,7 @@ [_ (void)]))) (ret (apply Un body-ty handler-tys))) +;; syntax type -> any (define (check-subforms/with-handlers/check form expected) (let loop ([form form]) (parameterize ([current-orig-stx form]) @@ -73,7 +74,7 @@ (ret expected)) ;; typecheck the expansion of a with-handlers form -;; syntax -> type +;; syntax -> any (define (check-subforms/ignore form) (let loop ([form form]) (kernel-syntax-case* form #f () diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss index 572becfda2..530ad0094c 100644 --- a/collects/typed-scheme/typecheck/signatures.ss +++ b/collects/typed-scheme/typecheck/signatures.ss @@ -1,28 +1,49 @@ #lang scheme/base -(require scheme/unit) +(require scheme/unit scheme/contract "../utils/utils.ss") +(require (rep type-rep) + (utils unit-utils) + (private type-utils)) (provide (all-defined-out)) (define-signature typechecker^ - (type-check tc-toplevel-form)) + ([cnt type-check (syntax? . -> . syntax?)] + [cnt tc-toplevel-form (syntax? . -> . any)])) (define-signature tc-expr^ - (tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t)) + ([cnt tc-expr (syntax? . -> . tc-result?)] + [cnt tc-expr/check (syntax? Type? . -> . tc-result?)] + [cnt tc-expr/check/t (syntax? Type? . -> . Type?)] + [cnt check-below (->d ([s (or/c Type? tc-result?)] [t Type?]) () [_ (if (Type? s) Type? tc-result?)])] + [cnt tc-literal (any/c . -> . Type?)] + [cnt tc-exprs ((listof syntax?) . -> . tc-result?)] + [cnt tc-exprs/check ((listof syntax?) Type? . -> . tc-result?)] + [cnt tc-expr/t (syntax? . -> . Type?)])) (define-signature check-subforms^ - (check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check)) + ([cnt check-subforms/ignore (syntax? . -> . any)] + [cnt check-subforms/with-handlers (syntax? . -> . any)] + [cnt check-subforms/with-handlers/check (syntax? Type? . -> . any)])) (define-signature tc-if^ - (tc/if-onearm tc/if-twoarm tc/if-onearm/check tc/if-twoarm/check)) + ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-result?)] + [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type? . -> . tc-result?)])) (define-signature tc-lambda^ - (tc/lambda tc/lambda/check tc/rec-lambda/check)) + ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)] + [cnt tc/lambda/check (syntax? syntax? syntax? Type? . -> . tc-result?)] + [cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type?) Type? . -> . Type?)])) (define-signature tc-app^ - (tc/app tc/app/check tc/funapp)) + ([cnt tc/app (syntax? . -> . tc-result?)] + [cnt tc/app/check (syntax? Type? . -> . tc-result?)] + [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type?) . -> . tc-result?)])) (define-signature tc-let^ - (tc/let-values tc/letrec-values tc/let-values/check tc/letrec-values/check)) + ([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-result?)] + [cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-result?)] + [cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)] + [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)])) (define-signature tc-dots^ - (tc/dots)) + ([cnt tc/dots (syntax? . -> . (values Type? symbol?))])) diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss index a341e184c7..3c75308f3d 100644 --- a/collects/typed-scheme/typecheck/tc-app-unit.ss +++ b/collects/typed-scheme/typecheck/tc-app-unit.ss @@ -2,6 +2,8 @@ (require (only-in "../utils/utils.ss" debug in-syntax printf/log in-pairs rep utils private env [infer r:infer])) (require "signatures.ss" + stxclass + (for-syntax stxclass) (rep type-rep effect-rep) (utils tc-utils) (private subtype type-utils union type-effect-convenience type-effect-printer resolve-type @@ -359,7 +361,7 @@ ""))))) (define-syntax (handle-clauses stx) - (syntax-case stx () + (syntax-parse stx [(_ (lsts ... rngs) f-stx pred infer t argtypes expected) (with-syntax ([(vars ... rng) (generate-temporaries #'(lsts ... rngs))]) (syntax/loc stx @@ -368,8 +370,8 @@ (let ([substitution (infer vars ... rng)]) (and substitution (log-result substitution) - (or expected - (ret (subst-all substitution rng)))))) + (ret (or expected + (subst-all substitution rng)))))) (poly-fail t argtypes #:name (and (identifier? f-stx) f-stx)))))])) (define (poly-fail t argtypes #:name [name #f]) @@ -501,6 +503,40 @@ (check-below t expected) (ret expected)) +(define-syntax-class lv-clause + #:transparent + (pattern [(v:id ...) e:expr])) + +(define-syntax-class lv-clauses + #:transparent + (pattern (cl:lv-clause ...) + #:with (e ...) #'(cl.e ...) + #:with (vs ...) #'((cl.v ...) ...))) + +(define-syntax-class core-expr + #:literals (reverse letrec-syntaxes+values let-values #%plain-app + if letrec-values begin #%plain-lambda set! case-lambda + begin0 with-continuation-mark) + #:transparent + (pattern (let-values cls:lv-clauses body) + #:with (expr ...) #'(cls.e ... body)) + (pattern (letrec-values cls:lv-clauses body) + #:with (expr ...) #'(cls.e ... body)) + (pattern (letrec-syntaxes+values _ cls:lv-clauses body) + #:with (expr ...) #'(cls.e ... body)) + (pattern (#%plain-app expr ...)) + (pattern (if expr ...)) + (pattern (with-continuation-mark expr ...)) + (pattern (begin expr ...)) + (pattern (begin0 expr ...)) + (pattern (#%plain-lambda _ e) + #:with (expr ...) #'(e)) + (pattern (case-lambda [_ expr] ...)) + (pattern (set! _ e) + #:with (expr ...) #'(e)) + (pattern _ + #:with (expr ...) #'())) + ;; expr id -> type or #f ;; if there is a binding in stx of the form: ;; (let ([x (reverse name)]) e) @@ -508,28 +544,20 @@ (define (find-annotation stx name) (define (find s) (find-annotation s name)) (define (match? b) - (kernel-syntax-case* b #f (reverse) - [[(v) (#%plain-app reverse n)] - (free-identifier=? name #'n) - (begin ;(printf "found annotation: ~a ~a~n~a~n" (syntax-e name) (syntax-e #'v) (type-annotation #'v)) - (type-annotation #'v))] + (syntax-parse b + #:literals (#%plain-app reverse) + [c:lv-clause + #:with (#%plain-app reverse n:id) #'c.e + #:when (free-identifier=? name #'n) + (type-annotation #'v)] [_ #f])) - (kernel-syntax-case* - stx #f (reverse letrec-syntaxes+values) - [(let-values (binding ...) body) - (cond [(ormap match? (syntax->list #'(binding ...)))] - [else (find #'body)])] - [(#%plain-app e ...) (ormap find (syntax->list #'(e ...)))] - [(if e1 e2 e3) (ormap find (syntax->list #'(e1 e2 e3)))] - [(letrec-values ([(v ...) e] ...) b) - (ormap find (syntax->list #'(e ... b)))] - [(letrec-syntaxes+values _ ([(v ...) e] ...) b) - (ormap find (syntax->list #'(e ... b)))] - [(begin . es) - (ormap find (syntax->list #'es))] - [(#%plain-lambda (v ...) e) - (find #'e)] - [_ #f])) + (syntax-parse stx + #:literals (let-values) + [(let-values cls:lv-clauses body) + (or (ormap match? (syntax->list #'cls)) + (find #'body))] + [e:core-expr + (ormap find (syntax->list #'(e.expr ...)))])) (define (check-do-make-object cl pos-args names named-args) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index 49129a13b6..133e87c649 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -5,12 +5,14 @@ (require syntax/kerncase scheme/match "signatures.ss" - (r:private type-utils type-effect-convenience union subtype parse-type type-annotation) + (r:private type-utils type-effect-convenience union subtype + parse-type type-annotation stxclass-util) (rep type-rep effect-rep) (utils tc-utils) (env lexical-env) (only-in (env type-environments) lookup current-tvars extend-env) scheme/private/class-internal + (except-in stxclass id) (only-in srfi/1 split-at)) (require (for-template scheme/base scheme/private/class-internal)) @@ -22,28 +24,23 @@ ;; return the type of a literal value ;; scheme-value -> type (define (tc-literal v-stx) - ;; find the meet of the types of a list of expressions - ;; list[syntax] -> type - (define (types-of-literals es) - (apply Un (map tc-literal es))) - (define v (syntax-e v-stx)) - (cond - [(exact-integer? v) -Integer] - [(number? v) N] - [(char? v) -Char] - [(boolean? v) (-val v)] - [(null? v) (-val null)] - [(symbol? v) (-val v)] - [(string? v) -String] - [(keyword? v) (-val v)] - [(bytes? v) -Bytes] - [(list? v) (-Tuple (map tc-literal v))] - [(vector? v) (make-Vector (types-of-literals (vector->list v)))] - [(pregexp? v) -PRegexp] - [(byte-pregexp? v) -Byte-PRegexp] - [(byte-regexp? v) -Byte-Regexp] - [(regexp? v) -Regexp] - [else Univ])) + (syntax-parse v-stx + [i:boolean (-val #'i.datum)] + [i:identifier (-val #'i.datum)] + [i:exact-integer -Integer] + [i:number N] + [i:str -String] + [i:char -Char] + [i:keyword (-val #'i.datum)] + [i:bytes -Bytes] + [i:byte-pregexp -Byte-PRegexp] + [i:byte-regexp -Byte-Regexp] + [i:regexp -Regexp] + [(i ...) + (-Tuple (map tc-literal (syntax->list #'(i ...))))] + [i #:declare i (3d vector?) + (make-Vector (apply Un (map tc-literal (vector->list #'i.datum))))] + [_ Univ])) ;; do-inst : syntax type -> type @@ -190,7 +187,6 @@ (begin (tc-exprs/check (syntax->list #'es) Univ) (tc-expr/check #'e expected))] ;; if - [(if tst body) (tc/if-onearm/check #'tst #'body expected)] [(if tst thn els) (tc/if-twoarm/check #'tst #'thn #'els expected)] ;; lambda [(#%plain-lambda formals . body) diff --git a/collects/typed-scheme/typecheck/tc-if-unit.ss b/collects/typed-scheme/typecheck/tc-if-unit.ss index bf3a4e43bb..cc87ca8b13 100644 --- a/collects/typed-scheme/typecheck/tc-if-unit.ss +++ b/collects/typed-scheme/typecheck/tc-if-unit.ss @@ -13,9 +13,6 @@ mzlib/trace mzlib/plt-match) -;; necessary for creating (#%app void) in tc-if/onearm -(require (for-template scheme/base)) - ;; if typechecking (import tc-expr^) (export tc-if^) @@ -88,12 +85,6 @@ ;; v cannot have type (-val #f) [(Var-True-Effect: v) (check-rest *remove (-val #f) v)]))))) -;; create a dummy else branch for typechecking -(define (tc/if-onearm tst body) (tc/if-twoarm tst body (syntax/loc body (#%app void)))) - -(define (tc/if-onearm/check tst body expected) - (tc/if-twoarm/check tst body (syntax/loc body (#%app void)) expected)) - ;; the main function (define (tc/if-twoarm tst thn els) #;(printf "tc-if/twoarm~n") diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss index 962c480e05..a4159fb63f 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss @@ -199,16 +199,18 @@ (cons (car bodies) bodies*) (cons (syntax-len (car formals)) nums-seen))])))) +;; tc/lambda : syntax syntax-list syntax-list -> tc-result (define (tc/lambda form formals bodies) (tc/lambda/internal form formals bodies #f)) ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic -;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> Type +;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result (define (tc/lambda/internal form formals bodies expected) (if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected)) (tc/plambda form formals bodies expected) (ret (tc/mono-lambda formals bodies expected)))) +;; tc/lambda : syntax syntax-list syntax-list Type -> tc-result (define (tc/lambda/check form formals bodies expected) (tc/lambda/internal form formals bodies expected)) diff --git a/collects/typed-scheme/utils/unit-utils.ss b/collects/typed-scheme/utils/unit-utils.ss index 728edcd193..ebec947551 100644 --- a/collects/typed-scheme/utils/unit-utils.ss +++ b/collects/typed-scheme/utils/unit-utils.ss @@ -7,7 +7,13 @@ scheme/unit-exptime scheme/match)) -(provide define-values/link-units/infer) +(provide define-values/link-units/infer cnt) + +(define-signature-form (cnt stx) + (syntax-case stx () + [(_ nm cnt) + (list #'nm) + #;(list #'[contracted (nm cnt)])])) (define-syntax (define-values/link-units/infer stx) ;; construct something we can put in the imports/exports clause from the datum diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss index bfa0e50592..f08a44ff90 100644 --- a/collects/typed-scheme/utils/utils.ss +++ b/collects/typed-scheme/utils/utils.ss @@ -3,7 +3,8 @@ (require (for-syntax scheme/base) mzlib/plt-match scheme/require-syntax - mzlib/struct) + mzlib/struct + (except-in stxclass id)) (provide with-syntax* syntax-map start-timing do-time reverse-begin printf/log with-logging-to-file log-file-name == @@ -222,3 +223,4 @@ ;; pads out t to be as long as s (define (extend s t extra) (append t (build-list (- (length s) (length t)) (lambda _ extra)))) +