diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lux/analyser/base.clj | 2 | ||||
| -rw-r--r-- | src/lux/analyser/case.clj | 67 | ||||
| -rw-r--r-- | src/lux/analyser/lux.clj | 43 | ||||
| -rw-r--r-- | src/lux/base.clj | 16 | ||||
| -rw-r--r-- | src/lux/compiler/case.clj | 8 | ||||
| -rw-r--r-- | src/lux/compiler/lux.clj | 8 | ||||
| -rw-r--r-- | src/lux/compiler/type.clj | 4 | ||||
| -rw-r--r-- | src/lux/host.clj | 2 | ||||
| -rw-r--r-- | src/lux/type.clj | 136 |
9 files changed, 183 insertions, 103 deletions
diff --git a/src/lux/analyser/base.clj b/src/lux/analyser/base.clj index 2d6d72fb8..bbbe18a89 100644 --- a/src/lux/analyser/base.clj +++ b/src/lux/analyser/base.clj @@ -185,7 +185,7 @@ (return ?module))] (return (&/T module* ?name)))) -(let [tag-names #{"DataT" "VoidT" "UnitT" "SumT" "TupleT" "LambdaT" "BoundT" "VarT" "ExT" "UnivQ" "ExQ" "AppT" "NamedT"}] +(let [tag-names #{"DataT" "VoidT" "UnitT" "SumT" "ProdT" "LambdaT" "BoundT" "VarT" "ExT" "UnivQ" "ExQ" "AppT" "NamedT"}] (defn type-tag? [module name] (and (= "lux" module) (contains? tag-names name)))) diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj index 3b6dceb27..d71782914 100644 --- a/src/lux/analyser/case.clj +++ b/src/lux/analyser/case.clj @@ -74,20 +74,20 @@ =type (&type/apply-type type $var)] (adjust-type* up =type)) - (&/$TupleT ?members) - (|do [(&/$TupleT ?members*) (&/fold% (fn [_abody ena] - (|let [[_aenv _aidx (&/$VarT _avar)] ena] - (|do [_ (&type/set-var _avar (&/V &/$BoundT _aidx))] - (&type/clean* _avar _abody)))) - type - up)] - (return (&type/Tuple$ (&/|map (fn [v] - (&/fold (fn [_abody ena] - (|let [[_aenv _aidx _avar] ena] - (&/V &/$UnivQ (&/T _aenv _abody)))) - v - up)) - ?members*)))) + (&/$ProdT ?left ?right) + (|do [(&/$ProdT =left =right) (&/fold% (fn [_abody ena] + (|let [[_aenv _aidx (&/$VarT _avar)] ena] + (|do [_ (&type/set-var _avar (&/V &/$BoundT _aidx))] + (&type/clean* _avar _abody)))) + type + up) + :let [distributor (fn [v] + (&/fold (fn [_abody ena] + (|let [[_aenv _aidx _avar] ena] + (&/V &/$UnivQ (&/T _aenv _abody)))) + v + up))]] + (return (&type/Prod$ (distributor =left) (distributor =right)))) (&/$SumT ?left ?right) (|do [(&/$SumT =left =right) (&/fold% (fn [_abody ena] @@ -178,19 +178,25 @@ =kont kont] (return (&/T (&/V $TupleTestAC (&/|list)) =kont))) + (&/$Cons ?member (&/$Nil)) + (analyse-pattern var?? value-type ?member kont) + _ (|do [value-type* (adjust-type value-type)] (|case value-type* - (&/$TupleT ?member-types) - (if (not (.equals ^Object (&/|length ?member-types) (&/|length ?members))) - (fail (str "[Pattern-matching Error] Pattern-matching mismatch. Require tuple[" (&/|length ?member-types) "]. Given tuple [" (&/|length ?members) "]" " -- " (&/show-ast pattern))) + (&/$ProdT _) + (|case (&type/tuple-types-for (&/|length ?members) value-type*) + (&/$None) + (fail (str "[Pattern-matching Error] Pattern-matching mismatch. Require tuple[" (&/|length (&type/flatten-prod value-type*)) "]. Given tuple [" (&/|length ?members) "]" " -- " (&/show-ast pattern))) + + (&/$Some ?member-types*) (|do [[=tests =kont] (&/fold (fn [kont* vm] (|let [[v m] vm] (|do [[=test [=tests =kont]] (analyse-pattern &/None$ v m kont*)] (return (&/T (&/Cons$ =test =tests) =kont))))) (|do [=kont kont] (return (&/T &/Nil$ =kont))) - (&/|reverse (&/zip2 ?member-types ?members)))] + (&/|reverse (&/zip2 ?member-types* ?members)))] (return (&/T (&/V $TupleTestAC =tests) =kont)))) _ @@ -382,18 +388,26 @@ (|do [unknown? (&type/unknown? value-type)] (if unknown? (|do [=structs (&/map% (check-totality+ check-totality) ?structs) - _ (&type/check value-type (&/V &/$TupleT (&/|map &/|second =structs)))] + _ (&type/check value-type (|case (->> (&/|map &/|second =structs) (&/|reverse)) + (&/$Cons last prevs) + (&/fold (fn [right left] (&type/Prod$ left right)) + last prevs)))] (return (or ?total (&/fold #(and %1 %2) true (&/|map &/|first =structs))))) (if ?total (return true) (|do [value-type* (resolve-type value-type)] (|case value-type* - (&/$TupleT ?members) - (|do [totals (&/map2% (fn [sub-struct ?member] - (check-totality ?member sub-struct)) - ?structs ?members)] - (return (&/fold #(and %1 %2) true totals))) + (&/$ProdT _) + (|case (&type/tuple-types-for (&/|length ?structs) value-type*) + (&/$None) + (fail (str "[Pattern-maching Error] Tuple-mismatch. Require tuple[" (&/|length (&type/flatten-prod value-type*)) "]. Given tuple [" (&/|length ?structs) "]")) + + (&/$Some ?member-types*) + (|do [totals (&/map2% check-totality + ?member-types* + ?structs)] + (return (&/fold #(and %1 %2) true totals)))) _ (fail "[Pattern-maching Error] Tuple is not total."))))))) @@ -404,8 +418,9 @@ (|do [value-type* (resolve-type value-type)] (|case value-type* (&/$SumT _) - (|do [:let [?members (&type/flatten-sum value-type*)] - totals (&/map2% check-totality ?members ?structs)] + (|do [totals (&/map2% check-totality + (&type/flatten-sum value-type*) + ?structs)] (return (&/fold #(and %1 %2) true totals))) _ diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj index 415565c7c..3777e8053 100644 --- a/src/lux/analyser/lux.clj +++ b/src/lux/analyser/lux.clj @@ -56,6 +56,12 @@ (&/$Left exo-type) exo-type (&/$Right exo-type) exo-type)) + (&/$Cons ?elem (&/$Nil)) + (analyse (|case ?exo-type + (&/$Left exo-type) exo-type + (&/$Right exo-type) exo-type) + ?elem) + _ (|case ?exo-type (&/$Left exo-type) @@ -88,7 +94,10 @@ (|do [=elems (&/map% #(|do [=analysis (&&/analyse-1+ analyse %)] (return =analysis)) ?elems) - _ (&type/check exo-type (&/V &/$TupleT (&/|map &&/expr-type* =elems))) + _ (&type/check exo-type (|case (->> (&/|map &&/expr-type* =elems) (&/|reverse)) + (&/$Cons last prevs) + (&/fold (fn [right left] (&type/Prod$ left right)) + last prevs))) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&/V &&/$tuple =elems) @@ -96,14 +105,20 @@ (|do [exo-type* (&type/actual-type exo-type)] (&/with-attempt (|case exo-type* - (&/$TupleT ?members) - (|do [=elems (&/map2% (fn [elem-t elem] - (&&/analyse-1 analyse elem-t elem)) - ?members ?elems) - _cursor &/cursor] - (return (&/|list (&&/|meta exo-type _cursor - (&/V &&/$tuple =elems) - )))) + (&/$ProdT _) + (|case (&type/tuple-types-for (&/|length ?elems) exo-type*) + (&/$None) + (fail (str "[Analysis Error] Tuple-mismatch. Require tuple[" (&/|length (&type/flatten-prod exo-type*)) "]. Given tuple [" (&/|length ?elems) "]" " -- " (str "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]"))) + + (&/$Some ?member-types*) + (|do [=elems (&/map2% (fn [elem-t elem] + (&&/analyse-1 analyse elem-t elem)) + ?member-types* + ?elems) + _cursor &/cursor] + (return (&/|list (&&/|meta exo-type _cursor + (&/V &&/$tuple =elems) + ))))) (&/$UnivQ _) (|do [$var &type/existential @@ -356,7 +371,15 @@ (|do [[real-name [?type ?meta ?value]] (&&module/find-def ?module ?name)] (|case (&&meta/meta-get &&meta/macro?-tag ?meta) (&/$Some _) - (|do [macro-expansion (fn [state] (-> ?value (.apply ?args) (.apply state)))] + (|do [macro-expansion (fn [state] (-> ?value (.apply ?args) (.apply state))) + ;; :let [_ (when (or (= "using" (aget real-name 1)) + ;; ;; (= "defsig" (aget real-name 1)) + ;; ) + ;; (->> (&/|map &/show-ast macro-expansion) + ;; (&/|interpose "\n") + ;; (&/fold str "") + ;; (prn (&/ident->text real-name))))] + ] (&/flat-map% (partial analyse exo-type) macro-expansion)) _ diff --git a/src/lux/base.clj b/src/lux/base.clj index fe8ce184a..ba1489726 100644 --- a/src/lux/base.clj +++ b/src/lux/base.clj @@ -48,7 +48,7 @@ "VoidT" "UnitT" "SumT" - "TupleT" + "ProdT" "LambdaT" "BoundT" "VarT" @@ -1082,3 +1082,17 @@ ($Left msg) (V $Left msg))))) + +(defn |take [n xs] + (|case (T n xs) + [0 _] Nil$ + [_ ($Nil)] Nil$ + [_ ($Cons x xs*)] (Cons$ x (|take (dec n) xs*)) + )) + +(defn |drop [n xs] + (|case (T n xs) + [0 _] xs + [_ ($Nil)] Nil$ + [_ ($Cons x xs*)] (|drop (dec n) xs*) + )) diff --git a/src/lux/compiler/case.clj b/src/lux/compiler/case.clj index e0d1b886e..1a4006312 100644 --- a/src/lux/compiler/case.clj +++ b/src/lux/compiler/case.clj @@ -86,10 +86,16 @@ (.visitJumpInsn Opcodes/GOTO $target)) (&a-case/$TupleTestAC ?members) - (if (&/|empty? ?members) + (|case ?members + (&/$Nil) (doto writer (.visitInsn Opcodes/POP) (.visitJumpInsn Opcodes/GOTO $target)) + + (&/$Cons ?member (&/$Nil)) + (compile-match ?member $target $else) + + _ (doto writer (.visitTypeInsn Opcodes/CHECKCAST "[Ljava/lang/Object;") (-> (doto (.visitInsn Opcodes/DUP) diff --git a/src/lux/compiler/lux.clj b/src/lux/compiler/lux.clj index edafc67e2..cbe9cb0f3 100644 --- a/src/lux/compiler/lux.clj +++ b/src/lux/compiler/lux.clj @@ -56,9 +56,15 @@ (defn compile-tuple [compile ?elems] (|do [^MethodVisitor *writer* &/get-writer :let [num-elems (&/|length ?elems)]] - (if (= 0 num-elems) + (|case num-elems + 0 (|do [:let [_ (.visitInsn *writer* Opcodes/ACONST_NULL)]] (return nil)) + + 1 + (compile (&/|head ?elems)) + + _ (|do [:let [_ (doto *writer* (.visitLdcInsn (int num-elems)) (.visitTypeInsn Opcodes/ANEWARRAY "java/lang/Object"))] diff --git a/src/lux/compiler/type.clj b/src/lux/compiler/type.clj index e053c8b3c..0abb4d42e 100644 --- a/src/lux/compiler/type.clj +++ b/src/lux/compiler/type.clj @@ -68,8 +68,8 @@ (&/$UnitT) (variant$ &/$UnitT (tuple$ (&/|list))) - (&/$TupleT members) - (variant$ &/$TupleT (List$ (&/|map type->analysis members))) + (&/$ProdT left right) + (variant$ &/$ProdT (tuple$ (&/|list (type->analysis left) (type->analysis right)))) (&/$SumT left right) (variant$ &/$SumT (tuple$ (&/|list (type->analysis left) (type->analysis right)))) diff --git a/src/lux/host.clj b/src/lux/host.clj index c54da0799..473d0dc60 100644 --- a/src/lux/host.clj +++ b/src/lux/host.clj @@ -69,7 +69,7 @@ (&/$SumT _) (return object-array) - (&/$TupleT _) + (&/$ProdT _) (return object-array) (&/$NamedT ?name ?type) diff --git a/src/lux/type.clj b/src/lux/type.clj index 66ea59f6c..0655aa8b2 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -5,7 +5,8 @@ (ns lux.type (:refer-clojure :exclude [deref apply merge bound?]) - (:require clojure.core.match + (:require [clojure.template :refer [do-template]] + clojure.core.match clojure.core.match.array (lux [base :as & :refer [|do return* return fail fail* assert! |let |case]]) [lux.type.host :as &&host])) @@ -35,9 +36,8 @@ (&/V &/$LambdaT (&/T in out))) (defn App$ [fun arg] (&/V &/$AppT (&/T fun arg))) -(defn Tuple$ [members] - (assert (> (&/|length members) 0)) - (&/V &/$TupleT members)) +(defn Prod$ [left right] + (&/V &/$ProdT (&/T left right))) (defn Sum$ [left right] (&/V &/$SumT (&/T left right))) (defn Univ$ [env body] @@ -54,7 +54,7 @@ (def Real (Named$ (&/T "lux" "Real") (Data$ "java.lang.Double" &/Nil$))) (def Char (Named$ (&/T "lux" "Char") (Data$ "java.lang.Character" &/Nil$))) (def Text (Named$ (&/T "lux" "Text") (Data$ "java.lang.String" &/Nil$))) -(def Ident (Named$ (&/T "lux" "Ident") (Tuple$ (&/|list Text Text)))) +(def Ident (Named$ (&/T "lux" "Ident") (Prod$ Text Text))) (def IO (Named$ (&/T "lux/data" "IO") @@ -68,9 +68,9 @@ ;; lux;Nil Unit ;; lux;Cons - (Tuple$ (&/|list (Bound$ 1) - (App$ (Bound$ 0) - (Bound$ 1)))))))) + (Prod$ (Bound$ 1) + (App$ (Bound$ 0) + (Bound$ 1))))))) (def Maybe (Named$ (&/T "lux" "Maybe") @@ -86,11 +86,11 @@ (Named$ (&/T "lux" "Type") (let [Type (App$ (Bound$ 0) (Bound$ 1)) TypeList (App$ List Type) - TypePair (Tuple$ (&/|list Type Type))] + TypePair (Prod$ Type Type)] (App$ (Univ$ empty-env (Sum$ ;; DataT - (Tuple$ (&/|list Text TypeList)) + (Prod$ Text TypeList) (Sum$ ;; VoidT Unit @@ -101,8 +101,8 @@ ;; SumT TypePair (Sum$ - ;; TupleT - TypeList + ;; ProdT + TypePair (Sum$ ;; LambdaT TypePair @@ -117,15 +117,15 @@ Int (Sum$ ;; UnivQ - (Tuple$ (&/|list TypeList Type)) + (Prod$ TypeList Type) (Sum$ ;; ExQ - (Tuple$ (&/|list TypeList Type)) + (Prod$ TypeList Type) (Sum$ ;; AppT TypePair ;; NamedT - (Tuple$ (&/|list Ident Type)))))))))))))) + (Prod$ Ident Type))))))))))))) ) $Void)))) @@ -155,13 +155,13 @@ ;; ListM (App$ List DefMetaValue) ;; DictM - (App$ List (Tuple$ (&/|list Text DefMetaValue)))))))))) + (App$ List (Prod$ Text DefMetaValue))))))))) ) $Void)))) (def DefMeta (Named$ (&/T "lux" "DefMeta") - (App$ List (Tuple$ (&/|list Ident DefMetaValue))))) + (App$ List (Prod$ Ident DefMetaValue)))) (def Macro) @@ -209,7 +209,7 @@ (&/$None) (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id (&/V &/$Some type) %) - ts)) + ts)) state) nil)) (fail* (str "[Type Error] <set-var> Unknown type-var: " id " | " (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) &/|length)))))) @@ -290,9 +290,10 @@ =param (clean* ?tid ?param)] (return (App$ =lambda =param))) - (&/$TupleT ?members) - (|do [=members (&/map% (partial clean* ?tid) ?members)] - (return (Tuple$ =members))) + (&/$ProdT ?left ?right) + (|do [=left (clean* ?tid ?left) + =right (clean* ?tid ?right)] + (return (Prod$ =left =right))) (&/$SumT ?left ?right) (|do [=left (clean* ?tid ?left) @@ -334,31 +335,36 @@ _ (&/T fun-type &/Nil$))) -(defn flatten-sum [type] - "(-> Type (List Type))" - (|case type - (&/$SumT left right) - (&/Cons$ left (flatten-sum right)) +(do-template [<tag> <flatten> <at> <desc>] + (do (defn <flatten> [type] + "(-> Type (List Type))" + (|case type + (<tag> left right) + (&/Cons$ left (<flatten> right)) - _ - (&/|list type))) + _ + (&/|list type))) -(defn sum-at [tag type] - "(-> Int Type (Lux Type))" - (|case type - (&/$NamedT ?name ?type) - (sum-at tag ?type) - - (&/$SumT ?left ?right) - (|case (&/T tag ?right) - [0 _] (return ?left) - [1 (&/$SumT ?left* _)] (return ?left*) - [1 _] (return ?right) - [_ (&/$SumT _ _)] (sum-at (dec tag) ?right) - _ (fail (str "[Type Error] Variant lacks case: " tag " | " (show-type type)))) + (defn <at> [tag type] + "(-> Int Type (Lux Type))" + (|case type + (&/$NamedT ?name ?type) + (<at> tag ?type) + + (<tag> ?left ?right) + (|case (&/T tag ?right) + [0 _] (return ?left) + [1 (<tag> ?left* _)] (return ?left*) + [1 _] (return ?right) + [_ (<tag> _ _)] (<at> (dec tag) ?right) + _ (fail (str "[Type Error] " <desc> " lacks member: " tag " | " (show-type type)))) - _ - (fail (str "[Type Error] Type is not a variant: " (show-type type))))) + _ + (fail (str "[Type Error] Type is not a " <desc> ": " (show-type type)))))) + + &/$SumT flatten-sum sum-at "Sum" + &/$ProdT flatten-prod prod-at "Product" + ) (defn show-type [^objects type] (|case type @@ -376,10 +382,8 @@ (&/$UnitT) "Unit" - (&/$TupleT elems) - (if (&/|empty? elems) - "(,)" - (str "(, " (->> elems (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")) + (&/$ProdT _) + (str "(, " (->> (flatten-prod type) (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")") (&/$SumT _) (str "(|| " (->> (flatten-sum type) (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")") @@ -431,10 +435,9 @@ [(&/$UnitT) (&/$UnitT)] true - [(&/$TupleT xelems) (&/$TupleT yelems)] - (&/fold2 (fn [old x y] (and old (type= x y))) - true - xelems yelems) + [(&/$ProdT xL xR) (&/$ProdT yL yR)] + (and (type= xL yL) + (type= xR yR)) [(&/$SumT xL xR) (&/$SumT yL yR)] (and (type= xL yL) @@ -519,8 +522,10 @@ =right (beta-reduce env ?right)] (Sum$ =left =right)) - (&/$TupleT ?members) - (Tuple$ (&/|map (partial beta-reduce env) ?members)) + (&/$ProdT ?left ?right) + (let [=left (beta-reduce env ?left) + =right (beta-reduce env ?right)] + (Prod$ =left =right)) (&/$AppT ?type-fn ?type-arg) (App$ (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)) @@ -745,13 +750,9 @@ (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? aI eI)] (check* class-loader fixpoints* invariant?? eO aO)) - [(&/$TupleT e!members) (&/$TupleT a!members)] - (|do [fixpoints* (&/fold2% (fn [fp e a] - (|do [[fp* _] (check* class-loader fp invariant?? e a)] - (return fp*))) - fixpoints - e!members a!members)] - (return (&/T fixpoints* nil))) + [(&/$ProdT eL eR) (&/$ProdT aL aR)] + (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? eL aL)] + (check* class-loader fixpoints* invariant?? eR aR)) [(&/$SumT eL eR) (&/$SumT aL aR)] (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? eL aL)] @@ -827,3 +828,18 @@ _ (return type))) + +(defn tuple-types-for [size-members type] + "(-> Int Type (Maybe (List Type)))" + (|let [?member-types (flatten-prod type) + size-types (&/|length ?member-types)] + (if (not (>= size-types size-members)) + &/None$ + (|let [?member-types* (if (= size-types size-members) + ?member-types + (&/|++ (&/|take (dec size-members) ?member-types) + (&/|list (|case (->> (&/|drop (dec size-members) ?member-types) (&/|reverse)) + (&/$Cons last prevs) + (&/fold (fn [right left] (Prod$ left right)) + last prevs)))))] + (&/Some$ ?member-types*))))) |