Permalink
Browse files

propagate expected type info further down AST

Previously expected propositions were erased frequently
(at lets and ifs) and checking for logical entailment
was unidirectional instead of bidirectional. In other words,
instead of checking if propositions held at the leaves
of the AST, we would typecheck the AST and blindly propagate
up ALL logical info we learned at each step. This meant that
we would get exponential blow up of propositions even when
we didn't care about their content.

With this commit, instead now we send down expected types
*and* propositions so we can verify expected types and
propisitions are satisfied at leaves, thereby relieving the
need to constantly report up huge amounts of logical info
while typechecking.
  • Loading branch information...
pnwamk committed Dec 18, 2016
1 parent aa1d36f commit be155fa3e3236caa93ef927e205c45b00d6d6e6e
@@ -220,12 +220,12 @@
(substitute (make-F var) v ty*))))
-(define/cond-contract (cgen/prop context s t)
+(define/cond-contract (cgen/prop context p q)
(context? Prop? Prop? . -> . (or/c #f cset?))
- (match* (s t)
- [(e e) (empty-cset/context context)]
- [(e (TrueProp:)) (empty-cset/context context)]
- [((FalseProp:) e) (empty-cset/context context)]
+ (match* (p q)
+ [(p p) (empty-cset/context context)]
+ [(p (TrueProp:)) (empty-cset/context context)]
+ [((FalseProp:) q) (empty-cset/context context)]
;; FIXME - is there something to be said about the logical ones?
[((TypeProp: o s) (TypeProp: o t)) (cgen/inv context s t)]
[((NotTypeProp: o s) (NotTypeProp: o t)) (cgen/inv context s t)]
@@ -919,7 +919,7 @@
(substs-gen m X (list dotted-var) R #f)))
-;(trace subst-gen)
+;(trace substs-gen)
;(trace cgen)
;(trace cgen/list)
;(trace cgen/arr)
@@ -3,19 +3,19 @@
(require "../utils/utils.rkt"
racket/match (prefix-in - (contract-req))
racket/format
- (types utils subtype prop-ops abbrev)
+ (env lexical-env)
+ (types utils subtype prop-ops abbrev tc-result)
(utils tc-utils)
(rep type-rep object-rep prop-rep)
- (typecheck error-message))
+ (typecheck error-message tc-envops))
(provide/cond-contract
[check-below (-->i ([s (-or/c Type? full-tc-results/c)]
[t (s) (if (Type? s) Type? tc-results/c)])
[_ (s) (if (Type? s) Type? full-tc-results/c)])]
[cond-check-below (-->i ([s (-or/c Type? full-tc-results/c)]
[t (s) (-or/c #f (if (Type? s) Type? tc-results/c))])
- [_ (s) (-or/c #f (if (Type? s) Type? full-tc-results/c))])]
- [fix-results (--> tc-results/c full-tc-results/c)])
+ [_ (s) (-or/c #f (if (Type? s) Type? full-tc-results/c))])])
(provide type-mismatch)
@@ -45,38 +45,6 @@
(value-string expected) (value-string actual)
"mismatch in number of values"))
-;; fix-props:
-;; PropSet [PropSet] -> PropSet
-;; or
-;; Prop [Prop] -> Prop
-;; Turns #f prop/propset into the actual prop; leaves other props alone.
-(define (fix-props p1 [p2 -tt-propset])
- (or p1 p2))
-
-;; fix-object: Object [Object] -> Object
-;; Turns #f into the actual object; leaves other objects alone.
-(define (fix-object o1 [o2 -empty-obj])
- (or o1 o2))
-
-;; fix-results: tc-results -> tc-results
-;; Turns #f Prop or Obj into the Empty/Trivial
-(define (fix-results r)
- (match r
- [(tc-any-results: f) (tc-any-results (fix-props f -tt))]
- [(tc-results: ts ps os)
- (ret ts (map fix-props ps) (map fix-object os))]
- [(tc-results: ts ps os dty dbound)
- (ret ts (map fix-props ps) (map fix-object os) dty dbound)]))
-
-(define (fix-results/bottom r)
- (match r
- [(tc-any-results: f) (tc-any-results (fix-props f -ff))]
- [(tc-results: ts ps os)
- (ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os))]
- [(tc-results: ts ps os dty dbound)
- (ret ts (for/list ([p ps]) (fix-props p -ff-propset)) (map fix-object os) dty dbound)]))
-
-
;; check-below : (/\ (Results Type -> Result)
;; (Results Results -> Result)
@@ -88,8 +56,18 @@
[(p p) #t]
[(p #f) #t]
[((PropSet: p1+ p1-) (PropSet: p2+ p2-))
- (and (implies? p1+ p2+)
- (implies? p1- p2-))]
+ (define positive-implies?
+ (or (TrueProp? p2+)
+ (FalseProp? p1+)
+ (let ([p1-and-not-p2 (-and p1+ (negate-prop p2+))])
+ (or (FalseProp? p1-and-not-p2)
+ (impossible-in-lexical-env? p1-and-not-p2)))))
+ (and positive-implies?
+ (or (TrueProp? p2-)
+ (FalseProp? p1-)
+ (let ([p1-and-not-p2 (-and p1- (negate-prop p2-))])
+ (or (FalseProp? p1-and-not-p2)
+ (impossible-in-lexical-env? p1-and-not-p2)))))]
[(_ _) #f]))
(define (object-better? o1 o2)
(match* (o1 o2)
@@ -6,6 +6,7 @@
(contract-req)
(rep type-rep prop-rep object-rep rep-utils)
(utils tc-utils)
+ racket/set
(types tc-result resolve subtype update prop-ops)
(env type-env-structs lexical-env mvar-env)
(rename-in (types abbrev)
@@ -14,64 +15,82 @@
[one-of/c -one-of/c])
(typecheck tc-metafunctions))
-(provide with-lexical-env/extend-props)
+(provide with-lexical-env+props
+ impossible-in-lexical-env?)
+
+(define (impossible-in-lexical-env? p)
+ (not (env+ (lexical-env) (list p))))
;; Returns #f if anything becomes (U)
(define (env+ env ps)
- (define-values (props atoms) (combine-props ps (env-props env)))
(cond
- [props
- (let loop ([ps atoms]
- [negs '()]
- [Γ (env-replace-props env props)])
- (match ps
- [(cons p ps)
- (match p
- [(TypeProp: (Path: lo x) pt)
- #:when (and (not (is-var-mutated? x))
- (identifier-binding x))
- (let* ([t (lookup-type/lexical x Γ #:fail (lambda _ Univ))]
- [new-t (update t pt #t lo)])
- (if (Bottom? new-t)
- (values #f '())
- (loop ps negs (env-set-type Γ x new-t))))]
- ;; process negative info _after_ positive info so we don't miss anything
- [(NotTypeProp: (Path: _ x) _)
- #:when (and (not (is-var-mutated? x))
- (identifier-binding x))
- (loop ps (cons p negs) Γ)]
- [_ (loop ps negs Γ)])]
- [_ (let ([Γ (let loop ([negs negs]
- [Γ Γ])
- (match negs
- [(cons (NotTypeProp: (Path: lo x) pt) rst)
- (let* ([t (lookup-type/lexical x Γ #:fail (lambda _ Univ))]
- [new-t (update t pt #f lo)])
- (if (Bottom? new-t)
- #f
- (loop rst (env-set-type Γ x new-t))))]
- [_ Γ]))])
- (values Γ atoms))]))]
- [else (values #f '())]))
+ [(null? ps) env]
+ [else
+ (define-values (props atoms) (combine-props ps (env-props env)))
+ (cond
+ [props
+ (let loop ([ps atoms]
+ [negs '()]
+ [Γ (env-replace-props env props)])
+ (match ps
+ [(cons p ps)
+ (match p
+ [(TypeProp: (Path: lo x) pt)
+ #:when (and (not (is-var-mutated? x))
+ (identifier-binding x))
+ (let* ([t (lookup-type/lexical x Γ #:fail (λ (_) Univ))]
+ [new-t (update t pt #t lo)])
+ (and (not (Bottom? new-t))
+ (loop ps negs (env-set-type Γ x new-t))))]
+ ;; process negative info _after_ positive info so we don't miss anything
+ [(NotTypeProp: (Path: _ x) _)
+ #:when (and (not (is-var-mutated? x))
+ (identifier-binding x))
+ (loop ps (cons p negs) Γ)]
+ [_ (loop ps negs Γ)])]
+ [_ (let ([Γ (let loop ([negs negs]
+ [Γ Γ])
+ (match negs
+ [(cons (NotTypeProp: (Path: lo x) pt) rst)
+ (let* ([t (lookup-type/lexical x Γ #:fail (λ (_) Univ))]
+ [new-t (update t pt #f lo)])
+ (and (not (Bottom? new-t))
+ (loop rst (env-set-type Γ x new-t))))]
+ [_ Γ]))])
+ (and Γ (env-replace-props Γ (append atoms (env-props Γ)))))]))]
+ [else #f])]))
+
-;; run code in an extended env and with replaced props. Requires the body to return a tc-results.
-;; TODO make this only add the new prop instead of the entire environment once tc-id is fixed to
-;; include the interesting props in its prop.
-;; TODO figure out what the heck the above TODO means -amk
+;; run code in an extended env and with replaced props.
+;; Requires the body to return a tc-results.
;; WARNING: this may bail out when code is unreachable
-(define-syntax (with-lexical-env/extend-props stx)
+(define-syntax (with-lexical-env+props stx)
(define-splicing-syntax-class unreachable?
(pattern (~seq #:unreachable form:expr))
(pattern (~seq) #:with form #'(begin)))
(syntax-parse stx
- [(_ ps:expr u:unreachable? . b)
- #'(let-values ([(new-env atoms) (env+ (lexical-env) ps)])
+ [(_ ps:expr
+ #:expected expected
+ u:unreachable? . b)
+ (syntax/loc stx
+ (let ([old-props (env-props (lexical-env))]
+ [new-env (env+ (lexical-env) ps)])
(cond
[new-env
(with-lexical-env
- new-env
- (add-unconditional-prop (let () . b) (apply -and (append atoms (env-props new-env)))))]
+ new-env
+ (let ([result (let () . b)])
+ (match expected
+ ;; if there was not any expected results, then
+ ;; return any new info that was learned while
+ ;; extending the environment
+ [(or #f (tc-any-results: #f))
+ (define new-props
+ (make-AndProp (set-subtract (env-props new-env) old-props)))
+ (add-unconditional-prop result new-props)]
+ ;; otherwise, just return the expected results
+ [_ (fix-results expected)])))]
[else
;; unreachable, bail out
u.form
- (ret -Bottom)]))]))
+ (ret -Bottom)])))]))
@@ -339,33 +339,29 @@
;; Body must be a non empty sequence of expressions to typecheck.
;; The final one will be checked against expected.
(define (tc-body/check body expected)
- (match (syntax->list body)
- [(list es ... e-final)
- ;; First, typecheck all the forms whose results are discarded.
- ;; If any one those causes the rest to be unreachable (e.g. `exit' or `error`,
- ;; then mark the rest as ignored.
- (let loop ([es es])
- (cond [(empty? es) ; Done, typecheck the return form.
- (tc-expr/check e-final expected)]
- [else
- ;; Typecheck the first form.
- (define e (first es))
- (define results (tc-expr/check e (tc-any-results #f)))
- (define props
- (match results
- [(tc-any-results: f) (list f)]
- [(tc-results: _ (list (PropSet: p+ p-) ...) _)
- (map -or p+ p-)]
- [(tc-results: _ (list (PropSet: p+ p-) ...) _ _ _)
- (map -or p+ p-)]))
- (with-lexical-env/extend-props
- props
- ;; If `e` bails out, mark the rest as ignored.
- #:unreachable (for ([x (in-list (cons e-final (rest es)))])
- (register-ignored! x))
- ;; Keep going with an environment extended with the propositions that are
- ;; true if execution reaches this point.
- (loop (rest es)))]))]))
+ (define any-res (tc-any-results #f))
+ (define exps (syntax->list body))
+ (let loop ([exps exps])
+ (match exps
+ [(list tail-exp) (tc-expr/check tail-exp expected)]
+ [(cons e rst)
+ (define results (tc-expr/check e any-res))
+ (define props
+ (match results
+ [(tc-any-results: p) (list p)]
+ [(tc-results: _ (list (PropSet: p+ p-) ...) _)
+ (map -or p+ p-)]
+ [(tc-results: _ (list (PropSet: p+ p-) ...) _ _ _)
+ (map -or p+ p-)]))
+ (with-lexical-env+props
+ props
+ #:expected any-res
+ ;; If `e` bails out, mark the rest as ignored.
+ #:unreachable (for-each register-ignored! rst)
+ ;; Keep going with an environment extended with the
+ ;; propositions that are true if execution reaches this
+ ;; point.
+ (loop rst))])))
;; find-stx-type : Any [(or/c Type? #f)] -> Type?
;; recursively find the type of either a syntax object or the result of syntax-e
@@ -8,7 +8,7 @@
(for-syntax syntax/parse racket/base)
(types utils subtype resolve abbrev
substitute classes prop-ops)
- (typecheck tc-metafunctions tc-app-helper)
+ (typecheck tc-metafunctions tc-app-helper tc-subst)
(rep type-rep)
(r:infer infer))
@@ -35,8 +35,15 @@
#:name (and (identifier? f-stx) f-stx)
#:expected expected))))]))
+(define (subst-dom-objs argtys argobjs rng)
+ (subst-rep rng (for/list ([o (in-list argobjs)]
+ [t (in-list argtys)]
+ [idx (in-naturals)]
+ #:when (not (Empty? o)))
+ (list (cons 0 idx) o t))))
+
(define (tc/funapp f-stx args-stx f-type args-res expected)
- (match-define (list (tc-result1: argtys (PropSet: argps+ argps-) _) ...) args-res)
+ (match-define (list (tc-result1: argtys (PropSet: argps+ argps-) argobjs) ...) args-res)
(define result
(match f-type
;; we special-case this (no case-lambda) for improved error messages
@@ -74,18 +81,19 @@
;; Only try to infer the free vars of the rng (which includes the vars
;; in props/objects).
(λ (dom rng rest drest a)
- (extend-tvars fixed-vars
- (cond
- [drest
- (infer/dots
- fixed-vars dotted-var argtys dom (car drest) rng (fv rng)
- #:expected (and expected (tc-results->values expected)))]
- [rest
- (infer/vararg fixed-vars (list dotted-var) argtys dom rest rng
- (and expected (tc-results->values expected)))]
- ;; no rest or drest
- [else (infer fixed-vars (list dotted-var) argtys dom rng
- (and expected (tc-results->values expected)))])))
+ (let ([rng (subst-dom-objs argtys argobjs rng)])
+ (extend-tvars fixed-vars
+ (cond
+ [drest
+ (infer/dots
+ fixed-vars dotted-var argtys dom (car drest) rng (fv rng)
+ #:expected (and expected (tc-results->values expected)))]
+ [rest
+ (infer/vararg fixed-vars (list dotted-var) argtys dom rest rng
+ (and expected (tc-results->values expected)))]
+ ;; no rest or drest
+ [else (infer fixed-vars (list dotted-var) argtys dom rng
+ (and expected (tc-results->values expected)))]))))
f-type args-res expected)]
;; regular polymorphic functions without dotted rest,
;; we do not choose any instantiations with mandatory keyword arguments
@@ -99,9 +107,10 @@
;; Only try to infer the free vars of the rng (which includes the vars
;; in props/objects).
(λ (dom rng rest kw? a)
- (extend-tvars vars
- (infer/vararg vars null argtys dom rest rng
- (and expected (tc-results->values expected)))))
+ (let ([rng (subst-dom-objs argtys argobjs rng)])
+ (extend-tvars vars
+ (infer/vararg vars null argtys dom rest rng
+ (and expected (tc-results->values expected))))))
f-type args-res expected)]
;; Row polymorphism. For now we do really dumb inference that only works
;; in very restricted cases, but is probably enough for most cases in
Oops, something went wrong.

0 comments on commit be155fa

Please sign in to comment.