(.using
  [library
   [lux {"-" Type Label int try}
    ["[0]" ffi {"+" import:}]
    [abstract
     [monoid {"+" Monoid}]
     ["[0]" monad {"+" Monad do}]]
    [control
     ["[0]" writer {"+" Writer}]
     ["[0]" state {"+" +State}]
     ["[0]" function]
     ["[0]" maybe]
     ["[0]" try {"+" Try}]
     ["[0]" exception {"+" exception:}]]
    [data
     ["[0]" product]
     [text
      ["%" format {"+" format}]]
     [collection
      ["[0]" list ("[1]#[0]" functor mix)]
      ["[0]" dictionary {"+" Dictionary}]
      ["[0]" sequence {"+" Sequence}]]]
    [macro
     ["[0]" template]]
    [math
     [number
      ["n" nat]
      ["i" int]
      ["[0]" i32 {"+" I32}]]]]]
  ["[0]" / "_"
   ["[1][0]" address {"+" Address}]
   ["[1][0]" jump {"+" Jump Big_Jump}]
   ["_" instruction {"+" Primitive_Array_Type Instruction Estimator} ("[1]#[0]" monoid)]
   ["[1][0]" environment {"+" Environment}
    [limit
     ["/[0]" registry {"+" Register Registry}]
     ["/[0]" stack {"+" Stack}]]]
   ["/[1]" // "_"
    ["[1][0]" index {"+" Index}]
    [encoding
     ["[1][0]" name]
     ["[1][0]" unsigned {"+" U1 U2}]
     ["[1][0]" signed {"+" S1 S2 S4}]]
    ["[1][0]" constant {"+" UTF8}
     ["[1]/[0]" pool {"+" Pool Resource}]]
    [attribute
     [code
      ["[1][0]" exception {"+" Exception}]]]
    ["[0]" type {"+" Type}
     [category {"+" Class Object Value' Value Return' Return Method}]
     ["[0]" reflection]
     ["[0]" parser]]]])

(type: .public Label
  Nat)

(type: .public Resolver
  (Dictionary Label [Stack (Maybe Address)]))

(type: .public Tracker
  (Record
   [#program_counter Address
    #next Label
    #known Resolver]))

(def: fresh
  Tracker
  [#program_counter /address.start
   #next 0
   #known (dictionary.empty n.hash)])

(type: .public Relative
  (-> Resolver (Try [(Sequence Exception) Instruction])))

(def: no_exceptions
  (Sequence Exception)
  sequence.empty)

(def: relative_identity
  Relative
  (function.constant {try.#Success [..no_exceptions _.empty]}))

(implementation: relative_monoid
  (Monoid Relative)

  (def: identity ..relative_identity)

  (def: (composite left right)
    (cond (same? ..relative_identity left)
          right

          (same? ..relative_identity right)
          left

          ... else
          (function (_ resolver)
            (do try.monad
              [[left_exceptions left_instruction] (left resolver)
               [right_exceptions right_instruction] (right resolver)]
              (in [(# sequence.monoid composite left_exceptions right_exceptions)
                   (_#composite left_instruction right_instruction)]))))))

(type: .public (Bytecode a)
  (+State Try [Pool Environment Tracker] (Writer Relative a)))

(def: .public new_label
  (Bytecode Label)
  (function (_ [pool environment tracker])
    {try.#Success [[pool
                    environment
                    (revised@ #next ++ tracker)]
                   [..relative_identity
                    (value@ #next tracker)]]}))

(exception: .public (label_has_already_been_set [label Label])
  (exception.report
   ["Label" (%.nat label)]))

(exception: .public (mismatched_environments [instruction Symbol
                                              label Label
                                              address Address
                                              expected Stack
                                              actual Stack])
  (exception.report
   ["Instruction" (%.symbol instruction)]
   ["Label" (%.nat label)]
   ["Address" (/address.format address)]
   ["Expected" (/stack.format expected)]
   ["Actual" (/stack.format actual)]))

(def: .public (set? label)
  (-> Label (Bytecode (Maybe [Stack Address])))
  (function (_ state)
    (let [[pool environment tracker] state]
      {try.#Success [state
                     [..relative_identity
                      (case (dictionary.value label (value@ #known tracker))
                        {.#Some [expected {.#Some address}]}
                        {.#Some [expected address]}
                        
                        _
                        {.#None})]]})))

(def: .public (acknowledged? label)
  (-> Label (Bytecode (Maybe Stack)))
  (function (_ state)
    (let [[pool environment tracker] state]
      {try.#Success [state
                     [..relative_identity
                      (case (dictionary.value label (value@ #known tracker))
                        {.#Some [expected {.#None}]}
                        {.#Some expected}

                        _
                        {.#None})]]})))

(def: .public stack
  (Bytecode (Maybe Stack))
  (function (_ state)
    (let [[pool environment tracker] state]
      {try.#Success [state
                     [..relative_identity
                      (value@ /environment.#stack environment)]]})))

(with_expansions [<success> (as_is (in [[pool
                                         environment
                                         (revised@ #known
                                                   (dictionary.has label [actual {.#Some @here}])
                                                   tracker)]
                                        [..relative_identity
                                         []]]))]
  (def: .public (set_label label)
    (-> Label (Bytecode Any))
    (function (_ [pool environment tracker])
      (let [@here (value@ #program_counter tracker)]
        (case (dictionary.value label (value@ #known tracker))
          {.#Some [expected {.#Some address}]}
          (exception.except ..label_has_already_been_set [label])
          
          {.#Some [expected {.#None}]}
          (do try.monad
            [[actual environment] (/environment.continue expected environment)]
            <success>)

          {.#None}
          (do try.monad
            [[actual environment] (/environment.continue (|> environment
                                                             (value@ /environment.#stack)
                                                             (maybe.else /stack.empty))
                                                         environment)]
            <success>))))))

(def: .public monad
  (Monad Bytecode)
  (<| (:as (Monad Bytecode))
      (writer.with ..relative_monoid)
      (: (Monad (+State Try [Pool Environment Tracker])))
      state.with
      (: (Monad Try))
      try.monad))

(def: .public (when_continuous it)
  (-> (Bytecode Any) (Bytecode Any))
  (do ..monad
    [stack ..stack]
    (.case stack
      {.#None} (in [])
      {.#Some _} it)))

(def: .public failure
  (-> Text Bytecode)
  (|>> {try.#Failure} function.constant))

(def: .public (except exception value)
  (All (_ e) (-> (exception.Exception e) e Bytecode))
  (..failure (exception.error exception value)))

(def: .public (resolve environment bytecode)
  (All (_ a) (-> Environment (Bytecode a) (Resource [Environment (Sequence Exception) Instruction a])))
  (function (_ pool)
    (do try.monad
      [[[pool environment tracker] [relative output]] (bytecode [pool environment ..fresh])
       [exceptions instruction] (relative (value@ #known tracker))]
      (in [pool [environment exceptions instruction output]]))))

(def: (step estimator counter)
  (-> Estimator Address (Try Address))
  (/address.move (estimator counter) counter))

(def: (bytecode consumption production registry [estimator bytecode] input)
  (All (_ a) (-> U2 U2 Registry [Estimator (-> [a] Instruction)] a (Bytecode Any)))
  (function (_ [pool environment tracker])
    (do [! try.monad]
      [environment' (|> environment
                        (/environment.consumes consumption)
                        (monad.then ! (/environment.produces production))
                        (monad.then ! (/environment.has registry)))
       program_counter' (step estimator (value@ #program_counter tracker))]
      (in [[pool
            environment'
            (with@ #program_counter program_counter' tracker)]
           [(function.constant (in [..no_exceptions (bytecode input)]))
            []]]))))

(template [<name> <frames>]
  [(def: <name> U2
     (|> <frames> //unsigned.u2 try.trusted))]

  [$0 0]
  [$1 1]
  [$2 2]
  [$3 3]
  [$4 4]
  [$5 5]
  [$6 6]
  )

(template [<name> <registry>]
  [(def: <name> Registry (|> <registry> //unsigned.u2 try.trusted /registry.registry))]

  [@_ 0]
  [@0 1]
  [@1 2]
  [@2 3]
  [@3 4]
  [@4 5]
  )

(template [<name> <consumption> <production> <registry> <instruction>]
  [(def: .public <name>
     (Bytecode Any)
     (..bytecode <consumption>
                 <production>
                 <registry>
                 <instruction>
                 []))]

  [nop $0 $0 @_ _.nop]
  
  [aconst_null $0 $1 @_ _.aconst_null]

  [iconst_m1 $0 $1 @_ _.iconst_m1]
  [iconst_0 $0 $1 @_ _.iconst_0]
  [iconst_1 $0 $1 @_ _.iconst_1]
  [iconst_2 $0 $1 @_ _.iconst_2]
  [iconst_3 $0 $1 @_ _.iconst_3]
  [iconst_4 $0 $1 @_ _.iconst_4]
  [iconst_5 $0 $1 @_ _.iconst_5]

  [lconst_0 $0 $2 @_ _.lconst_0]
  [lconst_1 $0 $2 @_ _.lconst_1]

  [fconst_0 $0 $1 @_ _.fconst_0]
  [fconst_1 $0 $1 @_ _.fconst_1]
  [fconst_2 $0 $1 @_ _.fconst_2]
  
  [dconst_0 $0 $2 @_ _.dconst_0]
  [dconst_1 $0 $2 @_ _.dconst_1]

  [pop $1 $0 @_ _.pop]
  [pop2 $2 $0 @_ _.pop2]
  
  [dup $1 $2 @_ _.dup]
  [dup_x1 $2 $3 @_ _.dup_x1]
  [dup_x2 $3 $4 @_ _.dup_x2]
  [dup2 $2 $4 @_ _.dup2]
  [dup2_x1 $3 $5 @_ _.dup2_x1]
  [dup2_x2 $4 $6 @_ _.dup2_x2]
  
  [swap $2 $2 @_ _.swap]

  [iaload $2 $1 @_ _.iaload]
  [laload $2 $2 @_ _.laload]
  [faload $2 $1 @_ _.faload]
  [daload $2 $2 @_ _.daload]
  [aaload $2 $1 @_ _.aaload]
  [baload $2 $1 @_ _.baload]
  [caload $2 $1 @_ _.caload]
  [saload $2 $1 @_ _.saload]

  [iload_0 $0 $1 @0 _.iload_0]
  [iload_1 $0 $1 @1 _.iload_1]
  [iload_2 $0 $1 @2 _.iload_2]
  [iload_3 $0 $1 @3 _.iload_3]

  [lload_0 $0 $2 @1 _.lload_0]
  [lload_1 $0 $2 @2 _.lload_1]
  [lload_2 $0 $2 @3 _.lload_2]
  [lload_3 $0 $2 @4 _.lload_3]
  
  [fload_0 $0 $1 @0 _.fload_0]
  [fload_1 $0 $1 @1 _.fload_1]
  [fload_2 $0 $1 @2 _.fload_2]
  [fload_3 $0 $1 @3 _.fload_3]
  
  [dload_0 $0 $2 @1 _.dload_0]
  [dload_1 $0 $2 @2 _.dload_1]
  [dload_2 $0 $2 @3 _.dload_2]
  [dload_3 $0 $2 @4 _.dload_3]
  
  [aload_0 $0 $1 @0 _.aload_0]
  [aload_1 $0 $1 @1 _.aload_1]
  [aload_2 $0 $1 @2 _.aload_2]
  [aload_3 $0 $1 @3 _.aload_3]

  [iastore $3 $0 @_ _.iastore]
  [lastore $4 $0 @_ _.lastore]
  [fastore $3 $0 @_ _.fastore]
  [dastore $4 $0 @_ _.dastore]
  [aastore $3 $0 @_ _.aastore]
  [bastore $3 $0 @_ _.bastore]
  [castore $3 $0 @_ _.castore]
  [sastore $3 $0 @_ _.sastore]

  [istore_0 $1 $0 @0 _.istore_0]
  [istore_1 $1 $0 @1 _.istore_1]
  [istore_2 $1 $0 @2 _.istore_2]
  [istore_3 $1 $0 @3 _.istore_3]

  [lstore_0 $2 $0 @1 _.lstore_0]
  [lstore_1 $2 $0 @2 _.lstore_1]
  [lstore_2 $2 $0 @3 _.lstore_2]
  [lstore_3 $2 $0 @4 _.lstore_3]

  [fstore_0 $1 $0 @0 _.fstore_0]
  [fstore_1 $1 $0 @1 _.fstore_1]
  [fstore_2 $1 $0 @2 _.fstore_2]
  [fstore_3 $1 $0 @3 _.fstore_3]

  [dstore_0 $2 $0 @1 _.dstore_0]
  [dstore_1 $2 $0 @2 _.dstore_1]
  [dstore_2 $2 $0 @3 _.dstore_2]
  [dstore_3 $2 $0 @4 _.dstore_3]
  
  [astore_0 $1 $0 @0 _.astore_0]
  [astore_1 $1 $0 @1 _.astore_1]
  [astore_2 $1 $0 @2 _.astore_2]
  [astore_3 $1 $0 @3 _.astore_3]

  [iadd $2 $1 @_ _.iadd]
  [isub $2 $1 @_ _.isub]
  [imul $2 $1 @_ _.imul]
  [idiv $2 $1 @_ _.idiv]
  [irem $2 $1 @_ _.irem]
  [ineg $1 $1 @_ _.ineg]
  [iand $2 $1 @_ _.iand]
  [ior $2 $1 @_ _.ior]
  [ixor $2 $1 @_ _.ixor]
  [ishl $2 $1 @_ _.ishl]
  [ishr $2 $1 @_ _.ishr]
  [iushr $2 $1 @_ _.iushr]

  [ladd $4 $2 @_ _.ladd]
  [lsub $4 $2 @_ _.lsub]
  [lmul $4 $2 @_ _.lmul]
  [ldiv $4 $2 @_ _.ldiv]
  [lrem $4 $2 @_ _.lrem]
  [lneg $2 $2 @_ _.lneg]
  [land $4 $2 @_ _.land]
  [lor $4 $2 @_ _.lor]
  [lxor $4 $2 @_ _.lxor]
  [lshl $3 $2 @_ _.lshl]
  [lshr $3 $2 @_ _.lshr]
  [lushr $3 $2 @_ _.lushr]
  
  [fadd $2 $1 @_ _.fadd]
  [fsub $2 $1 @_ _.fsub]
  [fmul $2 $1 @_ _.fmul]
  [fdiv $2 $1 @_ _.fdiv]
  [frem $2 $1 @_ _.frem]
  [fneg $1 $1 @_ _.fneg]
  
  [dadd $4 $2 @_ _.dadd]
  [dsub $4 $2 @_ _.dsub]
  [dmul $4 $2 @_ _.dmul]
  [ddiv $4 $2 @_ _.ddiv]
  [drem $4 $2 @_ _.drem]
  [dneg $2 $2 @_ _.dneg]

  [l2i $2 $1 @_ _.l2i]
  [l2f $2 $1 @_ _.l2f]
  [l2d $2 $2 @_ _.l2d]
  
  [f2i $1 $1 @_ _.f2i]
  [f2l $1 $2 @_ _.f2l]
  [f2d $1 $2 @_ _.f2d]
  
  [d2i $2 $1 @_ _.d2i]
  [d2l $2 $2 @_ _.d2l]
  [d2f $2 $1 @_ _.d2f]

  [i2l $1 $2 @_ _.i2l]
  [i2f $1 $1 @_ _.i2f]
  [i2d $1 $2 @_ _.i2d]
  [i2b $1 $1 @_ _.i2b]
  [i2c $1 $1 @_ _.i2c]
  [i2s $1 $1 @_ _.i2s]

  [lcmp $4 $1 @_ _.lcmp]
  
  [fcmpl $2 $1 @_ _.fcmpl]
  [fcmpg $2 $1 @_ _.fcmpg]

  [dcmpl $4 $1 @_ _.dcmpl]
  [dcmpg $4 $1 @_ _.dcmpg]

  [arraylength $1 $1 @_ _.arraylength]
  
  [monitorenter $1 $0 @_ _.monitorenter]
  [monitorexit $1 $0 @_ _.monitorexit]
  )

(def: discontinuity!
  (Bytecode Any)
  (function (_ [pool environment tracker])
    (do try.monad
      [_ (/environment.stack environment)]
      (in [[pool
            (/environment.discontinue environment)
            tracker]
           [..relative_identity
            []]]))))

(template [<name> <consumption> <instruction>]
  [(def: .public <name>
     (Bytecode Any)
     (do ..monad
       [_ (..bytecode <consumption> $0 @_ <instruction> [])]
       ..discontinuity!))]

  [ireturn $1 _.ireturn]
  [lreturn $2 _.lreturn]
  [freturn $1 _.freturn]
  [dreturn $2 _.dreturn]
  [areturn $1 _.areturn]
  [return $0 _.return]

  [athrow $1 _.athrow]
  )

(def: .public (bipush byte)
  (-> S1 (Bytecode Any))
  (..bytecode $0 $1 @_ _.bipush [byte]))

(def: (lifted resource)
  (All (_ a)
    (-> (Resource a)
        (Bytecode a)))
  (function (_ [pool environment tracker])
    (do try.monad
      [[pool' output] (resource pool)]
      (in [[pool' environment tracker]
           [..relative_identity
            output]]))))

(def: .public (string value)
  (-> //constant.UTF8 (Bytecode Any))
  (do ..monad
    [index (..lifted (//constant/pool.string value))]
    (case (|> index //index.value //unsigned.value //unsigned.u1)
      {try.#Success index}
      (..bytecode $0 $1 @_ _.ldc [index])

      {try.#Failure _}
      (..bytecode $0 $1 @_ _.ldc_w/string [index]))))

(import: java/lang/Float
  ["[1]::[0]"
   ("static" floatToRawIntBits "manual" [float] int)])

(import: java/lang/Double
  ["[1]::[0]"
   ("static" doubleToRawLongBits "manual" [double] long)])

(template [<name> <type> <constructor> <constant> <wide> <to_lux> <specializations>]
  [(def: .public (<name> value)
     (-> <type> (Bytecode Any))
     (case (|> value <to_lux>)
       (^template [<special> <instruction>]
         [<special> (..bytecode $0 $1 @_ <instruction> [])])
       <specializations>
       
       _ (do ..monad
           [index (..lifted (<constant> (<constructor> value)))]
           (case (|> index //index.value //unsigned.value //unsigned.u1)
             {try.#Success index}
             (..bytecode $0 $1 @_ _.ldc [index])

             {try.#Failure _}
             (..bytecode $0 $1 @_ <wide> [index])))))]

  [int I32 //constant.integer //constant/pool.integer _.ldc_w/integer
   (<| .int i32.i64)
   ([-1 _.iconst_m1]
    [+0 _.iconst_0]
    [+1 _.iconst_1]
    [+2 _.iconst_2]
    [+3 _.iconst_3]
    [+4 _.iconst_4]
    [+5 _.iconst_5])]
  )

(def: (arbitrary_float value)
  (-> java/lang/Float (Bytecode Any))
  (do ..monad
    [index (..lifted (//constant/pool.float (//constant.float value)))]
    (case (|> index //index.value //unsigned.value //unsigned.u1)
      {try.#Success index}
      (..bytecode $0 $1 @_ _.ldc [index])

      {try.#Failure _}
      (..bytecode $0 $1 @_ _.ldc_w/float [index]))))

(def: float_bits
  (-> java/lang/Float Int)
  (|>> java/lang/Float::floatToRawIntBits
       ffi.int_to_long
       (:as Int)))

(def: negative_zero_float_bits
  (|> -0.0 (:as java/lang/Double) ffi.double_to_float ..float_bits))

(def: .public (float value)
  (-> java/lang/Float (Bytecode Any))
  (if (i.= ..negative_zero_float_bits
           (..float_bits value))
    (..arbitrary_float value)
    (case (|> value ffi.float_to_double (:as Frac))
      (^template [<special> <instruction>]
        [<special> (..bytecode $0 $1 @_ <instruction> [])])
      ([+0.0 _.fconst_0]
       [+1.0 _.fconst_1]
       [+2.0 _.fconst_2])
      
      _ (..arbitrary_float value))))

(template [<name> <type> <constructor> <constant> <wide> <to_lux> <specializations>]
  [(def: .public (<name> value)
     (-> <type> (Bytecode Any))
     (case (|> value <to_lux>)
       (^template [<special> <instruction>]
         [<special> (..bytecode $0 $2 @_ <instruction> [])])
       <specializations>
       
       _ (do ..monad
           [index (..lifted (<constant> (<constructor> value)))]
           (..bytecode $0 $2 @_ <wide> [index]))))]

  [long Int //constant.long //constant/pool.long _.ldc2_w/long
   (<|)
   ([+0 _.lconst_0]
    [+1 _.lconst_1])]
  )

(def: (arbitrary_double value)
  (-> java/lang/Double (Bytecode Any))
  (do ..monad
    [index (..lifted (//constant/pool.double (//constant.double (:as Frac value))))]
    (..bytecode $0 $2 @_ _.ldc2_w/double [index])))

(def: double_bits
  (-> java/lang/Double Int)
  (|>> java/lang/Double::doubleToRawLongBits
       (:as Int)))

(def: negative_zero_double_bits
  (..double_bits (:as java/lang/Double -0.0)))

(def: .public (double value)
  (-> java/lang/Double (Bytecode Any))
  (if (i.= ..negative_zero_double_bits
           (..double_bits value))
    (..arbitrary_double value)
    (case (:as Frac value)
      (^template [<special> <instruction>]
        [<special> (..bytecode $0 $2 @_ <instruction> [])])
      ([+0.0 _.dconst_0]
       [+1.0 _.dconst_1])
      
      _ (..arbitrary_double value))))

(exception: .public (invalid_register [id Nat])
  (exception.report
   ["ID" (%.nat id)]))

(def: (register id)
  (-> Nat (Bytecode Register))
  (case (//unsigned.u1 id)
    {try.#Success register}
    (# ..monad in register)
    
    {try.#Failure error}
    (..except ..invalid_register [id])))

(template [<for> <size> <name> <general> <specials>]
  [(def: .public (<name> local)
     (-> Nat (Bytecode Any))
     (with_expansions [<specials>' (template.spliced <specials>)]
       (`` (case local
             (~~ (template [<case> <instruction> <registry>]
                   [<case> (..bytecode $0 <size> <registry> <instruction> [])]
                   
                   <specials>'))
             _ (do ..monad
                 [local (..register local)]
                 (..bytecode $0 <size> (<for> local) <general> [local]))))))]
  
  [/registry.for $1 iload _.iload
   [[0 _.iload_0 @0]
    [1 _.iload_1 @1]
    [2 _.iload_2 @2]
    [3 _.iload_3 @3]]]
  [/registry.for_wide $2 lload _.lload
   [[0 _.lload_0 @1]
    [1 _.lload_1 @2]
    [2 _.lload_2 @3]
    [3 _.lload_3 @4]]]
  [/registry.for $1 fload _.fload
   [[0 _.fload_0 @0]
    [1 _.fload_1 @1]
    [2 _.fload_2 @2]
    [3 _.fload_3 @3]]]
  [/registry.for_wide $2 dload _.dload
   [[0 _.dload_0 @1]
    [1 _.dload_1 @2]
    [2 _.dload_2 @3]
    [3 _.dload_3 @4]]]
  [/registry.for $1 aload _.aload
   [[0 _.aload_0 @0]
    [1 _.aload_1 @1]
    [2 _.aload_2 @2]
    [3 _.aload_3 @3]]]
  )

(template [<for> <size> <name> <general> <specials>]
  [(def: .public (<name> local)
     (-> Nat (Bytecode Any))
     (with_expansions [<specials>' (template.spliced <specials>)]
       (`` (case local
             (~~ (template [<case> <instruction> <registry>]
                   [<case> (..bytecode <size> $0 <registry> <instruction> [])]
                   
                   <specials>'))
             _ (do ..monad
                 [local (..register local)]
                 (..bytecode <size> $0 (<for> local) <general> [local]))))))]
  
  [/registry.for $1 istore _.istore
   [[0 _.istore_0 @0]
    [1 _.istore_1 @1]
    [2 _.istore_2 @2]
    [3 _.istore_3 @3]]]
  [/registry.for_wide $2 lstore _.lstore
   [[0 _.lstore_0 @1]
    [1 _.lstore_1 @2]
    [2 _.lstore_2 @3]
    [3 _.lstore_3 @4]]]
  [/registry.for $1 fstore _.fstore
   [[0 _.fstore_0 @0]
    [1 _.fstore_1 @1]
    [2 _.fstore_2 @2]
    [3 _.fstore_3 @3]]]
  [/registry.for_wide $2 dstore _.dstore
   [[0 _.dstore_0 @1]
    [1 _.dstore_1 @2]
    [2 _.dstore_2 @3]
    [3 _.dstore_3 @4]]]
  [/registry.for $1 astore _.astore
   [[0 _.astore_0 @0]
    [1 _.astore_1 @1]
    [2 _.astore_2 @2]
    [3 _.astore_3 @3]]]
  )

(template [<consumption> <production> <name> <instruction> <input>]
  [(def: .public <name>
     (-> <input> (Bytecode Any))
     (..bytecode <consumption> <production> @_ <instruction>))]
  
  [$1 $1 newarray _.newarray Primitive_Array_Type]
  [$0 $1 sipush _.sipush S2]
  )

(exception: .public (unknown_label [label Label])
  (exception.report
   ["Label" (%.nat label)]))

(exception: .public (cannot_do_a_big_jump [label Label
                                           @from Address
                                           jump Big_Jump])
  (exception.report
   ["Label" (%.nat label)]
   ["Start" (|> @from /address.value //unsigned.value %.nat)]
   ["Target" (|> jump //signed.value %.int)]))

(type: Any_Jump
  (Either Big_Jump
          Jump))

(def: (jump @from @to)
  (-> Address Address (Try Any_Jump))
  (do [! try.monad]
    [jump (# ! each //signed.value
             (/address.jump @from @to))]
    (let [big? (n.> (//unsigned.value //unsigned.maximum/2)
                    (.nat (i.* (if (i.< +0 jump)
                                 -1
                                 +1)
                               jump)))]
      (if big?
        (# ! each (|>> {.#Left}) (//signed.s4 jump))
        (# ! each (|>> {.#Right}) (//signed.s2 jump))))))

(exception: .public (unset_label [label Label])
  (exception.report
   ["Label" (%.nat label)]))

(def: (resolve_label label resolver)
  (-> Label Resolver (Try [Stack Address]))
  (case (dictionary.value label resolver)
    {.#Some [actual {.#Some address}]}
    {try.#Success [actual address]}

    {.#Some [actual {.#None}]}
    (exception.except ..unset_label [label])
    
    {.#None}
    (exception.except ..unknown_label [label])))

(def: (acknowledge_label stack label tracker)
  (-> Stack Label Tracker Tracker)
  (case (dictionary.value label (value@ #known tracker))
    {.#Some _}
    tracker

    {.#None}
    (revised@ #known (dictionary.has label [stack {.#None}]) tracker)))

(template [<consumption> <name> <instruction>]
  [(def: .public (<name> label)
     (-> Label (Bytecode Any))
     (let [[estimator bytecode] <instruction>]
       (function (_ [pool environment tracker])
         (let [@here (value@ #program_counter tracker)]
           (do try.monad
             [environment' (|> environment
                               (/environment.consumes <consumption>))
              actual (/environment.stack environment')
              program_counter' (step estimator @here)]
             (in (let [@from @here]
                   [[pool
                     environment'
                     (|> tracker
                         (..acknowledge_label actual label)
                         (with@ #program_counter program_counter'))]
                    [(function (_ resolver)
                       (do try.monad
                         [[expected @to] (..resolve_label label resolver)
                          _ (exception.assertion ..mismatched_environments [(symbol <instruction>) label @here expected actual]
                                                 (# /stack.equivalence = expected actual))
                          jump (..jump @from @to)]
                         (case jump
                           {.#Left jump}
                           (exception.except ..cannot_do_a_big_jump [label @from jump])

                           {.#Right jump}
                           (in [..no_exceptions (bytecode jump)]))))
                     []]])))))))]

  [$1 ifeq _.ifeq]
  [$1 ifne _.ifne]
  [$1 iflt _.iflt]
  [$1 ifge _.ifge]
  [$1 ifgt _.ifgt]
  [$1 ifle _.ifle]
  
  [$1 ifnull _.ifnull]
  [$1 ifnonnull _.ifnonnull]

  [$2 if_icmpeq _.if_icmpeq]
  [$2 if_icmpne _.if_icmpne]
  [$2 if_icmplt _.if_icmplt]
  [$2 if_icmpge _.if_icmpge]
  [$2 if_icmpgt _.if_icmpgt]
  [$2 if_icmple _.if_icmple]
  
  [$2 if_acmpeq _.if_acmpeq]
  [$2 if_acmpne _.if_acmpne]
  )

(template [<name> <instruction> <on_long_jump> <on_short_jump>]
  [(def: .public (<name> label)
     (-> Label (Bytecode Any))
     (let [[estimator bytecode] <instruction>]
       (function (_ [pool environment tracker])
         (do try.monad
           [actual (/environment.stack environment)
            .let [@here (value@ #program_counter tracker)]
            program_counter' (step estimator @here)]
           (in (let [@from @here]
                 [[pool
                   (/environment.discontinue environment)
                   (|> tracker
                       (..acknowledge_label actual label)
                       (with@ #program_counter program_counter'))]
                  [(function (_ resolver)
                     (case (dictionary.value label resolver)
                       {.#Some [expected {.#Some @to}]}
                       (do try.monad
                         [_ (exception.assertion ..mismatched_environments [(symbol <instruction>) label @here expected actual]
                                                 (# /stack.equivalence = expected actual))
                          jump (..jump @from @to)]
                         (case jump
                           {.#Left jump}
                           <on_long_jump>

                           {.#Right jump}
                           <on_short_jump>))

                       {.#Some [expected {.#None}]}
                       (exception.except ..unset_label [label])

                       {.#None}
                       (exception.except ..unknown_label [label])))
                   []]]))))))]

  [goto _.goto
   (exception.except ..cannot_do_a_big_jump [label @from jump])
   (in [..no_exceptions (bytecode jump)])]
  [goto_w _.goto_w
   (in [..no_exceptions (bytecode jump)])
   (in [..no_exceptions (bytecode (/jump.lifted jump))])]
  )

(def: (big_jump jump)
  (-> Any_Jump Big_Jump)
  (case jump
    {.#Left big}
    big

    {.#Right small}
    (/jump.lifted small)))

(exception: .public invalid_tableswitch)

(def: .public (tableswitch minimum default [at_minimum afterwards])
  (-> S4 Label [Label (List Label)] (Bytecode Any))
  (let [[estimator bytecode] _.tableswitch]
    (function (_ [pool environment tracker])
      (do try.monad
        [environment' (|> environment
                          (/environment.consumes $1))
         actual (/environment.stack environment')
         program_counter' (step (estimator (list.size afterwards)) (value@ #program_counter tracker))]
        (in (let [@from (value@ #program_counter tracker)]
              [[pool
                environment'
                (|> (list#mix (..acknowledge_label actual) tracker (list& default at_minimum afterwards))
                    (with@ #program_counter program_counter'))]
               [(function (_ resolver)
                  (let [get (: (-> Label (Maybe [Stack (Maybe Address)]))
                               (function (_ label)
                                 (dictionary.value label resolver)))]
                    (case (do [! maybe.monad]
                            [@default (|> default get (monad.then ! product.right))
                             @at_minimum (|> at_minimum get (monad.then ! product.right))
                             @afterwards (|> afterwards
                                             (monad.each ! get)
                                             (monad.then ! (monad.each ! product.right)))]
                            (in [@default @at_minimum @afterwards]))
                      {.#Some [@default @at_minimum @afterwards]}
                      (do [! try.monad]
                        [>default (# ! each ..big_jump (..jump @from @default))
                         >at_minimum (# ! each ..big_jump (..jump @from @at_minimum))
                         >afterwards (monad.each ! (|>> (..jump @from) (# ! each ..big_jump))
                                                 @afterwards)]
                        (in [..no_exceptions (bytecode minimum >default [>at_minimum >afterwards])]))

                      {.#None}
                      (exception.except ..invalid_tableswitch []))))
                []]]))))))

(exception: .public invalid_lookupswitch)

(def: .public (lookupswitch default cases)
  (-> Label (List [S4 Label]) (Bytecode Any))
  (let [cases (list.sorted (function (_ [left _] [right _])
                             (i.< (//signed.value left)
                                  (//signed.value right)))
                           cases)
        [estimator bytecode] _.lookupswitch]
    (function (_ [pool environment tracker])
      (do try.monad
        [environment' (|> environment
                          (/environment.consumes $1))
         actual (/environment.stack environment')
         program_counter' (step (estimator (list.size cases)) (value@ #program_counter tracker))]
        (in (let [@from (value@ #program_counter tracker)]
              [[pool
                environment'
                (|> (list#mix (..acknowledge_label actual) tracker (list& default (list#each product.right cases)))
                    (with@ #program_counter program_counter'))]
               [(function (_ resolver)
                  (let [get (: (-> Label (Maybe [Stack (Maybe Address)]))
                               (function (_ label)
                                 (dictionary.value label resolver)))]
                    (case (do [! maybe.monad]
                            [@default (|> default get (monad.then ! product.right))
                             @cases (|> cases
                                        (monad.each ! (|>> product.right get))
                                        (monad.then ! (monad.each ! product.right)))]
                            (in [@default @cases]))
                      {.#Some [@default @cases]}
                      (do [! try.monad]
                        [>default (# ! each ..big_jump (..jump @from @default))
                         >cases (|> @cases
                                    (monad.each ! (|>> (..jump @from) (# ! each ..big_jump)))
                                    (# ! each (|>> (list.zipped/2 (list#each product.left cases)))))]
                        (in [..no_exceptions (bytecode >default >cases)]))

                      {.#None}
                      (exception.except ..invalid_lookupswitch []))))
                []]]))))))

(def: reflection
  (All (_ category)
    (-> (Type (<| Return' Value' category)) Text))
  (|>> type.reflection reflection.reflection))

(template [<consumption> <production> <name> <category> <instruction>]
  [(def: .public (<name> class)
     (-> (Type <category>) (Bytecode Any))
     (do ..monad
       [... TODO: Make sure it's impossible to have indexes greater than U2.
        index (..lifted (//constant/pool.class (//name.internal (..reflection class))))]
       (..bytecode <consumption> <production> @_ <instruction> [index])))]

  [$0 $1 new Class _.new]
  [$1 $1 anewarray Object _.anewarray]
  [$1 $1 checkcast Object _.checkcast]
  [$1 $1 instanceof Object _.instanceof]
  )

(def: .public (iinc register increase)
  (-> Nat U1 (Bytecode Any))
  (do ..monad
    [register (..register register)]
    (..bytecode $0 $0 (/registry.for register) _.iinc [register increase])))

(exception: .public (multiarray_cannot_be_zero_dimensional [class (Type Object)])
  (exception.report ["Class" (..reflection class)]))

(def: .public (multianewarray class dimensions)
  (-> (Type Object) U1 (Bytecode Any))
  (do ..monad
    [_ (: (Bytecode Any)
          (case (|> dimensions //unsigned.value)
            0 (..except ..multiarray_cannot_be_zero_dimensional [class])
            _ (in [])))
     index (..lifted (//constant/pool.class (//name.internal (..reflection class))))]
    (..bytecode (//unsigned.lifted/2 dimensions) $1 @_ _.multianewarray [index dimensions])))

(def: (type_size type)
  (-> (Type Return) Nat)
  (cond (same? type.void type)
        0

        (or (same? type.long type)
            (same? type.double type))
        2

        ... else
        1))

(template [<static?> <name> <instruction> <method>]
  [(def: .public (<name> class method type)
     (-> (Type Class) Text (Type Method) (Bytecode Any))
     (let [[type_variables inputs output exceptions] (parser.method type)]
       (do ..monad
         [index (<| ..lifted
                    (<method> (..reflection class))
                    [//constant/pool.#name method
                     //constant/pool.#descriptor (type.descriptor type)])
          .let [consumption (|> inputs
                                (list#each ..type_size)
                                (list#mix n.+ (if <static?> 0 1))
                                //unsigned.u1
                                try.trusted)
                production (|> output ..type_size //unsigned.u1 try.trusted)]]
         (..bytecode (//unsigned.lifted/2 consumption)
                     (//unsigned.lifted/2 production)
                     @_
                     <instruction> [index consumption production]))))]

  [#1 invokestatic _.invokestatic //constant/pool.method]
  [#0 invokevirtual _.invokevirtual //constant/pool.method]
  [#0 invokespecial _.invokespecial //constant/pool.method]
  [#0 invokeinterface _.invokeinterface //constant/pool.interface_method]
  )

(template [<consumption> <name> <1> <2>]
  [(def: .public (<name> class field type)
     (-> (Type Class) Text (Type Value) (Bytecode Any))
     (do ..monad
       [index (<| ..lifted
                  (//constant/pool.field (..reflection class))
                  [//constant/pool.#name field
                   //constant/pool.#descriptor (type.descriptor type)])]
       (if (or (same? type.long type)
               (same? type.double type))
         (..bytecode <consumption> $2 @_ <2> [index])
         (..bytecode <consumption> $1 @_ <1> [index]))))]

  [$0 getstatic _.getstatic/1 _.getstatic/2]
  [$1 putstatic _.putstatic/1 _.putstatic/2]
  [$1 getfield  _.getfield/1  _.getfield/2]
  [$2 putfield  _.putfield/1  _.putfield/2]
  )

(exception: .public (invalid_range_for_try [start Address
                                            end Address])
  (exception.report
   ["Start" (|> start /address.value //unsigned.value %.nat)]
   ["End" (|> end /address.value //unsigned.value %.nat)]))

(def: .public (try @start @end @handler catch)
  (-> Label Label Label (Type Class) (Bytecode Any))
  (do ..monad
    [@catch (..lifted (//constant/pool.class (//name.internal (..reflection catch))))]
    (function (_ [pool environment tracker])
      {try.#Success
       [[pool
         environment
         (..acknowledge_label /stack.catch @handler tracker)]
        [(function (_ resolver)
           (do try.monad
             [[_ @start] (..resolve_label @start resolver)
              [_ @end] (..resolve_label @end resolver)
              _ (if (/address.after? @start @end)
                  (in [])
                  (exception.except ..invalid_range_for_try [@start @end]))
              [_ @handler] (..resolve_label @handler resolver)]
             (in [(sequence.sequence
                   [//exception.#start @start
                    //exception.#end @end
                    //exception.#handler @handler
                    //exception.#catch @catch])
                  _.empty])))
         []]]})))

(def: .public (composite pre post)
  (All (_ pre post)
    (-> (Bytecode pre) (Bytecode post) (Bytecode post)))
  (do ..monad
    [_ pre]
    post))