aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/lux/analyser/case.clj53
-rw-r--r--src/lux/analyser/lux.clj57
-rw-r--r--src/lux/type.clj34
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
+ )