aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--source/lux.lux43
-rw-r--r--source/lux/data/list.lux3
-rw-r--r--source/lux/meta/ast.lux4
-rw-r--r--source/lux/meta/type.lux24
-rw-r--r--src/lux/analyser/host.clj48
-rw-r--r--src/lux/analyser/lux.clj12
-rw-r--r--src/lux/compiler/host.clj18
-rw-r--r--src/lux/compiler/type.clj62
-rw-r--r--src/lux/host.clj7
-rw-r--r--src/lux/type.clj164
10 files changed, 190 insertions, 195 deletions
diff --git a/source/lux.lux b/source/lux.lux
index f5cc8d3d1..39cbb7765 100644
--- a/source/lux.lux
+++ b/source/lux.lux
@@ -9,23 +9,23 @@
## Basic types
(_lux_def Bool (10 ["lux" "Bool"]
- (0 "java.lang.Boolean")))
+ (0 "java.lang.Boolean" (0))))
(_lux_export Bool)
(_lux_def Int (10 ["lux" "Int"]
- (0 "java.lang.Long")))
+ (0 "java.lang.Long" (0))))
(_lux_export Int)
(_lux_def Real (10 ["lux" "Real"]
- (0 "java.lang.Double")))
+ (0 "java.lang.Double" (0))))
(_lux_export Real)
(_lux_def Char (10 ["lux" "Char"]
- (0 "java.lang.Character")))
+ (0 "java.lang.Character" (0))))
(_lux_export Char)
(_lux_def Text (10 ["lux" "Text"]
- (0 "java.lang.String")))
+ (0 "java.lang.String" (0))))
(_lux_export Text)
(_lux_def Unit (10 ["lux" "Unit"]
@@ -71,7 +71,7 @@
(_lux_declare-tags [#None #Some] Maybe)
## (deftype #rec Type
-## (| (#DataT Text)
+## (| (#DataT (, Text (List Type)))
## (#VariantT (List Type))
## (#TupleT (List Type))
## (#LambdaT Type Type)
@@ -90,7 +90,7 @@
TypeList
(9 (7 (0)
(1 (1 ## "lux;DataT"
- Text
+ (2 (1 Text (1 TypeList (0))))
(1 ## "lux;VariantT"
TypeList
(1 ## "lux;TupleT"
@@ -279,11 +279,11 @@
(_lux_def Host
(#NamedT ["lux" "Host"]
(#TupleT (#Cons [## "lux;writer"
- (#DataT "org.objectweb.asm.ClassWriter")
+ (#DataT "org.objectweb.asm.ClassWriter" #Nil)
(#Cons [## "lux;loader"
- (#DataT "java.lang.ClassLoader")
+ (#DataT "java.lang.ClassLoader" #Nil)
(#Cons [## "lux;classes"
- (#DataT "clojure.lang.Atom")
+ (#DataT "clojure.lang.Atom" #Nil)
#Nil])])]))))
(_lux_declare-tags [#writer #loader #classes] Host)
@@ -912,14 +912,6 @@
_
(fail "Wrong syntax for @list&")))
-(defmacro' #export (^ tokens)
- (_lux_case tokens
- (#Cons [_ (#SymbolS "" class-name)] #Nil)
- (return (@list (form$ (@list (tag$ ["lux" "DataT"]) (text$ class-name)))))
-
- _
- (fail "Wrong syntax for ^")))
-
(defmacro' #export (, tokens)
(return (@list (form$ (@list (tag$ ["lux" "TupleT"])
(foldL (lambda'' [tail head] (form$ (@list (tag$ ["lux" "Cons"]) head tail)))
@@ -1352,6 +1344,17 @@
(wrap (wrap-meta (form$ (@list (tag$ ["lux" "RecordS"]) (untemplate-list =fields))))))
))
+(defmacro' #export (^ tokens)
+ (_lux_case tokens
+ (#Cons [_ (#SymbolS "" class-name)] #Nil)
+ (return (@list (form$ (@list (tag$ ["lux" "DataT"]) (text$ class-name) (tag$ ["lux" "Nil"])))))
+
+ (#Cons [_ (#SymbolS "" class-name)] params)
+ (return (@list (form$ (@list (tag$ ["lux" "DataT"]) (text$ class-name) (untemplate-list params)))))
+
+ _
+ (fail "Wrong syntax for ^")))
+
(def'' (get-module-name state)
($' Lux Text)
(_lux_case state
@@ -3192,8 +3195,8 @@
(def (type->ast type)
(-> Type AST)
(case type
- (#DataT name)
- (` (#DataT (~ (text$ name))))
+ (#DataT name params)
+ (` (#DataT (~ (text$ name)) (~ (untemplate-list (map type->ast params)))))
(#;VariantT cases)
(` (#VariantT (~ (untemplate-list (map type->ast cases)))))
diff --git a/source/lux/data/list.lux b/source/lux/data/list.lux
index 54f8fed4c..e538007bf 100644
--- a/source/lux/data/list.lux
+++ b/source/lux/data/list.lux
@@ -333,3 +333,6 @@
_
(#;Left "Wrong syntax for zip")))
+
+(def #export zip2 (zip 2))
+(def #export zip3 (zip 3))
diff --git a/source/lux/meta/ast.lux b/source/lux/meta/ast.lux
index 398acf6cc..6d9271847 100644
--- a/source/lux/meta/ast.lux
+++ b/source/lux/meta/ast.lux
@@ -99,7 +99,7 @@
(foldL (lambda [old [x' y']]
(and old (= x' y')))
true
- ((zip 2) xs' ys')))])
+ (zip2 xs' ys')))])
[[#;FormS] [#;TupleS]]
[[_ (#;RecordS xs')] [_ (#;RecordS ys')]]
@@ -107,7 +107,7 @@
(foldL (lambda [old [[xl' xr'] [yl' yr']]]
(and old (= xl' yl') (= xr' yr')))
true
- ((zip 2) xs' ys')))
+ (zip2 xs' ys')))
_
false)))
diff --git a/source/lux/meta/type.lux b/source/lux/meta/type.lux
index 4147e37d4..a1c34b1ac 100644
--- a/source/lux/meta/type.lux
+++ b/source/lux/meta/type.lux
@@ -10,7 +10,7 @@
(data (text #open ("text:" Text/Monoid Text/Eq))
(number/int #open ("int:" Int/Eq Int/Show))
maybe
- (list #refer #all #open ("list:" List/Monad)))
+ (list #refer #all #open ("list:" List/Monad List/Fold)))
))
(open List/Fold)
@@ -19,8 +19,13 @@
(defstruct #export Type/Show (Show Type)
(def (show type)
(case type
- (#;DataT name)
- ($ text:++ "(^ " name ")")
+ (#;DataT name params)
+ (case params
+ #;Nil
+ ($ text:++ "(^ " name ")")
+
+ _
+ ($ text:++ "(^ " name " " (|> params (list:map show) (interpose " ") (list:foldL text:++ "")) ")"))
(#;TupleT members)
(case members
@@ -66,8 +71,13 @@
(defstruct #export Type/Eq (Eq Type)
(def (= x y)
(case [x y]
- [(#;DataT xname) (#;DataT yname)]
- (text:= xname yname)
+ [(#;DataT xname xparams) (#;DataT yname yparams)]
+ (and (text:= xname yname)
+ (int:= (size xparams) (size yparams))
+ (foldL (lambda [prev [x y]]
+ (and prev (= x y)))
+ true
+ (zip2 xparams yparams)))
(\or [(#;VarT xid) (#;VarT yid)]
[(#;ExT xid) (#;ExT yid)]
@@ -90,7 +100,7 @@
(foldL (lambda [prev [x y]]
(and prev (= x y)))
true
- ((zip 2) xmembers ymembers)))
+ (zip2 xmembers ymembers)))
(\or [(#;UnivQ xenv xbody) (#;UnivQ yenv ybody)]
[(#;ExQ xenv xbody) (#;ExQ yenv ybody)])
@@ -98,7 +108,7 @@
(foldL (lambda [prev [x y]]
(and prev (= x y)))
(= xbody ybody)
- ((zip 2) xenv yenv)))
+ (zip2 xenv yenv)))
_
false
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