(;module:
  lux
  (lux (control [monad #+ do]
                ["ex" exception #+ exception:])
       (data [maybe]
             [text]
             text/format
             (coll [list "list/" Functor<List>]))
       [meta #+ Monad<Meta>]
       (meta [type]
             (type ["tc" check])))
  (luxc ["&" base]
        (lang ["la" analysis #+ Analysis])
        (analyser ["&;" common])))

(exception: #export Cannot-Infer)
(exception: #export Cannot-Infer-Argument)
(exception: #export Smaller-Variant-Than-Expected)

## When doing inference, type-variables often need to be created in
## order to figure out which types are present in the expression being
## inferred.
## If a type-variable never gets bound/resolved to a type, then that
## means the expression can be generalized through universal
## quantification.
## When that happens, the type-variable must be replaced by an
## argument to the universally-quantified type.
(def: #export (replace-var var-id bound-idx type)
  (-> Nat Nat Type Type)
  (case type
    (#;Primitive name params)
    (#;Primitive name (list/map (replace-var var-id bound-idx) params))

    (^template [<tag>]
      (<tag> left right)
      (<tag> (replace-var var-id bound-idx left)
             (replace-var var-id bound-idx right)))
    ([#;Sum]
     [#;Product]
     [#;Function]
     [#;Apply])
    
    (#;Var id)
    (if (n.= var-id id)
      (#;Bound bound-idx)
      type)

    (^template [<tag>]
      (<tag> env quantified)
      (<tag> (list/map (replace-var var-id bound-idx) env)
             (replace-var var-id (n.+ +2 bound-idx) quantified)))
    ([#;UnivQ]
     [#;ExQ])
    
    _
    type))

(def: (replace-bound bound-idx replacementT type)
  (-> Nat Type Type Type)
  (case type
    (#;Primitive name params)
    (#;Primitive name (list/map (replace-bound bound-idx replacementT) params))

    (^template [<tag>]
      (<tag> left right)
      (<tag> (replace-bound bound-idx replacementT left)
             (replace-bound bound-idx replacementT right)))
    ([#;Sum]
     [#;Product]
     [#;Function]
     [#;Apply])
    
    (#;Bound idx)
    (if (n.= bound-idx idx)
      replacementT
      type)

    (^template [<tag>]
      (<tag> env quantified)
      (<tag> (list/map (replace-bound bound-idx replacementT) env)
             (replace-bound (n.+ +2 bound-idx) replacementT quantified)))
    ([#;UnivQ]
     [#;ExQ])
    
    _
    type))

## Type-inference works by applying some (potentially quantified) type
## to a sequence of values.
## Function types are used for this, although inference is not always
## done for function application (alternative uses may be records and
## tagged variants).
## But, so long as the type being used for the inference can be trated
## as a function type, this method of inference should work.
(def: #export (apply-function analyse funcT args)
  (-> &;Analyser Type (List Code) (Meta [Type (List Analysis)]))
  (case args
    #;Nil
    (:: Monad<Meta> wrap [funcT (list)])
    
    (#;Cons argC args')
    (case funcT
      (#;Named name unnamedT)
      (apply-function analyse unnamedT args)

      (#;UnivQ _)
      (&common;with-var
        (function [[var-id varT]]
          (do Monad<Meta>
            [[outputT argsA] (apply-function analyse (maybe;assume (type;apply (list varT) funcT)) args)]
            (do @
              [? (&;with-type-env
                   (tc;bound? var-id))
               ## Quantify over the type if genericity/parametricity
               ## is discovered.
               outputT' (if ?
                          (&;with-type-env
                            (tc;clean var-id outputT))
                          (wrap (type;univ-q +1 (replace-var var-id +1 outputT))))]
              (wrap [outputT' argsA])))))

      (#;ExQ _)
      (do Monad<Meta>
        [[ex-id exT] (&;with-type-env
                       tc;existential)]
        (apply-function analyse (maybe;assume (type;apply (list exT) funcT)) args))

      ## Arguments are inferred back-to-front because, by convention,
      ## Lux functions take the most important arguments *last*, which
      ## means that the most information for doing proper inference is
      ## located in the last arguments to a function call.
      ## By inferring back-to-front, a lot of type-annotations can be
      ## avoided in Lux code, since the inference algorithm can piece
      ## things together more easily.
      (#;Function inputT outputT)
      (do Monad<Meta>
        [[outputT' args'A] (apply-function analyse outputT args')
         argA (&;with-stacked-errors
                (function [_] (Cannot-Infer-Argument
                               (format "Inferred Type: " (%type inputT) "\n"
                                       "     Argument: " (%code argC))))
                (&;with-expected-type inputT
                  (analyse argC)))]
        (wrap [outputT' (list& argA args'A)]))

      _
      (&;throw Cannot-Infer (format "Inference Type: " (%type funcT)
                                    "     Arguments: " (|> args (list/map %code) (text;join-with " ")))))
    ))

## Turns a record type into the kind of function type suitable for inference.
(def: #export (record type)
  (-> Type (Meta Type))
  (case type
    (#;Named name unnamedT)
    (do Monad<Meta>
      [unnamedT+ (record unnamedT)]
      (wrap unnamedT+))

    (^template [<tag>]
      (<tag> env bodyT)
      (do Monad<Meta>
        [bodyT+ (record bodyT)]
        (wrap (<tag> env bodyT+))))
    ([#;UnivQ]
     [#;ExQ])

    (#;Product _)
    (:: Monad<Meta> wrap (type;function (type;flatten-tuple type) type))

    _
    (&;fail (format "Not a record type: " (%type type)))))

## Turns a variant type into the kind of function type suitable for inference.
(def: #export (variant tag expected-size type)
  (-> Nat Nat Type (Meta Type))
  (loop [depth +0
         currentT type]
    (case currentT
      (#;Named name unnamedT)
      (do Monad<Meta>
        [unnamedT+ (recur depth unnamedT)]
        (wrap unnamedT+))

      (^template [<tag>]
        (<tag> env bodyT)
        (do Monad<Meta>
          [bodyT+ (recur (n.inc depth) bodyT)]
          (wrap (<tag> env bodyT+))))
      ([#;UnivQ]
       [#;ExQ])

      (#;Sum _)
      (let [cases (type;flatten-variant currentT)
            actual-size (list;size cases)
            boundary (n.dec expected-size)]
        (cond (or (n.= expected-size actual-size)
                  (and (n.> expected-size actual-size)
                       (n.< boundary tag)))
              (case (list;nth tag cases)
                (#;Some caseT)
                (:: Monad<Meta> wrap (if (n.= +0 depth)
                                       (type;function (list caseT) currentT)
                                       (let [replace! (replace-bound (|> depth n.dec (n.* +2)) type)]
                                         (type;function (list (replace! caseT))
                                           (replace! currentT)))))

                #;None
                (&common;variant-out-of-bounds-error type expected-size tag))
              
              (n.< expected-size actual-size)
              (&;throw Smaller-Variant-Than-Expected
                       (format "Expected: " (%i (nat-to-int expected-size)) "\n"
                               "  Actual: " (%i (nat-to-int actual-size))))

              (n.= boundary tag)
              (let [caseT (type;variant (list;drop boundary cases))]
                (:: Monad<Meta> wrap (if (n.= +0 depth)
                                       (type;function (list caseT) currentT)
                                       (let [replace! (replace-bound (|> depth n.dec (n.* +2)) type)]
                                         (type;function (list (replace! caseT))
                                           (replace! currentT))))))
              
              ## else
              (&common;variant-out-of-bounds-error type expected-size tag)))

      _
      (&;fail (format "Not a variant type: " (%type type))))))