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

(.module:
  [library
   [lux {"-" [Variant]}
    [abstract
     equivalence
     ["[0]" monad {"+" [do]}]]
    [control
     ["[0]" maybe]
     ["[0]" try {"+" [Try]} ("[1]\[0]" monad)]
     ["[0]" exception {"+" [exception:]}]]
    [data
     ["[0]" bit ("[1]\[0]" equivalence)]
     ["[0]" text
      ["%" format {"+" [Format format]}]]
     [collection
      ["[0]" list ("[1]\[0]" functor mix)]
      ["[0]" dictionary {"+" [Dictionary]}]]]
    [math
     [number
      ["n" nat]]]]]
  ["[0]" //// "_"
   [//
    ["/" analysis {"+" [Pattern Variant Operation]}]
    [///
     ["[1]" phase ("[1]\[0]" monad)]]]])

(exception: .public invalid_tuple_pattern
  "Tuple size must be >= 2")

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

(def: known_cases?
  (-> Nat Bit)
  (n.> 0))

... 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: .public Coverage
  (Rec Coverage
    (.Variant
     #Partial
     {#Bit Bit}
     {#Variant (Maybe Nat) (Dictionary Nat Coverage)}
     {#Seq Coverage Coverage}
     {#Alt Coverage Coverage}
     #Exhaustive)))

(def: .public (exhaustive? coverage)
  (-> Coverage Bit)
  (case coverage
    {#Exhaustive _}
    #1

    _
    #0))

(def: .public (%coverage value)
  (Format Coverage)
  (case value
    #Partial
    "#Partial"
    
    {#Bit value'}
    (|> value'
        %.bit
        (text.enclosed ["{#Bit " "}"]))
    
    {#Variant ?max_cases cases}
    (|> cases
        dictionary.entries
        (list\each (function (_ [idx coverage])
                     (format (%.nat idx) " " (%coverage coverage))))
        (text.interposed " ")
        (text.enclosed ["{" "}"])
        (format (%.nat (..cases ?max_cases)) " ")
        (text.enclosed ["{#Variant " "}"]))

    {#Seq left right}
    (format "{#Seq " (%coverage left) " " (%coverage right) "}")
    
    {#Alt left right}
    (format "{#Alt " (%coverage left) " " (%coverage right) "}")

    #Exhaustive
    "#Exhaustive"))

(def: .public (determine pattern)
  (-> Pattern (Operation Coverage))
  (case pattern
    (^or {#/.Simple #/.Unit}
         {#/.Bind _})
    (////\in #Exhaustive)

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

    ... Bits are the exception, since there is only "#1" and
    ... "#0", which means it is possible for bit
    ... pattern-matching to become exhaustive if complementary parts meet.
    {#/.Simple {#/.Bit value}}
    (////\in {#Bit value})

    ... Tuple patterns can be exhaustive if there is exhaustiveness for all of
    ... their sub-patterns.
    {#/.Complex {#/.Tuple membersP+}}
    (case (list.reversed membersP+)
      (^or #.End {#.Item _ #.End})
      (/.except ..invalid_tuple_pattern [])
      
      {#.Item lastP prevsP+}
      (do ////.monad
        [lastC (determine lastP)]
        (monad.mix ////.monad
                   (function (_ leftP rightC)
                     (do ////.monad
                       [leftC (determine leftP)]
                       (case rightC
                         #Exhaustive
                         (in leftC)

                         _
                         (in {#Seq leftC rightC}))))
                   lastC prevsP+)))

    ... Variant patterns can be shown to be exhaustive if all the possible
    ... cases are handled exhaustively.
    {#/.Complex {#/.Variant [lefts right? value]}}
    (do ////.monad
      [value_coverage (determine value)
       .let [idx (if right?
                   (++ lefts)
                   lefts)]]
      (in {#Variant (if right?
                      {#.Some idx}
                      #.None)
           (|> (dictionary.empty n.hash)
               (dictionary.has 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.
(exception: .public (redundant_pattern [so_far Coverage
                                        addition Coverage])
  (exception.report
   ["Coverage so-far" (%coverage so_far)]
   ["Coverage addition" (%coverage addition)]))

(def: (flat_alt coverage)
  (-> Coverage (List Coverage))
  (case coverage
    {#Alt left right}
    (list& left (flat_alt right))

    _
    (list coverage)))

(implementation: equivalence (Equivalence Coverage)
  (def: (= reference sample)
    (case [reference sample]
      [#Exhaustive #Exhaustive]
      #1

      [{#Bit sideR} {#Bit sideS}]
      (bit\= sideR sideS)

      [{#Variant allR casesR} {#Variant allS casesS}]
      (and (n.= (cases allR)
                (cases allS))
           (\ (dictionary.equivalence =) = casesR casesS))
      
      [{#Seq leftR rightR} {#Seq leftS rightS}]
      (and (= leftR leftS)
           (= rightR rightS))

      [{#Alt _} {#Alt _}]
      (let [flatR (flat_alt reference)
            flatS (flat_alt sample)]
        (and (n.= (list.size flatR) (list.size flatS))
             (list.every? (function (_ [coverageR coverageS])
                            (= coverageR coverageS))
                          (list.zipped/2 flatR flatS))))

      _
      #0)))

(open: "coverage/[0]" ..equivalence)

(exception: .public (variants_do_not_match [addition_cases Nat
                                            so_far_cases Nat])
  (exception.report
   ["So-far Cases" (%.nat so_far_cases)]
   ["Addition Cases" (%.nat addition_cases)]))

... 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: .public (merged addition so_far)
  (-> Coverage Coverage (Try Coverage))
  (case [addition so_far]
    [#Partial #Partial]
    (try\in #Partial)

    ... 2 bit coverages are exhaustive if they complement one another.
    (^multi [{#Bit sideA} {#Bit sideSF}]
            (xor sideA sideSF))
    (try\in #Exhaustive)

    [{#Variant allA casesA} {#Variant allSF casesSF}]
    (let [addition_cases (cases allSF)
          so_far_cases (cases allA)]
      (cond (and (known_cases? addition_cases)
                 (known_cases? so_far_cases)
                 (not (n.= addition_cases so_far_cases)))
            (exception.except ..variants_do_not_match [addition_cases so_far_cases])

            (\ (dictionary.equivalence ..equivalence) = casesSF casesA)
            (exception.except ..redundant_pattern [so_far addition])

            ... else
            (do [! try.monad]
              [casesM (monad.mix !
                                 (function (_ [tagA coverageA] casesSF')
                                   (case (dictionary.value tagA casesSF')
                                     {#.Some coverageSF}
                                     (do !
                                       [coverageM (merged coverageA coverageSF)]
                                       (in (dictionary.has tagA coverageM casesSF')))

                                     #.None
                                     (in (dictionary.has tagA coverageA casesSF'))))
                                 casesSF (dictionary.entries casesA))]
              (in (if (and (or (known_cases? addition_cases)
                               (known_cases? so_far_cases))
                           (n.= (++ (n.max addition_cases so_far_cases))
                                (dictionary.size casesM))
                           (list.every? exhaustive? (dictionary.values casesM)))
                    #Exhaustive
                    {#Variant (case allSF
                                {#.Some _}
                                allSF

                                _
                                allA)
                     casesM})))))

    [{#Seq leftA rightA} {#Seq leftSF rightSF}]
    (case [(coverage/= leftSF leftA) (coverage/= rightSF rightA)]
      ... Same prefix
      [#1 #0]
      (do try.monad
        [rightM (merged 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).
          (in leftSF)
          (in {#Seq leftSF rightM})))

      ... Same suffix
      [#0 #1]
      (do try.monad
        [leftM (merged leftA leftSF)]
        (in {#Seq leftM rightA}))

      ... The 2 sequences cannot possibly be merged.
      [#0 #0]
      (try\in {#Alt so_far addition})

      ... There is nothing the addition adds to the coverage.
      [#1 #1]
      (exception.except ..redundant_pattern [so_far addition]))

    ... The addition cannot possibly improve the coverage.
    [_ #Exhaustive]
    (exception.except ..redundant_pattern [so_far addition])

    ... The addition completes the coverage.
    [#Exhaustive _]
    (try\in #Exhaustive)
    
    ... The left part will always match, so the addition is redundant.
    (^multi [{#Seq left right} single]
            (coverage/= left single))
    (exception.except ..redundant_pattern [so_far addition])

    ... The right part is not necessary, since it can always match the left.
    (^multi [single {#Seq left right}]
            (coverage/= left single))
    (try\in 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 [! try.monad]
      [.let [fuse_once (: (-> Coverage (List Coverage)
                              (Try [(Maybe Coverage)
                                    (List Coverage)]))
                          (function (_ coverageA possibilitiesSF)
                            (loop [altsSF possibilitiesSF]
                              (case altsSF
                                #.End
                                (in [#.None (list coverageA)])
                                
                                {#.Item altSF altsSF'}
                                (case (merged coverageA altSF)
                                  {#try.Success altMSF}
                                  (case altMSF
                                    {#Alt _}
                                    (do !
                                      [[success altsSF+] (recur altsSF')]
                                      (in [success {#.Item altSF altsSF+}]))

                                    _
                                    (in [{#.Some altMSF} altsSF']))
                                  
                                  {#try.Failure error}
                                  {#try.Failure error})
                                ))))]
       [successA possibilitiesSF] (fuse_once addition (flat_alt so_far))]
      (loop [successA successA
             possibilitiesSF possibilitiesSF]
        (case successA
          {#.Some coverageA'}
          (do !
            [[successA' possibilitiesSF'] (fuse_once coverageA' possibilitiesSF)]
            (recur successA' possibilitiesSF'))
          
          #.None
          (case (list.reversed possibilitiesSF)
            {#.Item last prevs}
            (in (list\mix (function (_ left right) {#Alt left right})
                          last
                          prevs))

            #.End
            (undefined)))))

    _
    (if (coverage/= so_far addition)
      ... The addition cannot possibly improve the coverage.
      (exception.except ..redundant_pattern [so_far addition])
      ... There are now 2 alternative paths.
      (try\in {#Alt so_far addition}))))