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

(.using
 [library
  [lux (.except case)
   ["[0]" meta]
   [abstract
    ["[0]" monad (.only do)]]
   [control
    ["[0]" maybe]
    ["[0]" try]
    ["[0]" exception (.only exception:)]]
   [data
    ["[0]" product]
    [text
     ["%" format (.only format)]]
    [collection
     ["[0]" list ("[1]#[0]" mix monoid monad)]]]
   [math
    [number
     ["n" nat]]]
   [macro
    ["^" pattern]
    ["[0]" code]]
   ["[0]" type (.only)
    ["[0]" check (.only Check)]]]]
 ["[0]" /
  ["/[1]" //
   ["[1][0]" complex]
   ["/[1]" //
    ["[1][0]" extension]
    [//
     ["/" analysis (.only Analysis Operation Phase)
      ["[1][0]" simple]
      ["[1][0]" complex]
      ["[1][0]" pattern (.only Pattern)]
      ["[1][0]" type]
      ["[1][0]" scope]
      ["[1][0]" coverage (.only Coverage)]]
     [///
      ["[1]" phase]]]]]])

(exception: .public (mismatch [type Type
                               pattern Code])
  (exception.report
   "Type" (%.type type)
   "Pattern" (%.code pattern)))

(exception: .public (sum_has_no_case [case Nat
                                      type Type])
  (exception.report
   "Case" (%.nat case)
   "Type" (%.type type)))

(exception: .public (invalid [it Code])
  (exception.report
   "Pattern" (%.code it)))

(exception: .public (non_tuple [type Type])
  (exception.report
   "Type" (%.type type)))

(exception: .public (non_exhaustive [input Code
                                     branches (List [Code Code])
                                     coverage Coverage])
  (exception.report
   "Input" (%.code input)
   "Branches" (%.code (code.tuple (|> branches
                                      (list#each (function (_ [slot value])
                                                   (list slot value)))
                                      list#conjoint)))
   "Coverage" (/coverage.format coverage)))

(exception: .public empty_branches)

(def: (quantified envs baseT)
  (-> (List (List Type)) Type Type)
  (.case envs
    {.#End}
    baseT

    {.#Item head tail}
    (quantified tail {.#UnivQ head baseT})))

... 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: .public (tuple :it:)
  (-> Type (Check [(List check.Var) Type]))
  (loop (again [envs (is (List (List Type))
                         (list))
                :it: :it:])
    (.case :it:
      {.#Var id}
      (do check.monad
        [?:it:' (check.peek id)]
        (.case ?:it:'
          {.#Some :it:'}
          (again envs :it:')

          _
          (check.except ..non_tuple :it:)))

      {.#Named name unnamedT}
      (again envs unnamedT)

      {.#UnivQ env unquantifiedT}
      (again {.#Item env envs} unquantifiedT)

      {.#ExQ _}
      (do check.monad
        [[@head :head:] check.var
         [tail :tuple:] (again envs (maybe.trusted (type.applied (list :head:) :it:)))]
        (in [(partial_list @head tail) :tuple:]))

      {.#Apply _}
      (do [! check.monad]
        [.let [[:abstraction: :parameters:] (type.flat_application :it:)]
         :abstraction: (.case :abstraction:
                         {.#Var @abstraction}
                         (do !
                           [?:abstraction: (check.peek @abstraction)]
                           (.case ?:abstraction:
                             {.#Some :abstraction:}
                             (in :abstraction:)

                             _
                             (check.except ..non_tuple :it:)))

                         _
                         (in :abstraction:))]
        (.case (type.applied :parameters: :abstraction:)
          {.#Some :it:}
          (again envs :it:)

          {.#None}
          (check.except ..non_tuple :it:)))

      {.#Product _}
      (|> :it:
          type.flat_tuple
          (list#each (..quantified envs))
          type.tuple
          [(list)]
          (# check.monad in))

      _
      (# check.monad in [(list) (..quantified envs :it:)]))))

(def: (simple_pattern_analysis type :input: location output next)
  (All (_ a) (-> Type Type Location Pattern (Operation a) (Operation [Pattern a])))
  (/.with_location location
    (do ///.monad
      [_ (/type.check (check.check :input: type))
       outputA next]
      (in [output outputA]))))

(def: (tuple_pattern_analysis pattern_analysis :input: sub_patterns next)
  (All (_ a)
    (-> (-> (Maybe Nat) Type Code (Operation a) (Operation [Pattern a]))
        Type (List Code) (Operation a) (Operation [Pattern a])))
  (do [! ///.monad]
    [[@ex_var+ :input:'] (/type.check (..tuple :input:))]
    (.case :input:'
      {.#Product _}
      (let [matches (loop (again [types (type.flat_tuple :input:')
                                  patterns sub_patterns
                                  output (is (List [Type Code])
                                             {.#End})])
                      (.case [types patterns]
                        [{.#End} {.#End}]
                        output

                        [{.#Item headT {.#End}} {.#Item headP {.#End}}]
                        {.#Item [headT headP] output}

                        [remainingT {.#Item headP {.#End}}]
                        {.#Item [(type.tuple remainingT) headP] output}

                        [{.#Item headT {.#End}} remainingP]
                        {.#Item [headT (code.tuple remainingP)] output}
                        
                        [{.#Item headT tailT} {.#Item headP tailP}]
                        (again tailT tailP {.#Item [headT headP] output})

                        _
                        (undefined)))]
        (do !
          [[memberP+ thenA] (list#mix (is (All (_ a)
                                            (-> [Type Code] (Operation [(List Pattern) a])
                                                (Operation [(List Pattern) a])))
                                          (function (_ [memberT memberC] then)
                                            (do !
                                              [[memberP [memberP+ thenA]] ((as (All (_ a) (-> (Maybe Nat) Type Code (Operation a) (Operation [Pattern a])))
                                                                               pattern_analysis)
                                                                           {.#None} memberT memberC then)]
                                              (in [(partial_list memberP memberP+) thenA]))))
                                      (do !
                                        [nextA next]
                                        (in [(list) nextA]))
                                      matches)
           _ (/type.check (monad.each check.monad check.forget! @ex_var+))]
          (in [(/pattern.tuple memberP+)
               thenA])))

      _
      (/.except ..mismatch [:input:' (code.tuple sub_patterns)]))))

... 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: (pattern_analysis num_tags :input: pattern next)
  (All (_ a) (-> (Maybe Nat) Type Code (Operation a) (Operation [Pattern a])))
  (.case pattern
    [location {.#Symbol ["" name]}]
    (/.with_location location
      (do ///.monad
        [outputA (/scope.with_local [name :input:]
                   next)
         idx /scope.next]
        (in [{/pattern.#Bind idx} outputA])))

    (^.template [<type> <input> <output>]
      [[location <input>]
       (simple_pattern_analysis <type> :input: location {/pattern.#Simple <output>} next)])
    ([Bit  {.#Bit pattern_value}  {/simple.#Bit pattern_value}]
     [Nat  {.#Nat pattern_value}  {/simple.#Nat pattern_value}]
     [Int  {.#Int pattern_value}  {/simple.#Int pattern_value}]
     [Rev  {.#Rev pattern_value}  {/simple.#Rev pattern_value}]
     [Frac {.#Frac pattern_value} {/simple.#Frac pattern_value}]
     [Text {.#Text pattern_value} {/simple.#Text pattern_value}]
     [Any  {.#Tuple {.#End}}      {/simple.#Unit}])
    
    (pattern [location {.#Tuple (list singleton)}])
    (pattern_analysis {.#None} :input: singleton next)
    
    [location {.#Tuple sub_patterns}]
    (/.with_location location
      (do [! ///.monad]
        [record (//complex.normal true sub_patterns)
         record_size,members,recordT (is (Operation (Maybe [Nat (List Code) Type]))
                                         (.case record
                                           {.#Some record}
                                           (//complex.order true record)

                                           {.#None}
                                           (in {.#None})))]
        (.case record_size,members,recordT
          {.#Some [record_size members recordT]}
          (do !
            [_ (.case :input:
                 {.#Var @input}
                 (/type.check (do check.monad
                                [? (check.bound? @input)]
                                (if ?
                                  (in [])
                                  (check.check :input: recordT))))

                 _
                 (in []))]
            (.case members
              (pattern (list singleton))
              (pattern_analysis {.#None} :input: singleton next)

              _
              (..tuple_pattern_analysis pattern_analysis :input: members next)))
          
          {.#None}
          (..tuple_pattern_analysis pattern_analysis :input: sub_patterns next))))

    (pattern [location {.#Variant (partial_list [_ {.#Nat lefts}] [_ {.#Bit right?}] values)}])
    (/.with_location location
      (do ///.monad
        [[@ex_var+ :input:'] (/type.check (..tuple :input:))]
        (.case :input:'
          {.#Sum _}
          (let [flat_sum (type.flat_variant :input:')
                size_sum (list.size flat_sum)
                num_cases (maybe.else size_sum num_tags)
                idx (/complex.tag right? lefts)]
            (.case (list.item idx flat_sum)
              (^.multi {.#Some caseT}
                       (n.< num_cases idx))
              (do ///.monad
                [[testP nextA] (if (and (n.> num_cases size_sum)
                                        (n.= (-- num_cases) idx))
                                 (pattern_analysis {.#None}
                                                   (type.variant (list.after (-- num_cases) flat_sum))
                                                   (` [(~+ values)])
                                                   next)
                                 (pattern_analysis {.#None} caseT (` [(~+ values)]) next))
                 _ (/type.check (monad.each check.monad check.forget! @ex_var+))]
                (in [(/pattern.variant [lefts right? testP])
                     nextA]))

              _
              (/.except ..sum_has_no_case [idx :input:])))

          {.#UnivQ _}
          (do ///.monad
            [[ex_id exT] (/type.check check.existential)
             it (pattern_analysis num_tags
                                  (maybe.trusted (type.applied (list exT) :input:'))
                                  pattern
                                  next)
             _ (/type.check (monad.each check.monad check.forget! @ex_var+))]
            (in it))
          
          _
          (/.except ..mismatch [:input:' pattern]))))

    (pattern [location {.#Variant (partial_list [_ {.#Symbol tag}] values)}])
    (/.with_location location
      (do ///.monad
        [tag (///extension.lifted (meta.normal tag))
         [idx group variantT] (///extension.lifted (meta.tag tag))
         _ (/type.check (check.check :input: variantT))
         .let [[lefts right?] (/complex.choice (list.size group) idx)]]
        (pattern_analysis {.#Some (list.size group)} :input: (` {(~ (code.nat lefts)) (~ (code.bit right?)) (~+ values)}) next)))

    _
    (/.except ..invalid [pattern])
    ))

(def: .public (case analyse branches archive inputC)
  (-> Phase (List [Code Code]) Phase)
  (.case branches
    {.#Item [patternH bodyH] branchesT}
    (do [! ///.monad]
      [[:input: inputA] (<| /type.inferring
                            (analyse archive inputC))
       outputH (pattern_analysis {.#None} :input: patternH (analyse archive bodyH))
       outputT (monad.each !
                           (function (_ [patternT bodyT])
                             (pattern_analysis {.#None} :input: patternT (analyse archive bodyT)))
                           branchesT)
       outputHC (|> outputH product.left /coverage.coverage /.of_try)
       outputTC (monad.each ! (|>> product.left /coverage.coverage /.of_try) outputT)
       _ (.case (monad.mix try.monad /coverage.composite outputHC outputTC)
           {try.#Success coverage}
           (///.assertion ..non_exhaustive [inputC branches coverage]
                          (/coverage.exhaustive? coverage))

           {try.#Failure error}
           (/.failure error))]
      (in {/.#Case inputA [outputH outputT]}))

    {.#End}
    (/.except ..empty_branches [])))