From 9e095a1a8708a114a4105b4c5a583f6a2830ffc9 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Mon, 30 Mar 2015 23:41:58 -0400 Subject: - Beginning to add type-system + type-inferencer. - Removed exec, get@' & set@' special forms, as they are not primitive enough as to be part of the language. --- src/lux.clj | 1 + src/lux/analyser.clj | 44 ++-- src/lux/analyser/host.clj | 30 +-- src/lux/analyser/lux.clj | 63 ++--- src/lux/base.clj | 14 +- src/lux/compiler.clj | 11 +- src/lux/compiler/host.clj | 12 +- src/lux/compiler/lambda.clj | 2 +- src/lux/compiler/lux.clj | 93 ------- src/lux/host.clj | 14 +- src/lux/type.clj | 598 +++++++++++++++++++++++++++++--------------- 11 files changed, 482 insertions(+), 400 deletions(-) (limited to 'src') 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 [ ] - (let [input-type (&/V "lux;TData" (to-array [ (&/V "lux;Nil" nil)])) - output-type (&/V "lux;TData" (to-array [ (&/V "lux;Nil" nil)]))] + (let [input-type (&/V "lux;DataT" (to-array [ (&/V "lux;Nil" nil)])) + output-type (&/V "lux;DataT" (to-array [ (&/V "lux;Nil" nil)]))] (defn [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 [ ] (defn [analyse ?value] (exec [=value (&&/analyse-1 analyse ?value)] - (return (&/|list (&/V "Expression" (&/T (&/V =value) (&/V "lux;TData" (&/T (&/V "lux;Nil" nil))))))))) + (return (&/|list (&/V "Expression" (&/T (&/V =value) (&/V "lux;DataT" (&/T (&/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 [ ] (defn [analyse ?value] (exec [=value (&&/analyse-1 analyse ?value)] - (return (&/|list (&/V "Expression" (&/T (&/V =value) (&/V "lux;TData" (&/T (&/V "lux;Nil" nil))))))))) + (return (&/|list (&/V "Expression" (&/T (&/V =value) (&/V "lux;DataT" (&/T (&/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!")) + ) -- cgit v1.2.3