(.module:
  [lux #*
   [abstract
    [monad (#+ do)]]
   [control
    ["." function]]
   [data
    ["." error]]
   [type
    ["." check (#+ Check)]]
   ["." macro]]
  ["." ///
   ["#." extension]
   [//
    ["/" analysis (#+ Operation)]]])

(def: #export (with-type expected)
  (All [a] (-> Type (Operation a) (Operation a)))
  (///extension.localized (get@ #.expected) (set@ #.expected)
                          (function.constant (#.Some expected))))

(def: #export (with-env action)
  (All [a] (-> (Check a) (Operation a)))
  (function (_ (^@ stateE [bundle state]))
    (case (action (get@ #.type-context state))
      (#error.Success [context' output])
      (#error.Success [[bundle (set@ #.type-context context' state)]
                       output])

      (#error.Failure error)
      ((/.fail error) stateE))))

(def: #export with-fresh-env
  (All [a] (-> (Operation a) (Operation a)))
  (///extension.localized (get@ #.type-context) (set@ #.type-context)
                          (function.constant check.fresh-context)))

(def: #export (infer actualT)
  (-> Type (Operation Any))
  (do ///.monad
    [expectedT (///extension.lift macro.expected-type)]
    (with-env
      (check.check expectedT actualT))))

(def: #export (with-inference action)
  (All [a] (-> (Operation a) (Operation [Type a])))
  (do ///.monad
    [[_ varT] (..with-env
                check.var)
     output (with-type varT
              action)
     knownT (..with-env
              (check.clean varT))]
    (wrap [knownT output])))