(.module:
  lux
  (lux (control [monad #+ do]
                ["ex" exception #+ exception:]
                eq)
       (data [bool]
             [number]
             [product]
             ["e" error]
             [maybe]
             [text]
             text/format
             (coll [list "list/" Fold<List> Monoid<List> Functor<List>]))
       [macro]
       (macro [code])
       (lang [type]
             (type ["tc" check])))
  (luxc ["&" lang]
        (lang ["&." scope]
              ["la" analysis]
              (analysis [".A" common]
                        [".A" structure]
                        (case [".A" coverage])))))

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

  [Cannot-Match-Type-With-Pattern]
  [Sum-Type-Has-No-Case]
  [Unrecognized-Pattern-Syntax]
  [Cannot-Simplify-Type-For-Pattern-Matching]
  [Cannot-Have-Empty-Branches]
  [Non-Exhaustive-Pattern-Matching]
  [Symbols-Must-Be-Unqualified-Inside-Patterns]
  )

(def: (pattern-error type pattern)
  (-> Type Code Text)
  (format "   Type: " (%type type) "\n"
          "Pattern: " (%code pattern)))

(def: (re-quantify envs baseT)
  (-> (List (List Type)) Type Type)
  (case envs
    #.Nil
    baseT

    (#.Cons head tail)
    (re-quantify tail (#.UnivQ head baseT))))

## Type-checking on the input value is done during the analysis of a
## "case" expression, to ensure that the patterns being used make
## sense for the type of the input value.
## Sometimes, that input value is complex, by depending on
## type-variables or quantifications.
## This function makes it easier for "case" analysis to properly
## type-check the input with respect to the patterns.
(def: (simplify-case-type caseT)
  (-> Type (Meta Type))
  (loop [envs (: (List (List Type))
                 (list))
         caseT caseT]
    (case caseT
      (#.Var id)
      (do macro.Monad<Meta>
        [?caseT' (&.with-type-env
                   (tc.read id))]
        (case ?caseT'
          (#.Some caseT')
          (recur envs caseT')

          _
          (&.throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT))))

      (#.Named name unnamedT)
      (recur envs unnamedT)

      (#.UnivQ env unquantifiedT)
      (recur (#.Cons env envs) unquantifiedT)

      ## (^template [<tag> <instancer>]
      ##   (<tag> _)
      ##   (do macro.Monad<Meta>
      ##     [[_ instanceT] (&.with-type-env
      ##                      <instancer>)]
      ##     (recur (maybe.assume (type.apply (list instanceT) caseT)))))
      ## ([#.UnivQ tc.var]
      ##  [#.ExQ tc.existential])
      
      (#.ExQ _)
      (do macro.Monad<Meta>
        [[ex-id exT] (&.with-type-env
                       tc.existential)]
        (recur envs (maybe.assume (type.apply (list exT) caseT))))

      (#.Apply inputT funcT)
      (case funcT
        (#.Var funcT-id)
        (do macro.Monad<Meta>
          [funcT' (&.with-type-env
                    (do tc.Monad<Check>
                      [?funct' (tc.read funcT-id)]
                      (case ?funct'
                        (#.Some funct')
                        (wrap funct')

                        _
                        (tc.throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT)))))]
          (recur envs (#.Apply inputT funcT')))

        _
        (case (type.apply (list inputT) funcT)
          (#.Some outputT)
          (recur envs outputT)

          #.None
          (&.throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT))))

      (#.Product _)
      (|> caseT
          type.flatten-tuple
          (list/map (re-quantify envs))
          type.tuple
          (:: macro.Monad<Meta> wrap))

      _
      (:: macro.Monad<Meta> wrap (re-quantify envs caseT)))))

## This function handles several concerns at once, but it must be that
## way because those concerns are interleaved when doing
## pattern-matching and they cannot be separated.
## The pattern is analysed in order to get a general feel for what is
## expected of the input value. This, in turn, informs the
## type-checking of the input.
## A kind of "continuation" value is passed around which signifies
## what needs to be done _after_ analysing a pattern.
## In general, this is done to analyse the "body" expression
## associated to a particular pattern _in the context of_ said
## pattern.
## The reason why *context* is important is because patterns may bind
## values to local variables, which may in turn be referenced in the
## body expressions.
## That is why the body must be analysed in the context of the
## pattern, and not separately.
(def: (analyse-pattern num-tags inputT pattern next)
  (All [a] (-> (Maybe Nat) Type Code (Meta a) (Meta [la.Pattern a])))
  (case pattern
    [cursor (#.Symbol ["" name])]
    (&.with-cursor cursor
      (do macro.Monad<Meta>
        [outputA (&scope.with-local [name inputT]
                   next)
         idx &scope.next-local]
        (wrap [(` ("lux case bind" (~ (code.nat idx)))) outputA])))

    [cursor (#.Symbol ident)]
    (&.with-cursor cursor
      (&.throw Symbols-Must-Be-Unqualified-Inside-Patterns (%ident ident)))

    (^template [<type> <code-tag>]
      [cursor (<code-tag> test)]
      (&.with-cursor cursor
        (do macro.Monad<Meta>
          [_ (&.with-type-env
               (tc.check inputT <type>))
           outputA next]
          (wrap [pattern outputA]))))
    ([Bool #.Bool]
     [Nat  #.Nat]
     [Int  #.Int]
     [Deg  #.Deg]
     [Frac #.Frac]
     [Text #.Text])

    (^ [cursor (#.Tuple (list))])
    (&.with-cursor cursor
      (do macro.Monad<Meta>
        [_ (&.with-type-env
             (tc.check inputT Unit))
         outputA next]
        (wrap [(` ("lux case tuple" [])) outputA])))

    (^ [cursor (#.Tuple (list singleton))])
    (analyse-pattern #.None inputT singleton next)
    
    [cursor (#.Tuple sub-patterns)]
    (&.with-cursor cursor
      (do macro.Monad<Meta>
        [inputT' (simplify-case-type inputT)]
        (case inputT'
          (#.Product _)
          (let [sub-types (type.flatten-tuple inputT')
                num-sub-types (maybe.default (list.size sub-types)
                                             num-tags)
                num-sub-patterns (list.size sub-patterns)
                matches (cond (n/< num-sub-types num-sub-patterns)
                              (let [[prefix suffix] (list.split (n/dec num-sub-patterns) sub-types)]
                                (list.zip2 (list/compose prefix (list (type.tuple suffix))) sub-patterns))

                              (n/> num-sub-types num-sub-patterns)
                              (let [[prefix suffix] (list.split (n/dec num-sub-types) sub-patterns)]
                                (list.zip2 sub-types (list/compose prefix (list (code.tuple suffix)))))
                              
                              ## (n/= num-sub-types num-sub-patterns)
                              (list.zip2 sub-types sub-patterns)
                              )]
            (do @
              [[memberP+ thenA] (list/fold (: (All [a]
                                                (-> [Type Code] (Meta [(List la.Pattern) a])
                                                    (Meta [(List la.Pattern) a])))
                                              (function (_ [memberT memberC] then)
                                                (do @
                                                  [[memberP [memberP+ thenA]] ((:! (All [a] (-> (Maybe Nat) Type Code (Meta a) (Meta [la.Pattern a])))
                                                                                   analyse-pattern)
                                                                               #.None memberT memberC then)]
                                                  (wrap [(list& memberP memberP+) thenA]))))
                                           (do @
                                             [nextA next]
                                             (wrap [(list) nextA]))
                                           (list.reverse matches))]
              (wrap [(` ("lux case tuple" [(~+ memberP+)]))
                     thenA])))

          _
          (&.throw Cannot-Match-Type-With-Pattern (pattern-error inputT pattern))
          )))

    [cursor (#.Record record)]
    (do macro.Monad<Meta>
      [record (structureA.normalize record)
       [members recordT] (structureA.order record)
       _ (&.with-type-env
           (tc.check inputT recordT))]
      (analyse-pattern (#.Some (list.size members)) inputT [cursor (#.Tuple members)] next))

    [cursor (#.Tag tag)]
    (&.with-cursor cursor
      (analyse-pattern #.None inputT (` ((~ pattern))) next))

    (^ [cursor (#.Form (list& [_ (#.Nat idx)] values))])
    (&.with-cursor cursor
      (do macro.Monad<Meta>
        [inputT' (simplify-case-type inputT)]
        (case inputT'
          (#.Sum _)
          (let [flat-sum (type.flatten-variant inputT')
                size-sum (list.size flat-sum)
                num-cases (maybe.default size-sum num-tags)]
            (case (list.nth idx flat-sum)
              (^multi (#.Some case-type)
                      (n/< num-cases idx))
              (if (and (n/> num-cases size-sum)
                       (n/= (n/dec num-cases) idx))
                (do macro.Monad<Meta>
                  [[testP nextA] (analyse-pattern #.None
                                                  (type.variant (list.drop (n/dec num-cases) flat-sum))
                                                  (` [(~+ values)])
                                                  next)]
                  (wrap [(` ("lux case variant" (~ (code.nat idx)) (~ (code.nat num-cases)) (~ testP)))
                         nextA]))
                (do macro.Monad<Meta>
                  [[testP nextA] (analyse-pattern #.None case-type (` [(~+ values)]) next)]
                  (wrap [(` ("lux case variant" (~ (code.nat idx)) (~ (code.nat num-cases)) (~ testP)))
                         nextA])))

              _
              (&.throw Sum-Type-Has-No-Case
                       (format "Case: " (%n idx) "\n"
                               "Type: " (%type inputT)))))

          _
          (&.throw Cannot-Match-Type-With-Pattern (pattern-error inputT pattern)))))

    (^ [cursor (#.Form (list& [_ (#.Tag tag)] values))])
    (&.with-cursor cursor
      (do macro.Monad<Meta>
        [tag (macro.normalize tag)
         [idx group variantT] (macro.resolve-tag tag)
         _ (&.with-type-env
             (tc.check inputT variantT))]
        (analyse-pattern (#.Some (list.size group)) inputT (` ((~ (code.nat idx)) (~+ values))) next)))

    _
    (&.throw Unrecognized-Pattern-Syntax (%code pattern))
    ))

(def: #export (analyse-case analyse inputC branches)
  (-> &.Analyser Code (List [Code Code]) (Meta la.Analysis))
  (case branches
    #.Nil
    (&.throw Cannot-Have-Empty-Branches "")

    (#.Cons [patternH bodyH] branchesT)
    (do macro.Monad<Meta>
      [[inputT inputA] (commonA.with-unknown-type
                         (analyse inputC))
       outputH (analyse-pattern #.None inputT patternH (analyse bodyH))
       outputT (monad.map @
                          (function (_ [patternT bodyT])
                            (analyse-pattern #.None inputT patternT (analyse bodyT)))
                          branchesT)
       outputHC (|> outputH product.left coverageA.determine)
       outputTC (monad.map @ (|>> product.left coverageA.determine) outputT)
       _ (case (monad.fold e.Monad<Error> coverageA.merge outputHC outputTC)
           (#e.Success coverage)
           (&.assert Non-Exhaustive-Pattern-Matching ""
                     (coverageA.exhaustive? coverage))

           (#e.Error error)
           (&.fail error))]
      (wrap (` ("lux case" (~ inputA) (~ (code.record (list& outputH outputT)))))))))