- Added type inference for functions.

- Fixed a bug wherein the "case" macro ignored tokens when receiving uneven inputs.

4 files changed, 124 insertions, 68 deletions

diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index 0b333ce07..9a05a6695 100644
--- a/src/lux/analyser/host.clj
+++ b/src/lux/analyser/host.clj
@@ -49,6 +49,29 @@
     _
     type))
 
+(defn ^:private as-otype [tname]
+  (case tname
+    "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"
+    ;; else
+    tname
+    ))
+
+(defn ^:private as-otype+ [type]
+  "(-> Type Type)"
+  (|case type
+    (&/$DataT tname)
+    (&/V &/$DataT (as-otype tname))
+
+    _
+    type))
+
 ;; [Resources]
 (do-template [<name> <output-tag> <input-class> <output-class>]
   (let [input-type (&/V &/$DataT <input-class>)
@@ -144,7 +167,7 @@
                        =classes
                        ?args)
         :let [output-type =return]
-        _ (&type/check exo-type output-type)]
+        _ (&type/check exo-type (as-otype+ output-type))]
     (return (&/|list (&/T (&/V &&/$jvm-invokestatic (&/T ?class ?method =classes =args)) output-type)))))
 
 (defn analyse-jvm-instanceof [analyse exo-type ?class ?object]
@@ -163,7 +186,7 @@
           =args (&/map2% (fn [?c ?o] (&&/analyse-1 analyse (&/V &/$DataT ?c) ?o))
                          =classes ?args)
           :let [output-type =return]
-          _ (&type/check exo-type output-type)]
+          _ (&type/check exo-type (as-otype+ output-type))]
       (return (&/|list (&/T (&/V <tag> (&/T ?class ?method =classes =object =args)) output-type)))))
 
   analyse-jvm-invokevirtual   &&/$jvm-invokevirtual
@@ -181,7 +204,7 @@
                          (&&/analyse-1 analyse (&/V &/$DataT ?c) ?o))
                        =classes ?args)
         :let [output-type =return]
-        _ (&type/check exo-type output-type)]
+        _ (&type/check exo-type (as-otype+ output-type))]
     (return (&/|list (&/T (&/V &&/$jvm-invokespecial (&/T ?class ?method =classes =object =args)) output-type)))))
 
 (defn analyse-jvm-null? [analyse exo-type ?object]
@@ -252,20 +275,6 @@
             :concurrency nil}
            modifiers))
 
-(defn ^:private as-otype [tname]
-  (case tname
-    "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"
-    ;; else
-    tname
-    ))
-
 (defn analyse-jvm-class [analyse compile-token ?name ?super-class ?interfaces ?fields ?methods]
   (|do [=interfaces (&/map% extract-text ?interfaces)
         =fields (&/map% (fn [?field]
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index f22cc6c9a..39eda451f 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -301,27 +301,80 @@
     (return (&/|list (&/T (&/V &&/$case (&/T =value =match))
                           exo-type)))))
 
+(defn ^:private count-univq [type]
+  "(-> Type Int)"
+  (|case type
+    (&/$UnivQ env type*)
+    (inc (count-univq type*))
+
+    _
+    0))
+
+(defn ^:private embed-inferred-input [input output]
+  "(-> Type Type Type)"
+  (|case output
+    (&/$UnivQ env output*)
+    (&type/Univ$ env (embed-inferred-input input output*))
+
+    _
+    (&type/Lambda$ input output)))
+
 (defn analyse-lambda* [analyse exo-type ?self ?arg ?body]
-  (|do [exo-type* (&type/actual-type exo-type)]
-    (|case exo-type
-      (&/$UnivQ _)
-      (&type/with-var
-        (fn [$var]
-          (|do [exo-type** (&type/apply-type exo-type* $var)]
-            (analyse-lambda* analyse exo-type** ?self ?arg ?body))))
-      ;; (|do [$var &type/existential
-      ;;       exo-type** (&type/apply-type exo-type* $var)]
-      ;;   (analyse-lambda* analyse exo-type** ?self ?arg ?body))
-      
-      (&/$LambdaT ?arg-t ?return-t)
-      (|do [[=scope =captured =body] (&&lambda/with-lambda ?self exo-type*
-                                       ?arg ?arg-t
-                                       (&&/analyse-1 analyse ?return-t ?body))]
-        (return (&/T (&/V &&/$lambda (&/T =scope =captured =body)) exo-type*)))
-      
-      _
-      (fail (str "[Analyser Error] Functions require function types: "
-                 (&type/show-type exo-type*))))))
+  (|case exo-type
+    (&/$VarT id)
+    (|do [? (&type/bound? id)]
+      (if ?
+        (|do [exo-type* (&type/deref id)]
+          (analyse-lambda* analyse exo-type* ?self ?arg ?body))
+        ;; Inference
+        (&type/with-var
+          (fn [$input]
+            (&type/with-var
+              (fn [$output]
+                (|do [[lambda-analysis lambda-type] (analyse-lambda* analyse (&type/Lambda$ $input $output) ?self ?arg ?body)
+                      =input (&type/resolve-type $input)
+                      =output (&type/resolve-type $output)
+                      inferred-type (|case =input
+                                      (&/$VarT iid)
+                                      (|do [:let [=input* (&type/Bound$ (->> (count-univq =output) (* 2) (+ 1)))]
+                                            _ (&type/set-var iid =input*)
+                                            =output* (&type/clean $input =output)
+                                            =output** (&type/clean $output =output*)]
+                                        (return (&type/Univ$ (&/|list) (embed-inferred-input =input* =output**))))
+
+                                      _
+                                      (|do [=output* (&type/clean $input =output)
+                                            =output** (&type/clean $output =output*)]
+                                        (return (embed-inferred-input =input =output**))))
+                      _ (&type/check exo-type inferred-type)
+                      ]
+                  (return (&/T lambda-analysis inferred-type)))
+                ))))))
+
+    _
+    (|do [exo-type* (&type/actual-type exo-type)]
+      (|case exo-type
+        (&/$UnivQ _)
+        (&type/with-var
+          (fn [$var]
+            (|do [exo-type** (&type/apply-type exo-type* $var)]
+              (analyse-lambda* analyse exo-type** ?self ?arg ?body))))
+        ;; (|do [$var &type/existential
+        ;;       exo-type** (&type/apply-type exo-type* $var)]
+        ;;   (analyse-lambda* analyse exo-type** ?self ?arg ?body))
+        
+        (&/$LambdaT ?arg-t ?return-t)
+        (|do [[=scope =captured =body] (&&lambda/with-lambda ?self exo-type*
+                                         ?arg ?arg-t
+                                         (&&/analyse-1 analyse ?return-t ?body))]
+          (return (&/T (&/V &&/$lambda (&/T =scope =captured =body)) exo-type*)))
+
+        
+        
+        _
+        (fail (str "[Analyser Error] Functions require function types: "
+                   (&type/show-type exo-type*)))))
+    ))
 
 (defn analyse-lambda** [analyse exo-type ?self ?arg ?body]
   (|case exo-type
@@ -330,35 +383,14 @@
           exo-type* (&type/apply-type exo-type $var)
           [_expr _] (analyse-lambda** analyse exo-type* ?self ?arg ?body)]
       (return (&/T _expr exo-type)))
-    ;; (&type/with-var
-    ;;   (fn [$var]
-    ;;     (|do [exo-type* (&type/apply-type exo-type $var)
-    ;;           [_expr _] (analyse-lambda** analyse exo-type* ?self ?arg ?body)]
-    ;;       (|case $var
-    ;;         (&/$VarT ?id)
-    ;;         (|do [? (&type/bound? ?id)]
-    ;;           (if ?
-    ;;             (|do [dtype (&type/deref ?id)
-    ;;                   ;; dtype* (&type/actual-type dtype)
-    ;;                   ]
-    ;;               (|case dtype
-    ;;                 (&/$BoundT ?vname)
-    ;;                 (return (&/T _expr exo-type))
-    
-    ;;                 (&/$ExT _)
-    ;;                 (return (&/T _expr exo-type))
-
-    ;;                 (&/$VarT ?_id)
-    ;;                 (|do [?? (&type/bound? ?_id)]
-    ;;                   ;; (return (&/T _expr exo-type))
-    ;;                   (if ??
-    ;;                     (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype)))
-    ;;                     (return (&/T _expr exo-type)))
-    ;;                   )
-
-    ;;                 _
-    ;;                 (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype)))))
-    ;;             (return (&/T _expr exo-type))))))))
+
+    (&/$VarT id)
+    (|do [? (&type/bound? id)]
+      (if ?
+        (|do [exo-type* (&type/actual-type exo-type)]
+          (analyse-lambda* analyse exo-type* ?self ?arg ?body))
+        ;; Inference
+        (analyse-lambda* analyse exo-type ?self ?arg ?body)))
     
     _
     (|do [exo-type* (&type/actual-type exo-type)]
diff --git a/src/lux/compiler/type.clj b/src/lux/compiler/type.clj
index 0d0300844..d75f6afef 100644
--- a/src/lux/compiler/type.clj
+++ b/src/lux/compiler/type.clj
@@ -80,4 +80,7 @@
     (&/$NamedT [?module ?name] ?type)
     (variant$ &/$NamedT (tuple$ (&/|list (tuple$ (&/|list (text$ ?module) (text$ ?name)))
                                          (->analysis ?type))))
+
+    _
+    (assert false (&type/show-type type))
     ))
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 4672b18d4..3b7349fca 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -26,8 +26,8 @@
 (def ^:private empty-env (&/V &/$Nil nil))
 (defn Data$ [name]
   (&/V &/$DataT name))
-(defn Bound$ [name]
-  (&/V &/$BoundT name))
+(defn Bound$ [idx]
+  (&/V &/$BoundT idx))
 (defn Var$ [id]
   (&/V &/$VarT id))
 (defn Lambda$ [in out]
@@ -986,3 +986,15 @@
 
     _
     (return false)))
+
+(defn resolve-type [type]
+  "(-> Type (Lux Type))"
+  (|case type
+    (&/$VarT id)
+    (|do [? (bound? id)]
+      (if ?
+        (deref id)
+        (return type)))
+
+    _
+    (return type)))