    Copyright ( c )     ,    contributors .
;;   The use and distribution terms for this software are covered by the
;;   Eclipse Public License 1.0 (-1.0.php)
;;   which can be found in the file epl-v10.html at the root of this distribution.
;;   By using this software in any fashion, you are agreeing to be bound by
;;   the terms of this license.
;;   You must not remove this notice, or any other, from this software.

(ns typed.cljc.checker.check.do
  (:require [clojure.core.typed.ast-utils :as ast-u]
            [clojure.core.typed.contract-utils :as con]
            [clojure.core.typed.errors :as err]
            [clojure.core.typed.special-form :as spec]
            [clojure.core.typed.util-vars :as vs]
            [typed.cljc.checker.check.utils :as cu]
            [typed.cljc.checker.filter-ops :as fo]
            [typed.cljc.checker.filter-rep :as fl]
            [typed.cljc.checker.lex-env :as lex]
            [typed.cljc.checker.object-rep :as orep]
            [typed.cljc.checker.type-rep :as r]
            [typed.cljc.checker.update :as update]
            [typed.cljc.checker.utils :as u]
            [typed.cljc.checker.var-env :as var-env]))

(defn internal-form? [expr]
  (u/internal-form? expr spec/special-form))

(defn enforce-do-folding [{:keys [statements] :as expr} kw]
  (when-not (#{0 1} (count 
                      (filter #{kw}
                              (map :val statements))))
    (err/int-error (str "Folded special-forms detected " (ast-u/emit-form-fn expr)))))

(defn check-do [check internal-special-form expr expected]
  {:post [(-> % u/expr-type r/TCResult?)
          (vector? (:statements %))]}
  (enforce-do-folding expr spec/special-form)
  (cond
    (internal-form? expr)
    (internal-special-form expr expected)

    :else
    (let [exprs (conj (vec (:statements expr)) (:ret expr))
          #_#_
          _ (assert (every? (comp #{:unanalyzed} :op) exprs)
                    (mapv (juxt :op :form) exprs))
          nexprs (count exprs)
          reachable-atom (atom true)
          [env cexprs]
          (reduce (fn [[env cexprs] ^long n]
                    {:pre [(lex/PropEnv?-workaround env)
                           (integer? n)
                           (< n nexprs)]
                     ; :post checked after the reduce
                     }
                    (cond
                      (not @reachable-atom) [env (assoc-in cexprs [n u/expr-type]
                                                           (r/ret (r/Bottom)
                                                                  (fo/-unreachable-filter)
                                                                  orep/-empty))]
                      :else
                      (let [expr (get cexprs n)
                            _ (assert (map? expr))
                            cexpr (binding [; always prefer envs with :line information, even if inaccurate
                                            vs/*current-env* (if (:line (:env expr))
                                                               (:env expr)
                                                               vs/*current-env*)
                                            vs/*current-expr* expr]
                                    (var-env/with-lexical-env env
                                      (check expr
                                             ;propagate expected type only to final expression
                                             (when (= (inc n) nexprs)
                                               expected))))
                            res (u/expr-type cexpr)
                            {fs+ :then fs- :else} (r/ret-f res)
                            nenv (update/env+ env [(fo/-or fs+ fs-)] reachable-atom)
                            _ (u/trace-when-let
                                [ls (seq (cu/find-updated-locals (:l env) (:l nenv)))]
                                (str "Updated local in exceptional control flow (do): " ls))
_ ( prn  )
                            ]
                        (if @reachable-atom
                          ;reachable
                          [nenv (assoc cexprs n cexpr)]
                          ;unreachable
                          (do ;(prn "Detected unreachable code")
                              [nenv (assoc cexprs n
                                           (assoc cexpr 
                                                  u/expr-type (r/ret (r/Bottom)
                                                                     (fo/-unreachable-filter)
                                                                     orep/-empty)))])))))
                  [(lex/lexical-env) exprs] (range nexprs))
          _ (assert (= (count cexprs) nexprs))
          actual-types (mapv u/expr-type cexprs)
          _ (assert (lex/PropEnv?-workaround env))
          _ (assert ((every-pred vector? seq) cexprs)) ; make sure we conj'ed in the right order
          _ (assert ((every-pred (con/every-c? r/TCResult?) seq) actual-types)
                    actual-types)]
      ;(prn "do actual-types" actual-types)
      (assoc expr
             :statements (pop cexprs)
             :ret (peek cexprs)
should be a r / ret already

   The use and distribution terms for this software are covered by the
   Eclipse Public License 1.0 (-1.0.php)
   which can be found in the file epl-v10.html at the root of this distribution.
   By using this software in any fashion, you are agreeing to be bound by
   the terms of this license.
   You must not remove this notice, or any other, from this software.
 :post checked after the reduce
 always prefer envs with :line information, even if inaccurate
propagate expected type only to final expression
reachable
unreachable
(prn "Detected unreachable code")
 make sure we conj'ed in the right order
(prn "do actual-types" actual-types)
    Copyright ( c )     ,    contributors .

(ns typed.cljc.checker.check.do
  (:require [clojure.core.typed.ast-utils :as ast-u]
            [clojure.core.typed.contract-utils :as con]
            [clojure.core.typed.errors :as err]
            [clojure.core.typed.special-form :as spec]
            [clojure.core.typed.util-vars :as vs]
            [typed.cljc.checker.check.utils :as cu]
            [typed.cljc.checker.filter-ops :as fo]
            [typed.cljc.checker.filter-rep :as fl]
            [typed.cljc.checker.lex-env :as lex]
            [typed.cljc.checker.object-rep :as orep]
            [typed.cljc.checker.type-rep :as r]
            [typed.cljc.checker.update :as update]
            [typed.cljc.checker.utils :as u]
            [typed.cljc.checker.var-env :as var-env]))

(defn internal-form? [expr]
  (u/internal-form? expr spec/special-form))

(defn enforce-do-folding [{:keys [statements] :as expr} kw]
  (when-not (#{0 1} (count 
                      (filter #{kw}
                              (map :val statements))))
    (err/int-error (str "Folded special-forms detected " (ast-u/emit-form-fn expr)))))

(defn check-do [check internal-special-form expr expected]
  {:post [(-> % u/expr-type r/TCResult?)
          (vector? (:statements %))]}
  (enforce-do-folding expr spec/special-form)
  (cond
    (internal-form? expr)
    (internal-special-form expr expected)

    :else
    (let [exprs (conj (vec (:statements expr)) (:ret expr))
          #_#_
          _ (assert (every? (comp #{:unanalyzed} :op) exprs)
                    (mapv (juxt :op :form) exprs))
          nexprs (count exprs)
          reachable-atom (atom true)
          [env cexprs]
          (reduce (fn [[env cexprs] ^long n]
                    {:pre [(lex/PropEnv?-workaround env)
                           (integer? n)
                           (< n nexprs)]
                     }
                    (cond
                      (not @reachable-atom) [env (assoc-in cexprs [n u/expr-type]
                                                           (r/ret (r/Bottom)
                                                                  (fo/-unreachable-filter)
                                                                  orep/-empty))]
                      :else
                      (let [expr (get cexprs n)
                            _ (assert (map? expr))
                                            vs/*current-env* (if (:line (:env expr))
                                                               (:env expr)
                                                               vs/*current-env*)
                                            vs/*current-expr* expr]
                                    (var-env/with-lexical-env env
                                      (check expr
                                             (when (= (inc n) nexprs)
                                               expected))))
                            res (u/expr-type cexpr)
                            {fs+ :then fs- :else} (r/ret-f res)
                            nenv (update/env+ env [(fo/-or fs+ fs-)] reachable-atom)
                            _ (u/trace-when-let
                                [ls (seq (cu/find-updated-locals (:l env) (:l nenv)))]
                                (str "Updated local in exceptional control flow (do): " ls))
_ ( prn  )
                            ]
                        (if @reachable-atom
                          [nenv (assoc cexprs n cexpr)]
                              [nenv (assoc cexprs n
                                           (assoc cexpr 
                                                  u/expr-type (r/ret (r/Bottom)
                                                                     (fo/-unreachable-filter)
                                                                     orep/-empty)))])))))
                  [(lex/lexical-env) exprs] (range nexprs))
          _ (assert (= (count cexprs) nexprs))
          actual-types (mapv u/expr-type cexprs)
          _ (assert (lex/PropEnv?-workaround env))
          _ (assert ((every-pred (con/every-c? r/TCResult?) seq) actual-types)
                    actual-types)]
      (assoc expr
             :statements (pop cexprs)
             :ret (peek cexprs)
should be a r / ret already
