(.require
 [library
  [lux (.except)
   [control
    [monad (.only Monad do)]
    ["[0]" try (.only Try)]
    ["ex" exception (.only exception)]]
   [data
    ["[0]" text (.use "[1]#[0]" equivalence)
     ["%" \\format (.only format)]]]
   [type (.only sharing)
    ["[0]" check]]
   [compiler
    ["[0]" phase
     ["[0]" analysis
      ["[0]" module]
      ["[0]" type]]
     ["[0]" generation]
     ["[0]" declaration (.only State+ Operation)
      ["[0]" total]]
     ["[0]" extension]]
    ["[0]" default
     ["[0]" syntax]
     ["[0]" platform (.only Platform)]
     ["[0]" init]]
    ["[0]" cli (.only Configuration)]]
   [world
    ["[0]" file (.only File)]
    ["[0]" console (.only Console)]]]]
 ["[0]" /type])

(exception .public (error [message Text])
  message)

(def .public module "<INTERPRETER>")

(def fresh_source
  Source
  [[..module 1 0] 0 ""])

(def (add_line line [where offset input])
  (-> Text Source Source)
  [where offset (format input text.new_line line)])

(def exit_command
  Text
  "exit")

(def welcome_message
  Text
  (format text.new_line
          "Welcome to the interpreter!" text.new_line
          "Type '" ..exit_command "' to leave." text.new_line
          text.new_line))

(def farewell_message
  Text
  "Till next time...")

(def enter_module
  (All (_ anchor expression declaration)
    (Operation anchor expression declaration Any))
  (declaration.lifted_analysis
   (do phase.monad
     [_ (module.create 0 ..module)]
     (analysis.set_current_module ..module))))

(def (initialize Monad<!> Console<!> platform configuration generation_bundle)
  (All (_ ! anchor expression declaration)
    (-> (Monad !)
        (Console !) (Platform ! anchor expression declaration)
        Configuration
        (generation.Bundle anchor expression declaration)
        (! (State+ anchor expression declaration))))
  (do Monad<!>
    [state (platform.initialize platform generation_bundle)
     state (platform.compile platform
                             (has cli.#module syntax.prelude configuration)
                             (has [extension.#state
                                   declaration.#analysis declaration.#state
                                   extension.#state
                                   .#info .#mode]
                                  {.#Interpreter}
                                  state))
     [state _] (at (the platform.#file_system platform)
                   lift (phase.result' state enter_module))
     _ (at Console<!> write ..welcome_message)]
    (in state)))

(with_expansions [<Interpretation> (these (Operation anchor expression declaration [Type Any]))]
  
  (def (interpret_declaration code)
    (All (_ anchor expression declaration)
      (-> Code <Interpretation>))
    (do phase.monad
      [_ (total.phase code)
       _ init.refresh]
      (in [Any []])))

  (def (interpret_expression code)
    (All (_ anchor expression declaration)
      (-> Code <Interpretation>))
    (do [! phase.monad]
      [state (extension.lifted phase.state)
       .let [analyse (the [declaration.#analysis declaration.#phase] state)
             synthesize (the [declaration.#synthesis declaration.#phase] state)
             generate (the [declaration.#generation declaration.#phase] state)]
       [_ codeT codeA] (declaration.lifted_analysis
                        (analysis.with_scope
                          (type.with_fresh_env
                            (do !
                              [[codeT codeA] (type.with_inference
                                               (analyse code))
                               codeT (type.with_env
                                       (check.clean codeT))]
                              (in [codeT codeA])))))
       codeS (declaration.lifted_synthesis
              (synthesize codeA))]
      (declaration.lifted_generation
       (generation.with_buffer
         (do !
           [codeH (generate codeS)
            count generation.next
            codeV (generation.evaluate! (format "interpretation_" (%.nat count)) codeH)]
           (in [codeT codeV]))))))

  (def (interpret configuration code)
    (All (_ anchor expression declaration)
      (-> Configuration Code <Interpretation>))
    (function (_ state)
      (when (<| (phase.result' state)
                (sharing [anchor expression declaration]
                  (is (State+ anchor expression declaration)
                      state)
                  (is <Interpretation>
                      (interpret_declaration code))))
        {try.#Success [state' output]}
        {try.#Success [state' output]}

        {try.#Failure error}
        (if (ex.match? total.not_a_declaration error)
          (<| (phase.result' state)
              (sharing [anchor expression declaration]
                (is (State+ anchor expression declaration)
                    state)
                (is <Interpretation>
                    (interpret_expression code))))
          {try.#Failure error}))))
  )

(def (execute configuration code)
  (All (_ anchor expression declaration)
    (-> Configuration Code (Operation anchor expression declaration Text)))
  (do phase.monad
    [[codeT codeV] (interpret configuration code)
     state phase.state]
    (in (/type.represent (the [extension.#state
                               declaration.#analysis declaration.#state
                               extension.#state]
                              state)
                         codeT
                         codeV))))

(type (Context anchor expression declaration)
  (Record
   [#configuration Configuration
    #state (State+ anchor expression declaration)
    #source Source]))

(with_expansions [<Context> (these (Context anchor expression declaration))]
  (def (read_eval_print context)
    (All (_ anchor expression declaration)
      (-> <Context> (Try [<Context> Text])))
    (do try.monad
      [.let [[_where _offset _code] (the #source context)]
       [source' input] (syntax.parse ..module syntax.no_aliases (text.size _code) (the #source context))
       [state' representation] (let [... TODO: Simplify ASAP
                                     state (sharing [anchor expression declaration]
                                             (is <Context>
                                                 context)
                                             (is (State+ anchor expression declaration)
                                                 (the #state context)))]
                                 (<| (phase.result' state)
                                     ... TODO: Simplify ASAP
                                     (sharing [anchor expression declaration]
                                       (is <Context>
                                           context)
                                       (is (Operation anchor expression declaration Text)
                                           (execute (the #configuration context) input)))))]
      (in [(|> context
               (has #state state')
               (has #source source'))
           representation]))))

(def .public (run! Monad<!> Console<!> platform configuration generation_bundle)
  (All (_ ! anchor expression declaration)
    (-> (Monad !)
        (Console !) (Platform ! anchor expression declaration)
        Configuration
        (generation.Bundle anchor expression declaration)
        (! Any)))
  (do [! Monad<!>]
    [state (initialize Monad<!> Console<!> platform configuration)]
    (loop (again [context [#configuration configuration
                           #state state
                           #source ..fresh_source]
                  multi_line? false])
      (do !
        [_ (if multi_line?
             (at Console<!> write "  ")
             (at Console<!> write "> "))
         line (at Console<!> read_line)]
        (if (and (not multi_line?)
                 (text#= ..exit_command line))
          (at Console<!> write ..farewell_message)
          (when (read_eval_print (revised #source (add_line line) context))
            {try.#Success [context' representation]}
            (do !
              [_ (at Console<!> write representation)]
              (again context' false))

            {try.#Failure error}
            (if (ex.match? syntax.end_of_file error)
              (again context true)
              (exec (log! (ex.error ..error error))
                (again (has #source ..fresh_source context) false))))))
      )))