Use more descriptive variable names.

This commit is contained in:
Vincent St-Amour 2011-05-18 14:16:06 -04:00
parent c02071b262
commit 027947eef2
4 changed files with 268 additions and 267 deletions

View File

@ -17,51 +17,51 @@
(define name-ref/c (or/c identifier? integer?)) (define name-ref/c (or/c identifier? integer?))
(define (hash-name v) (if (identifier? v) (hash-id v) (list v))) (define (hash-name v) (if (identifier? v) (hash-id v) (list v)))
(df Bot () [#:fold-rhs #:base]) (def-filter Bot () [#:fold-rhs #:base])
(df Top () [#:fold-rhs #:base]) (def-filter Top () [#:fold-rhs #:base])
(df TypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c]) (def-filter TypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
[#:intern (list t p (hash-name v))] [#:intern (list t p (hash-name v))]
[#:frees (combine-frees (map free-vars* (cons t p))) [#:frees (combine-frees (map free-vars* (cons t p)))
(combine-frees (map free-idxs* (cons t p)))] (combine-frees (map free-idxs* (cons t p)))]
[#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) [#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
(df NotTypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c]) (def-filter NotTypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
[#:intern (list t p (hash-name v))] [#:intern (list t p (hash-name v))]
[#:frees (combine-frees (map free-vars* (cons t p))) [#:frees (combine-frees (map free-vars* (cons t p)))
(combine-frees (map free-idxs* (cons t p)))] (combine-frees (map free-idxs* (cons t p)))]
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
;; implication ;; implication
(df ImpFilter ([a Filter/c] [c Filter/c])) (def-filter ImpFilter ([a Filter/c] [c Filter/c]))
(df AndFilter ([fs (non-empty-listof Filter/c)]) (def-filter AndFilter ([fs (non-empty-listof Filter/c)])
[#:fold-rhs (*AndFilter (map filter-rec-id fs))] [#:fold-rhs (*AndFilter (map filter-rec-id fs))]
[#:frees (combine-frees (map free-vars* fs)) [#:frees (combine-frees (map free-vars* fs))
(combine-frees (map free-idxs* fs))]) (combine-frees (map free-idxs* fs))])
(df OrFilter ([fs (non-empty-listof Filter/c)]) (def-filter OrFilter ([fs (non-empty-listof Filter/c)])
[#:fold-rhs (*OrFilter (map filter-rec-id fs))] [#:fold-rhs (*OrFilter (map filter-rec-id fs))]
[#:frees (combine-frees (map free-vars* fs)) [#:frees (combine-frees (map free-vars* fs))
(combine-frees (map free-idxs* fs))]) (combine-frees (map free-idxs* fs))])
(df FilterSet (thn els) (def-filter FilterSet (thn els)
[#:contract (->i ([t any/c] [#:contract (->i ([t any/c]
[e any/c]) [e any/c])
(#:syntax [stx #f]) (#:syntax [stx #f])
#:pre (t e) #:pre (t e)
(and (cond [(Bot? t) #t] (and (cond [(Bot? t) #t]
[(Bot? e) (Top? t)] [(Bot? e) (Top? t)]
[else (Filter/c-predicate? t)]) [else (Filter/c-predicate? t)])
(cond [(Bot? e) #t] (cond [(Bot? e) #t]
[(Bot? t) (Top? e)] [(Bot? t) (Top? e)]
[else (Filter/c-predicate? e)])) [else (Filter/c-predicate? e)]))
[result FilterSet?])] [result FilterSet?])]
[#:fold-rhs (*FilterSet (filter-rec-id thn) (filter-rec-id els))]) [#:fold-rhs (*FilterSet (filter-rec-id thn) (filter-rec-id els))])
;; represents no info about the filters of this expression ;; represents no info about the filters of this expression
;; should only be used for parsing type annotations and expected types ;; should only be used for parsing type annotations and expected types
(df NoFilter () [#:fold-rhs #:base]) (def-filter NoFilter () [#:fold-rhs #:base])
(define (filter-equal? a b) (= (Rep-seq a) (Rep-seq b))) (define (filter-equal? a b) (= (Rep-seq a) (Rep-seq b)))
(provide filter-equal?) (provide filter-equal?)

View File

@ -3,24 +3,24 @@
(require racket/match scheme/contract "rep-utils.rkt" "free-variance.rkt" "filter-rep.rkt") (require racket/match scheme/contract "rep-utils.rkt" "free-variance.rkt" "filter-rep.rkt")
(provide object-equal?) (provide object-equal?)
(dpe CarPE () [#:fold-rhs #:base]) (def-pathelem CarPE () [#:fold-rhs #:base])
(dpe CdrPE () [#:fold-rhs #:base]) (def-pathelem CdrPE () [#:fold-rhs #:base])
(dpe SyntaxPE () [#:fold-rhs #:base]) (def-pathelem SyntaxPE () [#:fold-rhs #:base])
;; t is always a Name (can't put that into the contract b/c of circularity) ;; t is always a Name (can't put that into the contract b/c of circularity)
(dpe StructPE ([t Type?] [idx natural-number/c]) (def-pathelem StructPE ([t Type?] [idx natural-number/c])
[#:frees (free-vars* t) (free-idxs* t)] [#:frees (free-vars* t) (free-idxs* t)]
[#:fold-rhs (*StructPE (type-rec-id t) idx)]) [#:fold-rhs (*StructPE (type-rec-id t) idx)])
(do Empty () [#:fold-rhs #:base]) (def-object Empty () [#:fold-rhs #:base])
(do Path ([p (listof PathElem?)] [v name-ref/c]) (def-object Path ([p (listof PathElem?)] [v name-ref/c])
[#:intern (list p (hash-name v))] [#:intern (list p (hash-name v))]
[#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))] [#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
[#:fold-rhs (*Path (map pathelem-rec-id p) v)]) [#:fold-rhs (*Path (map pathelem-rec-id p) v)])
;; represents no info about the object of this expression ;; represents no info about the object of this expression
;; should only be used for parsing type annotations and expected types ;; should only be used for parsing type annotations and expected types
(do NoObject () [#:fold-rhs #:base]) (def-object NoObject () [#:fold-rhs #:base])
(define (object-equal? o1 o2) (= (Rep-seq o1) (Rep-seq o2))) (define (object-equal? o1 o2) (= (Rep-seq o1) (Rep-seq o2)))

View File

@ -226,10 +226,10 @@
'(i.kw ...))) '(i.kw ...)))
(list i.ht ...))))))])) (list i.ht ...))))))]))
(make-prim-type [Type dt #:Type type-case print-type* type-name-ht type-rec-id #:key] (make-prim-type [Type def-type #:Type type-case print-type* type-name-ht type-rec-id #:key]
[Filter df #:Filter filter-case print-filter* filter-name-ht filter-rec-id] [Filter def-filter #:Filter filter-case print-filter* filter-name-ht filter-rec-id]
[Object do #:Object object-case print-object* object-name-ht object-rec-id] [Object def-object #:Object object-case print-object* object-name-ht object-rec-id]
[PathElem dpe #:PathElem pathelem-case print-pathelem* pathelem-name-ht pathelem-rec-id]) [PathElem def-pathelem #:PathElem pathelem-case print-pathelem* pathelem-name-ht pathelem-rec-id])
(provide PathElem? (rename-out [Rep-seq Type-seq] (provide PathElem? (rename-out [Rep-seq Type-seq]
[Rep-free-vars free-vars*] [Rep-free-vars free-vars*]

View File

@ -26,7 +26,7 @@
;; Type is defined in rep-utils.rkt ;; Type is defined in rep-utils.rkt
;; t must be a Type ;; t must be a Type
(dt Scope ([t (or/c Type/c Scope?)]) [#:key (Type-key t)]) (def-type Scope ([t (or/c Type/c Scope?)]) [#:key (Type-key t)])
(define (scope-depth k) (define (scope-depth k)
(flat-named-contract (flat-named-contract
@ -39,29 +39,29 @@
(f k sc)))) (f k sc))))
;; this is ONLY used when a type error ocurrs ;; this is ONLY used when a type error ocurrs
(dt Error () [#:frees #f] [#:fold-rhs #:base]) (def-type Error () [#:frees #f] [#:fold-rhs #:base])
;; de Bruijn indexes - should never appear outside of this file ;; de Bruijn indexes - should never appear outside of this file
;; bound type variables ;; bound type variables
;; i is an nat ;; i is an nat
(dt B ([i natural-number/c]) [#:frees #f] [#:fold-rhs #:base]) (def-type B ([i natural-number/c]) [#:frees #f] [#:fold-rhs #:base])
;; free type variables ;; free type variables
;; n is a Name ;; n is a Name
(dt F ([n symbol?]) [#:frees (make-immutable-hasheq (list (cons n Covariant))) #hasheq()] [#:fold-rhs #:base]) (def-type F ([n symbol?]) [#:frees (make-immutable-hasheq (list (cons n Covariant))) #hasheq()] [#:fold-rhs #:base])
;; id is an Identifier ;; id is an Identifier
(dt Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base]) (def-type Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
;; rator is a type ;; rator is a type
;; rands is a list of types ;; rands is a list of types
;; stx is the syntax of the pair of parens ;; stx is the syntax of the pair of parens
(dt App ([rator Type/c] [rands (listof Type/c)] [stx (or/c #f syntax?)]) (def-type App ([rator Type/c] [rands (listof Type/c)] [stx (or/c #f syntax?)])
[#:intern (list rator rands)] [#:intern (list rator rands)]
[#:frees (λ (f) (combine-frees (map f (cons rator rands))))] [#:frees (λ (f) (combine-frees (map f (cons rator rands))))]
[#:fold-rhs (*App (type-rec-id rator) [#:fold-rhs (*App (type-rec-id rator)
(map type-rec-id rands) (map type-rec-id rands)
stx)]) stx)])
(define (get-variances t num-rands) (define (get-variances t num-rands)
(match t (match t
@ -90,53 +90,54 @@
[(Contravariant) (flip-variances tbl)])) [(Contravariant) (flip-variances tbl)]))
;; left and right are Types ;; left and right are Types
(dt Pair ([left Type/c] [right Type/c]) [#:key 'pair]) (def-type Pair ([left Type/c] [right Type/c]) [#:key 'pair])
;; dotted list -- after expansion, becomes normal Pair-based list type ;; dotted list -- after expansion, becomes normal Pair-based list type
(dt ListDots ([dty Type/c] [dbound (or/c symbol? natural-number/c)]) (def-type ListDots ([dty Type/c] [dbound (or/c symbol? natural-number/c)])
[#:frees (if (symbol? dbound) [#:frees (if (symbol? dbound)
(hash-remove (free-vars* dty) dbound) (hash-remove (free-vars* dty) dbound)
(free-vars* dty)) (free-vars* dty))
(if (symbol? dbound) (if (symbol? dbound)
(combine-frees (list (make-immutable-hasheq (list (cons dbound Covariant))) (free-idxs* dty))) (combine-frees (list (make-immutable-hasheq (list (cons dbound Covariant))) (free-idxs* dty)))
(free-idxs* dty))] (free-idxs* dty))]
[#:fold-rhs (*ListDots (type-rec-id dty) dbound)]) [#:fold-rhs (*ListDots (type-rec-id dty) dbound)])
;; *mutable* pairs - distinct from regular pairs ;; *mutable* pairs - distinct from regular pairs
;; left and right are Types ;; left and right are Types
(dt MPair ([left Type/c] [right Type/c]) (def-type MPair ([left Type/c] [right Type/c])
[#:frees (λ (f) (make-invariant (combine-frees (list (f left) (f right)))))] [#:frees (λ (f) (make-invariant (combine-frees (list (f left) (f right)))))]
[#:key 'mpair]) [#:key 'mpair])
;; elem is a Type ;; elem is a Type
(dt Vector ([elem Type/c]) (def-type Vector ([elem Type/c])
[#:frees (λ (f) (make-invariant (f elem)))] [#:frees (λ (f) (make-invariant (f elem)))]
[#:key 'vector]) [#:key 'vector])
;; elems are all Types ;; elems are all Types
(dt HeterogenousVector ([elems (listof Type/c)]) (def-type HeterogenousVector ([elems (listof Type/c)])
[#:frees (λ (f) (make-invariant (combine-frees (map f elems))))] [#:frees (λ (f) (make-invariant (combine-frees (map f elems))))]
[#:key 'vector] [#:key 'vector]
[#:fold-rhs (*HeterogenousVector (map type-rec-id elems))]) [#:fold-rhs (*HeterogenousVector (map type-rec-id elems))])
;; elem is a Type ;; elem is a Type
(dt Box ([elem Type/c]) (def-type Box ([elem Type/c])
[#:frees (λ (f) (make-invariant (f elem)))] [#:frees (λ (f) (make-invariant (f elem)))]
[#:key 'box]) [#:key 'box])
;; elem is a Type ;; elem is a Type
(dt Channel ([elem Type/c]) (def-type Channel ([elem Type/c])
[#:frees (λ (f) (make-invariant (f elem)))] [#:frees (λ (f) (make-invariant (f elem)))]
[#:key 'channel]) [#:key 'channel])
;; elem is a Type ;; elem is a Type
(dt Ephemeron ([elem Type/c]) (def-type Ephemeron ([elem Type/c])
[#:key 'ephemeron]) [#:key 'ephemeron])
;; elem is a Type ;; elem is a Type
(dt Set ([elem Type/c]) [#:key 'set]) (def-type Set ([elem Type/c])
[#:key 'set])
;; name is a Symbol (not a Name) ;; name is a Symbol (not a Name)
@ -147,130 +148,130 @@
;; marshaled has to be a syntax object that refers to the base type ;; marshaled has to be a syntax object that refers to the base type
;; being created. this allows us to avoid reconstructing the base type ;; being created. this allows us to avoid reconstructing the base type
;; when using it from its marshaled representation ;; when using it from its marshaled representation
(dt Base ([name symbol?] [contract syntax?] [predicate procedure?] [marshaled syntax?]) (def-type Base ([name symbol?] [contract syntax?] [predicate procedure?] [marshaled syntax?])
[#:frees #f] [#:fold-rhs #:base] [#:intern name] [#:frees #f] [#:fold-rhs #:base] [#:intern name]
[#:key (case name [#:key (case name
[(Number Integer) 'number] [(Number Integer) 'number]
[(Boolean) 'boolean] [(Boolean) 'boolean]
[(String) 'string] [(String) 'string]
[(Symbol) 'symbol] [(Symbol) 'symbol]
[(Keyword) 'keyword] [(Keyword) 'keyword]
[else #f])]) [else #f])])
;; body is a Scope ;; body is a Scope
(dt Mu ([body (scope-depth 1)]) #:no-provide [#:frees (λ (f) (f body))] (def-type Mu ([body (scope-depth 1)]) #:no-provide [#:frees (λ (f) (f body))]
[#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))] [#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))]
[#:key (Type-key body)]) [#:key (Type-key body)])
;; n is how many variables are bound here ;; n is how many variables are bound here
;; body is a Scope ;; body is a Scope
(dt Poly (n body) #:no-provide (def-type Poly (n body) #:no-provide
[#:contract (->i ([n natural-number/c] [#:contract (->i ([n natural-number/c]
[body (n) (scope-depth n)]) [body (n) (scope-depth n)])
(#:syntax [stx (or/c #f syntax?)]) (#:syntax [stx (or/c #f syntax?)])
[result Poly?])] [result Poly?])]
[#:frees (λ (f) (f body))] [#:frees (λ (f) (f body))]
[#:fold-rhs (let ([body* (remove-scopes n body)]) [#:fold-rhs (let ([body* (remove-scopes n body)])
(*Poly n (add-scopes n (type-rec-id body*))))] (*Poly n (add-scopes n (type-rec-id body*))))]
[#:key (Type-key body)]) [#:key (Type-key body)])
;; n is how many variables are bound here ;; n is how many variables are bound here
;; there are n-1 'normal' vars and 1 ... var ;; there are n-1 'normal' vars and 1 ... var
;; body is a Scope ;; body is a Scope
(dt PolyDots (n body) #:no-provide (def-type PolyDots (n body) #:no-provide
[#:contract (->i ([n natural-number/c] [#:contract (->i ([n natural-number/c]
[body (n) (scope-depth n)]) [body (n) (scope-depth n)])
(#:syntax [stx (or/c #f syntax?)]) (#:syntax [stx (or/c #f syntax?)])
[result PolyDots?])] [result PolyDots?])]
[#:key (Type-key body)] [#:key (Type-key body)]
[#:frees (λ (f) (f body))] [#:frees (λ (f) (f body))]
[#:fold-rhs (let ([body* (remove-scopes n body)]) [#:fold-rhs (let ([body* (remove-scopes n body)])
(*PolyDots n (add-scopes n (type-rec-id body*))))]) (*PolyDots n (add-scopes n (type-rec-id body*))))])
;; pred : identifier ;; pred : identifier
;; cert : syntax certifier ;; cert : syntax certifier
(dt Opaque ([pred identifier?] [cert procedure?]) (def-type Opaque ([pred identifier?] [cert procedure?])
[#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred]) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred])
;; kw : keyword? ;; kw : keyword?
;; ty : Type ;; ty : Type
;; required? : Boolean ;; required? : Boolean
(dt Keyword ([kw keyword?] [ty Type/c] [required? boolean?]) (def-type Keyword ([kw keyword?] [ty Type/c] [required? boolean?])
[#:frees (λ (f) (f ty))] [#:frees (λ (f) (f ty))]
[#:fold-rhs (*Keyword kw (type-rec-id ty) required?)]) [#:fold-rhs (*Keyword kw (type-rec-id ty) required?)])
(dt Result ([t Type/c] [f FilterSet?] [o Object?]) (def-type Result ([t Type/c] [f FilterSet?] [o Object?])
[#:frees (λ (frees) (combine-frees (map frees (list t f o))))] [#:frees (λ (frees) (combine-frees (map frees (list t f o))))]
[#:fold-rhs (*Result (type-rec-id t) (filter-rec-id f) (object-rec-id o))]) [#:fold-rhs (*Result (type-rec-id t) (filter-rec-id f) (object-rec-id o))])
(dt Values ([rs (listof Result?)]) (def-type Values ([rs (listof Result?)])
[#:frees (λ (f) (combine-frees (map f rs)))] [#:frees (λ (f) (combine-frees (map f rs)))]
[#:fold-rhs (*Values (map type-rec-id rs))]) [#:fold-rhs (*Values (map type-rec-id rs))])
(dt ValuesDots ([rs (listof Result?)] [dty Type/c] [dbound (or/c symbol? natural-number/c)]) (def-type ValuesDots ([rs (listof Result?)] [dty Type/c] [dbound (or/c symbol? natural-number/c)])
[#:frees (if (symbol? dbound) [#:frees (if (symbol? dbound)
(hash-remove (combine-frees (map free-vars* (cons dty rs))) dbound) (hash-remove (combine-frees (map free-vars* (cons dty rs))) dbound)
(combine-frees (map free-vars* (cons dty rs)))) (combine-frees (map free-vars* (cons dty rs))))
(if (symbol? dbound) (if (symbol? dbound)
(combine-frees (cons (make-immutable-hasheq (list (cons dbound Covariant))) (combine-frees (cons (make-immutable-hasheq (list (cons dbound Covariant)))
(map free-idxs* (cons dty rs)))) (map free-idxs* (cons dty rs))))
(combine-frees (map free-idxs* (cons dty rs))))] (combine-frees (map free-idxs* (cons dty rs))))]
[#:fold-rhs (*ValuesDots (map type-rec-id rs) (type-rec-id dty) dbound)]) [#:fold-rhs (*ValuesDots (map type-rec-id rs) (type-rec-id dty) dbound)])
;; arr is NOT a Type ;; arr is NOT a Type
(dt arr ([dom (listof Type/c)] (def-type arr ([dom (listof Type/c)]
[rng (or/c Values? ValuesDots?)] [rng (or/c Values? ValuesDots?)]
[rest (or/c #f Type/c)] [rest (or/c #f Type/c)]
[drest (or/c #f (cons/c Type/c (or/c natural-number/c symbol?)))] [drest (or/c #f (cons/c Type/c (or/c natural-number/c symbol?)))]
[kws (listof Keyword?)]) [kws (listof Keyword?)])
[#:intern (list dom rng rest drest kws)] [#:intern (list dom rng rest drest kws)]
[#:frees (combine-frees [#:frees (combine-frees
(append (map (compose flip-variances free-vars*) (append (map (compose flip-variances free-vars*)
(append (if rest (list rest) null) (append (if rest (list rest) null)
(map Keyword-ty kws) (map Keyword-ty kws)
dom)) dom))
(match drest (match drest
[(cons t (? symbol? bnd)) [(cons t (? symbol? bnd))
(list (hash-remove (flip-variances (free-vars* t)) bnd))] (list (hash-remove (flip-variances (free-vars* t)) bnd))]
[(cons t _) [(cons t _)
(list (flip-variances (free-vars* t)))] (list (flip-variances (free-vars* t)))]
[_ null]) [_ null])
(list (free-vars* rng)))) (list (free-vars* rng))))
(combine-frees (combine-frees
(append (map (compose flip-variances free-idxs*) (append (map (compose flip-variances free-idxs*)
(append (if rest (list rest) null) (append (if rest (list rest) null)
(map Keyword-ty kws) (map Keyword-ty kws)
dom)) dom))
(match drest (match drest
[(cons t (? symbol? bnd)) [(cons t (? symbol? bnd))
(list (make-immutable-hasheq (list (cons bnd Contravariant))) (list (make-immutable-hasheq (list (cons bnd Contravariant)))
(flip-variances (free-idxs* t)))] (flip-variances (free-idxs* t)))]
[(cons t _) [(cons t _)
(list (flip-variances (free-idxs* t)))] (list (flip-variances (free-idxs* t)))]
[_ null]) [_ null])
(list (free-idxs* rng))))] (list (free-idxs* rng))))]
[#:fold-rhs (*arr (map type-rec-id dom) [#:fold-rhs (*arr (map type-rec-id dom)
(type-rec-id rng) (type-rec-id rng)
(and rest (type-rec-id rest)) (and rest (type-rec-id rest))
(and drest (cons (type-rec-id (car drest)) (cdr drest))) (and drest (cons (type-rec-id (car drest)) (cdr drest)))
(map type-rec-id kws))]) (map type-rec-id kws))])
;; top-arr is the supertype of all function types ;; top-arr is the supertype of all function types
(dt top-arr () [#:fold-rhs #:base]) (def-type top-arr () [#:fold-rhs #:base])
(define arr/c (or/c top-arr? arr?)) (define arr/c (or/c top-arr? arr?))
;; arities : Listof[arr] ;; arities : Listof[arr]
(dt Function ([arities (listof arr/c)]) (def-type Function ([arities (listof arr/c)])
[#:key 'procedure] [#:key 'procedure]
[#:frees (λ (f) (combine-frees (map f arities)))] [#:frees (λ (f) (combine-frees (map f arities)))]
[#:fold-rhs (*Function (map type-rec-id arities))]) [#:fold-rhs (*Function (map type-rec-id arities))])
(dt fld ([t Type/c] [acc identifier?] [mutable? boolean?]) (def-type fld ([t Type/c] [acc identifier?] [mutable? boolean?])
[#:frees (λ (f) (if mutable? (make-invariant (f t)) (f t)))] [#:frees (λ (f) (if mutable? (make-invariant (f t)) (f t)))]
[#:fold-rhs (*fld (type-rec-id t) acc mutable?)] [#:fold-rhs (*fld (type-rec-id t) acc mutable?)]
[#:intern (list t (hash-id acc) mutable?)]) [#:intern (list t (hash-id acc) mutable?)])
;; name : symbol ;; name : symbol
;; parent : Struct ;; parent : Struct
@ -281,128 +282,128 @@
;; cert : syntax certifier for pred-id ;; cert : syntax certifier for pred-id
;; acc-ids : names of the accessors ;; acc-ids : names of the accessors
;; maker-id : name of the constructor ;; maker-id : name of the constructor
(dt Struct ([name symbol?] (def-type Struct ([name symbol?]
[parent (or/c #f Struct? Name?)] [parent (or/c #f Struct? Name?)]
[flds (listof fld?)] [flds (listof fld?)]
[proc (or/c #f Function?)] [proc (or/c #f Function?)]
[poly? (or/c #f (listof symbol?))] [poly? (or/c #f (listof symbol?))]
[pred-id identifier?] [pred-id identifier?]
[cert procedure?] [cert procedure?]
[maker-id identifier?]) [maker-id identifier?])
[#:intern (list name parent flds proc)] [#:intern (list name parent flds proc)]
[#:frees (λ (f) (combine-frees (map f (append (if proc (list proc) null) [#:frees (λ (f) (combine-frees (map f (append (if proc (list proc) null)
(if parent (list parent) null) (if parent (list parent) null)
flds))))] flds))))]
[#:fold-rhs (*Struct name [#:fold-rhs (*Struct name
(and parent (type-rec-id parent)) (and parent (type-rec-id parent))
(map type-rec-id flds) (map type-rec-id flds)
(and proc (type-rec-id proc)) (and proc (type-rec-id proc))
poly? poly?
pred-id pred-id
cert cert
maker-id)] maker-id)]
[#:key 'struct]) [#:key 'struct])
;; A structure type descriptor ;; A structure type descriptor
;; s : struct ;; s : struct
(dt StructType ([s Struct?]) [#:key 'struct-type]) (def-type StructType ([s Struct?]) [#:key 'struct-type])
;; the supertype of all of these values ;; the supertype of all of these values
(dt BoxTop () [#:fold-rhs #:base] [#:key 'box]) (def-type BoxTop () [#:fold-rhs #:base] [#:key 'box])
(dt ChannelTop () [#:fold-rhs #:base] [#:key 'channel]) (def-type ChannelTop () [#:fold-rhs #:base] [#:key 'channel])
(dt VectorTop () [#:fold-rhs #:base] [#:key 'vector]) (def-type VectorTop () [#:fold-rhs #:base] [#:key 'vector])
(dt HashtableTop () [#:fold-rhs #:base] [#:key 'hash]) (def-type HashtableTop () [#:fold-rhs #:base] [#:key 'hash])
(dt MPairTop () [#:fold-rhs #:base] [#:key 'mpair]) (def-type MPairTop () [#:fold-rhs #:base] [#:key 'mpair])
(dt StructTop ([name Struct?]) [#:key 'struct]) (def-type StructTop ([name Struct?]) [#:key 'struct])
;; v : Scheme Value ;; v : Scheme Value
(dt Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number] (def-type Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number]
[(boolean? v) 'boolean] [(boolean? v) 'boolean]
[(null? v) 'null] [(null? v) 'null]
[else #f])]) [else #f])])
;; elems : Listof[Type] ;; elems : Listof[Type]
(dt Union ([elems (and/c (listof Type/c) (def-type Union ([elems (and/c (listof Type/c)
(lambda (es) (lambda (es)
(or (null? es) (or (null? es)
(let-values ([(sorted? k) (let-values ([(sorted? k)
(for/fold ([sorted? #t] (for/fold ([sorted? #t]
[last (car es)]) [last (car es)])
([e (cdr es)]) ([e (cdr es)])
(values (values
(and sorted? (type<? last e)) (and sorted? (type<? last e))
e))]) e))])
sorted?))))]) sorted?))))])
[#:frees (λ (f) (combine-frees (map f elems)))] [#:frees (λ (f) (combine-frees (map f elems)))]
[#:fold-rhs ((get-union-maker) (map type-rec-id elems))] [#:fold-rhs ((get-union-maker) (map type-rec-id elems))]
[#:key (let loop ([res null] [ts elems]) [#:key (let loop ([res null] [ts elems])
(if (null? ts) res (if (null? ts) res
(let ([k (Type-key (car ts))]) (let ([k (Type-key (car ts))])
(cond [(pair? k) (loop (append k res) (cdr ts))] (cond [(pair? k) (loop (append k res) (cdr ts))]
[k (loop (cons k res) (cdr ts))] [k (loop (cons k res) (cdr ts))]
[else #f]))))]) [else #f]))))])
(dt Univ () [#:frees #f] [#:fold-rhs #:base]) (def-type Univ () [#:frees #f] [#:fold-rhs #:base])
;; in : Type ;; in : Type
;; out : Type ;; out : Type
(dt Param ([in Type/c] [out Type/c]) (def-type Param ([in Type/c] [out Type/c])
[#:key 'parameter] [#:key 'parameter]
[#:frees (λ (f) (combine-frees (list (f out) (flip-variances (f in)))))]) [#:frees (λ (f) (combine-frees (list (f out) (flip-variances (f in)))))])
;; key : Type ;; key : Type
;; value : Type ;; value : Type
(dt Hashtable ([key Type/c] [value Type/c]) [#:key 'hash] (def-type Hashtable ([key Type/c] [value Type/c]) [#:key 'hash]
[#:frees (λ (f) (combine-frees (list (make-invariant (f key)) (make-invariant (f value)))))]) [#:frees (λ (f) (combine-frees (list (make-invariant (f key)) (make-invariant (f value)))))])
;; parent : Type ;; parent : Type
;; pred : Identifier ;; pred : Identifier
;; cert : Certifier ;; cert : Certifier
(dt Refinement (parent pred cert) (def-type Refinement (parent pred cert)
[#:key (Type-key parent)] [#:key (Type-key parent)]
[#:intern (list parent (hash-id pred))] [#:intern (list parent (hash-id pred))]
[#:fold-rhs (*Refinement (type-rec-id parent) pred cert)] [#:fold-rhs (*Refinement (type-rec-id parent) pred cert)]
[#:frees (λ (f) (f parent))]) [#:frees (λ (f) (f parent))])
;; t : Type ;; t : Type
(dt Syntax ([t Type/c]) [#:key 'syntax]) (def-type Syntax ([t Type/c]) [#:key 'syntax])
;; pos-flds : (Listof Type) ;; pos-flds : (Listof Type)
;; name-flds : (Listof (Tuple Symbol Type Boolean)) ;; name-flds : (Listof (Tuple Symbol Type Boolean))
;; methods : (Listof (Tuple Symbol Function)) ;; methods : (Listof (Tuple Symbol Function))
(dt Class ([pos-flds (listof Type/c)] (def-type Class ([pos-flds (listof Type/c)]
[name-flds (listof (list/c symbol? Type/c boolean?))] [name-flds (listof (list/c symbol? Type/c boolean?))]
[methods (listof (list/c symbol? Function?))]) [methods (listof (list/c symbol? Function?))])
[#:frees (λ (f) (combine-frees [#:frees (λ (f) (combine-frees
(map f (append pos-flds (map f (append pos-flds
(map cadr name-flds) (map cadr name-flds)
(map cadr methods)))))] (map cadr methods)))))]
[#:key 'class] [#:key 'class]
[#:fold-rhs (match (list pos-flds name-flds methods) [#:fold-rhs (match (list pos-flds name-flds methods)
[(list [(list
pos-tys pos-tys
(list (list init-names init-tys reqd) ___) (list (list init-names init-tys reqd) ___)
(list (list mname mty) ___)) (list (list mname mty) ___))
(*Class (*Class
(map type-rec-id pos-tys) (map type-rec-id pos-tys)
(map list (map list
init-names init-names
(map type-rec-id init-tys) (map type-rec-id init-tys)
reqd) reqd)
(map list mname (map type-rec-id mty)))])]) (map list mname (map type-rec-id mty)))])])
;; cls : Class ;; cls : Class
(dt Instance ([cls Type/c]) [#:key 'instance]) (def-type Instance ([cls Type/c]) [#:key 'instance])
;; sequences ;; sequences
;; includes lists, vectors, etc ;; includes lists, vectors, etc
;; tys : sequence produces this set of values at each step ;; tys : sequence produces this set of values at each step
(dt Sequence ([tys (listof Type/c)]) (def-type Sequence ([tys (listof Type/c)])
[#:frees (λ (f) (combine-frees (map f tys)))] [#:frees (λ (f) (combine-frees (map f tys)))]
[#:key #f] [#:fold-rhs (*Sequence (map type-rec-id tys))]) [#:key #f] [#:fold-rhs (*Sequence (map type-rec-id tys))])
(dt Future ([t Type/c]) [#:key 'future]) (def-type Future ([t Type/c]) [#:key 'future])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;