diff options
Diffstat (limited to 'luxc/src')
| -rw-r--r-- | luxc/src/lux/analyser.clj | 6 | ||||
| -rw-r--r-- | luxc/src/lux/analyser/base.clj | 2 | ||||
| -rw-r--r-- | luxc/src/lux/analyser/case.clj | 104 | ||||
| -rw-r--r-- | luxc/src/lux/analyser/lux.clj | 56 | ||||
| -rw-r--r-- | luxc/src/lux/analyser/proc/common.clj | 32 | ||||
| -rw-r--r-- | luxc/src/lux/analyser/proc/js.clj | 20 | ||||
| -rw-r--r-- | luxc/src/lux/analyser/proc/jvm.clj | 106 | ||||
| -rw-r--r-- | luxc/src/lux/analyser/record.clj | 2 | ||||
| -rw-r--r-- | luxc/src/lux/base.clj | 22 | ||||
| -rw-r--r-- | luxc/src/lux/compiler/cache/type.clj | 44 | ||||
| -rw-r--r-- | luxc/src/lux/compiler/jvm/proc/host.clj | 24 | ||||
| -rw-r--r-- | luxc/src/lux/host.clj | 20 | ||||
| -rw-r--r-- | luxc/src/lux/type.clj | 452 | ||||
| -rw-r--r-- | luxc/src/lux/type/host.clj | 42 |
14 files changed, 466 insertions, 466 deletions
diff --git a/luxc/src/lux/analyser.clj b/luxc/src/lux/analyser.clj index 18bfdcd3e..1c854acb9 100644 --- a/luxc/src/lux/analyser.clj +++ b/luxc/src/lux/analyser.clj @@ -26,7 +26,7 @@ (|do [_cursor &/cursor] (analyse exo-type (&/T [_cursor (&/$Tuple values)]))) (|case exo-type - (&/$VarT id) + (&/$Var id) (|do [? (&type/bound? id)] (if (or ? (&&/type-tag? module tag-name)) (&&lux/analyse-variant analyse (&/$Right exo-type) idx is-last? values) @@ -46,7 +46,7 @@ (fn [?var] (|do [[[?output-type ?output-cursor] ?output-term] (&&/analyse-1 analyser ?var syntax)] (|case [?var ?output-type] - [(&/$VarT ?e-id) (&/$VarT ?a-id)] + [(&/$Var ?e-id) (&/$Var ?a-id)] (if (= ?e-id ?a-id) (|do [=output-type (&type/clean ?var ?output-type)] (return (&&/|meta =output-type ?output-cursor ?output-term))) @@ -203,7 +203,7 @@ ;; [Resources] (defn analyse [optimize eval! compile-module compilers] (|do [asts &parser/parse] - (&/flat-map% (partial analyse-ast optimize eval! compile-module compilers &/$VoidT) asts))) + (&/flat-map% (partial analyse-ast optimize eval! compile-module compilers &/$Void) asts))) (defn clean-output [?var analysis] (|do [:let [[[?output-type ?output-cursor] ?output-term] analysis] diff --git a/luxc/src/lux/analyser/base.clj b/luxc/src/lux/analyser/base.clj index e1678fb2b..e762c3870 100644 --- a/luxc/src/lux/analyser/base.clj +++ b/luxc/src/lux/analyser/base.clj @@ -75,7 +75,7 @@ (return ?module))] (return (&/T [module* ?name])))) -(let [tag-names #{"HostT" "VoidT" "UnitT" "SumT" "ProdT" "FunctionT" "BoundT" "VarT" "ExT" "UnivQ" "ExQ" "AppT" "NamedT"}] +(let [tag-names #{"Host" "Void" "Unit" "Sum" "Product" "Function" "Bound" "Var" "Ex" "UnivQ" "ExQ" "App" "Named"}] (defn type-tag? [module name] (and (= "lux" module) (contains? tag-names name)))) diff --git a/luxc/src/lux/analyser/case.clj b/luxc/src/lux/analyser/case.clj index 1e3214dad..613e415f5 100644 --- a/luxc/src/lux/analyser/case.clj +++ b/luxc/src/lux/analyser/case.clj @@ -41,7 +41,7 @@ (defn ^:private resolve-type [type] (|case type - (&/$VarT ?id) + (&/$Var ?id) (|do [type* (&/try-all% (&/|list (&type/deref ?id) (&/fail-with-loc "##1##")))] (resolve-type type*)) @@ -65,30 +65,30 @@ (defn clean! [level ?tid bound-idx type] (|case type - (&/$VarT ?id) + (&/$Var ?id) (if (= ?tid ?id) - (&/$BoundT (+ (* 2 level) bound-idx)) + (&/$Bound (+ (* 2 level) bound-idx)) type) - (&/$HostT ?name ?params) - (&/$HostT ?name (&/|map (partial clean! level ?tid bound-idx) - ?params)) + (&/$Host ?name ?params) + (&/$Host ?name (&/|map (partial clean! level ?tid bound-idx) + ?params)) - (&/$FunctionT ?arg ?return) - (&/$FunctionT (clean! level ?tid bound-idx ?arg) - (clean! level ?tid bound-idx ?return)) + (&/$Function ?arg ?return) + (&/$Function (clean! level ?tid bound-idx ?arg) + (clean! level ?tid bound-idx ?return)) - (&/$AppT ?lambda ?param) - (&/$AppT (clean! level ?tid bound-idx ?lambda) - (clean! level ?tid bound-idx ?param)) + (&/$App ?lambda ?param) + (&/$App (clean! level ?tid bound-idx ?lambda) + (clean! level ?tid bound-idx ?param)) - (&/$ProdT ?left ?right) - (&/$ProdT (clean! level ?tid bound-idx ?left) - (clean! level ?tid bound-idx ?right)) + (&/$Product ?left ?right) + (&/$Product (clean! level ?tid bound-idx ?left) + (clean! level ?tid bound-idx ?right)) - (&/$SumT ?left ?right) - (&/$SumT (clean! level ?tid bound-idx ?left) - (clean! level ?tid bound-idx ?right)) + (&/$Sum ?left ?right) + (&/$Sum (clean! level ?tid bound-idx ?left) + (clean! level ?tid bound-idx ?right)) (&/$UnivQ ?env ?body) (&/$UnivQ (&/|map (partial clean! level ?tid bound-idx) ?env) @@ -104,20 +104,20 @@ (defn beta-reduce! [level env type] (|case type - (&/$HostT ?name ?params) - (&/$HostT ?name (&/|map (partial beta-reduce! level env) ?params)) + (&/$Host ?name ?params) + (&/$Host ?name (&/|map (partial beta-reduce! level env) ?params)) - (&/$SumT ?left ?right) - (&/$SumT (beta-reduce! level env ?left) - (beta-reduce! level env ?right)) + (&/$Sum ?left ?right) + (&/$Sum (beta-reduce! level env ?left) + (beta-reduce! level env ?right)) - (&/$ProdT ?left ?right) - (&/$ProdT (beta-reduce! level env ?left) - (beta-reduce! level env ?right)) + (&/$Product ?left ?right) + (&/$Product (beta-reduce! level env ?left) + (beta-reduce! level env ?right)) - (&/$AppT ?type-fn ?type-arg) - (&/$AppT (beta-reduce! level env ?type-fn) - (beta-reduce! level env ?type-arg)) + (&/$App ?type-fn ?type-arg) + (&/$App (beta-reduce! level env ?type-fn) + (beta-reduce! level env ?type-arg)) (&/$UnivQ ?local-env ?local-def) (|case ?local-env @@ -135,11 +135,11 @@ _ type) - (&/$FunctionT ?input ?output) - (&/$FunctionT (beta-reduce! level env ?input) - (beta-reduce! level env ?output)) + (&/$Function ?input ?output) + (&/$Function (beta-reduce! level env ?input) + (beta-reduce! level env ?output)) - (&/$BoundT ?idx) + (&/$Bound ?idx) (|case (&/|at (- ?idx (* 2 level)) env) (&/$Some bound) (beta-reduce! level env bound) @@ -165,17 +165,17 @@ (&/$Cons type-fn)) local-def)) - (&/$AppT F A) + (&/$App F A) (|do [type-fn* (apply-type! F A)] (apply-type! type-fn* param)) - (&/$NamedT ?name ?type) + (&/$Named ?name ?type) (apply-type! ?type param) - (&/$ExT id) - (return (&/$AppT type-fn param)) + (&/$Ex id) + (return (&/$App type-fn param)) - (&/$VarT id) + (&/$Var id) (|do [=type-fun (deref id)] (apply-type! =type-fun param)) @@ -199,9 +199,9 @@ =type (apply-type! type $var)] (adjust-type* up =type)) - (&/$ProdT ?left ?right) + (&/$Product ?left ?right) (let [=type (&/fold (fn [_abody ena] - (|let [[_aenv _aidx (&/$VarT _avar)] ena] + (|let [[_aenv _aidx (&/$Var _avar)] ena] (clean! 0 _avar _aidx _abody))) type up) @@ -214,9 +214,9 @@ (return (&type/Tuple$ (&/|map distributor (&type/flatten-prod =type))))) - (&/$SumT ?left ?right) + (&/$Sum ?left ?right) (let [=type (&/fold (fn [_abody ena] - (|let [[_aenv _aidx (&/$VarT _avar)] ena] + (|let [[_aenv _aidx (&/$Var _avar)] ena] (clean! 0 _avar _aidx _abody))) type up) @@ -229,19 +229,19 @@ (return (&type/Variant$ (&/|map distributor (&type/flatten-sum =type))))) - (&/$AppT ?tfun ?targ) + (&/$App ?tfun ?targ) (|do [=type (apply-type! ?tfun ?targ)] (adjust-type* up =type)) - (&/$VarT ?id) + (&/$Var ?id) (|do [type* (&/try-all% (&/|list (&type/deref ?id) (&/fail-with-loc (str "##2##: " ?id))))] (adjust-type* up type*)) - (&/$NamedT ?name ?type) + (&/$Named ?name ?type) (adjust-type* up ?type) - (&/$UnitT) + (&/$Unit) (return type) _ @@ -309,7 +309,7 @@ (&/$Tuple ?members) (|case ?members (&/$Nil) - (|do [_ (&type/check value-type &/$UnitT) + (|do [_ (&type/check value-type &/$Unit) =kont kont] (return (&/T [($TupleTestAC (&/|list)) =kont]))) @@ -323,7 +323,7 @@ (return (&type/fold-prod member-types))) (adjust-type value-type))] (|case value-type* - (&/$ProdT _) + (&/$Product _) (|let [num-elems (&/|length ?members) [_shorter _tuple-types] (&type/tuple-types-for (&/|length ?members) value-type*)] (if (= num-elems _shorter) @@ -604,7 +604,7 @@ (&/$Nil) (|do [value-type* (resolve-type value-type)] (|case value-type* - (&/$UnitT) + (&/$Unit) (return true) _ @@ -616,7 +616,7 @@ (|do [=structs (&/map% (check-totality+ check-totality) ?structs) _ (&type/check value-type (|case (->> (&/|map &/|second =structs) (&/|reverse)) (&/$Cons last prevs) - (&/fold (fn [right left] (&/$ProdT left right)) + (&/fold (fn [right left] (&/$Product left right)) last prevs)))] (return (or ?total (&/fold #(and %1 %2) true (&/|map &/|first =structs))))) @@ -624,7 +624,7 @@ (return true) (|do [value-type* (resolve-type value-type)] (|case value-type* - (&/$ProdT _) + (&/$Product _) (|let [num-elems (&/|length ?structs) [_shorter _tuple-types] (&type/tuple-types-for (&/|length ?structs) value-type*) _ (&/assert! (= num-elems _shorter) @@ -640,7 +640,7 @@ (return true) (|do [value-type* (resolve-type value-type)] (|case value-type* - (&/$SumT _) + (&/$Sum _) (|do [totals (&/map2% check-totality (&type/flatten-sum value-type*) ?structs)] diff --git a/luxc/src/lux/analyser/lux.clj b/luxc/src/lux/analyser/lux.clj index 95dc9af59..2a76ec86a 100644 --- a/luxc/src/lux/analyser/lux.clj +++ b/luxc/src/lux/analyser/lux.clj @@ -31,7 +31,7 @@ ;; nested quantifications that cannot be directly counted. (defn ^:private next-bound-type [type] "(-> Type Type)" - (&/$BoundT (->> (count-univq type) (* 2) (+ 1)))) + (&/$Bound (->> (count-univq type) (* 2) (+ 1)))) (defn ^:private embed-inferred-input [input output] "(-> Type Type Type)" @@ -40,12 +40,12 @@ (&/$UnivQ env (embed-inferred-input input output*)) _ - (&/$FunctionT input output))) + (&/$Function input output))) ;; [Exports] (defn analyse-unit [analyse ?exo-type] (|do [_cursor &/cursor - _ (&type/check ?exo-type &/$UnitT)] + _ (&type/check ?exo-type &/$Unit)] (return (&/|list (&&/|meta ?exo-type _cursor (&&/$tuple (&/|list))))))) @@ -74,7 +74,7 @@ [[tuple-type tuple-cursor] tuple-analysis] (&&/cap-1 (analyse-tuple analyse (&/$Left exo-type**) ?elems)) =var (&type/resolve-type $var) inferred-type (|case =var - (&/$VarT iid) + (&/$Var iid) (|do [:let [=var* (next-bound-type tuple-type)] _ (&type/set-var iid =var*) tuple-type* (&type/clean $var tuple-type)] @@ -96,7 +96,7 @@ ?elems) _ (&type/check exo-type (|case (->> (&/|map &&/expr-type* =elems) (&/|reverse)) (&/$Cons last prevs) - (&/fold (fn [right left] (&/$ProdT left right)) + (&/fold (fn [right left] (&/$Product left right)) last prevs))) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor @@ -105,7 +105,7 @@ (|do [exo-type* (&type/actual-type exo-type)] (&/with-attempt (|case exo-type* - (&/$ProdT _) + (&/$Product _) (|let [num-elems (&/|length ?elems) [_shorter _tuple-types] (&type/tuple-types-for num-elems exo-type*)] (if (= num-elems _shorter) @@ -139,7 +139,7 @@ (&/$UnivQ _) (|do [$var &type/existential - :let [(&/$ExT $var-id) $var] + :let [(&/$Ex $var-id) $var] exo-type** (&type/apply-type exo-type* $var) [[tuple-type tuple-cursor] tuple-analysis] (&/with-scope-type-var $var-id (&&/cap-1 (analyse-tuple analyse (&/$Right exo-type**) ?elems)))] @@ -183,7 +183,7 @@ [[variant-type variant-cursor] variant-analysis] (&&/cap-1 (analyse-variant analyse (&/$Left exo-type**) idx is-last? ?values)) =var (&type/resolve-type $var) inferred-type (|case =var - (&/$VarT iid) + (&/$Var iid) (|do [:let [=var* (next-bound-type variant-type)] _ (&type/set-var iid =var*) variant-type* (&type/clean $var variant-type)] @@ -199,7 +199,7 @@ (&/$Right exo-type) (|do [exo-type* (|case exo-type - (&/$VarT ?id) + (&/$Var ?id) (&/try-all% (&/|list (|do [exo-type* (&type/deref ?id)] (&type/actual-type exo-type*)) (|do [_ (&type/set-var ?id &type/Type)] @@ -209,7 +209,7 @@ (&type/actual-type exo-type))] (&/with-attempt (|case exo-type* - (&/$SumT _) + (&/$Sum _) (|do [vtype (&type/sum-at idx exo-type*) :let [num-variant-types (&/|length (&type/flatten-sum exo-type*)) is-last?* (if (nil? is-last?) @@ -238,7 +238,7 @@ (&/fail-with-loc (str "[Analyser Error] Cannot create variant if the expected type is " (&type/show-type exo-type*) " " idx " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str ""))))) (fn [err] (|case exo-type - (&/$VarT ?id) + (&/$Var ?id) (|do [=exo-type (&type/deref ?id)] (&/fail-with-loc (str err "\n" "[Analyser Error] Cannot create variant if the expected type is " (&type/show-type =exo-type) " " idx " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str ""))))) @@ -249,7 +249,7 @@ (defn analyse-record [analyse exo-type ?elems] (|do [[rec-members rec-type] (&&record/order-record ?elems)] (|case exo-type - (&/$VarT id) + (&/$Var id) (|do [? (&type/bound? id)] (if ? (analyse-tuple analyse (&/$Right exo-type) rec-members) @@ -324,7 +324,7 @@ [=output-t =args] (analyse-apply* analyse exo-type type* ?args) ==args (&/map% (partial &&/clean-analysis $var) =args)] (|case $var - (&/$VarT ?id) + (&/$Var ?id) (|do [? (&type/bound? ?id) type** (if ? (&type/clean $var =output-t) @@ -341,7 +341,7 @@ type* (&type/apply-type ?fun-type* $var)] (analyse-apply* analyse exo-type type* ?args)) - (&/$FunctionT ?input-t ?output-t) + (&/$Function ?input-t ?output-t) (|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*) =arg (&/with-attempt (&&/analyse-1 analyse ?input-t ?arg) @@ -411,7 +411,7 @@ (defn ^:private unravel-inf-appt [type] (|case type - (&/$AppT =input+ (&/$VarT _inf-var)) + (&/$App =input+ (&/$Var _inf-var)) (&/$Cons _inf-var (unravel-inf-appt =input+)) _ @@ -419,16 +419,16 @@ (defn ^:private clean-func-inference [$input $output =input =func] (|case =input - (&/$VarT iid) + (&/$Var iid) (|do [:let [=input* (next-bound-type =func)] _ (&type/set-var iid =input*) =func* (&type/clean $input =func) =func** (&type/clean $output =func*)] (return (&/$UnivQ &/$Nil =func**))) - (&/$AppT =input+ (&/$VarT _inf-var)) + (&/$App =input+ (&/$Var _inf-var)) (&/fold% (fn [_func _inf-var] - (|do [:let [$inf-var (&/$VarT _inf-var)] + (|do [:let [$inf-var (&/$Var _inf-var)] =inf-var (&type/resolve-type $inf-var) _func* (clean-func-inference $inf-var $output =inf-var _func) _ (&type/delete-var _inf-var)] @@ -436,9 +436,9 @@ =func (unravel-inf-appt =input)) - (&/$ProdT _ _) + (&/$Product _ _) (&/fold% (fn [_func _inf-var] - (|do [:let [$inf-var (&/$VarT _inf-var)] + (|do [:let [$inf-var (&/$Var _inf-var)] =inf-var (&type/resolve-type $inf-var) _func* (clean-func-inference $inf-var $output =inf-var _func) _ (&type/delete-var _inf-var)] @@ -453,7 +453,7 @@ (defn analyse-function* [analyse exo-type ?self ?arg ?body] (|case exo-type - (&/$VarT id) + (&/$Var id) (|do [? (&type/bound? id)] (if ? (|do [exo-type* (&type/deref id)] @@ -463,7 +463,7 @@ (fn [$input] (&type/with-var (fn [$output] - (|do [[[function-type function-cursor] function-analysis] (analyse-function* analyse (&/$FunctionT $input $output) ?self ?arg ?body) + (|do [[[function-type function-cursor] function-analysis] (analyse-function* analyse (&/$Function $input $output) ?self ?arg ?body) =input (&type/resolve-type $input) =output (&type/resolve-type $output) inferred-type (clean-func-inference $input $output =input (embed-inferred-input =input =output)) @@ -478,7 +478,7 @@ (|case exo-type* (&/$UnivQ _) (|do [$var &type/existential - :let [(&/$ExT $var-id) $var] + :let [(&/$Ex $var-id) $var] exo-type** (&type/apply-type exo-type* $var)] (&/with-scope-type-var $var-id (analyse-function* analyse exo-type** ?self ?arg ?body))) @@ -490,7 +490,7 @@ =expr (analyse-function* analyse exo-type** ?self ?arg ?body)] (&&/clean-analysis $var =expr)))) - (&/$FunctionT ?arg-t ?return-t) + (&/$Function ?arg-t ?return-t) (|do [[=scope =captured =body] (&&function/with-function ?self exo-type* ?arg ?arg-t (&&/analyse-1 analyse ?return-t ?body)) @@ -509,14 +509,14 @@ (|case exo-type (&/$UnivQ _) (|do [$var &type/existential - :let [(&/$ExT $var-id) $var] + :let [(&/$Ex $var-id) $var] exo-type* (&type/apply-type exo-type $var) [_ _expr] (&/with-scope-type-var $var-id (analyse-function** analyse exo-type* ?self ?arg ?body)) _cursor &/cursor] (return (&&/|meta exo-type _cursor _expr))) - (&/$VarT id) + (&/$Var id) (|do [? (&type/bound? id)] (if ? (|do [exo-type* (&type/actual-type exo-type)] @@ -683,8 +683,8 @@ =value (&&/analyse-1+ analyse ?value)] (return (&/|list (coerce ==type =value))))) -(let [input-type (&/$AppT &type/List &type/Text) - output-type (&/$AppT &type/IO &/$UnitT)] +(let [input-type (&/$App &type/List &type/Text) + output-type (&/$App &type/IO &/$Unit)] (defn analyse-program [analyse optimize compile-program ?args ?body] (|do [_ &/ensure-statement =body (&/with-scope "" diff --git a/luxc/src/lux/analyser/proc/common.clj b/luxc/src/lux/analyser/proc/common.clj index b6727ff53..29797224f 100644 --- a/luxc/src/lux/analyser/proc/common.clj +++ b/luxc/src/lux/analyser/proc/common.clj @@ -21,10 +21,10 @@ (&type/with-var (fn [$var] (|do [:let [(&/$Cons op (&/$Nil)) ?values] - =op (&&/analyse-1 analyse (&/$AppT &type/IO $var) op) - _ (&type/check exo-type (&/$SumT &type/Text ;; lux;Left - $var ;; lux;Right - )) + =op (&&/analyse-1 analyse (&/$App &type/IO $var) op) + _ (&type/check exo-type (&/$Sum &type/Text ;; lux;Left + $var ;; lux;Right + )) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["lux" "try"]) (&/|list =op) (&/|list))))))))) @@ -57,8 +57,8 @@ (&/|list =text =part =start) (&/|list))))))) - ^:private analyse-text-index "index" (&/$AppT &type/Maybe &type/Nat) - ^:private analyse-text-last-index "last-index" (&/$AppT &type/Maybe &type/Nat) + ^:private analyse-text-index "index" (&/$App &type/Maybe &type/Nat) + ^:private analyse-text-last-index "last-index" (&/$App &type/Maybe &type/Nat) ) (defn ^:private analyse-text-contains? [analyse exo-type ?values] @@ -77,7 +77,7 @@ =text (&&/analyse-1 analyse &type/Text text) =from (&&/analyse-1 analyse &type/Nat from) =to (&&/analyse-1 analyse &type/Nat to) - _ (&type/check exo-type (&/$AppT &type/Maybe &type/Text)) + _ (&type/check exo-type (&/$App &type/Maybe &type/Text)) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["text" "clip"]) @@ -131,7 +131,7 @@ (|do [:let [(&/$Cons text (&/$Cons idx (&/$Nil))) ?values] =text (&&/analyse-1 analyse &type/Text text) =idx (&&/analyse-1 analyse &type/Nat idx) - _ (&type/check exo-type (&/$AppT &type/Maybe &type/Char)) + _ (&type/check exo-type (&/$App &type/Maybe &type/Char)) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["text" "char"]) @@ -245,7 +245,7 @@ (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T <encode-op>) (&/|list =x) (&/|list))))))) - (let [decode-type (&/$AppT &type/Maybe <type>)] + (let [decode-type (&/$App &type/Maybe <type>)] (defn <decode> [analyse exo-type ?values] (|do [:let [(&/$Cons x (&/$Nil)) ?values] =x (&&/analyse-1 analyse &type/Text x) @@ -306,7 +306,7 @@ ^:private analyse-deg-to-real &type/Deg &type/Real ["deg" "to-real"] ^:private analyse-real-to-deg &type/Real &type/Deg ["real" "to-deg"] - ^:private analyse-io-log &type/Text &/$UnitT ["io" "log"] + ^:private analyse-io-log &type/Text &/$Unit ["io" "log"] ^:private analyse-io-error &type/Text &type/Bottom ["io" "error"] ^:private analyse-io-exit &type/Int &type/Bottom ["io" "exit"] ) @@ -321,7 +321,7 @@ (defn ^:private analyse-array-new [analyse exo-type ?values] (|do [:let [(&/$Cons length (&/$Nil)) ?values] =length (&&/analyse-1 analyse &type/Nat length) - _ (&type/check exo-type (&/$UnivQ (&/|list) (&type/Array (&/$BoundT 1)))) + _ (&type/check exo-type (&/$UnivQ (&/|list) (&type/Array (&/$Bound 1)))) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["array" "new"]) (&/|list =length) (&/|list))))))) @@ -332,7 +332,7 @@ (|do [:let [(&/$Cons array (&/$Cons idx (&/$Nil))) ?values] =array (&&/analyse-1 analyse (&type/Array $var) array) =idx (&&/analyse-1 analyse &type/Nat idx) - _ (&type/check exo-type (&/$AppT &type/Maybe $var)) + _ (&type/check exo-type (&/$App &type/Maybe $var)) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["array" "get"]) (&/|list =array =idx) (&/|list))))))))) @@ -466,8 +466,8 @@ (defn ^:private analyse-process-future [analyse exo-type ?values] (|do [:let [(&/$Cons ?procedure (&/$Nil)) ?values] - =procedure (&&/analyse-1 analyse (&/$AppT &type/IO &type/Top) ?procedure) - _ (&type/check exo-type &/$UnitT) + =procedure (&&/analyse-1 analyse (&/$App &type/IO &type/Top) ?procedure) + _ (&type/check exo-type &/$Unit) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["process" "future"]) (&/|list =procedure) (&/|list))))))) @@ -475,8 +475,8 @@ (defn ^:private analyse-process-schedule [analyse exo-type ?values] (|do [:let [(&/$Cons ?milliseconds (&/$Cons ?procedure (&/$Nil))) ?values] =milliseconds (&&/analyse-1 analyse &type/Nat ?milliseconds) - =procedure (&&/analyse-1 analyse (&/$AppT &type/IO &type/Top) ?procedure) - _ (&type/check exo-type &/$UnitT) + =procedure (&&/analyse-1 analyse (&/$App &type/IO &type/Top) ?procedure) + _ (&type/check exo-type &/$Unit) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["process" "schedule"]) (&/|list =milliseconds =procedure) (&/|list))))))) diff --git a/luxc/src/lux/analyser/proc/js.clj b/luxc/src/lux/analyser/proc/js.clj index 986720108..33fa7816d 100644 --- a/luxc/src/lux/analyser/proc/js.clj +++ b/luxc/src/lux/analyser/proc/js.clj @@ -10,9 +10,9 @@ (do-template [<name> <proc>] (defn <name> [analyse exo-type ?values] (|do [:let [(&/$Cons ?function ?args) ?values] - =function (&&/analyse-1 analyse (&/$HostT "function" &/$Nil) ?function) + =function (&&/analyse-1 analyse (&/$Host "function" &/$Nil) ?function) =args (&/map% (partial &&/analyse-1+ analyse) ?args) - _ (&type/check exo-type (&/$HostT "object" &/$Nil)) + _ (&type/check exo-type (&/$Host "object" &/$Nil)) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["js" <proc>]) (&/$Cons =function =args) (&/|list))))))) @@ -23,17 +23,17 @@ (defn ^:private analyse-js-object-call [analyse exo-type ?values] (|do [:let [(&/$Cons ?object (&/$Cons ?field ?args)) ?values] - =object (&&/analyse-1 analyse (&/$HostT "object" &/$Nil) ?object) + =object (&&/analyse-1 analyse (&/$Host "object" &/$Nil) ?object) =field (&&/analyse-1 analyse &type/Text ?field) =args (&/map% (partial &&/analyse-1+ analyse) ?args) - _ (&type/check exo-type (&/$HostT "object" &/$Nil)) + _ (&type/check exo-type (&/$Host "object" &/$Nil)) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["js" "object-call"]) (&/$Cons =object (&/$Cons =field =args)) (&/|list))))))) (defn ^:private analyse-js-ref [analyse exo-type ?values] (|do [:let [(&/$Cons [_ (&/$Text ?ref-name)] (&/$Nil)) ?values] - _ (&type/check exo-type (&/$HostT "object" &/$Nil)) + _ (&type/check exo-type (&/$Host "object" &/$Nil)) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["js" "ref"]) (&/|list) (&/|list ?ref-name))))))) @@ -41,9 +41,9 @@ (do-template [<name> <proc>] (defn <name> [analyse exo-type ?values] (|do [:let [(&/$Cons ?object (&/$Cons ?field (&/$Nil))) ?values] - =object (&&/analyse-1 analyse (&/$HostT "object" &/$Nil) ?object) + =object (&&/analyse-1 analyse (&/$Host "object" &/$Nil) ?object) =field (&&/analyse-1 analyse &type/Text ?field) - _ (&type/check exo-type (&/$HostT "object" &/$Nil)) + _ (&type/check exo-type (&/$Host "object" &/$Nil)) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["js" <proc>]) (&/|list =object =field) (&/|list))))))) @@ -54,10 +54,10 @@ (defn ^:private analyse-js-set-field [analyse exo-type ?values] (|do [:let [(&/$Cons ?object (&/$Cons ?field (&/$Cons ?value (&/$Nil)))) ?values] - =object (&&/analyse-1 analyse (&/$HostT "object" &/$Nil) ?object) + =object (&&/analyse-1 analyse (&/$Host "object" &/$Nil) ?object) =field (&&/analyse-1 analyse &type/Text ?field) =value (&&/analyse-1+ analyse ?value) - _ (&type/check exo-type (&/$HostT "object" &/$Nil)) + _ (&type/check exo-type (&/$Host "object" &/$Nil)) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["js" "set-field"]) (&/|list =object =field =value) (&/|list))))))) @@ -65,7 +65,7 @@ (do-template [<name> <proc> <type>] (defn <name> [analyse exo-type ?values] (|do [:let [(&/$Nil) ?values] - :let [output-type (&/$HostT <type> &/$Nil)] + :let [output-type (&/$Host <type> &/$Nil)] _ (&type/check exo-type output-type) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor diff --git a/luxc/src/lux/analyser/proc/jvm.clj b/luxc/src/lux/analyser/proc/jvm.clj index ba9be52b1..977c07787 100644 --- a/luxc/src/lux/analyser/proc/jvm.clj +++ b/luxc/src/lux/analyser/proc/jvm.clj @@ -21,16 +21,16 @@ (defn ^:private ensure-object [type] "(-> Type (Lux (, Text (List Type))))" (|case type - (&/$HostT payload) + (&/$Host payload) (return payload) - (&/$VarT id) + (&/$Var id) (return (&/T ["java.lang.Object" (&/|list)])) - (&/$ExT id) + (&/$Ex id) (return (&/T ["java.lang.Object" (&/|list)])) - (&/$NamedT _ type*) + (&/$Named _ type*) (ensure-object type*) (&/$UnivQ _ type*) @@ -39,7 +39,7 @@ (&/$ExQ _ type*) (ensure-object type*) - (&/$AppT F A) + (&/$App F A) (|do [type* (&type/apply-type F A)] (ensure-object type*)) @@ -49,8 +49,8 @@ (defn ^:private as-object [type] "(-> Type Type)" (|case type - (&/$HostT class params) - (&/$HostT (&host-type/as-obj class) params) + (&/$Host class params) + (&/$Host (&host-type/as-obj class) params) _ type)) @@ -72,19 +72,19 @@ (defn ^:private as-otype+ [type] "(-> Type Type)" (|case type - (&/$HostT name params) - (&/$HostT (as-otype name) params) + (&/$Host name params) + (&/$Host (as-otype name) params) _ type)) (defn ^:private clean-gtype-var [idx gtype-var] - (|let [(&/$VarT id) gtype-var] + (|let [(&/$Var id) gtype-var] (|do [? (&type/bound? id)] (if ? (|do [real-type (&type/deref id)] (return (&/T [idx real-type]))) - (return (&/T [(+ 2 idx) (&/$BoundT idx)])))))) + (return (&/T [(+ 2 idx) (&/$Bound idx)])))))) (defn ^:private clean-gtype-vars [gtype-vars] (|do [[_ clean-types] (&/fold% (fn [idx+types gtype-var] @@ -99,19 +99,19 @@ "(-> Text (List Type) Type)" (&/fold (fn [base-type type-arg] (|case type-arg - (&/$BoundT _) + (&/$Bound _) (&/$UnivQ &type/empty-env base-type) _ base-type)) - (&/$HostT class-name type-args) + (&/$Host class-name type-args) type-args)) ;; [Resources] (defn ^:private analyse-field-access-helper [obj-type gvars gtype] "(-> Type (List (^ java.lang.reflect.Type)) (^ java.lang.reflect.Type) (Lux Type))" (|case obj-type - (&/$HostT class targs) + (&/$Host class targs) (if (= (&/|length targs) (&/|length gvars)) (|let [gtype-env (&/fold2 (fn [m ^TypeVariable g t] (&/$Cons (&/T [(.getName g) t]) m)) (&/|table) @@ -186,25 +186,25 @@ (&/$GenericClass name params) (case name - "boolean" (return (&/$HostT "java.lang.Boolean" &/$Nil)) - "byte" (return (&/$HostT "java.lang.Byte" &/$Nil)) - "short" (return (&/$HostT "java.lang.Short" &/$Nil)) - "int" (return (&/$HostT "java.lang.Integer" &/$Nil)) - "long" (return (&/$HostT "java.lang.Long" &/$Nil)) - "float" (return (&/$HostT "java.lang.Float" &/$Nil)) - "double" (return (&/$HostT "java.lang.Double" &/$Nil)) - "char" (return (&/$HostT "java.lang.Character" &/$Nil)) - "void" (return &/$UnitT) + "boolean" (return (&/$Host "java.lang.Boolean" &/$Nil)) + "byte" (return (&/$Host "java.lang.Byte" &/$Nil)) + "short" (return (&/$Host "java.lang.Short" &/$Nil)) + "int" (return (&/$Host "java.lang.Integer" &/$Nil)) + "long" (return (&/$Host "java.lang.Long" &/$Nil)) + "float" (return (&/$Host "java.lang.Float" &/$Nil)) + "double" (return (&/$Host "java.lang.Double" &/$Nil)) + "char" (return (&/$Host "java.lang.Character" &/$Nil)) + "void" (return &/$Unit) ;; else (|do [=params (&/map% (partial generic-class->type env) params)] - (return (&/$HostT name =params)))) + (return (&/$Host name =params)))) (&/$GenericArray param) (|do [=param (generic-class->type env param)] - (return (&/$HostT &host-type/array-data-tag (&/|list =param)))) + (return (&/$Host &host-type/array-data-tag (&/|list =param)))) (&/$GenericWildcard _) - (return (&/$ExQ &/$Nil (&/$BoundT 1))) + (return (&/$ExQ &/$Nil (&/$Bound 1))) )) (defn gen-super-env [class-env supers class-decl] @@ -252,7 +252,7 @@ itype (generic-class->type full-env itype*)] (if (double-register-gclass? itype*) (&&env/with-local iname itype - (&&env/with-local "" &/$VoidT + (&&env/with-local "" &/$Void body*)) (&&env/with-local iname itype body*))))) @@ -260,12 +260,12 @@ (defn ^:private analyse-method [analyse class-decl class-env all-supers method] "(-> Analyser ClassDecl (List (, TypeVar Type)) (List SuperClassDecl) MethodSyntax (Lux MethodAnalysis))" (|let [[?cname ?cparams] class-decl - class-type (&/$HostT ?cname (&/|map &/|second class-env))] + class-type (&/$Host ?cname (&/|map &/|second class-env))] (|case method (&/$ConstructorMethodSyntax =privacy-modifier ?strict ?anns ?gvars ?exceptions ?inputs ?ctor-args ?body) (|do [method-env (make-type-env ?gvars) :let [full-env (&/|++ class-env method-env)] - :let [output-type &/$UnitT] + :let [output-type &/$Unit] =ctor-args (&/map% (fn [ctor-arg] (|do [:let [[ca-type ca-term] ctor-arg] =ca-type (generic-class->type full-env ca-type) @@ -383,10 +383,10 @@ )) (do-template [<name> <proc> <from-class> <to-class>] - (let [output-type (&/$HostT <to-class> &/$Nil)] + (let [output-type (&/$Host <to-class> &/$Nil)] (defn <name> [analyse exo-type _?value] (|do [:let [(&/$Cons ?value (&/$Nil)) _?value] - =value (&&/analyse-1 analyse (&/$HostT <from-class> &/$Nil) ?value) + =value (&&/analyse-1 analyse (&/$Host <from-class> &/$Nil) ?value) _ (&type/check exo-type output-type) _cursor &/cursor] (return (&/|list (&&/|meta output-type _cursor (&&/$proc (&/T ["jvm" <proc>]) (&/|list =value) (&/|list)))))))) @@ -423,11 +423,11 @@ ) (do-template [<name> <proc> <v1-class> <v2-class> <to-class>] - (let [output-type (&/$HostT <to-class> &/$Nil)] + (let [output-type (&/$Host <to-class> &/$Nil)] (defn <name> [analyse exo-type ?values] (|do [:let [(&/$Cons ?value1 (&/$Cons ?value2 (&/$Nil))) ?values] - =value1 (&&/analyse-1 analyse (&/$HostT <v1-class> &/$Nil) ?value1) - =value2 (&&/analyse-1 analyse (&/$HostT <v2-class> &/$Nil) ?value2) + =value1 (&&/analyse-1 analyse (&/$Host <v1-class> &/$Nil) ?value1) + =value2 (&&/analyse-1 analyse (&/$Host <v2-class> &/$Nil) ?value2) _ (&type/check exo-type output-type) _cursor &/cursor] (return (&/|list (&&/|meta output-type _cursor (&&/$proc (&/T ["jvm" <proc>]) (&/|list =value1 =value2) (&/|list)))))))) @@ -448,8 +448,8 @@ ) (do-template [<name> <proc> <input-class> <output-class>] - (let [input-type (&/$HostT <input-class> &/$Nil) - output-type (&/$HostT <output-class> &/$Nil)] + (let [input-type (&/$Host <input-class> &/$Nil) + output-type (&/$Host <output-class> &/$Nil)] (defn <name> [analyse exo-type ?values] (|do [:let [(&/$Cons x (&/$Cons y (&/$Nil))) ?values] =x (&&/analyse-1 analyse input-type x) @@ -503,8 +503,8 @@ (let [length-type &type/Nat idx-type &type/Nat] (do-template [<elem-class> <array-class> <new-name> <new-tag> <load-name> <load-tag> <store-name> <store-tag>] - (let [elem-type (&/$HostT <elem-class> &/$Nil) - array-type (&/$HostT <array-class> &/$Nil)] + (let [elem-type (&/$Host <elem-class> &/$Nil) + array-type (&/$Host <array-class> &/$Nil)] (defn <new-name> [analyse exo-type ?values] (|do [:let [(&/$Cons length (&/$Nil)) ?values] =length (&&/analyse-1 analyse length-type length) @@ -558,7 +558,7 @@ &&a-parser/parse-gclass) gtype-env &/get-type-env =gclass (&host-type/instance-gtype &type/existential gtype-env gclass) - :let [array-type (&/$HostT &host-type/array-data-tag (&/|list =gclass))] + :let [array-type (&/$Host &host-type/array-data-tag (&/|list =gclass))] =length (&&/analyse-1 analyse length-type length) _ (&type/check exo-type array-type) _cursor &/cursor] @@ -614,7 +614,7 @@ (defn ^:private analyse-jvm-null [analyse exo-type ?values] (|do [:let [(&/$Nil) ?values] - :let [output-type (&/$HostT &host-type/null-data-tag &/$Nil)] + :let [output-type (&/$Host &host-type/null-data-tag &/$Nil)] _ (&type/check exo-type output-type) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor @@ -632,7 +632,7 @@ (defn ^:private analyse-jvm-throw [analyse exo-type ?values] (|do [:let [(&/$Cons ?ex (&/$Nil)) ?values] =ex (&&/analyse-1+ analyse ?ex) - _ (&type/check (&/$HostT "java.lang.Throwable" &/$Nil) (&&/expr-type* =ex)) + _ (&type/check (&/$Host "java.lang.Throwable" &/$Nil) (&&/expr-type* =ex)) [throw-class throw-params] (ensure-object (&&/expr-type* =ex)) _cursor &/cursor _ (&type/check exo-type &type/Bottom)] @@ -673,7 +673,7 @@ :let [gclass (&host-type/gtype->gclass gtype)] =type (&host-type/instance-param &type/existential &/$Nil gtype) =value (&&/analyse-1 analyse =type value) - :let [output-type &/$UnitT] + :let [output-type &/$Unit] _ (&type/check exo-type output-type) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor @@ -690,7 +690,7 @@ :let [gclass (&host-type/gtype->gclass gtype)] =type (analyse-field-access-helper obj-type gvars gtype) =value (&&/analyse-1 analyse =type value) - :let [output-type &/$UnitT] + :let [output-type &/$Unit] _ (&type/check exo-type output-type) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor @@ -709,7 +709,7 @@ (&/$Cons ^TypeVariable gtv gtype-vars*) (&type/with-var (fn [$var] - (|do [:let [(&/$VarT _id) $var + (|do [:let [(&/$Var _id) $var gtype-env* (&/$Cons (&/T [(.getName gtv) $var]) gtype-env)] [=gret =args] (analyse-method-call-helper analyse exo-type gret gtype-env* gtype-vars* gtype-args args) ==gret (&type/clean $var =gret) @@ -717,7 +717,7 @@ (return (&/T [==gret ==args]))))) )) -(let [dummy-type-param (&/$HostT "java.lang.Object" &/$Nil)] +(let [dummy-type-param (&/$Host "java.lang.Object" &/$Nil)] (do-template [<name> <tag> <only-interface?>] (defn <name> [analyse exo-type class method classes ?values] (|do [!class! (&/de-alias-class class) @@ -735,10 +735,10 @@ (&host/lookup-virtual-method class-loader !class! method classes)) =object (&&/analyse-1+ analyse object) [sub-class sub-params] (ensure-object (&&/expr-type* =object)) - (&/$HostT super-class* super-params*) (&host-type/->super-type &type/existential class-loader !class! (if (= sub-class class) - !class! - sub-class) - sub-params) + (&/$Host super-class* super-params*) (&host-type/->super-type &type/existential class-loader !class! (if (= sub-class class) + !class! + sub-class) + sub-params) :let [gtype-env (&/fold2 (fn [m ^TypeVariable g t] (&/$Cons (&/T [(.getName g) t]) m)) (&/|table) parent-gvars @@ -811,7 +811,7 @@ (return nil)) (catch Exception e (&/fail-with-loc (str "[Analyser Error] Unknown class: " _class-name)))) - :let [output-type (&/$HostT "java.lang.Class" (&/|list (&/$HostT _class-name (&/|list))))] + :let [output-type (&/$Host "java.lang.Class" (&/|list (&/$Host _class-name (&/|list))))] _ (&type/check exo-type output-type) _cursor &/cursor] (return (&/|list (&&/|meta output-type _cursor @@ -822,7 +822,7 @@ _ (compile-interface interface-decl supers =anns =methods) :let [_ (println 'INTERFACE (str module "." (&/|first interface-decl)))] _cursor &/cursor] - (return (&/|list (&&/|meta &/$UnitT _cursor + (return (&/|list (&&/|meta &/$Unit _cursor (&&/$tuple (&/|list))))))) (defn ^:private analyse-jvm-class [analyse compile-class class-decl super-class interfaces =inheritance-modifier =anns ?fields methods] @@ -841,7 +841,7 @@ _ &/pop-dummy-name :let [_ (println 'CLASS full-name)] _cursor &/cursor] - (return (&/|list (&&/|meta &/$UnitT _cursor + (return (&/|list (&&/|meta &/$Unit _cursor (&&/$tuple (&/|list)))))))) (defn ^:private captured-source [env-entry] @@ -866,7 +866,7 @@ :let [name (->> scope &/|reverse &/|tail &host/location) class-decl (&/T [name &/$Nil]) anon-class (str (string/replace module "/" ".") "." name) - anon-class-type (&/$HostT anon-class &/$Nil)] + anon-class-type (&/$Host anon-class &/$Nil)] =ctor-args (&/map% (fn [ctor-arg] (|let [[arg-type arg-term] ctor-arg] (|do [=arg-term (&&/analyse-1+ analyse arg-term)] diff --git a/luxc/src/lux/analyser/record.clj b/luxc/src/lux/analyser/record.clj index 90be7d330..ac9a0e64d 100644 --- a/luxc/src/lux/analyser/record.clj +++ b/luxc/src/lux/analyser/record.clj @@ -11,7 +11,7 @@ "(-> (List (, Syntax Syntax)) (Lux (List Syntax)))" (|do [[tag-group tag-type] (|case pairs (&/$Nil) - (return (&/T [&/$Nil &/$UnitT])) + (return (&/T [&/$Nil &/$Unit])) (&/$Cons [[_ (&/$Tag tag1)] _] _) (|do [[module name] (&&/resolved-ident tag1) diff --git a/luxc/src/lux/base.clj b/luxc/src/lux/base.clj index 98b6ce4e8..6ce50c06f 100644 --- a/luxc/src/lux/base.clj +++ b/luxc/src/lux/base.clj @@ -86,19 +86,19 @@ ;; Type (defvariant - ("HostT" 2) - ("VoidT" 0) - ("UnitT" 0) - ("SumT" 2) - ("ProdT" 2) - ("FunctionT" 2) - ("BoundT" 1) - ("VarT" 1) - ("ExT" 1) + ("Host" 2) + ("Void" 0) + ("Unit" 0) + ("Sum" 2) + ("Product" 2) + ("Function" 2) + ("Bound" 1) + ("Var" 1) + ("Ex" 1) ("UnivQ" 2) ("ExQ" 2) - ("AppT" 2) - ("NamedT" 2)) + ("App" 2) + ("Named" 2)) ;; Vars (defvariant diff --git a/luxc/src/lux/compiler/cache/type.clj b/luxc/src/lux/compiler/cache/type.clj index 5715866f7..f6f06f03c 100644 --- a/luxc/src/lux/compiler/cache/type.clj +++ b/luxc/src/lux/compiler/cache/type.clj @@ -24,22 +24,22 @@ (if (clojure.lang.Util/identical &type/Type type) "T" (|case type - (&/$HostT name params) + (&/$Host name params) (str "^" name stop (serialize-list serialize-type params)) - (&/$VoidT) + (&/$Void) "0" - (&/$UnitT) + (&/$Unit) "1" - (&/$ProdT left right) + (&/$Product left right) (str "*" (serialize-type left) (serialize-type right)) - (&/$SumT left right) + (&/$Sum left right) (str "+" (serialize-type left) (serialize-type right)) - (&/$FunctionT left right) + (&/$Function left right) (str ">" (serialize-type left) (serialize-type right)) (&/$UnivQ env body) @@ -48,19 +48,19 @@ (&/$ExQ env body) (str "E" (serialize-list serialize-type env) (serialize-type body)) - (&/$BoundT idx) + (&/$Bound idx) (str "$" idx stop) - (&/$ExT idx) + (&/$Ex idx) (str "!" idx stop) - (&/$VarT idx) + (&/$Var idx) (str "?" idx stop) - (&/$AppT left right) + (&/$App left right) (str "%" (serialize-type left) (serialize-type right)) - (&/$NamedT [module name] type*) + (&/$Named [module name] type*) (str "@" module ident-separator name stop (serialize-type type*)) _ @@ -85,8 +85,8 @@ [<type> (.substring input 1)] )) - ^:private deserialize-void "0" &/$VoidT - ^:private deserialize-unit "1" &/$UnitT + ^:private deserialize-void "0" &/$Void + ^:private deserialize-unit "1" &/$Unit ^:private deserialize-type* "T" &type/Type ) @@ -98,10 +98,10 @@ [(<type> left right) input*])) )) - ^:private deserialize-sum "+" &/$SumT - ^:private deserialize-prod "*" &/$ProdT - ^:private deserialize-lambda ">" &/$FunctionT - ^:private deserialize-app "%" &/$AppT + ^:private deserialize-sum "+" &/$Sum + ^:private deserialize-prod "*" &/$Product + ^:private deserialize-lambda ">" &/$Function + ^:private deserialize-app "%" &/$App ) (do-template [<name> <signal> <type>] @@ -110,9 +110,9 @@ (let [[idx ^String input*] (.split (.substring input 1) stop 2)] [(<type> (Long/parseLong idx)) input*]))) - ^:private deserialize-bound "$" &/$BoundT - ^:private deserialize-ex "!" &/$ExT - ^:private deserialize-var "?" &/$VarT + ^:private deserialize-bound "$" &/$Bound + ^:private deserialize-ex "!" &/$Ex + ^:private deserialize-var "?" &/$Var ) (defn ^:private deserialize-named [^String input] @@ -120,7 +120,7 @@ (let [[^String module+name ^String input*] (.split (.substring input 1) stop 2) [module name] (.split module+name ident-separator 2)] (when-let [[type* ^String input*] (deserialize-type input*)] - [(&/$NamedT (&/T [module name]) type*) input*])))) + [(&/$Named (&/T [module name]) type*) input*])))) (do-template [<name> <signal> <type>] (defn <name> [^String input] @@ -137,7 +137,7 @@ (when (.startsWith input "^") (let [[name ^String input*] (.split (.substring input 1) stop 2)] (when-let [[params ^String input*] (deserialize-list input*)] - [(&/$HostT name params) input*])))) + [(&/$Host name params) input*])))) (defn deserialize-type "(-> Text Type)" diff --git a/luxc/src/lux/compiler/jvm/proc/host.clj b/luxc/src/lux/compiler/jvm/proc/host.clj index 2c5bbc6cd..94b7ca0d8 100644 --- a/luxc/src/lux/compiler/jvm/proc/host.clj +++ b/luxc/src/lux/compiler/jvm/proc/host.clj @@ -48,40 +48,40 @@ char-class "java.lang.Character"] (defn prepare-return! [^MethodVisitor *writer* *type*] (|case *type* - (&/$UnitT) + (&/$Unit) (.visitLdcInsn *writer* &/unit-tag) - (&/$HostT "boolean" (&/$Nil)) + (&/$Host "boolean" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name boolean-class) "valueOf" (str "(Z)" (&host-generics/->type-signature boolean-class))) - (&/$HostT "byte" (&/$Nil)) + (&/$Host "byte" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name byte-class) "valueOf" (str "(B)" (&host-generics/->type-signature byte-class))) - (&/$HostT "short" (&/$Nil)) + (&/$Host "short" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name short-class) "valueOf" (str "(S)" (&host-generics/->type-signature short-class))) - (&/$HostT "int" (&/$Nil)) + (&/$Host "int" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name int-class) "valueOf" (str "(I)" (&host-generics/->type-signature int-class))) - (&/$HostT "long" (&/$Nil)) + (&/$Host "long" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name long-class) "valueOf" (str "(J)" (&host-generics/->type-signature long-class))) - (&/$HostT "float" (&/$Nil)) + (&/$Host "float" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name float-class) "valueOf" (str "(F)" (&host-generics/->type-signature float-class))) - (&/$HostT "double" (&/$Nil)) + (&/$Host "double" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name double-class) "valueOf" (str "(D)" (&host-generics/->type-signature double-class))) - (&/$HostT "char" (&/$Nil)) + (&/$Host "char" (&/$Nil)) (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name char-class) "valueOf" (str "(C)" (&host-generics/->type-signature char-class))) - (&/$HostT _ _) + (&/$Host _ _) nil - (&/$NamedT ?name ?type) + (&/$Named ?name ?type) (prepare-return! *writer* ?type) - (&/$ExT _) + (&/$Ex _) nil _ diff --git a/luxc/src/lux/host.clj b/luxc/src/lux/host.clj index e222baf10..f602376fb 100644 --- a/luxc/src/lux/host.clj +++ b/luxc/src/lux/host.clj @@ -30,7 +30,7 @@ (defn unfold-array [type] "(-> Type (, Int Type))" (|case type - (&/$HostT "#Array" (&/$Cons param (&/$Nil))) + (&/$Host "#Array" (&/$Cons param (&/$Nil))) (|let [[count inner] (unfold-array param)] (&/T [(inc count) inner])) @@ -42,10 +42,10 @@ (defn ->java-sig [^objects type] "(-> Type (Lux Text))" (|case type - (&/$HostT ?name params) + (&/$Host ?name params) (cond (= &host-type/array-data-tag ?name) (|do [:let [[level base] (unfold-array type)] base-sig (|case base - (&/$HostT base-class _) + (&/$Host base-class _) (return (&host-generics/->type-signature base-class)) _ @@ -55,26 +55,26 @@ (= &host-type/null-data-tag ?name) (return (&host-generics/->type-signature "java.lang.Object")) :else (return (&host-generics/->type-signature ?name))) - (&/$FunctionT _ _) + (&/$Function _ _) (return (&host-generics/->type-signature function-class)) - (&/$UnitT) + (&/$Unit) (return "V") - (&/$SumT _) + (&/$Sum _) (return object-array) - (&/$ProdT _) + (&/$Product _) (return object-array) - (&/$NamedT ?name ?type) + (&/$Named ?name ?type) (->java-sig ?type) - (&/$AppT ?F ?A) + (&/$App ?F ?A) (|do [type* (&type/apply-type ?F ?A)] (->java-sig type*)) - (&/$ExT _) + (&/$Ex _) (return ex-type-class) _ diff --git a/luxc/src/lux/type.clj b/luxc/src/lux/type.clj index f69542442..85ce1613b 100644 --- a/luxc/src/lux/type.clj +++ b/luxc/src/lux/type.clj @@ -23,145 +23,145 @@ (def empty-env &/$Nil) -(def Bool (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "#Bool" &/$Nil))) -(def Nat (&/$NamedT (&/T ["lux" "Nat"]) (&/$HostT &&host/nat-data-tag &/$Nil))) -(def Deg (&/$NamedT (&/T ["lux" "Deg"]) (&/$HostT &&host/deg-data-tag &/$Nil))) -(def Int (&/$NamedT (&/T ["lux" "Int"]) (&/$HostT "#Int" &/$Nil))) -(def Real (&/$NamedT (&/T ["lux" "Real"]) (&/$HostT "#Real" &/$Nil))) -(def Char (&/$NamedT (&/T ["lux" "Char"]) (&/$HostT "#Char" &/$Nil))) -(def Text (&/$NamedT (&/T ["lux" "Text"]) (&/$HostT "#Text" &/$Nil))) -(def Ident (&/$NamedT (&/T ["lux" "Ident"]) (&/$ProdT Text Text))) +(def Bool (&/$Named (&/T ["lux" "Bool"]) (&/$Host "#Bool" &/$Nil))) +(def Nat (&/$Named (&/T ["lux" "Nat"]) (&/$Host &&host/nat-data-tag &/$Nil))) +(def Deg (&/$Named (&/T ["lux" "Deg"]) (&/$Host &&host/deg-data-tag &/$Nil))) +(def Int (&/$Named (&/T ["lux" "Int"]) (&/$Host "#Int" &/$Nil))) +(def Real (&/$Named (&/T ["lux" "Real"]) (&/$Host "#Real" &/$Nil))) +(def Char (&/$Named (&/T ["lux" "Char"]) (&/$Host "#Char" &/$Nil))) +(def Text (&/$Named (&/T ["lux" "Text"]) (&/$Host "#Text" &/$Nil))) +(def Ident (&/$Named (&/T ["lux" "Ident"]) (&/$Product Text Text))) (do-template [<name> <tag>] (defn <name> [elem-type] - (&/$HostT <tag> (&/|list elem-type))) + (&/$Host <tag> (&/|list elem-type))) Array "#Array" Atom "#Atom" ) (def Bottom - (&/$NamedT (&/T ["lux" "Bottom"]) - (&/$UnivQ empty-env - (&/$BoundT 1)))) + (&/$Named (&/T ["lux" "Bottom"]) + (&/$UnivQ empty-env + (&/$Bound 1)))) (def Top - (&/$NamedT (&/T ["lux" "Top"]) - (&/$ExQ empty-env - (&/$BoundT 1)))) + (&/$Named (&/T ["lux" "Top"]) + (&/$ExQ empty-env + (&/$Bound 1)))) (def IO - (&/$NamedT (&/T ["lux/codata" "IO"]) - (&/$UnivQ empty-env - (&/$FunctionT &/$VoidT (&/$BoundT 1))))) + (&/$Named (&/T ["lux/codata" "IO"]) + (&/$UnivQ empty-env + (&/$Function &/$Void (&/$Bound 1))))) (def List - (&/$NamedT (&/T ["lux" "List"]) - (&/$UnivQ empty-env - (&/$SumT - ;; lux;Nil - &/$UnitT - ;; lux;Cons - (&/$ProdT (&/$BoundT 1) - (&/$AppT (&/$BoundT 0) - (&/$BoundT 1))))))) + (&/$Named (&/T ["lux" "List"]) + (&/$UnivQ empty-env + (&/$Sum + ;; lux;Nil + &/$Unit + ;; lux;Cons + (&/$Product (&/$Bound 1) + (&/$App (&/$Bound 0) + (&/$Bound 1))))))) (def Maybe - (&/$NamedT (&/T ["lux" "Maybe"]) - (&/$UnivQ empty-env - (&/$SumT - ;; lux;None - &/$UnitT - ;; lux;Some - (&/$BoundT 1)) - ))) + (&/$Named (&/T ["lux" "Maybe"]) + (&/$UnivQ empty-env + (&/$Sum + ;; lux;None + &/$Unit + ;; lux;Some + (&/$Bound 1)) + ))) (def Type - (&/$NamedT (&/T ["lux" "Type"]) - (let [Type (&/$AppT (&/$BoundT 0) (&/$BoundT 1)) - TypeList (&/$AppT List Type) - TypePair (&/$ProdT Type Type)] - (&/$AppT (&/$UnivQ empty-env - (&/$SumT - ;; HostT - (&/$ProdT Text TypeList) - (&/$SumT - ;; VoidT - &/$UnitT - (&/$SumT - ;; UnitT - &/$UnitT - (&/$SumT - ;; SumT + (&/$Named (&/T ["lux" "Type"]) + (let [Type (&/$App (&/$Bound 0) (&/$Bound 1)) + TypeList (&/$App List Type) + TypePair (&/$Product Type Type)] + (&/$App (&/$UnivQ empty-env + (&/$Sum + ;; Host + (&/$Product Text TypeList) + (&/$Sum + ;; Void + &/$Unit + (&/$Sum + ;; Unit + &/$Unit + (&/$Sum + ;; Sum + TypePair + (&/$Sum + ;; Product + TypePair + (&/$Sum + ;; Function TypePair - (&/$SumT - ;; ProdT - TypePair - (&/$SumT - ;; FunctionT - TypePair - (&/$SumT - ;; BoundT + (&/$Sum + ;; Bound + Nat + (&/$Sum + ;; Var + Nat + (&/$Sum + ;; Ex Nat - (&/$SumT - ;; VarT - Nat - (&/$SumT - ;; ExT - Nat - (&/$SumT - ;; UnivQ - (&/$ProdT TypeList Type) - (&/$SumT - ;; ExQ - (&/$ProdT TypeList Type) - (&/$SumT - ;; AppT - TypePair - ;; NamedT - (&/$ProdT Ident Type))))))))))))) - ) - &/$VoidT)))) + (&/$Sum + ;; UnivQ + (&/$Product TypeList Type) + (&/$Sum + ;; ExQ + (&/$Product TypeList Type) + (&/$Sum + ;; App + TypePair + ;; Named + (&/$Product Ident Type))))))))))))) + ) + &/$Void)))) (def Ann-Value - (&/$NamedT (&/T ["lux" "Ann-Value"]) - (let [Ann-Value (&/$AppT (&/$BoundT 0) (&/$BoundT 1))] - (&/$AppT (&/$UnivQ empty-env - (&/$SumT - ;; BoolA - Bool - (&/$SumT - ;; NatA - Nat - (&/$SumT - ;; IntA - Int - (&/$SumT - ;; DegA - Deg - (&/$SumT - ;; RealA - Real - (&/$SumT - ;; CharA - Char - (&/$SumT - ;; TextA - Text - (&/$SumT - ;; IdentA - Ident - (&/$SumT - ;; ListA - (&/$AppT List Ann-Value) - ;; DictA - (&/$AppT List (&/$ProdT Text Ann-Value))))))))))) - ) - &/$VoidT)))) + (&/$Named (&/T ["lux" "Ann-Value"]) + (let [Ann-Value (&/$App (&/$Bound 0) (&/$Bound 1))] + (&/$App (&/$UnivQ empty-env + (&/$Sum + ;; BoolA + Bool + (&/$Sum + ;; NatA + Nat + (&/$Sum + ;; IntA + Int + (&/$Sum + ;; DegA + Deg + (&/$Sum + ;; RealA + Real + (&/$Sum + ;; CharA + Char + (&/$Sum + ;; TextA + Text + (&/$Sum + ;; IdentA + Ident + (&/$Sum + ;; ListA + (&/$App List Ann-Value) + ;; DictA + (&/$App List (&/$Product Text Ann-Value))))))))))) + ) + &/$Void)))) (def Anns - (&/$NamedT (&/T ["lux" "Anns"]) - (&/$AppT List (&/$ProdT Ident Ann-Value)))) + (&/$Named (&/T ["lux" "Anns"]) + (&/$App List (&/$Product Ident Ann-Value)))) (def Macro) @@ -196,7 +196,7 @@ (defn deref+ [type] (|case type - (&/$VarT id) + (&/$Var id) (deref id) _ @@ -270,7 +270,7 @@ (->> compiler (&/get$ &/$type-context) (&/get$ &/$ex-counter) - &/$ExT)))) + &/$Ex)))) (declare clean*) (defn delete-var [id] @@ -290,7 +290,7 @@ (&/$Some ?type*) (|case ?type* - (&/$VarT ?id*) + (&/$Var ?id*) (if (= id ?id*) (return (&/T [?id &/$None])) (return binding)) @@ -308,13 +308,13 @@ (defn with-var [k] (|do [id create-var - output (k (&/$VarT id)) + output (k (&/$Var id)) _ (delete-var id)] (return output))) (defn clean* [?tid type] (|case type - (&/$VarT ?id) + (&/$Var ?id) (if (= ?tid ?id) (|do [? (bound? ?id)] (if ? @@ -325,7 +325,7 @@ (|do [=type (deref ?id) ==type (clean* ?tid =type)] (|case ==type - (&/$VarT =id) + (&/$Var =id) (if (= ?tid =id) (|do [_ (unset-var ?id)] (return type)) @@ -338,38 +338,38 @@ (return type))) ) - (&/$HostT ?name ?params) + (&/$Host ?name ?params) (|do [=params (&/map% (partial clean* ?tid) ?params)] - (return (&/$HostT ?name =params))) + (return (&/$Host ?name =params))) - (&/$FunctionT ?arg ?return) + (&/$Function ?arg ?return) (|do [=arg (clean* ?tid ?arg) =return (clean* ?tid ?return)] - (return (&/$FunctionT =arg =return))) + (return (&/$Function =arg =return))) - (&/$AppT ?lambda ?param) + (&/$App ?lambda ?param) (|do [=lambda (clean* ?tid ?lambda) =param (clean* ?tid ?param)] - (return (&/$AppT =lambda =param))) + (return (&/$App =lambda =param))) - (&/$ProdT ?left ?right) + (&/$Product ?left ?right) (|do [=left (clean* ?tid ?left) =right (clean* ?tid ?right)] - (return (&/$ProdT =left =right))) + (return (&/$Product =left =right))) - (&/$SumT ?left ?right) + (&/$Sum ?left ?right) (|do [=left (clean* ?tid ?left) =right (clean* ?tid ?right)] - (return (&/$SumT =left =right))) + (return (&/$Sum =left =right))) (&/$UnivQ ?env ?body) (|do [=env (&/map% (partial clean* ?tid) ?env) - body* (clean* ?tid ?body)] ;; TODO: DON'T CLEAN THE BODY + body* (clean* ?tid ?body)] ;; TODO: DO NOT CLEAN THE BODY (return (&/$UnivQ =env body*))) (&/$ExQ ?env ?body) (|do [=env (&/map% (partial clean* ?tid) ?env) - body* (clean* ?tid ?body)] ;; TODO: DON'T CLEAN THE BODY + body* (clean* ?tid ?body)] ;; TODO: DO NOT CLEAN THE BODY (return (&/$ExQ =env body*))) _ @@ -378,7 +378,7 @@ (defn clean [tvar type] (|case tvar - (&/$VarT ?id) + (&/$Var ?id) (clean* ?id type) _ @@ -386,7 +386,7 @@ (defn ^:private unravel-fun [type] (|case type - (&/$FunctionT ?in ?out) + (&/$Function ?in ?out) (|let [[??out ?args] (unravel-fun ?out)] (&/T [??out (&/$Cons ?in ?args)])) @@ -395,7 +395,7 @@ (defn ^:private unravel-app [fun-type] (|case fun-type - (&/$AppT ?left ?right) + (&/$App ?left ?right) (|let [[?fun-type ?args] (unravel-app ?left)] (&/T [?fun-type (&/|++ ?args (&/|list ?right))])) @@ -415,7 +415,7 @@ (defn <at> [tag type] "(-> Int Type (Lux Type))" (|case type - (&/$NamedT ?name ?type) + (&/$Named ?name ?type) (<at> tag ?type) (<tag> ?left ?right) @@ -429,8 +429,8 @@ _ (&/fail-with-loc (str "[Type Error] Type is not a " <desc> ": " (show-type type)))))) - &/$SumT flatten-sum sum-at "Sum" - &/$ProdT flatten-prod prod-at "Product" + &/$Sum flatten-sum sum-at "Sum" + &/$Product flatten-prod prod-at "Product" ) (do-template [<name> <ctor> <unit>] @@ -443,13 +443,13 @@ (&/$Nil) <unit>)) - Variant$ &/$SumT &/$VoidT - Tuple$ &/$ProdT &/$UnitT + Variant$ &/$Sum &/$Void + Tuple$ &/$Product &/$Unit ) (defn show-type [^objects type] (|case type - (&/$HostT name params) + (&/$Host name params) (|case params (&/$Nil) (str "(host " name ")") @@ -457,32 +457,32 @@ _ (str "(host " name " " (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")) - (&/$VoidT) + (&/$Void) "Void" - (&/$UnitT) + (&/$Unit) "Unit" - (&/$ProdT _) + (&/$Product _) (str "[" (->> (flatten-prod type) (&/|map show-type) (&/|interpose " ") (&/fold str "")) "]") - (&/$SumT _) + (&/$Sum _) (str "(| " (->> (flatten-sum type) (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")") - (&/$FunctionT input output) + (&/$Function input output) (|let [[?out ?ins] (unravel-fun type)] (str "(-> " (->> ?ins (&/|map show-type) (&/|interpose " ") (&/fold str "")) " " (show-type ?out) ")")) - (&/$VarT id) + (&/$Var id) (str "⌈v:" id "⌋") - (&/$ExT ?id) + (&/$Ex ?id) (str "⟨e:" ?id "⟩") - (&/$BoundT idx) + (&/$Bound idx) (str idx) - (&/$AppT _ _) + (&/$App _ _) (|let [[?call-fun ?call-args] (unravel-app type)] (str "(" (show-type ?call-fun) " " (->> ?call-args (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")) @@ -494,7 +494,7 @@ (str "(Ex " "{" (->> ?env (&/|map show-type) (&/|interpose " ") (&/fold str "")) "} " (show-type ?body) ")") - (&/$NamedT ?name ?type) + (&/$Named ?name ?type) (&/ident->text ?name) _ @@ -503,52 +503,52 @@ (defn type= [x y] (or (clojure.lang.Util/identical x y) (let [output (|case [x y] - [(&/$NamedT [?xmodule ?xname] ?xtype) (&/$NamedT [?ymodule ?yname] ?ytype)] + [(&/$Named [?xmodule ?xname] ?xtype) (&/$Named [?ymodule ?yname] ?ytype)] (and (= ?xmodule ?ymodule) (= ?xname ?yname)) - [(&/$HostT xname xparams) (&/$HostT yname yparams)] + [(&/$Host xname xparams) (&/$Host yname yparams)] (and (.equals ^Object xname yname) (= (&/|length xparams) (&/|length yparams)) (&/fold2 #(and %1 (type= %2 %3)) true xparams yparams)) - [(&/$VoidT) (&/$VoidT)] + [(&/$Void) (&/$Void)] true - [(&/$UnitT) (&/$UnitT)] + [(&/$Unit) (&/$Unit)] true - [(&/$ProdT xL xR) (&/$ProdT yL yR)] + [(&/$Product xL xR) (&/$Product yL yR)] (and (type= xL yL) (type= xR yR)) - [(&/$SumT xL xR) (&/$SumT yL yR)] + [(&/$Sum xL xR) (&/$Sum yL yR)] (and (type= xL yL) (type= xR yR)) - [(&/$FunctionT xinput xoutput) (&/$FunctionT yinput youtput)] + [(&/$Function xinput xoutput) (&/$Function yinput youtput)] (and (type= xinput yinput) (type= xoutput youtput)) - [(&/$VarT xid) (&/$VarT yid)] + [(&/$Var xid) (&/$Var yid)] (= xid yid) - [(&/$BoundT xidx) (&/$BoundT yidx)] + [(&/$Bound xidx) (&/$Bound yidx)] (= xidx yidx) - [(&/$ExT xid) (&/$ExT yid)] + [(&/$Ex xid) (&/$Ex yid)] (= xid yid) - [(&/$AppT xlambda xparam) (&/$AppT ylambda yparam)] + [(&/$App xlambda xparam) (&/$App ylambda yparam)] (and (type= xlambda ylambda) (type= xparam yparam)) [(&/$UnivQ xenv xbody) (&/$UnivQ yenv ybody)] (type= xbody ybody) - [(&/$NamedT ?xname ?xtype) _] + [(&/$Named ?xname ?xtype) _] (type= ?xtype y) - [_ (&/$NamedT ?yname ?ytype)] + [_ (&/$Named ?yname ?ytype)] (type= x ?ytype) [_ _] @@ -574,7 +574,7 @@ (defn show-type+ [type] (|case type - (&/$VarT ?id) + (&/$Var ?id) (fn [state] (|case ((deref ?id) state) (&/$Right state* bound) @@ -597,17 +597,17 @@ (defn beta-reduce [env type] (|case type - (&/$HostT ?name ?params) - (&/$HostT ?name (&/|map (partial beta-reduce env) ?params)) + (&/$Host ?name ?params) + (&/$Host ?name (&/|map (partial beta-reduce env) ?params)) - (&/$SumT ?left ?right) - (&/$SumT (beta-reduce env ?left) (beta-reduce env ?right)) + (&/$Sum ?left ?right) + (&/$Sum (beta-reduce env ?left) (beta-reduce env ?right)) - (&/$ProdT ?left ?right) - (&/$ProdT (beta-reduce env ?left) (beta-reduce env ?right)) + (&/$Product ?left ?right) + (&/$Product (beta-reduce env ?left) (beta-reduce env ?right)) - (&/$AppT ?type-fn ?type-arg) - (&/$AppT (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)) + (&/$App ?type-fn ?type-arg) + (&/$App (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)) (&/$UnivQ ?local-env ?local-def) (|case ?local-env @@ -625,10 +625,10 @@ _ type) - (&/$FunctionT ?input ?output) - (&/$FunctionT (beta-reduce env ?input) (beta-reduce env ?output)) + (&/$Function ?input ?output) + (&/$Function (beta-reduce env ?input) (beta-reduce env ?output)) - (&/$BoundT ?idx) + (&/$Bound ?idx) (|case (&/|at ?idx env) (&/$Some bound) (beta-reduce env bound) @@ -654,18 +654,18 @@ (&/$Cons type-fn)) local-def)) - (&/$AppT F A) + (&/$App F A) (|do [type-fn* (apply-type F A)] (apply-type type-fn* param)) - (&/$NamedT ?name ?type) + (&/$Named ?name ?type) (apply-type ?type param) ;; TODO: This one must go... - (&/$ExT id) - (return (&/$AppT type-fn param)) + (&/$Ex id) + (return (&/$App type-fn param)) - (&/$VarT id) + (&/$Var id) (|do [=type-fun (deref id)] (apply-type =type-fun param)) @@ -679,7 +679,7 @@ (return fixpoints) (&/with-attempt (|case [expected actual] - [(&/$VarT ?eid) (&/$VarT ?aid)] + [(&/$Var ?eid) (&/$Var ?aid)] (if (= ?eid ?aid) (return fixpoints) (|do [ebound (fn [state] @@ -710,7 +710,7 @@ [(&/$Some etype) (&/$Some atype)] (check* fixpoints invariant?? etype atype)))) - [(&/$VarT ?id) _] + [(&/$Var ?id) _] (fn [state] (|case ((set-var ?id actual) state) (&/$Right state* _) @@ -721,7 +721,7 @@ (check* fixpoints invariant?? bound actual)) state))) - [_ (&/$VarT ?id)] + [_ (&/$Var ?id)] (fn [state] (|case ((set-var ?id expected) state) (&/$Right state* _) @@ -732,15 +732,15 @@ (check* fixpoints invariant?? expected bound)) state))) - [(&/$AppT (&/$ExT eid) eA) (&/$AppT (&/$ExT aid) aA)] + [(&/$App (&/$Ex eid) eA) (&/$App (&/$Ex aid) aA)] (if (= eid aid) (check* fixpoints invariant?? eA aA) (check-error "" expected actual)) - [(&/$AppT (&/$VarT ?id) A1) (&/$AppT F2 A2)] + [(&/$App (&/$Var ?id) A1) (&/$App F2 A2)] (fn [state] (|case ((|do [F1 (deref ?id)] - (check* fixpoints invariant?? (&/$AppT F1 A1) actual)) + (check* fixpoints invariant?? (&/$App F1 A1) actual)) state) (&/$Right state* output) (return* state* output) @@ -752,34 +752,34 @@ (check* fixpoints invariant?? expected actual*)) state) - (&/$ExT _) - ((|do [fixpoints* (check* fixpoints invariant?? (&/$VarT ?id) F2)] + (&/$Ex _) + ((|do [fixpoints* (check* fixpoints invariant?? (&/$Var ?id) F2)] (check* fixpoints* invariant?? A1 A2)) state) _ - ((|do [fixpoints* (check* fixpoints invariant?? (&/$VarT ?id) F2) + ((|do [fixpoints* (check* fixpoints invariant?? (&/$Var ?id) F2) e* (apply-type F2 A1) a* (apply-type F2 A2)] (check* fixpoints* invariant?? e* a*)) state)))) - [(&/$AppT F1 A1) (&/$AppT (&/$VarT ?id) A2)] + [(&/$App F1 A1) (&/$App (&/$Var ?id) A2)] (fn [state] (|case ((|do [F2 (deref ?id)] - (check* fixpoints invariant?? expected (&/$AppT F2 A2))) + (check* fixpoints invariant?? expected (&/$App F2 A2))) state) (&/$Right state* output) (return* state* output) (&/$Left _) - ((|do [fixpoints* (check* fixpoints invariant?? F1 (&/$VarT ?id)) + ((|do [fixpoints* (check* fixpoints invariant?? F1 (&/$Var ?id)) e* (apply-type F1 A1) a* (apply-type F1 A2)] (check* fixpoints* invariant?? e* a*)) state))) - [(&/$AppT F A) _] + [(&/$App F A) _] (let [fp-pair (&/T [expected actual]) _ (when (> (&/|length fixpoints) 64) (&/|log! (println-str 'FIXPOINTS (->> (&/|keys fixpoints) @@ -789,7 +789,7 @@ (show-type a))))) (&/|interpose "\n\n") (&/fold str "")))) - (assert false (prn-str 'check* '[(&/$AppT F A) _] (&/|length fixpoints) (show-type expected) (show-type actual))))] + (assert false (prn-str 'check* '[(&/$App F A) _] (&/|length fixpoints) (show-type expected) (show-type actual))))] (|case (fp-get fp-pair fixpoints) (&/$Some ?) (if ? @@ -800,10 +800,10 @@ (|do [expected* (apply-type F A)] (check* (fp-put fp-pair true fixpoints) invariant?? expected* actual)))) - [_ (&/$AppT (&/$ExT aid) A)] + [_ (&/$App (&/$Ex aid) A)] (check-error "" expected actual) - [_ (&/$AppT F A)] + [_ (&/$App F A)] (|do [actual* (apply-type F A)] (check* fixpoints invariant?? expected actual*)) @@ -833,7 +833,7 @@ actual* (apply-type actual $arg)] (check* fixpoints invariant?? expected actual*)) - [(&/$HostT e!data) (&/$HostT a!data)] + [(&/$Host e!data) (&/$Host a!data)] (|do [? &/jvm?] (if ? (|do [class-loader &/loader] @@ -853,33 +853,33 @@ (return fixpoints)) (check-error "" expected actual))))) - [(&/$VoidT) (&/$VoidT)] + [(&/$Void) (&/$Void)] (return fixpoints) - [(&/$UnitT) (&/$UnitT)] + [(&/$Unit) (&/$Unit)] (return fixpoints) - [(&/$FunctionT eI eO) (&/$FunctionT aI aO)] + [(&/$Function eI eO) (&/$Function aI aO)] (|do [fixpoints* (check* fixpoints invariant?? aI eI)] (check* fixpoints* invariant?? eO aO)) - [(&/$ProdT eL eR) (&/$ProdT aL aR)] + [(&/$Product eL eR) (&/$Product aL aR)] (|do [fixpoints* (check* fixpoints invariant?? eL aL)] (check* fixpoints* invariant?? eR aR)) - [(&/$SumT eL eR) (&/$SumT aL aR)] + [(&/$Sum eL eR) (&/$Sum aL aR)] (|do [fixpoints* (check* fixpoints invariant?? eL aL)] (check* fixpoints* invariant?? eR aR)) - [(&/$ExT e!id) (&/$ExT a!id)] + [(&/$Ex e!id) (&/$Ex a!id)] (if (= e!id a!id) (return fixpoints) (check-error "" expected actual)) - [(&/$NamedT _ ?etype) _] + [(&/$Named _ ?etype) _] (check* fixpoints invariant?? ?etype actual) - [_ (&/$NamedT _ ?atype)] + [_ (&/$Named _ ?atype)] (check* fixpoints invariant?? expected ?atype) [_ _] @@ -894,15 +894,15 @@ (defn actual-type [type] "(-> Type (Lux Type))" (|case type - (&/$AppT ?all ?param) + (&/$App ?all ?param) (|do [type* (apply-type ?all ?param)] (actual-type type*)) - (&/$VarT id) + (&/$Var id) (|do [=type (deref id)] (actual-type =type)) - (&/$NamedT ?name ?type) + (&/$Named ?name ?type) (actual-type ?type) _ @@ -912,7 +912,7 @@ (defn type-name [type] "(-> Type (Lux Ident))" (|case type - (&/$NamedT name _) + (&/$Named name _) (return name) _ @@ -922,7 +922,7 @@ (defn unknown? [type] "(-> Type (Lux Bool))" (|case type - (&/$VarT id) + (&/$Var id) (|do [? (bound? id)] (return (not ?))) @@ -932,7 +932,7 @@ (defn resolve-type [type] "(-> Type (Lux Type))" (|case type - (&/$VarT id) + (&/$Var id) (|do [? (bound? id)] (if ? (deref id) @@ -949,7 +949,7 @@ (&/T [size-members (&/|++ (&/|take (dec size-members) ?member-types) (&/|list (|case (->> ?member-types (&/|drop (dec size-members)) (&/|reverse)) (&/$Cons last prevs) - (&/fold (fn [right left] (&/$ProdT left right)) + (&/fold (fn [right left] (&/$Product left right)) last prevs))))]) (&/T [size-types ?member-types]) ))) @@ -966,48 +966,48 @@ (&/$Cons last prevs) (&/fold (fn [r l] (<plus> l r)) last prevs))) - fold-prod &/$UnitT &/$ProdT - fold-sum &/$VoidT &/$SumT + fold-prod &/$Unit &/$Product + fold-sum &/$Void &/$Sum ) (def create-var+ (|do [id create-var] - (return (&/$VarT id)))) + (return (&/$Var id)))) (defn ^:private push-app [inf-type inf-var] (|case inf-type - (&/$AppT inf-type* inf-var*) - (&/$AppT (push-app inf-type* inf-var) inf-var*) + (&/$App inf-type* inf-var*) + (&/$App (push-app inf-type* inf-var) inf-var*) _ - (&/$AppT inf-type inf-var))) + (&/$App inf-type inf-var))) (defn ^:private push-name [name inf-type] (|case inf-type - (&/$AppT inf-type* inf-var*) - (&/$AppT (push-name name inf-type*) inf-var*) + (&/$App inf-type* inf-var*) + (&/$App (push-name name inf-type*) inf-var*) _ - (&/$NamedT name inf-type))) + (&/$Named name inf-type))) (defn ^:private push-univq [env inf-type] (|case inf-type - (&/$AppT inf-type* inf-var*) - (&/$AppT (push-univq env inf-type*) inf-var*) + (&/$App inf-type* inf-var*) + (&/$App (push-univq env inf-type*) inf-var*) _ (&/$UnivQ env inf-type))) (defn instantiate-inference [type] (|case type - (&/$NamedT ?name ?type) + (&/$Named ?name ?type) (|do [output (instantiate-inference ?type)] (return (push-name ?name output))) (&/$UnivQ _aenv _abody) (|do [inf-var create-var output (instantiate-inference _abody)] - (return (push-univq _aenv (push-app output (&/$VarT inf-var))))) + (return (push-univq _aenv (push-app output (&/$Var inf-var))))) _ (return type))) diff --git a/luxc/src/lux/type/host.clj b/luxc/src/lux/type/host.clj index e2f7c1c1f..7d894b4df 100644 --- a/luxc/src/lux/type/host.clj +++ b/luxc/src/lux/type/host.clj @@ -77,18 +77,18 @@ (let [gclass-name (.getName class)] (case gclass-name ("[Z" "[B" "[S" "[I" "[J" "[F" "[D" "[C") - (&/$HostT gclass-name (&/|list)) + (&/$Host gclass-name (&/|list)) ;; else (if-let [[_ _ arr-obrackets arr-obase simple-base arr-pbrackets arr-pbase] (re-find class-name-re gclass-name)] (let [base (or arr-obase simple-base (jprim->lprim arr-pbase))] (if (.equals "void" base) - &/$UnitT - (reduce (fn [inner _] (&/$HostT array-data-tag (&/|list inner))) - (&/$HostT base (try (-> (Class/forName base) .getTypeParameters - seq count (repeat (&/$HostT "java.lang.Object" &/$Nil)) - &/->list) - (catch Exception e - (&/|list)))) + &/$Unit + (reduce (fn [inner _] (&/$Host array-data-tag (&/|list inner))) + (&/$Host base (try (-> (Class/forName base) .getTypeParameters + seq count (repeat (&/$Host "java.lang.Object" &/$Nil)) + &/->list) + (catch Exception e + (&/|list)))) (range (count (or arr-obrackets arr-pbrackets ""))))) )))))) @@ -99,7 +99,7 @@ (instance? GenericArrayType refl-type) (|do [inner-type (instance-param existential matchings (.getGenericComponentType ^GenericArrayType refl-type))] - (return (&/$HostT array-data-tag (&/|list inner-type)))) + (return (&/$Host array-data-tag (&/|list inner-type)))) (instance? ParameterizedType refl-type) (|do [:let [refl-type* ^ParameterizedType refl-type] @@ -107,8 +107,8 @@ .getActualTypeArguments seq &/->list (&/map% (partial instance-param existential matchings)))] - (return (&/$HostT (->> refl-type* ^Class (.getRawType) .getName) - params*))) + (return (&/$Host (->> refl-type* ^Class (.getRawType) .getName) + params*))) (instance? TypeVariable refl-type) (let [gvar (.getName ^TypeVariable refl-type)] @@ -127,13 +127,13 @@ (defn principal-class [refl-type] (cond (instance? Class refl-type) (|case (class->type refl-type) - (&/$HostT "#Array" (&/$Cons (&/$HostT class-name _) (&/$Nil))) + (&/$Host "#Array" (&/$Cons (&/$Host class-name _) (&/$Nil))) (str "[" (&host-generics/->type-signature class-name)) - (&/$HostT class-name _) + (&/$Host class-name _) (&host-generics/->type-signature class-name) - (&/$UnitT) + (&/$Unit) "V") (instance? GenericArrayType refl-type) @@ -157,7 +157,7 @@ (|case gtype (&/$GenericArray component-type) (|do [inner-type (instance-gtype existential matchings component-type)] - (return (&/$HostT array-data-tag (&/|list inner-type)))) + (return (&/$Host array-data-tag (&/|list inner-type)))) (&/$GenericClass type-name type-params) ;; When referring to type-parameters during class or method @@ -171,7 +171,7 @@ (return m-type) (|do [params* (&/map% (partial instance-gtype existential matchings) type-params)] - (return (&/$HostT type-name params*)))) + (return (&/$Host type-name params*)))) (&/$GenericTypeVar var-name) (if-let [m-type (&/|get var-name matchings)] @@ -232,7 +232,7 @@ (if (.isAssignableFrom super-class+ sub-class+) (let [lineage (trace-lineage sub-class+ super-class+)] (|do [[^Class sub-class* sub-params*] (raise existential lineage sub-class+ sub-params)] - (return (&/$HostT (.getName sub-class*) sub-params*)))) + (return (&/$Host (.getName sub-class*) sub-params*)))) (&/fail-with-loc (str "[Host Error] Classes do not have a subtyping relationship: " sub-class " </= " super-class))))) (defn as-obj [class] @@ -271,7 +271,7 @@ (if (= (&/|length e!params) (&/|length a!params)) (|do [_ (&/map2% check e!params a!params)] (return fixpoints)) - (check-error "" (&/$HostT e!name e!params) (&/$HostT a!name a!params))) + (check-error "" (&/$Host e!name e!params) (&/$Host a!name a!params))) (or (lux-type? e!name) (lux-type? a!name)) @@ -280,14 +280,14 @@ (and (not (primitive-type? e!name)) (= null-data-tag a!name))) (return fixpoints) - (check-error "" (&/$HostT e!name e!params) (&/$HostT a!name a!params))) + (check-error "" (&/$Host e!name e!params) (&/$Host a!name a!params))) (not invariant??) (|do [actual* (->super-type existential class-loader e!name a!name a!params)] - (check (&/$HostT e!name e!params) actual*)) + (check (&/$Host e!name e!params) actual*)) :else - (check-error "" (&/$HostT e!name e!params) (&/$HostT a!name a!params)))) + (check-error "" (&/$Host e!name e!params) (&/$Host a!name a!params)))) (catch Exception e (throw e))))) |