diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/lux/macro/poly.lux | 90 | ||||
| -rw-r--r-- | stdlib/source/lux/macro/poly/eq.lux | 67 |
2 files changed, 103 insertions, 54 deletions
diff --git a/stdlib/source/lux/macro/poly.lux b/stdlib/source/lux/macro/poly.lux index 8c3a5b288..0cf0e64f1 100644 --- a/stdlib/source/lux/macro/poly.lux +++ b/stdlib/source/lux/macro/poly.lux @@ -30,6 +30,21 @@ (type: #export Env (Dict Nat AST)) ## [Combinators] +(do-template [<combinator> <name> <type>] + [(def: #export <combinator> + (Matcher Unit) + (lambda [:type:] + (case (type;un-name :type:) + <type> + (:: compiler;Monad<Lux> wrap []) + + _ + (compiler;fail (format "Not " <name> " type: " (%type :type:))))))] + + [void "Void" #;VoidT] + [unit "Unit" #;UnitT] + ) + (do-template [<combinator> <name>] [(def: #export <combinator> (Matcher Unit) @@ -41,7 +56,6 @@ _ (compiler;fail (format "Not " <name> " type: " (%type :type:))))))] - [unit "Unit"] [bool "Bool"] [nat "Nat"] [int "Int"] @@ -234,36 +248,30 @@ _ (compiler;fail (format "Not a bound type: " (%type :type:)))))) -(def: #export (var env var-id) - (-> Env Nat (Matcher Unit)) - (lambda [:type:] - (case :type: - (^=> (#;BoundT idx) - (n.= var-id (adjusted-idx env idx))) - (:: compiler;Monad<Lux> wrap []) - - _ - (compiler;fail (format "Not a bound type: " (%type :type:)))))) - (def: #export (recur env) - (-> Env (Matcher Unit)) + (-> Env (Matcher AST)) (lambda [:type:] (do Monad<Lux> - [[t-fun t-args] (apply :type:)] - (loop [base +0 - :parts: (list& t-fun t-args)] - (case :parts: - #;Nil - (wrap []) - - (^=> (#;Cons (#;BoundT idx) :parts:') - [(adjusted-idx env idx) - idx'] - (n.= base idx')) - (recur (n.inc base) :parts:') - - _ - (compiler;fail (format "Type is not a recursive instance: " (%type :type:))))) + [[t-func t-args] (apply :type:)] + (case t-func + (^=> (#;BoundT t-func-idx) + (n.= +0 (adjusted-idx env t-func-idx)) + [(do maybe;Monad<Maybe> + [=func (dict;get +0 env) + =args (mapM @ (lambda [t-arg] + (case t-arg + (#;BoundT idx) + (dict;get (adjusted-idx env idx) env) + + _ + #;None)) + t-args)] + (wrap (` ((~ =func) (~@ =args))))) + (#;Some call)]) + (wrap call) + + _ + (compiler;fail (format "Type is not a recursive instance: " (%type :type:)))) ))) ## [Syntax] @@ -343,6 +351,32 @@ (~ impl))))))) ## [Derivers] +(def: #export (contains-bound-types? type) + (-> Type Bool) + (case type + (#;HostT name params) + (list;any? contains-bound-types? params) + + (^template [<tag>] + (<tag> _) + false) + ([#;VoidT] [#;UnitT] + [#;VarT] [#;ExT] + [#;UnivQ] [#;ExQ]) + + (#;BoundT idx) + true + + (^template [<tag>] + (<tag> left right) + (or (contains-bound-types? left) + (contains-bound-types? right))) + ([#;LambdaT] [#;AppT] [#;SumT] [#;ProdT]) + + (#;NamedT name sub-type) + (contains-bound-types? sub-type) + )) + (def: #export (gen-type converter type-fun tvars type) (-> (-> AST AST) AST (List AST) Type AST) (let [type' (type;to-ast type)] diff --git a/stdlib/source/lux/macro/poly/eq.lux b/stdlib/source/lux/macro/poly/eq.lux index 025797751..ce42c2eab 100644 --- a/stdlib/source/lux/macro/poly/eq.lux +++ b/stdlib/source/lux/macro/poly/eq.lux @@ -24,8 +24,20 @@ [type] )) +## [Utils] +(def: (function$ func inputs output) + (-> AST (List AST) AST AST) + (case inputs + #;Nil + output + + _ + (` (lambda (~@ (if (list;empty? inputs) (list) (list func))) + [(~@ inputs)] + (~ output))))) + ## [Derivers] -(poly: #export (|Eq| env :x:) +(poly: #export (Eq<?> env :x:) (let [->Eq (: (-> AST AST) (lambda [.type.] (` (eq;Eq (~ .type.)))))] (let% [<basic> (do-template [<type> <matcher> <eq>] @@ -53,19 +65,21 @@ pattern-matching (mapM @ (lambda [[name :case:]] (do @ - [encoder (|Eq| new-env :case:)] + [g!eq (Eq<?> new-env :case:)] (wrap (list (` [((~ (ast;tag name)) (~ g!left)) ((~ (ast;tag name)) (~ g!right))]) - (` ((~ encoder) (~ g!left) (~ g!right))))))) - cases)] - (wrap (` (: (~ (poly;gen-type ->Eq g!type-fun g!vars :x:)) - (lambda [(~@ g!vars)] - (lambda [(~ g!left) (~ g!right)] - (case [(~ g!left) (~ g!right)] - (~@ (List/join pattern-matching))))) - ))))) + (` ((~ g!eq) (~ g!left) (~ g!right))))))) + cases) + #let [base (function$ g!type-fun g!vars + (` (lambda [(~ g!left) (~ g!right)] + (case [(~ g!left) (~ g!right)] + (~@ (List/join pattern-matching))))))]] + (wrap (if (and false (poly;contains-bound-types? :x:)) + base + (` (: (~ (poly;gen-type ->Eq g!type-fun g!vars :x:)) + (~ base))))))) ## Tuples - (with-gensyms [g!type-fun g!left g!right] + (with-gensyms [g!type-fun] (do @ [[g!vars members] (poly;tuple :x:) #let [new-env (poly;extend-env g!type-fun g!vars env)] @@ -74,26 +88,27 @@ (do @ [g!left (compiler;gensym "g!left") g!right (compiler;gensym "g!right") - encoder (|Eq| new-env :member:)] - (wrap [g!left g!right encoder]))) + g!eq (Eq<?> new-env :member:)] + (wrap [g!left g!right g!eq]))) members) #let [.left. (` [(~@ (List/map product;left pattern-matching))]) - .right. (` [(~@ (List/map (|>. product;right product;left) pattern-matching))])]] - (wrap (` (: (~ (poly;gen-type ->Eq g!type-fun g!vars :x:)) - (lambda [(~@ g!vars)] - (lambda [(~ g!left) (~ g!right)] - (case [(~ g!left) (~ g!right)] - [(~ .left.) (~ .right.)] - (;;array (list (~@ (List/map (lambda [[g!left g!right g!encoder]] - (` ((~ g!encoder) (~ g!left) (~ g!right)))) - pattern-matching))))))) - ))) - )) + .right. (` [(~@ (List/map (|>. product;right product;left) pattern-matching))]) + base (function$ g!type-fun g!vars + (` (lambda [(~ .left.) (~ .right.)] + (and (~@ (List/map (lambda [[g!left g!right g!eq]] + (` ((~ g!eq) (~ g!left) (~ g!right)))) + pattern-matching))))))]] + (wrap (if (and false (poly;contains-bound-types? :x:)) + base + (` (: (~ (poly;gen-type ->Eq g!type-fun g!vars :x:)) + (~ base))))))) + ## Type recursion + (poly;recur env :x:) ## Type applications (do @ [[:func: :args:] (poly;apply :x:) - .func. (|Eq| env :func:) - .args. (mapM @ (|Eq| env) :args:)] + .func. (Eq<?> env :func:) + .args. (mapM @ (Eq<?> env) :args:)] (wrap (` (: (~ (->Eq (type;to-ast :x:))) ((~ .func.) (~@ .args.)))))) ## Bound type-vars |