(;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>]))
       [meta]
       (meta [code]
             [type]
             (type ["tc" check])))
  (luxc ["&" base]
        (lang ["la" analysis]
              (analysis [";A" common]
                        [";A" structure]
                        (case [";A" coverage])))
        ["&;" scope]))

(exception: #export Cannot-Match-Type-With-Pattern)
(exception: #export Sum-Type-Has-No-Case)
(exception: #export Unrecognized-Pattern-Syntax)
(exception: #export Cannot-Simplify-Type-For-Pattern-Matching)

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

## 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 type)
  (-> Type (Meta Type))
  (case type
    (#;Var id)
    (do meta;Monad<Meta>
      [? (&;with-type-env
           (tc;bound? id))]
      (if ?
        (do @
          [type' (&;with-type-env
                   (tc;read id))]
          (simplify-case-type type'))
        (&;throw Cannot-Simplify-Type-For-Pattern-Matching (%type type))))

    (#;Named name unnamedT)
    (simplify-case-type unnamedT)

    (^or (#;UnivQ _) (#;ExQ _))
    (do meta;Monad<Meta>
      [[ex-id exT] (&;with-type-env
                     tc;existential)]
      (simplify-case-type (maybe;assume (type;apply (list exT) type))))

    (#;Apply inputT funcT)
    (case (type;apply (list inputT) funcT)
      (#;Some outputT)
      (:: meta;Monad<Meta> wrap outputT)

      #;None
      (&;fail (format "Cannot apply type " (%type funcT) " to  type " (%type inputT))))

    _
    (:: meta;Monad<Meta> wrap type)))

## 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 meta;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
      (&;fail (format "Symbols must be unqualified inside patterns: " (%ident ident))))

    (^template [<type> <code-tag>]
      [cursor (<code-tag> test)]
      (&;with-cursor cursor
        (do meta;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 meta;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 meta;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])))

          _
          (&;fail (pattern-error inputT pattern))
          )))

    [cursor (#;Record record)]
    (do meta;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 meta;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 meta;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 meta;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)))))

          _
          (&;fail (pattern-error inputT pattern)))))

    (^ [cursor (#;Form (list& [_ (#;Tag tag)] values))])
    (&;with-cursor cursor
      (do meta;Monad<Meta>
        [tag (meta;normalize tag)
         [idx group variantT] (meta;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
    (&;fail "Cannot have empty branches in pattern-matching expression.")

    (#;Cons [patternH bodyH] branchesT)
    (do meta;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)
           (if (coverageA;exhaustive? coverage)
             (wrap [])
             (&;fail "Pattern-matching is not exhaustive."))

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