path: root/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux

(.module:
  [lux #- char]
  (lux (control [monad #+ do]
                ["p" parser]
                ["ex" exception #+ exception:])
       (concurrency ["A" atom])
       (data ["e" error]
             [maybe]
             [product]
             [bool "bool/" Eq<Bool>]
             [text "text/" Eq<Text>]
             (text format
                   ["l" lexer])
             (coll [list "list/" Fold<List> Functor<List> Monoid<List>]
                   [array]
                   [dict #+ Dict]))
       [macro "macro/" Monad<Meta>]
       (macro [code]
              ["s" syntax])
       (lang [type]
             (type ["tc" check]))
       [host])
  (luxc ["&" lang]
        (lang ["&." host]
              ["la" analysis]
              (analysis ["&." common]
                        [".A" inference])))
  ["@" //common]
  )

(exception: #export Wrong-Syntax)
(def: (wrong-syntax procedure args)
  (-> Text (List Code) Text)
  (format "Procedure: " procedure "\n"
          "Arguments: " (%code (code.tuple args))))

(exception: #export JVM-Type-Is-Not-Class)

(exception: #export Non-Interface)
(exception: #export Non-Object)
(exception: #export Non-Array)
(exception: #export Non-Throwable)
(exception: #export Non-JVM-Type)

(exception: #export Unknown-Class)
(exception: #export Primitives-Cannot-Have-Type-Parameters)
(exception: #export Primitives-Are-Not-Objects)
(exception: #export Invalid-Type-For-Array-Element)

(exception: #export Unknown-Field)
(exception: #export Mistaken-Field-Owner)
(exception: #export Not-Virtual-Field)
(exception: #export Not-Static-Field)
(exception: #export Cannot-Set-Final-Field)

(exception: #export No-Candidates)
(exception: #export Too-Many-Candidates)

(exception: #export Cannot-Cast)
(def: (cannot-cast to from)
  (-> Type Type Text)
  (format "From: " (%type from) "\n"
          "  To: " (%type to)))

(exception: #export Cannot-Possibly-Be-Instance)

(exception: #export Cannot-Convert-To-Class)
(exception: #export Cannot-Convert-To-Parameter)
(exception: #export Cannot-Convert-To-Lux-Type)
(exception: #export Unknown-Type-Var)
(exception: #export Type-Parameter-Mismatch)
(exception: #export Cannot-Correspond-Type-With-Class)

(def: #export null-class Text "#Null")

(do-template [<name> <class>]
  [(def: #export <name> Type (#.Primitive <class> (list)))]

  ## Boxes
  [Boolean   "java.lang.Boolean"]
  [Byte      "java.lang.Byte"]
  [Short     "java.lang.Short"]
  [Integer   "java.lang.Integer"]
  [Long      "java.lang.Long"]
  [Float     "java.lang.Float"]
  [Double    "java.lang.Double"]
  [Character "java.lang.Character"]
  [String    "java.lang.String"]

  ## Primitives
  [boolean   "boolean"]
  [byte      "byte"]
  [short     "short"]
  [int       "int"]
  [long      "long"]
  [float     "float"]
  [double    "double"]
  [char      "char"]
  )

(def: conversion-procs
  @.Bundle
  (<| (@.prefix "convert")
      (|> (dict.new text.Hash<Text>)
          (@.install "double-to-float" (@.unary Double Float))
          (@.install "double-to-int" (@.unary Double Integer))
          (@.install "double-to-long" (@.unary Double Long))
          (@.install "float-to-double" (@.unary Float Double))
          (@.install "float-to-int" (@.unary Float Integer))
          (@.install "float-to-long" (@.unary Float Long))
          (@.install "int-to-byte" (@.unary Integer Byte))
          (@.install "int-to-char" (@.unary Integer Character))
          (@.install "int-to-double" (@.unary Integer Double))
          (@.install "int-to-float" (@.unary Integer Float))
          (@.install "int-to-long" (@.unary Integer Long))
          (@.install "int-to-short" (@.unary Integer Short))
          (@.install "long-to-double" (@.unary Long Double))
          (@.install "long-to-float" (@.unary Long Float))
          (@.install "long-to-int" (@.unary Long Integer))
          (@.install "long-to-short" (@.unary Long Short))
          (@.install "long-to-byte" (@.unary Long Byte))
          (@.install "char-to-byte" (@.unary Character Byte))
          (@.install "char-to-short" (@.unary Character Short))
          (@.install "char-to-int" (@.unary Character Integer))
          (@.install "char-to-long" (@.unary Character Long))
          (@.install "byte-to-long" (@.unary Byte Long))
          (@.install "short-to-long" (@.unary Short Long))
          )))

(do-template [<name> <prefix> <type>]
  [(def: <name>
     @.Bundle
     (<| (@.prefix <prefix>)
         (|> (dict.new text.Hash<Text>)
             (@.install "+" (@.binary <type> <type> <type>))
             (@.install "-" (@.binary <type> <type> <type>))
             (@.install "*" (@.binary <type> <type> <type>))
             (@.install "/" (@.binary <type> <type> <type>))
             (@.install "%" (@.binary <type> <type> <type>))
             (@.install "=" (@.binary <type> <type> Boolean))
             (@.install "<" (@.binary <type> <type> Boolean))
             (@.install "and" (@.binary <type> <type> <type>))
             (@.install "or" (@.binary <type> <type> <type>))
             (@.install "xor" (@.binary <type> <type> <type>))
             (@.install "shl" (@.binary <type> Integer <type>))
             (@.install "shr" (@.binary <type> Integer <type>))
             (@.install "ushr" (@.binary <type> Integer <type>))
             )))]

  [int-procs  "int"  Integer]
  [long-procs "long" Long]
  )

(do-template [<name> <prefix> <type>]
  [(def: <name>
     @.Bundle
     (<| (@.prefix <prefix>)
         (|> (dict.new text.Hash<Text>)
             (@.install "+" (@.binary <type> <type> <type>))
             (@.install "-" (@.binary <type> <type> <type>))
             (@.install "*" (@.binary <type> <type> <type>))
             (@.install "/" (@.binary <type> <type> <type>))
             (@.install "%" (@.binary <type> <type> <type>))
             (@.install "=" (@.binary <type> <type> Boolean))
             (@.install "<" (@.binary <type> <type> Boolean))
             )))]

  [float-procs  "float"  Float]
  [double-procs "double" Double]
  )

(def: char-procs
  @.Bundle
  (<| (@.prefix "char")
      (|> (dict.new text.Hash<Text>)
          (@.install "=" (@.binary Character Character Boolean))
          (@.install "<" (@.binary Character Character Boolean))
          )))

(def: #export boxes
  (Dict Text Text)
  (|> (list ["boolean" "java.lang.Boolean"]
            ["byte" "java.lang.Byte"]
            ["short" "java.lang.Short"]
            ["int" "java.lang.Integer"]
            ["long" "java.lang.Long"]
            ["float" "java.lang.Float"]
            ["double" "java.lang.Double"]
            ["char" "java.lang.Character"])
      (dict.from-list text.Hash<Text>)))

(def: (array-length proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list arrayC))
      (do macro.Monad<Meta>
        [_ (&.infer Nat)
         [var-id varT] (&.with-type-env tc.var)
         arrayA (&.with-type (type (Array varT))
                  (analyse arrayC))]
        (wrap (la.procedure proc (list arrayA))))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +1 (list.size args))))))

(def: (array-new proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list lengthC))
      (do macro.Monad<Meta>
        [lengthA (&.with-type Nat
                   (analyse lengthC))
         expectedT macro.expected-type
         [level elem-class] (: (Meta [Nat Text])
                               (loop [analysisT expectedT
                                      level +0]
                                 (case analysisT
                                   (#.Apply inputT funcT)
                                   (case (type.apply (list inputT) funcT)
                                     (#.Some outputT)
                                     (recur outputT level)

                                     #.None
                                     (&.throw Non-Array (%type expectedT)))

                                   (^ (#.Primitive "#Array" (list elemT)))
                                   (recur elemT (n/inc level))

                                   (#.Primitive class _)
                                   (wrap [level class])
                                   
                                   _
                                   (&.throw Non-Array (%type expectedT)))))
         _ (if (n/> +0 level)
             (wrap [])
             (&.throw Non-Array (%type expectedT)))]
        (wrap (la.procedure proc (list (code.nat (n/dec level)) (code.text elem-class) lengthA))))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +1 (list.size args))))))

(def: (check-jvm objectT)
  (-> Type (Meta Text))
  (case objectT
    (#.Primitive name _)
    (macro/wrap name)

    (#.Named name unnamed)
    (check-jvm unnamed)

    (#.Var id)
    (macro/wrap "java.lang.Object")

    (^template [<tag>]
      (<tag> env unquantified)
      (check-jvm unquantified))
    ([#.UnivQ]
     [#.ExQ])

    (#.Apply inputT funcT)
    (case (type.apply (list inputT) funcT)
      (#.Some outputT)
      (check-jvm outputT)

      #.None
      (&.throw Non-Object (%type objectT)))

    _
    (&.throw Non-Object (%type objectT))))

(def: (check-object objectT)
  (-> Type (Meta Text))
  (do macro.Monad<Meta>
    [name (check-jvm objectT)]
    (if (dict.contains? name boxes)
      (&.throw Primitives-Are-Not-Objects name)
      (macro/wrap name))))

(def: (box-array-element-type elemT)
  (-> Type (Meta [Type Text]))
  (case elemT
    (#.Primitive name #.Nil)
    (let [boxed-name (|> (dict.get name boxes)
                         (maybe.default name))]
      (macro/wrap [(#.Primitive boxed-name #.Nil)
                   boxed-name]))

    (#.Primitive name _)
    (if (dict.contains? name boxes)
      (&.throw Primitives-Cannot-Have-Type-Parameters name)
      (macro/wrap [elemT name]))

    _
    (&.throw Invalid-Type-For-Array-Element (%type elemT))))

(def: (array-read proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list arrayC idxC))
      (do macro.Monad<Meta>
        [[var-id varT] (&.with-type-env tc.var)
         _ (&.infer varT)
         arrayA (&.with-type (type (Array varT))
                  (analyse arrayC))
         ?elemT (&.with-type-env
                  (tc.read var-id))
         [elemT elem-class] (box-array-element-type (maybe.default varT ?elemT))
         idxA (&.with-type Nat
                (analyse idxC))]
        (wrap (la.procedure proc (list (code.text elem-class) idxA arrayA))))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +2 (list.size args))))))

(def: (array-write proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list arrayC idxC valueC))
      (do macro.Monad<Meta>
        [[var-id varT] (&.with-type-env tc.var)
         _ (&.infer (type (Array varT)))
         arrayA (&.with-type (type (Array varT))
                  (analyse arrayC))
         ?elemT (&.with-type-env
                  (tc.read var-id))
         [valueT elem-class] (box-array-element-type (maybe.default varT ?elemT))
         idxA (&.with-type Nat
                (analyse idxC))
         valueA (&.with-type valueT
                  (analyse valueC))]
        (wrap (la.procedure proc (list (code.text elem-class) idxA valueA arrayA))))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +3 (list.size args))))))

(def: array-procs
  @.Bundle
  (<| (@.prefix "array")
      (|> (dict.new text.Hash<Text>)
          (@.install "length" array-length)
          (@.install "new" array-new)
          (@.install "read" array-read)
          (@.install "write" array-write)
          )))

(def: (object-null proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list))
      (do macro.Monad<Meta>
        [expectedT macro.expected-type
         _ (check-object expectedT)]
        (wrap (la.procedure proc (list))))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +0 (list.size args))))))

(def: (object-null? proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list objectC))
      (do macro.Monad<Meta>
        [_ (&.infer Bool)
         [objectT objectA] (&common.with-unknown-type
                             (analyse objectC))
         _ (check-object objectT)]
        (wrap (la.procedure proc (list objectA))))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +1 (list.size args))))))

(def: (object-synchronized proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list monitorC exprC))
      (do macro.Monad<Meta>
        [[monitorT monitorA] (&common.with-unknown-type
                               (analyse monitorC))
         _ (check-object monitorT)
         exprA (analyse exprC)]
        (wrap (la.procedure proc (list monitorA exprA))))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +2 (list.size args))))))

(host.import java/lang/Object
  (equals [Object] boolean))

(host.import java/lang/ClassLoader)

(host.import #long java/lang/reflect/Type
  (getTypeName [] String))

(host.import java/lang/reflect/GenericArrayType
  (getGenericComponentType [] java/lang/reflect/Type))

(host.import java/lang/reflect/ParameterizedType
  (getRawType [] java/lang/reflect/Type)
  (getActualTypeArguments [] (Array java/lang/reflect/Type)))

(host.import (java/lang/reflect/TypeVariable d)
  (getName [] String)
  (getBounds [] (Array java/lang/reflect/Type)))

(host.import (java/lang/reflect/WildcardType d)
  (getLowerBounds [] (Array java/lang/reflect/Type))
  (getUpperBounds [] (Array java/lang/reflect/Type)))

(host.import java/lang/reflect/Modifier
  (#static isStatic [int] boolean)
  (#static isFinal [int] boolean)
  (#static isInterface [int] boolean)
  (#static isAbstract [int] boolean))

(host.import java/lang/reflect/Field
  (getDeclaringClass [] (java/lang/Class Object))
  (getModifiers [] int)
  (getGenericType [] java/lang/reflect/Type))

(host.import java/lang/reflect/Method
  (getName [] String)
  (getModifiers [] int)
  (getDeclaringClass [] (Class Object))
  (getTypeParameters [] (Array (TypeVariable Method)))
  (getGenericParameterTypes [] (Array java/lang/reflect/Type))
  (getGenericReturnType [] java/lang/reflect/Type)
  (getGenericExceptionTypes [] (Array java/lang/reflect/Type)))

(host.import (java/lang/reflect/Constructor c)
  (getModifiers [] int)
  (getDeclaringClass [] (Class c))
  (getTypeParameters [] (Array (TypeVariable (Constructor c))))
  (getGenericParameterTypes [] (Array java/lang/reflect/Type))
  (getGenericExceptionTypes [] (Array java/lang/reflect/Type)))

(host.import (java/lang/Class c)
  (getName [] String)
  (getModifiers [] int)
  (#static forName [String boolean ClassLoader] #try (Class Object))
  (isAssignableFrom [(Class Object)] boolean)
  (getTypeParameters [] (Array (TypeVariable (Class c))))
  (getGenericInterfaces [] (Array java/lang/reflect/Type))
  (getGenericSuperclass [] java/lang/reflect/Type)
  (getDeclaredField [String] #try Field)
  (getConstructors [] (Array (Constructor Object)))
  (getDeclaredMethods [] (Array Method)))

(def: (load-class name)
  (-> Text (Meta (Class Object)))
  (do macro.Monad<Meta>
    [class-loader &host.class-loader]
    (case (Class::forName [name false class-loader])
      (#e.Success [class])
      (wrap class)

      (#e.Error error)
      (&.throw Unknown-Class name))))

(def: (sub-class? super sub)
  (-> Text Text (Meta Bool))
  (do macro.Monad<Meta>
    [super (load-class super)
     sub (load-class sub)]
    (wrap (Class::isAssignableFrom [sub] super))))

(def: (object-throw proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list exceptionC))
      (do macro.Monad<Meta>
        [_ (&.infer Bottom)
         [exceptionT exceptionA] (&common.with-unknown-type
                                   (analyse exceptionC))
         exception-class (check-object exceptionT)
         ? (sub-class? "java.lang.Throwable" exception-class)
         _ (: (Meta Unit)
              (if ?
                (wrap [])
                (&.throw Non-Throwable exception-class)))]
        (wrap (la.procedure proc (list exceptionA))))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +1 (list.size args))))))

(def: (object-class proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list classC))
      (case classC
        [_ (#.Text class)]
        (do macro.Monad<Meta>
          [_ (&.infer (#.Primitive "java.lang.Class" (list (#.Primitive class (list)))))
           _ (load-class class)]
          (wrap (la.procedure proc (list (code.text class)))))

        _
        (&.throw Wrong-Syntax (wrong-syntax proc args)))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +1 (list.size args))))))

(def: (object-instance? proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list classC objectC))
      (case classC
        [_ (#.Text class)]
        (do macro.Monad<Meta>
          [_ (&.infer Bool)
           [objectT objectA] (&common.with-unknown-type
                               (analyse objectC))
           object-class (check-object objectT)
           ? (sub-class? class object-class)]
          (if ?
            (wrap (la.procedure proc (list (code.text class))))
            (&.throw Cannot-Possibly-Be-Instance (format object-class " !<= "  class))))

        _
        (&.throw Wrong-Syntax (wrong-syntax proc args)))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +2 (list.size args))))))

(def: object-procs
  @.Bundle
  (<| (@.prefix "object")
      (|> (dict.new text.Hash<Text>)
          (@.install "null" object-null)
          (@.install "null?" object-null?)
          (@.install "synchronized" object-synchronized)
          (@.install "throw" object-throw)
          (@.install "class" object-class)
          (@.install "instance?" object-instance?)
          )))

(def: type-descriptor
  (-> java/lang/reflect/Type Text)
  (java/lang/reflect/Type::getTypeName []))

(def: (java-type-to-class type)
  (-> java/lang/reflect/Type (Meta Text))
  (cond (host.instance? Class type)
        (macro/wrap (Class::getName [] (:! Class type)))

        (host.instance? ParameterizedType type)
        (java-type-to-class (ParameterizedType::getRawType [] (:! ParameterizedType type)))

        ## else
        (&.throw Cannot-Convert-To-Class (type-descriptor type))))

(type: Mappings
  (Dict Text Type))

(def: fresh-mappings Mappings (dict.new text.Hash<Text>))

(def: (java-type-to-lux-type mappings java-type)
  (-> Mappings java/lang/reflect/Type (Meta Type))
  (cond (host.instance? TypeVariable java-type)
        (let [var-name (TypeVariable::getName [] (:! TypeVariable java-type))]
          (case (dict.get var-name mappings)
            (#.Some var-type)
            (macro/wrap var-type)
            
            #.None
            (&.throw Unknown-Type-Var var-name)))

        (host.instance? WildcardType java-type)
        (let [java-type (:! WildcardType java-type)]
          (case [(array.read +0 (WildcardType::getUpperBounds [] java-type))
                 (array.read +0 (WildcardType::getLowerBounds [] java-type))]
            (^or [(#.Some bound) _] [_ (#.Some bound)])
            (java-type-to-lux-type mappings bound)
            
            _
            (macro/wrap Top)))

        (host.instance? Class java-type)
        (let [java-type (:! (Class Object) java-type)
              class-name (Class::getName [] java-type)]
          (macro/wrap (case (array.size (Class::getTypeParameters [] java-type))
                        +0
                        (#.Primitive class-name (list))
                        
                        arity
                        (|> (list.n/range +0 (n/dec arity))
                            list.reverse
                            (list/map (|>> (n/* +2) n/inc #.Bound))
                            (#.Primitive class-name)
                            (type.univ-q arity)))))

        (host.instance? ParameterizedType java-type)
        (let [java-type (:! ParameterizedType java-type)
              raw (ParameterizedType::getRawType [] java-type)]
          (if (host.instance? Class raw)
            (do macro.Monad<Meta>
              [paramsT (|> java-type
                           (ParameterizedType::getActualTypeArguments [])
                           array.to-list
                           (monad.map @ (java-type-to-lux-type mappings)))]
              (macro/wrap (#.Primitive (Class::getName [] (:! (Class Object) raw))
                                       paramsT)))
            (&.throw JVM-Type-Is-Not-Class (type-descriptor raw))))

        (host.instance? GenericArrayType java-type)
        (do macro.Monad<Meta>
          [innerT (|> (:! GenericArrayType java-type)
                      (GenericArrayType::getGenericComponentType [])
                      (java-type-to-lux-type mappings))]
          (wrap (#.Primitive "#Array" (list innerT))))

        ## else
        (&.throw Cannot-Convert-To-Lux-Type (type-descriptor java-type))))

(type: Direction
  #In
  #Out)

(def: (choose direction to from)
  (-> Direction Text Text Text)
  (case direction
    #In to
    #Out from))

(def: (correspond-type-params class type)
  (-> (Class Object) Type (Meta Mappings))
  (case type
    (#.Primitive name params)
    (let [class-name (Class::getName [] class)
          class-params (array.to-list (Class::getTypeParameters [] class))
          num-class-params (list.size class-params)
          num-type-params (list.size params)]
      (cond (not (text/= class-name name))
            (&.throw Cannot-Correspond-Type-With-Class
                     (format "Class = " class-name "\n"
                             "Type = " (%type type)))

            (not (n/= num-class-params num-type-params))
            (&.throw Type-Parameter-Mismatch
                     (format "Expected: " (%i (nat-to-int num-class-params)) "\n"
                             "  Actual: " (%i (nat-to-int num-type-params)) "\n"
                             "   Class: " class-name "\n"
                             "    Type: " (%type type)))

            ## else
            (macro/wrap (|> params
                            (list.zip2 (list/map (TypeVariable::getName []) class-params))
                            (dict.from-list text.Hash<Text>)))
            ))

    _
    (&.throw Non-JVM-Type (%type type))))

(def: (cast direction to from)
  (-> Direction Type Type (Meta [Text Type]))
  (do macro.Monad<Meta>
    [to-name (check-jvm to)
     from-name (check-jvm from)]
    (cond (dict.contains? to-name boxes)
          (let [box (maybe.assume (dict.get to-name boxes))]
            (if (text/= box from-name)
              (wrap [(choose direction to-name from-name) (#.Primitive to-name (list))])
              (&.throw Cannot-Cast (cannot-cast to from))))

          (dict.contains? from-name boxes)
          (let [box (maybe.assume (dict.get from-name boxes))]
            (do @
              [[_ castT] (cast direction to (#.Primitive box (list)))]
              (wrap [(choose direction to-name from-name) castT])))

          (text/= to-name from-name)
          (wrap [(choose direction to-name from-name) from])

          (text/= null-class from-name)
          (wrap [(choose direction to-name from-name) to])

          ## else
          (do @
            [to-class (load-class to-name)
             from-class (load-class from-name)
             _ (&.assert Cannot-Cast (cannot-cast to from)
                         (Class::isAssignableFrom [from-class] to-class))
             candiate-parents (monad.map @
                                         (function [java-type]
                                           (do @
                                             [class-name (java-type-to-class java-type)
                                              class (load-class class-name)]
                                             (wrap [java-type (Class::isAssignableFrom [class] to-class)])))
                                         (list& (Class::getGenericSuperclass [] from-class)
                                                (array.to-list (Class::getGenericInterfaces [] from-class))))]
            (case (|> candiate-parents
                      (list.filter product.right)
                      (list/map product.left))
              (#.Cons parent _)
              (do @
                [mapping (correspond-type-params from-class from)
                 parentT (java-type-to-lux-type mapping parent)
                 [_ castT] (cast direction to parentT)]
                (wrap [(choose direction to-name from-name) castT]))

              #.Nil
              (&.throw Cannot-Cast (cannot-cast to from)))))))

(def: (infer-out outputT)
  (-> Type (Meta [Text Type]))
  (do macro.Monad<Meta>
    [expectedT macro.expected-type
     [unboxed castT] (cast #Out expectedT outputT)
     _ (&.with-type-env
         (tc.check expectedT castT))]
    (wrap [unboxed castT])))

(def: (find-field class-name field-name)
  (-> Text Text (Meta [(Class Object) Field]))
  (do macro.Monad<Meta>
    [class (load-class class-name)]
    (case (Class::getDeclaredField [field-name] class)
      (#e.Success field)
      (let [owner (Field::getDeclaringClass [] field)]
        (if (is owner class)
          (wrap [class field])
          (&.throw Mistaken-Field-Owner
                   (format "       Field: " field-name "\n"
                           " Owner Class: " (Class::getName [] owner) "\n"
                           "Target Class: " class-name "\n"))))

      (#e.Error _)
      (&.throw Unknown-Field (format class-name "#" field-name)))))

(def: (static-field class-name field-name)
  (-> Text Text (Meta [Type Bool]))
  (do macro.Monad<Meta>
    [[class fieldJ] (find-field class-name field-name)
     #let [modifiers (Field::getModifiers [] fieldJ)]]
    (if (Modifier::isStatic [modifiers])
      (let [fieldJT (Field::getGenericType [] fieldJ)]
        (do @
          [fieldT (java-type-to-lux-type fresh-mappings fieldJT)]
          (wrap [fieldT (Modifier::isFinal [modifiers])])))
      (&.throw Not-Static-Field (format class-name "#" field-name)))))

(def: (virtual-field class-name field-name objectT)
  (-> Text Text Type (Meta [Type Bool]))
  (do macro.Monad<Meta>
    [[class fieldJ] (find-field class-name field-name)
     #let [modifiers (Field::getModifiers [] fieldJ)]]
    (if (not (Modifier::isStatic [modifiers]))
      (do @
        [#let [fieldJT (Field::getGenericType [] fieldJ)
               var-names (|> class
                             (Class::getTypeParameters [])
                             array.to-list
                             (list/map (TypeVariable::getName [])))]
         mappings (: (Meta Mappings)
                     (case objectT
                       (#.Primitive _class-name _class-params)
                       (do @
                         [#let [num-params (list.size _class-params)
                                num-vars (list.size var-names)]
                          _ (&.assert Type-Parameter-Mismatch
                                      (format "Expected: " (%i (nat-to-int num-params)) "\n"
                                              "  Actual: " (%i (nat-to-int num-vars)) "\n"
                                              "   Class: " _class-name "\n"
                                              "    Type: " (%type objectT))
                                      (n/= num-params num-vars))]
                         (wrap (|> (list.zip2 var-names _class-params)
                                   (dict.from-list text.Hash<Text>))))

                       _
                       (&.throw Non-Object (%type objectT))))
         fieldT (java-type-to-lux-type mappings fieldJT)]
        (wrap [fieldT (Modifier::isFinal [modifiers])]))
      (&.throw Not-Virtual-Field (format class-name "#" field-name)))))

(def: (analyse-object class analyse sourceC)
  (-> Text &.Analyser Code (Meta [Type la.Analysis]))
  (do macro.Monad<Meta>
    [target-class (load-class class)
     targetT (java-type-to-lux-type fresh-mappings
                                    (:! java/lang/reflect/Type
                                        target-class))
     [sourceT sourceA] (&common.with-unknown-type
                         (analyse sourceC))
     [unboxed castT] (cast #Out targetT sourceT)
     _ (&.assert Cannot-Cast (cannot-cast targetT sourceT)
                 (not (dict.contains? unboxed boxes)))]
    (wrap [castT sourceA])))

(def: (analyse-input analyse targetT sourceC)
  (-> &.Analyser Type Code (Meta [Type Text la.Analysis]))
  (do macro.Monad<Meta>
    [[sourceT sourceA] (&common.with-unknown-type
                         (analyse sourceC))
     [unboxed castT] (cast #In targetT sourceT)]
    (wrap [castT unboxed sourceA])))

(def: (static-get proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list classC fieldC))
      (case [classC fieldC]
        [[_ (#.Text class)] [_ (#.Text field)]]
        (do macro.Monad<Meta>
          [[fieldT final?] (static-field class field)
           [unboxed castT] (infer-out fieldT)]
          (wrap (la.procedure proc (list (code.text class) (code.text field)
                                         (code.text unboxed)))))

        _
        (&.throw Wrong-Syntax (wrong-syntax proc args)))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +2 (list.size args))))))

(def: (static-put proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list classC fieldC valueC))
      (case [classC fieldC]
        [[_ (#.Text class)] [_ (#.Text field)]]
        (do macro.Monad<Meta>
          [_ (&.infer Unit)
           [fieldT final?] (static-field class field)
           _ (&.assert Cannot-Set-Final-Field (format class "#" field)
                       (not final?))
           [valueT unboxed valueA] (analyse-input analyse fieldT valueC)
           _ (&.with-type-env
               (tc.check fieldT valueT))]
          (wrap (la.procedure proc (list (code.text class) (code.text field)
                                         (code.text unboxed) valueA))))

        _
        (&.throw Wrong-Syntax (wrong-syntax proc args)))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +3 (list.size args))))))

(def: (virtual-get proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list classC fieldC objectC))
      (case [classC fieldC]
        [[_ (#.Text class)] [_ (#.Text field)]]
        (do macro.Monad<Meta>
          [[objectT objectA] (analyse-object class analyse objectC)
           [fieldT final?] (virtual-field class field objectT)
           [unboxed castT] (infer-out fieldT)]
          (wrap (la.procedure proc (list (code.text class) (code.text field)
                                         (code.text unboxed) objectA))))

        _
        (&.throw Wrong-Syntax (wrong-syntax proc args)))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +3 (list.size args))))))

(def: (virtual-put proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case args
      (^ (list classC fieldC valueC objectC))
      (case [classC fieldC]
        [[_ (#.Text class)] [_ (#.Text field)]]
        (do macro.Monad<Meta>
          [[objectT objectA] (analyse-object class analyse objectC)
           _ (&.infer objectT)
           [fieldT final?] (virtual-field class field objectT)
           _ (&.assert Cannot-Set-Final-Field (format class "#" field)
                       (not final?))
           [valueT unboxed valueA] (analyse-input analyse fieldT valueC)]
          (wrap (la.procedure proc (list (code.text class) (code.text field) (code.text unboxed) valueA objectA))))

        _
        (&.throw Wrong-Syntax (wrong-syntax proc args)))

      _
      (&.throw @.Incorrect-Procedure-Arity (@.wrong-arity proc +4 (list.size args))))))

(def: (java-type-to-parameter type)
  (-> java/lang/reflect/Type (Meta Text))
  (cond (host.instance? Class type)
        (macro/wrap (Class::getName [] (:! Class type)))

        (host.instance? ParameterizedType type)
        (java-type-to-parameter (ParameterizedType::getRawType [] (:! ParameterizedType type)))

        (or (host.instance? TypeVariable type)
            (host.instance? WildcardType type))
        (macro/wrap "java.lang.Object")

        (host.instance? GenericArrayType type)
        (do macro.Monad<Meta>
          [componentP (java-type-to-parameter (GenericArrayType::getGenericComponentType [] (:! GenericArrayType type)))]
          (wrap (format componentP "[]")))

        ## else
        (&.throw Cannot-Convert-To-Parameter (type-descriptor type))))

(type: Method-Type
  #Static
  #Abstract
  #Virtual
  #Special
  #Interface)

(def: (check-method class method-name method-type arg-classes method)
  (-> (Class Object) Text Method-Type (List Text) Method (Meta Bool))
  (do macro.Monad<Meta>
    [parameters (|> (Method::getGenericParameterTypes [] method)
                    array.to-list
                    (monad.map @ java-type-to-parameter))
     #let [modifiers (Method::getModifiers [] method)]]
    (wrap (and (Object::equals [class] (Method::getDeclaringClass [] method))
               (text/= method-name (Method::getName [] method))
               (case #Static
                 #Special
                 (Modifier::isStatic [modifiers])

                 _
                 true)
               (case method-type
                 #Special
                 (not (or (Modifier::isInterface [(Class::getModifiers [] class)])
                          (Modifier::isAbstract [modifiers])))

                 _
                 true)
               (n/= (list.size arg-classes) (list.size parameters))
               (list/fold (function [[expectedJC actualJC] prev]
                            (and prev
                                 (text/= expectedJC actualJC)))
                          true
                          (list.zip2 arg-classes parameters))))))

(def: (check-constructor class arg-classes constructor)
  (-> (Class Object) (List Text) (Constructor Object) (Meta Bool))
  (do macro.Monad<Meta>
    [parameters (|> (Constructor::getGenericParameterTypes [] constructor)
                    array.to-list
                    (monad.map @ java-type-to-parameter))]
    (wrap (and (Object::equals [class] (Constructor::getDeclaringClass [] constructor))
               (n/= (list.size arg-classes) (list.size parameters))
               (list/fold (function [[expectedJC actualJC] prev]
                            (and prev
                                 (text/= expectedJC actualJC)))
                          true
                          (list.zip2 arg-classes parameters))))))

(def: idx-to-bound
  (-> Nat Type)
  (|>> (n/* +2) n/inc #.Bound))

(def: (type-vars amount offset)
  (-> Nat Nat (List Type))
  (if (n/= +0 amount)
    (list)
    (|> (list.n/range offset (|> amount n/dec (n/+ offset)))
        (list/map idx-to-bound))))

(def: (method-to-type method-type method)
  (-> Method-Type Method (Meta [Type (List Type)]))
  (let [owner (Method::getDeclaringClass [] method)
        owner-name (Class::getName [] owner)
        owner-tvars (case method-type
                      #Static
                      (list)

                      _
                      (|> (Class::getTypeParameters [] owner)
                          array.to-list
                          (list/map (TypeVariable::getName []))))
        method-tvars (|> (Method::getTypeParameters [] method)
                         array.to-list
                         (list/map (TypeVariable::getName [])))
        num-owner-tvars (list.size owner-tvars)
        num-method-tvars (list.size method-tvars)
        all-tvars (list/compose owner-tvars method-tvars)
        num-all-tvars (list.size all-tvars)
        owner-tvarsT (type-vars num-owner-tvars +0)
        method-tvarsT (type-vars num-method-tvars num-owner-tvars)
        mappings (: Mappings
                    (if (list.empty? all-tvars)
                      fresh-mappings
                      (|> (list/compose owner-tvarsT method-tvarsT)
                          list.reverse
                          (list.zip2 all-tvars)
                          (dict.from-list text.Hash<Text>))))]
    (do macro.Monad<Meta>
      [inputsT (|> (Method::getGenericParameterTypes [] method)
                   array.to-list
                   (monad.map @ (java-type-to-lux-type mappings)))
       outputT (java-type-to-lux-type mappings (Method::getGenericReturnType [] method))
       exceptionsT (|> (Method::getGenericExceptionTypes [] method)
                       array.to-list
                       (monad.map @ (java-type-to-lux-type mappings)))
       #let [methodT (<| (type.univ-q num-all-tvars)
                         (type.function (case method-type
                                          #Static
                                          inputsT

                                          _
                                          (list& (#.Primitive owner-name (list.reverse owner-tvarsT))
                                                 inputsT)))
                         outputT)]]
      (wrap [methodT exceptionsT]))))

(def: (methods class-name method-name method-type arg-classes)
  (-> Text Text Method-Type (List Text) (Meta [Type (List Type)]))
  (do macro.Monad<Meta>
    [class (load-class class-name)
     candidates (|> class
                    (Class::getDeclaredMethods [])
                    array.to-list
                    (monad.map @ (function [method]
                                   (do @
                                     [passes? (check-method class method-name method-type arg-classes method)]
                                     (wrap [passes? method])))))]
    (case (list.filter product.left candidates)
      #.Nil
      (&.throw No-Candidates (format class-name "#" method-name))
      
      (#.Cons candidate #.Nil)
      (|> candidate product.right (method-to-type method-type))

      _
      (&.throw Too-Many-Candidates (format class-name "#" method-name)))))

(def: (constructor-to-type constructor)
  (-> (Constructor Object) (Meta [Type (List Type)]))
  (let [owner (Constructor::getDeclaringClass [] constructor)
        owner-name (Class::getName [] owner)
        owner-tvars (|> (Class::getTypeParameters [] owner)
                        array.to-list
                        (list/map (TypeVariable::getName [])))
        constructor-tvars (|> (Constructor::getTypeParameters [] constructor)
                              array.to-list
                              (list/map (TypeVariable::getName [])))
        num-owner-tvars (list.size owner-tvars)
        all-tvars (list/compose owner-tvars constructor-tvars)
        num-all-tvars (list.size all-tvars)
        owner-tvarsT (type-vars num-owner-tvars +0)
        constructor-tvarsT (type-vars num-all-tvars num-owner-tvars)
        mappings (: Mappings
                    (if (list.empty? all-tvars)
                      fresh-mappings
                      (|> (list/compose owner-tvarsT constructor-tvarsT)
                          list.reverse
                          (list.zip2 all-tvars)
                          (dict.from-list text.Hash<Text>))))]
    (do macro.Monad<Meta>
      [inputsT (|> (Constructor::getGenericParameterTypes [] constructor)
                   array.to-list
                   (monad.map @ (java-type-to-lux-type mappings)))
       exceptionsT (|> (Constructor::getGenericExceptionTypes [] constructor)
                       array.to-list
                       (monad.map @ (java-type-to-lux-type mappings)))
       #let [objectT (#.Primitive owner-name (list.reverse owner-tvarsT))
             constructorT (<| (type.univ-q num-all-tvars)
                              (type.function inputsT)
                              objectT)]]
      (wrap [constructorT exceptionsT]))))

(def: (constructor-methods class-name arg-classes)
  (-> Text (List Text) (Meta [Type (List Type)]))
  (do macro.Monad<Meta>
    [class (load-class class-name)
     candidates (|> class
                    (Class::getConstructors [])
                    array.to-list
                    (monad.map @ (function [constructor]
                                   (do @
                                     [passes? (check-constructor class arg-classes constructor)]
                                     (wrap [passes? constructor])))))]
    (case (list.filter product.left candidates)
      #.Nil
      (&.throw No-Candidates (format class-name "(" (text.join-with ", " arg-classes) ")"))
      
      (#.Cons candidate #.Nil)
      (|> candidate product.right constructor-to-type)

      _
      (&.throw Too-Many-Candidates class-name))))

(def: (decorate-inputs typesT inputsA)
  (-> (List Text) (List la.Analysis) (List la.Analysis))
  (|> inputsA
      (list.zip2 (list/map code.text typesT))
      (list/map (function [[type value]]
                  (la.product (list type value))))))

(def: (sub-type-analyser analyse)
  (-> &.Analyser &.Analyser)
  (function [argC]
    (do macro.Monad<Meta>
      [[argT argA] (&common.with-unknown-type
                     (analyse argC))
       expectedT macro.expected-type
       [unboxed castT] (cast #In expectedT argT)]
      (wrap argA))))

(def: (invoke//static proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case (: (e.Error [Text Text (List [Text Code])])
             (s.run args ($_ p.seq s.text s.text (p.some (s.tuple (p.seq s.text s.any))))))
      (#e.Success [class method argsTC])
      (do macro.Monad<Meta>
        [#let [argsT (list/map product.left argsTC)]
         [methodT exceptionsT] (methods class method #Static argsT)
         [outputT argsA] (inferenceA.general (sub-type-analyser analyse) methodT (list/map product.right argsTC))
         [unboxed castT] (infer-out outputT)]
        (wrap (la.procedure proc (list& (code.text class) (code.text method)
                                        (code.text unboxed) (decorate-inputs argsT argsA)))))

      _
      (&.throw Wrong-Syntax (wrong-syntax proc args)))))

(def: (invoke//virtual proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case (: (e.Error [Text Text Code (List [Text Code])])
             (s.run args ($_ p.seq s.text s.text s.any (p.some (s.tuple (p.seq s.text s.any))))))
      (#e.Success [class method objectC argsTC])
      (do macro.Monad<Meta>
        [#let [argsT (list/map product.left argsTC)]
         [methodT exceptionsT] (methods class method #Virtual argsT)
         [outputT allA] (inferenceA.general (sub-type-analyser analyse) methodT (list& objectC (list/map product.right argsTC)))
         #let [[objectA argsA] (case allA
                                 (#.Cons objectA argsA)
                                 [objectA argsA]

                                 _
                                 (undefined))]
         [unboxed castT] (infer-out outputT)]
        (wrap (la.procedure proc (list& (code.text class) (code.text method)
                                        (code.text unboxed) objectA (decorate-inputs argsT argsA)))))

      _
      (&.throw Wrong-Syntax (wrong-syntax proc args)))))

(def: (invoke//special proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case (: (e.Error [(List Code) [Text Text Code (List [Text Code]) Unit]])
             (p.run args ($_ p.seq s.text s.text s.any (p.some (s.tuple (p.seq s.text s.any))) s.end!)))
      (#e.Success [_ [class method objectC argsTC _]])
      (do macro.Monad<Meta>
        [#let [argsT (list/map product.left argsTC)]
         [methodT exceptionsT] (methods class method #Special argsT)
         [outputT argsA] (inferenceA.general (sub-type-analyser analyse) methodT (list& objectC (list/map product.right argsTC)))
         [unboxed castT] (infer-out outputT)]
        (wrap (la.procedure proc (list& (code.text class) (code.text method)
                                        (code.text unboxed) (decorate-inputs argsT argsA)))))

      _
      (&.throw Wrong-Syntax (wrong-syntax proc args)))))

(def: (invoke//interface proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case (: (e.Error [Text Text Code (List [Text Code])])
             (s.run args ($_ p.seq s.text s.text s.any (p.some (s.tuple (p.seq s.text s.any))))))
      (#e.Success [class-name method objectC argsTC])
      (do macro.Monad<Meta>
        [#let [argsT (list/map product.left argsTC)]
         class (load-class class-name)
         _ (&.assert Non-Interface class-name
                     (Modifier::isInterface [(Class::getModifiers [] class)]))
         [methodT exceptionsT] (methods class-name method #Interface argsT)
         [outputT argsA] (inferenceA.general (sub-type-analyser analyse) methodT (list& objectC (list/map product.right argsTC)))
         [unboxed castT] (infer-out outputT)]
        (wrap (la.procedure proc
                            (list& (code.text class-name) (code.text method) (code.text unboxed)
                                   (decorate-inputs argsT argsA)))))

      _
      (&.throw Wrong-Syntax (wrong-syntax proc args)))))

(def: (invoke//constructor proc)
  (-> Text @.Proc)
  (function [analyse eval args]
    (case (: (e.Error [Text (List [Text Code])])
             (s.run args ($_ p.seq s.text (p.some (s.tuple (p.seq s.text s.any))))))
      (#e.Success [class argsTC])
      (do macro.Monad<Meta>
        [#let [argsT (list/map product.left argsTC)]
         [methodT exceptionsT] (constructor-methods class argsT)
         [outputT argsA] (inferenceA.general (sub-type-analyser analyse) methodT (list/map product.right argsTC))
         [unboxed castT] (infer-out outputT)]
        (wrap (la.procedure proc (list& (code.text class) (decorate-inputs argsT argsA)))))

      _
      (&.throw Wrong-Syntax (wrong-syntax proc args)))))

(def: member-procs
  @.Bundle
  (<| (@.prefix "member")
      (|> (dict.new text.Hash<Text>)
          (dict.merge (<| (@.prefix "static")
                          (|> (dict.new text.Hash<Text>)
                              (@.install "get" static-get)
                              (@.install "put" static-put))))
          (dict.merge (<| (@.prefix "virtual")
                          (|> (dict.new text.Hash<Text>)
                              (@.install "get" virtual-get)
                              (@.install "put" virtual-put))))
          (dict.merge (<| (@.prefix "invoke")
                          (|> (dict.new text.Hash<Text>)
                              (@.install "static" invoke//static)
                              (@.install "virtual" invoke//virtual)
                              (@.install "special" invoke//special)
                              (@.install "interface" invoke//interface)
                              (@.install "constructor" invoke//constructor)
                              )))
          )))

(def: #export procedures
  @.Bundle
  (<| (@.prefix "jvm")
      (|> (dict.new text.Hash<Text>)
          (dict.merge conversion-procs)
          (dict.merge int-procs)
          (dict.merge long-procs)
          (dict.merge float-procs)
          (dict.merge double-procs)
          (dict.merge char-procs)
          (dict.merge array-procs)
          (dict.merge object-procs)
          (dict.merge member-procs)
          )))