From dbbd680d0a47c64eeb2627d458c22e8ea16206d5 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 9 Sep 2015 18:36:22 -0400 Subject: - Added type inference for functions. - Fixed a bug wherein the "case" macro ignored tokens when receiving uneven inputs. --- src/lux/analyser/host.clj | 43 +++++++++------ src/lux/analyser/lux.clj | 130 +++++++++++++++++++++++++++++----------------- src/lux/compiler/type.clj | 3 ++ src/lux/type.clj | 16 +++++- 4 files changed, 124 insertions(+), 68 deletions(-) (limited to 'src') 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 [ ] (let [input-type (&/V &/$DataT ) @@ -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 (&/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))) -- cgit v1.2.3