(.module:
  [lux (#- if let case)
   [abstract
    [monad (#+ do)]]
   [control
    ["." function]
    ["ex" exception (#+ exception:)]]
   [data
    [text
     format]]
   [tool
    [compiler
     ["." synthesis (#+ Path Synthesis)]
     ["." phase ("operation/." monad)]]]]
  [luxc
   [lang
    [host
     ["$" jvm (#+ Label Inst Operation Phase)
      ["$t" type]
      ["_" inst]]]]]
  ["." // (#+ $Object)
   ["." 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
       (_.INVOKESTATIC //.runtime-class
                       "pm_peek"
                       ($t.method (list runtime.$Stack)
                                  (#.Some $Object)
                                  (list))
                       #0)))

(def: popI
  Inst
  (|>> (_.INVOKESTATIC //.runtime-class
                       "pm_pop"
                       ($t.method (list runtime.$Stack)
                                  (#.Some runtime.$Stack)
                                  (list))
                       #0)))

(def: pushI
  Inst
  (|>> (_.INVOKESTATIC //.runtime-class
                       "pm_push"
                       ($t.method (list runtime.$Stack $Object)
                                  (#.Some runtime.$Stack)
                                  (list))
                       #0)))

(def: (path' phase stack-depth @else @end path)
  (-> Phase Nat Label Label 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 #$.Boolean)
                           (jumpI @else))))
    
    (^ (synthesis.path/i64 value))
    (operation/wrap (|>> peekI
                         (_.unwrap #$.Long)
                         (_.long (.int value))
                         _.LCMP
                         (_.IFNE @else)))
    
    (^ (synthesis.path/f64 value))
    (operation/wrap (|>> peekI
                         (_.unwrap #$.Double)
                         (_.double value)
                         _.DCMPL
                         (_.IFNE @else)))
    
    (^ (synthesis.path/text value))
    (operation/wrap (|>> peekI
                         (_.string value)
                         (_.INVOKEVIRTUAL "java.lang.Object"
                                          "equals"
                                          ($t.method (list $Object)
                                                     (#.Some $t.boolean)
                                                     (list))
                                          #0)
                         (_.IFEQ @else)))
    
    (#synthesis.Then bodyS)
    (do phase.monad
      [bodyI (phase 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 ($t.descriptor runtime.$Variant))
                               (_.int (.int (<prepare> idx)))
                               <flag>
                               (_.INVOKESTATIC //.runtime-class "pm_variant"
                                               ($t.method (list runtime.$Variant runtime.$Tag runtime.$Flag)
                                                          (#.Some runtime.$Datum)
                                                          (list))
                                               #0)
                               _.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 (.let [accessI (.case lefts
                                     0
                                     _.AALOAD
                                     
                                     lefts
                                     (_.INVOKESTATIC //.runtime-class
                                                     "tuple_left"
                                                     ($t.method (list runtime.$Tuple $t.int)
                                                                (#.Some $Object)
                                                                (list))
                                                     #0))]
                      (|>> peekI
                           (_.CHECKCAST ($t.descriptor runtime.$Tuple))
                           (_.int (.int lefts))
                           accessI
                           pushI)))

    (^ (synthesis.member/right lefts))
    (operation/wrap (|>> peekI
                         (_.CHECKCAST ($t.descriptor runtime.$Tuple))
                         (_.int (.int lefts))
                         (_.INVOKESTATIC //.runtime-class
                                         "tuple_right"
                                         ($t.method (list runtime.$Tuple $t.int)
                                                    (#.Some $Object)
                                                    (list))
                                         #0)
                         pushI))

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

(def: (path phase path @end)
  (-> Phase Path Label (Operation Inst))
  (do phase.monad
    [@else _.make-label
     pathI (..path' phase 1 @else @end path)]
    (wrap (|>> pathI
               (_.label @else)
               _.POP
               (_.INVOKESTATIC //.runtime-class
                               "pm_fail"
                               ($t.method (list) #.None (list))
                               #0)
               _.NULL
               (_.GOTO @end)))))

(def: #export (if phase testS thenS elseS)
  (-> Phase Synthesis Synthesis Synthesis (Operation Inst))
  (do phase.monad
    [testI (phase testS)
     thenI (phase thenS)
     elseI (phase elseS)]
    (wrap (<| _.with-label (function (_ @else))
              _.with-label (function (_ @end))
              (|>> testI
                   (_.unwrap #$.Boolean)
                   (_.IFEQ @else)
                   thenI
                   (_.GOTO @end)
                   (_.label @else)
                   elseI
                   (_.label @end))))))

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

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