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

(do-template [<name>]
  [(exception: #export (<name> {message Text})
     message)]

  [Cannot-Analyse-Function]
  [Invalid-Function-Type]
  [Cannot-Apply-Function]
  )

## [Analysers]
(def: #export (analyse-function analyse func-name arg-name body)
  (-> &.Analyser Text Text Code (Meta Analysis))
  (do macro.Monad<Meta>
    [functionT macro.expected-type]
    (loop [expectedT functionT]
      (&.with-stacked-errors
        (function (_ _)
          (ex.construct Cannot-Analyse-Function
                        (format "    Type: " (%type expectedT) "\n"
                                "Function: " func-name "\n"
                                "Argument: " arg-name "\n"
                                "    Body: " (%code body))))
        (case expectedT
          (#.Named name unnamedT)
          (recur unnamedT)

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

            #.None
            (&.throw Invalid-Function-Type (%type expectedT)))

          (^template [<tag> <instancer>]
            (<tag> _)
            (do @
              [[_ instanceT] (&.with-type-env <instancer>)]
              (recur (maybe.assume (type.apply (list instanceT) expectedT)))))
          ([#.UnivQ tc.existential]
           [#.ExQ tc.var])
          
          (#.Var id)
          (do @
            [?expectedT' (&.with-type-env
                           (tc.read id))]
            (case ?expectedT'
              (#.Some expectedT')
              (recur expectedT')

              _
              ## Inference
              (do @
                [[input-id inputT] (&.with-type-env tc.var)
                 [output-id outputT] (&.with-type-env tc.var)
                 #let [funT (#.Function inputT outputT)]
                 funA (recur 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-type outputT)
              (analyse body))
          
          _
          (&.fail "")
          )))))

(def: #export (analyse-apply analyse funcT funcA args)
  (-> &.Analyser Type Analysis (List Code) (Meta Analysis))
  (&.with-stacked-errors
    (function (_ _)
      (ex.construct 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 macro.Monad<Meta>
      [[applyT argsA] (&inference.general analyse funcT args)]
      (wrap (la.apply argsA funcA)))))