diff options
Diffstat (limited to '')
| -rw-r--r-- | src/lux/analyser/case.clj | 227 | ||||
| -rw-r--r-- | src/lux/analyser/lux.clj | 27 | ||||
| -rw-r--r-- | src/lux/compiler/lux.clj | 20 | ||||
| -rw-r--r-- | src/lux/type.clj | 7 |
4 files changed, 210 insertions, 71 deletions
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj index 1c315e405..13e982fef 100644 --- a/src/lux/analyser/case.clj +++ b/src/lux/analyser/case.clj @@ -64,71 +64,188 @@ (|let [[_env _idx _var] frame] (&/T [_env (+ 2 _idx) _var]))) -(defn adjust-type* [up type] - "(-> (List (, (Maybe (List Type)) Int Type)) Type (Lux Type))" +(defn clean! [level ?tid bound-idx type] (|case type - (&/$UnivQ _aenv _abody) - (&type/with-var - (fn [$var] - (|do [=type (&type/apply-type type $var) - ==type (adjust-type* (&/$Cons (&/T [_aenv 1 $var]) (&/|map update-up-frame up)) =type)] - (&type/clean $var ==type)))) - - (&/$ExQ _aenv _abody) - (|do [$var &type/existential - =type (&type/apply-type type $var)] - (adjust-type* up =type)) + (&/$VarT ?id) + (if (= ?tid ?id) + (let [new-bound (&/$BoundT (+ (* 2 level) bound-idx))] + (do ;; (prn 'CLEANED level ?tid bound-idx (&type/show-type new-bound)) + new-bound)) + type) + + (&/$HostT ?name ?params) + (&/$HostT ?name (&/|map (partial clean! level ?tid bound-idx) + ?params)) + + (&/$LambdaT ?arg ?return) + (&/$LambdaT (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)) (&/$ProdT ?left ?right) - (|do [=type (&/fold% (fn [_abody ena] - (|let [[_aenv _aidx (&/$VarT _avar)] ena] - (|do [_ (&type/set-var _avar (&/$BoundT _aidx))] - (&type/clean* _avar _abody)))) - type - up) - :let [distributor (fn [v] - (&/fold (fn [_abody ena] - (|let [[_aenv _aidx _avar] ena] - (&/$UnivQ _aenv _abody))) - v - up)) - adjusted-type (&type/Tuple$ (&/|map distributor (&type/flatten-prod =type)))]] - (return adjusted-type)) - + (&/$ProdT (clean! level ?tid bound-idx ?left) + (clean! level ?tid bound-idx ?right)) + (&/$SumT ?left ?right) - (|do [=type (&/fold% (fn [_abody ena] - (|let [[_aenv _aidx (&/$VarT _avar)] ena] - (|do [_ (&type/set-var _avar (&/$BoundT _aidx))] - (&type/clean* _avar _abody)))) - type - up) - :let [distributor (fn [v] - (&/fold (fn [_abody ena] - (|let [[_aenv _aidx _avar] ena] - (&/$UnivQ _aenv _abody))) - v - up)) - adjusted-type (&type/Variant$ (&/|map distributor (&type/flatten-sum =type)))]] - (return adjusted-type)) - - (&/$AppT ?tfun ?targ) - (|do [=type (&type/apply-type ?tfun ?targ)] - (adjust-type* up =type)) + (&/$SumT (clean! level ?tid bound-idx ?left) + (clean! level ?tid bound-idx ?right)) - (&/$VarT ?id) - (|do [type* (&/try-all% (&/|list (&type/deref ?id) - (fail (str "##2##: " ?id))))] - (adjust-type* up type*)) + (&/$UnivQ ?env ?body) + (&/$UnivQ (&/|map (partial clean! level ?tid bound-idx) ?env) + (clean! (inc level) ?tid bound-idx ?body)) + + (&/$ExQ ?env ?body) + (&/$ExQ (&/|map (partial clean! level ?tid bound-idx) ?env) + (clean! (inc level) ?tid bound-idx ?body)) + + _ + type + )) + +(defn beta-reduce! [level env type] + (do ;; (prn 0 'beta-reduce! level (&type/show-type type) (&/|length env)) + (|case type + (&/$HostT ?name ?params) + (&/$HostT ?name (&/|map (partial beta-reduce! level env) ?params)) + + (&/$SumT ?left ?right) + (&/$SumT (beta-reduce! level env ?left) + (beta-reduce! level env ?right)) + + (&/$ProdT ?left ?right) + (&/$ProdT (beta-reduce! level env ?left) + (beta-reduce! level env ?right)) + + (&/$AppT ?type-fn ?type-arg) + (do ;; (prn 'beta-reduce! level 'APP (show-type ?type-fn) (show-type ?type-arg)) + (&/$AppT (beta-reduce! level env ?type-fn) + (beta-reduce! level env ?type-arg))) + + (&/$UnivQ ?local-env ?local-def) + (&/$UnivQ ?local-env (beta-reduce! (inc level) env ?local-def)) + + (&/$ExQ ?local-env ?local-def) + (&/$ExQ ?local-env (beta-reduce! (inc level) env ?local-def)) + + (&/$LambdaT ?input ?output) + (&/$LambdaT (beta-reduce! level env ?input) + (beta-reduce! level env ?output)) + + (&/$BoundT ?idx) + (do ;; (prn 1 'beta-reduce! level [?idx (- ?idx (* 2 level))] (&/|length env)) + (|case (&/|at (- ?idx (* 2 level)) env) + (&/$Some bound) + (do ;; (prn 'beta-reduce! level 'BOUND ?idx (&type/show-type bound)) + (beta-reduce! level env bound)) + + _ + type)) + + _ + type + ))) + +(defn apply-type! [type-fn param] + (|case type-fn + (&/$UnivQ local-env local-def) + (return (beta-reduce! 0 (->> local-env + (&/$Cons param) + (&/$Cons type-fn)) + local-def)) + + (&/$ExQ local-env local-def) + (return (beta-reduce! 0 (->> local-env + (&/$Cons param) + (&/$Cons type-fn)) + local-def)) + + (&/$AppT F A) + (|do [type-fn* (apply-type! F A)] + (apply-type! type-fn* param)) (&/$NamedT ?name ?type) - (adjust-type* up ?type) + (apply-type! ?type param) - (&/$UnitT) - (return type) + (&/$ExT id) + (return (&/$AppT type-fn param)) + (&/$VarT id) + (|do [=type-fun (deref id)] + (apply-type! =type-fun param)) + _ - (fail (str "[Pattern-matching Error] Can't adjust type: " (&type/show-type type))) - )) + (fail (str "[Type System] Not a type function:\n" (&type/show-type type-fn) "\n")))) + +(defn adjust-type* [up type] + "(-> (List (, (Maybe (List Type)) Int Type)) Type (Lux Type))" + (do ;; (prn 'adjust-type* 0 (&type/show-type type)) + (|case type + (&/$UnivQ _aenv _abody) + (&type/with-var + (fn [$var] + (|do [=type (apply-type! type $var) + ==type (adjust-type* (&/$Cons (&/T [_aenv 1 $var]) (&/|map update-up-frame up)) =type)] + (&type/clean $var ==type)))) + + (&/$ExQ _aenv _abody) + (|do [$var &type/existential + =type (apply-type! type $var)] + (adjust-type* up =type)) + + (&/$ProdT ?left ?right) + (|do [:let [=type (&/fold (fn [_abody ena] + (|let [[_aenv _aidx (&/$VarT _avar)] ena] + (clean! 0 _avar _aidx _abody))) + type + up)] + ;; :let [_ (prn 'adjust-type* 1 (&type/show-type =type))] + :let [distributor (fn [v] + (&/fold (fn [_abody ena] + (|let [[_aenv _aidx _avar] ena] + (&/$UnivQ _aenv _abody))) + v + up)) + adjusted-type (&type/Tuple$ (&/|map distributor (&type/flatten-prod =type)))] + ;; :let [_ (prn 'adjust-type* 2 (&type/show-type adjusted-type))] + ] + (return adjusted-type)) + + (&/$SumT ?left ?right) + (|do [:let [=type (&/fold (fn [_abody ena] + (|let [[_aenv _aidx (&/$VarT _avar)] ena] + (clean! 0 _avar _aidx _abody))) + type + up)] + :let [distributor (fn [v] + (&/fold (fn [_abody ena] + (|let [[_aenv _aidx _avar] ena] + (&/$UnivQ _aenv _abody))) + v + up)) + adjusted-type (&type/Variant$ (&/|map distributor (&type/flatten-sum =type)))]] + (return adjusted-type)) + + (&/$AppT ?tfun ?targ) + (|do [=type (apply-type! ?tfun ?targ)] + (adjust-type* up =type)) + + (&/$VarT ?id) + (|do [type* (&/try-all% (&/|list (&type/deref ?id) + (fail (str "##2##: " ?id))))] + (adjust-type* up type*)) + + (&/$NamedT ?name ?type) + (adjust-type* up ?type) + + (&/$UnitT) + (return type) + + _ + (fail (str "[Pattern-matching Error] Can't adjust type: " (&type/show-type type))) + ))) (defn adjust-type [type] "(-> Type (Lux Type))" diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj index d51ac2168..6ecd45974 100644 --- a/src/lux/analyser/lux.clj +++ b/src/lux/analyser/lux.clj @@ -20,6 +20,8 @@ [meta :as &&meta]))) ;; [Utils] +;; TODO: Walk the type to set up the bound-type, instead of doing a +;; rough calculation like this one. (defn ^:private count-univq [type] "(-> Type Int)" (|case type @@ -29,6 +31,8 @@ _ 0)) +;; TODO: This technique won't work if the body of the type contains +;; nested quantifications that are cannot be directly counted. (defn ^:private next-bound-type [type] "(-> Type Type)" (&/$BoundT (->> (count-univq type) (* 2) (+ 1)))) @@ -333,8 +337,10 @@ (|do [? (&type/bound? ?id) type** (if ? (&type/clean $var =output-t) - (|do [_ (&type/set-var ?id (next-bound-type =output-t))] - (&type/clean $var =output-t))) + (|do [_ (&type/set-var ?id (next-bound-type =output-t)) + cleaned-output* (&type/clean $var =output-t) + :let [cleaned-output (&/$UnivQ &/$Nil cleaned-output*)]] + (return cleaned-output))) _ (&type/clean $var exo-type)] (return (&/T [type** ==args]))) )))) @@ -486,7 +492,7 @@ _ (&/with-attempt (|do [exo-type* (&type/actual-type exo-type)] - (|case exo-type + (|case exo-type* (&/$UnivQ _) (|do [$var &type/existential :let [(&/$ExT $var-id) $var] @@ -564,21 +570,22 @@ (defn analyse-import [analyse compile-module path ex-alias] (|do [_ &/ensure-statement - module-name &/get-module-name - _ (if (= module-name path) + current-module &/get-module-name + _ (if (= current-module path) (&/fail-with-loc (str "[Analyser Error] Module can't import itself: " path)) (return nil))] (&/save-module (|do [already-compiled? (&&module/exists? path) active? (&/active-module? path) - _ (&/assert! (not active?) (str "[Analyser Error] Can't import a module that is mid-compilation: " path " @ " module-name)) + _ (&/assert! (not active?) + (str "[Analyser Error] Can't import a module that is mid-compilation: " path " @ " current-module)) _ (&&module/add-import path) - _ (if (not already-compiled?) - (compile-module path) - (return nil)) + ?module-hash (if (not already-compiled?) + (compile-module path) + (&&module/module-hash path)) _ (if (= "" ex-alias) (return nil) - (&&module/alias module-name ex-alias path))] + (&&module/alias current-module ex-alias path))] (return &/$Nil))))) (defn ^:private coerce [new-type analysis] diff --git a/src/lux/compiler/lux.clj b/src/lux/compiler/lux.clj index d5481dbd8..a9cd3756f 100644 --- a/src/lux/compiler/lux.clj +++ b/src/lux/compiler/lux.clj @@ -151,6 +151,20 @@ (defn compile-loop [compile $begin ?args] (|do [^MethodVisitor *writer* &/get-writer + :let [idxs+args (&/zip2 (&/|range* 1 (&/|length ?args)) + ?args)] + _ (&/map% (fn [idx+?arg] + (|do [:let [[idx ?arg] idx+?arg + already-set? (|case ?arg + [_ (&o/$var (&/$Local l-idx))] + (= idx l-idx) + + _ + false)]] + (if already-set? + (return nil) + (compile ?arg)))) + idxs+args) _ (&/map% (fn [idx+?arg] (|do [:let [[idx ?arg] idx+?arg already-set? (|case ?arg @@ -159,14 +173,10 @@ _ false)] - _ (if already-set? - (return nil) - (compile ?arg)) :let [_ (when (not already-set?) (.visitVarInsn *writer* Opcodes/ASTORE idx))]] (return nil))) - (&/zip2 (&/|range* 1 (&/|length ?args)) - ?args)) + (&/|reverse idxs+args)) :let [_ (.visitJumpInsn *writer* Opcodes/GOTO $begin)]] (return nil))) diff --git a/src/lux/type.clj b/src/lux/type.clj index 898088ff8..f0ec289c2 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -323,9 +323,14 @@ (&/$UnivQ ?env ?body) (|do [=env (&/map% (partial clean* ?tid) ?env) - body* (clean* ?tid ?body)] + body* (clean* ?tid ?body)] ;; TODO: DON'T 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 + (return (&/$ExQ =env body*))) + _ (return type) )) |