(.module:
  [lux (#- Type if let case)
   [abstract
    [monad (#+ do)]]
   [control
    ["." function]
    ["ex" exception (#+ exception:)]]
   [data
    [number
     ["n" nat]]
    [collection
     ["." list ("#@." fold)]]]
   [target
    [jvm
     ["." type (#+ Type)
      ["." category (#+ Void Value Return Primitive Object Class Array Var Parameter Method)]
      ["." descriptor (#+ Descriptor)]
      ["." signature (#+ Signature)]]]]
   [tool
    [compiler
     ["." phase ("operation@." monad)]
     [meta
      [archive (#+ Archive)]]
     [language
      [lux
       ["." synthesis (#+ Path Synthesis)]]]]]]
  [luxc
   [lang
    [host
     ["$" jvm (#+ Label Inst Operation Phase Generator)
      ["_" inst]]]]]
  ["." //
   ["." runtime]])

(def: (pop-altI stack-depth)
  (-> Nat Inst)
  (.case stack-depth
    0 function.identity
    1 _.POP
    2 _.POP2
    _ ## (n.> 2)
    (|>> _.POP2
         (pop-altI (n.- 2 stack-depth)))))

(def: peekI
  Inst
  (|>> _.DUP
       (_.int +0)
       _.AALOAD))

(def: pushI
  Inst
  (_.INVOKESTATIC //.$Runtime "pm_push" (type.method [(list runtime.$Stack //.$Value) runtime.$Stack (list)])))

(def: popI
  (|>> (_.int +1)
       _.AALOAD
       (_.CHECKCAST runtime.$Stack)))

(def: (left-projection lefts)
  (-> Nat Inst)
  (.let [accessI (.case lefts
                   0
                   _.AALOAD
                   
                   lefts
                   (_.INVOKESTATIC //.$Runtime "tuple_left" (type.method [(list //.$Tuple runtime.$Index) //.$Value (list)])))]
    (|>> (_.CHECKCAST //.$Tuple)
         (_.int (.int lefts))
         accessI)))

(def: (right-projection lefts)
  (-> Nat Inst)
  (|>> (_.CHECKCAST //.$Tuple)
       (_.int (.int lefts))
       (_.INVOKESTATIC //.$Runtime "tuple_right" (type.method [(list //.$Tuple runtime.$Index) //.$Value (list)]))))

(def: (path' stack-depth @else @end phase archive path)
  (-> Nat Label Label Phase Archive Path (Operation Inst))
  (.case path
    #synthesis.Pop
    (operation@wrap ..popI)
    
    (#synthesis.Bind register)
    (operation@wrap (|>> peekI
                         (_.ASTORE register)))

    (^ (synthesis.path/bit value))
    (operation@wrap (.let [jumpI (.if value _.IFEQ _.IFNE)]
                      (|>> peekI
                           (_.unwrap type.boolean)
                           (jumpI @else))))
    
    (^ (synthesis.path/i64 value))
    (operation@wrap (|>> peekI
                         (_.unwrap type.long)
                         (_.long (.int value))
                         _.LCMP
                         (_.IFNE @else)))
    
    (^ (synthesis.path/f64 value))
    (operation@wrap (|>> peekI
                         (_.unwrap type.double)
                         (_.double value)
                         _.DCMPL
                         (_.IFNE @else)))
    
    (^ (synthesis.path/text value))
    (operation@wrap (|>> peekI
                         (_.string value)
                         (_.INVOKEVIRTUAL (type.class "java.lang.Object" (list))
                                          "equals"
                                          (type.method [(list //.$Value) type.boolean (list)]))
                         (_.IFEQ @else)))
    
    (#synthesis.Then bodyS)
    (do phase.monad
      [bodyI (phase archive bodyS)]
      (wrap (|>> (pop-altI stack-depth)
                 bodyI
                 (_.GOTO @end))))
    
    (^template [<pattern> <flag> <prepare>]
      (^ (<pattern> idx))
      (operation@wrap (<| _.with-label (function (_ @success))
                          _.with-label (function (_ @fail))
                          (|>> peekI
                               (_.CHECKCAST //.$Variant)
                               (_.int (.int (<prepare> idx)))
                               <flag>
                               (_.INVOKESTATIC //.$Runtime "pm_variant" (type.method [(list //.$Variant runtime.$Tag runtime.$Flag) runtime.$Value (list)]))
                               _.DUP
                               (_.IFNULL @fail)
                               (_.GOTO @success)
                               (_.label @fail)
                               _.POP
                               (_.GOTO @else)
                               (_.label @success)
                               pushI))))
    ([synthesis.side/left  _.NULL        function.identity]
     [synthesis.side/right (_.string "") .inc])

    (^ (synthesis.member/left lefts))
    (operation@wrap (|>> peekI
                         (..left-projection lefts)
                         pushI))

    (^ (synthesis.member/right lefts))
    (operation@wrap (|>> peekI
                         (..right-projection lefts)
                         pushI))

    ## Extra optimization
    (^ (synthesis.path/seq
        (synthesis.member/left 0)
        (synthesis.!bind-top register thenP)))
    (do phase.monad
      [then! (path' stack-depth @else @end phase archive thenP)]
      (wrap (|>> peekI
                 (_.CHECKCAST //.$Tuple)
                 (_.int +0)
                 _.AALOAD
                 (_.ASTORE register)
                 then!)))

    ## Extra optimization
    (^template [<pm> <getter>]
      (^ (synthesis.path/seq
          (<pm> lefts)
          (synthesis.!bind-top register thenP)))
      (do phase.monad
        [then! (path' stack-depth @else @end phase archive thenP)]
        (wrap (|>> peekI
                   (_.CHECKCAST //.$Tuple)
                   (_.int (.int lefts))
                   (_.INVOKESTATIC //.$Runtime <getter> (type.method [(list //.$Tuple runtime.$Index) //.$Value (list)]))
                   (_.ASTORE register)
                   then!))))
    ([synthesis.member/left  "tuple_left"]
     [synthesis.member/right "tuple_right"])

    (#synthesis.Alt leftP rightP)
    (do phase.monad
      [@alt-else _.make-label
       leftI (path' (inc stack-depth) @alt-else @end phase archive leftP)
       rightI (path' stack-depth @else @end phase archive rightP)]
      (wrap (|>> _.DUP
                 leftI
                 (_.label @alt-else)
                 _.POP
                 rightI)))
    
    (#synthesis.Seq leftP rightP)
    (do phase.monad
      [leftI (path' stack-depth @else @end phase archive leftP)
       rightI (path' stack-depth @else @end phase archive rightP)]
      (wrap (|>> leftI
                 rightI)))
    ))

(def: (path @end phase archive path)
  (-> Label Phase Archive Path (Operation Inst))
  (do phase.monad
    [@else _.make-label
     pathI (..path' 1 @else @end phase archive path)]
    (wrap (|>> pathI
               (_.label @else)
               _.POP
               (_.INVOKESTATIC //.$Runtime "pm_fail" (type.method [(list) type.void (list)]))
               _.NULL
               (_.GOTO @end)))))

(def: #export (if phase archive [testS thenS elseS])
  (Generator [Synthesis Synthesis Synthesis])
  (do phase.monad
    [testI (phase archive testS)
     thenI (phase archive thenS)
     elseI (phase archive elseS)]
    (wrap (<| _.with-label (function (_ @else))
              _.with-label (function (_ @end))
              (|>> testI
                   (_.unwrap type.boolean)
                   (_.IFEQ @else)
                   thenI
                   (_.GOTO @end)
                   (_.label @else)
                   elseI
                   (_.label @end))))))

(def: #export (let phase archive [inputS register exprS])
  (Generator [Synthesis Nat Synthesis])
  (do phase.monad
    [inputI (phase archive inputS)
     exprI (phase archive exprS)]
    (wrap (|>> inputI
               (_.ASTORE register)
               exprI))))

(def: #export (get phase archive [path recordS])
  (Generator [(List synthesis.Member) Synthesis])
  (do phase.monad
    [recordG (phase archive recordS)]
    (wrap (list@fold (function (_ step so-far)
                       (.let [next (.case step
                                     (#.Left lefts)
                                     (..left-projection lefts)
                                     
                                     (#.Right lefts)
                                     (..right-projection lefts))]
                         (|>> so-far next)))
                     recordG
                     path))))

(def: #export (case phase archive [valueS path])
  (Generator [Synthesis Path])
  (do phase.monad
    [@end _.make-label
     valueI (phase archive valueS)
     pathI (..path @end phase archive path)]
    (wrap (|>> _.NULL
               valueI
               pushI
               pathI
               (_.label @end)))))