Give more meaningful names to conditional contract forms.
This commit is contained in:
parent
027947eef2
commit
a1fab6ec06
2
collects/typed-scheme/env/lexical-env.rkt
vendored
2
collects/typed-scheme/env/lexical-env.rkt
vendored
|
@ -18,7 +18,7 @@
|
||||||
|
|
||||||
(provide lexical-env with-lexical-env with-lexical-env/extend
|
(provide lexical-env with-lexical-env with-lexical-env/extend
|
||||||
with-lexical-env/extend/props)
|
with-lexical-env/extend/props)
|
||||||
(p/c
|
(provide/cond-contract
|
||||||
[lookup-type/lexical ((identifier?) (prop-env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
|
[lookup-type/lexical ((identifier?) (prop-env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
|
||||||
[update-type/lexical (((identifier? Type/c . -> . Type/c) identifier?) (prop-env?) . ->* . env?)])
|
[update-type/lexical (((identifier? Type/c . -> . Type/c) identifier?) (prop-env?) . ->* . env?)])
|
||||||
|
|
||||||
|
|
12
collects/typed-scheme/env/type-env-structs.rkt
vendored
12
collects/typed-scheme/env/type-env-structs.rkt
vendored
|
@ -20,12 +20,12 @@
|
||||||
|
|
||||||
;; eq? has the type of equal?, and l is an alist (with conses!)
|
;; eq? has the type of equal?, and l is an alist (with conses!)
|
||||||
;; props is a list of known propositions
|
;; props is a list of known propositions
|
||||||
(r:d-s/c env ([l (and/c (not/c dict-mutable?) dict?)])
|
(r:define-struct/cond-contract env ([l (and/c (not/c dict-mutable?) dict?)])
|
||||||
#:transparent
|
#:transparent
|
||||||
#:property prop:custom-write
|
#:property prop:custom-write
|
||||||
(lambda (e prt mode)
|
(lambda (e prt mode)
|
||||||
(fprintf prt "(env ~a)" (dict-map (env-l e) list))))
|
(fprintf prt "(env ~a)" (dict-map (env-l e) list))))
|
||||||
(r:d-s/c (prop-env env) ([props (listof Filter/c)])
|
(r:define-struct/cond-contract (prop-env env) ([props (listof Filter/c)])
|
||||||
#:transparent
|
#:transparent
|
||||||
#:property prop:custom-write
|
#:property prop:custom-write
|
||||||
(lambda (e prt mode)
|
(lambda (e prt mode)
|
||||||
|
@ -45,15 +45,15 @@
|
||||||
#:when (not (f (cons k v))))
|
#:when (not (f (cons k v))))
|
||||||
(dict-remove h k)))]))
|
(dict-remove h k)))]))
|
||||||
|
|
||||||
(r:d/c (make-empty-env dict)
|
(r:define/cond-contract (make-empty-env dict)
|
||||||
(dict? . -> . env?)
|
(dict? . -> . env?)
|
||||||
(env dict))
|
(env dict))
|
||||||
|
|
||||||
(r:d/c (make-empty-prop-env dict)
|
(r:define/cond-contract (make-empty-prop-env dict)
|
||||||
(dict? . -> . prop-env?)
|
(dict? . -> . prop-env?)
|
||||||
(prop-env dict null))
|
(prop-env dict null))
|
||||||
|
|
||||||
(r:d/c (env-props e)
|
(r:define/cond-contract (env-props e)
|
||||||
(prop-env? . -> . (listof Filter/c))
|
(prop-env? . -> . (listof Filter/c))
|
||||||
(prop-env-props e))
|
(prop-env-props e))
|
||||||
|
|
||||||
|
@ -61,7 +61,7 @@
|
||||||
(match e
|
(match e
|
||||||
[(env l) (for/list ([(k v) (in-dict l)]) (cons k v))]))
|
[(env l) (for/list ([(k v) (in-dict l)]) (cons k v))]))
|
||||||
|
|
||||||
(r:d/c (env-map f e)
|
(r:define/cond-contract (env-map f e)
|
||||||
((any/c any/c . -> . any/c) env? . -> . env?)
|
((any/c any/c . -> . any/c) env? . -> . env?)
|
||||||
(mk-env e (dict-map f (env-l e))))
|
(mk-env e (dict-map f (env-l e))))
|
||||||
|
|
||||||
|
|
|
@ -5,28 +5,28 @@
|
||||||
;; S, T types
|
;; S, T types
|
||||||
;; X a var
|
;; X a var
|
||||||
;; represents S <: X <: T
|
;; represents S <: X <: T
|
||||||
(d-s/c c ([S Type/c] [X symbol?] [T Type/c]) #:transparent)
|
(define-struct/cond-contract c ([S Type/c] [X symbol?] [T Type/c]) #:transparent)
|
||||||
|
|
||||||
;; fixed : Listof[c]
|
;; fixed : Listof[c]
|
||||||
;; rest : option[c]
|
;; rest : option[c]
|
||||||
;; a constraint on an index variable
|
;; a constraint on an index variable
|
||||||
;; the index variable must be instantiated with |fixed| arguments, each meeting the appropriate constraint
|
;; the index variable must be instantiated with |fixed| arguments, each meeting the appropriate constraint
|
||||||
;; and further instantions of the index variable must respect the rest constraint, if it exists
|
;; and further instantions of the index variable must respect the rest constraint, if it exists
|
||||||
(d-s/c dcon ([fixed (listof c?)] [rest (or/c c? #f)]) #:transparent)
|
(define-struct/cond-contract dcon ([fixed (listof c?)] [rest (or/c c? #f)]) #:transparent)
|
||||||
|
|
||||||
;; fixed : Listof[c]
|
;; fixed : Listof[c]
|
||||||
;; rest : c
|
;; rest : c
|
||||||
(d-s/c dcon-exact ([fixed (listof c?)] [rest c?]) #:transparent)
|
(define-struct/cond-contract dcon-exact ([fixed (listof c?)] [rest c?]) #:transparent)
|
||||||
|
|
||||||
;; fixed : Listof[c]
|
;; fixed : Listof[c]
|
||||||
;; type : c
|
;; type : c
|
||||||
;; bound : var
|
;; bound : var
|
||||||
(d-s/c dcon-dotted ([fixed (listof c?)] [type c?] [bound symbol?]) #:transparent)
|
(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 dcon/c (or/c dcon? dcon-exact? dcon-dotted?))
|
||||||
|
|
||||||
;; map : hash mapping index variables to dcons
|
;; map : hash mapping index variables to dcons
|
||||||
(d-s/c dmap ([map (hash/c symbol? dcon/c)]) #:transparent)
|
(define-struct/cond-contract dmap ([map (hash/c symbol? dcon/c)]) #:transparent)
|
||||||
|
|
||||||
;; maps is a list of pairs of
|
;; maps is a list of pairs of
|
||||||
;; - functional maps from vars to c's
|
;; - functional maps from vars to c's
|
||||||
|
@ -34,7 +34,7 @@
|
||||||
;; we need a bunch of mappings for each cset to handle case-lambda
|
;; we need a bunch of mappings for each cset to handle case-lambda
|
||||||
;; because case-lambda can generate multiple possible solutions, and we
|
;; because case-lambda can generate multiple possible solutions, and we
|
||||||
;; don't want to rule them out too early
|
;; don't want to rule them out too early
|
||||||
(d-s/c cset ([maps (listof (cons/c (hash/c symbol? c? #:immutable #t) dmap?))]) #:transparent)
|
(define-struct/cond-contract cset ([maps (listof (cons/c (hash/c symbol? c? #:immutable #t) dmap?))]) #:transparent)
|
||||||
|
|
||||||
(define-match-expander c:
|
(define-match-expander c:
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
(export dmap^)
|
(export dmap^)
|
||||||
|
|
||||||
;; dcon-meet : dcon dcon -> dcon
|
;; dcon-meet : dcon dcon -> dcon
|
||||||
(d/c (dcon-meet dc1 dc2)
|
(define/cond-contract (dcon-meet dc1 dc2)
|
||||||
(dcon/c dcon/c . -> . dcon/c)
|
(dcon/c dcon/c . -> . dcon/c)
|
||||||
(match* (dc1 dc2)
|
(match* (dc1 dc2)
|
||||||
[((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2))
|
[((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2))
|
||||||
|
|
|
@ -55,7 +55,7 @@
|
||||||
;; cset : the constraints being manipulated
|
;; cset : the constraints being manipulated
|
||||||
;; takes the constraints on vars and creates a dmap entry contstraining dbound to be |vars|
|
;; takes the constraints on vars and creates a dmap entry contstraining dbound to be |vars|
|
||||||
;; with the constraints that cset places on vars
|
;; with the constraints that cset places on vars
|
||||||
(d/c (move-vars-to-dmap cset dbound vars)
|
(define/cond-contract (move-vars-to-dmap cset dbound vars)
|
||||||
(cset? symbol? (listof symbol?) . -> . cset?)
|
(cset? symbol? (listof symbol?) . -> . cset?)
|
||||||
(mover cset dbound vars
|
(mover cset dbound vars
|
||||||
(λ (cmap dmap)
|
(λ (cmap dmap)
|
||||||
|
@ -67,7 +67,7 @@
|
||||||
;; dbound : index variable
|
;; dbound : index variable
|
||||||
;; cset : the constraints being manipulated
|
;; cset : the constraints being manipulated
|
||||||
;;
|
;;
|
||||||
(d/c (move-rest-to-dmap cset dbound #:exact [exact? #f])
|
(define/cond-contract (move-rest-to-dmap cset dbound #:exact [exact? #f])
|
||||||
((cset? symbol?) (#:exact boolean?) . ->* . cset?)
|
((cset? symbol?) (#:exact boolean?) . ->* . cset?)
|
||||||
(mover cset dbound null
|
(mover cset dbound null
|
||||||
(λ (cmap dmap)
|
(λ (cmap dmap)
|
||||||
|
@ -79,7 +79,7 @@
|
||||||
;; dbound : index variable
|
;; dbound : index variable
|
||||||
;; cset : the constraints being manipulated
|
;; cset : the constraints being manipulated
|
||||||
;;
|
;;
|
||||||
(d/c (move-dotted-rest-to-dmap cset dbound)
|
(define/cond-contract (move-dotted-rest-to-dmap cset dbound)
|
||||||
(cset? symbol? . -> . cset?)
|
(cset? symbol? . -> . cset?)
|
||||||
(mover cset dbound null
|
(mover cset dbound null
|
||||||
(λ (cmap dmap)
|
(λ (cmap dmap)
|
||||||
|
@ -94,7 +94,7 @@
|
||||||
;; in place, and the "simple" case will then call move-rest-to-dmap. This means
|
;; in place, and the "simple" case will then call move-rest-to-dmap. This means
|
||||||
;; we need to extract that result from the dmap and merge it with the fixed vars
|
;; we need to extract that result from the dmap and merge it with the fixed vars
|
||||||
;; we now handled. So I've extended the mover to give access to the dmap, which we use here.
|
;; we now handled. So I've extended the mover to give access to the dmap, which we use here.
|
||||||
(d/c (move-vars+rest-to-dmap cset dbound vars #:exact [exact? #f])
|
(define/cond-contract (move-vars+rest-to-dmap cset dbound vars #:exact [exact? #f])
|
||||||
((cset? symbol? (listof symbol?)) (#:exact boolean?) . ->* . cset?)
|
((cset? symbol? (listof symbol?)) (#:exact boolean?) . ->* . cset?)
|
||||||
(mover cset dbound vars
|
(mover cset dbound vars
|
||||||
(λ (cmap dmap)
|
(λ (cmap dmap)
|
||||||
|
@ -298,7 +298,7 @@
|
||||||
;; produces a cset which determines a substitution that makes S a subtype of T
|
;; produces a cset which determines a substitution that makes S a subtype of T
|
||||||
;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
|
;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
|
||||||
;; the index variables from the TOPLAS paper
|
;; the index variables from the TOPLAS paper
|
||||||
(d/c (cgen V X Y S T)
|
(define/cond-contract (cgen V X Y S T)
|
||||||
((listof symbol?) (listof symbol?) (listof symbol?) Type? Type? . -> . cset?)
|
((listof symbol?) (listof symbol?) (listof symbol?) Type? Type? . -> . cset?)
|
||||||
;; useful quick loop
|
;; useful quick loop
|
||||||
(define (cg S T) (cgen V X Y S T))
|
(define (cg S T) (cgen V X Y S T))
|
||||||
|
@ -541,7 +541,7 @@
|
||||||
;; C : cset? - set of constraints found by the inference engine
|
;; C : cset? - set of constraints found by the inference engine
|
||||||
;; Y : (listof symbol?) - index variables that must have entries
|
;; Y : (listof symbol?) - index variables that must have entries
|
||||||
;; R : Type? - result type into which we will be substituting
|
;; R : Type? - result type into which we will be substituting
|
||||||
(d/c (subst-gen C Y R)
|
(define/cond-contract (subst-gen C Y R)
|
||||||
(cset? (listof symbol?) Type? . -> . (or/c #f substitution/c))
|
(cset? (listof symbol?) Type? . -> . (or/c #f substitution/c))
|
||||||
(define var-hash (free-vars* R))
|
(define var-hash (free-vars* R))
|
||||||
(define idx-hash (free-idxs* R))
|
(define idx-hash (free-idxs* R))
|
||||||
|
@ -647,8 +647,8 @@
|
||||||
;; expected-cset : a cset representing the expected type, to meet early and
|
;; expected-cset : a cset representing the expected type, to meet early and
|
||||||
;; keep the number of constraints in check. (empty by default)
|
;; keep the number of constraints in check. (empty by default)
|
||||||
;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
|
;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
|
||||||
(d/c (cgen/list V X Y S T
|
(define/cond-contract (cgen/list V X Y S T
|
||||||
#:expected-cset [expected-cset (empty-cset '() '())])
|
#:expected-cset [expected-cset (empty-cset '() '())])
|
||||||
(((listof symbol?) (listof symbol?) (listof symbol?) (listof Type?) (listof Type?))
|
(((listof symbol?) (listof symbol?) (listof symbol?) (listof Type?) (listof Type?))
|
||||||
(#:expected-cset cset?) . ->* . cset?)
|
(#:expected-cset cset?) . ->* . cset?)
|
||||||
(unless (= (length S) (length T))
|
(unless (= (length S) (length T))
|
||||||
|
|
|
@ -5,59 +5,59 @@
|
||||||
(provide (all-defined-out))
|
(provide (all-defined-out))
|
||||||
|
|
||||||
(define-signature dmap^
|
(define-signature dmap^
|
||||||
([cnt dmap-meet (dmap? dmap? . -> . dmap?)]))
|
([cond-contracted dmap-meet (dmap? dmap? . -> . dmap?)]))
|
||||||
|
|
||||||
(define-signature promote-demote^
|
(define-signature promote-demote^
|
||||||
([cnt var-promote (Type? (listof symbol?) . -> . Type?)]
|
([cond-contracted var-promote (Type? (listof symbol?) . -> . Type?)]
|
||||||
[cnt var-demote (Type? (listof symbol?) . -> . Type?)]))
|
[cond-contracted var-demote (Type? (listof symbol?) . -> . Type?)]))
|
||||||
|
|
||||||
(define-signature constraints^
|
(define-signature constraints^
|
||||||
([cnt exn:infer? (any/c . -> . boolean?)]
|
([cond-contracted exn:infer? (any/c . -> . boolean?)]
|
||||||
[cnt fail-sym symbol?]
|
[cond-contracted fail-sym symbol?]
|
||||||
;; inference failure - masked before it gets to the user program
|
;; inference failure - masked before it gets to the user program
|
||||||
(define-syntaxes (fail!)
|
(define-syntaxes (fail!)
|
||||||
(syntax-rules ()
|
(syntax-rules ()
|
||||||
[(_ s t) (raise (list fail-sym s t))]))
|
[(_ s t) (raise (list fail-sym s t))]))
|
||||||
[cnt cset-meet (cset? cset? . -> . cset?)]
|
[cond-contracted cset-meet (cset? cset? . -> . cset?)]
|
||||||
[cnt cset-meet* ((listof cset?) . -> . cset?)]
|
[cond-contracted cset-meet* ((listof cset?) . -> . cset?)]
|
||||||
no-constraint
|
no-constraint
|
||||||
[cnt empty-cset ((listof symbol?) (listof symbol?) . -> . cset?)]
|
[cond-contracted empty-cset ((listof symbol?) (listof symbol?) . -> . cset?)]
|
||||||
[cnt insert (cset? symbol? Type? Type? . -> . cset?)]
|
[cond-contracted insert (cset? symbol? Type? Type? . -> . cset?)]
|
||||||
[cnt cset-combine ((listof cset?) . -> . cset?)]
|
[cond-contracted cset-combine ((listof cset?) . -> . cset?)]
|
||||||
[cnt c-meet ((c? c?) (symbol?) . ->* . c?)]))
|
[cond-contracted c-meet ((c? c?) (symbol?) . ->* . c?)]))
|
||||||
|
|
||||||
(define-signature restrict^
|
(define-signature restrict^
|
||||||
([cnt restrict (Type? Type? . -> . Type?)]))
|
([cond-contracted restrict (Type? Type? . -> . Type?)]))
|
||||||
|
|
||||||
(define-signature infer^
|
(define-signature infer^
|
||||||
([cnt infer ((;; variables from the forall
|
([cond-contracted infer ((;; variables from the forall
|
||||||
(listof symbol?)
|
(listof symbol?)
|
||||||
;; indexes from the forall
|
;; indexes from the forall
|
||||||
(listof symbol?)
|
(listof symbol?)
|
||||||
;; actual argument types from call site
|
;; actual argument types from call site
|
||||||
(listof Type?)
|
(listof Type?)
|
||||||
;; domain
|
;; domain
|
||||||
(listof Type?)
|
(listof Type?)
|
||||||
;; range
|
;; range
|
||||||
(or/c #f Type?))
|
(or/c #f Type?))
|
||||||
;; optional expected type
|
;; optional expected type
|
||||||
((or/c #f Type?))
|
((or/c #f Type?))
|
||||||
. ->* . any)]
|
. ->* . any)]
|
||||||
[cnt infer/vararg ((;; variables from the forall
|
[cond-contracted infer/vararg ((;; variables from the forall
|
||||||
(listof symbol?)
|
(listof symbol?)
|
||||||
;; indexes from the forall
|
;; indexes from the forall
|
||||||
(listof symbol?)
|
(listof symbol?)
|
||||||
;; actual argument types from call site
|
;; actual argument types from call site
|
||||||
(listof Type?)
|
(listof Type?)
|
||||||
;; domain
|
;; domain
|
||||||
(listof Type?)
|
(listof Type?)
|
||||||
;; rest
|
;; rest
|
||||||
(or/c #f Type?)
|
(or/c #f Type?)
|
||||||
;; range
|
;; range
|
||||||
(or/c #f Type?))
|
(or/c #f Type?))
|
||||||
;; [optional] expected type
|
;; [optional] expected type
|
||||||
((or/c #f Type?)) . ->* . any)]
|
((or/c #f Type?)) . ->* . any)]
|
||||||
[cnt infer/dots (((listof symbol?)
|
[cond-contracted infer/dots (((listof symbol?)
|
||||||
symbol?
|
symbol?
|
||||||
(listof Type?) (listof Type?) Type? Type? (listof symbol?))
|
(listof Type?) (listof Type?) Type? Type? (listof symbol?))
|
||||||
(#:expected (or/c #f Type?)) . ->* . any)]))
|
(#:expected (or/c #f Type?)) . ->* . any)]))
|
||||||
|
|
|
@ -15,10 +15,10 @@
|
||||||
|
|
||||||
(define-struct poly (name vars) #:prefab)
|
(define-struct poly (name vars) #:prefab)
|
||||||
|
|
||||||
(p/c [parse-type (syntax? . c:-> . Type/c)]
|
(provide/cond-contract [parse-type (syntax? . c:-> . Type/c)]
|
||||||
[parse-type/id (syntax? c:any/c . c:-> . Type/c)]
|
[parse-type/id (syntax? c:any/c . c:-> . Type/c)]
|
||||||
[parse-tc-results (syntax? . c:-> . tc-results?)]
|
[parse-tc-results (syntax? . c:-> . tc-results?)]
|
||||||
[parse-tc-results/id (syntax? c:any/c . c:-> . tc-results?)])
|
[parse-tc-results/id (syntax? c:any/c . c:-> . tc-results?)])
|
||||||
|
|
||||||
(provide star ddd/bound)
|
(provide star ddd/bound)
|
||||||
(define enable-mu-parsing (make-parameter #t))
|
(define enable-mu-parsing (make-parameter #t))
|
||||||
|
|
|
@ -115,7 +115,7 @@
|
||||||
;; expr : the RHS expression
|
;; expr : the RHS expression
|
||||||
;; tc-expr : a function like `tc-expr' from tc-expr-unit
|
;; tc-expr : a function like `tc-expr' from tc-expr-unit
|
||||||
;; tc-expr/check : a function like `tc-expr/check' from tc-expr-unit
|
;; tc-expr/check : a function like `tc-expr/check' from tc-expr-unit
|
||||||
(d/c (get-type/infer stxs expr tc-expr tc-expr/check)
|
(define/cond-contract (get-type/infer stxs expr tc-expr tc-expr/check)
|
||||||
((listof identifier?) syntax? (syntax? . -> . tc-results?) (syntax? tc-results? . -> . tc-results?) . -> . tc-results?)
|
((listof identifier?) syntax? (syntax? . -> . tc-results?) (syntax? tc-results? . -> . tc-results?) . -> . tc-results?)
|
||||||
(match stxs
|
(match stxs
|
||||||
[(list stx ...)
|
[(list stx ...)
|
||||||
|
|
|
@ -114,7 +114,7 @@
|
||||||
#'(begin)
|
#'(begin)
|
||||||
#'(begin
|
#'(begin
|
||||||
(provide nm.ex flds.pred flds.acc ...)
|
(provide nm.ex flds.pred flds.acc ...)
|
||||||
(p/c (rename nm.*maker flds.maker cnt))))])
|
(provide/cond-contract (rename nm.*maker flds.maker cnt))))])
|
||||||
#`(begin
|
#`(begin
|
||||||
(define-struct (nm #,par) flds.fs #:inspector #f)
|
(define-struct (nm #,par) flds.fs #:inspector #f)
|
||||||
(define-match-expander nm.ex
|
(define-match-expander nm.ex
|
||||||
|
@ -126,7 +126,7 @@
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
(hash-set! #,ht-stx 'nm.kw (list #'nm.ex #'flds.fs fold-rhs.proc #f)))
|
(hash-set! #,ht-stx 'nm.kw (list #'nm.ex #'flds.fs fold-rhs.proc #f)))
|
||||||
#,(quasisyntax/loc stx
|
#,(quasisyntax/loc stx
|
||||||
(w/c nm ([nm.*maker cnt])
|
(with-cond-contract nm ([nm.*maker cnt])
|
||||||
#,(quasisyntax/loc #'nm
|
#,(quasisyntax/loc #'nm
|
||||||
(defintern (nm.*maker . flds.fs) flds.maker intern?
|
(defintern (nm.*maker . flds.fs) flds.maker intern?
|
||||||
#:extra-args
|
#:extra-args
|
||||||
|
@ -235,11 +235,11 @@
|
||||||
[Rep-free-vars free-vars*]
|
[Rep-free-vars free-vars*]
|
||||||
[Rep-free-idxs free-idxs*]))
|
[Rep-free-idxs free-idxs*]))
|
||||||
|
|
||||||
(p/c (struct Rep ([seq exact-nonnegative-integer?]
|
(provide/cond-contract (struct Rep ([seq exact-nonnegative-integer?]
|
||||||
[free-vars (hash/c symbol? variance?)]
|
[free-vars (hash/c symbol? variance?)]
|
||||||
[free-idxs (hash/c symbol? variance?)]
|
[free-idxs (hash/c symbol? variance?)]
|
||||||
[stx (or/c #f syntax?)]))
|
[stx (or/c #f syntax?)]))
|
||||||
[replace-syntax (Rep? syntax? . -> . Rep?)])
|
[replace-syntax (Rep? syntax? . -> . Rep?)])
|
||||||
|
|
||||||
(define (replace-field val new-val idx)
|
(define (replace-field val new-val idx)
|
||||||
(define-values (type skipped) (struct-info val))
|
(define-values (type skipped) (struct-info val))
|
||||||
|
|
|
@ -420,7 +420,7 @@
|
||||||
|
|
||||||
;; remove-dups: List[Type] -> List[Type]
|
;; remove-dups: List[Type] -> List[Type]
|
||||||
;; removes duplicate types from a SORTED list
|
;; removes duplicate types from a SORTED list
|
||||||
(d/c (remove-dups types)
|
(define/cond-contract (remove-dups types)
|
||||||
((listof Rep?) . -> . (listof Rep?))
|
((listof Rep?) . -> . (listof Rep?))
|
||||||
(cond [(null? types) types]
|
(cond [(null? types) types]
|
||||||
[(null? (cdr types)) types]
|
[(null? (cdr types)) types]
|
||||||
|
@ -443,14 +443,16 @@
|
||||||
[_ (int-err "Tried to remove too many scopes: ~a" sc)])))
|
[_ (int-err "Tried to remove too many scopes: ~a" sc)])))
|
||||||
|
|
||||||
;; type equality
|
;; type equality
|
||||||
(d/c (type-equal? s t) (Rep? Rep? . -> . boolean?) (eq? (Rep-seq s) (Rep-seq t)))
|
(define/cond-contract (type-equal? s t)
|
||||||
|
(Rep? Rep? . -> . boolean?)
|
||||||
|
(eq? (Rep-seq s) (Rep-seq t)))
|
||||||
|
|
||||||
;; inequality - good
|
;; inequality - good
|
||||||
(d/c (type<? s t)
|
(define/cond-contract (type<? s t)
|
||||||
(Rep? Rep? . -> . boolean?)
|
(Rep? Rep? . -> . boolean?)
|
||||||
(< (Rep-seq s) (Rep-seq t)))
|
(< (Rep-seq s) (Rep-seq t)))
|
||||||
|
|
||||||
(d/c (type-compare s t)
|
(define/cond-contract (type-compare s t)
|
||||||
(Rep? Rep? . -> . (or/c -1 0 1))
|
(Rep? Rep? . -> . (or/c -1 0 1))
|
||||||
(cond [(type-equal? s t) 0]
|
(cond [(type-equal? s t) 0]
|
||||||
[(type<? s t) 1]
|
[(type<? s t) 1]
|
||||||
|
@ -732,6 +734,6 @@
|
||||||
[Poly-body* Poly-body]
|
[Poly-body* Poly-body]
|
||||||
[PolyDots-body* PolyDots-body]))
|
[PolyDots-body* PolyDots-body]))
|
||||||
|
|
||||||
(p/c [type-equal? (Rep? Rep? . -> . boolean?)])
|
(provide/cond-contract [type-equal? (Rep? Rep? . -> . boolean?)])
|
||||||
|
|
||||||
;(trace unfold)
|
;(trace unfold)
|
||||||
|
|
|
@ -11,7 +11,7 @@
|
||||||
(except-in syntax/parse id)
|
(except-in syntax/parse id)
|
||||||
(only-in srfi/1 split-at))
|
(only-in srfi/1 split-at))
|
||||||
|
|
||||||
(p/c
|
(provide/cond-contract
|
||||||
[check-below (-->d ([s (-or/c Type/c tc-results?)] [t (-or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])])
|
[check-below (-->d ([s (-or/c Type/c tc-results?)] [t (-or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])])
|
||||||
|
|
||||||
(define (print-object o)
|
(define (print-object o)
|
||||||
|
|
|
@ -7,7 +7,8 @@
|
||||||
(define-struct (def-stx-binding binding) () #:transparent)
|
(define-struct (def-stx-binding binding) () #:transparent)
|
||||||
(define-struct (def-struct-stx-binding def-stx-binding) (static-info) #:transparent)
|
(define-struct (def-struct-stx-binding def-stx-binding) (static-info) #:transparent)
|
||||||
|
|
||||||
(p/c (struct binding ([name identifier?]))
|
(provide/cond-contract
|
||||||
(struct (def-binding binding) ([name identifier?] [ty any/c]))
|
(struct binding ([name identifier?]))
|
||||||
(struct (def-stx-binding binding) ([name identifier?]))
|
(struct (def-binding binding) ([name identifier?] [ty any/c]))
|
||||||
(struct (def-struct-stx-binding binding) ([name identifier?] [static-info (or/c #f struct-info?)])))
|
(struct (def-stx-binding binding) ([name identifier?]))
|
||||||
|
(struct (def-struct-stx-binding binding) ([name identifier?] [static-info (or/c #f struct-info?)])))
|
||||||
|
|
|
@ -7,7 +7,7 @@
|
||||||
(private type-annotation)
|
(private type-annotation)
|
||||||
(for-template scheme/base))
|
(for-template scheme/base))
|
||||||
|
|
||||||
(p/c [find-annotation (syntax? identifier? . -> . (or/c #f Type/c))])
|
(provide/cond-contract [find-annotation (syntax? identifier? . -> . (or/c #f Type/c))])
|
||||||
|
|
||||||
(define-syntax-class lv-clause
|
(define-syntax-class lv-clause
|
||||||
#:transparent
|
#:transparent
|
||||||
|
|
|
@ -7,39 +7,39 @@
|
||||||
(provide (all-defined-out))
|
(provide (all-defined-out))
|
||||||
|
|
||||||
(define-signature tc-expr^
|
(define-signature tc-expr^
|
||||||
([cnt tc-expr (syntax? . -> . tc-results?)]
|
([cond-contracted tc-expr (syntax? . -> . tc-results?)]
|
||||||
[cnt tc-literal (->* (syntax?) ((or/c #f Type/c)) Type/c)]
|
[cond-contracted tc-literal (->* (syntax?) ((or/c #f Type/c)) Type/c)]
|
||||||
[cnt tc-expr/check (syntax? tc-results? . -> . tc-results?)]
|
[cond-contracted tc-expr/check (syntax? tc-results? . -> . tc-results?)]
|
||||||
[cnt tc-expr/check/t (syntax? tc-results? . -> . Type/c)]
|
[cond-contracted tc-expr/check/t (syntax? tc-results? . -> . Type/c)]
|
||||||
[cnt tc-exprs ((listof syntax?) . -> . tc-results?)]
|
[cond-contracted tc-exprs ((listof syntax?) . -> . tc-results?)]
|
||||||
[cnt tc-exprs/check ((listof syntax?) tc-results? . -> . tc-results?)]
|
[cond-contracted tc-exprs/check ((listof syntax?) tc-results? . -> . tc-results?)]
|
||||||
[cnt tc-expr/t (syntax? . -> . Type/c)]
|
[cond-contracted tc-expr/t (syntax? . -> . Type/c)]
|
||||||
[cnt single-value ((syntax?) ((or/c tc-results? #f)) . ->* . tc-results?)]))
|
[cond-contracted single-value ((syntax?) ((or/c tc-results? #f)) . ->* . tc-results?)]))
|
||||||
|
|
||||||
(define-signature check-subforms^
|
(define-signature check-subforms^
|
||||||
([cnt check-subforms/ignore (syntax? . -> . any)]
|
([cond-contracted check-subforms/ignore (syntax? . -> . any)]
|
||||||
[cnt check-subforms/with-handlers (syntax? . -> . any)]
|
[cond-contracted check-subforms/with-handlers (syntax? . -> . any)]
|
||||||
[cnt check-subforms/with-handlers/check (syntax? tc-results? . -> . any)]))
|
[cond-contracted check-subforms/with-handlers/check (syntax? tc-results? . -> . any)]))
|
||||||
|
|
||||||
(define-signature tc-if^
|
(define-signature tc-if^
|
||||||
([cnt tc/if-twoarm ((syntax? syntax? syntax?) (tc-results?) . ->* . tc-results?)]))
|
([cond-contracted tc/if-twoarm ((syntax? syntax? syntax?) (tc-results?) . ->* . tc-results?)]))
|
||||||
|
|
||||||
(define-signature tc-lambda^
|
(define-signature tc-lambda^
|
||||||
([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-results?)]
|
([cond-contracted tc/lambda (syntax? syntax? syntax? . -> . tc-results?)]
|
||||||
[cnt tc/lambda/check (syntax? syntax? syntax? tc-results? . -> . tc-results?)]
|
[cond-contracted tc/lambda/check (syntax? syntax? syntax? tc-results? . -> . tc-results?)]
|
||||||
[cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type/c) tc-results? . -> . tc-results?)]))
|
[cond-contracted tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type/c) tc-results? . -> . tc-results?)]))
|
||||||
|
|
||||||
(define-signature tc-app^
|
(define-signature tc-app^
|
||||||
([cnt tc/app (syntax? . -> . tc-results?)]
|
([cond-contracted tc/app (syntax? . -> . tc-results?)]
|
||||||
[cnt tc/app/check (syntax? tc-results? . -> . tc-results?)]))
|
[cond-contracted tc/app/check (syntax? tc-results? . -> . tc-results?)]))
|
||||||
|
|
||||||
(define-signature tc-apply^
|
(define-signature tc-apply^
|
||||||
([cnt tc/apply (syntax? syntax? . -> . tc-results?)]))
|
([cond-contracted tc/apply (syntax? syntax? . -> . tc-results?)]))
|
||||||
|
|
||||||
(define-signature tc-let^
|
(define-signature tc-let^
|
||||||
([cnt tc/let-values ((syntax? syntax? syntax? syntax?) ((or/c #f tc-results?)) . ->* . tc-results?)]
|
([cond-contracted tc/let-values ((syntax? syntax? syntax? syntax?) ((or/c #f tc-results?)) . ->* . tc-results?)]
|
||||||
[cnt tc/letrec-values ((syntax? syntax? syntax? syntax?) ((or/c #f tc-results?)) . ->* . tc-results?)]))
|
[cond-contracted tc/letrec-values ((syntax? syntax? syntax? syntax?) ((or/c #f tc-results?)) . ->* . tc-results?)]))
|
||||||
|
|
||||||
(define-signature tc-dots^
|
(define-signature tc-dots^
|
||||||
([cnt tc/dots (syntax? . -> . (values Type/c symbol?))]))
|
([cond-contracted tc/dots (syntax? . -> . (values Type/c symbol?))]))
|
||||||
|
|
||||||
|
|
|
@ -12,7 +12,7 @@
|
||||||
|
|
||||||
|
|
||||||
;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results?
|
;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results?
|
||||||
(d/c (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t])
|
(define/cond-contract (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t])
|
||||||
((syntax? syntax? arr? (c:listof tc-results?) (c:or/c #f tc-results?)) (#:check boolean?) . c:->* . tc-results?)
|
((syntax? syntax? arr? (c:listof tc-results?) (c:or/c #f tc-results?)) (#:check boolean?) . c:->* . tc-results?)
|
||||||
(match* (ftype0 argtys)
|
(match* (ftype0 argtys)
|
||||||
;; we check that all kw args are optional
|
;; we check that all kw args are optional
|
||||||
|
@ -65,9 +65,9 @@
|
||||||
[else (string-append (stringify (map make-printable dom)) rng-string)])))
|
[else (string-append (stringify (map make-printable dom)) rng-string)])))
|
||||||
|
|
||||||
;; Generates error messages when operand types don't match operator domains.
|
;; Generates error messages when operand types don't match operator domains.
|
||||||
(d/c (domain-mismatches f-stx args-stx ty doms rests drests rngs arg-tys tail-ty tail-bound
|
(define/cond-contract (domain-mismatches f-stx args-stx ty doms rests drests rngs arg-tys tail-ty tail-bound
|
||||||
#:expected [expected #f] #:return [return (make-Union null)]
|
#:expected [expected #f] #:return [return (make-Union null)]
|
||||||
#:msg-thunk [msg-thunk (lambda (dom) dom)])
|
#:msg-thunk [msg-thunk (lambda (dom) dom)])
|
||||||
((syntax? syntax? Type/c (c:listof (c:listof Type/c)) (c:listof (c:or/c #f Type/c))
|
((syntax? syntax? Type/c (c:listof (c:listof Type/c)) (c:listof (c:or/c #f Type/c))
|
||||||
(c:listof (c:or/c #f (c:cons/c Type/c (c:or/c c:natural-number/c symbol?))))
|
(c:listof (c:or/c #f (c:cons/c Type/c (c:or/c c:natural-number/c symbol?))))
|
||||||
(c:listof (c:or/c Values? ValuesDots?)) (c:listof tc-results?) (c:or/c #f Type/c) c:any/c)
|
(c:listof (c:or/c Values? ValuesDots?)) (c:listof tc-results?) (c:or/c #f Type/c) c:any/c)
|
||||||
|
|
|
@ -71,7 +71,7 @@
|
||||||
t]))
|
t]))
|
||||||
|
|
||||||
;; sets the flag box to #f if anything becomes (U)
|
;; sets the flag box to #f if anything becomes (U)
|
||||||
(d/c (env+ env fs flag)
|
(define/cond-contract (env+ env fs flag)
|
||||||
(([e env?] [fs (listof Filter/c)] [bx (box/c boolean?)])
|
(([e env?] [fs (listof Filter/c)] [bx (box/c boolean?)])
|
||||||
#:pre (bx) (unbox bx) . ->i . [_ env?])
|
#:pre (bx) (unbox bx) . ->i . [_ env?])
|
||||||
(define-values (props atoms) (combine-props fs (env-props env) flag))
|
(define-values (props atoms) (combine-props fs (env-props env) flag))
|
||||||
|
@ -86,5 +86,6 @@
|
||||||
x Γ)]
|
x Γ)]
|
||||||
[_ Γ])))
|
[_ Γ])))
|
||||||
|
|
||||||
(p/c [env+ (([e env?] [fs (listof Filter/c)] [bx (box/c boolean?)])
|
(provide/cond-contract
|
||||||
#:pre (bx) (unbox bx) . ->i . [_ env?])])
|
[env+ (([e env?] [fs (listof Filter/c)] [bx (box/c boolean?)])
|
||||||
|
#:pre (bx) (unbox bx) . ->i . [_ env?])])
|
||||||
|
|
|
@ -170,7 +170,7 @@
|
||||||
;; typecheck an identifier
|
;; typecheck an identifier
|
||||||
;; the identifier has variable effect
|
;; the identifier has variable effect
|
||||||
;; tc-id : identifier -> tc-results
|
;; tc-id : identifier -> tc-results
|
||||||
(d/c (tc-id id)
|
(define/cond-contract (tc-id id)
|
||||||
(--> identifier? tc-results?)
|
(--> identifier? tc-results?)
|
||||||
(let* ([ty (lookup-type/lexical id)])
|
(let* ([ty (lookup-type/lexical id)])
|
||||||
(ret ty
|
(ret ty
|
||||||
|
@ -229,7 +229,7 @@
|
||||||
t)]))))
|
t)]))))
|
||||||
|
|
||||||
;; tc-expr/check : syntax tc-results -> tc-results
|
;; tc-expr/check : syntax tc-results -> tc-results
|
||||||
(d/c (tc-expr/check/internal form expected)
|
(define/cond-contract (tc-expr/check/internal form expected)
|
||||||
(--> syntax? tc-results? tc-results?)
|
(--> syntax? tc-results? tc-results?)
|
||||||
(parameterize ([current-orig-stx form])
|
(parameterize ([current-orig-stx form])
|
||||||
;(printf "form: ~a\n" (syntax-object->datum form))
|
;(printf "form: ~a\n" (syntax-object->datum form))
|
||||||
|
@ -426,7 +426,7 @@
|
||||||
(add-typeof-expr form r)
|
(add-typeof-expr form r)
|
||||||
r)]))))
|
r)]))))
|
||||||
|
|
||||||
(d/c (tc/send form rcvr method args [expected #f])
|
(define/cond-contract (tc/send form rcvr method args [expected #f])
|
||||||
(-->* (syntax? syntax? syntax? syntax?) ((-or/c tc-results? #f)) tc-results?)
|
(-->* (syntax? syntax? syntax? syntax?) ((-or/c tc-results? #f)) tc-results?)
|
||||||
(match (tc-expr rcvr)
|
(match (tc-expr rcvr)
|
||||||
[(tc-result1: (Instance: (and c (Class: _ _ methods))))
|
[(tc-result1: (Instance: (and c (Class: _ _ methods))))
|
||||||
|
|
|
@ -38,7 +38,7 @@
|
||||||
(tc/funapp1 f-stx args-stx (subst-all substitution a) argtys expected #:check #f))))
|
(tc/funapp1 f-stx args-stx (subst-all substitution a) argtys expected #:check #f))))
|
||||||
(poly-fail f-stx args-stx t argtys #:name (and (identifier? f-stx) f-stx) #:expected expected))))]))
|
(poly-fail f-stx args-stx t argtys #:name (and (identifier? f-stx) f-stx) #:expected expected))))]))
|
||||||
|
|
||||||
(d/c (tc/funapp f-stx args-stx ftype0 argtys expected)
|
(define/cond-contract (tc/funapp f-stx args-stx ftype0 argtys expected)
|
||||||
(syntax? syntax? tc-results? (c:listof tc-results?) (c:or/c #f tc-results?) . c:-> . tc-results?)
|
(syntax? syntax? tc-results? (c:listof tc-results?) (c:or/c #f tc-results?) . c:-> . tc-results?)
|
||||||
(match* (ftype0 argtys)
|
(match* (ftype0 argtys)
|
||||||
;; we special-case this (no case-lambda) for improved error messages
|
;; we special-case this (no case-lambda) for improved error messages
|
||||||
|
|
|
@ -22,12 +22,12 @@
|
||||||
(import tc-expr^)
|
(import tc-expr^)
|
||||||
(export tc-lambda^)
|
(export tc-lambda^)
|
||||||
|
|
||||||
(d-s/c lam-result ([args (listof (list/c identifier? Type/c))]
|
(define-struct/cond-contract lam-result ([args (listof (list/c identifier? Type/c))]
|
||||||
[kws (listof (list/c keyword? identifier? Type/c boolean?))]
|
[kws (listof (list/c keyword? identifier? Type/c boolean?))]
|
||||||
[rest (or/c #f (list/c identifier? Type/c))]
|
[rest (or/c #f (list/c identifier? Type/c))]
|
||||||
[drest (or/c #f (cons/c identifier? (cons/c Type/c symbol?)))]
|
[drest (or/c #f (cons/c identifier? (cons/c Type/c symbol?)))]
|
||||||
[body tc-results?])
|
[body tc-results?])
|
||||||
#:transparent)
|
#:transparent)
|
||||||
|
|
||||||
(define (lam-result->type lr)
|
(define (lam-result->type lr)
|
||||||
(match lr
|
(match lr
|
||||||
|
@ -57,7 +57,7 @@
|
||||||
(if rest " and a rest arg" "")))
|
(if rest " and a rest arg" "")))
|
||||||
|
|
||||||
;; listof[id] option[id] block listof[type] option[type] option[(cons type var)] tc-result -> lam-result
|
;; listof[id] option[id] block listof[type] option[type] option[(cons type var)] tc-result -> lam-result
|
||||||
(d/c (check-clause arg-list rest body arg-tys rest-ty drest ret-ty)
|
(define/cond-contract (check-clause arg-list rest body arg-tys rest-ty drest ret-ty)
|
||||||
((listof identifier?)
|
((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?
|
(or/c #f identifier?) syntax? (listof Type/c) (or/c #f Type/c) (or/c #f (cons/c Type/c symbol?)) tc-results?
|
||||||
. --> .
|
. --> .
|
||||||
|
@ -230,9 +230,9 @@
|
||||||
|
|
||||||
;; tc/plambda syntax syntax-list syntax-list type -> Poly
|
;; tc/plambda syntax syntax-list syntax-list type -> Poly
|
||||||
;; formals and bodies must by syntax-lists
|
;; formals and bodies must by syntax-lists
|
||||||
(d/c (tc/plambda form formals bodies expected)
|
(define/cond-contract (tc/plambda form formals bodies expected)
|
||||||
(syntax? syntax? syntax? (or/c tc-results? #f) . --> . Type/c)
|
(syntax? syntax? syntax? (or/c tc-results? #f) . --> . Type/c)
|
||||||
(d/c (maybe-loop form formals bodies expected)
|
(define/cond-contract (maybe-loop form formals bodies expected)
|
||||||
(syntax? syntax? syntax? tc-results? . --> . Type/c)
|
(syntax? syntax? syntax? tc-results? . --> . Type/c)
|
||||||
(match expected
|
(match expected
|
||||||
[(tc-result1: (Function: _)) (tc/mono-lambda/type formals bodies expected)]
|
[(tc-result1: (Function: _)) (tc/mono-lambda/type formals bodies expected)]
|
||||||
|
|
|
@ -27,16 +27,16 @@
|
||||||
[(tc-results: ts _ _)
|
[(tc-results: ts _ _)
|
||||||
(ret ts (for/list ([f ts]) (make-NoFilter)) (for/list ([f ts]) (make-NoObject)))]))
|
(ret ts (for/list ([f ts]) (make-NoFilter)) (for/list ([f ts]) (make-NoObject)))]))
|
||||||
|
|
||||||
(d/c (do-check expr->type namess results expected-results form exprs body clauses expected #:abstract [abstract null])
|
(define/cond-contract (do-check expr->type namess results expected-results form exprs body clauses expected #:abstract [abstract null])
|
||||||
(((syntax? syntax? tc-results? . c:-> . any/c)
|
(((syntax? syntax? tc-results? . c:-> . any/c)
|
||||||
(listof (listof identifier?)) (listof tc-results?) (listof tc-results?)
|
(listof (listof identifier?)) (listof tc-results?) (listof tc-results?)
|
||||||
syntax? (listof syntax?) syntax? (listof syntax?) (or/c #f tc-results?))
|
syntax? (listof syntax?) syntax? (listof syntax?) (or/c #f tc-results?))
|
||||||
(#:abstract any/c)
|
(#:abstract any/c)
|
||||||
. c:->* .
|
. c:->* .
|
||||||
tc-results?)
|
tc-results?)
|
||||||
(w/c t/p ([types (listof (listof Type/c))] ; types that may contain undefined (letrec)
|
(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)
|
[expected-types (listof (listof Type/c))] ; types that may not contain undefined (what we got from the user)
|
||||||
[props (listof (listof Filter?))])
|
[props (listof (listof Filter?))])
|
||||||
(define-values (types expected-types props)
|
(define-values (types expected-types props)
|
||||||
(for/lists (t e p)
|
(for/lists (t e p)
|
||||||
([r (in-list results)]
|
([r (in-list results)]
|
||||||
|
@ -56,8 +56,8 @@
|
||||||
(make-ImpFilter (-filter (-val #f) n) f-)))))]
|
(make-ImpFilter (-filter (-val #f) n) f-)))))]
|
||||||
[((tc-results: ts (NoFilter:) _) (tc-results: e-ts (NoFilter:) _))
|
[((tc-results: ts (NoFilter:) _) (tc-results: e-ts (NoFilter:) _))
|
||||||
(values ts e-ts null)]))))
|
(values ts e-ts null)]))))
|
||||||
(w/c append-region ([p1 (listof Filter?)]
|
(with-cond-contract append-region ([p1 (listof Filter?)]
|
||||||
[p2 (listof Filter?)])
|
[p2 (listof Filter?)])
|
||||||
(define-values (p1 p2)
|
(define-values (p1 p2)
|
||||||
(combine-props (apply append props) (env-props (lexical-env)) (box #t))))
|
(combine-props (apply append props) (env-props (lexical-env)) (box #t))))
|
||||||
;; extend the lexical environment for checking the body
|
;; extend the lexical environment for checking the body
|
||||||
|
|
|
@ -12,7 +12,7 @@
|
||||||
(provide abstract-results)
|
(provide abstract-results)
|
||||||
|
|
||||||
|
|
||||||
(d/c (abstract-results results arg-names)
|
(define/cond-contract (abstract-results results arg-names)
|
||||||
(tc-results? (listof identifier?) . -> . (or/c Values? ValuesDots?))
|
(tc-results? (listof identifier?) . -> . (or/c Values? ValuesDots?))
|
||||||
(define keys (for/list ([(nm k) (in-indexed arg-names)]) k))
|
(define keys (for/list ([(nm k) (in-indexed arg-names)]) k))
|
||||||
(match results
|
(match results
|
||||||
|
@ -27,7 +27,7 @@
|
||||||
(make-Result t (abstract-filter arg-names keys f) (abstract-object arg-names keys o))))]))
|
(make-Result t (abstract-filter arg-names keys f) (abstract-object arg-names keys o))))]))
|
||||||
|
|
||||||
|
|
||||||
(d/c (abstract-object ids keys o)
|
(define/cond-contract (abstract-object ids keys o)
|
||||||
(-> (listof identifier?) (listof name-ref/c) Object? Object?)
|
(-> (listof identifier?) (listof name-ref/c) Object? Object?)
|
||||||
(define (lookup y)
|
(define (lookup y)
|
||||||
(for/first ([x ids] [i keys] #:when (free-identifier=? x y)) i))
|
(for/first ([x ids] [i keys] #:when (free-identifier=? x y)) i))
|
||||||
|
@ -39,16 +39,16 @@
|
||||||
[_ (make-Empty)]))
|
[_ (make-Empty)]))
|
||||||
|
|
||||||
|
|
||||||
(d/c (abstract-filter ids keys fs)
|
(define/cond-contract (abstract-filter ids keys fs)
|
||||||
(-> (listof identifier?) (listof name-ref/c) FilterSet/c FilterSet/c)
|
(-> (listof identifier?) (listof name-ref/c) FilterSet/c FilterSet/c)
|
||||||
(match fs
|
(match fs
|
||||||
[(FilterSet: f+ f-)
|
[(FilterSet: f+ f-)
|
||||||
(-FS (abo ids keys f+) (abo ids keys f-))]
|
(-FS (abo ids keys f+) (abo ids keys f-))]
|
||||||
[(NoFilter:) (-FS -top -top)]))
|
[(NoFilter:) (-FS -top -top)]))
|
||||||
|
|
||||||
(d/c (abo xs idxs f)
|
(define/cond-contract (abo xs idxs f)
|
||||||
((listof identifier?) (listof name-ref/c) Filter/c . -> . Filter/c)
|
((listof identifier?) (listof name-ref/c) Filter/c . -> . Filter/c)
|
||||||
(d/c (lookup y)
|
(define/cond-contract (lookup y)
|
||||||
(identifier? . -> . (or/c #f integer?))
|
(identifier? . -> . (or/c #f integer?))
|
||||||
(for/first ([x xs] [i idxs] #:when (free-identifier=? x y)) i))
|
(for/first ([x xs] [i idxs] #:when (free-identifier=? x y)) i))
|
||||||
(define-match-expander lookup:
|
(define-match-expander lookup:
|
||||||
|
@ -77,7 +77,7 @@
|
||||||
(provide combine-props tc-results->values)
|
(provide combine-props tc-results->values)
|
||||||
|
|
||||||
|
|
||||||
(d/c (resolve atoms prop)
|
(define/cond-contract (resolve atoms prop)
|
||||||
((listof Filter/c)
|
((listof Filter/c)
|
||||||
Filter/c
|
Filter/c
|
||||||
. -> .
|
. -> .
|
||||||
|
@ -102,7 +102,7 @@
|
||||||
[(cons (AndFilter: ps*) ps) (loop (append ps* ps))]
|
[(cons (AndFilter: ps*) ps) (loop (append ps* ps))]
|
||||||
[(cons p ps) (cons p (loop ps))])))
|
[(cons p ps) (cons p (loop ps))])))
|
||||||
|
|
||||||
(d/c (combine-props new-props old-props flag)
|
(define/cond-contract (combine-props new-props old-props flag)
|
||||||
((listof Filter/c) (listof Filter/c) (box/c boolean?)
|
((listof Filter/c) (listof Filter/c) (box/c boolean?)
|
||||||
. -> .
|
. -> .
|
||||||
(values (listof (or/c ImpFilter? OrFilter? AndFilter?)) (listof (or/c TypeFilter? NotTypeFilter?))))
|
(values (listof (or/c ImpFilter? OrFilter? AndFilter?)) (listof (or/c TypeFilter? NotTypeFilter?))))
|
||||||
|
|
|
@ -89,18 +89,18 @@
|
||||||
|
|
||||||
;; construct all the various types for structs, and then register the approriate names
|
;; construct all the various types for structs, and then register the approriate names
|
||||||
;; identifier listof[identifier] type listof[fld] listof[Type] boolean -> Type listof[Type] listof[Type]
|
;; identifier listof[identifier] type listof[fld] listof[Type] boolean -> Type listof[Type] listof[Type]
|
||||||
(d/c (mk/register-sty nm flds parent parent-fields types
|
(define/cond-contract (mk/register-sty nm flds parent parent-fields types
|
||||||
#:wrapper [wrapper values]
|
#:wrapper [wrapper values]
|
||||||
#:type-wrapper [type-wrapper values]
|
#:type-wrapper [type-wrapper values]
|
||||||
#:pred-wrapper [pred-wrapper values]
|
#:pred-wrapper [pred-wrapper values]
|
||||||
#:mutable [setters? #f]
|
#:mutable [setters? #f]
|
||||||
#:struct-info [si #f]
|
#:struct-info [si #f]
|
||||||
#:proc-ty [proc-ty #f]
|
#:proc-ty [proc-ty #f]
|
||||||
#:maker [maker* #f]
|
#:maker [maker* #f]
|
||||||
#:predicate [pred* #f]
|
#:predicate [pred* #f]
|
||||||
#:constructor-return [cret #f]
|
#:constructor-return [cret #f]
|
||||||
#:poly? [poly? #f]
|
#:poly? [poly? #f]
|
||||||
#:type-only [type-only #f])
|
#:type-only [type-only #f])
|
||||||
(c->* (identifier? (listof identifier?) (or/c Type/c #f) (listof fld?) (listof Type/c))
|
(c->* (identifier? (listof identifier?) (or/c Type/c #f) (listof fld?) (listof Type/c))
|
||||||
(#:wrapper procedure?
|
(#:wrapper procedure?
|
||||||
#:type-wrapper procedure?
|
#:type-wrapper procedure?
|
||||||
|
@ -144,15 +144,15 @@
|
||||||
;; generate names, and register the approriate types give field types and structure type
|
;; generate names, and register the approriate types give field types and structure type
|
||||||
;; optionally wrap things
|
;; optionally wrap things
|
||||||
;; identifier Type Listof[identifer] Listof[Type] Listof[Type] #:wrapper (Type -> Type) #:maker identifier
|
;; identifier Type Listof[identifer] Listof[Type] Listof[Type] #:wrapper (Type -> Type) #:maker identifier
|
||||||
(d/c (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
|
(define/cond-contract (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters?
|
||||||
#:wrapper [wrapper values]
|
#:wrapper [wrapper values]
|
||||||
#:struct-info [si #f]
|
#:struct-info [si #f]
|
||||||
#:type-wrapper [type-wrapper values]
|
#:type-wrapper [type-wrapper values]
|
||||||
#:pred-wrapper [pred-wrapper values]
|
#:pred-wrapper [pred-wrapper values]
|
||||||
#:maker [maker* #f]
|
#:maker [maker* #f]
|
||||||
#:predicate [pred* #f]
|
#:predicate [pred* #f]
|
||||||
#:poly? [poly? #f]
|
#:poly? [poly? #f]
|
||||||
#:constructor-return [cret #f])
|
#:constructor-return [cret #f])
|
||||||
(c->* (identifier? Struct? (listof identifier?) (listof Type/c) (listof Type/c) boolean?)
|
(c->* (identifier? Struct? (listof identifier?) (listof Type/c) (listof Type/c) boolean?)
|
||||||
(#:wrapper procedure?
|
(#:wrapper procedure?
|
||||||
#:type-wrapper procedure?
|
#:type-wrapper procedure?
|
||||||
|
@ -248,10 +248,10 @@
|
||||||
|
|
||||||
;; typecheck a non-polymophic struct and register the approriate types
|
;; typecheck a non-polymophic struct and register the approriate types
|
||||||
;; tc/struct : (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void
|
;; tc/struct : (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void
|
||||||
(d/c (tc/struct nm/par flds tys [proc-ty #f]
|
(define/cond-contract (tc/struct nm/par flds tys [proc-ty #f]
|
||||||
#:maker [maker #f] #:constructor-return [cret #f] #:mutable [mutable #f]
|
#:maker [maker #f] #:constructor-return [cret #f] #:mutable [mutable #f]
|
||||||
#:predicate [pred #f]
|
#:predicate [pred #f]
|
||||||
#:type-only [type-only #f])
|
#:type-only [type-only #f])
|
||||||
(c->* (syntax? (listof identifier?) (listof syntax?))
|
(c->* (syntax? (listof identifier?) (listof syntax?))
|
||||||
((or/c #f syntax?)
|
((or/c #f syntax?)
|
||||||
#:maker any/c
|
#:maker any/c
|
||||||
|
@ -283,7 +283,7 @@
|
||||||
;; register a struct type
|
;; register a struct type
|
||||||
;; convenience function for built-in structs
|
;; convenience function for built-in structs
|
||||||
;; tc/builtin-struct : identifier identifier Listof[identifier] Listof[Type] Listof[Type] -> void
|
;; tc/builtin-struct : identifier identifier Listof[identifier] Listof[Type] Listof[Type] -> void
|
||||||
(d/c (tc/builtin-struct nm parent flds tys #;parent-tys)
|
(define/cond-contract (tc/builtin-struct nm parent flds tys #;parent-tys)
|
||||||
(c-> identifier? (or/c #f identifier?) (listof identifier?)
|
(c-> identifier? (or/c #f identifier?) (listof identifier?)
|
||||||
(listof Type/c) #;(listof fld?)
|
(listof Type/c) #;(listof fld?)
|
||||||
any/c)
|
any/c)
|
||||||
|
|
|
@ -12,7 +12,7 @@
|
||||||
|
|
||||||
(provide (all-defined-out))
|
(provide (all-defined-out))
|
||||||
|
|
||||||
(d/c (open-Result r objs [ts #f])
|
(define/cond-contract (open-Result r objs [ts #f])
|
||||||
(->* (Result? (listof Object?)) ((listof Type/c)) (values Type/c FilterSet? Object?))
|
(->* (Result? (listof Object?)) ((listof Type/c)) (values Type/c FilterSet? Object?))
|
||||||
(match r
|
(match r
|
||||||
[(Result: t fs old-obj)
|
[(Result: t fs old-obj)
|
||||||
|
@ -23,7 +23,7 @@
|
||||||
(subst-filter-set fs k o #t arg-ty)
|
(subst-filter-set fs k o #t arg-ty)
|
||||||
(subst-object old-obj k o #t)))]))
|
(subst-object old-obj k o #t)))]))
|
||||||
|
|
||||||
(d/c (subst-filter-set fs k o polarity [t #f])
|
(define/cond-contract (subst-filter-set fs k o polarity [t #f])
|
||||||
(->* ((or/c FilterSet? NoFilter?) name-ref/c Object? boolean?) ((or/c #f Type/c)) FilterSet?)
|
(->* ((or/c FilterSet? NoFilter?) name-ref/c Object? boolean?) ((or/c #f Type/c)) FilterSet?)
|
||||||
(define extra-filter (if t (make-TypeFilter t null k) -top))
|
(define extra-filter (if t (make-TypeFilter t null k) -top))
|
||||||
(define (add-extra-filter f)
|
(define (add-extra-filter f)
|
||||||
|
@ -37,10 +37,10 @@
|
||||||
(subst-filter (add-extra-filter f-) k o polarity))]
|
(subst-filter (add-extra-filter f-) k o polarity))]
|
||||||
[_ (-FS -top -top)]))
|
[_ (-FS -top -top)]))
|
||||||
|
|
||||||
(d/c (subst-type t k o polarity)
|
(define/cond-contract (subst-type t k o polarity)
|
||||||
(-> Type/c name-ref/c Object? boolean? Type/c)
|
(-> Type/c name-ref/c Object? boolean? Type/c)
|
||||||
(define (st t) (subst-type t k o polarity))
|
(define (st t) (subst-type t k o polarity))
|
||||||
(d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity))
|
(define/cond-contract (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity))
|
||||||
(type-case (#:Type st
|
(type-case (#:Type st
|
||||||
#:Filter sf
|
#:Filter sf
|
||||||
#:Object (lambda (f) (subst-object f k o polarity)))
|
#:Object (lambda (f) (subst-object f k o polarity)))
|
||||||
|
@ -57,7 +57,7 @@
|
||||||
(and drest (cons (st (car drest)) (cdr drest)))
|
(and drest (cons (st (car drest)) (cdr drest)))
|
||||||
(map st kws)))]))
|
(map st kws)))]))
|
||||||
|
|
||||||
(d/c (subst-object t k o polarity)
|
(define/cond-contract (subst-object t k o polarity)
|
||||||
(-> Object? name-ref/c Object? boolean? Object?)
|
(-> Object? name-ref/c Object? boolean? Object?)
|
||||||
(match t
|
(match t
|
||||||
[(NoObject:) t]
|
[(NoObject:) t]
|
||||||
|
@ -72,7 +72,7 @@
|
||||||
t)]))
|
t)]))
|
||||||
|
|
||||||
;; this is the substitution metafunction
|
;; this is the substitution metafunction
|
||||||
(d/c (subst-filter f k o polarity)
|
(define/cond-contract (subst-filter f k o polarity)
|
||||||
(-> Filter/c name-ref/c Object? boolean? Filter/c)
|
(-> Filter/c name-ref/c Object? boolean? Filter/c)
|
||||||
(define (ap f) (subst-filter f k o polarity))
|
(define (ap f) (subst-filter f k o polarity))
|
||||||
(define (tf-matcher t p i k o polarity maker)
|
(define (tf-matcher t p i k o polarity maker)
|
||||||
|
@ -146,7 +146,7 @@
|
||||||
|
|
||||||
|
|
||||||
;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
|
;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
|
||||||
(d/c (values->tc-results tc formals)
|
(define/cond-contract (values->tc-results tc formals)
|
||||||
((or/c Values? ValuesDots?) (or/c #f (listof identifier?)) . -> . tc-results?)
|
((or/c Values? ValuesDots?) (or/c #f (listof identifier?)) . -> . tc-results?)
|
||||||
(match tc
|
(match tc
|
||||||
[(ValuesDots: (list (and rs (Result: ts fs os)) ...) dty dbound)
|
[(ValuesDots: (list (and rs (Result: ts fs os)) ...) dty dbound)
|
||||||
|
|
|
@ -89,11 +89,11 @@
|
||||||
#'(Mu: var (Union: (list (Value: '()) (MPair: elem-pat (F: var)))))])))
|
#'(Mu: var (Union: (list (Value: '()) (MPair: elem-pat (F: var)))))])))
|
||||||
|
|
||||||
|
|
||||||
(d/c (-result t [f -no-filter] [o -no-obj])
|
(define/cond-contract (-result t [f -no-filter] [o -no-obj])
|
||||||
(c:->* (Type/c) (FilterSet? Object?) Result?)
|
(c:->* (Type/c) (FilterSet? Object?) Result?)
|
||||||
(make-Result t f o))
|
(make-Result t f o))
|
||||||
|
|
||||||
(d/c (-values args)
|
(define/cond-contract (-values args)
|
||||||
(c:-> (listof Type/c) (or/c Type/c Values?))
|
(c:-> (listof Type/c) (or/c Type/c Values?))
|
||||||
(match args
|
(match args
|
||||||
;[(list t) t]
|
;[(list t) t]
|
||||||
|
@ -178,7 +178,7 @@
|
||||||
(define -no-obj (make-Empty))
|
(define -no-obj (make-Empty))
|
||||||
|
|
||||||
|
|
||||||
(d/c (-FS + -)
|
(define/cond-contract (-FS + -)
|
||||||
(c:-> Filter/c Filter/c FilterSet?)
|
(c:-> Filter/c Filter/c FilterSet?)
|
||||||
(match* (+ -)
|
(match* (+ -)
|
||||||
[((Bot:) _) (make-FilterSet -bot -top)]
|
[((Bot:) _) (make-FilterSet -bot -top)]
|
||||||
|
@ -219,9 +219,9 @@
|
||||||
|
|
||||||
(define top-func (make-Function (list (make-top-arr))))
|
(define top-func (make-Function (list (make-top-arr))))
|
||||||
|
|
||||||
(d/c (make-arr* dom rng
|
(define/cond-contract (make-arr* dom rng
|
||||||
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
|
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
|
||||||
#:filters [filters -no-filter] #:object [obj -no-obj])
|
#:filters [filters -no-filter] #:object [obj -no-obj])
|
||||||
(c:->* ((listof Type/c) (or/c Values? ValuesDots? Type/c))
|
(c:->* ((listof Type/c) (or/c Values? ValuesDots? Type/c))
|
||||||
(#:rest (or/c #f Type/c)
|
(#:rest (or/c #f Type/c)
|
||||||
#:drest (or/c #f (cons/c Type/c symbol?))
|
#:drest (or/c #f (cons/c Type/c symbol?))
|
||||||
|
@ -305,13 +305,13 @@
|
||||||
(define (-struct name parent flds constructor [proc #f] [poly #f] [pred #'dummy] [cert values])
|
(define (-struct name parent flds constructor [proc #f] [poly #f] [pred #'dummy] [cert values])
|
||||||
(make-Struct name parent flds proc poly pred cert constructor))
|
(make-Struct name parent flds proc poly pred cert constructor))
|
||||||
|
|
||||||
(d/c (-filter t i [p null])
|
(define/cond-contract (-filter t i [p null])
|
||||||
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
|
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
|
||||||
(if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
|
(if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
|
||||||
-top
|
-top
|
||||||
(make-TypeFilter t p i)))
|
(make-TypeFilter t p i)))
|
||||||
|
|
||||||
(d/c (-not-filter t i [p null])
|
(define/cond-contract (-not-filter t i [p null])
|
||||||
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
|
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
|
||||||
(if (or (type-equal? (make-Union null) t) (and (identifier? i) (is-var-mutated? i)))
|
(if (or (type-equal? (make-Union null) t) (and (identifier? i) (is-var-mutated? i)))
|
||||||
-top
|
-top
|
||||||
|
@ -329,7 +329,7 @@
|
||||||
(define (asym-pred dom rng filter)
|
(define (asym-pred dom rng filter)
|
||||||
(make-Function (list (make-arr* (list dom) rng #:filters filter))))
|
(make-Function (list (make-arr* (list dom) rng #:filters filter))))
|
||||||
|
|
||||||
(d/c make-pred-ty
|
(define/cond-contract make-pred-ty
|
||||||
(case-> (c:-> Type/c Type/c)
|
(case-> (c:-> Type/c Type/c)
|
||||||
(c:-> (listof Type/c) Type/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? Type/c)
|
||||||
|
|
|
@ -59,7 +59,7 @@
|
||||||
;; compact : (Listof prop) bool -> (Listof prop)
|
;; compact : (Listof prop) bool -> (Listof prop)
|
||||||
;; props : propositions to compress
|
;; props : propositions to compress
|
||||||
;; or? : is this an OrFilter (alternative is AndFilter)
|
;; or? : is this an OrFilter (alternative is AndFilter)
|
||||||
(d/c (compact props or?)
|
(define/cond-contract (compact props or?)
|
||||||
((listof Filter/c) boolean? . --> . (listof Filter/c))
|
((listof Filter/c) boolean? . --> . (listof Filter/c))
|
||||||
(define tf-map (make-hash))
|
(define tf-map (make-hash))
|
||||||
(define ntf-map (make-hash))
|
(define ntf-map (make-hash))
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
scheme/contract)
|
scheme/contract)
|
||||||
|
|
||||||
(provide resolve-name resolve-app needs-resolving? resolve)
|
(provide resolve-name resolve-app needs-resolving? resolve)
|
||||||
(p/c [resolve-once (Type/c . -> . (or/c Type/c #f))])
|
(provide/cond-contract [resolve-once (Type/c . -> . (or/c Type/c #f))])
|
||||||
|
|
||||||
(define-struct poly (name vars) #:prefab)
|
(define-struct poly (name vars) #:prefab)
|
||||||
|
|
||||||
|
|
|
@ -12,17 +12,17 @@
|
||||||
(struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted)
|
(struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted)
|
||||||
substitution/c make-simple-substitution)
|
substitution/c make-simple-substitution)
|
||||||
|
|
||||||
(d-s/c subst-rhs () #:transparent)
|
(define-struct/cond-contract subst-rhs () #:transparent)
|
||||||
(d-s/c (t-subst subst-rhs) ([type Type/c]) #:transparent)
|
(define-struct/cond-contract (t-subst subst-rhs) ([type Type/c]) #:transparent)
|
||||||
(d-s/c (i-subst subst-rhs) ([types (listof Type/c)]) #:transparent)
|
(define-struct/cond-contract (i-subst subst-rhs) ([types (listof Type/c)]) #:transparent)
|
||||||
(d-s/c (i-subst/starred subst-rhs) ([types (listof Type/c)] [starred Type/c]) #:transparent)
|
(define-struct/cond-contract (i-subst/starred subst-rhs) ([types (listof Type/c)] [starred Type/c]) #:transparent)
|
||||||
(d-s/c (i-subst/dotted subst-rhs) ([types (listof Type/c)] [dty Type/c] [dbound symbol?]) #: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 substitution/c (hash/c symbol? subst-rhs? #:immutable #t))
|
||||||
|
|
||||||
(define (subst v t e) (substitute t v e))
|
(define (subst v t e) (substitute t v e))
|
||||||
|
|
||||||
(d/c (make-simple-substitution vs ts)
|
(define/cond-contract (make-simple-substitution vs ts)
|
||||||
(([vs (listof symbol?)] [ts (listof Type/c)]) ()
|
(([vs (listof symbol?)] [ts (listof Type/c)]) ()
|
||||||
#:pre (vs ts) (= (length vs) (length ts))
|
#:pre (vs ts) (= (length vs) (length ts))
|
||||||
. ->i . [_ substitution/c])
|
. ->i . [_ substitution/c])
|
||||||
|
@ -31,7 +31,7 @@
|
||||||
|
|
||||||
|
|
||||||
;; substitute : Type Name Type -> Type
|
;; substitute : Type Name Type -> Type
|
||||||
(d/c (substitute image name target #:Un [Un (get-union-maker)])
|
(define/cond-contract (substitute image name target #:Un [Un (get-union-maker)])
|
||||||
((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
|
((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
|
||||||
(define (sb t) (substitute image name t))
|
(define (sb t) (substitute image name t))
|
||||||
(if (hash-ref (free-vars* target) name #f)
|
(if (hash-ref (free-vars* target) name #f)
|
||||||
|
@ -64,7 +64,7 @@
|
||||||
|
|
||||||
;; implements angle bracket substitution from the formalism
|
;; implements angle bracket substitution from the formalism
|
||||||
;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
|
;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
|
||||||
(d/c (substitute-dots images rimage name target)
|
(define/cond-contract (substitute-dots images rimage name target)
|
||||||
((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?)
|
((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?)
|
||||||
(define (sb t) (substitute-dots images rimage name t))
|
(define (sb t) (substitute-dots images rimage name t))
|
||||||
(if (or (hash-ref (free-idxs* target) name #f) (hash-ref (free-vars* target) name #f))
|
(if (or (hash-ref (free-idxs* target) name #f) (hash-ref (free-vars* target) name #f))
|
||||||
|
@ -140,7 +140,7 @@
|
||||||
;; substitute many variables
|
;; substitute many variables
|
||||||
;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
|
;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
|
||||||
;; subst-all : substitution Type -> Type
|
;; subst-all : substitution Type -> Type
|
||||||
(d/c (subst-all s t)
|
(define/cond-contract (subst-all s t)
|
||||||
(substitution/c Type? . -> . Type?)
|
(substitution/c Type? . -> . Type?)
|
||||||
(for/fold ([t t]) ([(v r) (in-hash s)])
|
(for/fold ([t t]) ([(v r) (in-hash s)])
|
||||||
(match r
|
(match r
|
||||||
|
|
|
@ -184,7 +184,7 @@
|
||||||
|
|
||||||
;(trace subtypes*/varargs)
|
;(trace subtypes*/varargs)
|
||||||
|
|
||||||
(d/c (combine-arrs arrs)
|
(define/cond-contract (combine-arrs arrs)
|
||||||
(c-> (listof arr?) (or/c #f arr?))
|
(c-> (listof arr?) (or/c #f arr?))
|
||||||
(match arrs
|
(match arrs
|
||||||
[(list (and a1 (arr: dom1 rng1 #f #f '())) (arr: dom rng #f #f '()) ...)
|
[(list (and a1 (arr: dom1 rng1 #f #f '())) (arr: dom rng #f #f '()) ...)
|
||||||
|
|
|
@ -70,17 +70,18 @@
|
||||||
(eq? t? (hash-ref tautology-contradiction-table e 'not-there)))
|
(eq? t? (hash-ref tautology-contradiction-table e 'not-there)))
|
||||||
(values (mk 'tautology) (mk 'contradiction) (mk 'neither))))
|
(values (mk 'tautology) (mk 'contradiction) (mk 'neither))))
|
||||||
|
|
||||||
(p/c [add-typeof-expr (syntax? tc-results? . -> . any/c)]
|
(provide/cond-contract
|
||||||
[type-of (syntax? . -> . tc-results?)]
|
[add-typeof-expr (syntax? tc-results? . -> . any/c)]
|
||||||
[reset-type-table (-> any/c)]
|
[type-of (syntax? . -> . tc-results?)]
|
||||||
[add-struct-fn! (identifier? StructPE? boolean? . -> . any/c)]
|
[reset-type-table (-> any/c)]
|
||||||
[struct-accessor? (identifier? . -> . (or/c #f StructPE?))]
|
[add-struct-fn! (identifier? StructPE? boolean? . -> . any/c)]
|
||||||
[struct-mutator? (identifier? . -> . (or/c #f StructPE?))]
|
[struct-accessor? (identifier? . -> . (or/c #f StructPE?))]
|
||||||
[struct-fn-idx (identifier? . -> . exact-integer?)]
|
[struct-mutator? (identifier? . -> . (or/c #f StructPE?))]
|
||||||
[make-struct-table-code (-> syntax?)]
|
[struct-fn-idx (identifier? . -> . exact-integer?)]
|
||||||
[add-tautology (syntax? . -> . any/c)]
|
[make-struct-table-code (-> syntax?)]
|
||||||
[add-contradiction (syntax? . -> . any/c)]
|
[add-tautology (syntax? . -> . any/c)]
|
||||||
[add-neither (syntax? . -> . any/c)]
|
[add-contradiction (syntax? . -> . any/c)]
|
||||||
[tautology? (syntax? . -> . boolean?)]
|
[add-neither (syntax? . -> . any/c)]
|
||||||
[contradiction? (syntax? . -> . boolean?)]
|
[tautology? (syntax? . -> . boolean?)]
|
||||||
[neither? (syntax? . -> . boolean?)])
|
[contradiction? (syntax? . -> . boolean?)]
|
||||||
|
[neither? (syntax? . -> . boolean?)])
|
||||||
|
|
|
@ -60,8 +60,8 @@
|
||||||
|
|
||||||
|
|
||||||
;; this structure represents the result of typechecking an expression
|
;; this structure represents the result of typechecking an expression
|
||||||
(d-s/c tc-result ([t Type/c] [f FilterSet/c] [o Object?]) #:transparent)
|
(define-struct/cond-contract tc-result ([t Type/c] [f FilterSet/c] [o Object?]) #:transparent)
|
||||||
(d-s/c tc-results ([ts (listof tc-result?)] [drest (or/c (cons/c Type/c symbol?) #f)]) #:transparent)
|
(define-struct/cond-contract tc-results ([ts (listof tc-result?)] [drest (or/c (cons/c Type/c symbol?) #f)]) #:transparent)
|
||||||
|
|
||||||
(define-match-expander tc-result:
|
(define-match-expander tc-result:
|
||||||
(syntax-parser
|
(syntax-parser
|
||||||
|
@ -133,7 +133,7 @@
|
||||||
|
|
||||||
;(trace ret)
|
;(trace ret)
|
||||||
|
|
||||||
(p/c
|
(provide/cond-contract
|
||||||
[ret
|
[ret
|
||||||
(->i ([t (or/c Type/c (listof Type/c))])
|
(->i ([t (or/c Type/c (listof Type/c))])
|
||||||
([f (t) (if (list? t)
|
([f (t) (if (list? t)
|
||||||
|
|
|
@ -163,14 +163,20 @@ at least theoretically.
|
||||||
|
|
||||||
|
|
||||||
;; turn contracts on and off - off by default for performance.
|
;; turn contracts on and off - off by default for performance.
|
||||||
(provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c d/c/p)
|
(provide (for-syntax enable-contracts?)
|
||||||
|
provide/cond-contract
|
||||||
|
with-cond-contract
|
||||||
|
cond-contracted
|
||||||
|
define-struct/cond-contract
|
||||||
|
define/cond-contract
|
||||||
|
define/cond-contract/provide)
|
||||||
|
|
||||||
(define-syntax-rule (d/c/p (name . args) c . body)
|
(define-syntax-rule (define/cond-contract/provide (name . args) c . body)
|
||||||
(begin (d/c (name . args) c . body)
|
(begin (define/cond-contract (name . args) c . body)
|
||||||
(p/c [name c])))
|
(provide/cond-contract [name c])))
|
||||||
|
|
||||||
;; these are versions of the contract forms conditionalized by `enable-contracts?'
|
;; these are versions of the contract forms conditionalized by `enable-contracts?'
|
||||||
(define-syntax p/c
|
(define-syntax provide/cond-contract
|
||||||
(if enable-contracts?
|
(if enable-contracts?
|
||||||
(make-rename-transformer #'provide/contract)
|
(make-rename-transformer #'provide/contract)
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
|
@ -186,7 +192,7 @@ at least theoretically.
|
||||||
[(_ c:clause ...)
|
[(_ c:clause ...)
|
||||||
#'(provide c.i ...)]))))
|
#'(provide c.i ...)]))))
|
||||||
|
|
||||||
(define-syntax w/c
|
(define-syntax with-cond-contract
|
||||||
(if enable-contracts?
|
(if enable-contracts?
|
||||||
(make-rename-transformer #'with-contract)
|
(make-rename-transformer #'with-contract)
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
|
@ -196,7 +202,7 @@ at least theoretically.
|
||||||
[(_ name specs . body)
|
[(_ name specs . body)
|
||||||
#'(begin . body)]))))
|
#'(begin . body)]))))
|
||||||
|
|
||||||
(define-syntax d/c
|
(define-syntax define/cond-contract
|
||||||
(if enable-contracts?
|
(if enable-contracts?
|
||||||
(make-rename-transformer #'define/contract)
|
(make-rename-transformer #'define/contract)
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
|
@ -204,14 +210,14 @@ at least theoretically.
|
||||||
[(_ head cnt . body)
|
[(_ head cnt . body)
|
||||||
#'(define head . body)]))))
|
#'(define head . body)]))))
|
||||||
|
|
||||||
(define-syntax d-s/c
|
(define-syntax define-struct/cond-contract
|
||||||
(if enable-contracts?
|
(if enable-contracts?
|
||||||
(make-rename-transformer #'define-struct/contract)
|
(make-rename-transformer #'define-struct/contract)
|
||||||
(syntax-rules ()
|
(syntax-rules ()
|
||||||
[(_ hd ([i c] ...) . opts)
|
[(_ hd ([i c] ...) . opts)
|
||||||
(define-struct hd (i ...) . opts)])))
|
(define-struct hd (i ...) . opts)])))
|
||||||
|
|
||||||
(define-signature-form (cnt stx)
|
(define-signature-form (cond-contracted stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ nm cnt)
|
[(_ nm cnt)
|
||||||
(if enable-contracts?
|
(if enable-contracts?
|
||||||
|
|
Loading…
Reference in New Issue
Block a user