diff options
Diffstat (limited to 'luxc')
-rw-r--r-- | luxc/src/lux/analyser/base.clj | 2 | ||||
-rw-r--r-- | luxc/src/lux/analyser/case.clj | 18 | ||||
-rw-r--r-- | luxc/src/lux/analyser/lux.clj | 8 | ||||
-rw-r--r-- | luxc/src/lux/analyser/proc/common.clj | 18 | ||||
-rw-r--r-- | luxc/src/lux/analyser/proc/jvm.clj | 2 | ||||
-rw-r--r-- | luxc/src/lux/base.clj | 2 | ||||
-rw-r--r-- | luxc/src/lux/compiler/cache/type.clj | 4 | ||||
-rw-r--r-- | luxc/src/lux/host.clj | 2 | ||||
-rw-r--r-- | luxc/src/lux/type.clj | 185 |
9 files changed, 121 insertions, 120 deletions
diff --git a/luxc/src/lux/analyser/base.clj b/luxc/src/lux/analyser/base.clj index e762c3870..b71df2b1f 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 #{"Host" "Void" "Unit" "Sum" "Product" "Function" "Bound" "Var" "Ex" "UnivQ" "ExQ" "App" "Named"}] +(let [tag-names #{"Host" "Void" "Unit" "Sum" "Product" "Function" "Bound" "Var" "Ex" "UnivQ" "ExQ" "Apply" "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 613e415f5..c60059540 100644 --- a/luxc/src/lux/analyser/case.clj +++ b/luxc/src/lux/analyser/case.clj @@ -78,9 +78,9 @@ (&/$Function (clean! level ?tid bound-idx ?arg) (clean! level ?tid bound-idx ?return)) - (&/$App ?lambda ?param) - (&/$App (clean! level ?tid bound-idx ?lambda) - (clean! level ?tid bound-idx ?param)) + (&/$Apply ?param ?lambda) + (&/$Apply (clean! level ?tid bound-idx ?param) + (clean! level ?tid bound-idx ?lambda)) (&/$Product ?left ?right) (&/$Product (clean! level ?tid bound-idx ?left) @@ -115,9 +115,9 @@ (&/$Product (beta-reduce! level env ?left) (beta-reduce! level env ?right)) - (&/$App ?type-fn ?type-arg) - (&/$App (beta-reduce! level env ?type-fn) - (beta-reduce! level env ?type-arg)) + (&/$Apply ?type-arg ?type-fn) + (&/$Apply (beta-reduce! level env ?type-arg) + (beta-reduce! level env ?type-fn)) (&/$UnivQ ?local-env ?local-def) (|case ?local-env @@ -165,7 +165,7 @@ (&/$Cons type-fn)) local-def)) - (&/$App F A) + (&/$Apply A F) (|do [type-fn* (apply-type! F A)] (apply-type! type-fn* param)) @@ -173,7 +173,7 @@ (apply-type! ?type param) (&/$Ex id) - (return (&/$App type-fn param)) + (return (&/$Apply param type-fn)) (&/$Var id) (|do [=type-fun (deref id)] @@ -229,7 +229,7 @@ (return (&type/Variant$ (&/|map distributor (&type/flatten-sum =type))))) - (&/$App ?tfun ?targ) + (&/$Apply ?targ ?tfun) (|do [=type (apply-type! ?tfun ?targ)] (adjust-type* up =type)) diff --git a/luxc/src/lux/analyser/lux.clj b/luxc/src/lux/analyser/lux.clj index 2a76ec86a..b2292d879 100644 --- a/luxc/src/lux/analyser/lux.clj +++ b/luxc/src/lux/analyser/lux.clj @@ -411,7 +411,7 @@ (defn ^:private unravel-inf-appt [type] (|case type - (&/$App =input+ (&/$Var _inf-var)) + (&/$Apply (&/$Var _inf-var) =input+) (&/$Cons _inf-var (unravel-inf-appt =input+)) _ @@ -426,7 +426,7 @@ =func** (&type/clean $output =func*)] (return (&/$UnivQ &/$Nil =func**))) - (&/$App =input+ (&/$Var _inf-var)) + (&/$Apply (&/$Var _inf-var) =input+) (&/fold% (fn [_func _inf-var] (|do [:let [$inf-var (&/$Var _inf-var)] =inf-var (&type/resolve-type $inf-var) @@ -683,8 +683,8 @@ =value (&&/analyse-1+ analyse ?value)] (return (&/|list (coerce ==type =value))))) -(let [input-type (&/$App &type/List &type/Text) - output-type (&/$App &type/IO &/$Unit)] +(let [input-type (&/$Apply &type/Text &type/List) + output-type (&/$Apply &/$Unit &type/IO)] (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 a0430feb7..0695de2a6 100644 --- a/luxc/src/lux/analyser/proc/common.clj +++ b/luxc/src/lux/analyser/proc/common.clj @@ -21,7 +21,7 @@ (&type/with-var (fn [$var] (|do [:let [(&/$Cons op (&/$Nil)) ?values] - =op (&&/analyse-1 analyse (&/$App &type/IO $var) op) + =op (&&/analyse-1 analyse (&/$Apply $var &type/IO) op) _ (&type/check exo-type (&/$Sum &type/Text ;; lux;Left $var ;; lux;Right )) @@ -57,8 +57,8 @@ (&/|list =text =part =start) (&/|list))))))) - ^:private analyse-text-index "index" (&/$App &type/Maybe &type/Nat) - ^:private analyse-text-last-index "last-index" (&/$App &type/Maybe &type/Nat) + ^:private analyse-text-index "index" (&/$Apply &type/Nat &type/Maybe) + ^:private analyse-text-last-index "last-index" (&/$Apply &type/Nat &type/Maybe) ) (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 (&/$App &type/Maybe &type/Text)) + _ (&type/check exo-type (&/$Apply &type/Text &type/Maybe)) _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 (&/$App &type/Maybe &type/Char)) + _ (&type/check exo-type (&/$Apply &type/Char &type/Maybe)) _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 (&/$App &type/Maybe <type>)] + (let [decode-type (&/$Apply <type> &type/Maybe)] (defn <decode> [analyse exo-type ?values] (|do [:let [(&/$Cons x (&/$Nil)) ?values] =x (&&/analyse-1 analyse &type/Text x) @@ -331,7 +331,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 (&/$App &type/Maybe $var)) + _ (&type/check exo-type (&/$Apply $var &type/Maybe)) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor (&&/$proc (&/T ["array" "get"]) (&/|list =array =idx) (&/|list))))))))) @@ -465,7 +465,7 @@ (defn ^:private analyse-process-future [analyse exo-type ?values] (|do [:let [(&/$Cons ?procedure (&/$Nil)) ?values] - =procedure (&&/analyse-1 analyse (&/$App &type/IO &type/Top) ?procedure) + =procedure (&&/analyse-1 analyse (&/$Apply &type/Top &type/IO) ?procedure) _ (&type/check exo-type &/$Unit) _cursor &/cursor] (return (&/|list (&&/|meta exo-type _cursor @@ -474,7 +474,7 @@ (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 (&/$App &type/IO &type/Top) ?procedure) + =procedure (&&/analyse-1 analyse (&/$Apply &type/Top &type/IO) ?procedure) _ (&type/check exo-type &/$Unit) _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 977c07787..910f5c72f 100644 --- a/luxc/src/lux/analyser/proc/jvm.clj +++ b/luxc/src/lux/analyser/proc/jvm.clj @@ -39,7 +39,7 @@ (&/$ExQ _ type*) (ensure-object type*) - (&/$App F A) + (&/$Apply A F) (|do [type* (&type/apply-type F A)] (ensure-object type*)) diff --git a/luxc/src/lux/base.clj b/luxc/src/lux/base.clj index 87d6786e5..2f2d879fe 100644 --- a/luxc/src/lux/base.clj +++ b/luxc/src/lux/base.clj @@ -97,7 +97,7 @@ ("Ex" 1) ("UnivQ" 2) ("ExQ" 2) - ("App" 2) + ("Apply" 2) ("Named" 2)) ;; Vars diff --git a/luxc/src/lux/compiler/cache/type.clj b/luxc/src/lux/compiler/cache/type.clj index f6f06f03c..04fb01540 100644 --- a/luxc/src/lux/compiler/cache/type.clj +++ b/luxc/src/lux/compiler/cache/type.clj @@ -57,7 +57,7 @@ (&/$Var idx) (str "?" idx stop) - (&/$App left right) + (&/$Apply left right) (str "%" (serialize-type left) (serialize-type right)) (&/$Named [module name] type*) @@ -101,7 +101,7 @@ ^:private deserialize-sum "+" &/$Sum ^:private deserialize-prod "*" &/$Product ^:private deserialize-lambda ">" &/$Function - ^:private deserialize-app "%" &/$App + ^:private deserialize-app "%" &/$Apply ) (do-template [<name> <signal> <type>] diff --git a/luxc/src/lux/host.clj b/luxc/src/lux/host.clj index f602376fb..7ee553d53 100644 --- a/luxc/src/lux/host.clj +++ b/luxc/src/lux/host.clj @@ -70,7 +70,7 @@ (&/$Named ?name ?type) (->java-sig ?type) - (&/$App ?F ?A) + (&/$Apply ?A ?F) (|do [type* (&type/apply-type ?F ?A)] (->java-sig type*)) diff --git a/luxc/src/lux/type.clj b/luxc/src/lux/type.clj index 85ce1613b..b569d890f 100644 --- a/luxc/src/lux/type.clj +++ b/luxc/src/lux/type.clj @@ -63,8 +63,8 @@ &/$Unit ;; lux;Cons (&/$Product (&/$Bound 1) - (&/$App (&/$Bound 0) - (&/$Bound 1))))))) + (&/$Apply (&/$Bound 1) + (&/$Bound 0))))))) (def Maybe (&/$Named (&/T ["lux" "Maybe"]) @@ -78,90 +78,90 @@ (def Type (&/$Named (&/T ["lux" "Type"]) - (let [Type (&/$App (&/$Bound 0) (&/$Bound 1)) - TypeList (&/$App List Type) + (let [Type (&/$Apply (&/$Bound 1) (&/$Bound 0)) + TypeList (&/$Apply Type List) TypePair (&/$Product Type Type)] - (&/$App (&/$UnivQ empty-env - (&/$Sum - ;; Host - (&/$Product Text TypeList) - (&/$Sum - ;; Void - &/$Unit + (&/$Apply &/$Void + (&/$UnivQ empty-env (&/$Sum - ;; Unit - &/$Unit + ;; Host + (&/$Product Text TypeList) (&/$Sum - ;; Sum - TypePair + ;; Void + &/$Unit (&/$Sum - ;; Product - TypePair + ;; Unit + &/$Unit (&/$Sum - ;; Function + ;; Sum TypePair (&/$Sum - ;; Bound - Nat + ;; Product + TypePair (&/$Sum - ;; Var - Nat + ;; Function + TypePair (&/$Sum - ;; Ex + ;; Bound Nat (&/$Sum - ;; UnivQ - (&/$Product TypeList Type) + ;; Var + Nat (&/$Sum - ;; ExQ - (&/$Product TypeList Type) + ;; Ex + Nat (&/$Sum - ;; App - TypePair - ;; Named - (&/$Product Ident Type))))))))))))) - ) - &/$Void)))) + ;; UnivQ + (&/$Product TypeList Type) + (&/$Sum + ;; ExQ + (&/$Product TypeList Type) + (&/$Sum + ;; App + TypePair + ;; Named + (&/$Product Ident Type))))))))))))) + ))))) (def Ann-Value (&/$Named (&/T ["lux" "Ann-Value"]) - (let [Ann-Value (&/$App (&/$Bound 0) (&/$Bound 1))] - (&/$App (&/$UnivQ empty-env - (&/$Sum - ;; BoolA - Bool - (&/$Sum - ;; NatA - Nat + (let [Ann-Value (&/$Apply (&/$Bound 1) (&/$Bound 0))] + (&/$Apply &/$Void + (&/$UnivQ empty-env (&/$Sum - ;; IntA - Int + ;; BoolA + Bool (&/$Sum - ;; DegA - Deg + ;; NatA + Nat (&/$Sum - ;; RealA - Real + ;; IntA + Int (&/$Sum - ;; CharA - Char + ;; DegA + Deg (&/$Sum - ;; TextA - Text + ;; RealA + Real (&/$Sum - ;; IdentA - Ident + ;; CharA + Char (&/$Sum - ;; ListA - (&/$App List Ann-Value) - ;; DictA - (&/$App List (&/$Product Text Ann-Value))))))))))) - ) - &/$Void)))) + ;; TextA + Text + (&/$Sum + ;; IdentA + Ident + (&/$Sum + ;; ListA + (&/$Apply Ann-Value List) + ;; DictA + (&/$Apply (&/$Product Text Ann-Value) List)))))))))) + ))))) (def Anns (&/$Named (&/T ["lux" "Anns"]) - (&/$App List (&/$Product Ident Ann-Value)))) + (&/$Apply (&/$Product Ident Ann-Value) List))) (def Macro) @@ -225,7 +225,7 @@ (fn [state] (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))] (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id (&/$Some type) %) - ts)) + ts)) state) nil) ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length))) @@ -235,7 +235,7 @@ (fn [state] (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))] (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id &/$None %) - ts)) + ts)) state) nil) ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length))) @@ -347,10 +347,10 @@ =return (clean* ?tid ?return)] (return (&/$Function =arg =return))) - (&/$App ?lambda ?param) + (&/$Apply ?param ?lambda) (|do [=lambda (clean* ?tid ?lambda) =param (clean* ?tid ?param)] - (return (&/$App =lambda =param))) + (return (&/$Apply =param =lambda))) (&/$Product ?left ?right) (|do [=left (clean* ?tid ?left) @@ -395,9 +395,9 @@ (defn ^:private unravel-app [fun-type] (|case fun-type - (&/$App ?left ?right) - (|let [[?fun-type ?args] (unravel-app ?left)] - (&/T [?fun-type (&/|++ ?args (&/|list ?right))])) + (&/$Apply ?arg ?func) + (|let [[?fun-type ?args] (unravel-app ?func)] + (&/T [?fun-type (&/$Cons ?arg ?args)])) _ (&/T [fun-type &/$Nil]))) @@ -482,7 +482,7 @@ (&/$Bound idx) (str idx) - (&/$App _ _) + (&/$Apply _ _) (|let [[?call-fun ?call-args] (unravel-app type)] (str "(" (show-type ?call-fun) " " (->> ?call-args (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")) @@ -539,8 +539,8 @@ [(&/$Ex xid) (&/$Ex yid)] (= xid yid) - [(&/$App xlambda xparam) (&/$App ylambda yparam)] - (and (type= xlambda ylambda) (type= xparam yparam)) + [(&/$Apply xparam xlambda) (&/$Apply yparam ylambda)] + (and (type= xparam yparam) (type= xlambda ylambda)) [(&/$UnivQ xenv xbody) (&/$UnivQ yenv ybody)] (type= xbody ybody) @@ -606,8 +606,8 @@ (&/$Product ?left ?right) (&/$Product (beta-reduce env ?left) (beta-reduce env ?right)) - (&/$App ?type-fn ?type-arg) - (&/$App (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)) + (&/$Apply ?type-arg ?type-fn) + (&/$Apply (beta-reduce env ?type-arg) (beta-reduce env ?type-fn)) (&/$UnivQ ?local-env ?local-def) (|case ?local-env @@ -654,7 +654,7 @@ (&/$Cons type-fn)) local-def)) - (&/$App F A) + (&/$Apply A F) (|do [type-fn* (apply-type F A)] (apply-type type-fn* param)) @@ -663,14 +663,15 @@ ;; TODO: This one must go... (&/$Ex id) - (return (&/$App type-fn param)) + (return (&/$Apply param type-fn)) (&/$Var id) (|do [=type-fun (deref id)] (apply-type =type-fun param)) _ - (&/fail-with-loc (str "[Type System] Not a type function:\n" (show-type type-fn) "\n")))) + (&/fail-with-loc (str "[Type System] Not a type function:\n" (show-type type-fn) "\n" + "for arg: " (show-type param))))) (def ^:private init-fixpoints &/$Nil) @@ -732,15 +733,15 @@ (check* fixpoints invariant?? expected bound)) state))) - [(&/$App (&/$Ex eid) eA) (&/$App (&/$Ex aid) aA)] + [(&/$Apply eA (&/$Ex eid)) (&/$Apply aA (&/$Ex aid))] (if (= eid aid) (check* fixpoints invariant?? eA aA) (check-error "" expected actual)) - [(&/$App (&/$Var ?id) A1) (&/$App F2 A2)] + [(&/$Apply A1 (&/$Var ?id)) (&/$Apply A2 F2)] (fn [state] (|case ((|do [F1 (deref ?id)] - (check* fixpoints invariant?? (&/$App F1 A1) actual)) + (check* fixpoints invariant?? (&/$Apply A1 F1) actual)) state) (&/$Right state* output) (return* state* output) @@ -764,10 +765,10 @@ (check* fixpoints* invariant?? e* a*)) state)))) - [(&/$App F1 A1) (&/$App (&/$Var ?id) A2)] + [(&/$Apply A1 F1) (&/$Apply A2 (&/$Var ?id))] (fn [state] (|case ((|do [F2 (deref ?id)] - (check* fixpoints invariant?? expected (&/$App F2 A2))) + (check* fixpoints invariant?? expected (&/$Apply A2 F2))) state) (&/$Right state* output) (return* state* output) @@ -779,7 +780,7 @@ (check* fixpoints* invariant?? e* a*)) state))) - [(&/$App F A) _] + [(&/$Apply A F) _] (let [fp-pair (&/T [expected actual]) _ (when (> (&/|length fixpoints) 64) (&/|log! (println-str 'FIXPOINTS (->> (&/|keys fixpoints) @@ -789,7 +790,7 @@ (show-type a))))) (&/|interpose "\n\n") (&/fold str "")))) - (assert false (prn-str 'check* '[(&/$App F A) _] (&/|length fixpoints) (show-type expected) (show-type actual))))] + (assert false (prn-str 'check* '[(&/$Apply A F) _] (&/|length fixpoints) (show-type expected) (show-type actual))))] (|case (fp-get fp-pair fixpoints) (&/$Some ?) (if ? @@ -800,10 +801,10 @@ (|do [expected* (apply-type F A)] (check* (fp-put fp-pair true fixpoints) invariant?? expected* actual)))) - [_ (&/$App (&/$Ex aid) A)] + [_ (&/$Apply A (&/$Ex aid))] (check-error "" expected actual) - [_ (&/$App F A)] + [_ (&/$Apply A F)] (|do [actual* (apply-type F A)] (check* fixpoints invariant?? expected actual*)) @@ -894,7 +895,7 @@ (defn actual-type [type] "(-> Type (Lux Type))" (|case type - (&/$App ?all ?param) + (&/$Apply ?param ?all) (|do [type* (apply-type ?all ?param)] (actual-type type*)) @@ -976,24 +977,24 @@ (defn ^:private push-app [inf-type inf-var] (|case inf-type - (&/$App inf-type* inf-var*) - (&/$App (push-app inf-type* inf-var) inf-var*) + (&/$Apply inf-var* inf-type*) + (&/$Apply inf-var* (push-app inf-type* inf-var)) _ - (&/$App inf-type inf-var))) + (&/$Apply inf-var inf-type))) (defn ^:private push-name [name inf-type] (|case inf-type - (&/$App inf-type* inf-var*) - (&/$App (push-name name inf-type*) inf-var*) + (&/$Apply inf-var* inf-type*) + (&/$Apply inf-var* (push-name name inf-type*)) _ (&/$Named name inf-type))) (defn ^:private push-univq [env inf-type] (|case inf-type - (&/$App inf-type* inf-var*) - (&/$App (push-univq env inf-type*) inf-var*) + (&/$Apply inf-var* inf-type*) + (&/$Apply inf-var* (push-univq env inf-type*)) _ (&/$UnivQ env inf-type))) |