(.module:
  [lux #*
   [control
    [monad (#+ do)]
    pipe]
   [data
    [text
     format]
    [collection
     [list ("list/." Functor<List>)]
     ["." dictionary]]]
   ["." macro]
   [type (#+ :share)
    ["." check]]]
  ["." //
   ["." bundle]
   ["/." //
    ["." analysis
     ["." module]
     ["." type]]
    ["." synthesis]
    ["." translation]
    ["." statement (#+ Operation Handler Bundle)]]])

(def: (evaluate! type codeC)
  (All [anchor expression statement]
    (-> Type Code (Operation anchor expression statement [Type expression Any])))
  (do ///.Monad<Operation>
    [state (//.lift ///.get-state)
     #let [analyse (get@ [#statement.analysis #statement.phase] state)
           synthesize (get@ [#statement.synthesis #statement.phase] state)
           translate (get@ [#statement.translation #statement.phase] state)]
     [_ code//type codeA] (statement.lift-analysis
                           (analysis.with-scope
                             (type.with-fresh-env
                               (type.with-type type
                                 (do @
                                   [codeA (analyse codeC)]
                                   (wrap [type codeA]))))))
     codeS (statement.lift-synthesis
            (synthesize codeA))]
    (statement.lift-translation
     (translation.with-buffer
       (do @
         [codeT (translate codeS)
          count translation.next
          codeV (translation.evaluate! (format "evaluate" (%n count)) codeT)]
         (wrap [code//type codeT codeV]))))))

(def: (define! name ?type codeC)
  (All [anchor expression statement]
    (-> Name (Maybe Type) Code
        (Operation anchor expression statement [Type expression Text Any])))
  (do ///.Monad<Operation>
    [state (//.lift ///.get-state)
     #let [analyse (get@ [#statement.analysis #statement.phase] state)
           synthesize (get@ [#statement.synthesis #statement.phase] state)
           translate (get@ [#statement.translation #statement.phase] state)]
     [_ code//type codeA] (statement.lift-analysis
                           (analysis.with-scope
                             (type.with-fresh-env
                               (case ?type
                                 (#.Some type)
                                 (type.with-type type
                                   (do @
                                     [codeA (analyse codeC)]
                                     (wrap [type codeA])))

                                 #.None
                                 (do @
                                   [[code//type codeA] (type.with-inference (analyse codeC))
                                    code//type (type.with-env
                                                 (check.clean code//type))]
                                   (wrap [code//type codeA]))))))
     codeS (statement.lift-synthesis
            (synthesize codeA))]
    (statement.lift-translation
     (translation.with-buffer
       (do @
         [codeT (translate codeS)
          codeN+V (translation.define! name codeT)]
         (wrap [code//type codeT codeN+V]))))))

(def: lux::def
  Handler
  (function (_ extension-name phase inputsC+)
    (case inputsC+
      (^ (list [_ (#.Identifier ["" short-name])] valueC annotationsC))
      (do ///.Monad<Operation>
        [current-module (statement.lift-analysis
                         (//.lift macro.current-module-name))
         #let [full-name [current-module short-name]]
         [_ annotationsT annotationsV] (evaluate! Code annotationsC)
         #let [annotationsV (:coerce Code annotationsV)]
         [value//type valueT valueN valueV] (define! full-name
                                                     (if (macro.type? annotationsV)
                                                       (#.Some Type)
                                                       #.None)
                                                     valueC)
         _ (statement.lift-analysis
            (do @
              [_ (module.define short-name [value//type annotationsV valueV])]
              (if (macro.type? annotationsV)
                (case (macro.declared-tags annotationsV)
                  #.Nil
                  (wrap [])

                  tags
                  (module.declare-tags tags (macro.export? annotationsV) (:coerce Type valueV)))
                (wrap []))))
         #let [_ (log! (format "Definition " (%name full-name)))]]
        (statement.lift-translation
         (translation.learn full-name valueN)))

      _
      (///.throw //.invalid-syntax [extension-name]))))

(def: (alias! alias def-name)
  (-> Text Name (analysis.Operation Any))
  (do ///.Monad<Operation>
    [definition (//.lift (macro.find-def def-name))]
    (module.define alias definition)))

(def: def::module
  Handler
  (function (_ extension-name phase inputsC+)
    (case inputsC+
      (^ (list annotationsC))
      (do ///.Monad<Operation>
        [[_ annotationsT annotationsV] (evaluate! Code annotationsC)
         _ (statement.lift-analysis
            (module.set-annotations (:coerce Code annotationsV)))]
        (wrap []))

      _
      (///.throw //.invalid-syntax [extension-name]))))

(def: def::alias
  Handler
  (function (_ extension-name phase inputsC+)
    (case inputsC+
      (^ (list [_ (#.Identifier ["" alias])] [_ (#.Identifier def-name)]))
      (//.lift
       (///.sub [(get@ [#statement.analysis #statement.state])
                 (set@ [#statement.analysis #statement.state])]
                (alias! alias def-name)))

      _
      (///.throw //.invalid-syntax [extension-name]))))

(do-template [<mame> <type> <scope>]
  [(def: <mame>
     (All [anchor expression statement]
       (Handler anchor expression statement))
     (function (handler extension-name phase inputsC+)
       (case inputsC+
         (^ (list [_ (#.Text name)] valueC))
         (do ///.Monad<Operation>
           [[_ handlerT handlerV] (evaluate! (:of (:share [anchor expression statement]
                                                          {(Handler anchor expression statement)
                                                           handler}
                                                          {<type>
                                                           (:assume [])}))
                                             valueC)]
           (<| <scope>
               (//.install name)
               (:share [anchor expression statement]
                       {(Handler anchor expression statement)
                        handler}
                       {<type>
                        (:assume handlerV)})))

         _
         (///.throw //.invalid-syntax [extension-name]))))]

  [def::analysis    analysis.Handler                                  statement.lift-analysis]
  [def::synthesis   synthesis.Handler                                 statement.lift-synthesis]
  [def::translation (translation.Handler anchor expression statement) statement.lift-translation]
  [def::statement   (statement.Handler anchor expression statement)   (<|)]
  )

(def: bundle::def
  Bundle
  (<| (bundle.prefix "def")
      (|> bundle.empty
          (dictionary.put "module"      def::module)
          (dictionary.put "alias"       def::alias)
          (dictionary.put "analysis"    def::analysis)
          (dictionary.put "synthesis"   def::synthesis)
          (dictionary.put "translation" def::translation)
          (dictionary.put "statement"   def::statement)
          )))

(def: #export bundle
  Bundle
  (<| (bundle.prefix "lux")
      (|> bundle.empty
          (dictionary.put "def" lux::def)
          (dictionary.merge ..bundle::def))))