order-of-evaluation props

Use props from checking a function to check its first argument,
use props from checking the first argument to check the second,
and so on.

Author: bennn

typed-racket-lib/typed-racket/typecheck/signatures.rkt

@@ -14,6 +14,7 @@
    [cond-contracted tc-body/check (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]
    [cond-contracted tc-expr/t (syntax? . -> . Type?)]
    [cond-contracted single-value ((syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]
+   [cond-contracted map-single-value ((listof syntax?) . -> . (listof full-tc-results/c))]
    [cond-contracted tc-dep-fun-arg ((syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]))
 
 (define-signature check-subforms^

typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt

@@ -9,7 +9,7 @@
          "../signatures.rkt" "../tc-funapp.rkt"
          (types abbrev utils prop-ops)
          (env lexical-env)
-         (typecheck tc-subst tc-envops check-below)
+         (typecheck tc-subst tc-envops check-below tc-metafunctions)
          (rep type-rep prop-rep object-rep values-rep))
 
 (import tc-expr^ tc-app-keywords^
@@ -80,8 +80,10 @@
 (define (tc/app-regular form expected)
   (syntax-case form ()
     [(f . args)
-     (let ([f-ty (tc-expr/t #'f)]
-           [args* (syntax->list #'args)])
+     (let* ([f-res (single-value #'f)]
+            [f-ty (match f-res [(tc-result1: t _ _) t])]
+            [f-prop (unconditional-prop f-res)]
+            [args* (syntax->list #'args)])
        (define (matching-arities arrs)
          (for/list ([arr (in-list arrs)] #:when (arrow-matches? arr args*)) arr))
        (define (has-drest/props? arrs)
@@ -94,7 +96,8 @@
             (cond
               [(with-refinements?)
                (map tc-dep-fun-arg args*)]
-              [else (map single-value args*)]))
+              [else
+               (map-single-value args* (list f-prop))]))
           (tc/funapp #'f #'args f-ty arg-types expected)]
          [(or (? DepFun?)
               (Poly-unsafe: _ (? DepFun?)))
@@ -119,5 +122,5 @@
                  (single-value arg-stx (ret dom-ty))]
                 [else (single-value arg-stx)])))
           (tc/funapp #'f #'args f-ty arg-types expected)]
-         [_ (tc/funapp #'f #'args f-ty (map single-value args*) expected)]))]))
+         [_ (tc/funapp #'f #'args f-ty (map-single-value args* (list f-prop)) expected)]))]))
 

typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt

@@ -16,7 +16,7 @@
          racket/list
          racket/private/class-internal
          syntax/parse
-         (typecheck internal-forms tc-envops)
+         (typecheck internal-forms tc-envops tc-metafunctions)
          racket/sequence
          racket/extflonum
          ;; Needed for current implementation of typechecking letrec-syntax+values
@@ -352,6 +352,25 @@
           #:stx form
           "expected single value, got multiple (or zero) values")]))
 
+;; Apply `single-value` to a list of forms in order, accumulate the prop info
+(define (map-single-value forms [props '()])
+  (define any-res (-tc-any-results #f))
+  (let loop ((forms forms)
+             (props props))
+    (match forms
+     ['()
+      '()]
+     [(cons e rst)
+      (define tcr
+        (with-lexical-env+props
+          props
+          #:expected any-res
+          #:unreachable (for-each register-ignored! rst)
+          (single-value e)))
+      (define prop+
+        (cons (unconditional-prop tcr) props))
+      (cons tcr (loop rst prop+))])))
+
 (define (tc-dep-fun-arg form [expected #f])
   (define t (tc-expr/check form expected #t))
   (match t

typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt

@@ -13,7 +13,8 @@
          combine-props
          merge-tc-results
          tc-results->values
-         erase-existentials)
+         erase-existentials
+         unconditional-prop)
 
 ;; Objects representing the rest argument are currently not supported
 (define/cond-contract (abstract-results results arg-names #:rest-id [rest-id #f])

typed-racket-test/unit-tests/typecheck-tests.rkt

@@ -4467,6 +4467,9 @@
         [tc-e/t (let: ([x : (Un Flonum Natural) 0.0])
                   (if (not (natural? x)) x 1.0))
                -Flonum]
+        ;; props + evaluation order
+        [tc-e ((lambda: ((x : (Un Symbol Natural))) (+ (assert x integer?) x)) 1) -Nat]
+        [tc-e ((lambda: ((x : (Un Symbol Natural))) ((begin (assert x integer?) +) x x)) 1) -Nat]
        )
 
   (test-suite