(;module:
  lux
  (lux (control monad
                eq)
       (data [bool "B/" Eq<Bool>]
             [number]
             [char]
             [text]
             text/format
             [product]
             ["R" result "R/" Monad<Result>]
             (coll [list "L/" Fold<List> Monoid<List> Monad<List>]
                   ["D" dict]))
       [macro #+ Monad<Lux>]
       (macro [code])
       [type]
       (type ["TC" check]))
  (../.. ["&" base]
         (lang ["la" analysis])
         ["&;" env])
  (.. ["&;" common]
      ["&;" structure])
  (. ["&&;" coverage]))

(def: (pattern-error type pattern)
  (-> Type Code Text)
  (format "Cannot match this type: " (%type type) "\n"
          "     With this 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 (Lux Type))
  (case type
    (#;Var id)
    (do Monad<Lux>
      [? (&;within-type-env
          (TC;bound? id))]
      (if ?
        (do @
          [type' (&;within-type-env
                  (TC;read-var id))]
          (simplify-case-type type'))
        (&;fail (format "Cannot simplify type for pattern-matching: " (%type type)))))

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

    (^or (#;UnivQ _) (#;ExQ _))
    (do Monad<Lux>
      [[ex-id exT] (&;within-type-env
                    TC;existential)]
      (simplify-case-type (assume (type;apply-type type exT))))

    _
    (:: Monad<Lux> 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 (Lux a) (Lux [la;Pattern a])))
  (case pattern
    [cursor (#;Symbol ["" name])]
    (&;with-cursor cursor
      (do Monad<Lux>
        [outputA (&env;with-local [name inputT]
                   next)
         idx &env;next-local]
        (wrap [(#la;BindP idx) outputA])))

    [cursor (#;Symbol ident)]
    (&;with-cursor cursor
      (&;fail (format "Symbols must be unqualified inside patterns: " (%ident ident))))

    (^template [<type> <code-tag> <pattern-tag>]
      [cursor (<code-tag> test)]
      (&;with-cursor cursor
        (do Monad<Lux>
          [_ (&;within-type-env
              (TC;check inputT <type>))
           outputA next]
          (wrap [(<pattern-tag> test) outputA]))))
    ([Bool #;Bool #la;BoolP]
     [Nat  #;Nat  #la;NatP]
     [Int  #;Int  #la;IntP]
     [Deg  #;Deg  #la;DegP]
     [Real #;Real #la;RealP]
     [Char #;Char #la;CharP]
     [Text #;Text #la;TextP])

    (^ [cursor (#;Tuple (list))])
    (&;with-cursor cursor
      (do Monad<Lux>
        [_ (&;within-type-env
            (TC;check inputT Unit))
         outputA next]
        (wrap [(#la;TupleP (list)) outputA])))

    (^ [cursor (#;Tuple (list singleton))])
    (analyse-pattern #;None inputT singleton next)
    
    [cursor (#;Tuple sub-patterns)]
    (&;with-cursor cursor
      (do Monad<Lux>
        [inputT' (simplify-case-type inputT)]
        (case inputT'
          (#;Product _)
          (let [sub-types (type;flatten-tuple inputT)
                num-sub-types (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 (L/append 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 (L/append prefix (list (code;tuple suffix)))))
                              
                              ## (n.= num-sub-types num-sub-patterns)
                              (list;zip2 sub-types sub-patterns)
                              )]
            (do @
              [[memberP+ thenA] (L/fold (: (All [a]
                                             (-> [Type Code] (Lux [(List la;Pattern) a])
                                                 (Lux [(List la;Pattern) a])))
                                           (function [[memberT memberC] then]
                                             (do @
                                               [[memberP [memberP+ thenA]] ((:! (All [a] (-> (Maybe Nat) Type Code (Lux a) (Lux [la;Pattern a])))
                                                                                analyse-pattern)
                                                                            #;None memberT memberC then)]
                                               (wrap [(list& memberP memberP+) thenA]))))
                                        (do @
                                          [nextA next]
                                          (wrap [(list) nextA]))
                                        matches)]
              (wrap [(#la;TupleP memberP+) thenA])))

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

    [cursor (#;Record record)]
    (do Monad<Lux>
      [record (&structure;normalize record)
       [members recordT] (&structure;order record)
       _ (&;within-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 Monad<Lux>
        [inputT' (simplify-case-type inputT)]
        (case inputT'
          (#;Sum _)
          (let [flat-sum (type;flatten-variant inputT)
                size-sum (list;size flat-sum)
                num-cases (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 Monad<Lux>
                  [[testP nextA] (analyse-pattern #;None
                                                  (type;variant (list;drop (n.dec num-cases) flat-sum))
                                                  (` [(~@ values)])
                                                  next)]
                  (wrap [(#la;VariantP idx num-cases testP)
                         nextA]))
                (do Monad<Lux>
                  [[testP nextA] (analyse-pattern #;None case-type (` [(~@ values)]) next)]
                  (wrap [(#la;VariantP idx num-cases testP)
                         nextA])))

              _
              (&;fail (format "Cannot match index " (%n idx) " against type: " (%type inputT)))))

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

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

    _
    (&;fail (format "Unrecognized pattern syntax: " (%code pattern)))
    ))

(def: #export (analyse-case analyse input branches)
  (-> &;Analyser Code (List [Code Code]) (Lux la;Analysis))
  (case branches
    #;Nil
    (&;fail "Cannot have empty branches in pattern-matching expression.")

    (#;Cons [patternH bodyH] branchesT)
    (do Monad<Lux>
      [[inputT inputA] (&common;with-unknown-type
                         (analyse input))
       outputH (analyse-pattern #;None inputT patternH (analyse bodyH))
       outputT (mapM @
                     (function [[patternT bodyT]]
                       (analyse-pattern #;None inputT patternT (analyse bodyT)))
                     branchesT)
       _ (case (foldM R;Monad<Result>
                      &&coverage;merge
                      (|> outputH product;left &&coverage;determine)
                      (L/map (|>. product;left &&coverage;determine) outputT))
           (#R;Success coverage)
           (if (&&coverage;total? coverage)
             (wrap [])
             (&;fail "Pattern-matching is not total."))

           (#R;Error error)
           (&;fail error))]
      (wrap (#la;Case inputA (#;Cons outputH outputT))))))