(;module:
  lux
  (lux (control monad
                ["ex" exception #+ exception:])
       (data [maybe]
             [text]
             text/format
             (coll [list "list/" Fold<List> Monoid<List> Monad<List>]))
       [meta]
       (meta [code]
             [type]
             (type ["tc" check])))
  (luxc ["&" base]
        (lang ["la" analysis #+ Analysis]
              (analysis ["&;" common]
                        ["&;" inference])
              [";L" variable #+ Variable])
        ["&;" scope]))

(exception: #export Invalid-Function-Type)
(exception: #export Cannot-Apply-Function)

## [Analysers]
(def: #export (analyse-function analyse func-name arg-name body)
  (-> &;Analyser Text Text Code (Meta Analysis))
  (do meta;Monad<Meta>
    [functionT meta;expected-type]
    (loop [expectedT functionT]
      (&;with-stacked-errors
        (function [_] (Invalid-Function-Type (%type expectedT)))
        (case expectedT
          (#;Named name unnamedT)
          (recur unnamedT)

          (#;Apply argT funT)
          (case (type;apply (list argT) funT)
            (#;Some value)
            (recur value)

            #;None
            (&;fail (format "Cannot apply type " (%type funT) " to  type " (%type argT))))
          
          (#;UnivQ _)
          (do @
            [[var-id var] (&;with-type-env
                            tc;existential)]
            (recur (maybe;assume (type;apply (list var) expectedT))))

          (#;ExQ _)
          (&common;with-var
            (function [[var-id var]]
              (recur (maybe;assume (type;apply (list var) expectedT)))))
          
          (#;Var id)
          (do @
            [? (&;with-type-env
                 (tc;concrete? id))]
            (if ?
              (do @
                [expectedT' (&;with-type-env
                              (tc;read id))]
                (recur expectedT'))
              ## Inference
              (&common;with-var
                (function [[input-id inputT]]
                  (&common;with-var
                    (function [[output-id outputT]]
                      (do @
                        [#let [funT (#;Function inputT outputT)]
                         funA (recur funT)
                         funT' (&;with-type-env
                                 (tc;clean output-id funT))
                         concrete-input? (&;with-type-env
                                           (tc;concrete? input-id))
                         funT'' (if concrete-input?
                                  (&;with-type-env
                                    (tc;clean input-id funT'))
                                  (wrap (type;univ-q +1 (&inference;replace-var input-id +1 funT'))))
                         _ (&;with-type-env
                             (tc;check expectedT funT''))]
                        (wrap funA))
                      ))))))

          (#;Function inputT outputT)
          (<| (:: @ map (function [[scope bodyA]]
                          (` ("lux function" [(~@ (list/map code;int (variableL;environment scope)))]
                              (~ bodyA)))))
              &;with-scope
              ## Functions have access not only to their argument, but
              ## also to themselves, through a local variable.
              (&scope;with-local [func-name expectedT])
              (&scope;with-local [arg-name inputT])
              (&;with-expected-type outputT)
              (analyse body))
          
          _
          (&;fail "")
          )))))

(def: #export (analyse-apply analyse funcT funcA args)
  (-> &;Analyser Type Analysis (List Code) (Meta Analysis))
  (&;with-stacked-errors
    (function [_]
      (Cannot-Apply-Function (format " Function: " (%type funcT) "\n"
                                     "Arguments:" (|> args
                                                      list;enumerate
                                                      (list/map (function [[idx argC]]
                                                                  (format "\n  " (%n idx) " " (%code argC))))
                                                      (text;join-with "")))))
    (do meta;Monad<Meta>
      [expectedT meta;expected-type
       [applyT argsA] (&inference;apply-function analyse funcT args)
       _ (&;with-type-env
           (tc;check expectedT applyT))]
      (wrap (la;apply argsA funcA)))))