(.module:
  lux
  (lux (control [monad #+ do]
                ["ex" exception #+ exception:]
                eq)
       (data [bool "bool/" Eq<Bool>]
             [number]
             ["e" error "error/" Monad<Error>]
             text/format
             (coll [list "list/" Fold<List>]
                   [dict #+ Dict]))
       [macro "macro/" Monad<Meta>])
  (luxc ["&" lang]
        (lang ["la" analysis])))

(exception: #export (Unknown-Pattern {message Text})
  message)

## The coverage of a pattern-matching expression summarizes how well
## all the possible values of an input are being covered by the
## different patterns involved.
## Ideally, the pattern-matching has "exhaustive" coverage, which just
## means that every possible value can be matched by at least 1
## pattern.
## Every other coverage is considered partial, and it would be valued
## as insuficient (since it could lead to runtime errors due to values
## not being handled by any pattern).
## The #Partial tag covers arbitrary partial coverages in a general
## way, while the other tags cover more specific cases for booleans
## and variants.
(type: #export #rec Coverage
  #Partial
  (#Bool Bool)
  (#Variant Nat (Dict Nat Coverage))
  (#Seq Coverage Coverage)
  (#Alt Coverage Coverage)
  #Exhaustive)

(def: #export (exhaustive? coverage)
  (-> Coverage Bool)
  (case coverage
    (#Exhaustive _)
    true

    _
    false))

(def: #export (determine pattern)
  (-> la.Pattern (Meta Coverage))
  (case pattern
    ## Binding amounts to exhaustive coverage because any value can be
    ## matched that way.
    ## Unit [] amounts to exhaustive coverage because there is only one
    ## possible value, so matching against it covers all cases.
    (^or (^code ("lux case bind" (~ _))) (^code ("lux case tuple" [])))
    (macro/wrap #Exhaustive)

    (^code ("lux case tuple" [(~ singleton)]))
    (determine singleton)

    ## Primitive patterns always have partial coverage because there
    ## are too many possibilities as far as values go.
    (^or [_ (#.Nat _)]  [_ (#.Int _)]  [_ (#.Deg _)]
         [_ (#.Frac _)] [_ (#.Text _)])
    (macro/wrap #Partial)

    ## Bools are the exception, since there is only "true" and
    ## "false", which means it is possible for boolean
    ## pattern-matching to become exhaustive if complementary parts meet.
    [_ (#.Bool value)]
    (macro/wrap (#Bool value))

    ## Tuple patterns can be exhaustive if there is exhaustiveness for all of
    ## their sub-patterns.
    (^code ("lux case tuple" [(~+ subs)]))
    (loop [subs subs]
      (case subs
        #.Nil
        (macro/wrap #Exhaustive)

        (#.Cons sub subs')
        (do macro.Monad<Meta>
          [pre (determine sub)
           post (recur subs')]
          (if (exhaustive? post)
            (wrap pre)
            (wrap (#Seq pre post))))))

    ## Variant patterns can be shown to be exhaustive if all the possible
    ## cases are handled exhaustively.
    (^code ("lux case variant" (~ [_ (#.Nat tag-id)]) (~ [_ (#.Nat num-tags)]) (~ sub)))
    (do macro.Monad<Meta>
      [=sub (determine sub)]
      (wrap (#Variant num-tags
                      (|> (dict.new number.Hash<Nat>)
                          (dict.put tag-id =sub)))))

    _
    (&.throw Unknown-Pattern (%code pattern))))

(def: (xor left right)
  (-> Bool Bool Bool)
  (or (and left (not right))
      (and (not left) right)))

## The coverage checker not only verifies that pattern-matching is
## exhaustive, but also that there are no redundant patterns.
## Redundant patterns will never be executed, since there will
## always be a pattern prior to them that would match the input.
## Because of that, the presence of redundant patterns is assumed to
## be a bug, likely due to programmer carelessness.
(def: redundant-pattern
  (e.Error Coverage)
  (e.fail "Redundant pattern."))

(def: (flatten-alt coverage)
  (-> Coverage (List Coverage))
  (case coverage
    (#Alt left right)
    (list& left (flatten-alt right))

    _
    (list coverage)))

(struct: _ (Eq Coverage)
  (def: (= reference sample)
    (case [reference sample]
      [#Exhaustive #Exhaustive]
      true

      [(#Bool sideR) (#Bool sideS)]
      (bool/= sideR sideS)

      [(#Variant allR casesR) (#Variant allS casesS)]
      (and (n/= allR allS)
           (:: (dict.Eq<Dict> =) = casesR casesS))

      [(#Seq leftR rightR) (#Seq leftS rightS)]
      (and (= leftR leftS)
           (= rightR rightS))

      [(#Alt _) (#Alt _)]
      (let [flatR (flatten-alt reference)
            flatS (flatten-alt sample)]
        (and (n/= (list.size flatR) (list.size flatS))
             (list.every? (function (_ [coverageR coverageS])
                            (= coverageR coverageS))
                          (list.zip2 flatR flatS))))

      _
      false)))

(open Eq<Coverage> "C/")

## After determining the coverage of each individual pattern, it is
## necessary to merge them all to figure out if the entire
## pattern-matching expression is exhaustive and whether it contains
## redundant patterns.
(def: #export (merge addition so-far)
  (-> Coverage Coverage (e.Error Coverage))
  (case [addition so-far]
    ## The addition cannot possibly improve the coverage.
    [_ #Exhaustive]
    redundant-pattern

    ## The addition completes the coverage.
    [#Exhaustive _]
    (error/wrap #Exhaustive)

    [#Partial #Partial]
    (error/wrap #Partial)

    ## 2 boolean coverages are exhaustive if they compliment one another.
    (^multi [(#Bool sideA) (#Bool sideSF)]
            (xor sideA sideSF))
    (error/wrap #Exhaustive)

    [(#Variant allA casesA) (#Variant allSF casesSF)]
    (cond (not (n/= allSF allA))
          (e.fail "Variants do not match.")

          (:: (dict.Eq<Dict> Eq<Coverage>) = casesSF casesA)
          redundant-pattern

          ## else
          (do e.Monad<Error>
            [casesM (monad.fold @
                                (function (_ [tagA coverageA] casesSF')
                                  (case (dict.get tagA casesSF')
                                    (#.Some coverageSF)
                                    (do @
                                      [coverageM (merge coverageA coverageSF)]
                                      (wrap (dict.put tagA coverageM casesSF')))

                                    #.None
                                    (wrap (dict.put tagA coverageA casesSF'))))
                                casesSF (dict.entries casesA))]
            (wrap (if (let [case-coverages (dict.values casesM)]
                        (and (n/= allSF (list.size case-coverages))
                             (list.every? exhaustive? case-coverages)))
                    #Exhaustive
                    (#Variant allSF casesM)))))

    [(#Seq leftA rightA) (#Seq leftSF rightSF)]
    (case [(C/= leftSF leftA) (C/= rightSF rightA)]
      ## There is nothing the addition adds to the coverage.
      [true true]
      redundant-pattern

      ## The 2 sequences cannot possibly be merged.
      [false false]
      (error/wrap (#Alt so-far addition))

      ## Same prefix
      [true false]
      (do e.Monad<Error>
        [rightM (merge rightA rightSF)]
        (if (exhaustive? rightM)
          ## If all that follows is exhaustive, then it can be safely dropped
          ## (since only the "left" part would influence whether the
          ## merged coverage is exhaustive or not).
          (wrap leftSF)
          (wrap (#Seq leftSF rightM))))

      ## Same suffix
      [false true]
      (do e.Monad<Error>
        [leftM (merge leftA leftSF)]
        (wrap (#Seq leftM rightA))))
    
    ## The left part will always match, so the addition is redundant.
    (^multi [(#Seq left right) single]
            (C/= left single))
    redundant-pattern

    ## The right part is not necessary, since it can always match the left.
    (^multi [single (#Seq left right)]
            (C/= left single))
    (error/wrap single)

    ## When merging a new coverage against one based on Alt, it may be
    ## that one of the many coverages in the Alt is complementary to
    ## the new one, so effort must be made to fuse carefully, to match
    ## the right coverages together.
    ## If one of the Alt sub-coverages matches the new one, the cycle
    ## must be repeated, in case the resulting coverage can now match
    ## other ones in the original Alt.
    ## This process must be repeated until no further productive
    ## merges can be done.
    [_ (#Alt leftS rightS)]
    (do e.Monad<Error>
      [#let [fuse-once (: (-> Coverage (List Coverage)
                              (e.Error [(Maybe Coverage)
                                        (List Coverage)]))
                          (function (_ coverage possibilities)
                            (loop [alts possibilities]
                              (case alts
                                #.Nil
                                (wrap [#.None (list coverage)])
                                
                                (#.Cons alt alts')
                                (case (merge coverage alt)
                                  (#e.Success altM)
                                  (case altM
                                    (#Alt _)
                                    (do @
                                      [[success alts+] (recur alts')]
                                      (wrap [success (#.Cons alt alts+)]))

                                    _
                                    (wrap [(#.Some altM) alts']))
                                  
                                  (#e.Error error)
                                  (e.fail error))
                                ))))]
       [success possibilities] (fuse-once addition (flatten-alt so-far))]
      (loop [success success
             possibilities possibilities]
        (case success
          (#.Some coverage')
          (do @
            [[success' possibilities'] (fuse-once coverage' possibilities)]
            (recur success' possibilities'))
          
          #.None
          (case (list.reverse possibilities)
            (#.Cons last prevs)
            (wrap (list/fold (function (_ left right) (#Alt left right))
                             last
                             prevs))

            #.Nil
            (undefined)))))

    _
    (if (C/= so-far addition)
      ## The addition cannot possibly improve the coverage.
      redundant-pattern
      ## There are now 2 alternative paths.
      (error/wrap (#Alt so-far addition)))))