Massive cleanup of requriements in TR.

This commit is contained in:
Eric Dobson 2013-02-06 09:50:33 -08:00
parent 4fcda73adf
commit f332affa5a
35 changed files with 268 additions and 291 deletions

View File

@ -7,18 +7,15 @@
;; but split here for performance
(require "../utils/utils.rkt"
"type-env-structs.rkt"
"global-env.rkt"
"../types/kw-types.rkt"
"mvar-env.rkt"
syntax/id-table
racket/keyword-transform racket/list
(for-syntax syntax/parse syntax/parse/experimental/contract racket/base)
(only-in racket/contract ->* -> or/c any/c listof cons/c)
(for-syntax syntax/parse racket/base)
(contract-req)
(env type-env-structs global-env mvar-env)
(utils tc-utils)
(only-in (rep type-rep) Type/c)
(typecheck tc-metafunctions)
(except-in (types utils abbrev) -> ->*))
(except-in (types utils abbrev kw-types) -> ->* one-of/c))
(provide lexical-env with-lexical-env with-lexical-env/extend
with-lexical-env/extend/props update-type/lexical)

View File

@ -1,8 +1,9 @@
#lang racket/base
(require racket/contract unstable/sequence racket/dict syntax/id-table
(require unstable/sequence racket/dict syntax/id-table racket/match unstable/struct
(prefix-in r: "../utils/utils.rkt")
racket/match (r:rep filter-rep rep-utils type-rep) unstable/struct
(r:contract-req)
(r:rep filter-rep rep-utils type-rep)
(except-in (r:utils tc-utils) make-env))
(provide extend

View File

@ -1,6 +1,6 @@
#lang racket/base
(require "../utils/utils.rkt" (rep type-rep) racket/contract racket/match (for-syntax racket/base syntax/parse))
(require "../utils/utils.rkt" (rep type-rep) (contract-req) racket/match (for-syntax racket/base syntax/parse))
;; S, T types
;; X a var
@ -23,7 +23,7 @@
;; bound : var
(define-struct/cond-contract dcon-dotted ([fixed (listof c?)] [type c?] [bound symbol?]) #:transparent)
(define dcon/c (or/c dcon? dcon-exact? dcon-dotted?))
(define-for-cond-contract dcon/c (or/c dcon? dcon-exact? dcon-dotted?))
;; map : hash mapping index variables to dcons
(define-struct/cond-contract dmap ([map (hash/c symbol? dcon/c)]) #:transparent)
@ -42,5 +42,12 @@
[(_ s x t)
#'(struct c (s x t))])))
(provide (struct-out cset) (struct-out dmap) (struct-out dcon) (struct-out dcon-dotted) (struct-out dcon-exact) (struct-out c)
c: dcon/c)
(provide-for-cond-contract dcon/c)
(provide
(struct-out cset)
(struct-out dmap)
(struct-out dcon)
(struct-out dcon-dotted)
(struct-out dcon-exact)
(struct-out c)
c:)

View File

@ -2,7 +2,8 @@
(require "../utils/utils.rkt"
"signatures.rkt" "constraint-structs.rkt"
(utils tc-utils) racket/contract
(utils tc-utils)
(contract-req)
unstable/sequence unstable/hash racket/match)
(import constraints^)

View File

@ -1,6 +1,6 @@
#lang racket/unit
(require racket/require (path-up "utils/utils.rkt")
(require "../utils/utils.rkt"
(except-in
(combine-in
(utils tc-utils)
@ -13,7 +13,7 @@
"signatures.rkt"
racket/match
mzlib/etc
racket/contract
(contract-req)
unstable/sequence unstable/list unstable/hash
racket/list)

View File

@ -1,7 +1,9 @@
#lang racket/base
(require racket/unit racket/contract racket/require
"constraint-structs.rkt"
(path-up "utils/utils.rkt" "utils/unit-utils.rkt" "rep/type-rep.rkt"))
(require "../utils/utils.rkt"
racket/unit (contract-req)
(infer constraint-structs)
(utils unit-utils)
(rep type-rep))
(provide (all-defined-out))
(define-signature dmap^

View File

@ -7,7 +7,7 @@
(rename-in (types abbrev union utils printer filter-ops resolve)
[make-arr* make-arr])
(utils tc-utils stxclass-util)
syntax/stx (prefix-in c: racket/contract)
syntax/stx (prefix-in c: (contract-req))
syntax/parse racket/dict
(env type-env-structs tvar-env type-name-env type-alias-env
lexical-env index-env)
@ -28,7 +28,6 @@
[parse-tc-results/id (syntax? c:any/c . c:-> . tc-results/c)])
(provide star ddd/bound)
(define enable-mu-parsing (make-parameter #t))
(print-complex-filters? #t)
;; (Syntax -> Type) -> Syntax Any -> Syntax
@ -217,7 +216,6 @@
(add-disappeared-use #'kw)
(make-Vector (parse-type #'t))]
[((~and kw t:Rec) x:id t)
#:fail-unless (enable-mu-parsing) "Recursive types not allowed"
(let* ([var (syntax-e #'x)]
[tvar (make-F var)])
(add-disappeared-use #'kw)

View File

@ -15,7 +15,7 @@
(prefix-in t: (types abbrev numeric-tower))
(private parse-type)
racket/match unstable/match syntax/struct syntax/stx racket/syntax racket/list
(only-in racket/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
(contract-req)
(for-template racket/base racket/contract racket/set (utils any-wrap)
(prefix-in t: (types numeric-predicates))
(only-in unstable/contract sequence/c)

View File

@ -1,6 +1,7 @@
#lang racket/base
(require racket/require racket/promise
(require "../utils/utils.rkt"
racket/require racket/promise
(for-template
(except-in racket/base for for* with-handlers lambda λ define
default-continuation-prompt-tag)
@ -19,7 +20,6 @@
"env/global-env.rkt"
"env/tvar-env.rkt"
"utils/tc-utils.rkt"
"utils/utils.rkt"
"types/utils.rkt"))
(provide wt-core)

View File

@ -1,7 +1,10 @@
#lang racket/base
;;TODO use contract-req
(require "rep-utils.rkt" "free-variance.rkt" racket/contract/base)
(provide Filter/c FilterSet/c name-ref/c hash-name filter-equal?)
(define (Filter/c-predicate? e)
(and (Filter? e) (not (NoFilter? e)) (not (FilterSet? e))))
(define Filter/c (flat-named-contract 'Filter Filter/c-predicate?))
@ -11,7 +14,6 @@
'FilterSet
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
(provide Filter/c FilterSet/c name-ref/c hash-name)
(define name-ref/c (or/c identifier? integer?))
(define (hash-name v) (if (identifier? v) (hash-id v) (list v)))
@ -50,4 +52,3 @@
(def-filter NoFilter () [#:fold-rhs #:base])
(define (filter-equal? a b) (= (Rep-seq a) (Rep-seq b)))
(provide filter-equal?)

View File

@ -5,9 +5,10 @@
(require "../utils/utils.rkt")
;; TODO use contract-req
(require (utils tc-utils)
"rep-utils.rkt" "object-rep.rkt" "filter-rep.rkt" "free-variance.rkt"
racket/match ;mzlib/etc
racket/match
racket/contract
racket/lazy-require
(for-syntax racket/base syntax/parse))

View File

@ -1,15 +1,10 @@
#lang racket/base
(require (rename-in "../utils/utils.rkt" [private private-in])
racket/match (prefix-in - racket/contract)
(types utils union subtype type-table filter-ops)
(private-in parse-type type-annotation)
(rep type-rep object-rep filter-rep)
(only-in (infer infer) restrict)
(except-in (utils tc-utils stxclass-util))
(env lexical-env type-env-structs tvar-env index-env)
(except-in syntax/parse id)
(only-in srfi/1 split-at))
(require "../utils/utils.rkt"
racket/match (prefix-in - (contract-req))
(types utils union subtype filter-ops)
(utils tc-utils)
(rep type-rep object-rep filter-rep))
(provide/cond-contract
[check-below (-->d ([s (-or/c Type/c tc-results/c)] [t (-or/c Type/c tc-results/c)]) ()

View File

@ -1,6 +1,6 @@
#lang racket/base
(require racket/contract "../utils/utils.rkt" racket/struct-info)
(require "../utils/utils.rkt" (contract-req) racket/struct-info)
(define-struct binding (name) #:transparent)
(define-struct (def-binding binding) (ty) #:transparent)

View File

@ -1,7 +1,7 @@
#lang racket/base
(require "../utils/utils.rkt" syntax/parse
racket/contract
(contract-req)
(rep type-rep)
(env lexical-env)
(private type-annotation)

View File

@ -1,18 +1,15 @@
#lang racket/base
(require "../utils/utils.rkt"
unstable/list syntax/id-table racket/dict racket/syntax
racket/struct-info racket/match syntax/parse syntax/location
(only-in srfi/1/list s:member)
syntax/kerncase syntax/boundmap
(env type-name-env type-alias-env)
(only-in (private type-contract) type->contract)
"renamer.rkt"
(env type-name-env type-alias-env)
(typecheck renamer def-binding)
(rep type-rep)
(utils tc-utils)
(for-syntax syntax/parse racket/base)
racket/contract/private/provide unstable/list
syntax/id-table syntax/location racket/dict
racket/syntax racket/struct-info racket/match
"def-binding.rkt" syntax/parse
(for-template racket/base "def-export.rkt" racket/contract))
(provide remove-provides provide? generate-prov get-alternate)

View File

@ -1,7 +1,8 @@
#lang racket/base
(require racket/unit racket/contract
"../utils/utils.rkt" "../utils/unit-utils.rkt"
(rep type-rep) (types utils))
(require "../utils/utils.rkt"
racket/unit
(contract-req)
(utils unit-utils) (rep type-rep) (types utils))
(provide (all-defined-out))
(define-signature tc-expr^

View File

@ -1,12 +1,13 @@
#lang racket/base
(require racket/unit
"../../utils/utils.rkt" "../../utils/unit-utils.rkt"
syntax/parse/experimental/reflect
racket/contract
(types utils))
(provide (except-out (all-defined-out) checker/c))
"../../utils/utils.rkt"
(contract-req)
(utils unit-utils))
(require-for-cond-contract syntax/parse/experimental/reflect)
(define checker/c reified-syntax-class?)
(provide (all-defined-out))
(define-for-cond-contract checker/c reified-syntax-class?)
(define-signature tc-app-hetero^
([cond-contracted tc/app-hetero checker/c]))

View File

@ -1,25 +1,24 @@
#lang racket/base
(require (rename-in "../utils/utils.rkt" [infer infer-in]))
(require (rename-in (types subtype abbrev remove-intersect union)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(require racket/match
unstable/list
(contract-req)
(infer-in infer)
(rep type-rep filter-rep object-rep)
(utils tc-utils)
(types resolve)
(types resolve subtype remove-intersect union)
(only-in (env type-env-structs lexical-env)
env? update-type/lexical env-map env-props replace-props)
racket/contract racket/match
unstable/struct
unstable/list
"tc-metafunctions.rkt"
(for-syntax racket/base))
(rename-in (types abbrev)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(typecheck tc-metafunctions))
;(trace replace-nth)
(define/contract (update t lo)
(define/cond-contract (update t lo)
(Type/c Filter/c . -> . Type/c)
(match* ((resolve t) lo)
;; pair ops

View File

@ -2,7 +2,7 @@
(require (rename-in "../utils/utils.rkt" [private private-in])
racket/match (prefix-in - racket/contract)
racket/match (prefix-in - (contract-req))
"signatures.rkt" "tc-envops.rkt" "tc-metafunctions.rkt" "tc-subst.rkt"
"check-below.rkt" "tc-funapp.rkt" "tc-app-helper.rkt" "../types/kw-types.rkt"
(types utils abbrev numeric-tower union subtype

View File

@ -1,31 +1,20 @@
#lang racket/base
(require (rename-in "../utils/utils.rkt" [infer r:infer])
"signatures.rkt" "tc-metafunctions.rkt"
"tc-app-helper.rkt" "find-annotation.rkt"
(prefix-in c: racket/contract)
syntax/parse racket/match racket/list
;; fixme - don't need to be bound in this phase - only to make
;; syntax/parse happy
racket/bool racket/unsafe/ops
(only-in racket/private/class-internal make-object do-make-object)
(only-in '#%kernel [apply k:apply])
;; end fixme
(for-syntax syntax/parse racket/base (utils tc-utils))
(private type-annotation)
(types utils union subtype resolve abbrev type-table substitute)
racket/match
(prefix-in c: (contract-req))
(for-syntax syntax/parse racket/base)
(types utils union subtype resolve abbrev substitute)
(typecheck tc-metafunctions tc-app-helper)
(utils tc-utils)
(except-in (env type-env-structs tvar-env index-env) extend)
(rep type-rep filter-rep rep-utils)
(r:infer infer)
'#%paramz
(for-template
racket/unsafe/ops
(only-in '#%kernel [apply k:apply])
"internal-forms.rkt" racket/base racket/bool '#%paramz
(only-in racket/private/class-internal make-object do-make-object)))
(rep type-rep)
(r:infer infer))
(provide tc/funapp)
(provide/cond-contract
[tc/funapp
(syntax? (c:and/c syntax? syntax->list) tc-results/c (c:listof tc-results/c)
(c:or/c #f tc-results/c)
. c:-> . tc-results/c)])
(define-syntax (handle-clauses stx)
(syntax-parse stx
@ -42,10 +31,7 @@
#:name (and (identifier? f-stx) f-stx)
#:expected expected))))]))
(define/cond-contract (tc/funapp f-stx args-stx ftype0 argtys expected)
(syntax? (c:and/c syntax? syntax->list) tc-results/c (c:listof tc-results/c)
(c:or/c #f tc-results/c)
. c:-> . tc-results/c)
(define (tc/funapp f-stx args-stx ftype0 argtys expected)
(match* (ftype0 argtys)
;; we special-case this (no case-lambda) for improved error messages
[((tc-result1: (and t (Function: (list (and a (arr: dom (Values: _)

View File

@ -1,23 +1,17 @@
#lang racket/unit
(require (rename-in "../utils/utils.rkt" [infer r:infer])
"signatures.rkt"
"tc-metafunctions.rkt"
"tc-subst.rkt"
racket/dict
racket/list syntax/parse
syntax/id-table
racket/syntax unstable/struct syntax/stx
(rename-in racket/contract [-> -->] [->* -->*] [one-of/c -one-of/c])
(require "../utils/utils.rkt"
racket/dict racket/list syntax/parse racket/syntax syntax/stx
racket/match syntax/id-table
(contract-req)
(except-in (rep type-rep) make-arr)
(rename-in (types abbrev utils union)
(rename-in (except-in (types abbrev utils union) -> ->* one-of/c)
[make-arr* make-arr])
(private type-annotation)
(typecheck signatures tc-metafunctions tc-subst check-below)
(env type-env-structs lexical-env tvar-env index-env)
(utils tc-utils)
racket/match)
(require (for-template racket/base "internal-forms.rkt"))
(for-template racket/base "internal-forms.rkt"))
(import tc-expr^)
(export tc-lambda^)
@ -78,7 +72,7 @@
((listof identifier?)
(or/c #f identifier?) syntax? (listof Type/c) (or/c #f Type/c)
(or/c #f (cons/c Type/c symbol?)) tc-results/c
. --> .
. -> .
lam-result?)
(let* ([arg-len (length arg-list)]
[tys-len (length arg-tys)]
@ -174,7 +168,7 @@
(for/list ([arg-types (in-list new-arg-types)])
(with-lexical-env/extend
arg-list arg-types
(make lam-result
(lam-result
(map list arg-list arg-types)
null
#f
@ -213,7 +207,7 @@
(with-lexical-env/extend
(cons rest-id arg-list)
(cons (make-ListDots rest-type bound) arg-types)
(make lam-result
(lam-result
combined-args
null
#f
@ -225,7 +219,7 @@
(with-lexical-env/extend
(cons rest-id arg-list)
(cons (make-Listof rest-type) arg-types)
(make lam-result
(lam-result
combined-args
null
(list rest-id rest-type)
@ -235,7 +229,7 @@
[else
(with-lexical-env/extend
arg-list arg-types
(make lam-result
(lam-result
combined-args
null
#f
@ -337,9 +331,9 @@
;; tc/plambda syntax syntax-list syntax-list type -> Poly
;; formals and bodies must by syntax-lists
(define/cond-contract (tc/plambda form formals bodies expected)
(syntax? syntax? syntax? (or/c tc-results/c #f) . --> . Type/c)
(syntax? syntax? syntax? (or/c tc-results/c #f) . -> . Type/c)
(define/cond-contract (maybe-loop form formals bodies expected)
(syntax? syntax? syntax? tc-results/c . --> . Type/c)
(syntax? syntax? syntax? tc-results/c . -> . Type/c)
(match expected
[(tc-result1: (Function: _)) (tc/mono-lambda/type formals bodies expected)]
[(tc-result1: (or (Poly: _ _) (PolyDots: _ _)))

View File

@ -1,21 +1,18 @@
#lang racket/unit
(require (rename-in "../utils/utils.rkt" [infer r:infer])
"signatures.rkt" "tc-metafunctions.rkt" "tc-subst.rkt"
(types utils abbrev union)
(require "../utils/utils.rkt"
(only-in srfi/1/list s:member)
(except-in (types utils abbrev union) -> ->* one-of/c)
(only-in (types abbrev) (-> t:->))
(private type-annotation parse-type)
(env lexical-env type-alias-env global-env type-env-structs)
(rep type-rep filter-rep object-rep)
syntax/free-vars
racket/match (prefix-in c: racket/contract)
(except-in racket/contract -> ->* one-of/c)
(typecheck signatures tc-metafunctions tc-subst check-below)
racket/match (contract-req)
syntax/kerncase syntax/parse unstable/syntax
(for-template racket/base (typecheck internal-forms)))
(for-template
racket/base
"internal-forms.rkt"))
(require (only-in srfi/1/list s:member))
(import tc-expr^)
(export tc-let^)
@ -27,11 +24,11 @@
(ret ts (for/list ([f ts]) (make-NoFilter)) (for/list ([f ts]) (make-NoObject)))]))
(define/cond-contract (do-check expr->type namess results expected-results form exprs body clauses expected #:abstract [abstract null])
(((syntax? syntax? tc-results/c . c:-> . any/c)
(((syntax? syntax? tc-results/c . -> . any/c)
(listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c)
syntax? (listof syntax?) syntax? (listof syntax?) (or/c #f tc-results/c))
(#:abstract any/c)
. c:->* .
. ->* .
tc-results/c)
(with-cond-contract t/p ([types (listof (listof Type/c))] ; types that may contain undefined (letrec)
[expected-types (listof (listof Type/c))] ; types that may not contain undefined (what we got from the user)
@ -211,7 +208,7 @@
(syntax-parse e #:literals (#%plain-lambda)
[(#%plain-lambda () _)
#:fail-unless (and expected (syntax-property e 'typechecker:called-in-tail-position)) #f
(tc-expr/check e (ret (-> (tc-results->values expected))))]
(tc-expr/check e (ret (t:-> (tc-results->values expected))))]
[_
#:fail-unless (and expected (syntax-property e 'typechecker:called-in-tail-position)) #f
(tc-expr/check e expected)]

View File

@ -1,13 +1,11 @@
#lang racket/base
(require "../utils/utils.rkt"
(rename-in (types subtype abbrev union utils filter-ops)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(rep type-rep filter-rep object-rep rep-utils) racket/list
racket/contract racket/match unstable/match
(for-syntax racket/base))
racket/match racket/list
(except-in (types subtype abbrev union utils filter-ops)
-> ->* one-of/c)
(rep type-rep filter-rep object-rep rep-utils)
(contract-req))
(provide abstract-results)

View File

@ -1,29 +1,18 @@
#lang racket/base
(require "../utils/utils.rkt"
syntax/struct syntax/parse racket/function racket/match racket/list
racket/struct-info
(prefix-in c: (contract-req))
(rep type-rep object-rep free-variance)
(private parse-type)
(types abbrev utils union resolve substitute type-table)
(env global-env type-env-structs type-name-env tvar-env)
(utils tc-utils)
"def-binding.rkt"
syntax/kerncase
syntax/struct
syntax/parse
racket/function
racket/match
racket/list
racket/struct-info
(only-in racket/contract
listof any/c or/c
[->* c->*]
[-> c->])
(for-syntax
syntax/parse
racket/base))
(require (for-template racket/base
(typecheck def-binding)
(for-syntax syntax/parse racket/base)
(for-template racket/base
"internal-forms.rkt"))
(provide tc/struct name-of-struct d-s
@ -77,7 +66,7 @@
;; parse name field of struct, determining whether a parent struct was specified
;; syntax -> (values identifier Option[Name] Option[Struct])
(define/cond-contract (parse-parent nm/par)
(c-> syntax? (values identifier? (or/c Name? #f) (or/c Mu? Poly? Struct? #f)))
(c:-> syntax? (values identifier? (c:or/c Name? #f) (c:or/c Mu? Poly? Struct? #f)))
(syntax-parse nm/par
[v:parent
(if (attribute v.par)
@ -114,7 +103,7 @@
;; gets the fields of the parent type, if they exist
;; Option[Struct-Ty] -> Listof[Type]
(define/cond-contract (get-flds p)
(c-> (or/c Struct? #f) (listof fld?))
(c:-> (c:or/c Struct? #f) (c:listof fld?))
(match p
[(Struct: _ _ flds _ _ _) flds]
[#f null]))
@ -122,8 +111,8 @@
;; Constructs the Struct value for a structure type
;; The returned value has free type variables
(define (mk/inner-struct-type names desc parent)
(c-> struct-names? struct-desc? (or/c Struct? #f) void?)
(define/cond-contract (mk/inner-struct-type names desc parent)
(c:-> struct-names? struct-desc? (c:or/c Struct? #f) Struct?)
(let* ([this-flds (for/list ([t (in-list (struct-desc-self-fields desc))]
[g (in-list (struct-names-getters names))])
@ -139,7 +128,7 @@
;; identifier listof[identifier] type listof[fld] listof[Type] boolean ->
;; (values Type listof[Type] listof[Type])
(define/cond-contract (register-sty! sty names desc)
(c-> Struct? struct-names? struct-desc? void?)
(c:-> Struct? struct-names? struct-desc? void?)
(register-type-name (struct-names-type-name names)
(make-Poly (struct-desc-tvars desc) sty)))
@ -149,7 +138,7 @@
;; Register the approriate types to the struct bindings.
(define/cond-contract (register-struct-bindings! sty names desc si)
(c-> Struct? struct-names? struct-desc? (or/c #f struct-info?) (listof binding?))
(c:-> Struct? struct-names? struct-desc? (c:or/c #f struct-info?) (c:listof binding?))
(define tvars (struct-desc-tvars desc))
@ -301,9 +290,9 @@
;; -> void
;; FIXME - figure out how to make this lots lazier
(define/cond-contract (tc/builtin-struct nm parent fld-names tys kernel-maker)
(c-> identifier? (or/c #f identifier?) (listof identifier?)
(listof Type/c) (or/c #f identifier?)
any/c)
(c:-> identifier? (c:or/c #f identifier?) (c:listof identifier?)
(c:listof Type/c) (c:or/c #f identifier?)
c:any/c)
(define parent-type (and parent (resolve-name (make-Name parent))))
(define parent-tys (map fld-t (get-flds parent-type)))

View File

@ -1,14 +1,13 @@
#lang racket/base
(require "../utils/utils.rkt")
(require (rename-in (types subtype abbrev union utils filter-ops)
(require "../utils/utils.rkt"
racket/match
(contract-req)
(rename-in (types abbrev utils filter-ops)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(rep type-rep object-rep filter-rep rep-utils) racket/list
racket/contract racket/match unstable/match
(for-syntax racket/base)
"tc-metafunctions.rkt")
(rep type-rep object-rep filter-rep rep-utils))
(provide (all-defined-out))

View File

@ -1,34 +1,27 @@
#lang racket/base
(require (rename-in "../utils/utils.rkt" [infer r:infer])
syntax/kerncase
unstable/list racket/syntax syntax/parse
mzlib/etc racket/list
racket/match
"signatures.rkt"
"tc-structs.rkt"
"typechecker.rkt"
;; to appease syntax-parse
"internal-forms.rkt"
syntax/kerncase racket/syntax syntax/parse syntax/id-table
racket/list unstable/list racket/dict racket/match
(prefix-in c: (contract-req))
(rep type-rep free-variance)
(types utils abbrev type-table)
(private parse-type type-annotation type-contract)
(env global-env init-envs type-name-env type-alias-env lexical-env env-req mvar-env)
syntax/id-table
(utils tc-utils mutated-vars)
"provide-handling.rkt"
"def-binding.rkt"
(prefix-in c: racket/contract)
racket/dict
(typecheck provide-handling def-binding tc-structs typechecker)
;; to appease syntax-parse in the tests
(typecheck internal-forms)
syntax/location
(for-template
"internal-forms.rkt"
syntax/location
mzlib/contract
racket/base
"../env/env-req.rkt"))
(env env-req)))
(c:provide/contract
(provide/cond-contract
[type-check (syntax? . c:-> . (values syntax? syntax?))]
[tc-module (syntax? . c:-> . (values syntax? syntax?))]
[tc-toplevel-form (syntax? . c:-> . (values #f c:any/c))])

View File

@ -5,6 +5,7 @@
(for-syntax "utils/timing.rkt") ;; only for timing/debugging
;; the below requires are needed since they provide identifiers
;; that may appear in the residual program
;; TODO: figure out why this are needed here and not somewhere else
"utils/utils.rkt"
(for-syntax "utils/utils.rkt")
"utils/any-wrap.rkt" unstable/contract racket/contract/parametric)

View File

@ -1,25 +1,28 @@
#lang racket/base
(require "../utils/utils.rkt")
(require (rename-in (rep type-rep object-rep rep-utils) [make-Base make-Base*])
(utils tc-utils)
"base-abbrev.rkt" "match-expanders.rkt"
(types union numeric-tower)
(require "../utils/utils.rkt"
racket/list
racket/match
racket/function
racket/pretty
;; avoid the other dependencies of `racket/place`
'#%place
unstable/function
racket/lazy-require
(except-in racket/contract/base ->* -> one-of/c)
(prefix-in c: racket/contract/base)
(for-template racket/base racket/contract/base racket/promise racket/tcp racket/flonum racket/udp '#%place)
racket/pretty racket/udp
(prefix-in c: (contract-req))
(rename-in (rep type-rep object-rep rep-utils)
[make-Base make-Base*])
(utils tc-utils)
(types union numeric-tower)
;; Using this form so all-from-out works
"base-abbrev.rkt" "match-expanders.rkt"
(for-syntax racket/base syntax/parse racket/list)
;; for base type contracts
(for-template racket/base racket/contract/base racket/promise
racket/tcp racket/flonum racket/udp '#%place)
;; for base type predicates
racket/promise racket/tcp racket/flonum)
racket/pretty racket/udp
racket/promise racket/tcp racket/flonum
'#%place) ;; avoid the other dependencies of `racket/place`
(provide (except-out (all-defined-out) make-Base)
@ -64,7 +67,7 @@
;; convenient constructor for Values
;; (wraps arg types with Result)
(define/cond-contract (-values args)
(c:-> (listof Type/c) (or/c Type/c Values?))
(c:-> (c:listof Type/c) (c:or/c Type/c Values?))
(match args
;[(list t) t]
[_ (make-Values (for/list ([i args]) (-result i)))]))
@ -72,7 +75,7 @@
;; convenient constructor for ValuesDots
;; (wraps arg types with Result)
(define/cond-contract (-values-dots args dty dbound)
(c:-> (listof Type/c) Type/c (or/c symbol? natural-number/c)
(c:-> (c:listof Type/c) Type/c (c:or/c symbol? c:natural-number/c)
ValuesDots?)
(make-ValuesDots (for/list ([i args]) (-result i))
dty dbound))
@ -277,15 +280,14 @@
(define (-struct name parent flds [proc #f] [poly #f] [pred #'dummy])
(make-Struct name parent flds proc poly pred))
(define (asym-pred dom rng filter)
(make-Function (list (make-arr* (list dom) rng #:filters filter))))
(define/cond-contract make-pred-ty
(case-> (c:-> Type/c Type/c)
(c:-> (listof Type/c) Type/c Type/c Type/c)
(c:-> (listof Type/c) Type/c Type/c integer? Type/c)
(c:-> (listof Type/c) Type/c Type/c integer? (listof PathElem?) Type/c))
(c:case-> (c:-> Type/c Type/c)
(c:-> (c:listof Type/c) Type/c Type/c Type/c)
(c:-> (c:listof Type/c) Type/c Type/c integer? Type/c)
(c:-> (c:listof Type/c) Type/c Type/c integer? (c:listof PathElem?) Type/c))
(case-lambda
[(in out t n p)
(define xs (for/list ([(_ i) (in-indexed (in-list in))]) i))

View File

@ -1,14 +1,13 @@
#lang racket/base
(require "../utils/utils.rkt"
(rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils) (only-in (infer infer) restrict)
(only-in racket/contract [-> -->] listof)
(types union subtype utils remove-intersect abbrev)
racket/list racket/match
(for-syntax syntax/parse racket/base)
syntax/id-table racket/dict
(for-template racket/base))
racket/dict
(prefix-in c: (contract-req))
(rep type-rep filter-rep rep-utils)
(utils tc-utils)
(only-in (infer infer) restrict)
(types union subtype remove-intersect abbrev))
(provide (all-defined-out))
@ -59,7 +58,7 @@
;; props : propositions to compress
;; or? : is this an OrFilter (alternative is AndFilter)
(define/cond-contract (compact props or?)
((listof Filter/c) boolean? . --> . (listof Filter/c))
((c:listof Filter/c) boolean? . c:-> . (c:listof Filter/c))
(define tf-map (make-hash))
(define ntf-map (make-hash))
;; props: the propositions we're processing

View File

@ -1,14 +1,13 @@
#lang racket/base
(require "../utils/utils.rkt")
(require (rename-in (types numeric-predicates base-abbrev)
(require "../utils/utils.rkt"
(rename-in (types numeric-predicates base-abbrev)
[simple-Un *Un])
(rename-in (rep type-rep) [make-Base make-Base*])
racket/match
racket/function
unstable/function
(for-template racket/base racket/contract racket/flonum (types numeric-predicates)))
(for-template racket/base racket/contract/base racket/flonum (types numeric-predicates)))
(provide portable-fixnum? portable-index?
-Zero -One -PosByte -Byte -PosIndex -Index

View File

@ -6,7 +6,7 @@
(utils tc-utils)
(types utils current-seen)
racket/match
racket/contract
(contract-req)
racket/format)
(provide resolve-name resolve-app needs-resolving?
@ -18,7 +18,7 @@
(define (resolve-name t)
(match t
[(Name: n) (let ([t (lookup-type-name n)])
(if (Type/c t) t #f))]
(if (Type/c? t) t #f))]
[_ (int-err "resolve-name: not a name ~a" t)]))
(define already-resolving? (make-parameter #f))

View File

@ -1,20 +1,21 @@
#lang racket/base
(require "../utils/utils.rkt"
racket/match racket/set racket/function unstable/function
racket/lazy-require
(contract-req)
(only-in (types base-abbrev) -lst* -result)
(rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
(rep free-variance)
(env index-env tvar-env)
(only-in (types base-abbrev) -lst* -result)
racket/match
racket/set
racket/contract
racket/lazy-require)
(env index-env tvar-env))
(lazy-require ("union.rkt" (Un)))
(provide subst-all substitute substitute-dots substitute-dotted subst
(struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted)
substitution/c make-simple-substitution)
(struct-out t-subst) (struct-out i-subst)
(struct-out i-subst/starred) (struct-out i-subst/dotted)
make-simple-substitution)
(provide-for-cond-contract substitution/c)
(define-struct/cond-contract subst-rhs () #:transparent)
(define-struct/cond-contract (t-subst subst-rhs) ([type Type/c]) #:transparent)
@ -22,8 +23,8 @@
(define-struct/cond-contract (i-subst/starred subst-rhs) ([types (listof Type/c)] [starred Type/c]) #:transparent)
(define-struct/cond-contract (i-subst/dotted subst-rhs) ([types (listof Type/c)] [dty Type/c] [dbound symbol?]) #:transparent)
(define substitution/c (hash/c symbol? subst-rhs? #:immutable #t))
(define simple-substitution/c (hash/c symbol? Type/c #:immutable #t))
(define-for-cond-contract substitution/c (hash/c symbol? subst-rhs? #:immutable #t))
(define-for-cond-contract simple-substitution/c (hash/c symbol? Type/c #:immutable #t))
(define (subst v t e) (substitute t v e))
@ -66,13 +67,13 @@
(map sb kws))])]
[#:ValuesDots types dty dbound
(cond
[(ormap (and/c dbound (not/c bound-tvar?)) names) =>
[(ormap (lambda (x) (and (equal? dbound x) (not bound-tvar? x))) names) =>
(lambda (name)
(int-err "substitute used on ... variable ~a in type ~a" name target))]
[else (make-ValuesDots (map sb types) (sb dty) dbound)])]
[#:ListDots dty dbound
(cond
[(ormap (and/c dbound (not/c bound-tvar?)) names) =>
[(ormap (lambda (x) (and (equal? dbound x) (not bound-tvar? x))) names) =>
(lambda (name)
(int-err "substitute used on ... variable ~a in type ~a" name target))]
[else (make-ListDots (sb dty) dbound)])])

View File

@ -1,15 +1,11 @@
#lang racket/base
(require (except-in "../utils/utils.rkt" infer)
racket/match unstable/match racket/function racket/lazy-require racket/list
(prefix-in c: (contract-req))
(rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
(types utils resolve base-abbrev match-expanders
numeric-tower substitute current-seen)
(env type-name-env)
racket/match unstable/match
racket/function
racket/list
racket/lazy-require
(prefix-in c: racket/contract)
(for-syntax racket/base syntax/parse))
(lazy-require

View File

@ -97,7 +97,10 @@ at least theoretically.
define-struct/cond-contract
define/cond-contract
contract-req
define/cond-contract/provide)
define/cond-contract/provide
define-for-cond-contract
provide-for-cond-contract
require-for-cond-contract)
(define-require-syntax contract-req
(if enable-contracts?
@ -105,6 +108,25 @@ at least theoretically.
(syntax-rules ()
[(_) (combine-in)])))
(define-syntax define-for-cond-contract
(if enable-contracts?
(make-rename-transformer #'define)
(syntax-parser
[(_ args:expr body:expr) #'(begin)])))
(define-syntax provide-for-cond-contract
(if enable-contracts?
(make-rename-transformer #'provide)
(syntax-parser
[(_ provide-spec:expr ...) #'(begin)])))
(define-syntax require-for-cond-contract
(if enable-contracts?
(make-rename-transformer #'require)
(syntax-parser
[(_ require-spec:expr ...) #'(begin)])))
(define-syntax-rule (define/cond-contract/provide (name . args) c . body)
(begin (define/cond-contract name c
(begin