aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lux.clj1
-rw-r--r--src/lux/analyser.clj44
-rw-r--r--src/lux/analyser/host.clj30
-rw-r--r--src/lux/analyser/lux.clj63
-rw-r--r--src/lux/base.clj14
-rw-r--r--src/lux/compiler.clj11
-rw-r--r--src/lux/compiler/host.clj12
-rw-r--r--src/lux/compiler/lambda.clj2
-rw-r--r--src/lux/compiler/lux.clj93
-rw-r--r--src/lux/host.clj14
-rw-r--r--src/lux/type.clj598
11 files changed, 482 insertions, 400 deletions
diff --git a/src/lux.clj b/src/lux.clj
index 6d79b52bf..7bee8df16 100644
--- a/src/lux.clj
+++ b/src/lux.clj
@@ -15,6 +15,7 @@
;; Finish total-locals
(time (&compiler/compile-all (&/|list "lux")))
+ (System/gc)
(time (&compiler/compile-all (&/|list "lux" "test2")))
;; jar cvf test2.jar *.class test2 && java -cp "test2.jar" test2
diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index e73423ffc..9ed75b83d 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -35,19 +35,19 @@
(matchv ::M/objects [token]
;; Standard special forms
[["lux;Meta" [meta ["lux;Bool" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) (&/V "lux;TData" (&/T "java.lang.Boolean" (&/V "lux;Nil" nil)))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) (&/V "lux;DataT" (&/T "java.lang.Boolean" (&/V "lux;Nil" nil)))))))
[["lux;Meta" [meta ["lux;Int" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value) (&/V "lux;TData" (&/T "java.lang.Long" (&/V "lux;Nil" nil)))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value) (&/V "lux;DataT" (&/T "java.lang.Long" (&/V "lux;Nil" nil)))))))
[["lux;Meta" [meta ["lux;Real" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) (&/V "lux;TData" (&/T "java.lang.Double" (&/V "lux;Nil" nil)))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) (&/V "lux;DataT" (&/T "java.lang.Double" (&/V "lux;Nil" nil)))))))
[["lux;Meta" [meta ["lux;Char" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) (&/V "lux;TData" (&/T "java.lang.Character" (&/V "lux;Nil" nil)))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) (&/V "lux;DataT" (&/T "java.lang.Character" (&/V "lux;Nil" nil)))))))
[["lux;Meta" [meta ["lux;Text" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) (&/V "lux;TData" (&/T "java.lang.String" (&/V "lux;Nil" nil)))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) (&/V "lux;DataT" (&/T "java.lang.String" (&/V "lux;Nil" nil)))))))
[["lux;Meta" [meta ["lux;Tuple" ?elems]]]]
(&&lux/analyse-tuple analyse ?elems)
@@ -56,13 +56,13 @@
(&&lux/analyse-record analyse ?elems)
[["lux;Meta" [meta ["lux;Tag" [?module ?name]]]]]
- (let [tuple-type (&/V "lux;Tuple" (&/V "lux;Nil" nil))
+ (let [tuple-type (&/V "lux;TupleT" (&/V "lux;Nil" nil))
?tag (str ?module ";" ?name)]
(return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag (&/V "Expression" (&/T (&/V "tuple" (&/|list)) tuple-type))))
- (&/V "lux;TVariant" (&/V "lux;Cons" (&/T (&/T ?tag tuple-type) (&/V "lux;Nil" nil)))))))))
+ (&/V "lux;VariantT" (&/V "lux;Cons" (&/T (&/T ?tag tuple-type) (&/V "lux;Nil" nil)))))))))
[["lux;Meta" [meta ["lux;Symbol" [_ "jvm-null"]]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null" nil) (&/V "lux;TData" (&/T "null" (&/V "lux;Nil" nil)))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null" nil) (&/V "lux;DataT" (&/T "null" (&/V "lux;Nil" nil)))))))
[["lux;Meta" [meta ["lux;Symbol" ?ident]]]]
(&&lux/analyse-ident analyse ?ident)
@@ -78,18 +78,6 @@
["lux;Nil" _]]]]]]]]]]]]]
(&&lux/analyse-lambda analyse ?self ?arg ?body)
- [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "get@'"]]]]
- ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" ?slot]]]
- ["lux;Cons" [?record ["lux;Nil" _]]]]]]]]]]]
- (&&lux/analyse-get analyse ?slot ?record)
-
- [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "set@'"]]]]
- ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" ?slot]]]
- ["lux;Cons" [?value
- ["lux;Cons" [?record
- ["lux;Nil" _]]]]]]]]]]]]]
- (&&lux/analyse-set analyse ?slot ?value ?record)
-
[["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "def'"]]]]
["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ ?name]]]]
["lux;Cons" [?value
@@ -98,7 +86,7 @@
;; (prn "if" (&/show-ast ?value)))
(&&lux/analyse-def analyse ?name ?value))
- [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "declare-macro"]]]]
+ [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "declare-macro'"]]]]
["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" ?ident]]]
["lux;Nil" _]]]]]]]]]
(&&lux/analyse-declare-macro ?ident)
@@ -108,23 +96,19 @@
["lux;Nil" _]]]]]]]]]
(&&lux/analyse-import analyse ?path)
- [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ ":"]]]]
- ["lux;Cons" [?value
- ["lux;Cons" [?type
+ [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "check'"]]]]
+ ["lux;Cons" [?type
+ ["lux;Cons" [?value
["lux;Nil" _]]]]]]]]]]]
(&&lux/analyse-check analyse eval! ?type ?value)
- [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "coerce"]]]]
+ [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "coerce'"]]]]
["lux;Cons" [?type
["lux;Cons" [?value
["lux;Nil" _]]]]]]]]]]]
(&&lux/analyse-coerce analyse eval! ?type ?value)
;; Host special forms
- [["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "exec"]]]]
- ?exprs]]]]]]
- (&&host/analyse-exec analyse ?exprs)
-
;; Integer arithmetic
[["lux;Meta" [meta ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Symbol" [_ "jvm-iadd"]]]] ["lux;Cons" [?y ["lux;Cons" [?x ["lux;Nil" _]]]]]]]]]]]
(&&host/analyse-jvm-iadd analyse ?x ?y)
@@ -448,7 +432,7 @@
;; :let [_ (prn 'POST-ASSERT)]
=value (&&/analyse-1 (analyse-ast eval!) (&/|head ?values))
=value-type (&&/expr-type =value)]
- (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value)) (&/V "lux;TVariant" (&/V "lux;Cons" (&/T (&/T ?tag =value-type) (&/V "lux;Nil" nil)))))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "variant" (&/T ?tag =value)) (&/V "lux;VariantT" (&/V "lux;Cons" (&/T (&/T ?tag =value-type) (&/V "lux;Nil" nil)))))))))
[["lux;Meta" [meta ["lux;Form" ["lux;Cons" [?fn ?args]]]]]]
(fn [state]
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index b8963f73f..cfc79c0b3 100644
--- a/src/lux/analyser/host.clj
+++ b/src/lux/analyser/host.clj
@@ -20,8 +20,8 @@
;; [Resources]
(do-template [<name> <output-tag> <input-class> <output-class>]
- (let [input-type (&/V "lux;TData" (to-array [<input-class> (&/V "lux;Nil" nil)]))
- output-type (&/V "lux;TData" (to-array [<output-class> (&/V "lux;Nil" nil)]))]
+ (let [input-type (&/V "lux;DataT" (to-array [<input-class> (&/V "lux;Nil" nil)]))
+ output-type (&/V "lux;DataT" (to-array [<output-class> (&/V "lux;Nil" nil)]))]
(defn <name> [analyse ?x ?y]
(exec [[=x =y] (&&/analyse-2 analyse ?x ?y)
=x-type (&&/expr-type =x)
@@ -126,17 +126,17 @@
(defn analyse-jvm-null? [analyse ?object]
(exec [=object (&&/analyse-1 analyse ?object)]
- (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null?" =object) (&/V "lux;TData" (&/T "java.lang.Boolean" (&/V "lux;Nil" nil)))))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "jvm-null?" =object) (&/V "lux;DataT" (&/T "java.lang.Boolean" (&/V "lux;Nil" nil)))))))))
(defn analyse-jvm-new [analyse ?class ?classes ?args]
(exec [=class (&host/full-class-name ?class)
=classes (&/map% &host/extract-jvm-param ?classes)
=args (&/flat-map% analyse ?args)]
- (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new" (&/T =class =classes =args)) (&/V "lux;TData" (&/T =class (&/V "lux;Nil" nil)))))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new" (&/T =class =classes =args)) (&/V "lux;DataT" (&/T =class (&/V "lux;Nil" nil)))))))))
(defn analyse-jvm-new-array [analyse ?class ?length]
(exec [=class (&host/full-class-name ?class)]
- (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new-array" (&/T =class ?length)) (&/V "array" (&/T (&/V "lux;TData" (to-array [=class (&/V "lux;Nil" nil)]))
+ (return (&/|list (&/V "Expression" (&/T (&/V "jvm-new-array" (&/T =class ?length)) (&/V "array" (&/T (&/V "lux;DataT" (to-array [=class (&/V "lux;Nil" nil)]))
(&/V "lux;Nil" nil)))))))))
(defn analyse-jvm-aastore [analyse ?array ?idx ?elem]
@@ -195,16 +195,10 @@
$module &/get-module-name]
(return (&/|list (&/V "Statement" (&/V "jvm-interface" (&/T $module ?name =methods)))))))
-(defn analyse-exec [analyse ?exprs]
- (exec [_ (&/assert! (count ?exprs) "\"exec\" expressions can't have empty bodies.")
- =exprs (&/flat-map% analyse ?exprs)
- =exprs-types (&/map% &&/expr-type =exprs)]
- (return (&/|list (&/V "Expression" (&/T (&/V "exec" =exprs) (&/|head (&/|reverse =exprs-types))))))))
-
(defn analyse-jvm-try [analyse ?body [?catches ?finally]]
(exec [=body (&&/analyse-1 analyse ?body)
=catches (&/map% (fn [[?ex-class ?ex-arg ?catch-body]]
- (&&env/with-local ?ex-arg (&/V "lux;TData" (&/T ?ex-class (&/V "lux;Nil" nil)))
+ (&&env/with-local ?ex-arg (&/V "lux;DataT" (&/T ?ex-class (&/V "lux;Nil" nil)))
(exec [=catch-body (&&/analyse-1 analyse ?catch-body)]
(return [?ex-class ?ex-arg =catch-body]))))
?catches)
@@ -214,20 +208,20 @@
(defn analyse-jvm-throw [analyse ?ex]
(exec [=ex (&&/analyse-1 analyse ?ex)]
- (return (&/|list (&/V "Expression" (&/T (&/V "jvm-throw" =ex) (&/V "lux;TNothing" nil)))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "jvm-throw" =ex) (&/V "lux;NothingT" nil)))))))
(defn analyse-jvm-monitorenter [analyse ?monitor]
(exec [=monitor (&&/analyse-1 analyse ?monitor)]
- (return (&/|list (&/V "Expression" (&/T (&/V "jvm-monitorenter" =monitor) (&/V "lux;TTuple" (&/V "lux;Nil" nil))))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "jvm-monitorenter" =monitor) (&/V "lux;TupleT" (&/V "lux;Nil" nil))))))))
(defn analyse-jvm-monitorexit [analyse ?monitor]
(exec [=monitor (&&/analyse-1 analyse ?monitor)]
- (return (&/|list (&/V "Expression" (&/T (&/V "jvm-monitorexit" =monitor) (&/V "lux;TTuple" (&/V "lux;Nil" nil))))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "jvm-monitorexit" =monitor) (&/V "lux;TupleT" (&/V "lux;Nil" nil))))))))
(do-template [<name> <tag> <from-class> <to-class>]
(defn <name> [analyse ?value]
(exec [=value (&&/analyse-1 analyse ?value)]
- (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;TData" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;DataT" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
analyse-jvm-d2f "jvm-d2f" "java.lang.Double" "java.lang.Float"
analyse-jvm-d2i "jvm-d2i" "java.lang.Double" "java.lang.Integer"
@@ -252,7 +246,7 @@
(do-template [<name> <tag> <from-class> <to-class>]
(defn <name> [analyse ?value]
(exec [=value (&&/analyse-1 analyse ?value)]
- (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;TData" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V <tag> =value) (&/V "lux;DataT" (&/T <to-class> (&/V "lux;Nil" nil)))))))))
analyse-jvm-iand "jvm-iand" "java.lang.Integer" "java.lang.Integer"
analyse-jvm-ior "jvm-ior" "java.lang.Integer" "java.lang.Integer"
@@ -267,6 +261,6 @@
)
(defn analyse-jvm-program [analyse ?args ?body]
- (exec [=body (&&env/with-local ?args (&/V "lux;TAny" nil)
+ (exec [=body (&&env/with-local ?args (&/V "lux;AnyT" nil)
(&&/analyse-1 analyse ?body))]
(return (&/|list (&/V "Statement" (&/V "jvm-program" =body))))))
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index e6dd0d1d0..aa205bf06 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -19,7 +19,7 @@
=elems-types (&/map% &&/expr-type =elems)
;; :let [_ (prn 'analyse-tuple =elems)]
]
- (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems) (&/V "lux;TTuple" =elems-types)))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "tuple" =elems) (&/V "lux;TupleT" =elems-types)))))))
(defn analyse-record [analyse ?elems]
(exec [=elems (&/map% (fn [kv]
@@ -36,7 +36,7 @@
=elems)
;; :let [_ (prn 'analyse-tuple =elems)]
]
- (return (&/|list (&/V "Expression" (&/T (&/V "lux;record" =elems) (&/V "lux;TRecord" =elems-types)))))))
+ (return (&/|list (&/V "Expression" (&/T (&/V "lux;record" =elems) (&/V "lux;RecordT" =elems-types)))))))
(defn ^:private resolve-global [ident state]
(|let [[?module ?name] ident
@@ -160,7 +160,7 @@
;; :let [_ (prn '=bodies =bodies)]
;; :let [_ (prn 'analyse-case/=bodies =bodies)]
=body-types (&/map% &&/expr-type =bodies)
- =case-type (&/fold% &type/merge (&/V "lux;TNothing" nil) =body-types)
+ =case-type (&/fold% &type/merge (&/V "lux;NothingT" nil) =body-types)
:let [=branches (&/zip2 (&/|map &/|first branches) =bodies)]]
(return (&/|list (&/V "Expression" (&/T (&/V "case" (&/T =value base-register max-locals =branches))
=case-type))))))
@@ -169,39 +169,36 @@
;; (prn 'analyse-lambda ?self ?arg ?body)
(exec [=lambda-type* &type/fresh-lambda]
(matchv ::M/objects [=lambda-type*]
- [["lux;TLambda" [=arg =return]]]
+ [["lux;LambdaT" [=arg =return]]]
(exec [[=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
?arg =arg
(&&/analyse-1 analyse ?body))
=body-type (&&/expr-type =body)
;; _ =body-type
- =lambda-type (exec [_ (&type/solve =return =body-type)
- =lambda-type** (&type/clean =return =lambda-type*)]
- (&type/clean =arg =lambda-type**))
+ =lambda-type (exec [_ (&type/solve &type/init-fixpoints =return =body-type)]
+ (&type/clean =return =lambda-type*))
+ =bound-arg (&type/lookup =arg)
+ =lambda-type (matchv ::M/objects [=arg =bound-arg]
+ [["lux;VarT" id] ["lux;Some" bound]]
+ (&type/clean =arg =lambda-type)
+
+ [["lux;VarT" id] ["lux;None" _]]
+ (let [var-name (str (gensym ""))
+ bound (&/V "lux;BoundT" var-name)]
+ (exec [_ (&type/reset id bound)
+ lambda-type (&type/clean =arg =lambda-type)]
+ (return (&/V "lux;AllT" (&/T (&/|list) "" var-name lambda-type))))))
;; :let [_ (prn '=lambda-type =lambda-type)]
]
(return (&/|list (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured ?arg =body)) =lambda-type))))))))
-(defn analyse-get [analyse ?slot ?record]
- (exec [=record (&&/analyse-1 analyse ?record)
- =record-type (&&/expr-type =record)
- =slot-type (&type/slot-type =record-type ?slot)]
- (return (&/|list (&/V "Expression" (&/T (&/V "get" (?slot =record)) =slot-type))))))
-
-(defn analyse-set [analyse ?slot ?value ?record]
- (exec [=value (&&/analyse-1 analyse ?value)
- =record (&&/analyse-1 analyse ?record)
- =record-type (&&/expr-type =record)
- =slot-type (&type/slot-type =record-type ?slot)
- _ (&type/solve =slot-type =value)]
- (return (&/|list (&/V "Expression" (&/T (&/V "set" (&/T ?slot =value =record)) =slot-type))))))
-
(defn analyse-def [analyse ?name ?value]
;; (prn 'analyse-def ?name ?value)
(exec [module-name &/get-module-name]
(&/if% (&&def/defined? module-name ?name)
(fail (str "[Analyser Error] Can't redefine " ?name))
- (exec [=value (&&/analyse-1 analyse ?value)
+ (exec [=value (&/with-scope ?name
+ (&&/analyse-1 analyse ?value))
=value-type (&&/expr-type =value)
_ (&&def/define module-name ?name =value-type)]
(return (&/|list (&/V "Statement" (&/V "def" (&/T ?name =value)))))))))
@@ -219,22 +216,32 @@
(return (&/|list)))
(defn analyse-check [analyse eval! ?type ?value]
+ (println "analyse-check#0")
(exec [=type (&&/analyse-1 analyse ?type)
+ :let [_ (println "analyse-check#1")]
=type-type (&&/expr-type =type)
- _ (&type/solve &type/+type+ =type-type)
+ :let [_ (println "analyse-check#2")
+ _ (println 1 (&type/show-type &type/Type))
+ _ (println 2 (&type/show-type =type-type))]
+ _ (&type/solve &type/init-fixpoints &type/Type =type-type)
+ :let [_ (println "analyse-check#3")]
==type (eval! =type)
- =value (&&/analyse-1 analyse ?value)]
+ :let [_ (println "analyse-check#4" (&type/show-type ==type))]
+ =value (&&/analyse-1 analyse ?value)
+ :let [_ (println "analyse-check#5")]]
(matchv ::M/objects [=value]
[["Expression" [?expr ?expr-type]]]
- (exec [_ (&type/solve ==type ?expr-type)]
- (return (&/V "Expression" (&/T ?expr ==type)))))))
+ (exec [:let [_ (println "analyse-check#6" (&type/show-type ?expr-type))]
+ _ (&type/solve &type/init-fixpoints ==type ?expr-type)
+ :let [_ (println "analyse-check#7")]]
+ (return (&/|list (&/V "Expression" (&/T ?expr ==type))))))))
(defn analyse-coerce [analyse eval! ?type ?value]
(exec [=type (&&/analyse-1 analyse ?type)
=type-type (&&/expr-type =type)
- _ (&type/solve &type/+type+ =type-type)
+ _ (&type/solve &type/init-fixpoints &type/Type =type-type)
==type (eval! =type)
=value (&&/analyse-1 analyse ?value)]
(matchv ::M/objects [=value]
[["Expression" [?expr ?expr-type]]]
- (return (&/V "Expression" (&/T ?expr ==type))))))
+ (return (&/|list (&/V "Expression" (&/T ?expr ==type)))))))
diff --git a/src/lux/base.clj b/src/lux/base.clj
index 089d1bf8a..29ecfd123 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -132,15 +132,23 @@
(V "lux;Right" (T state value))))
(defn bind [m-value step]
+ (when (not (fn? m-value))
+ (prn 'bind (aget m-value 0)))
+ (when (not (fn? step))
+ (prn 'bind (aget step 0)))
;; (prn 'bind m-value step)
(fn [state]
(let [inputs (m-value state)]
;; (prn 'bind/inputs (aget inputs 0))
(matchv ::M/objects [inputs]
[["lux;Right" [?state ?datum]]]
- ((step ?datum) ?state)
+ (let [next-fn (step ?datum)]
+ (when (not (fn? next-fn))
+ (prn 'bind (aget next-fn 0)
+ (aget next-fn 1)))
+ (next-fn ?state))
- [_]
+ [["lux;Left" _]]
inputs))))
(defmacro exec [steps return]
@@ -598,7 +606,7 @@
(exec [module get-current-module-env]
(return (get$ "lux;name" module))))
-(defn ^:private with-scope [name body]
+(defn with-scope [name body]
(fn [state]
(let [output (body (update$ "lux;local-envs" #(|cons (env name) %) state))]
(matchv ::M/objects [output]
diff --git a/src/lux/compiler.clj b/src/lux/compiler.clj
index 53787473b..bf724c768 100644
--- a/src/lux/compiler.clj
+++ b/src/lux/compiler.clj
@@ -76,12 +76,6 @@
[["lambda" [?scope ?env ?args ?body]]]
(&&lambda/compile-lambda compile-expression ?scope ?env ?args ?body)
- [["get" [?slot ?record]]]
- (&&lux/compile-get compile-expression ?type ?slot ?record)
-
- [["set" [?slot ?value ?record]]]
- (&&lux/compile-set compile-expression ?type ?slot ?value ?record)
-
;; Integer arithmetic
[["jvm-iadd" [?x ?y]]]
(&&host/compile-jvm-iadd compile-expression ?type ?x ?y)
@@ -334,9 +328,10 @@
(fail "[Compiler Error] Can't compile expressions as top-level forms.")))
(defn ^:private eval! [expr]
+ (prn 'eval! (aget expr 0))
+ ;; (assert false)
(exec [eval-ctor &/get-eval-ctor
:let [class-name (str eval-ctor)
- class-file (str class-name ".class")
=class (doto (new ClassWriter ClassWriter/COMPUTE_MAXS)
(.visit Opcodes/V1_5 (+ Opcodes/ACC_PUBLIC Opcodes/ACC_SUPER)
class-name nil "java/lang/Object" nil)
@@ -354,7 +349,7 @@
(return nil)))
:let [bytecode (.toByteArray (doto =class
.visitEnd))]
- _ (&&/save-class! class-file bytecode)
+ _ (&&/save-class! class-name bytecode)
loader &/loader]
(-> (.loadClass loader class-name)
(.getField "_eval")
diff --git a/src/lux/compiler/host.clj b/src/lux/compiler/host.clj
index c46684622..40ad7bb6d 100644
--- a/src/lux/compiler/host.clj
+++ b/src/lux/compiler/host.clj
@@ -40,22 +40,22 @@
char-class "java.lang.Character"]
(defn prepare-return! [*writer* *type*]
(matchv ::M/objects [*type*]
- [["lux;TNothing" nil]]
+ [["lux;NothingT" nil]]
(.visitInsn *writer* Opcodes/ACONST_NULL)
- [["lux;TData" ["char" _]]]
+ [["lux;DataT" ["char" _]]]
(.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class char-class) "valueOf" (str "(C)" (&host/->type-signature char-class)))
- [["lux;TData" ["int" _]]]
+ [["lux;DataT" ["int" _]]]
(.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class integer-class) "valueOf" (str "(I)" (&host/->type-signature integer-class)))
- [["lux;TData" ["long" _]]]
+ [["lux;DataT" ["long" _]]]
(.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class long-class) "valueOf" (str "(J)" (&host/->type-signature long-class)))
- [["lux;TData" ["boolean" _]]]
+ [["lux;DataT" ["boolean" _]]]
(.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class boolean-class) "valueOf" (str "(Z)" (&host/->type-signature boolean-class)))
- [["lux;TData" [_ _]]]
+ [["lux;DataT" [_ _]]]
nil)
*writer*))
diff --git a/src/lux/compiler/lambda.clj b/src/lux/compiler/lambda.clj
index 7d53fa739..cce87e978 100644
--- a/src/lux/compiler/lambda.clj
+++ b/src/lux/compiler/lambda.clj
@@ -65,7 +65,7 @@
$start (new Label)
$end (new Label)
_ (doto *writer*
- (-> (.visitLocalVariable (str &&/local-prefix idx) (&host/->java-sig (&/V "lux;TAny" nil)) nil $start $end (+ 2 idx))
+ (-> (.visitLocalVariable (str &&/local-prefix idx) (&host/->java-sig (&/V "lux;AnyT" nil)) nil $start $end (+ 2 idx))
(->> (dotimes [idx num-locals])))
(.visitLabel $start))]
ret (compile impl-body)
diff --git a/src/lux/compiler/lux.clj b/src/lux/compiler/lux.clj
index 412055956..a761f431a 100644
--- a/src/lux/compiler/lux.clj
+++ b/src/lux/compiler/lux.clj
@@ -132,99 +132,6 @@
:let [_ (.visitMethodInsn *writer* Opcodes/INVOKEINTERFACE (&host/->class &host/function-class) "apply" &&/apply-signature)]]
(return nil)))
-(defn compile-get [compile *type* ?slot ?record]
- (exec [*writer* &/get-writer
- _ (compile ?record)
- :let [$then (new Label)
- $test-else (new Label)
- $end (new Label)
- $start (new Label)
- _ (doto *writer* ;; record
- (.visitInsn Opcodes/DUP) ;; record, record
- (.visitInsn Opcodes/ARRAYLENGTH) ;; record, length
- (.visitInsn Opcodes/ICONST_2) ;; record, length, 2
- (.visitInsn Opcodes/ISUB) ;; record, length--
-
- (.visitLabel $start)
- (.visitInsn Opcodes/DUP) ;; record, length, length
- (.visitLdcInsn (int -2)) ;; record, length, length, -2
- (.visitJumpInsn Opcodes/IF_ICMPEQ $then) ;; record, length
- ;;;
- (.visitInsn Opcodes/DUP2) ;; record, length, record, length
- (.visitInsn Opcodes/AALOAD) ;; record, length, aslot
- (.visitLdcInsn ?slot) ;; record, length, aslot, eslot
- (.visitMethodInsn Opcodes/INVOKEVIRTUAL (&host/->class "java.lang.Object") "equals" (str "(" (&host/->type-signature "java.lang.Object") ")Z")) ;; record, length, Z
- (.visitJumpInsn Opcodes/IFEQ $test-else) ;; record, length
- (.visitInsn Opcodes/ICONST_1) ;; record, length, 1
- (.visitInsn Opcodes/IADD) ;; record, length+
- (.visitInsn Opcodes/AALOAD) ;; value
- (.visitJumpInsn Opcodes/GOTO $end)
- (.visitLabel $test-else)
- (.visitInsn Opcodes/ICONST_2) ;; record, length, 2
- (.visitInsn Opcodes/ISUB) ;; record, length--
- (.visitJumpInsn Opcodes/GOTO $start)
- ;;;
- (.visitLabel $then)
- (.visitInsn Opcodes/POP) ;; record
- (.visitInsn Opcodes/POP) ;;
- (.visitInsn Opcodes/ACONST_NULL) ;; null
- (.visitLabel $end))]]
- (return nil)))
-
-(let [o-sig (&host/->type-signature "java.lang.Object")]
- (defn compile-set [compile *type* ?slot ?value ?record]
- (exec [*writer* &/get-writer
- _ (compile ?record)
- :let [$then (new Label)
- $test-else (new Label)
- $end (new Label)
- $start (new Label)
- _ (doto *writer* ;; record1
- ;;;
- (.visitInsn Opcodes/DUP) ;; record1, record1
- (.visitInsn Opcodes/ARRAYLENGTH) ;; record1, length1
- (.visitTypeInsn Opcodes/ANEWARRAY (&host/->class "java.lang.Object")) ;; record1, record2
- (.visitInsn Opcodes/DUP_X1) ;; record2, record1, record2
- (.visitInsn Opcodes/ICONST_0) ;; record2, record1, record2, 0
- (.visitInsn Opcodes/SWAP) ;; record2, record1, 0, record2
- (.visitInsn Opcodes/DUP) ;; record2, record1, 0, record2, record2
- (.visitInsn Opcodes/ARRAYLENGTH) ;; record2, record1, 0, record2, length2
- (.visitInsn Opcodes/ICONST_0) ;; record2, record1, 0, record2, length2, 0
- (.visitInsn Opcodes/SWAP) ;; record2, record1, 0, record2, 0, length2
- (.visitMethodInsn Opcodes/INVOKESTATIC (&host/->class "java.lang.System") "arraycopy" (str "(" o-sig "I" o-sig "I" "I" ")V")) ;; record2
- ;;;
- (.visitInsn Opcodes/DUP) ;; record, record
- (.visitInsn Opcodes/ARRAYLENGTH) ;; record, length
- (.visitInsn Opcodes/ICONST_2) ;; record, length, 2
- (.visitInsn Opcodes/ISUB) ;; record, length--
-
- (.visitLabel $start)
- (.visitInsn Opcodes/DUP) ;; record, length, length
- (.visitLdcInsn (int -2)) ;; record, length, length, -2
- (.visitJumpInsn Opcodes/IF_ICMPEQ $then) ;; record, length
- ;;;
- (.visitInsn Opcodes/DUP2) ;; record, length, record, length
- (.visitInsn Opcodes/AALOAD) ;; record, length, aslot
- (.visitLdcInsn ?slot) ;; record, length, aslot, eslot
- (.visitMethodInsn Opcodes/INVOKEVIRTUAL (&host/->class "java.lang.Object") "equals" (str "(" (&host/->type-signature "java.lang.Object") ")Z")) ;; record, length, Z
- (.visitJumpInsn Opcodes/IFEQ $test-else) ;; record, length
- (.visitInsn Opcodes/DUP2) ;; record, length, record, length
- (.visitInsn Opcodes/ICONST_1) ;; record, length, record, length, 1
- (.visitInsn Opcodes/IADD) ;; record, length, record, length+
- (do (compile ?value)) ;; record, length, record, length+, value
- (.visitInsn Opcodes/AASTORE) ;; record, length
- (.visitInsn Opcodes/POP) ;; record
- (.visitJumpInsn Opcodes/GOTO $end)
- (.visitLabel $test-else)
- (.visitInsn Opcodes/ICONST_2) ;; record, length, 2
- (.visitInsn Opcodes/ISUB) ;; record, length--
- (.visitJumpInsn Opcodes/GOTO $start)
- ;;;
- (.visitLabel $then)
- (.visitInsn Opcodes/POP) ;; record
- (.visitLabel $end))]]
- (return nil))))
-
(defn compile-def [compile ?name ?body]
(exec [*writer* &/get-writer
module-name &/get-module-name
diff --git a/src/lux/host.clj b/src/lux/host.clj
index 6432a6d5f..1dda5de5d 100644
--- a/src/lux/host.clj
+++ b/src/lux/host.clj
@@ -19,8 +19,8 @@
"")
(.getSimpleName class)))]
(if (= "void" base)
- (return (&/V "lux;TNothing" nil))
- (let [base* (&/V "lux;TData" (&/T base (&/V "lux;Nil" nil)))]
+ (return (&/V "lux;NothingT" nil))
+ (let [base* (&/V "lux;DataT" (&/T base (&/V "lux;Nil" nil)))]
(if arr-level
(return (reduce (fn [inner _]
(&/V "array" (&/V "lux;Cons" (&/T inner (&/V "lux;Nil" nil)))))
@@ -81,19 +81,19 @@
(defn ->java-sig [type]
(matchv ::M/objects [type]
- [["lux;TAny" _]]
+ [["lux;AnyT" _]]
(->type-signature "java.lang.Object")
- [["lux;TNothing" _]]
+ [["lux;NothingT" _]]
"V"
- [["lux;TData" ["array" ["lux;Cons" [?elem ["lux;Nil" _]]]]]]
+ [["lux;DataT" ["array" ["lux;Cons" [?elem ["lux;Nil" _]]]]]]
(str "[" (->java-sig ?elem))
- [["lux;TData" [?name ?params]]]
+ [["lux;DataT" [?name ?params]]]
(->type-signature ?name)
- [["lux;TLambda" [_ _]]]
+ [["lux;LambdaT" [_ _]]]
(->type-signature function-class)))
(defn extract-jvm-param [token]
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 68fb13b3d..7d05d65b4 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -2,12 +2,23 @@
(:refer-clojure :exclude [deref apply merge])
(:require [clojure.core.match :as M :refer [match matchv]]
clojure.core.match.array
- [lux.base :as & :refer [exec return* return fail fail* assert!]]))
+ [lux.base :as & :refer [exec return* return fail fail* assert! |let]]))
;; [Util]
(def ^:private success (return nil))
-(defn ^:private deref [id]
+(defn lookup [type]
+ (matchv ::M/objects [type]
+ [["lux;VarT" id]]
+ (fn [state]
+ (if-let [type* (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
+ (return* state type*)
+ (fail* (str "Unknown type-var: " id))))
+
+ [_]
+ (fail "[Type Error] Can't lookup non-vars.")))
+
+(defn deref [id]
(fn [state]
(if-let [type* (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
(matchv ::M/objects [type*]
@@ -18,7 +29,7 @@
(fail* (str "Unbound type-var: " id)))
(fail* (str "Unknown type-var: " id)))))
-(defn ^:private reset [id type]
+(defn reset [id type]
(fn [state]
(if-let [_ (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
(return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|put id (&/V "lux;Some" type) %)
@@ -35,147 +46,79 @@
(&/update$ "lux;counter" inc)
(&/update$ "lux;mappings" (fn [ms] (&/|put id (&/V "lux;None" nil) ms))))
state)
- (&/V "lux;TVar" id)))))
+ (&/V "lux;VarT" id)))))
(def fresh-lambda
(exec [=arg fresh-var
=return fresh-var]
- (return (&/V "lux;TLambda" (&/T =arg =return)))))
-
-(defn ^:private ->type [pseudo-type]
- (match pseudo-type
- [::Any]
- (&/V "lux;TAny" nil)
-
- [::Nothing]
- (&/V "lux;TNothing" nil)
-
- [::Data ?name ?elems]
- (&/V "lux;TData" (&/T ?name ?elems))
-
- [::Tuple ?members]
- (&/V "lux;TTuple" (&/|map ->type ?members))
-
- [::Variant ?members]
- (&/V "lux;TVariant" (&/|map (fn [[k v]] (&/T k (->type v)))
- ?members))
-
- [::Record ?members]
- (&/V "lux;TRecord" (&/|map (fn [[k v]] (&/T k (->type v)))
- ?members))
-
- [::Lambda ?input ?output]
- (&/V "lux;TLambda" (&/T (->type ?input) (->type ?output)))
-
- [::App ?lambda ?param]
- (&/V "lux;TApp" (&/T (->type ?lambda) (->type ?param)))
-
- [::Bound ?name]
- (&/V "lux;TBound" ?name)
-
- [::Var ?id]
- (&/V "lux;TVar" ?id)
-
- [::All ?env ?name ?arg ?body]
- (&/V "lux;TAll" (&/T (&/|map (fn [[k v]] (&/T k (->type v)))
- ?env)
- ?name
- ?arg
- (->type ?body)))
- ))
-
-(def +list+
- [::All (&/|list) "List" "a"
- [::Variant (&/|list ["lux;Cons" [::Tuple (&/|list [::Bound "a"] [::App [::Bound "List"] [::Bound "a"]])]]
- ["lux;Nil" [::Tuple (&/|list)]])]])
-
-(def +type+
- (let [text [::Data "java.lang.String" (&/|list)]
- type [::App [::Bound "Type"] [::Any]]
- list-of-types [::App +list+ type]
- string=>type [::App +list+ [::Tuple (&/|list text type)]]]
- (->type [::All (&/|list) "Type" "_"
- [::Variant (&/|list ["lux;TAny" [::Tuple (&/|list)]]
- ["lux;TNothing" [::Tuple (&/|list)]]
- ["lux;TData" [::Tuple (&/|list text list-of-types)]]
- ["lux;TTuple" list-of-types]
- ["lux;TVariant" string=>type]
- ["lux;TRecord" string=>type]
- ["lux;TLambda" [::Tuple (&/|list type
- type)]]
- ["lux;TApp" [::Tuple (&/|list type
- type)]]
- ["lux;TBound" text]
- ["lux;TVar" [::Data "java.lang.Long" (&/|list)]]
- ["lux;TAll" [::Tuple (&/|list string=>type text text type)]]
- )]])))
+ (return (&/V "lux;LambdaT" (&/T =arg =return)))))
(defn clean [tvar type]
(matchv ::M/objects [tvar]
- [["lux;TVar" ?tid]]
+ [["lux;VarT" ?tid]]
(matchv ::M/objects [type]
- [["lux;TVar" ?id]]
+ [["lux;VarT" ?id]]
(if (= ?tid ?id)
(&/try-all% (&/|list (exec [=type (deref ?id)]
(clean tvar =type))
(return type)))
(return type))
- [["lux;TLambda" [?arg ?return]]]
+ [["lux;LambdaT" [?arg ?return]]]
(exec [=arg (clean tvar ?arg)
=return (clean tvar ?return)]
- (return (&/V "lux;TLambda" (to-array [=arg =return]))))
+ (return (&/V "lux;LambdaT" (to-array [=arg =return]))))
- [["lux;TApp" [?lambda ?param]]]
+ [["lux;AppT" [?lambda ?param]]]
(exec [=lambda (clean tvar ?lambda)
=param (clean tvar ?param)]
- (return (&/V "lux;TApp" (to-array [=lambda =param]))))
+ (return (&/V "lux;AppT" (to-array [=lambda =param]))))
- [["lux;TTuple" ?members]]
+ [["lux;TupleT" ?members]]
(exec [=members (&/map% (partial clean tvar) ?members)]
- (return (&/V "lux;TTuple" =members)))
+ (return (&/V "lux;TupleT" =members)))
- [["lux;TVariant" ?members]]
+ [["lux;VariantT" ?members]]
(exec [=members (&/map% (fn [[k v]]
(exec [=v (clean tvar v)]
(return (to-array [k =v]))))
?members)]
- (return (&/V "lux;TVariant" =members)))
+ (return (&/V "lux;VariantT" =members)))
- [["lux;TRecord" ?members]]
+ [["lux;RecordT" ?members]]
(exec [=members (&/map% (fn [[k v]]
(exec [=v (clean tvar v)]
(return (to-array [k =v]))))
?members)]
- (return (&/V "lux;TRecord" =members)))
+ (return (&/V "lux;RecordT" =members)))
- [["lux;TAll" [?env ?name ?arg ?body]]]
+ [["lux;AllT" [?env ?name ?arg ?body]]]
(exec [=env (&/map% (fn [[k v]]
(exec [=v (clean tvar v)]
(return (to-array [k =v]))))
?env)]
- (return (&/V "lux;TAll" (to-array [=env ?name ?arg ?body]))))
+ (return (&/V "lux;AllT" (to-array [=env ?name ?arg ?body]))))
[_]
(return type)
)))
(defn show-type [type]
- (prn 'show-type (aget type 0))
+ ;; (prn 'show-type (aget type 0))
(matchv ::M/objects [type]
- [["lux;TAny" _]]
+ [["lux;AnyT" _]]
"Any"
- [["lux;TNothing" _]]
+ [["lux;NothingT" _]]
"Nothing"
- [["lux;TData" [name params]]]
+ [["lux;DataT" [name params]]]
(str "(^ " name " [" (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) "])")
- [["lux;TTuple" elems]]
+ [["lux;TupleT" elems]]
(str "(, " (->> elems (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")
- [["lux;TVariant" cases]]
+ [["lux;VariantT" cases]]
(str "(| " (->> cases
(&/|map (fn [kv]
(matchv ::M/objects [kv]
@@ -188,7 +131,7 @@
(&/fold str "")) ")")
- [["lux;TRecord" fields]]
+ [["lux;RecordT" fields]]
(str "(& " (->> fields
(&/|map (fn [kv]
(matchv ::M/objects [kv]
@@ -197,140 +140,146 @@
(&/|interpose " ")
(&/fold str "")) ")")
- [["lux;TLambda" [input output]]]
+ [["lux;LambdaT" [input output]]]
(str "(-> " (show-type input) " " (show-type output) ")")
- [["lux;TVar" id]]
+ [["lux;VarT" id]]
(str "⌈" id "⌋")
- [["lux;TBound" name]]
+ [["lux;BoundT" name]]
name
- [["lux;TApp" [?lambda ?param]]]
+ [["lux;AppT" [?lambda ?param]]]
(str "(" (show-type ?lambda) " " (show-type ?param) ")")
- [["lux;TAll" [?env ?name ?arg ?body]]]
+ [["lux;AllT" [?env ?name ?arg ?body]]]
(str "(All " ?name " " ?arg " " (show-type ?body) ")")
))
+(defn type= [x y]
+ (matchv ::M/objects [x y]
+ [["lux;AnyT" _] ["lux;AnyT" _]]
+ true
+
+ [["lux;NothingT" _] ["lux;NothingT" _]]
+ true
+
+ [["lux;DataT" [xname xparams]] ["lux;DataT" [yname yparams]]]
+ (&/fold (fn [old xy] (and old (type= (aget xy 0) (aget xy 1))))
+ (= xname yname)
+ (&/zip2 xparams yparams))
+
+ [["lux;TupleT" xelems] ["lux;TupleT" yelems]]
+ (&/fold (fn [old xy] (and old (type= (aget xy 0) (aget xy 1))))
+ true
+ (&/zip2 xelems yelems))
+
+ [["lux;VariantT" xcases] ["lux;VariantT" ycases]]
+ (&/fold (fn [old cases]
+ (matchv ::M/objects [cases]
+ [[[xtag xtype] [ytag ytype]]]
+ (and (= xtag ytag)
+ (type= xtype ytype))))
+ true (&/zip2 xcases ycases))
+
+
+ [["lux;RecordT" xfields] ["lux;RecordT" yfields]]
+ (&/fold (fn [old cases]
+ (matchv ::M/objects [cases]
+ [[[xtag xtype] [ytag ytype]]]
+ (and (= xtag ytag)
+ (type= xtype ytype))))
+ true (&/zip2 xfields yfields))
+
+ [["lux;LambdaT" [xinput xoutput]] ["lux;LambdaT" [yinput youtput]]]
+ (and (type= xinput yinput)
+ (type= xoutput youtput))
+
+ [["lux;VarT" xid] ["lux;VarT" yid]]
+ (= xid yid)
+
+ [["lux;BoundT" xname] ["lux;BoundT" yname]]
+ (= xname yname)
+
+ [["lux;AppT" [xlambda xparam]] ["lux;AppT" [ylambda yparam]]]
+ (and (type= xlambda ylambda)
+ (type= xparam yparam))
+
+ [["lux;AllT" [xenv xname xarg xbody]] ["lux;AllT" [yenv yname yarg ybody]]]
+ (and (&/fold (fn [old cases]
+ (matchv ::M/objects [cases]
+ [[[xtag xtype] [ytag ytype]]]
+ (and (= xtag ytag)
+ (type= xtype ytype))))
+ true (&/zip2 xenv yenv))
+ (= xname yname)
+ (= xarg yarg)
+ (type= xbody ybody))
+
+ [_ _]
+ (do (prn 'type= (show-type x) (show-type y))
+ false)
+ ))
+
+(defn ^:private fp-get [k xs]
+ (matchv ::M/objects [k]
+ [[e a]]
+ (matchv ::M/objects [xs]
+ [["lux;Nil" _]]
+ (&/V "lux;None" nil)
+
+ [["lux;Cons" [[[e* a*] v*] xs*]]]
+ (if (and (type= e e*)
+ (type= a a*))
+ (&/V "lux;Some" v*)
+ (fp-get k xs*))
+ )))
+
+(defn ^:private fp-put [k v fixpoints]
+ (&/|cons (&/T k v) fixpoints))
+
(defn ^:private solve-error [expected actual]
(str "Type " (show-type expected) " does not subsume type " (show-type actual)))
-(defn solve [expected actual]
- ;; (prn 'solve expected actual)
- ;; (prn 'solve (aget expected 0) (aget actual 0))
- success
- ;; (matchv ::M/objects [expected actual]
- ;; [["Any" _] _]
- ;; success
-
- ;; [_ ["Nothing" _]]
- ;; success
-
- ;; [["Data" [e!name e!params]] ["Data" [a!name a!params]]]
- ;; (if (or (= e!name a!name)
- ;; (.isAssignableFrom (Class/forName e!name) (Class/forName a!name)))
- ;; success
- ;; (fail (str "not (" actual " <= " expected ")")))
-
- ;; [["Tuple" e!elems] ["Tuple" a!elems]]
- ;; (exec [_ (assert! (= (&/|length e!elems) (&/|length a!elems))
- ;; "Tuples must have matching element sizes.")
- ;; _ (&/map% (fn [n g] (solve n g))
- ;; (&/zip2 e!elems a!elems))]
- ;; success)
-
- ;; [["Variant" e!cases] ["Variant" a!cases]]
- ;; (exec [_ (&/map% (fn [slot]
- ;; (solve (&/|get e!cases slot) (&/|get a!cases slot)))
- ;; (&/|keys a!cases))]
- ;; success)
-
- ;; [["Record" e!fields] ["Record" a!fields]]
- ;; (exec [_ (&/map% (fn [slot]
- ;; (solve (&/|get e!fields slot) (&/|get a!fields slot)))
- ;; (&/|keys e!fields))]
- ;; success)
-
- ;; [["Lambda" [e!input e!output]] ["Lambda" [a!input a!output]]]
- ;; (exec [_ (solve a!input e!input)]
- ;; (solve e!output a!output))
-
- ;; [["Var" e!id] _]
- ;; (&/try-all% (&/|list (exec [=e!type (deref e!id)
- ;; _ (solve =e!type actual)
- ;; _ (reset e!id =e!type)]
- ;; success)
- ;; (exec [_ (reset e!id actual)]
- ;; success)))
-
- ;; [_ ["Var" a!id]]
- ;; (&/try-all% (&/|list (exec [=a!type (deref a!id)
- ;; _ (solve expected =a!type)
- ;; _ (reset a!id =a!type)]
- ;; success)
- ;; (exec [_ (reset a!id expected)]
- ;; success)))
-
- ;; [_ _]
- ;; (solve-error expected actual)
- ;; )
- )
+(defn beta-reduce [env type]
+ ;; (prn 'beta-reduce (aget type 0))
+ (matchv ::M/objects [type]
+ [["lux;VariantT" ?cases]]
+ (&/V "lux;VariantT" (&/|map (fn [kv]
+ (|let [[k v] kv]
+ (&/T k (beta-reduce env v))))
+ ?cases))
-(let [&& #(and %1 %2)]
- (defn merge [x y]
- (matchv ::M/objects [x y]
- [_ ["lux;TAny" _]]
- (return y)
+ [["lux;RecordT" ?fields]]
+ (&/V "lux;RecordT" (&/|map (fn [kv]
+ (|let [[k v] kv]
+ (&/T k (beta-reduce env v))))
+ ?fields))
- [["lux;TAny" _] _]
- (return x)
+ [["lux;TupleT" ?members]]
+ (&/V "lux;TupleT" (&/|map (partial beta-reduce env) ?members))
- [_ ["lux;TNothing" _]]
- (return x)
+ [["lux;DataT" [?name ?params]]]
+ (&/V "lux;DataT" (&/T ?name (&/|map (partial beta-reduce env) ?params)))
- [["lux;TNothing" _] _]
- (return y)
+ [["lux;AppT" [?type-fn ?type-arg]]]
+ (&/V "lux;AppT" (&/T (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)))
- ;;;
-
- [_ _]
- (return x)
+ [["lux;AllT" [?local-env ?local-name ?local-arg ?local-def]]]
+ (&/V "lux;AllT" (&/T (&/|merge ?local-env env) ?local-name ?local-arg ?local-def))
- ;; [["Variant" x!cases] ["Variant" y!cases]]
- ;; (if (and (reduce && true
- ;; (for [[xslot xtype] (keys x!cases)]
- ;; (if-let [ytype (get y!cases xslot)]
- ;; (= xtype ytype)
- ;; true)))
- ;; (reduce && true
- ;; (for [[yslot ytype] (keys y!cases)]
- ;; (if-let [xtype (get x!cases yslot)]
- ;; (= xtype ytype)
- ;; true))))
- ;; (return (&/V "Variant" (clojure.core/merge x!cases y!cases)))
- ;; (fail (str "Incompatible variants: " (pr-str x) " and " (pr-str y))))
-
- ;; [["Record" x!fields] ["Record" y!fields]]
- ;; (if (and (= (keys x!fields) (keys y!fields))
- ;; (->> (keys x!fields)
- ;; (map #(= (get x!fields %) (get y!fields %)))
- ;; (reduce && true)))
- ;; (return x)
- ;; (fail (str "Incompatible records: " (pr-str x) " and " (pr-str y))))
-
- [_ _]
- (fail (str "[Type System] Can't merge types: " (pr-str x) " and " (pr-str y))))))
+ [["lux;LambdaT" [?input ?output]]]
+ (&/V "lux;LambdaT" (&/T (beta-reduce env ?input) (beta-reduce env ?output)))
-(defn apply-lambda [func param]
- (matchv ::M/objects [func]
- [["lux;TLambda" [input output]]]
- (exec [_ (solve input param)]
- (return output))
+ [["lux;BoundT" ?name]]
+ (if-let [bound (&/|get ?name env)]
+ (do ;; (prn 'beta-reduce "lux;BoundT" ?name (->> (&/|keys env) (&/|interpose " ") (&/fold str ""))
+ ;; (show-type bound))
+ (beta-reduce env bound))
+ type)
[_]
- (return (&/V "lux;TAny" nil))
- ;; (fail (str "[Type System] Can't apply type " (str func) " to type " (str param)))
+ type
))
(defn slot-type [record slot]
@@ -342,4 +291,241 @@
[["lux;Right" type]]
(return* state type))))
-(def +dont-care+ (&/V "lux;TAny" nil))
+(def +dont-care+ (&/V "lux;AnyT" nil))
+
+(defn apply-type [type-fn param]
+ (prn 'apply-type (aget type-fn 0) (aget param 0))
+ (matchv ::M/objects [type-fn]
+ [["lux;AllT" [local-env local-name local-arg local-def]]]
+ (return (beta-reduce (->> local-env
+ (&/|put local-name type-fn)
+ (&/|put local-arg param))
+ local-def))
+
+ [["lux;AppT" [F A]]]
+ (exec [type-fn* (apply-type F A)]
+ (apply-type type-fn* param))
+
+ [_]
+ (fail (str "[Type System] Can't apply type function " (show-type type-fn) " to type " (show-type param)))))
+
+(def init-fixpoints (&/|list))
+
+(defn solve [fixpoints expected actual]
+ (prn 'solve (aget expected 0) (aget actual 0))
+ ;; (prn 'solve (show-type expected) (show-type actual))
+ (matchv ::M/objects [expected actual]
+ [["Any" _] _]
+ success
+
+ [_ ["Nothing" _]]
+ success
+
+ [["lux;VarT" ?id] _]
+ (&/try-all% (&/|list (exec [bound (deref ?id)]
+ (solve fixpoints bound actual))
+ (reset ?id actual)))
+
+ [_ ["lux;VarT" ?id]]
+ (&/try-all% (&/|list (exec [bound (deref ?id)]
+ (solve fixpoints expected bound))
+ (reset ?id expected)))
+
+ [["lux;AppT" [F A]] _]
+ (exec [expected* (apply-type F A)
+ :let [fp-pair (&/T expected actual)]]
+ (matchv ::M/objects [(fp-get fp-pair fixpoints)]
+ [["lux;Some" ?]]
+ (if ?
+ success
+ (fail (solve-error expected actual)))
+
+ [["lux;None" _]]
+ (solve (fp-put fp-pair true fixpoints) expected* actual)))
+
+ [_ ["lux;AppT" [F A]]]
+ (exec [actual* (apply-type F A)]
+ (solve fixpoints expected actual*))
+
+ [["lux;AllT" _] _]
+ (exec [$var fresh-var
+ expected* (apply-type expected $var)]
+ (solve fixpoints expected* actual))
+
+ [_ ["lux;AllT" _]]
+ (exec [$var fresh-var
+ actual* (apply-type actual $var)]
+ (solve fixpoints expected actual*))
+
+ [["lux;DataT" [e!name e!params]] ["lux;DataT" [a!name a!params]]]
+ (cond (not= e!name a!name)
+ (fail (str "[Type Error] Names don't match: " e!name " & " a!name))
+
+ (not= (&/|length e!params) (&/|length a!params))
+ (fail "[Type Error] Params don't match in size.")
+
+ :else
+ (exec [_ (&/map% (fn [ea]
+ (|let [[e a] ea]
+ (solve fixpoints e a)))
+ (&/zip2 e!params a!params))]
+ success))
+
+ [["lux;LambdaT" [eI eO]] ["lux;LambdaT" [aI aO]]]
+ (exec [_ (solve fixpoints aI eI)]
+ (solve fixpoints eO aO))
+
+ [["lux;TupleT" e!members] ["lux;TupleT" a!members]]
+ (if (= (&/|length e!members) (&/|length a!members))
+ (exec [_ (&/map% (fn [ea]
+ (|let [[e a] ea]
+ (do (prn "lux;TupleT" 'ITER (show-type e) (show-type a))
+ (solve fixpoints e a))))
+ (&/zip2 e!members a!members))
+ :let [_ (prn "lux;TupleT" 'DONE)]]
+ success)
+ (do ;; (prn "lux;TupleT" (&/|length e!members) (&/|length a!members))
+ ;; (prn "lux;TupleT"
+ ;; (&/fold str "" (&/|interpose " " (&/|map show-type e!members)))
+ ;; (&/fold str "" (&/|interpose " " (&/|map show-type a!members))))
+ ;; (prn "lux;TupleT#fail" (fail "[Type Error] Tuples don't match in size."))
+ (fail "[Type Error] Tuples don't match in size.")))
+
+ [["lux;VariantT" e!cases] ["lux;VariantT" a!cases]]
+ (exec [_ (&/map% (fn [kv]
+ (|let [[k av] kv]
+ (if-let [ev (&/|get k e!cases)]
+ (solve fixpoints ev av)
+ (fail (str "[Type Error] The expected variant cannot handle case: #" k)))))
+ a!cases)]
+ success)
+
+ [["lux;RecordT" e!fields] ["lux;RecordT" a!fields]]
+ (if (= (&/|length e!fields) (&/|length a!fields))
+ (exec [_ (&/map% (fn [slot]
+ (if-let [e!type (&/|get e!fields slot)]
+ (if-let [a!type (&/|get a!fields slot)]
+ (solve fixpoints e!type a!type)
+ (fail (solve-error expected actual)))
+ (fail (solve-error expected actual))))
+ (&/|keys e!fields))]
+ success)
+ (fail "[Type Error] Records don't match in size."))
+
+ [["lux;BoundT" name] _]
+ (do (prn "lux;BoundT" name)
+ (assert false))
+ ;; ...
+
+ ;; [_ ["lux;BoundT" name]]
+ ;; ...
+ ))
+
+(defn apply-lambda [func param]
+ (matchv ::M/objects [func]
+ [["lux;LambdaT" [input output]]]
+ (exec [_ (solve init-fixpoints input param)]
+ (return output))
+
+ [_]
+ (fail (str "[Type System] Can't apply type " (show-type func) " to type " (show-type param)))
+ ))
+
+(def Any (&/V "lux;AnyT" nil))
+(def Int (&/V "lux;DataT" (&/T "java.lang.Long" (&/|list))))
+(def Text (&/V "lux;DataT" (&/T "java.lang.String" (&/|list))))
+
+(def List
+ (&/V "lux;AllT" (&/T (&/|table) "List" "a"
+ (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list)))
+ (&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a")
+ (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List")
+ (&/V "lux;BoundT" "a")))))))))))
+
+(def Type
+ (let [Type (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "Type") (&/V "lux;BoundT" "")))
+ TypeEnv (&/V "lux;AppT" (&/T List (&/V "lux;TupleT" (&/|list Text Type))))
+ Unit (&/V "lux;TupleT" (&/|list))
+ TypeList (&/V "lux;AppT" (&/T List Type))
+ TypePair (&/V "lux;TupleT" (&/|list Type Type))]
+ (&/V "lux;AppT" (&/T (&/V "lux;AllT" (&/T (&/|list) "Type" ""
+ (&/V "lux;VariantT" (&/|list (&/T "lux;AnyT" Unit)
+ (&/T "lux;NothingT" Unit)
+ (&/T "lux;DataT" (&/V "lux;TupleT" (&/|list Text TypeList)))
+ (&/T "lux;TupleT" TypeList)
+ (&/T "lux;VariantT" TypeEnv)
+ (&/T "lux;RecordT" TypeEnv)
+ (&/T "lux;LambdaT" TypePair)
+ (&/T "lux;BoundT" Text)
+ (&/T "lux;VarT" Int)
+ (&/T "lux;AllT" (&/V "lux;TupleT" (&/|list TypeEnv Text Text Type)))
+ (&/T "lux;AppT" TypePair)
+ ))))
+ (&/V "lux;NothingT" nil)))))
+
+(let [&& #(and %1 %2)]
+ (defn merge [x y]
+ (matchv ::M/objects [x y]
+ [_ ["lux;AnyT" _]]
+ (return y)
+
+ [["lux;AnyT" _] _]
+ (return x)
+
+ [_ ["lux;NothingT" _]]
+ (return x)
+
+ [["lux;NothingT" _] _]
+ (return y)
+
+ [["lux;VariantT" x!cases] ["lux;VariantT" y!cases]]
+ (exec [cases (&/fold% (fn [cases kv]
+ (matchv ::M/objects [kv]
+ [[k v]]
+ (if-let [cv (&/|get k cases)]
+ (exec [_ (solve init-fixpoints cv v)]
+ (return cases))
+ (return (&/|put k v cases)))))
+ x!cases
+ y!cases)]
+ (return (&/V "lux;VariantT" cases)))
+
+ [["lux;RecordT" x!fields] ["lux;RecordT" y!fields]]
+ (if (= (&/|length x!fields) (&/|length y!fields))
+ (exec [fields (&/fold% (fn [fields kv]
+ (matchv ::M/objects [kv]
+ [[k v]]
+ (if-let [cv (&/|get k fields)]
+ (exec [_ (solve init-fixpoints cv v)]
+ (return fields))
+ (fail (str "[Type System Error] Incompatible records: " (show-type x) " and " (show-type y))))))
+ x!fields
+ y!fields)]
+ (return (&/V "lux;RecordT" fields)))
+ (fail (str "[Type System Error] Incompatible records: " (show-type x) " and " (show-type y))))
+
+ [_ _]
+ (fail (str "[Type System Error] Can't merge types: " (show-type x) " and " (show-type y))))))
+
+(comment
+ (do (def Real (&/V "lux;DataT" (&/T "java.lang.Long" (&/|list))))
+ (def RealT (&/V "lux;VariantT" (&/|list (&/T "lux;DataT" (&/V "lux;TupleT" (&/|list Text
+ (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list)))))))))))
+ )
+
+ (matchv ::M/objects [((solve init-fixpoints Type RealT)
+ (&/init-state nil))]
+ [["lux;Left" ?msg]]
+ (assert false ?msg)
+
+ [_]
+ (println "YEAH!"))
+
+ (matchv ::M/objects [((solve init-fixpoints List (&/V "lux;AppT" (&/T List Real)))
+ (&/init-state nil))]
+ [["lux;Left" ?msg]]
+ (assert false ?msg)
+
+ [_]
+ (println "YEAH!"))
+ )
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-13 00:14:43 +0000