aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/lux/type.lux15
-rw-r--r--stdlib/source/lux/type/auto.lux103
-rw-r--r--stdlib/source/lux/type/check.lux7
-rw-r--r--stdlib/test/test/lux/type/auto.lux6
4 files changed, 104 insertions, 27 deletions
diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux
index a721c0926..1fb0afa6f 100644
--- a/stdlib/source/lux/type.lux
+++ b/stdlib/source/lux/type.lux
@@ -25,15 +25,10 @@
(^template [<tag>]
(<tag> left right)
(<tag> (beta-reduce env left) (beta-reduce env right)))
- ([#;SumT] [#;ProdT])
+ ([#;SumT] [#;ProdT]
+ [#;LambdaT] [#;AppT])
(^template [<tag>]
- (<tag> left right)
- (<tag> (beta-reduce env left) (beta-reduce env right)))
- ([#;LambdaT]
- [#;AppT])
-
- (^template [<tag>]
(<tag> old-env def)
(case old-env
#;Nil
@@ -45,11 +40,9 @@
[#;ExQ])
(#;BoundT idx)
- (default type (list;at idx env))
+ (default (error! (Text/append "Unknown type var: " (Nat/encode idx)))
+ (list;at idx env))
- (#;NamedT name type)
- (beta-reduce env type)
-
_
type
))
diff --git a/stdlib/source/lux/type/auto.lux b/stdlib/source/lux/type/auto.lux
index aa7074d4a..d2b8cb1e5 100644
--- a/stdlib/source/lux/type/auto.lux
+++ b/stdlib/source/lux/type/auto.lux
@@ -171,6 +171,20 @@
_
(tc;fail (format "Invalid function type: " (%type func)))))
+(def: (concrete-type type)
+ (-> Type (Check [(List Nat) Type]))
+ (case type
+ (#;UnivQ _)
+ (do Monad<Check>
+ [[id var] tc;create-var
+ [ids final-output] (concrete-type (default (undefined)
+ (type;apply-type type var)))]
+ (wrap [(#;Cons id ids)
+ final-output]))
+
+ _
+ (:: Monad<Check> wrap [(list) type])))
+
(def: (check-apply member-type input-types output-type)
(-> Type (List Type) Type (Check []))
(do Monad<Check>
@@ -190,17 +204,16 @@
(set@ #tc;bindings (dict;from-list number;Hash<Nat> (get@ #;mappings type-vars))))]
(#;Right [compiler context]))))
-(def: (test-alternatives sig-type member-idx input-types output-type alts)
- (-> Type Nat (List Type) Type (List [Ident Type]) (Lux (List Ident)))
+(def: (test-provision context dep alts)
+ (-> tc;Context Type (List [Ident Type]) (Lux (List Ident)))
(do Monad<Lux>
- [context compiler-type-context]
+ [compiler compiler;get-compiler]
(case (|> alts
(list;filter (lambda [[alt-name alt-type]]
(case (tc;run context
(do Monad<Check>
- [_ (tc;check alt-type sig-type)
- member-type (find-member-type member-idx alt-type)]
- (check-apply member-type input-types output-type)))
+ [_ (tc;check dep alt-type)]
+ (wrap [])))
(#;Left error)
false
@@ -208,13 +221,69 @@
true)))
(List/map product;left))
#;Nil
- (compiler;fail "No alternatives.")
+ (compiler;fail (format "No candidates for provisioning: " (%type dep)))
+
+ found
+ (wrap found))))
+
+(def: (provision compiler context dep)
+ (-> Compiler tc;Context Type (Check Ident))
+ (case (compiler;run compiler
+ ($_ compiler;either
+ (do Monad<Lux> [alts local-env] (test-provision context dep alts))
+ (do Monad<Lux> [alts local-structs] (test-provision context dep alts))
+ (do Monad<Lux> [alts import-structs] (test-provision context dep alts))))
+ (#;Left error)
+ (tc;fail error)
+
+ (#;Right candidates)
+ (case candidates
+ #;Nil
+ (tc;fail (format "No candidates for provisioning: " (%type dep)))
+
+ (#;Cons winner #;Nil)
+ (:: Monad<Check> wrap winner)
+
+ _
+ (tc;fail (format "Too many candidates for provisioning: " (%type dep) " --- " (%list %ident candidates))))
+ ))
+
+(def: (test-alternatives sig-type member-idx input-types output-type alts)
+ (-> Type Nat (List Type) Type (List [Ident Type]) (Lux (List [Ident (List Ident)])))
+ (do Monad<Lux>
+ [compiler compiler;get-compiler
+ context compiler-type-context]
+ (case (|> alts
+ (List/map (lambda [[alt-name alt-type]]
+ (case (tc;run context
+ (do Monad<Check>
+ [[tvars alt-type] (concrete-type alt-type)
+ #let [[deps alt-type] (type;flatten-function alt-type)]
+ _ (tc;check alt-type sig-type)
+ member-type (find-member-type member-idx alt-type)
+ _ (check-apply member-type input-types output-type)
+ =tvars (mapM @ tc;deref tvars)
+ context' tc;get-context
+ =deps (mapM @ (provision compiler context') deps)]
+ (wrap =deps)))
+ (#;Left error)
+ (list)
+
+ (#;Right =deps)
+ (list [alt-name =deps]))))
+ List/join)
+ #;Nil
+ (compiler;fail (format "No alternatives."
+ "\n"
+ (|> alts
+ (List/map product;left)
+ (%list %ident))))
found
(wrap found))))
(def: (find-alternatives sig-type member-idx input-types output-type)
- (-> Type Nat (List Type) Type (Lux (List Ident)))
+ (-> Type Nat (List Type) Type (Lux (List [Ident (List Ident)])))
(let [test (test-alternatives sig-type member-idx input-types output-type)]
($_ compiler;either
(do Monad<Lux> [alts local-env] (test alts))
@@ -248,15 +317,21 @@
#;Nil
(compiler;fail (format "No structure option could be found for member: " (%ident member)))
- (#;Cons chosen #;Nil)
- (wrap (list (` (:: (~ (ast;symbol chosen))
- (~ (ast;local-symbol (product;right member)))
- (~@ (List/map ast;symbol args))))))
+ (#;Cons [chosen deps] #;Nil)
+ (let [chosen-inst (case deps
+ #;Nil
+ (ast;symbol chosen)
+
+ _
+ (` ((~ (ast;symbol chosen)) (~@ (List/map ast;symbol deps)))))]
+ (wrap (list (` (:: (~ chosen-inst)
+ (~ (ast;local-symbol (product;right member)))
+ (~@ (List/map ast;symbol args)))))))
_
- (compiler;fail (format "Too many available options: "
+ (compiler;fail (format "Too many options available: "
(|> chosen-ones
- (List/map %ident)
+ (List/map (. %ident product;left))
(text;join-with ", ")
)))))
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index b9a1301bc..97a01d8ce 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -128,7 +128,7 @@
#;None
(#;Left (format "Unknown type-var: " (%n id))))))
-(def: (deref id)
+(def: #export (deref id)
(-> Id (Check Type))
(lambda [context]
(case (|> context (get@ #bindings) (dict;get id))
@@ -516,3 +516,8 @@
(#;Right _)
true))
+
+(def: #export get-context
+ (Check Context)
+ (lambda [context]
+ (#;Right [context context])))
diff --git a/stdlib/test/test/lux/type/auto.lux b/stdlib/test/test/lux/type/auto.lux
index cb58514bf..f759827f0 100644
--- a/stdlib/test/test/lux/type/auto.lux
+++ b/stdlib/test/test/lux/type/auto.lux
@@ -32,5 +32,9 @@
(L/= (list;n.range +1 +10)
(::: map n.inc (list;n.range +0 +9)))
)))
-
+
+ (assert "Can automatically select second-order structures."
+ (::: =
+ (list;n.range +1 +10)
+ (list;n.range +1 +10)))
))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 01:22:54 +0000