(.module:
  [lux #- function]
  (lux (control monad
                ["ex" exception #+ exception:])
       (data [maybe]
             [text]
             text/format
             (collection [list "list/" Fold<List> Monoid<List> Monad<List>]))
       [macro]
       (macro [code])
       (language [type]
                 (type ["tc" check])
                 [".L" scope]))
  [///]
  [// #+ Analysis Compiler]
  [//type]
  [//inference])

(exception: #export (cannot-analyse {expected Type} {function Text} {argument Text} {body Code})
  (ex.report ["Type" (%type expected)]
             ["Function" function]
             ["Argument" argument]
             ["Body" (%code body)]))

(exception: #export (cannot-apply {function Type} {arguments (List Code)})
  (ex.report [" Function" (%type function)]
             ["Arguments" (|> arguments
                              list.enumerate
                              (list/map (.function (_ [idx argC])
                                          (format "\n  " (%n idx) " " (%code argC))))
                              (text.join-with ""))]))

(def: #export (function analyse function-name arg-name body)
  (-> Compiler Text Text Code (Meta Analysis))
  (do macro.Monad<Meta>
    [functionT macro.expected-type]
    (loop [expectedT functionT]
      (///.with-stack cannot-analyse [expectedT function-name arg-name body]
        (case expectedT
          (#.Named name unnamedT)
          (recur unnamedT)

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

            #.None
            (///.fail (ex.construct cannot-analyse [expectedT function-name arg-name body])))

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

              ## Inference
              _
              (do @
                [[input-id inputT] (//type.with-env tc.var)
                 [output-id outputT] (//type.with-env tc.var)
                 #let [functionT (#.Function inputT outputT)]
                 functionA (recur functionT)
                 _ (//type.with-env
                     (tc.check expectedT functionT))]
                (wrap functionA))
              ))

          (#.Function inputT outputT)
          (<| (:: @ map (.function (_ [scope bodyA])
                          (#//.Function (scopeL.environment scope) bodyA)))
              //.with-scope
              ## Functions have access not only to their argument, but
              ## also to themselves, through a local variable.
              (scopeL.with-local [function-name expectedT])
              (scopeL.with-local [arg-name inputT])
              (//type.with-type outputT)
              (analyse body))
          
          _
          (///.fail "")
          )))))

(def: #export (apply analyse functionT functionA args)
  (-> Compiler Type Analysis (List Code) (Meta Analysis))
  (<| (///.with-stack cannot-apply [functionT args])
      (do macro.Monad<Meta>
        [[applyT argsA] (//inference.general analyse functionT args)])
      (wrap (//.apply [functionA argsA]))))