aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--stdlib/source/lux/macro/poly.lux90
-rw-r--r--stdlib/source/lux/macro/poly/eq.lux67
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