store/[org.clojure/core.typed "0.2.84"] clj::clojure.core.typed.check.let/check-let


(defn check-let [check {:keys [bindings] :as expr} expected & [{is-loop :loop? :keys [expected-bnds]}]]
  (let [_ (assert (contains? expr (ast-u/let-body-kw))
                  (keys expr))
        body ((ast-u/let-body-kw) expr)]
    (u/p :check/check-let
       (and is-loop (seq bindings) (not expected-bnds) )
         (err/tc-delayed-error "Loop requires more annotations")
         (assoc expr
                u/expr-type (r/ret (c/Un))))
       (let [[env cbindings] 
               (fn [[env cexprs] [{sym :name :keys [init] :as expr} expected-bnd]]
                 {:pre [(lex/PropEnv? env)
                        ((some-fn nil? r/Type?) expected-bnd)
                        (identical? (boolean expected-bnd) (boolean is-loop))]
                  :post [((con/hvector-c? lex/PropEnv? vector?) %)]}
                 (let [; check rhs
                       cinit (binding [vs/*current-expr* init]
                               (var-env/with-lexical-env env
                                 (check init (when is-loop
                                               (r/ret expected-bnd)))))
                       cexpr (assoc expr
                                    :init cinit
                                    u/expr-type (u/expr-type cinit))
                       {:keys [t fl flow o]} (u/expr-type cinit)
                       _ (when (and expected-bnd
                                    (not (sub/subtype? t expected-bnd)))
                             (str "Loop variable " sym " initialised to "
                                  (pr-str (prs/unparse-type t))
                                  ", expected " (pr-str (prs/unparse-type expected-bnd))
                                  "\n\nForm:\n\t" (ast-u/emit-form-fn init))))
                       t (or expected-bnd t)]
                     (fl/FilterSet? fl)
                     (let [{:keys [then else]} fl
                           p* (cond
                                (not (c/overlap t (c/Un r/-nil r/-false))) [then]
                                ;; n is being bound to an expression w/ object o
                                ;; we don't need any new info, aliasing and the
                                ;; lexical environment will have the needed info
                                (obj/Path? o) []

                                ;; n is being bound to an expression w/o an object
                                ;; so remember n in our propositions
                                :else [(fo/-or (fo/-and (fo/-not-filter (c/Un r/-nil r/-false) sym)
                                               (fo/-and (fo/-filter (c/Un r/-nil r/-false) sym) 
                           flow-f (r/flow-normal flow)
                           flow-atom (atom true)
                           new-env (-> env
                                       ;update binding type
                                       (lex/extend-env sym t o)
                                       ;update props
                                       (update-in [:props] #(set 
                                                              (apply concat 
                                                                     (update/combine-props p* % (atom true)))))
                                       (update/env+ [(if (= fl/-bot flow-f) fl/-top flow-f)] flow-atom))
                           _ (when-not @flow-atom 
                               (binding [vs/*current-expr* init]
                                   (str "Applying flow filter resulted in local being bottom"
                                        (with-out-str (print-env/print-env* new-env))
                                        "\nOld: "
                                        (with-out-str (print-env/print-env* env))))))]
                       [new-env (conj cexprs cexpr)])

                     (fl/NoFilter? fl) (do
                                         (assert (= (r/-flow fl/-top) flow))
                                         [(-> env
                                              ;no propositions to add, just update binding type
                                              (assoc-in [:l sym] t))
                                          (conj cexprs cexpr)])
                     :else (err/int-error (str "What is this?" fl)))))
               [lex/*lexical-env* []] (map vector bindings (or expected-bnds
                                                               (repeat nil))))

             cbody (var-env/with-lexical-env env
                     (if is-loop
                       (binding [recur-u/*recur-target* (recur-u/->RecurTarget expected-bnds nil nil nil)]
                         (check body expected))
                       (binding [vs/*current-expr* body]
                         (check body expected))))
             ;now we return a result to the enclosing scope, so we
             ;erase references to any bindings this scope introduces
             (reduce (fn [ty sym]
                       {:pre [(r/TCResult? ty)
                              (symbol? sym)]}
                       (-> ty
                           (update-in [:t] subst-obj/subst-type sym obj/-empty true)
                           (update-in [:fl] subst-obj/subst-filter-set sym obj/-empty true)
                           (update-in [:o] subst-obj/subst-object sym obj/-empty true)
                           (update-in [:flow :normal] subst-obj/subst-filter sym obj/-empty true)))
                     (u/expr-type cbody)
                     (map :name bindings))]
         (assoc expr
                (ast-u/let-body-kw) cbody
                :bindings cbindings
                u/expr-type unshadowed-ret))))))

Uses on crossclj