(;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>))))