(.module:
  lux
  (lux (data [bool "bool/" Eq<Bool>]
             [text "text/" Eq<Text>]
             text/format
             [number]
             (coll [list "list/" Fold<List> Monoid<List>]))
       (macro [code "code/" Eq<Code>]))
  (luxc (lang [".L" variable #+ Variable]
              ["la" analysis]
              ["ls" synthesis]
              (synthesis [".S" function]))))

(def: popPS ls.Path (' ("lux case pop")))

(def: (path' arity num-locals pattern)
  (-> ls.Arity Nat la.Pattern [Nat (List ls.Path)])
  (case pattern
    (^code ("lux case tuple" [(~+ membersP)]))
    (case membersP
      #.Nil
      [num-locals
       (list popPS)]

      (#.Cons singletonP #.Nil)
      (path' arity num-locals singletonP)

      (#.Cons _)
      (let [last-idx (n/dec (list.size membersP))
            [_ output] (list/fold (: (-> la.Pattern [Nat [Nat (List ls.Path)]] [Nat [Nat (List ls.Path)]])
                                     (function (_ current-pattern [current-idx num-locals' next])
                                       (let [[num-locals'' current-path] (path' arity num-locals' current-pattern)]
                                         [(n/dec current-idx)
                                          num-locals''
                                          (|> (list (if (n/= last-idx current-idx)
                                                      (` ("lux case tuple right" (~ (code.nat current-idx))))
                                                      (` ("lux case tuple left" (~ (code.nat current-idx))))))
                                              (list/compose current-path)
                                              (list/compose next))])))
                                  [last-idx num-locals (list popPS)]
                                  (list.reverse membersP))]
        output))

    (^code ("lux case variant" (~ [_ (#.Nat tag)]) (~ [_ (#.Nat num-tags)]) (~ memberP)))
    (let [[num-locals' member-path] (path' arity num-locals memberP)]
      [num-locals' (|> (list (if (n/= (n/dec num-tags) tag)
                               (` ("lux case variant right" (~ (code.nat tag))))
                               (` ("lux case variant left" (~ (code.nat tag))))))
                       (list/compose member-path)
                       (list& popPS))])

    (^code ("lux case bind" (~ [_ (#.Nat register)])))
    [(n/inc num-locals)
     (list popPS
           (` ("lux case bind" (~ (code.nat (if (functionS.nested? arity)
                                              (n/+ (n/dec arity) register)
                                              register))))))]

    _
    [num-locals
     (list popPS pattern)]))

(def: (clean-unnecessary-pops paths)
  (-> (List ls.Path) (List ls.Path))
  (case paths
    (#.Cons path paths')
    (if (is? popPS path)
      (clean-unnecessary-pops paths')
      paths)

    #.Nil
    paths))

(def: #export (path arity num-locals synthesize pattern bodyA)
  (->  ls.Arity Nat (-> Nat la.Analysis ls.Synthesis) la.Pattern la.Analysis ls.Path)
  (let [[num-locals' pieces] (path' arity num-locals pattern)]
    (|> pieces
        clean-unnecessary-pops
        (list/fold (function (_ pre post)
                     (` ("lux case seq" (~ pre) (~ post))))
                   (` ("lux case exec" (~ (synthesize num-locals' bodyA))))))))

(def: #export (weave leftP rightP)
  (-> ls.Path ls.Path ls.Path)
  (with-expansions [<default> (as-is (` ("lux case alt" (~ leftP) (~ rightP))))]
    (case [leftP rightP]
      (^ [(^code ("lux case seq" (~ preL) (~ postL)))
          (^code ("lux case seq" (~ preR) (~ postR)))])
      (case (weave preL preR)
        (^code ("lux case alt" (~ thenP) (~ elseP)))
        <default>

        weavedP
        (` ("lux case seq" (~ weavedP) (~ (weave postL postR)))))

      _
      (if (code/= leftP rightP)
        rightP
        <default>))))