resolve conflicts
svn: r14598 original commit: 1edf62a912ac0468c2a995043c58826607d645dc
This commit is contained in:
commit
ba8d0ff816
15
collects/tests/typed-scheme/fail/bad-map-poly.ss
Normal file
15
collects/tests/typed-scheme/fail/bad-map-poly.ss
Normal file
|
@ -0,0 +1,15 @@
|
|||
#;
|
||||
(exn-pred exn:fail:contract? ".*interface for bad-map.*")
|
||||
#lang scheme/load
|
||||
|
||||
(module bad-map scheme
|
||||
(provide bad-map)
|
||||
(define (bad-map f l)
|
||||
(list (f 'quux))))
|
||||
|
||||
(module use-bad-map typed-scheme
|
||||
(require/typed 'bad-map
|
||||
[bad-map (All (A B) ((A -> B) (Listof A) -> (Listof B)))])
|
||||
(bad-map add1 (list 12 13 14)))
|
||||
|
||||
(require 'use-bad-map)
|
25
collects/tests/typed-scheme/succeed/apply-dots-list.ss
Normal file
25
collects/tests/typed-scheme/succeed/apply-dots-list.ss
Normal file
|
@ -0,0 +1,25 @@
|
|||
|
||||
;; Change the lang to scheme for untyped version
|
||||
#lang typed-scheme
|
||||
|
||||
(define tests (list (list (λ() 1) 1 "test 1")
|
||||
(list (λ() 2) 2 "test 2")))
|
||||
|
||||
; Comment out the type signature when running untyped
|
||||
(: check-all (All (A ...) ((List (-> A) A String) ... A -> Void)))
|
||||
(define (check-all . tests)
|
||||
(let aux ([tests tests]
|
||||
[num-passed 0])
|
||||
(if (null? tests)
|
||||
(printf "~a tests passed.~n" num-passed)
|
||||
(let ((test (car tests)))
|
||||
(let ((actual ((car test)))
|
||||
(expected (cadr test))
|
||||
(msg (caddr test)))
|
||||
(if (equal? actual expected)
|
||||
(aux (cdr tests) (+ num-passed 1))
|
||||
(printf "Test failed: ~a. Expected ~a, got ~a.~n"
|
||||
msg expected actual)))))))
|
||||
|
||||
(apply check-all tests) ; Works in untyped, but not in typed
|
||||
(check-all (car tests) (cadr tests)) ; Works in typed or untyped
|
11
collects/tests/typed-scheme/succeed/no-bound-fl.ss
Normal file
11
collects/tests/typed-scheme/succeed/no-bound-fl.ss
Normal file
|
@ -0,0 +1,11 @@
|
|||
#lang typed-scheme
|
||||
|
||||
(: fold-left (All (a b ...) ((a b ... -> a) a (Listof b) ... -> a)))
|
||||
(define (fold-left f a . bss)
|
||||
(if (ormap null? bss)
|
||||
a
|
||||
(apply fold-left
|
||||
f
|
||||
(apply f a (map car bss))
|
||||
(map cdr bss))))
|
||||
|
|
@ -78,6 +78,10 @@
|
|||
[(All (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))]
|
||||
[(∀ (a) (Listof a)) (-poly (a) (make-Listof a))]
|
||||
[(∀ (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))]
|
||||
[(All (a ...) (a ... -> Number))
|
||||
(-polydots (a) ((list) [a a] . ->... . N))]
|
||||
[(All (a ...) (values a ...))
|
||||
(-polydots (a) (make-ValuesDots (list) a 'a))]
|
||||
[(case-lambda (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B]
|
||||
[(N N) N])]
|
||||
[1 (-val 1)]
|
||||
|
@ -89,6 +93,8 @@
|
|||
|
||||
[a (-v a) (extend-env (list 'a) (list (-v a))
|
||||
initial-tvar-env)]
|
||||
[(All (a ...) (a ... -> Number))
|
||||
(-polydots (a) ((list) [a a] . ->... . N))]
|
||||
|
||||
))
|
||||
|
||||
|
|
3
collects/typed-scheme/env/init-envs.ss
vendored
3
collects/typed-scheme/env/init-envs.ss
vendored
|
@ -29,6 +29,9 @@
|
|||
`(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))]
|
||||
[(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
|
||||
[(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
|
||||
[(Refinement: parent pred cert) `(make-Refinement ,(sub parent)
|
||||
(quote-syntax ,pred)
|
||||
(syntax-local-certifier))]
|
||||
[(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
|
||||
[(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
|
||||
[(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]
|
||||
|
|
2
collects/typed-scheme/env/lexical-env.ss
vendored
2
collects/typed-scheme/env/lexical-env.ss
vendored
|
@ -31,7 +31,7 @@
|
|||
=>
|
||||
(lambda (a)
|
||||
(-lst (substitute Univ (cdr a) (car a))))]
|
||||
[else (lookup-fail (syntax-e i))]))))))
|
||||
[else (lookup-fail i)]))))))
|
||||
|
||||
;; refine the type of i in the lexical env
|
||||
;; (identifier type -> type) identifier -> environment
|
||||
|
|
2
collects/typed-scheme/env/type-env.ss
vendored
2
collects/typed-scheme/env/type-env.ss
vendored
|
@ -39,7 +39,7 @@
|
|||
;; given an identifier, return the type associated with it
|
||||
;; if none found, calls lookup-fail
|
||||
;; identifier -> type
|
||||
(define (lookup-type id [fail-handler (lambda () (lookup-fail (syntax-e id)))])
|
||||
(define (lookup-type id [fail-handler (lambda () (lookup-type-fail id))])
|
||||
(let ([v (module-identifier-mapping-get the-mapping id fail-handler)])
|
||||
(if (box? v) (unbox v) v)))
|
||||
|
||||
|
|
2
collects/typed-scheme/env/type-name-env.ss
vendored
2
collects/typed-scheme/env/type-name-env.ss
vendored
|
@ -35,7 +35,7 @@
|
|||
;; given an identifier, return the type associated with it
|
||||
;; optional argument is failure continuation - default calls lookup-fail
|
||||
;; identifier (-> error) -> type
|
||||
(define (lookup-type-name id [k (lambda () (lookup-fail (syntax-e id)))])
|
||||
(define (lookup-type-name id [k (lambda () (lookup-type-fail id))])
|
||||
(begin0
|
||||
(module-identifier-mapping-get the-mapping id k)
|
||||
(add-type-name-reference id)))
|
||||
|
|
|
@ -243,6 +243,9 @@
|
|||
[(a a) empty]
|
||||
[(_ (Univ:)) empty]
|
||||
|
||||
[((Refinement: S _ _) T)
|
||||
(cg S T)]
|
||||
|
||||
[((F: (? (lambda (e) (memq e X)) v)) S)
|
||||
(when (match S
|
||||
[(F: v*)
|
||||
|
|
|
@ -3,10 +3,11 @@
|
|||
(require (except-in "../utils/utils.ss" infer))
|
||||
(require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss"
|
||||
"restrict.ss" "promote-demote.ss"
|
||||
(only-in scheme/unit provide-signature-elements)
|
||||
(only-in scheme/unit provide-signature-elements
|
||||
define-values/invoke-unit/infer link)
|
||||
(utils unit-utils))
|
||||
|
||||
(provide-signature-elements restrict^ infer^)
|
||||
|
||||
(define-values/link-units/infer
|
||||
infer@ constraints@ dmap@ restrict@ promote-demote@)
|
||||
(define-values/invoke-unit/infer
|
||||
(link infer@ constraints@ dmap@ restrict@ promote-demote@))
|
||||
|
|
|
@ -418,11 +418,12 @@
|
|||
[symbol->string (Sym . -> . -String)]
|
||||
[vector-length (-poly (a) ((-vec a) . -> . -Integer))]
|
||||
|
||||
[call-with-input-file (-poly (a) (cl-> [(-String (-Port . -> . a)) a]
|
||||
[(-String (-Port . -> . a) Sym) a]))]
|
||||
[call-with-input-file (-poly (a) (-String (-Input-Port . -> . a) #:mode (Un (-val 'binary) (-val 'text)) #f . ->key . a))]
|
||||
[call-with-output-file (-poly (a) (-String (-Output-Port . -> . a)
|
||||
#:exists (one-of/c error 'append 'update 'replace 'truncate 'truncate/replace) #f
|
||||
#:mode (Un (-val 'binary) (-val 'text)) #f
|
||||
. ->key . a))]
|
||||
|
||||
[call-with-output-file (-poly (a) (cl-> [(-String (-Port . -> . a)) a]
|
||||
[(-String (-Port . -> . a) Sym) a]))]
|
||||
[current-output-port (-Param -Output-Port -Output-Port)]
|
||||
[current-error-port (-Param -Output-Port -Output-Port)]
|
||||
[current-input-port (-Param -Input-Port -Input-Port)]
|
||||
|
@ -544,11 +545,29 @@
|
|||
[list->string ((-lst -Char) . -> . -String)]
|
||||
[string->list (-String . -> . (-lst -Char))]
|
||||
[sort (-poly (a) ((-lst a) (a a . -> . B) . -> . (-lst a)))]
|
||||
[find-system-path (Sym . -> . -Path)]
|
||||
|
||||
;; scheme/cmdline
|
||||
|
||||
[parse-command-line
|
||||
(let ([mode-sym (one-of/c 'once-each 'once-any 'multi 'final 'help-labels)])
|
||||
(-polydots (b a)
|
||||
(cl->* (-Pathlike
|
||||
(Un (-lst -String) (-vec -String))
|
||||
(-lst (-pair mode-sym (-lst (-lst Univ))))
|
||||
((list Univ) [a a] . ->... . b)
|
||||
(-lst -String)
|
||||
. -> . b))))]
|
||||
|
||||
;; scheme/list
|
||||
[last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
|
||||
. -> .
|
||||
(Un (-pair a a) (-pair a (-val '())))))]
|
||||
[remove-duplicates
|
||||
(-poly (a)
|
||||
(cl->*
|
||||
((-lst a) . -> . (-lst a))
|
||||
((-lst a) (a a . -> . Univ) . -> . (-lst a))))]
|
||||
|
||||
;; scheme/tcp
|
||||
[tcp-listener? (make-pred-ty -TCP-Listener)]
|
||||
|
|
|
@ -8,7 +8,7 @@
|
|||
(utils tc-utils stxclass-util)
|
||||
syntax/stx
|
||||
stxclass stxclass/util
|
||||
(env type-environments type-name-env type-alias-env)
|
||||
(env type-environments type-name-env type-alias-env lexical-env)
|
||||
(prefix-in t: "base-types-extra.ss")
|
||||
scheme/match
|
||||
(for-template scheme/base "base-types-extra.ss"))
|
||||
|
@ -296,6 +296,13 @@
|
|||
(map list
|
||||
(map syntax-e (syntax->list #'(mname ...)))
|
||||
(map parse-type (syntax->list #'(mty ...)))))]
|
||||
[(Refinement p?)
|
||||
(and (eq? (syntax-e #'Refinement) 'Refinement)
|
||||
(identifier? #'p?))
|
||||
(match (lookup-type/lexical #'p?)
|
||||
[(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
|
||||
(make-Refinement dom #'p? (syntax-local-certifier))]
|
||||
[t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
|
||||
[(Instance t)
|
||||
(eq? (syntax-e #'Instance) 'Instance)
|
||||
(let ([v (parse-type #'t)])
|
||||
|
|
|
@ -343,7 +343,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
|
|||
(list #'struct-info
|
||||
#'maker
|
||||
#'pred
|
||||
(list #'sel ...)
|
||||
(reverse (list #'sel ...))
|
||||
(list mut ...)
|
||||
#f))))
|
||||
#,(internal #'(define-typed-struct-internal nm ([fld : ty] ...) #:type-only))
|
||||
|
@ -407,4 +407,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
|
|||
[(_ [i:id t] ...)
|
||||
(syntax/loc stx
|
||||
(begin (: i t) ...
|
||||
(provide i ...)))]))
|
||||
(provide i ...)))]))
|
||||
|
||||
(define-syntax (declare-refinement stx)
|
||||
(syntax-parse stx
|
||||
[(_ p:id)
|
||||
(quasisyntax/loc stx #,(internal #'(declare-refinement-internal p)))]))
|
|
@ -62,6 +62,8 @@
|
|||
#`(listof #,(t->c elem-ty))]
|
||||
[(? (lambda (e) (eq? t:Any-Syntax e))) #'syntax?]
|
||||
[(Base: sym cnt) cnt]
|
||||
[(Refinement: par p? cert)
|
||||
#`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
|
||||
[(Union: elems)
|
||||
(with-syntax
|
||||
([cnts (map t->c elems)])
|
||||
|
@ -100,7 +102,7 @@
|
|||
[(Pair: t1 t2)
|
||||
#`(cons/c #,(t->c t1) #,(t->c t2))]
|
||||
[(Opaque: p? cert)
|
||||
#`(flat-contract #,(cert p?))]
|
||||
#`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
|
||||
[(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
|
||||
[else (int-err "unknown var: ~a" v)])]
|
||||
[(Poly: vs (and b (Function: _)))
|
||||
|
@ -122,7 +124,8 @@
|
|||
[(Instance: _) #'(is-a?/c object%)]
|
||||
[(Class: _ _ _) #'(subclass?/c object%)]
|
||||
[(Value: '()) #'null?]
|
||||
[(Struct: _ _ _ _ #f pred? cert) (cert pred?)]
|
||||
[(Struct: _ _ _ _ #f pred? cert)
|
||||
#`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))]
|
||||
[(Syntax: (Base: 'Symbol _)) #'identifier?]
|
||||
[(Syntax: t) #`(syntax/c #,(t->c t))]
|
||||
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
|
||||
|
|
|
@ -201,7 +201,7 @@
|
|||
poly?
|
||||
pred-id
|
||||
cert)]
|
||||
[#:key (gensym)])
|
||||
[#:key #f #;(gensym)])
|
||||
|
||||
|
||||
;; v : Scheme Value
|
||||
|
@ -243,6 +243,17 @@
|
|||
;; value : Type
|
||||
(dt Hashtable ([key Type/c] [value Type/c]) [#:key 'hash])
|
||||
|
||||
;; parent : Type
|
||||
;; pred : Identifier
|
||||
;; cert : Certifier
|
||||
(dt Refinement (parent pred cert)
|
||||
[#:key (Type-key parent)]
|
||||
[#:intern (list parent (hash-id pred))]
|
||||
[#:fold-rhs (*Refinement (type-rec-id parent) pred cert)]
|
||||
[#:frees (free-vars* parent)
|
||||
(free-idxs* parent)])
|
||||
|
||||
|
||||
;; t : Type
|
||||
(dt Syntax ([t Type/c]) [#:key 'syntax])
|
||||
|
||||
|
@ -400,7 +411,7 @@
|
|||
(map sb kws))]
|
||||
[#:ValuesDots rs dty dbound
|
||||
(*ValuesDots (map sb rs)
|
||||
(sb dty)
|
||||
(sb dty)
|
||||
(if (eqv? dbound (+ count outer)) (F-n image) dbound))]
|
||||
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
|
||||
[#:PolyDots n body*
|
||||
|
|
|
@ -62,11 +62,11 @@ typed-scheme
|
|||
|
||||
There are two differences between these programs:
|
||||
|
||||
@itemize{
|
||||
@itemize[
|
||||
@item*[@elem{The Language}]{@schememodname[scheme] has been replaced by @schememodname[typed-scheme].}
|
||||
|
||||
@item*[@elem{The Type Annotation}]{We have added a type annotation
|
||||
for the @scheme[fib] function, using the @scheme[:] form.} }
|
||||
for the @scheme[fib] function, using the @scheme[:] form.} ]
|
||||
|
||||
In general, these are most of the changes that have to be made to a
|
||||
PLT Scheme program to transform it into a Typed Scheme program.
|
||||
|
|
|
@ -87,7 +87,7 @@ The following base types are parameteric in their type arguments.
|
|||
types @scheme[t ...]. This can only appear as the return type of a
|
||||
function.}
|
||||
@defform/none[v]{where @scheme[v] is a number, boolean or string, is the singleton type containing only that value}
|
||||
@defform/none['sym]{where @scheme[sym] is a symbol, is the singleton type containing only that symbol}
|
||||
@defform/none['val]{where @scheme[val] is a Scheme value, is the singleton type containing only that value}
|
||||
@defform/none[i]{where @scheme[i] is an identifier can be a reference to a type
|
||||
name or a type variable}
|
||||
@defform[(Rec n t)]{is a recursive type where @scheme[n] is bound to the
|
||||
|
@ -294,3 +294,18 @@ Other libraries can be used with Typed Scheme via
|
|||
[check-version (-> (U Symbol (Listof Any)))])
|
||||
(check-version)
|
||||
]
|
||||
|
||||
@section{Typed Scheme Syntax Without Type Checking}
|
||||
|
||||
@defmodulelang[typed-scheme/no-check]
|
||||
|
||||
On occasions where the Typed Scheme syntax is useful, but actual
|
||||
typechecking is not desired, the @schememodname[typed-scheme/no-check]
|
||||
language is useful. It provides the same bindings and syntax as Typed
|
||||
Scheme, but does no type checking.
|
||||
|
||||
Examples:
|
||||
|
||||
@schememod[typed-scheme/no-check
|
||||
(: x Number)
|
||||
(define x "not-a-number")]
|
|
@ -11,4 +11,6 @@
|
|||
define-typed-struct-internal
|
||||
define-typed-struct/exec-internal
|
||||
assert-predicate-internal
|
||||
declare-refinement-internal
|
||||
:-internal)
|
||||
|
||||
|
|
|
@ -5,7 +5,7 @@
|
|||
syntax/kerncase syntax/boundmap
|
||||
(env type-name-env type-alias-env)
|
||||
mzlib/trace
|
||||
(private type-contract)
|
||||
(private type-contract typed-renaming)
|
||||
(rep type-rep)
|
||||
(utils tc-utils)
|
||||
"def-binding.ss")
|
||||
|
@ -13,7 +13,8 @@
|
|||
(require (for-template scheme/base
|
||||
scheme/contract))
|
||||
|
||||
(provide remove-provides provide? generate-prov)
|
||||
(provide remove-provides provide? generate-prov
|
||||
get-alternate)
|
||||
|
||||
(define (provide? form)
|
||||
(kernel-syntax-case form #f
|
||||
|
@ -24,6 +25,12 @@
|
|||
(define (remove-provides forms)
|
||||
(filter (lambda (e) (not (provide? e))) (syntax->list forms)))
|
||||
|
||||
|
||||
(define (renamer id #:alt [alt #f])
|
||||
(if alt
|
||||
(make-typed-renaming (syntax-property id 'not-free-identifier=? #t) alt)
|
||||
(make-rename-transformer (syntax-property id 'not-free-identifier=? #t))))
|
||||
|
||||
(define (generate-prov stx-defs val-defs)
|
||||
(define mapping (make-free-identifier-mapping))
|
||||
(lambda (form)
|
||||
|
@ -54,35 +61,35 @@
|
|||
(define/contract cnt-id #,cnt id)
|
||||
(define-syntax export-id
|
||||
(if (unbox typed-context?)
|
||||
(make-rename-transformer (syntax-property #'id
|
||||
'not-free-identifier=? #t))
|
||||
(make-rename-transformer (syntax-property #'cnt-id
|
||||
'not-free-identifier=? #t))))
|
||||
(renamer #'id #:alt #'cnt-id)
|
||||
(renamer #'cnt-id)))
|
||||
(#%provide (rename export-id out-id)))))]
|
||||
[else
|
||||
(with-syntax ([(export-id) (generate-temporaries #'(id))])
|
||||
#`(begin
|
||||
(with-syntax ([(export-id error-id) (generate-temporaries #'(id id))])
|
||||
#`(begin
|
||||
(define-syntax error-id
|
||||
(lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id))))
|
||||
(define-syntax export-id
|
||||
(if (unbox typed-context?)
|
||||
(make-rename-transformer (syntax-property #'id
|
||||
'not-free-identifier=? #t))
|
||||
(lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
|
||||
(renamer #'id #:alt #'error-id)
|
||||
(renamer #'error-id)))
|
||||
(provide (rename-out [export-id out-id]))))])))]
|
||||
[(mem? internal-id stx-defs)
|
||||
=>
|
||||
(lambda (b)
|
||||
(with-syntax ([id internal-id]
|
||||
[out-id external-id])
|
||||
(with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))])
|
||||
#`(begin
|
||||
(with-syntax ([(export-id error-id) (generate-temporaries #'(id id))])
|
||||
#`(begin
|
||||
(define-syntax error-id
|
||||
(lambda (stx)
|
||||
(tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id))))
|
||||
(define-syntax export-id
|
||||
(if (unbox typed-context?)
|
||||
(begin
|
||||
(begin
|
||||
(add-alias #'export-id #'id)
|
||||
(make-rename-transformer (syntax-property #'id
|
||||
'not-free-identifier=? #t)))
|
||||
(lambda (stx)
|
||||
(tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
|
||||
(renamer #'id #:alt #'error-id))
|
||||
(renamer #'error-id)))
|
||||
(provide (rename-out [export-id out-id]))))))]
|
||||
[(eq? (syntax-e internal-id) (syntax-e external-id))
|
||||
#`(provide #,internal-id)]
|
||||
|
|
|
@ -576,7 +576,7 @@
|
|||
[c:lv-clause
|
||||
#:with (#%plain-app reverse n:id) #'c.e
|
||||
#:with (v) #'(c.v ...)
|
||||
#:when (free-identifier=? name #'v)
|
||||
#:when (free-identifier=? name #'n)
|
||||
(type-annotation #'v)]
|
||||
[_ #f]))
|
||||
(syntax-parse stx
|
||||
|
@ -757,8 +757,8 @@
|
|||
(match (tc-expr #'fn)
|
||||
[(tc-result: (Function: arities))
|
||||
(tc-keywords form arities (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected)]
|
||||
[t (tc-error/expr #:return (ret (Un))
|
||||
"Cannot apply expression of type ~a, since it is not a function type" t)])]
|
||||
[(tc-result: t) (tc-error/expr #:return (ret (Un))
|
||||
"Cannot apply expression of type ~a, since it is not a function type" t)])]
|
||||
;; even more special case for match
|
||||
[(#%plain-app (letrec-values ([(lp) (#%plain-lambda args . body)]) lp*) . actuals)
|
||||
(and expected (not (andmap type-annotation (syntax->list #'args))) (free-identifier=? #'lp #'lp*))
|
||||
|
|
|
@ -136,7 +136,7 @@
|
|||
(ret expected)]
|
||||
[((? Type? t1) (? Type? t2))
|
||||
(unless (subtype t1 t2)
|
||||
(tc-error/expr"Expected ~a, but got ~a" t2 t1))
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
|
||||
expected]))
|
||||
|
||||
(define (tc-expr/check form expected)
|
||||
|
|
|
@ -86,6 +86,7 @@
|
|||
(define (mk/register-sty nm flds parent parent-field-types types
|
||||
#:wrapper [wrapper values]
|
||||
#:type-wrapper [type-wrapper values]
|
||||
#:pred-wrapper [pred-wrapper values]
|
||||
#:mutable [setters? #f]
|
||||
#:proc-ty [proc-ty #f]
|
||||
#:maker [maker* #f]
|
||||
|
@ -104,6 +105,7 @@
|
|||
(register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
|
||||
#:wrapper wrapper
|
||||
#:type-wrapper type-wrapper
|
||||
#:pred-wrapper pred-wrapper
|
||||
#:maker (or maker* maker)
|
||||
#:constructor-return cret))))
|
||||
|
||||
|
@ -113,6 +115,7 @@
|
|||
(define (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
|
||||
#:wrapper [wrapper values]
|
||||
#:type-wrapper [type-wrapper values]
|
||||
#:pred-wrapper [pred-wrapper values]
|
||||
#:maker [maker* #f]
|
||||
#:constructor-return [cret #f])
|
||||
;; create the approriate names that define-struct will bind
|
||||
|
@ -125,7 +128,7 @@
|
|||
(list (cons (or maker* maker)
|
||||
(wrapper (->* external-fld-types (if cret cret name))))
|
||||
(cons pred
|
||||
(make-pred-ty (wrapper name))))
|
||||
(make-pred-ty (pred-wrapper name))))
|
||||
(map (lambda (g t) (cons g (wrapper (->* (list name) t)))) getters external-fld-types/no-parent)
|
||||
(if setters?
|
||||
(map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent)
|
||||
|
@ -167,6 +170,7 @@
|
|||
;; wrap everything in the approriate forall
|
||||
#:wrapper (lambda (t) (make-Poly tvars t))
|
||||
#:type-wrapper (lambda (t) (make-App t new-tvars #f))
|
||||
#:pred-wrapper (lambda (t) (subst-all (for/list ([t tvars]) (list t Univ)) t))
|
||||
#:poly? #t))
|
||||
|
||||
|
||||
|
|
|
@ -10,7 +10,7 @@
|
|||
(rep type-rep)
|
||||
(types utils convenience)
|
||||
(private parse-type type-annotation type-contract)
|
||||
(env type-env init-envs type-name-env type-alias-env)
|
||||
(env type-env init-envs type-name-env type-alias-env lexical-env)
|
||||
(utils tc-utils mutated-vars)
|
||||
"provide-handling.ss"
|
||||
"def-binding.ss"
|
||||
|
@ -39,6 +39,17 @@
|
|||
;; type aliases have already been handled by an earlier pass
|
||||
[(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)))
|
||||
(list)]
|
||||
|
||||
;; declare-refinement
|
||||
[(define-values () (begin (quote-syntax (declare-refinement-internal pred)) (#%plain-app values)))
|
||||
(match (lookup-type/lexical #'pred)
|
||||
[(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
|
||||
(register-type #'pred
|
||||
(make-pred-ty (list dom)
|
||||
rng
|
||||
(make-Refinement dom #'pred (syntax-local-certifier))))
|
||||
(list)]
|
||||
[t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
|
||||
|
||||
;; require/typed
|
||||
[(define-values () (begin (quote-syntax (require/typed-internal nm ty)) (#%plain-app values)))
|
||||
|
|
|
@ -3,8 +3,10 @@
|
|||
(require "../utils/utils.ss")
|
||||
(require (utils unit-utils)
|
||||
mzlib/trace
|
||||
(only-in scheme/unit provide-signature-elements)
|
||||
"signatures.ss" "tc-toplevel.ss"
|
||||
(only-in scheme/unit
|
||||
provide-signature-elements
|
||||
define-values/invoke-unit/infer link)
|
||||
"signatures.ss" "tc-toplevel.ss"
|
||||
"tc-new-if.ss" "tc-lambda-unit.ss" "tc-new-app-unit.ss"
|
||||
"tc-let-unit.ss" "tc-dots-unit.ss"
|
||||
"tc-expr-unit.ss" "check-subforms-unit.ss")
|
||||
|
|
22
collects/typed/file/tar.ss
Normal file
22
collects/typed/file/tar.ss
Normal file
|
@ -0,0 +1,22 @@
|
|||
#lang typed-scheme
|
||||
;; typed-scheme wrapper on file/tar
|
||||
;; yc 2009/2/25
|
||||
|
||||
;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; basic type aliases.
|
||||
(define-type-alias Path-String (U Path String))
|
||||
|
||||
(require/typed file/tar
|
||||
;; tar appears to return exact-nonenegative-integer? instead of void?
|
||||
[tar (Path-String Path-String * -> Integer)]
|
||||
;; tar->output appears to take (listof path) instead of (listof path-string?)
|
||||
;; it also appears to return exact-nonenegative-integer?
|
||||
[tar->output (case-lambda ((Listof Path) -> Integer)
|
||||
((Listof Path) Output-Port -> Integer))]
|
||||
;; tar->gzip
|
||||
;; missing from file/tar but available in mzlib/tar
|
||||
;; actually returns void?
|
||||
[tar-gzip (Path-String Path-String * -> Void)]
|
||||
)
|
||||
|
||||
(provide tar tar->output tar-gzip)
|
|
@ -91,23 +91,28 @@
|
|||
[char-set:ascii Char-Set]
|
||||
[char-set:empty Char-Set]
|
||||
[char-set:full Char-Set]
|
||||
[char-set-fold (All (A) ((Char A -> A) A Char-Set -> A))]
|
||||
[char-set-unfold
|
||||
(All (A)
|
||||
(case-lambda
|
||||
((A -> Any) (A -> Char) (A -> A) A -> Char-Set)
|
||||
((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set)))]
|
||||
[char-set-unfold!
|
||||
(All (A) ((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set))]
|
||||
[char-set-for-each (All (A) ((Char -> A) Char-Set -> (U A Void)))]
|
||||
[char-set-any (All (A) ((Char -> A) Char-Set -> (U A #f)))]
|
||||
[char-set-every (All (A) ((Char -> A) Char-Set -> (U A Boolean)))]
|
||||
) ; end of require/typed
|
||||
|
||||
;; Definitions provided here for polymorphism
|
||||
|
||||
(: char-set-fold (All (A) ((Char A -> A) A Char-Set -> A)))
|
||||
#;
|
||||
(define (char-set-fold comb base cs)
|
||||
(let loop ((c (char-set-cursor cs)) (b base))
|
||||
(cond [(end-of-char-set? c) b]
|
||||
[else
|
||||
(loop (char-set-cursor-next cs c)
|
||||
(comb (char-set-ref cs c) b))])))
|
||||
|
||||
(: char-set-unfold
|
||||
(All (A)
|
||||
(case-lambda
|
||||
((A -> Any) (A -> Char) (A -> A) A -> Char-Set)
|
||||
((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set))))
|
||||
#;
|
||||
(define char-set-unfold
|
||||
(pcase-lambda: (A)
|
||||
[([p : (A -> Any)] [f : (A -> Char)] [g : (A -> A)] [seed : A])
|
||||
|
@ -115,29 +120,25 @@
|
|||
[([p : (A -> Any)] [f : (A -> Char)] [g : (A -> A)] [seed : A]
|
||||
[base-cs : Char-Set])
|
||||
(char-set-unfold! p f g seed (char-set-copy base-cs))]))
|
||||
|
||||
(: char-set-unfold!
|
||||
(All (A) ((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set)))
|
||||
#;
|
||||
(define (char-set-unfold! p f g seed base-cs)
|
||||
(let lp ((seed seed) (cs base-cs))
|
||||
(if (p seed) cs ; P says we are done.
|
||||
(lp (g seed) ; Loop on (G SEED).
|
||||
(char-set-adjoin! cs (f seed))))))
|
||||
|
||||
(: char-set-for-each (All (A) ((Char -> A) Char-Set -> (U A Void))))
|
||||
#;
|
||||
(define (char-set-for-each f cs)
|
||||
(char-set-fold (lambda: ([c : Char] [b : (U A Void)]) (f c))
|
||||
(void)
|
||||
cs))
|
||||
|
||||
(: char-set-any (All (A) ((Char -> A) Char-Set -> (U A #f))))
|
||||
#;
|
||||
(define (char-set-any pred cs)
|
||||
(let loop ((c (char-set-cursor cs)))
|
||||
(and (not (end-of-char-set? c))
|
||||
(or (pred (char-set-ref cs c))
|
||||
(loop (char-set-cursor-next cs c))))))
|
||||
|
||||
(: char-set-every (All (A) ((Char -> A) Char-Set -> (U A Boolean))))
|
||||
#;
|
||||
(define (char-set-every pred cs)
|
||||
(let loop ((c (char-set-cursor cs)) (b (ann #t (U #t A))))
|
||||
(cond [(end-of-char-set? c) b]
|
||||
|
|
Loading…
Reference in New Issue
Block a user