- Re-organized analysis.

2 files changed, 1659 insertions, 0 deletions

diff --git a/new-luxc/source/luxc/lang/analysis/procedure/common.lux b/new-luxc/source/luxc/lang/analysis/procedure/common.lux
new file mode 100644
index 000000000..e06a3d2b4
--- /dev/null
+++ b/new-luxc/source/luxc/lang/analysis/procedure/common.lux
@@ -0,0 +1,418 @@
+(;module:
+  lux
+  (lux (control [monad #+ do])
+       (concurrency ["A" atom])
+       (data [text]
+             text/format
+             (coll [list "list/" Functor<List>]
+                   [array]
+                   [dict #+ Dict]))
+       [meta]
+       (meta [code]
+             (type ["tc" check]))
+       [io])
+  (luxc ["&" base]
+        (lang ["la" analysis]
+              (analysis ["&;" common]
+                        [";A" function]
+                        [";A" case]
+                        [";A" type]))))
+
+## [Utils]
+(type: #export Proc
+  (-> &;Analyser &;Eval (List Code) (Meta la;Analysis)))
+
+(type: #export Bundle
+  (Dict Text Proc))
+
+(def: #export (install name unnamed)
+  (-> Text (-> Text Proc)
+      (-> Bundle Bundle))
+  (dict;put name (unnamed name)))
+
+(def: #export (prefix prefix bundle)
+  (-> Text Bundle Bundle)
+  (|> bundle
+      dict;entries
+      (list/map (function [[key val]] [(format prefix " " key) val]))
+      (dict;from-list text;Hash<Text>)))
+
+(def: #export (wrong-arity proc expected actual)
+  (-> Text Nat Nat Text)
+  (format "Wrong arity for " (%t proc) "\n"
+          "Expected: " (|> expected nat-to-int %i) "\n"
+          "  Actual: " (|> actual nat-to-int %i)))
+
+(def: (simple proc input-types output-type)
+  (-> Text (List Type) Type Proc)
+  (let [num-expected (list;size input-types)]
+    (function [analyse eval args]
+      (let [num-actual (list;size args)]
+        (if (n.= num-expected num-actual)
+          (do meta;Monad<Meta>
+            [argsA (monad;map @
+                              (function [[argT argC]]
+                                (&;with-expected-type argT
+                                  (analyse argC)))
+                              (list;zip2 input-types args))
+             expected meta;expected-type
+             _ (&;with-type-env
+                 (tc;check expected output-type))]
+            (wrap (la;procedure proc argsA)))
+          (&;fail (wrong-arity proc num-expected num-actual)))))))
+
+(def: #export (nullary valueT proc)
+  (-> Type Text Proc)
+  (simple proc (list) valueT))
+
+(def: #export (unary inputT outputT proc)
+  (-> Type Type Text Proc)
+  (simple proc (list inputT) outputT))
+
+(def: #export (binary subjectT paramT outputT proc)
+  (-> Type Type Type Text Proc)
+  (simple proc (list subjectT paramT) outputT))
+
+(def: #export (trinary subjectT param0T param1T outputT proc)
+  (-> Type Type Type Type Text Proc)
+  (simple proc (list subjectT param0T param1T) outputT))
+
+## [Analysers]
+## "lux is" represents reference/pointer equality.
+(def: (lux-is proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        ((binary varT varT Bool proc)
+         analyse eval args)))))
+
+## "lux try" provides a simple way to interact with the host platform's
+## error-handling facilities.
+(def: (lux-try proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list opC))
+          (do meta;Monad<Meta>
+            [opA (&;with-expected-type (type (io;IO varT))
+                   (analyse opC))
+             outputT (&;with-type-env
+                       (tc;clean var-id (type (Either Text varT))))
+             expected meta;expected-type
+             _ (&;with-type-env
+                 (tc;check expected outputT))]
+            (wrap (la;procedure proc (list opA))))
+          
+          _
+          (&;fail (wrong-arity proc +1 (list;size args))))))))
+
+(def: (lux//function proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list [_ (#;Symbol ["" func-name])]
+                   [_ (#;Symbol ["" arg-name])]
+                   body))
+          (functionA;analyse-function analyse func-name arg-name body)
+          
+          _
+          (&;fail (wrong-arity proc +3 (list;size args))))))))
+
+(def: (lux//case proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list input [_ (#;Record branches)]))
+          (caseA;analyse-case analyse input branches)
+          
+          _
+          (&;fail (wrong-arity proc +2 (list;size args))))))))
+
+(do-template [<name> <analyser>]
+  [(def: (<name> proc)
+     (-> Text Proc)
+     (function [analyse eval args]
+       (&common;with-var
+         (function [[var-id varT]]
+           (case args
+             (^ (list typeC valueC))
+             (<analyser> analyse eval typeC valueC)
+             
+             _
+             (&;fail (wrong-arity proc +2 (list;size args))))))))]
+
+  [lux//check typeA;analyse-check]
+  [lux//coerce typeA;analyse-coerce])
+
+(def: (lux//check//type proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (case args
+      (^ (list valueC))
+      (do meta;Monad<Meta>
+        [valueA (&;with-expected-type Type
+                  (analyse valueC))
+         expected meta;expected-type
+         _ (&;with-type-env
+             (tc;check expected Type))]
+        (wrap valueA))
+      
+      _
+      (&;fail (wrong-arity proc +1 (list;size args))))))
+
+(def: lux-procs
+  Bundle
+  (|> (dict;new text;Hash<Text>)
+      (install "is" lux-is)
+      (install "try" lux-try)
+      (install "function" lux//function)
+      (install "case" lux//case)
+      (install "check" lux//check)
+      (install "coerce" lux//coerce)
+      (install "check type" lux//check//type)))
+
+(def: io-procs
+  Bundle
+  (<| (prefix "io")
+      (|> (dict;new text;Hash<Text>)
+          (install "log" (unary Text Unit))
+          (install "error" (unary Text Bottom))
+          (install "exit" (unary Nat Bottom))
+          (install "current-time" (nullary Int)))))
+
+(def: bit-procs
+  Bundle
+  (<| (prefix "bit")
+      (|> (dict;new text;Hash<Text>)
+          (install "count" (unary Nat Nat))
+          (install "and" (binary Nat Nat Nat))
+          (install "or" (binary Nat Nat Nat))
+          (install "xor" (binary Nat Nat Nat))
+          (install "shift-left" (binary Nat Nat Nat))
+          (install "unsigned-shift-right" (binary Nat Nat Nat))
+          (install "shift-right" (binary Int Nat Int))
+          )))
+
+(def: nat-procs
+  Bundle
+  (<| (prefix "nat")
+      (|> (dict;new text;Hash<Text>)
+          (install "+" (binary Nat Nat Nat))
+          (install "-" (binary Nat Nat Nat))
+          (install "*" (binary Nat Nat Nat))
+          (install "/" (binary Nat Nat Nat))
+          (install "%" (binary Nat Nat Nat))
+          (install "=" (binary Nat Nat Bool))
+          (install "<" (binary Nat Nat Bool))
+          (install "min" (nullary Nat))
+          (install "max" (nullary Nat))
+          (install "to-int" (unary Nat Int))
+          (install "to-text" (unary Nat Text)))))
+
+(def: int-procs
+  Bundle
+  (<| (prefix "int")
+      (|> (dict;new text;Hash<Text>)
+          (install "+" (binary Int Int Int))
+          (install "-" (binary Int Int Int))
+          (install "*" (binary Int Int Int))
+          (install "/" (binary Int Int Int))
+          (install "%" (binary Int Int Int))
+          (install "=" (binary Int Int Bool))
+          (install "<" (binary Int Int Bool))
+          (install "min" (nullary Int))
+          (install "max" (nullary Int))
+          (install "to-nat" (unary Int Nat))
+          (install "to-frac" (unary Int Frac)))))
+
+(def: deg-procs
+  Bundle
+  (<| (prefix "deg")
+      (|> (dict;new text;Hash<Text>)
+          (install "+" (binary Deg Deg Deg))
+          (install "-" (binary Deg Deg Deg))
+          (install "*" (binary Deg Deg Deg))
+          (install "/" (binary Deg Deg Deg))
+          (install "%" (binary Deg Deg Deg))
+          (install "=" (binary Deg Deg Bool))
+          (install "<" (binary Deg Deg Bool))
+          (install "scale" (binary Deg Nat Deg))
+          (install "reciprocal" (binary Deg Nat Deg))
+          (install "min" (nullary Deg))
+          (install "max" (nullary Deg))
+          (install "to-frac" (unary Deg Frac)))))
+
+(def: frac-procs
+  Bundle
+  (<| (prefix "frac")
+      (|> (dict;new text;Hash<Text>)
+          (install "+" (binary Frac Frac Frac))
+          (install "-" (binary Frac Frac Frac))
+          (install "*" (binary Frac Frac Frac))
+          (install "/" (binary Frac Frac Frac))
+          (install "%" (binary Frac Frac Frac))
+          (install "=" (binary Frac Frac Bool))
+          (install "<" (binary Frac Frac Bool))
+          (install "smallest" (nullary Frac))
+          (install "min" (nullary Frac))
+          (install "max" (nullary Frac))
+          (install "not-a-number" (nullary Frac))
+          (install "positive-infinity" (nullary Frac))
+          (install "negative-infinity" (nullary Frac))
+          (install "to-deg" (unary Frac Deg))
+          (install "to-int" (unary Frac Int))
+          (install "encode" (unary Frac Text))
+          (install "decode" (unary Text (type (Maybe Frac)))))))
+
+(def: text-procs
+  Bundle
+  (<| (prefix "text")
+      (|> (dict;new text;Hash<Text>)
+          (install "=" (binary Text Text Bool))
+          (install "<" (binary Text Text Bool))
+          (install "prepend" (binary Text Text Text))
+          (install "index" (trinary Text Text Nat (type (Maybe Nat))))
+          (install "size" (unary Text Nat))
+          (install "hash" (unary Text Nat))
+          (install "replace-once" (trinary Text Text Text Text))
+          (install "replace-all" (trinary Text Text Text Text))
+          (install "char" (binary Text Nat Nat))
+          (install "clip" (trinary Text Nat Nat Text))
+          )))
+
+(def: (array-get proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        ((binary Nat (type (Array varT)) varT proc)
+         analyse eval args)))))
+
+(def: (array-put proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        ((trinary Nat varT (type (Array varT)) (type (Array varT)) proc)
+         analyse eval args)))))
+
+(def: (array-remove proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        ((binary Nat (type (Array varT)) (type (Array varT)) proc)
+         analyse eval args)))))
+
+(def: array-procs
+  Bundle
+  (<| (prefix "array")
+      (|> (dict;new text;Hash<Text>)
+          (install "new" (unary Nat Array))
+          (install "get" array-get)
+          (install "put" array-put)
+          (install "remove" array-remove)
+          (install "size" (unary (type (Ex [a] (Array a))) Nat))
+          )))
+
+(def: math-procs
+  Bundle
+  (<| (prefix "math")
+      (|> (dict;new text;Hash<Text>)
+          (install "cos" (unary Frac Frac))
+          (install "sin" (unary Frac Frac))
+          (install "tan" (unary Frac Frac))
+          (install "acos" (unary Frac Frac))
+          (install "asin" (unary Frac Frac))
+          (install "atan" (unary Frac Frac))
+          (install "cosh" (unary Frac Frac))
+          (install "sinh" (unary Frac Frac))
+          (install "tanh" (unary Frac Frac))
+          (install "exp" (unary Frac Frac))
+          (install "log" (unary Frac Frac))
+          (install "root2" (unary Frac Frac))
+          (install "root3" (unary Frac Frac))
+          (install "ceil" (unary Frac Frac))
+          (install "floor" (unary Frac Frac))
+          (install "round" (unary Frac Frac))
+          (install "atan2" (binary Frac Frac Frac))
+          (install "pow" (binary Frac Frac Frac))
+          )))
+
+(def: (atom-new proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list initC))
+          (do meta;Monad<Meta>
+            [initA (&;with-expected-type varT
+                     (analyse initC))
+             outputT (&;with-type-env
+                       (tc;clean var-id (type (A;Atom varT))))
+             expected meta;expected-type
+             _ (&;with-type-env
+                 (tc;check expected outputT))]
+            (wrap (la;procedure proc (list initA))))
+          
+          _
+          (&;fail (wrong-arity proc +1 (list;size args))))))))
+
+(def: (atom-read proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        ((unary (type (A;Atom varT)) varT proc)
+         analyse eval args)))))
+
+(def: (atom-compare-and-swap proc)
+  (-> Text Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        ((trinary varT varT (type (A;Atom varT)) Bool proc)
+         analyse eval args)))))
+
+(def: atom-procs
+  Bundle
+  (<| (prefix "atom")
+      (|> (dict;new text;Hash<Text>)
+          (install "new" atom-new)
+          (install "read" atom-read)
+          (install "compare-and-swap" atom-compare-and-swap)
+          )))
+
+(def: process-procs
+  Bundle
+  (<| (prefix "process")
+      (|> (dict;new text;Hash<Text>)
+          (install "concurrency-level" (nullary Nat))
+          (install "future" (unary (type (io;IO Top)) Unit))
+          (install "schedule" (binary Nat (type (io;IO Top)) Unit))
+          )))
+
+(def: #export procedures
+  Bundle
+  (<| (prefix "lux")
+      (|> (dict;new text;Hash<Text>)
+          (dict;merge lux-procs)
+          (dict;merge bit-procs)
+          (dict;merge nat-procs)
+          (dict;merge int-procs)
+          (dict;merge deg-procs)
+          (dict;merge frac-procs)
+          (dict;merge text-procs)
+          (dict;merge array-procs)
+          (dict;merge math-procs)
+          (dict;merge atom-procs)
+          (dict;merge process-procs)
+          (dict;merge io-procs))))
diff --git a/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux
new file mode 100644
index 000000000..3ba7713ac
--- /dev/null
+++ b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux
@@ -0,0 +1,1241 @@
+(;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]))
+       [meta "meta/" Monad<Meta>]
+       (meta [code]
+             ["s" syntax]
+             [type]
+             (type ["tc" check]))
+       [host])
+  (luxc ["&" base]
+        ["&;" host]
+        (lang ["la" analysis]
+              (analysis ["&;" common]
+                        ["&;" inference])))
+  ["@" ../common]
+  )
+
+(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]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list arrayC))
+          (do meta;Monad<Meta>
+            [arrayA (&;with-expected-type (type (Array varT))
+                      (analyse arrayC))
+             _ (&;infer Nat)]
+            (wrap (la;procedure proc (list arrayA))))
+
+          _
+          (&;fail (@;wrong-arity proc +1 (list;size args))))))))
+
+(def: (invalid-array-type arrayT)
+  (-> Type Text)
+  (format "Invalid type for array: " (%type arrayT)))
+
+(def: (array-new proc)
+  (-> Text @;Proc)
+  (function [analyse eval args]
+    (case args
+      (^ (list lengthC))
+      (do meta;Monad<Meta>
+        [lengthA (&;with-expected-type Nat
+                   (analyse lengthC))
+         expectedT meta;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
+                                     (&;fail (invalid-array-type expectedT)))
+
+                                   (^ (#;Primitive "#Array" (list elemT)))
+                                   (recur elemT (n.inc level))
+
+                                   (#;Primitive class _)
+                                   (wrap [level class])
+                                   
+                                   _
+                                   (&;fail (invalid-array-type expectedT)))))
+         _ (&;assert "Must have at least 1 level of nesting in array type."
+                     (n.> +0 level))]
+        (wrap (la;procedure proc (list (code;nat (n.dec level)) (code;text elem-class) lengthA))))
+
+      _
+      (&;fail (@;wrong-arity proc +1 (list;size args))))))
+
+(exception: #export Not-Object-Type)
+
+(def: (check-jvm objectT)
+  (-> Type (Meta Text))
+  (case objectT
+    (#;Primitive name _)
+    (meta/wrap name)
+
+    (#;Named name unnamed)
+    (check-jvm unnamed)
+
+    (#;Var id)
+    (meta/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 Not-Object-Type (%type objectT)))
+
+    _
+    (&;throw Not-Object-Type (%type objectT))))
+
+(def: (check-object objectT)
+  (-> Type (Meta Text))
+  (do meta;Monad<Meta>
+    [name (check-jvm objectT)]
+    (if (dict;contains? name boxes)
+      (&;fail (format "Primitives are not objects: " name))
+      (:: meta;Monad<Meta> wrap name))))
+
+(def: (box-array-element-type elemT)
+  (-> Type (Meta [Type Text]))
+  (do meta;Monad<Meta>
+    []
+    (case elemT
+      (#;Primitive name #;Nil)
+      (let [boxed-name (|> (dict;get name boxes)
+                           (maybe;default name))]
+        (wrap [(#;Primitive boxed-name #;Nil)
+               boxed-name]))
+
+      (#;Primitive name _)
+      (if (dict;contains? name boxes)
+        (&;fail (format "Primitives cannot be parameterized: " name))
+        (:: meta;Monad<Meta> wrap [elemT name]))
+
+      _
+      (&;fail (format "Invalid type for array element: " (%type elemT))))))
+
+(def: (array-read proc)
+  (-> Text @;Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list arrayC idxC))
+          (do meta;Monad<Meta>
+            [arrayA (&;with-expected-type (type (Array varT))
+                      (analyse arrayC))
+             elemT (&;with-type-env
+                     (tc;read var-id))
+             [elemT elem-class] (box-array-element-type elemT)
+             idxA (&;with-expected-type Nat
+                    (analyse idxC))
+             _ (&;infer elemT)]
+            (wrap (la;procedure proc (list (code;text elem-class) idxA arrayA))))
+
+          _
+          (&;fail (@;wrong-arity proc +2 (list;size args))))))))
+
+(def: (array-write proc)
+  (-> Text @;Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list arrayC idxC valueC))
+          (do meta;Monad<Meta>
+            [arrayA (&;with-expected-type (type (Array varT))
+                      (analyse arrayC))
+             elemT (&;with-type-env
+                     (tc;read var-id))
+             [valueT elem-class] (box-array-element-type elemT)
+             idxA (&;with-expected-type Nat
+                    (analyse idxC))
+             valueA (&;with-expected-type valueT
+                      (analyse valueC))
+             _ (&;infer (type (Array elemT)))]
+            (wrap (la;procedure proc (list (code;text elem-class) idxA valueA arrayA))))
+
+          _
+          (&;fail (@;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 meta;Monad<Meta>
+        [expectedT meta;expected-type
+         _ (check-object expectedT)]
+        (wrap (la;procedure proc (list))))
+
+      _
+      (&;fail (@;wrong-arity proc +0 (list;size args))))))
+
+(def: (object-null? proc)
+  (-> Text @;Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list objectC))
+          (do meta;Monad<Meta>
+            [objectA (&;with-expected-type varT
+                       (analyse objectC))
+             objectT (&;with-type-env
+                       (tc;read var-id))
+             _ (check-object objectT)
+             _ (&;infer Bool)]
+            (wrap (la;procedure proc (list objectA))))
+
+          _
+          (&;fail (@;wrong-arity proc +1 (list;size args))))))))
+
+(def: (object-synchronized proc)
+  (-> Text @;Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list monitorC exprC))
+          (do meta;Monad<Meta>
+            [monitorA (&;with-expected-type varT
+                        (analyse monitorC))
+             monitorT (&;with-type-env
+                        (tc;read var-id))
+             _ (check-object monitorT)
+             exprA (analyse exprC)]
+            (wrap (la;procedure proc (list monitorA exprA))))
+
+          _
+          (&;fail (@;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 meta;Monad<Meta>
+    [class-loader &host;class-loader]
+    (case (Class.forName [name false class-loader])
+      (#e;Success [class])
+      (wrap class)
+
+      (#e;Error error)
+      (&;fail (format "Unknown class: " name)))))
+
+(def: (sub-class? super sub)
+  (-> Text Text (Meta Bool))
+  (do meta;Monad<Meta>
+    [super (load-class super)
+     sub (load-class sub)]
+    (wrap (Class.isAssignableFrom [sub] super))))
+
+(exception: #export Not-Throwable)
+
+(def: (object-throw proc)
+  (-> Text @;Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list exceptionC))
+          (do meta;Monad<Meta>
+            [exceptionA (&;with-expected-type varT
+                          (analyse exceptionC))
+             exceptionT (&;with-type-env
+                          (tc;read var-id))
+             exception-class (check-object exceptionT)
+             ? (sub-class? "java.lang.Throwable" exception-class)
+             _ (: (Meta Unit)
+                  (if ?
+                    (wrap [])
+                    (&;throw Not-Throwable exception-class)))
+             _ (&;infer Bottom)]
+            (wrap (la;procedure proc (list exceptionA))))
+
+          _
+          (&;fail (@;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 meta;Monad<Meta>
+          [_ (load-class class)
+           _ (&;infer (#;Primitive "java.lang.Class" (list (#;Primitive class (list)))))]
+          (wrap (la;procedure proc (list (code;text class)))))
+
+        _
+        (&;fail (format "Wrong syntax for '" proc "'.")))
+
+      _
+      (&;fail (@;wrong-arity proc +1 (list;size args))))))
+
+(exception: #export Cannot-Be-Instance)
+
+(def: (object-instance? proc)
+  (-> Text @;Proc)
+  (function [analyse eval args]
+    (&common;with-var
+      (function [[var-id varT]]
+        (case args
+          (^ (list classC objectC))
+          (case classC
+            [_ (#;Text class)]
+            (do meta;Monad<Meta>
+              [objectA (&;with-expected-type varT
+                         (analyse objectC))
+               objectT (&;with-type-env
+                         (tc;read var-id))
+               object-class (check-object objectT)
+               ? (sub-class? class object-class)]
+              (if ?
+                (do @
+                  [_ (&;infer Bool)]
+                  (wrap (la;procedure proc (list (code;text class)))))
+                (&;throw Cannot-Be-Instance (format object-class " !<= "  class))))
+
+            _
+            (&;fail (format "Wrong syntax for '" proc "'.")))
+
+          _
+          (&;fail (@;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?)
+          )))
+
+(exception: #export Final-Field)
+
+(exception: #export Cannot-Convert-To-Class)
+(exception: #export Cannot-Convert-To-Parameter)
+(exception: #export Cannot-Convert-To-Lux-Type)
+(exception: #export Cannot-Cast-To-Primitive)
+(exception: #export JVM-Type-Is-Not-Class)
+
+(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)
+        (meta/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))))
+
+(exception: #export Unknown-Type-Var)
+
+(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)
+            (meta/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)
+            
+            _
+            (meta/wrap Top)))
+
+        (host;instance? Class java-type)
+        (let [java-type (:! (Class Object) java-type)
+              class-name (Class.getName [] java-type)]
+          (meta/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 meta;Monad<Meta>
+              [paramsT (|> java-type
+                           (ParameterizedType.getActualTypeArguments [])
+                           array;to-list
+                           (monad;map @ (java-type-to-lux-type mappings)))]
+              (meta/wrap (#;Primitive (Class.getName [] (:! (Class Object) raw))
+                                      paramsT)))
+            (&;throw JVM-Type-Is-Not-Class (type-descriptor raw))))
+
+        (host;instance? GenericArrayType java-type)
+        (do meta;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))]
+      (if (text/= class-name name)
+        (if (n.= (list;size class-params)
+                 (list;size params))
+          (meta/wrap (|> params
+                         (list;zip2 (list/map (TypeVariable.getName []) class-params))
+                         (dict;from-list text;Hash<Text>)))
+          (&;fail (format "Class and host-type parameters do not match: " "class = " class-name " | host type = " name)))
+        (&;fail (format "Class and host-type names do not match: " "class = " class-name " | host type = " name))))
+
+    _
+    (&;fail (format "Not a host type: " (%type type)))))
+
+(def: (cast direction to from)
+  (-> Direction Type Type (Meta [Text Type]))
+  (do meta;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-To-Primitive (format from-name " => " to-name))))
+
+          (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 (format "Class '" from-name "' is not a sub-class of class '" to-name "'.")
+                         (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
+              (&;fail (format "No valid path between " (%type from) "and " (%type to) ".")))))))
+
+(def: (infer-out outputT)
+  (-> Type (Meta [Text Type]))
+  (do meta;Monad<Meta>
+    [expectedT meta;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 meta;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])
+          (&;fail (format "Field '" field-name "' does not belong to class '" class-name "'.\n"
+                          "Belongs to '" (Class.getName [] owner) "'."))))
+
+      (#e;Error _)
+      (&;fail (format "Unknown field '" field-name "' for class '" class-name "'.")))))
+
+(def: (static-field class-name field-name)
+  (-> Text Text (Meta [Type Bool]))
+  (do meta;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])])))
+      (&;fail (format "Field '" field-name "' of class '" class-name "' is not static.")))))
+
+(exception: #export Non-Object-Type)
+
+(def: (virtual-field class-name field-name objectT)
+  (-> Text Text Type (Meta [Type Bool]))
+  (do meta;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 (format "Number of paremeters in type does not match expected amount (" (%n num-vars) "): " (%type objectT))
+                                      (n.= num-params num-vars))]
+                         (wrap (|> (list;zip2 var-names _class-params)
+                                   (dict;from-list text;Hash<Text>))))
+
+                       _
+                       (&;throw Non-Object-Type (%type objectT))))
+         fieldT (java-type-to-lux-type mappings fieldJT)]
+        (wrap [fieldT (Modifier.isFinal [modifiers])]))
+      (&;fail (format "Field '" field-name "' of class '" class-name "' is static.")))))
+
+(def: (analyse-object class analyse sourceC)
+  (-> Text &;Analyser Code (Meta [Type la;Analysis]))
+  (<| &common;with-var (function [[var-id varT]])
+      (do meta;Monad<Meta>
+        [target-class (load-class class)
+         targetT (java-type-to-lux-type fresh-mappings
+                                        (:! java.lang.reflect.Type
+                                            target-class))
+         sourceA (&;with-expected-type varT
+                   (analyse sourceC))
+         sourceT (&;with-type-env
+                   (tc;read var-id))
+         [unboxed castT] (cast #Out targetT sourceT)
+         _ (&;assert (format "Object cannot be a primitive: " unboxed)
+                     (not (dict;contains? unboxed boxes)))]
+        (wrap [castT sourceA]))))
+
+(def: (analyse-input analyse targetT sourceC)
+  (-> &;Analyser Type Code (Meta [Type Text la;Analysis]))
+  (<| &common;with-var (function [[var-id varT]])
+      (do meta;Monad<Meta>
+        [sourceA (&;with-expected-type varT
+                   (analyse sourceC))
+         sourceT (&;with-type-env
+                   (tc;read var-id))
+         [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 meta;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)))))
+
+        _
+        (&;fail (format "Wrong syntax for '" proc "'.")))
+
+      _
+      (&;fail (@;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 meta;Monad<Meta>
+          [[fieldT final?] (static-field class field)
+           _ (&;assert (Final-Field (format class "#" field))
+                       (not final?))
+           [valueT unboxed valueA] (analyse-input analyse fieldT valueC)
+           _ (&;with-type-env
+               (tc;check fieldT valueT))
+           _ (&;infer Unit)]
+          (wrap (la;procedure proc (list (code;text class) (code;text field)
+                                         (code;text unboxed) valueA))))
+
+        _
+        (&;fail (format "Wrong syntax for '" proc "'.")))
+
+      _
+      (&;fail (@;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 meta;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))))
+
+        _
+        (&;fail (format "Wrong syntax for '" proc "'.")))
+
+      _
+      (&;fail (@;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 meta;Monad<Meta>
+          [[objectT objectA] (analyse-object class analyse objectC)
+           [fieldT final?] (virtual-field class field objectT)
+           _ (&;assert (Final-Field (format class "#" field))
+                       (not final?))
+           [valueT unboxed valueA] (analyse-input analyse fieldT valueC)
+           _ (&;with-type-env
+               (tc;check fieldT valueT))
+           _ (&;infer objectT)]
+          (wrap (la;procedure proc (list (code;text class) (code;text field) (code;text unboxed) valueA objectA))))
+
+        _
+        (&;fail (format "Wrong syntax for '" proc "'.")))
+
+      _
+      (&;fail (@;wrong-arity proc +4 (list;size args))))))
+
+(def: (java-type-to-parameter type)
+  (-> java.lang.reflect.Type (Meta Text))
+  (cond (host;instance? Class type)
+        (meta/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))
+        (meta/wrap "java.lang.Object")
+
+        (host;instance? GenericArrayType type)
+        (do meta;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 meta;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 meta;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 meta;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]))))
+
+(exception: #export No-Candidate-Method)
+(exception: #export Too-Many-Candidate-Methods)
+
+(def: (methods class-name method-name method-type arg-classes)
+  (-> Text Text Method-Type (List Text) (Meta [Type (List Type)]))
+  (do meta;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-Candidate-Method (format class-name "#" method-name))
+      
+      (#;Cons candidate #;Nil)
+      (|> candidate product;right (method-to-type method-type))
+
+      _
+      (&;throw Too-Many-Candidate-Methods (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 meta;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]))))
+
+(exception: #export No-Candidate-Constructor)
+(exception: #export Too-Many-Candidate-Constructors)
+
+(def: (constructor-methods class-name arg-classes)
+  (-> Text (List Text) (Meta [Type (List Type)]))
+  (do meta;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-Candidate-Constructor (format class-name "(" (text;join-with ", " arg-classes) ")"))
+      
+      (#;Cons candidate #;Nil)
+      (|> candidate product;right constructor-to-type)
+
+      _
+      (&;throw Too-Many-Candidate-Constructors 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 meta;Monad<Meta>
+      [[argT argA] (&common;with-unknown-type
+                     (analyse argC))
+       expectedT meta;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 meta;Monad<Meta>
+        [#let [argsT (list/map product;left argsTC)]
+         [methodT exceptionsT] (methods class method #Static argsT)
+         [outputT argsA] (&inference;apply-function (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)))))
+
+      _
+      (&;fail (format "Wrong syntax for '" proc "'.")))))
+
+(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 meta;Monad<Meta>
+        [#let [argsT (list/map product;left argsTC)]
+         [methodT exceptionsT] (methods class method #Virtual argsT)
+         [outputT allA] (&inference;apply-function (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)))))
+
+      _
+      (&;fail (format "Wrong syntax for '" proc "'.")))))
+
+(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 meta;Monad<Meta>
+        [#let [argsT (list/map product;left argsTC)]
+         [methodT exceptionsT] (methods class method #Special argsT)
+         [outputT argsA] (&inference;apply-function (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)))))
+
+      _
+      (&;fail (format "Wrong syntax for '" proc "'.")))))
+
+(exception: #export Not-Interface)
+
+(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 meta;Monad<Meta>
+        [#let [argsT (list/map product;left argsTC)]
+         class (load-class class-name)
+         _ (&;assert (Not-Interface class-name)
+                     (Modifier.isInterface [(Class.getModifiers [] class)]))
+         [methodT exceptionsT] (methods class-name method #Interface argsT)
+         [outputT argsA] (&inference;apply-function (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)))))
+
+      _
+      (&;fail (format "Wrong syntax for '" proc "'.")))))
+
+(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 meta;Monad<Meta>
+        [#let [argsT (list/map product;left argsTC)]
+         [methodT exceptionsT] (constructor-methods class argsT)
+         [outputT argsA] (&inference;apply-function (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)))))
+
+      _
+      (&;fail (format "Wrong syntax for '" proc "'.")))))
+
+(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)
+          )))