diff options
| -rw-r--r-- | src/lux/analyser/case.clj | 53 | ||||
| -rw-r--r-- | src/lux/analyser/lux.clj | 57 | ||||
| -rw-r--r-- | src/lux/type.clj | 34 |
3 files changed, 125 insertions, 19 deletions
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj index 2e58d7baf..792999a68 100644 --- a/src/lux/analyser/case.clj +++ b/src/lux/analyser/case.clj @@ -124,6 +124,36 @@ (fail (str "[Pattern-matching Error] Can't adjust type: " (&type/show-type type))) )) +(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*) + + _ + (&/$AppT 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*) + + _ + (&/$NamedT name inf-type))) + +(defn ^:private instantiate-inference [type] + (|case type + (&/$NamedT ?name ?type) + (|do [output (instantiate-inference ?type)] + (return (push-name ?name output))) + + (&/$UnivQ _aenv _abody) + (|do [inf-var &type/create-var + output (instantiate-inference _abody)] + (return (push-app output inf-var))) + + _ + (return type))) + (defn adjust-type [type] "(-> Type (Lux Type))" (adjust-type* &/$Nil type)) @@ -183,7 +213,11 @@ (analyse-pattern var?? value-type ?member kont) _ - (|do [value-type* (adjust-type value-type)] + (|do [must-infer? (&type/unknown? value-type) + value-type* (if must-infer? + (|do [member-types (&/map% (fn [_] &type/create-var) (&/|range (&/|length ?members)))] + (return (&type/fold-prod member-types))) + (adjust-type value-type))] (|case value-type* (&/$ProdT _) (|case (&type/tuple-types-for (&/|length ?members) value-type*) @@ -204,16 +238,27 @@ _ (fail (str "[Pattern-matching Error] Tuples require tuple-types: " (&type/show-type value-type)))))) - + (&/$RecordS pairs) - (|do [[rec-members rec-type] (&&record/order-record pairs)] - (analyse-pattern &/$None value-type (&/T [meta (&/$TupleS rec-members)]) kont)) + (|do [[rec-members rec-type] (&&record/order-record pairs) + must-infer? (&type/unknown? value-type) + rec-type* (if must-infer? + (instantiate-inference rec-type) + (return value-type)) + _ (&type/check value-type rec-type*)] + (analyse-pattern &/$None rec-type* (&/T [meta (&/$TupleS rec-members)]) kont)) (&/$TagS ?ident) (|do [[=module =name] (&&/resolved-ident ?ident) value-type* (adjust-type value-type) idx (&module/tag-index =module =name) group (&module/tag-group =module =name) + must-infer? (&type/unknown? value-type*) + variant-type (if must-infer? + (|do [variant-type (&module/tag-type =module =name)] + (return (instantiate-inference variant-type))) + (return value-type*)) + _ (&type/check value-type variant-type) case-type (&type/sum-at idx value-type*) [=test =kont] (analyse-pattern &/$None case-type unit kont)] (return (&/T [($VariantTestAC (&/T [idx (&/|length group) =test])) =kont]))) diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj index 4ffa7a9c2..9526fed0f 100644 --- a/src/lux/analyser/lux.clj +++ b/src/lux/analyser/lux.clj @@ -386,7 +386,7 @@ (throw e)))))) module-name &/get-module-name ;; :let [[r-prefix r-name] real-name - ;; _ (when (or (= "get@" r-name) + ;; _ (when (or (= "jvm-import" r-name) ;; ;; (= "defclass" r-name) ;; ) ;; (->> (&/|map &/show-ast macro-expansion) @@ -421,6 +421,48 @@ (&&/$case =value =match) ))))) +(defn ^:private unravel-inf-appt [type] + (|case type + (&/$AppT =input+ (&/$VarT _inf-var)) + (&/$Cons _inf-var (unravel-inf-appt =input+)) + + _ + (&/|list))) + +(defn ^:private clean-func-inference [$input $output =input =func] + (|case =input + (&/$VarT 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)) + (&/fold% (fn [_func _inf-var] + (|do [:let [$inf-var (&/$VarT _inf-var)] + =inf-var (&type/resolve-type $inf-var) + _func* (clean-func-inference $inf-var $output =inf-var _func) + _ (&type/delete-var _inf-var)] + (return _func*))) + =func + (unravel-inf-appt =input)) + + (&/$ProdT _ _) + (&/fold% (fn [_func _inf-var] + (|do [:let [$inf-var (&/$VarT _inf-var)] + =inf-var (&type/resolve-type $inf-var) + _func* (clean-func-inference $inf-var $output =inf-var _func) + _ (&type/delete-var _inf-var)] + (return _func*))) + =func + (&/|reverse (&type/unfold-prod =input))) + + _ + (|do [=func* (&type/clean $input =func) + =func** (&type/clean $output =func*)] + (return =func**)))) + (defn analyse-lambda* [analyse exo-type ?self ?arg ?body] (|case exo-type (&/$VarT id) @@ -436,18 +478,7 @@ (|do [[[lambda-type lambda-cursor] lambda-analysis] (analyse-lambda* analyse (&/$LambdaT $input $output) ?self ?arg ?body) =input (&type/resolve-type $input) =output (&type/resolve-type $output) - inferred-type (|case =input - (&/$VarT iid) - (|do [:let [=input* (next-bound-type =output)] - _ (&type/set-var iid =input*) - =output* (&type/clean $input =output) - =output** (&type/clean $output =output*)] - (return (&/$UnivQ &/$Nil (embed-inferred-input =input* =output**)))) - - _ - (|do [=output* (&type/clean $input =output) - =output** (&type/clean $output =output*)] - (return (embed-inferred-input =input =output**)))) + inferred-type (clean-func-inference $input $output =input (embed-inferred-input =input =output)) _ (&type/check exo-type inferred-type)] (return (&&/|meta inferred-type lambda-cursor lambda-analysis))) diff --git a/src/lux/type.clj b/src/lux/type.clj index e9ebcc361..2b5f27d4e 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -212,7 +212,7 @@ ;; [Exports] ;; Type vars -(def ^:private create-var +(def create-var (fn [state] (let [id (->> state (&/get$ &/$type-vars) (&/get$ &/$counter))] (return* (&/update$ &/$type-vars #(->> % @@ -227,7 +227,7 @@ (return (&/$ExT seed)))) (declare clean*) -(defn ^:private delete-var [id] +(defn delete-var [id] (|do [? (bound? id) _ (if ? (return nil) @@ -885,3 +885,33 @@ (&/fold (fn [right left] (&/$ProdT left right)) last prevs)))))] (&/$Some ?member-types*))))) + +(do-template [<name> <zero> <plus>] + (defn <name> [types] + (|case (&/|reverse types) + (&/$Nil) + <zero> + + (&/$Cons type (&/$Nil)) + type + + (&/$Cons last prevs) + (&/fold (fn [r l] (<plus> l r)) last prevs))) + + fold-prod &/$UnitT &/$ProdT + fold-sum &/$VoidT &/$SumT + ) + + +(do-template [<name> <ctor>] + (defn <name> [type] + (|case type + (<ctor> l r) + (&/$Cons l (<name> r)) + + _ + (&/|list type))) + + unfold-prod &/$ProdT + unfold-sum &/$SumT + ) |