aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lux/analyser/host.clj43
-rw-r--r--src/lux/analyser/lux.clj130
-rw-r--r--src/lux/compiler/type.clj3
-rw-r--r--src/lux/type.clj16
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)))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 06:49:15 +0000