contracts on types and effects
svn: r13685 original commit: 14475467b2c7b84d240b48fb3cc62f4d31a484bf
This commit is contained in:
Sam Tobin-Hochstadt
parent
1c96929eea
commit
ab20aa8d85
|
|
@ -57,7 +57,7 @@
|
|||
[eqv? (-> Univ Univ B)]
|
||||
[equal? (-> Univ Univ B)]
|
||||
[even? (-> N B)]
|
||||
[assert (-poly (a) (-> (*Un a (-val #f)) a))]
|
||||
[assert (-poly (a) (-> (Un a (-val #f)) a))]
|
||||
[gensym (cl-> [(Sym) Sym]
|
||||
[() Sym])]
|
||||
[string-append (->* null -String -String)]
|
||||
|
|
@ -251,8 +251,8 @@
|
|||
. -> .
|
||||
(-values (list (-pair b (-val '())) N N N))))]
|
||||
|
||||
[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
|
||||
[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (*Un a b)))]
|
||||
[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
|
||||
[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
|
||||
|
||||
[quotient (-Integer -Integer . -> . -Integer)]
|
||||
[remainder (-Integer -Integer . -> . -Integer)]
|
||||
|
|
@ -276,9 +276,9 @@
|
|||
(let ([?outp (-opt -Output-Port)]
|
||||
[?N (-opt N)]
|
||||
[optlist (lambda (t) (-opt (-lst (-opt t))))]
|
||||
[-StrRx (*Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (*Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (*Un -Input-Port -Bytes)])
|
||||
[-StrRx (Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (Un -Input-Port -Bytes)])
|
||||
(cl-> [(-StrRx -String ) (optlist -String)]
|
||||
[(-StrRx -String N ) (optlist -String)]
|
||||
[(-StrRx -String N ?N ) (optlist -String)]
|
||||
|
|
@ -294,9 +294,9 @@
|
|||
|
||||
[regexp-match*
|
||||
(let ([?N (-opt N)]
|
||||
[-StrRx (*Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (*Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (*Un -Input-Port -Bytes)])
|
||||
[-StrRx (Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (Un -Input-Port -Bytes)])
|
||||
(cl->*
|
||||
(-StrRx -String [N ?N] . ->opt . (-lst -String))
|
||||
(-BtsRx -String [N ?N] . ->opt . (-lst -Bytes))
|
||||
|
|
@ -315,17 +315,17 @@
|
|||
(let ([?outp (-opt -Output-Port)]
|
||||
[?N (-opt N)]
|
||||
[optlist (lambda (t) (-opt (-lst (-opt t))))]
|
||||
[-StrRx (*Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (*Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (*Un -Input-Port -Bytes)])
|
||||
[-StrRx (Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (Un -Input-Port -Bytes)])
|
||||
(->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))]
|
||||
[regexp-match-positions*
|
||||
(let ([?outp (-opt -Output-Port)]
|
||||
[?N (-opt N)]
|
||||
[optlist (lambda (t) (-opt (-lst (-opt t))))]
|
||||
[-StrRx (*Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (*Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (*Un -Input-Port -Bytes)])
|
||||
[-StrRx (Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (Un -Input-Port -Bytes)])
|
||||
(->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (-lst (-pair -Nat -Nat))))]
|
||||
#;
|
||||
[regexp-match-peek-positions*]
|
||||
|
|
@ -443,8 +443,8 @@
|
|||
[hash-map (-poly (a b c) ((-HT a b) (a b . -> . c) . -> . (-lst c)))]
|
||||
[hash-ref (-poly (a b c)
|
||||
(cl-> [((-HT a b) a) b]
|
||||
[((-HT a b) a (-> c)) (*Un b c)]
|
||||
[((-HT a b) a c) (*Un b c)]))]
|
||||
[((-HT a b) a (-> c)) (Un b c)]
|
||||
[((-HT a b) a c) (Un b c)]))]
|
||||
#;[hash-table-index (-poly (a b) ((-HT a b) a b . -> . -Void))]
|
||||
|
||||
[bytes (->* (list) N -Bytes)]
|
||||
|
|
@ -464,7 +464,7 @@
|
|||
[force (-poly (a) (-> (-Promise a) a))]
|
||||
[bytes<? (->* (list -Bytes) -Bytes B)]
|
||||
[regexp-replace*
|
||||
(cl->* (-Pattern (*Un -Bytes -String) (*Un -Bytes -String) . -> . -Bytes)
|
||||
(cl->* (-Pattern (Un -Bytes -String) (Un -Bytes -String) . -> . -Bytes)
|
||||
(-Pattern -String -String . -> . -String))]
|
||||
[peek-char
|
||||
(cl->* [-> -Char]
|
||||
|
|
@ -503,7 +503,7 @@
|
|||
|
||||
[delete-file (-> -Pathlike -Void)]
|
||||
[make-namespace (cl->* (-> -Namespace)
|
||||
(-> (*Un (-val 'empty) (-val 'initial)) -Namespace))]
|
||||
(-> (Un (-val 'empty) (-val 'initial)) -Namespace))]
|
||||
[make-base-namespace (-> -Namespace)]
|
||||
[eval (-> -Sexp Univ)]
|
||||
|
||||
|
|
|
|||
|
|
@ -179,8 +179,8 @@
|
|||
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
|
||||
|
||||
(define -lst make-Listof)
|
||||
(define -Sexp (-mu x (*Un Sym N B -String (-val null) (-pair x x))))
|
||||
(define -Port (*Un -Input-Port -Output-Port))
|
||||
(define -Sexp (-mu x (*Un N B Sym -String (-val null) (-pair x x))))
|
||||
(define -Port (*Un -Output-Port -Input-Port))
|
||||
|
||||
(define (-lst* #:tail [tail (-val null)] . args)
|
||||
(if (null? args)
|
||||
|
|
@ -199,9 +199,9 @@
|
|||
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
|
||||
[(t) (make-pred-ty (list Univ) B t)]))
|
||||
|
||||
(define -Pathlike (*Un -Path -String))
|
||||
(define -Pathlike* (*Un (-val 'up) (-val 'same) -Path -String))
|
||||
(define -Pattern (*Un -String -Bytes -Regexp -Byte-Regexp -PRegexp -Byte-PRegexp))
|
||||
(define -Pathlike (*Un -String -Path))
|
||||
(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
|
||||
(define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String))
|
||||
(define -Byte N)
|
||||
|
||||
(define (-Tuple l)
|
||||
|
|
@ -220,16 +220,13 @@
|
|||
(define Any-Syntax ;(-Syntax Univ)
|
||||
(-mu x
|
||||
(-Syntax (*Un
|
||||
(-mu y (*Un (-pair x (*Un x y)) (-val '())))
|
||||
(make-Vector x)
|
||||
(make-Box x)
|
||||
N
|
||||
B
|
||||
-Keyword
|
||||
Sym
|
||||
-String
|
||||
Sym))))
|
||||
-Keyword
|
||||
(-mu y (*Un (-val '()) (-pair x (*Un x y))))
|
||||
(make-Vector x)
|
||||
(make-Box x)))))
|
||||
|
||||
(define Ident (-Syntax Sym))
|
||||
|
||||
;; DO NOT USE if t contains #f
|
||||
(define (-opt t) (*Un (-val #f) t))
|
||||
(define Ident (-Syntax Sym))
|
||||
|
|
@ -78,3 +78,7 @@
|
|||
|
||||
(define-syntax-rule (->opt args ... [opt ...] res)
|
||||
(opt-fn (list args ...) (list opt ...) res))
|
||||
|
||||
|
||||
;; DO NOT USE if t contains #f
|
||||
(define (-opt t) (Un (-val #f) t))
|
||||
|
|
@ -9,29 +9,29 @@
|
|||
(de False-Effect () [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
;; v is an identifier
|
||||
(de Var-True-Effect (v) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
|
||||
(de Var-True-Effect ([v identifier?]) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
;; v is an identifier
|
||||
(de Var-False-Effect (v) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
|
||||
(de Var-False-Effect ([v identifier?]) [#:intern (hash-id v)] [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
;; t is a Type
|
||||
;; v is an identifier
|
||||
(de Restrict-Effect (t v) [#:intern (list t (hash-id v))] [#:frees (free-vars* t) (free-idxs* t)]
|
||||
(de Restrict-Effect ([t Type?] [v identifier?]) [#:intern (list t (hash-id v))] [#:frees (free-vars* t) (free-idxs* t)]
|
||||
[#:fold-rhs (*Restrict-Effect (type-rec-id t) v)])
|
||||
|
||||
;; t is a Type
|
||||
;; v is an identifier
|
||||
(de Remove-Effect (t v)
|
||||
(de Remove-Effect ([t Type?] [v identifier?])
|
||||
[#:intern (list t (hash-id v))]
|
||||
[#:frees (free-vars* t) (free-idxs* t)]
|
||||
[#:fold-rhs (*Remove-Effect (type-rec-id t) v)])
|
||||
|
||||
;; t is a Type
|
||||
(de Latent-Restrict-Effect (t) [#:frees (free-vars* t) (free-idxs* t)]
|
||||
(de Latent-Restrict-Effect ([t Type?]) [#: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) [#:frees (free-vars* t) (free-idxs* t)]
|
||||
(de Latent-Remove-Effect ([t Type?]) [#: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])
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@
|
|||
"free-variance.ss"
|
||||
"interning.ss"
|
||||
mzlib/etc
|
||||
scheme/contract
|
||||
(for-syntax
|
||||
stxclass
|
||||
scheme/base
|
||||
|
|
@ -40,14 +41,25 @@
|
|||
(define-for-syntax effect-rec-id #'effect-rec-id)
|
||||
(define-for-syntax fold-target #'fold-target)
|
||||
|
||||
(define-for-syntax enable-contracts? #t)
|
||||
|
||||
(provide (for-syntax type-rec-id effect-rec-id fold-target))
|
||||
|
||||
(define-syntaxes (dt de)
|
||||
(let ()
|
||||
(define-syntax-class opt-cnt-id
|
||||
#:attributes (i cnt)
|
||||
(pattern i:id
|
||||
#:with cnt #'any/c)
|
||||
(pattern [i:id cnt]))
|
||||
(define-syntax-class no-provide-kw
|
||||
(pattern #:no-provide))
|
||||
(define-syntax-class idlist
|
||||
(pattern (i:id ...)))
|
||||
#:attributes ((i 1) (cnt 1) fs)
|
||||
(pattern (oci:opt-cnt-id ...)
|
||||
#:with (i ...) #'(oci.i ...)
|
||||
#:with (cnt ...) #'(oci.cnt ...)
|
||||
#:with fs #'(i ...)))
|
||||
(define (combiner f flds)
|
||||
(syntax-parse flds
|
||||
[() #'empty-hash-table]
|
||||
|
|
@ -74,14 +86,18 @@
|
|||
[[#:intern intern?:expr]] #:opt
|
||||
[[#:frees . frees:frees-pat]] #:opt
|
||||
[[#:fold-rhs fold-rhs:fold-pat]] #:opt
|
||||
[[#:contract cnt:expr]] #:opt
|
||||
[no-provide?:no-provide-kw] #:opt) ...*)
|
||||
(with-syntax*
|
||||
([ex (mk-id #'nm #'nm ":")]
|
||||
[kw-stx (string->keyword (symbol->string #'nm.datum))]
|
||||
[parent par]
|
||||
[(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds) #f #t #'nm)]
|
||||
[(s:ty maker pred acc ...) (build-struct-names #'nm (syntax->list #'flds.fs) #f #t #'nm)]
|
||||
[*maker (mk-id #'nm "*" #'nm)]
|
||||
[**maker (mk-id #'nm "**" #'nm)]
|
||||
[*maker-cnt (if enable-contracts?
|
||||
(or #'cnt #'(flds.cnt ... . -> . pred))
|
||||
#'any/c)]
|
||||
[ht-stx ht-stx]
|
||||
[bfs-fold-rhs (cond [#'fold-rhs #`(lambda (tr er) #,#'fold-rhs.e)]
|
||||
[else #'(lambda (type-rec-id effect-rec-id)
|
||||
|
|
@ -90,32 +106,33 @@
|
|||
#'(begin)
|
||||
#`(begin
|
||||
(provide ex pred acc ...)
|
||||
(provide (rename-out [*maker maker]))))]
|
||||
(provide/contract (rename *maker maker *maker-cnt))))]
|
||||
[intern
|
||||
(let ([mk (lambda (int) #`(defintern (**maker . flds) maker #,int #:extra-arg key-expr))])
|
||||
(syntax-parse #'flds
|
||||
(let ([mk (lambda (int) #`(defintern (**maker . flds.fs) maker #,int #:extra-arg key-expr))])
|
||||
(syntax-parse #'flds.fs
|
||||
[_ #:when #'intern?
|
||||
(mk #'intern?)]
|
||||
[() (mk #'#f)]
|
||||
[(f) (mk #'f)]
|
||||
[_ (mk #'(list . flds))]))]
|
||||
[frees
|
||||
(with-syntax ([(f1 f2) (if #'frees
|
||||
#'(frees.f1 frees.f2)
|
||||
(list (combiner #'free-vars* #'flds)
|
||||
(combiner #'free-idxs* #'flds)))])
|
||||
(quasisyntax/loc stx
|
||||
(define (*maker . flds)
|
||||
(define v (**maker . flds))
|
||||
(unless-in-table
|
||||
var-table v
|
||||
(define fvs f1)
|
||||
(define fis f2)
|
||||
(hash-set! var-table v fvs)
|
||||
(hash-set! index-table v fis))
|
||||
v)))])
|
||||
[_ (mk #'(list . flds.fs))]))]
|
||||
[frees
|
||||
(with-syntax ([(f1 f2) (if #'frees
|
||||
#'(frees.f1 frees.f2)
|
||||
(list (combiner #'free-vars* #'flds.fs)
|
||||
(combiner #'free-idxs* #'flds.fs)))])
|
||||
(quasisyntax/loc stx
|
||||
(with-contract nm ([*maker *maker-cnt])
|
||||
(define (*maker . flds.fs)
|
||||
(define v (**maker . flds.fs))
|
||||
(unless-in-table
|
||||
var-table v
|
||||
(define fvs f1)
|
||||
(define fis f2)
|
||||
(hash-set! var-table v fvs)
|
||||
(hash-set! index-table v fis))
|
||||
v))))])
|
||||
#`(begin
|
||||
(define-struct (nm parent) flds #:inspector #f)
|
||||
(define-struct (nm parent) flds.fs #:inspector #f)
|
||||
(define-match-expander ex
|
||||
(lambda (s)
|
||||
(syntax-parse s
|
||||
|
|
@ -123,7 +140,7 @@
|
|||
#:with pat (syntax/loc s (_ _ . fs))
|
||||
(syntax/loc s (struct nm pat))])))
|
||||
(begin-for-syntax
|
||||
(hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx)))
|
||||
(hash-set! ht-stx 'kw-stx (list #'ex #'flds.fs bfs-fold-rhs #'#,stx)))
|
||||
intern
|
||||
provides
|
||||
frees))])))
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@
|
|||
(require (utils tc-utils)
|
||||
"rep-utils.ss" "effect-rep.ss" "free-variance.ss"
|
||||
mzlib/trace scheme/match
|
||||
scheme/contract
|
||||
(for-syntax scheme/base))
|
||||
|
||||
(define name-table (make-weak-hasheq))
|
||||
|
|
@ -13,26 +14,36 @@
|
|||
;; Type is defined in rep-utils.ss
|
||||
|
||||
;; t must be a Type
|
||||
(dt Scope (t) [#:key (Type-key t)])
|
||||
(dt Scope ([t Type?]) [#:key (Type-key t)])
|
||||
|
||||
(define (scope-depth k)
|
||||
(flat-named-contract
|
||||
(format "Scope of depth ~a" k)
|
||||
(lambda (sc)
|
||||
(define (f k sc)
|
||||
(cond [(= 0 k) (not (Scope? sc))]
|
||||
[(not (Scope? sc)) #f]
|
||||
[else (f (sub1 k) (Scope-t sc))]))
|
||||
(f k sc))))
|
||||
|
||||
;; this is ONLY used when a type error ocurrs
|
||||
(dt Error () [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
;; i is an nat
|
||||
(dt B (i)
|
||||
(dt B ([i natural-number/c])
|
||||
[#:frees empty-hash-table (make-immutable-hasheq (list (cons i Covariant)))]
|
||||
[#:fold-rhs #:base])
|
||||
|
||||
;; n is a Name
|
||||
(dt F (n) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base])
|
||||
(dt F ([n symbol?]) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base])
|
||||
|
||||
;; id is an Identifier
|
||||
(dt Name (id) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
|
||||
(dt Name ([id identifier?]) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
;; rator is a type
|
||||
;; rands is a list of types
|
||||
;; stx is the syntax of the pair of parens
|
||||
(dt App (rator rands stx)
|
||||
(dt App ([rator Type?] [rands (listof Type?)] [stx syntax?])
|
||||
[#:intern (list rator rands)]
|
||||
[#:frees (combine-frees (map free-vars* (cons rator rands)))
|
||||
(combine-frees (map free-idxs* (cons rator rands)))]
|
||||
|
|
@ -41,19 +52,19 @@
|
|||
stx)])
|
||||
|
||||
;; left and right are Types
|
||||
(dt Pair (left right) [#:key 'pair])
|
||||
(dt Pair ([left Type?] [right Type?]) [#:key 'pair])
|
||||
|
||||
;; elem is a Type
|
||||
(dt Vector (elem)
|
||||
(dt Vector ([elem Type?])
|
||||
[#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
|
||||
[#:key 'vector])
|
||||
|
||||
;; elem is a Type
|
||||
(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
|
||||
(dt Box ([elem Type?]) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))]
|
||||
[#:key 'box])
|
||||
|
||||
;; name is a Symbol (not a Name)
|
||||
(dt Base (name contract) [#:frees #f] [#:fold-rhs #:base] [#:intern name]
|
||||
(dt Base ([name symbol?] [contract syntax?]) [#:frees #f] [#:fold-rhs #:base] [#:intern name]
|
||||
[#:key (case name
|
||||
[(Number Integer) 'number]
|
||||
[(Boolean) 'boolean]
|
||||
|
|
@ -63,13 +74,17 @@
|
|||
[else #f])])
|
||||
|
||||
;; body is a Scope
|
||||
(dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))]
|
||||
(dt Mu ([body (scope-depth 1)]) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))]
|
||||
[#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))]
|
||||
[#:key (Type-key body)])
|
||||
|
||||
;; n is how many variables are bound here
|
||||
;; body is a Scope
|
||||
(dt Poly (n body) #:no-provide
|
||||
[#:contract (->d ([n natural-number/c]
|
||||
[body (scope-depth n)])
|
||||
()
|
||||
[result Poly?])]
|
||||
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
|
||||
[#:fold-rhs (let ([body* (remove-scopes n body)])
|
||||
(*Poly n (add-scopes n (type-rec-id body*))))]
|
||||
|
|
@ -79,6 +94,10 @@
|
|||
;; there are n-1 'normal' vars and 1 ... var
|
||||
;; body is a Scope
|
||||
(dt PolyDots (n body) #:no-provide
|
||||
[#:contract (->d ([n natural-number/c]
|
||||
[body (scope-depth n)])
|
||||
()
|
||||
[result PolyDots?])]
|
||||
[#:key (Type-key body)]
|
||||
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
|
||||
[#:fold-rhs (let ([body* (remove-scopes n body)])
|
||||
|
|
@ -86,32 +105,13 @@
|
|||
|
||||
;; pred : identifier
|
||||
;; cert : syntax certifier
|
||||
(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred])
|
||||
|
||||
;; name : symbol
|
||||
;; parent : Struct
|
||||
;; flds : Listof[Type]
|
||||
;; proc : Function Type
|
||||
;; poly? : is this a polymorphic type?
|
||||
;; pred-id : identifier for the predicate of the struct
|
||||
;; cert : syntax certifier for pred-id
|
||||
(dt Struct (name parent flds proc poly? pred-id cert)
|
||||
[#:intern (list name parent flds proc)]
|
||||
[#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds)))
|
||||
(combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) flds)))]
|
||||
[#:fold-rhs (*Struct name
|
||||
(and parent (type-rec-id parent))
|
||||
(map type-rec-id flds)
|
||||
(and proc (type-rec-id proc))
|
||||
poly?
|
||||
pred-id
|
||||
cert)]
|
||||
[#:key (gensym)])
|
||||
(dt Opaque ([pred identifier?] [cert procedure?])
|
||||
[#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base] [#:key pred])
|
||||
|
||||
;; kw : keyword?
|
||||
;; ty : Type
|
||||
;; required? : Boolean
|
||||
(dt Keyword (kw ty required?)
|
||||
(dt Keyword ([kw keyword?] [ty Type?] [required? boolean?])
|
||||
[#:frees (free-vars* ty)
|
||||
(free-idxs* ty)]
|
||||
[#:fold-rhs (*Keyword kw (type-rec-id ty) required?)]
|
||||
|
|
@ -126,7 +126,13 @@
|
|||
;; thn-eff : Effect
|
||||
;; els-eff : Effect
|
||||
;; arr is NOT a Type
|
||||
(dt arr (dom rng rest drest kws thn-eff els-eff)
|
||||
(dt arr ([dom (listof Type?)]
|
||||
[rng Type?]
|
||||
[rest (or/c #f Type?)]
|
||||
[drest (or/c #f (cons/c Type? (or/c natural-number/c symbol?)))]
|
||||
[kws (listof Keyword?)]
|
||||
[thn-eff (listof Effect?)]
|
||||
[els-eff (listof Effect?)])
|
||||
[#:key 'procedure]
|
||||
[#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null)
|
||||
(map Keyword-ty kws)
|
||||
|
|
@ -163,11 +169,42 @@
|
|||
(dt top-arr ()
|
||||
[#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
(define arr/c (or/c top-arr? arr?))
|
||||
|
||||
;; arities : Listof[arr]
|
||||
(dt Function (arities) [#:frees (combine-frees (map free-vars* arities))
|
||||
(combine-frees (map free-idxs* arities))]
|
||||
(dt Function ([arities (listof arr/c)])
|
||||
[#:frees (combine-frees (map free-vars* arities))
|
||||
(combine-frees (map free-idxs* arities))]
|
||||
[#:fold-rhs (*Function (map type-rec-id arities))])
|
||||
|
||||
|
||||
;; name : symbol
|
||||
;; parent : Struct
|
||||
;; flds : Listof[Type]
|
||||
;; proc : Function Type
|
||||
;; poly? : is this a polymorphic type?
|
||||
;; pred-id : identifier for the predicate of the struct
|
||||
;; cert : syntax certifier for pred-id
|
||||
(dt Struct ([name symbol?]
|
||||
[parent (or/c #f Struct? Name?)]
|
||||
[flds (listof Type?)]
|
||||
[proc (or/c #f Function?)]
|
||||
[poly? boolean?]
|
||||
[pred-id identifier?]
|
||||
[cert procedure?])
|
||||
[#:intern (list name parent flds proc)]
|
||||
[#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds)))
|
||||
(combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) flds)))]
|
||||
[#:fold-rhs (*Struct name
|
||||
(and parent (type-rec-id parent))
|
||||
(map type-rec-id flds)
|
||||
(and proc (type-rec-id proc))
|
||||
poly?
|
||||
pred-id
|
||||
cert)]
|
||||
[#:key (gensym)])
|
||||
|
||||
|
||||
;; v : Scheme Value
|
||||
(dt Value (v) [#:frees #f] [#:fold-rhs #:base] [#:key (cond [(number? v) 'number]
|
||||
[(boolean? v) 'boolean]
|
||||
|
|
@ -175,8 +212,20 @@
|
|||
[else #f])])
|
||||
|
||||
;; elems : Listof[Type]
|
||||
(dt Union (elems) [#:frees (combine-frees (map free-vars* elems))
|
||||
(combine-frees (map free-idxs* elems))]
|
||||
(dt Union ([elems (and/c (listof Type?)
|
||||
(lambda (es)
|
||||
(let-values ([(sorted? k)
|
||||
(for/fold ([sorted? #t]
|
||||
[last -1])
|
||||
([e es])
|
||||
(let ([seq (Type-seq e)])
|
||||
(values
|
||||
(and sorted?
|
||||
(< last seq))
|
||||
seq)))])
|
||||
sorted?)))])
|
||||
[#:frees (combine-frees (map free-vars* elems))
|
||||
(combine-frees (map free-idxs* elems))]
|
||||
[#:fold-rhs ((get-union-maker) (map type-rec-id elems))]
|
||||
[#:key (let loop ([res null] [ts elems])
|
||||
(if (null? ts) res
|
||||
|
|
@ -188,14 +237,14 @@
|
|||
(dt Univ () [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
;; types : Listof[Type]
|
||||
(dt Values (types)
|
||||
(dt Values ([types (listof Type?)])
|
||||
#:no-provide
|
||||
[#:frees (combine-frees (map free-vars* types))
|
||||
(combine-frees (map free-idxs* types))]
|
||||
[#:fold-rhs (*Values (map type-rec-id types))]
|
||||
[#:key 'values])
|
||||
|
||||
(dt ValuesDots (types dty dbound)
|
||||
(dt ValuesDots ([types (listof Type?)] [dty Type?] [dbound (or/c symbol? natural-number/c)])
|
||||
[#:frees (combine-frees (map free-vars* (cons dty types)))
|
||||
(combine-frees (map free-idxs* (cons dty types)))]
|
||||
[#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)]
|
||||
|
|
@ -203,19 +252,21 @@
|
|||
|
||||
;; in : Type
|
||||
;; out : Type
|
||||
(dt Param (in out) [#:key 'parameter])
|
||||
(dt Param ([in Type?] [out Type?]) [#:key 'parameter])
|
||||
|
||||
;; key : Type
|
||||
;; value : Type
|
||||
(dt Hashtable (key value) [#:key 'hash])
|
||||
(dt Hashtable ([key Type?] [value Type?]) [#:key 'hash])
|
||||
|
||||
;; t : Type
|
||||
(dt Syntax (t) [#:key 'syntax])
|
||||
(dt Syntax ([t Type?]) [#:key 'syntax])
|
||||
|
||||
;; pos-flds : (Listof Type)
|
||||
;; name-flds : (Listof (Tuple Symbol Type Boolean))
|
||||
;; methods : (Listof (Tuple Symbol Function))
|
||||
(dt Class (pos-flds name-flds methods)
|
||||
(dt Class ([pos-flds (listof Type?)]
|
||||
[name-flds (listof (list/c symbol? Type? boolean?))]
|
||||
[methods (listof (list/c symbol? Function?))])
|
||||
[#:frees (combine-frees
|
||||
(map free-vars* (append pos-flds
|
||||
(map cadr name-flds)
|
||||
|
|
@ -238,7 +289,7 @@
|
|||
(map list mname (map type-rec-id mty)))])])
|
||||
|
||||
;; cls : Class
|
||||
(dt Instance (cls) [#:key 'instance])
|
||||
(dt Instance ([cls Class?]) [#:key 'instance])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
||||
|
|
|
|||
|
|
@ -166,7 +166,7 @@
|
|||
[(_ val)
|
||||
#'(? (lambda (x) (equal? val x)))])))
|
||||
|
||||
(define-for-syntax printing? #t)
|
||||
(define-for-syntax printing? #f)
|
||||
|
||||
(define print-type* (box (lambda _ (error "print-type* not yet defined"))))
|
||||
(define print-effect* (box (lambda _ (error "print-effect* not yet defined"))))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user