diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lux/analyser/host.clj | 48 | ||||
| -rw-r--r-- | src/lux/analyser/lux.clj | 12 | ||||
| -rw-r--r-- | src/lux/compiler/host.clj | 18 | ||||
| -rw-r--r-- | src/lux/compiler/type.clj | 62 | ||||
| -rw-r--r-- | src/lux/host.clj | 7 | ||||
| -rw-r--r-- | src/lux/type.clj | 164 |
6 files changed, 145 insertions, 166 deletions
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj index 9a05a6695..610f3c660 100644 --- a/src/lux/analyser/host.clj +++ b/src/lux/analyser/host.clj @@ -34,7 +34,7 @@ (defn ^:private ensure-object [token] "(-> Analysis (Lux (,)))" (|case token - [_ (&/$DataT _)] + [_ (&/$DataT _ _)] (return nil) _ @@ -43,8 +43,8 @@ (defn ^:private as-object [type] "(-> Type Type)" (|case type - (&/$DataT class) - (&/V &/$DataT (&type/as-obj class)) + (&/$DataT class params) + (&type/Data$ (&type/as-obj class) params) _ type)) @@ -66,16 +66,16 @@ (defn ^:private as-otype+ [type] "(-> Type Type)" (|case type - (&/$DataT tname) - (&/V &/$DataT (as-otype tname)) + (&/$DataT name params) + (&type/Data$ (as-otype name) params) _ type)) ;; [Resources] (do-template [<name> <output-tag> <input-class> <output-class>] - (let [input-type (&/V &/$DataT <input-class>) - output-type (&/V &/$DataT <output-class>)] + (let [input-type (&type/Data$ <input-class> (&/|list)) + output-type (&type/Data$ <output-class> (&/|list))] (defn <name> [analyse exo-type ?x ?y] (|do [=x (&&/analyse-1 analyse input-type ?x) =y (&&/analyse-1 analyse input-type ?y) @@ -160,10 +160,10 @@ =classes (&/map% extract-text ?classes) =return (&host/lookup-static-method class-loader ?class ?method =classes) ;; :let [_ (matchv ::M/objects [=return] - ;; [[&/$DataT _return-class]] + ;; [[&/$DataT _return-class (&/|list)]] ;; (prn 'analyse-jvm-invokestatic ?class ?method _return-class))] =args (&/map2% (fn [_class _arg] - (&&/analyse-1 analyse (&/V &/$DataT _class) _arg)) + (&&/analyse-1 analyse (&type/Data$ _class (&/|list)) _arg)) =classes ?args) :let [output-type =return] @@ -182,8 +182,8 @@ (|do [class-loader &/loader =classes (&/map% extract-text ?classes) =return (&host/lookup-virtual-method class-loader ?class ?method =classes) - =object (&&/analyse-1 analyse (&/V &/$DataT ?class) ?object) - =args (&/map2% (fn [?c ?o] (&&/analyse-1 analyse (&/V &/$DataT ?c) ?o)) + =object (&&/analyse-1 analyse (&type/Data$ ?class (&/|list)) ?object) + =args (&/map2% (fn [?c ?o] (&&/analyse-1 analyse (&type/Data$ ?c (&/|list)) ?o)) =classes ?args) :let [output-type =return] _ (&type/check exo-type (as-otype+ output-type))] @@ -199,9 +199,9 @@ =return (if (= "<init>" ?method) (return &type/Unit) (&host/lookup-virtual-method class-loader ?class ?method =classes)) - =object (&&/analyse-1 analyse (&/V &/$DataT ?class) ?object) + =object (&&/analyse-1 analyse (&type/Data$ ?class (&/|list)) ?object) =args (&/map2% (fn [?c ?o] - (&&/analyse-1 analyse (&/V &/$DataT ?c) ?o)) + (&&/analyse-1 analyse (&type/Data$ ?c (&/|list)) ?o)) =classes ?args) :let [output-type =return] _ (&type/check exo-type (as-otype+ output-type))] @@ -215,19 +215,19 @@ (return (&/|list (&/T (&/V &&/$jvm-null? =object) output-type))))) (defn analyse-jvm-null [analyse exo-type] - (|do [:let [output-type (&/V &/$DataT "null")] + (|do [:let [output-type (&type/Data$ "null" (&/|list))] _ (&type/check exo-type output-type)] (return (&/|list (&/T (&/V &&/$jvm-null nil) output-type))))) (defn analyse-jvm-new [analyse exo-type ?class ?classes ?args] (|do [=classes (&/map% extract-text ?classes) =args (&/map% (partial analyse-1+ analyse) ?args) - :let [output-type (&/V &/$DataT ?class)] + :let [output-type (&type/Data$ ?class (&/|list))] _ (&type/check exo-type output-type)] (return (&/|list (&/T (&/V &&/$jvm-new (&/T ?class =classes =args)) output-type))))) (defn analyse-jvm-new-array [analyse ?class ?length] - (return (&/|list (&/T (&/V &&/$jvm-new-array (&/T ?class ?length)) (&/V "array" (&/T (&/V &/$DataT ?class) + (return (&/|list (&/T (&/V &&/$jvm-new-array (&/T ?class ?length)) (&/V "array" (&/T (&type/Data$ ?class (&/|list)) (&/V &/$Nil nil))))))) (defn analyse-jvm-aastore [analyse ?array ?idx ?elem] @@ -313,11 +313,11 @@ =method-body (&/with-scope (str ?name "_" ?idx) (&/fold (fn [body* input*] (|let [[iname itype] input*] - (&&env/with-local iname (&/V &/$DataT (as-otype itype)) + (&&env/with-local iname (&type/Data$ (as-otype itype) (&/|list)) body*))) (if (= "void" ?method-output) (analyse-1+ analyse ?method-body) - (&&/analyse-1 analyse (&/V &/$DataT (as-otype ?method-output)) ?method-body)) + (&&/analyse-1 analyse (&type/Data$ (as-otype ?method-output) (&/|list)) ?method-body)) (&/|reverse (if (:static? =method-modifiers) =method-inputs (&/Cons$ (&/T ";this" ?super-class) @@ -360,7 +360,7 @@ (|do [:let [[?catches ?finally] ?catches+?finally] =body (&&/analyse-1 analyse exo-type ?body) =catches (&/map% (fn [[?ex-class ?ex-arg ?catch-body]] - (|do [=catch-body (&&env/with-local ?ex-arg (&/V &/$DataT ?ex-class) + (|do [=catch-body (&&env/with-local ?ex-arg (&type/Data$ ?ex-class (&/|list)) (&&/analyse-1 analyse exo-type ?catch-body)) idx &&env/next-local-idx] (return (&/T ?ex-class idx =catch-body)))) @@ -374,7 +374,7 @@ (defn analyse-jvm-throw [analyse exo-type ?ex] (|do [=ex (analyse-1+ analyse ?ex) :let [[_obj _type] =ex] - _ (&type/check (&/V &/$DataT "java.lang.Throwable") _type)] + _ (&type/check (&type/Data$ "java.lang.Throwable" (&/|list)) _type)] (return (&/|list (&/T (&/V &&/$jvm-throw =ex) &type/$Void))))) (do-template [<name> <tag>] @@ -390,9 +390,9 @@ ) (do-template [<name> <tag> <from-class> <to-class>] - (let [output-type (&/V &/$DataT <to-class>)] + (let [output-type (&type/Data$ <to-class> (&/|list))] (defn <name> [analyse exo-type ?value] - (|do [=value (&&/analyse-1 analyse (&/V &/$DataT <from-class>) ?value) + (|do [=value (&&/analyse-1 analyse (&type/Data$ <from-class> (&/|list)) ?value) _ (&type/check exo-type output-type)] (return (&/|list (&/T (&/V <tag> =value) output-type)))))) @@ -417,9 +417,9 @@ ) (do-template [<name> <tag> <from-class> <to-class>] - (let [output-type (&/V &/$DataT <to-class>)] + (let [output-type (&type/Data$ <to-class> (&/|list))] (defn <name> [analyse exo-type ?value] - (|do [=value (&&/analyse-1 analyse (&/V &/$DataT <from-class>) ?value) + (|do [=value (&&/analyse-1 analyse (&type/Data$ <from-class> (&/|list)) ?value) _ (&type/check exo-type output-type)] (return (&/|list (&/T (&/V <tag> =value) output-type)))))) diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj index b8239d1a9..6205adccb 100644 --- a/src/lux/analyser/lux.clj +++ b/src/lux/analyser/lux.clj @@ -364,7 +364,7 @@ (|do [;; :let [_ (prn 'MACRO-EXPAND|PRE (&/ident->text real-name))] macro-expansion #(-> macro (.apply ?args) (.apply %)) ;; :let [_ (prn 'MACRO-EXPAND|POST (&/ident->text real-name))] - ;; :let [_ (when (or (= "defsig" (aget real-name 1)) + ;; :let [_ (when (or (= "zip" (aget real-name 1)) ;; ;; (= "..?" (aget real-name 1)) ;; ;; (= "try$" (aget real-name 1)) ;; ) @@ -431,13 +431,9 @@ (|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)) + (|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* diff --git a/src/lux/compiler/host.clj b/src/lux/compiler/host.clj index 0529ac900..db54af8ac 100644 --- a/src/lux/compiler/host.clj +++ b/src/lux/compiler/host.clj @@ -52,31 +52,31 @@ (&/$TupleT (&/$Nil)) (.visitInsn *writer* Opcodes/ACONST_NULL) - (&/$DataT "boolean") + (&/$DataT "boolean" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class boolean-class) "valueOf" (str "(Z)" (&host/->type-signature boolean-class))) - (&/$DataT "byte") + (&/$DataT "byte" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class byte-class) "valueOf" (str "(B)" (&host/->type-signature byte-class))) - (&/$DataT "short") + (&/$DataT "short" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class short-class) "valueOf" (str "(S)" (&host/->type-signature short-class))) - (&/$DataT "int") + (&/$DataT "int" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class int-class) "valueOf" (str "(I)" (&host/->type-signature int-class))) - (&/$DataT "long") + (&/$DataT "long" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class long-class) "valueOf" (str "(J)" (&host/->type-signature long-class))) - (&/$DataT "float") + (&/$DataT "float" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class float-class) "valueOf" (str "(F)" (&host/->type-signature float-class))) - (&/$DataT "double") + (&/$DataT "double" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class double-class) "valueOf" (str "(D)" (&host/->type-signature double-class))) - (&/$DataT "char") + (&/$DataT "char" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class char-class) "valueOf" (str "(C)" (&host/->type-signature char-class))) - (&/$DataT _) + (&/$DataT _ (&/$Nil)) nil (&/$NamedT ?name ?type) diff --git a/src/lux/compiler/type.clj b/src/lux/compiler/type.clj index d75f6afef..6c128df80 100644 --- a/src/lux/compiler/type.clj +++ b/src/lux/compiler/type.clj @@ -39,48 +39,44 @@ "(-> Analysis Analysis Analysis)" (variant$ &/$Cons (tuple$ (&/|list head tail)))) +(defn ^:private List$ [elems] + (&/fold (fn [tail head] + (Cons$ head tail)) + $Nil + (&/|reverse elems))) + ;; [Exports] (defn ->analysis [type] "(-> Type Analysis)" (|case type - (&/$DataT ?class) - (variant$ &/$DataT (text$ ?class)) + (&/$DataT class params) + (variant$ &/$DataT (tuple$ (&/|list (text$ class) + (List$ (&/|map ->analysis params))))) - (&/$TupleT ?members) - (variant$ &/$TupleT - (&/fold (fn [tail head] - (Cons$ (->analysis head) tail)) - $Nil - (&/|reverse ?members))) - - (&/$VariantT ?members) - (variant$ &/$VariantT - (&/fold (fn [tail head] - (Cons$ (->analysis head) tail)) - $Nil - (&/|reverse ?members))) - - (&/$LambdaT ?input ?output) - (variant$ &/$LambdaT (tuple$ (&/|list (->analysis ?input) (->analysis ?output)))) - - (&/$UnivQ ?env ?body) + (&/$TupleT members) + (variant$ &/$TupleT (List$ (&/|map ->analysis members))) + + (&/$VariantT members) + (variant$ &/$VariantT (List$ (&/|map ->analysis members))) + + (&/$LambdaT input output) + (variant$ &/$LambdaT (tuple$ (&/|list (->analysis input) (->analysis output)))) + + (&/$UnivQ env body) (variant$ &/$UnivQ - (tuple$ (&/|list (&/fold (fn [tail head] - (Cons$ (->analysis head) tail)) - $Nil - (&/|reverse ?env)) - (->analysis ?body)))) + (tuple$ (&/|list (List$ (&/|map ->analysis env)) + (->analysis body)))) - (&/$BoundT ?idx) - (variant$ &/$BoundT (int$ ?idx)) + (&/$BoundT idx) + (variant$ &/$BoundT (int$ idx)) - (&/$AppT ?fun ?arg) - (variant$ &/$AppT (tuple$ (&/|list (->analysis ?fun) (->analysis ?arg)))) + (&/$AppT fun arg) + (variant$ &/$AppT (tuple$ (&/|list (->analysis fun) (->analysis arg)))) - (&/$NamedT [?module ?name] ?type) - (variant$ &/$NamedT (tuple$ (&/|list (tuple$ (&/|list (text$ ?module) (text$ ?name))) - (->analysis ?type)))) + (&/$NamedT [module name] type*) + (variant$ &/$NamedT (tuple$ (&/|list (tuple$ (&/|list (text$ module) (text$ name))) + (->analysis type*)))) _ - (assert false (&type/show-type type)) + (assert false (prn '->analysis (&type/show-type type) (&/adt->text type))) )) diff --git a/src/lux/host.clj b/src/lux/host.clj index 2290f2f0a..0936d90eb 100644 --- a/src/lux/host.clj +++ b/src/lux/host.clj @@ -29,8 +29,9 @@ (.getSimpleName class)))] (if (.equals "void" base) (return &type/Unit) - (return (&/V &/$DataT (str (reduce str "" (repeat (int (/ (count arr-level) 2)) "[")) - base))) + (return (&type/Data$ (str (reduce str "" (repeat (int (/ (count arr-level) 2)) "[")) + base) + (&/|list))) ))) (defn ^:private method->type [^Method method] @@ -70,7 +71,7 @@ (defn ->java-sig [^objects type] "(-> Type Text)" (|case type - (&/$DataT ?name) + (&/$DataT ?name params) (->type-signature ?name) (&/$LambdaT _ _) diff --git a/src/lux/type.clj b/src/lux/type.clj index 3b7349fca..0da579cf4 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -24,8 +24,8 @@ false)) (def ^:private empty-env (&/V &/$Nil nil)) -(defn Data$ [name] - (&/V &/$DataT name)) +(defn Data$ [name params] + (&/V &/$DataT (&/T name params))) (defn Bound$ [idx] (&/V &/$BoundT idx)) (defn Var$ [id] @@ -46,13 +46,13 @@ (&/V &/$NamedT (&/T name type))) -(def Bool (Named$ (&/T "lux" "Bool") (&/V &/$DataT "java.lang.Boolean"))) -(def Int (Named$ (&/T "lux" "Int") (&/V &/$DataT "java.lang.Long"))) -(def Real (Named$ (&/T "lux" "Real") (&/V &/$DataT "java.lang.Double"))) -(def Char (Named$ (&/T "lux" "Char") (&/V &/$DataT "java.lang.Character"))) -(def Text (Named$ (&/T "lux" "Text") (&/V &/$DataT "java.lang.String"))) -(def Unit (Named$ (&/T "lux" "Unit") (&/V &/$TupleT (&/|list)))) -(def $Void (Named$ (&/T "lux" "Void") (&/V &/$VariantT (&/|list)))) +(def Bool (Named$ (&/T "lux" "Bool") (Data$ "java.lang.Boolean" (&/|list)))) +(def Int (Named$ (&/T "lux" "Int") (Data$ "java.lang.Long" (&/|list)))) +(def Real (Named$ (&/T "lux" "Real") (Data$ "java.lang.Double" (&/|list)))) +(def Char (Named$ (&/T "lux" "Char") (Data$ "java.lang.Character" (&/|list)))) +(def Text (Named$ (&/T "lux" "Text") (Data$ "java.lang.String" (&/|list)))) +(def Unit (Named$ (&/T "lux" "Unit") (Tuple$ (&/|list)))) +(def $Void (Named$ (&/T "lux" "Void") (Variant$ (&/|list)))) (def Ident (Named$ (&/T "lux" "Ident") (Tuple$ (&/|list Text Text)))) (def IO @@ -90,7 +90,7 @@ (App$ (Univ$ empty-env (Variant$ (&/|list ;; DataT - Text + (Tuple$ (&/|list Text TypeList)) ;; VariantT TypeList ;; TupleT @@ -221,11 +221,11 @@ (Tuple$ (&/|list ;; "lux;writer" - (Data$ "org.objectweb.asm.ClassWriter") + (Data$ "org.objectweb.asm.ClassWriter" (&/|list)) ;; "lux;loader" - (Data$ "java.lang.ClassLoader") + (Data$ "java.lang.ClassLoader" (&/|list)) ;; "lux;classes" - (Data$ "clojure.lang.Atom"))))) + (Data$ "clojure.lang.Atom" (&/|list)))))) (def DefData* (Univ$ empty-env @@ -405,9 +405,7 @@ )))) (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings)))] (fn [state] - (return* (&/update$ &/$type-vars #(->> % - ;; (&/update$ &/$counter dec) - (&/set$ &/$mappings (&/|remove id mappings*))) + (return* (&/update$ &/$type-vars #(&/set$ &/$mappings (&/|remove id mappings*) %) state) nil))) state)))) @@ -418,12 +416,6 @@ _ (delete-var id)] (return output))) -(defn with-vars [amount k] - (|do [=vars (&/map% (constantly create-var) (&/|range amount)) - output (k (&/|map #(Var$ %) =vars)) - _ (&/map% delete-var (&/|reverse =vars))] - (return output))) - (defn clean* [?tid type] (|case type (&/$VarT ?id) @@ -486,8 +478,13 @@ (defn show-type [^objects type] (|case type - (&/$DataT name) - (str "(^ " name ")") + (&/$DataT name params) + (|case params + (&/$Nil) + (str "(^ " name ")") + + _ + (str "(^ " name " " (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")) (&/$TupleT elems) (if (&/|empty? elems) @@ -535,8 +532,10 @@ (and (= ?xmodule ?ymodule) (= ?xname ?yname)) - [(&/$DataT xname) (&/$DataT yname)] - (.equals ^Object xname yname) + [(&/$DataT xname xparams) (&/$DataT yname yparams)] + (and (.equals ^Object xname yname) + (= (&/|length xparams) (&/|length yparams)) + (&/fold2 #(and %1 (type= %2 %3)) true xparams yparams)) [(&/$TupleT xelems) (&/$TupleT yelems)] (&/fold2 (fn [old x y] (and old (type= x y))) @@ -677,7 +676,7 @@ (def ^:private init-fixpoints (&/|list)) -(defn ^:private check* [class-loader fixpoints expected actual] +(defn ^:private check* [class-loader fixpoints invariant?? expected actual] (if (clojure.lang.Util/identical expected actual) (return (&/T fixpoints nil)) (|case [expected actual] @@ -704,13 +703,13 @@ (return (&/T fixpoints nil))) [(&/$Some etype) (&/$None _)] - (check* class-loader fixpoints etype actual) + (check* class-loader fixpoints invariant?? etype actual) [(&/$None _) (&/$Some atype)] - (check* class-loader fixpoints expected atype) + (check* class-loader fixpoints invariant?? expected atype) [(&/$Some etype) (&/$Some atype)] - (check* class-loader fixpoints etype atype)))) + (check* class-loader fixpoints invariant?? etype atype)))) [(&/$VarT ?id) _] (fn [state] @@ -720,7 +719,7 @@ (&/$Left _) ((|do [bound (deref ?id)] - (check* class-loader fixpoints bound actual)) + (check* class-loader fixpoints invariant?? bound actual)) state))) [_ (&/$VarT ?id)] @@ -731,12 +730,12 @@ (&/$Left _) ((|do [bound (deref ?id)] - (check* class-loader fixpoints expected bound)) + (check* class-loader fixpoints invariant?? expected bound)) state))) [(&/$AppT (&/$ExT eid) eA) (&/$AppT (&/$ExT aid) aA)] (if (= eid aid) - (check* class-loader fixpoints eA aA) + (check* class-loader fixpoints invariant?? eA aA) (fail (check-error expected actual))) ;; [(&/$AppT (&/$VarT ?eid) A1) (&/$AppT (&/$VarT ?aid) A2)] @@ -744,13 +743,13 @@ ;; (|case ((|do [F1 (deref ?eid)] ;; (fn [state] ;; (|case ((|do [F2 (deref ?aid)] - ;; (check* class-loader fixpoints (App$ F1 A1) (App$ F2 A2))) + ;; (check* class-loader fixpoints invariant?? (App$ F1 A1) (App$ F2 A2))) ;; state) ;; (&/$Right state* output) ;; (return* state* output) ;; (&/$Left _) - ;; ((check* class-loader fixpoints (App$ F1 A1) actual) + ;; ((check* class-loader fixpoints invariant?? (App$ F1 A1) actual) ;; state)))) ;; state) ;; (&/$Right state* output) @@ -758,70 +757,70 @@ ;; (&/$Left _) ;; (|case ((|do [F2 (deref ?aid)] - ;; (check* class-loader fixpoints expected (App$ F2 A2))) + ;; (check* class-loader fixpoints invariant?? expected (App$ F2 A2))) ;; state) ;; (&/$Right state* output) ;; (return* state* output) ;; (&/$Left _) - ;; ((|do [[fixpoints* _] (check* class-loader fixpoints (Var$ ?eid) (Var$ ?aid)) - ;; [fixpoints** _] (check* class-loader fixpoints* A1 A2)] + ;; ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (Var$ ?eid) (Var$ ?aid)) + ;; [fixpoints** _] (check* class-loader fixpoints* invariant?? A1 A2)] ;; (return (&/T fixpoints** nil))) ;; state)))) - ;; (|do [_ (check* class-loader fixpoints (Var$ ?eid) (Var$ ?aid)) - ;; _ (check* class-loader fixpoints A1 A2)] + ;; (|do [_ (check* class-loader fixpoints invariant?? (Var$ ?eid) (Var$ ?aid)) + ;; _ (check* class-loader fixpoints invariant?? A1 A2)] ;; (return (&/T fixpoints nil))) [(&/$AppT (&/$VarT ?id) A1) (&/$AppT F2 A2)] (fn [state] (|case ((|do [F1 (deref ?id)] - (check* class-loader fixpoints (App$ F1 A1) actual)) + (check* class-loader fixpoints invariant?? (App$ F1 A1) actual)) state) (&/$Right state* output) (return* state* output) (&/$Left _) - ((|do [[fixpoints* _] (check* class-loader fixpoints (Var$ ?id) F2) + ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (Var$ ?id) F2) e* (apply-type F2 A1) a* (apply-type F2 A2) - [fixpoints** _] (check* class-loader fixpoints* e* a*)] + [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)] (return (&/T fixpoints** nil))) state))) ;; [[&/$AppT [[&/$VarT ?id] A1]] [&/$AppT [F2 A2]]] - ;; (|do [[fixpoints* _] (check* class-loader fixpoints (Var$ ?id) F2) + ;; (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (Var$ ?id) F2) ;; e* (apply-type F2 A1) ;; a* (apply-type F2 A2) - ;; [fixpoints** _] (check* class-loader fixpoints* e* a*)] + ;; [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)] ;; (return (&/T fixpoints** nil))) [(&/$AppT F1 A1) (&/$AppT (&/$VarT ?id) A2)] (fn [state] (|case ((|do [F2 (deref ?id)] - (check* class-loader fixpoints expected (App$ F2 A2))) + (check* class-loader fixpoints invariant?? expected (App$ F2 A2))) state) (&/$Right state* output) (return* state* output) (&/$Left _) - ((|do [[fixpoints* _] (check* class-loader fixpoints F1 (Var$ ?id)) + ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? F1 (Var$ ?id)) e* (apply-type F1 A1) a* (apply-type F1 A2) - [fixpoints** _] (check* class-loader fixpoints* e* a*)] + [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)] (return (&/T fixpoints** nil))) state))) ;; [[&/$AppT [F1 A1]] [&/$AppT [[&/$VarT ?id] A2]]] - ;; (|do [[fixpoints* _] (check* class-loader fixpoints F1 (Var$ ?id)) + ;; (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? F1 (Var$ ?id)) ;; e* (apply-type F1 A1) ;; a* (apply-type F1 A2) - ;; [fixpoints** _] (check* class-loader fixpoints* e* a*)] + ;; [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)] ;; (return (&/T fixpoints** nil))) ;; [(&/$AppT eF eA) (&/$AppT aF aA)] - ;; (|do [_ (check* class-loader fixpoints eF aF)] - ;; (check* class-loader fixpoints eA aA)) + ;; (|do [_ (check* class-loader fixpoints invariant?? eF aF)] + ;; (check* class-loader fixpoints invariant?? eA aA)) [(&/$AppT F A) _] (let [fp-pair (&/T expected actual) @@ -842,44 +841,51 @@ (&/$None) (|do [expected* (apply-type F A)] - (check* class-loader (fp-put fp-pair true fixpoints) expected* actual)))) + (check* class-loader (fp-put fp-pair true fixpoints) invariant?? expected* actual)))) [_ (&/$AppT F A)] (|do [actual* (apply-type F A)] - (check* class-loader fixpoints expected actual*)) + (check* class-loader fixpoints invariant?? expected actual*)) [(&/$UnivQ _) _] (with-var (fn [$arg] (|do [expected* (apply-type expected $arg)] - (check* class-loader fixpoints expected* actual)))) + (check* class-loader fixpoints invariant?? expected* actual)))) [_ (&/$UnivQ _)] (with-var (fn [$arg] (|do [actual* (apply-type actual $arg)] - (check* class-loader fixpoints expected actual*)))) + (check* class-loader fixpoints invariant?? expected actual*)))) - [(&/$DataT e!name) (&/$DataT "null")] + [(&/$DataT e!name e!params) (&/$DataT "null" (&/$Nil))] (if (contains? primitive-types e!name) (fail (str "[Type Error] Can't use \"null\" with primitive types.")) (return (&/T fixpoints nil))) - [(&/$DataT e!name) (&/$DataT a!name)] + [(&/$DataT e!name e!params) (&/$DataT a!name a!params)] (let [e!name (as-obj e!name) a!name (as-obj a!name)] - (if (or (.equals ^Object e!name a!name) - (.isAssignableFrom (Class/forName e!name true class-loader) (Class/forName a!name true class-loader))) - (return (&/T fixpoints nil)) - (fail (str "[Type Error] Names don't match: " e!name " =/= " a!name)))) + (cond (and (.equals ^Object e!name a!name) + (= (&/|length e!params) (&/|length a!params))) + (|do [_ (&/map2% (partial check* class-loader fixpoints true) e!params a!params)] + (return (&/T fixpoints nil))) + + (and (not invariant??) + (.isAssignableFrom (Class/forName e!name true class-loader) (Class/forName a!name true class-loader))) + (return (&/T fixpoints nil)) + + :else + (fail (str "[Type Error] Names don't match: " e!name " =/= " a!name)))) [(&/$LambdaT eI eO) (&/$LambdaT aI aO)] - (|do [[fixpoints* _] (check* class-loader fixpoints aI eI)] - (check* class-loader fixpoints* eO aO)) + (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? aI eI)] + (check* class-loader fixpoints* invariant?? eO aO)) [(&/$TupleT e!members) (&/$TupleT a!members)] (|do [fixpoints* (&/fold2% (fn [fp e a] - (|do [[fp* _] (check* class-loader fp e a)] + (|do [[fp* _] (check* class-loader fp invariant?? e a)] (return fp*))) fixpoints e!members a!members)] @@ -887,7 +893,7 @@ [(&/$VariantT e!cases) (&/$VariantT a!cases)] (|do [fixpoints* (&/fold2% (fn [fp e a] - (|do [[fp* _] (check* class-loader fp e a)] + (|do [[fp* _] (check* class-loader fp invariant?? e a)] (return fp*))) fixpoints e!cases a!cases)] @@ -899,10 +905,10 @@ (fail (check-error expected actual))) [(&/$NamedT ?ename ?etype) _] - (check* class-loader fixpoints ?etype actual) + (check* class-loader fixpoints invariant?? ?etype actual) [_ (&/$NamedT ?aname ?atype)] - (check* class-loader fixpoints expected ?atype) + (check* class-loader fixpoints invariant?? expected ?atype) [_ _] (fail (check-error expected actual)) @@ -910,29 +916,9 @@ (defn check [expected actual] (|do [class-loader &/loader - _ (check* class-loader init-fixpoints expected actual)] + _ (check* class-loader init-fixpoints false expected actual)] (return nil))) -(defn apply-lambda [func param] - (|case func - (&/$LambdaT input output) - (|do [_ (check* init-fixpoints input param)] - (return output)) - - (&/$UnivQ _) - (with-var - (fn [$var] - (|do [func* (apply-type func $var) - =return (apply-lambda func* param)] - (clean $var =return)))) - - (&/$NamedT ?name ?type) - (apply-lambda ?type param) - - _ - (fail (str "[Type System] Not a function type:\n" (show-type func) "\n")) - )) - (defn actual-type [type] "(-> Type (Lux Type))" (|case type |