path: root/stdlib/source/lux/language/compiler/analysis/case/coverage.lux

(.module:
  [lux #*
   [control
    [monad (#+ do)]
    ["ex" exception (#+ exception:)]
    equivalence]
   [data
    [bit ("bit/" Equivalence<Bit>)]
    [number]
    ["e" error ("error/" Monad<Error>)]
    [maybe]
    [text format]
    [collection
     [list ("list/" Fold<List>)]
     ["dict" dictionary (#+ Dictionary)]]]]
  [//// ("operation/" Monad<Operation>)]
  [/// (#+ Pattern Variant Operation)])

(def: cases
  (-> (Maybe Nat) Nat)
  (|>> (maybe.default +0)))

(def: (variant sum-side)
  (-> (Either Pattern Pattern) (Variant Pattern))
  (loop [lefts +0
         variantP sum-side]
    (case variantP
      (#.Left valueP)
      (case valueP
        (#///.Complex (#///.Sum value-side))
        (recur (inc lefts) value-side)

        _
        {#///.lefts lefts
         #///.right? false
         #///.value valueP})
      
      (#.Right valueP)
      {#///.lefts lefts
       #///.right? true
       #///.value valueP})))

## 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 bits
## and variants.
(type: #export #rec Coverage
  #Partial
  (#Bit Bit)
  (#Variant (Maybe Nat) (Dictionary Nat Coverage))
  (#Seq Coverage Coverage)
  (#Alt Coverage Coverage)
  #Exhaustive)

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

    _
    false))

(def: #export (determine pattern)
  (-> Pattern (Operation Coverage))
  (case pattern
    (^or (#///.Simple #///.Unit)
         (#///.Bind _))
    (operation/wrap #Exhaustive)

    ## Primitive patterns always have partial coverage because there
    ## are too many possibilities as far as values go.
    (^template [<tag>]
      (#///.Simple (<tag> _))
      (operation/wrap #Partial))
    ([#///.Nat]
     [#///.Int]
     [#///.Rev]
     [#///.Frac]
     [#///.Text])

    ## Bits are the exception, since there is only "true" and
    ## "false", which means it is possible for bit
    ## pattern-matching to become exhaustive if complementary parts meet.
    (#///.Simple (#///.Bit value))
    (operation/wrap (#Bit value))

    ## Tuple patterns can be exhaustive if there is exhaustiveness for all of
    ## their sub-patterns.
    (#///.Complex (#///.Product [left right]))
    (do ////.Monad<Operation>
      [left (determine left)
       right (determine right)]
      (case right
        (#Exhaustive _)
        (wrap left)

        _
        (wrap (#Seq left right))))

    (#///.Complex (#///.Sum sum-side))
    (let [[variant-lefts variant-right? variant-value] (variant sum-side)]
      ## Variant patterns can be shown to be exhaustive if all the possible
      ## cases are handled exhaustively.
      (do ////.Monad<Operation>
        [value-coverage (determine variant-value)
         #let [variant-idx (if variant-right?
                             (inc variant-lefts)
                             variant-lefts)]]
        (wrap (#Variant (if variant-right?
                          (#.Some variant-idx)
                          #.None)
                        (|> (dict.new number.Hash<Nat>)
                            (dict.put variant-idx value-coverage))))))))

(def: (xor left right)
  (-> Bit Bit Bit)
  (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)))

(structure: _ (Equivalence Coverage)
  (def: (= reference sample)
    (case [reference sample]
      [#Exhaustive #Exhaustive]
      true

      [(#Bit sideR) (#Bit sideS)]
      (bit/= sideR sideS)

      [(#Variant allR casesR) (#Variant allS casesS)]
      (and (n/= (cases allR)
                (cases allS))
           (:: (dict.Equivalence<Dictionary> =) = 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: "C/" Equivalence<Coverage>)

## 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 bit coverages are exhaustive if they complement one another.
    (^multi [(#Bit sideA) (#Bit sideSF)]
            (xor sideA sideSF))
    (error/wrap #Exhaustive)

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

          (:: (dict.Equivalence<Dictionary> Equivalence<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/= (cases 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)))))