aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--luxc/src/lux/type.clj4
-rw-r--r--stdlib/source/lux.lux3
-rw-r--r--stdlib/source/lux/control/predicate.lux37
-rw-r--r--stdlib/source/lux/lang/type.lux20
-rw-r--r--stdlib/source/lux/macro/poly.lux38
-rw-r--r--stdlib/source/lux/macro/poly/eq.lux4
-rw-r--r--stdlib/source/lux/macro/poly/functor.lux4
-rw-r--r--stdlib/source/lux/macro/poly/json.lux8
-rw-r--r--stdlib/source/lux/type/refinement.lux72
-rw-r--r--stdlib/test/test/lux/math/modular.lux2
-rw-r--r--stdlib/test/tests.lux6
11 files changed, 160 insertions, 38 deletions
diff --git a/luxc/src/lux/type.clj b/luxc/src/lux/type.clj
index 897b3bc67..d5d6b0316 100644
--- a/luxc/src/lux/type.clj
+++ b/luxc/src/lux/type.clj
@@ -423,10 +423,10 @@
(&/$Primitive name params)
(|case params
(&/$Nil)
- (str "(primitive " name ")")
+ (str "(primitive " (pr-str name) ")")
_
- (str "(primitive " name " " (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")"))
+ (str "(primitive " (pr-str name) " " (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")"))
(&/$Void)
"Void"
diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux
index cf5707996..e4214a899 100644
--- a/stdlib/source/lux.lux
+++ b/stdlib/source/lux.lux
@@ -2608,6 +2608,9 @@
#Nil))))]
(` ("lux in-module" (~ (text$ module)) (~ (walk-type type'))))
+ [_ (#Form (#Cons [_ (#Symbol ["" "~"])] (#Cons expression #Nil)))]
+ expression
+
[_ (#Form (#Cons type-fn args))]
(list/fold ("lux check" (-> Code Code Code)
(function' [arg type-fn] (` (#.Apply (~ arg) (~ type-fn)))))
diff --git a/stdlib/source/lux/control/predicate.lux b/stdlib/source/lux/control/predicate.lux
new file mode 100644
index 000000000..f4ca17d70
--- /dev/null
+++ b/stdlib/source/lux/control/predicate.lux
@@ -0,0 +1,37 @@
+(.module:
+ lux
+ (lux (data (coll [set #+ Set]))))
+
+(type: #export (Pred a)
+ (-> a Bool))
+
+(do-template [<name> <combo>]
+ [(def: #export (<name> left right)
+ (All [a] (-> (Pred a) (Pred a) (Pred a)))
+ (function [value]
+ (<combo> (left value)
+ (right value))))]
+
+ [union or]
+ [intersection and]
+ )
+
+(def: #export (complement predicate)
+ (All [a] (-> (Pred a) (Pred a)))
+ (|>> predicate not))
+
+(def: #export (difference sub base)
+ (All [a] (-> (Pred a) (Pred a) (Pred a)))
+ (function [value]
+ (and (base value)
+ (not (sub value)))))
+
+(def: #export (set set)
+ (All [a] (-> (Set a) (Pred a)))
+ (set.member? set))
+
+(def: #export (rec predicate)
+ (All [a]
+ (-> (-> (Pred a) (Pred a))
+ (Pred a)))
+ (|>> (predicate (rec predicate))))
diff --git a/stdlib/source/lux/lang/type.lux b/stdlib/source/lux/lang/type.lux
index 43febdb8c..33cb2a033 100644
--- a/stdlib/source/lux/lang/type.lux
+++ b/stdlib/source/lux/lang/type.lux
@@ -164,12 +164,12 @@
_
#.None)))
-(def: #export (to-ast type)
+(def: #export (to-code type)
(-> Type Code)
(case type
(#.Primitive name params)
(` (#.Primitive (~ (code.text name))
- (list (~+ (list/map to-ast params)))))
+ (.list (~+ (list/map to-code params)))))
(^template [<tag>]
<tag>
@@ -183,23 +183,17 @@
(^template [<tag>]
(<tag> left right)
- (` (<tag> (~ (to-ast left))
- (~ (to-ast right)))))
- ([#.Function] [#.Apply])
-
- (^template [<tag> <macro> <flattener>]
- (<tag> left right)
- (` (<macro> (~+ (list/map to-ast (<flattener> type))))))
- ([#.Sum | flatten-variant]
- [#.Product & flatten-tuple])
+ (` (<tag> (~ (to-code left))
+ (~ (to-code right)))))
+ ([#.Sum] [#.Product] [#.Function] [#.Apply])
(#.Named name sub-type)
(code.symbol name)
(^template [<tag>]
(<tag> env body)
- (` (<tag> (list (~+ (list/map to-ast env)))
- (~ (to-ast body)))))
+ (` (<tag> (.list (~+ (list/map to-code env)))
+ (~ (to-code body)))))
([#.UnivQ] [#.ExQ])
))
diff --git a/stdlib/source/lux/macro/poly.lux b/stdlib/source/lux/macro/poly.lux
index a14e415b4..a84196f2c 100644
--- a/stdlib/source/lux/macro/poly.lux
+++ b/stdlib/source/lux/macro/poly.lux
@@ -2,7 +2,8 @@
[lux #- function]
(lux (control [monad #+ do Monad]
[eq]
- ["p" parser])
+ ["p" parser]
+ ["ex" exception #+ exception:])
[function]
(data [text "text/" Monoid<Text>]
(coll [list "list/" Fold<List> Monad<List> Monoid<List>]
@@ -260,8 +261,8 @@
(case headT
(#.Bound idx)
(case (dict.get (adjusted-idx env idx) env)
- (#.Some [poly-type poly-ast])
- (wrap poly-ast)
+ (#.Some [poly-type poly-code])
+ (wrap poly-code)
#.None
(p.fail ($_ text/compose "Unknown bound type: " (type.to-text headT))))
@@ -285,6 +286,19 @@
_
(p.fail ($_ text/compose "Not a bound type: " (type.to-text headT))))))
+(exception: #export Not-Existential-Type)
+
+(def: #export existential
+ (Poly Nat)
+ (do p.Monad<Parser>
+ [headT any]
+ (case headT
+ (#.Ex ex-id)
+ (wrap ex-id)
+
+ _
+ (p.fail (Not-Existential-Type (type.to-text headT))))))
+
(def: #export named
(Poly [Ident Type])
(do p.Monad<Parser>
@@ -407,12 +421,12 @@
(~ impl)))))))
## [Derivers]
-(def: #export (to-ast env type)
+(def: #export (to-code env type)
(-> Env Type Code)
(case type
(#.Primitive name params)
(` (#.Primitive (~ (code.text name))
- (list (~+ (list/map (to-ast env) params)))))
+ (list (~+ (list/map (to-code env) params)))))
(^template [<tag>]
<tag>
@@ -427,24 +441,24 @@
(#.Bound idx)
(let [idx (adjusted-idx env idx)]
(if (n/= +0 idx)
- (|> (dict.get idx env) maybe.assume product.left (to-ast env))
+ (|> (dict.get idx env) maybe.assume product.left (to-code env))
(` (.$ (~ (code.nat (n/dec idx)))))))
(#.Apply #.Void (#.Bound idx))
(let [idx (adjusted-idx env idx)]
(if (n/= +0 idx)
- (|> (dict.get idx env) maybe.assume product.left (to-ast env))
+ (|> (dict.get idx env) maybe.assume product.left (to-code env))
(undefined)))
(^template [<tag>]
(<tag> left right)
- (` (<tag> (~ (to-ast env left))
- (~ (to-ast env right)))))
+ (` (<tag> (~ (to-code env left))
+ (~ (to-code env right)))))
([#.Function] [#.Apply])
(^template [<tag> <macro> <flattener>]
(<tag> left right)
- (` (<macro> (~+ (list/map (to-ast env) (<flattener> type))))))
+ (` (<macro> (~+ (list/map (to-code env) (<flattener> type))))))
([#.Sum | type.flatten-variant]
[#.Product & type.flatten-tuple])
@@ -453,7 +467,7 @@
(^template [<tag>]
(<tag> scope body)
- (` (<tag> (list (~+ (list/map (to-ast env) scope)))
- (~ (to-ast env body)))))
+ (` (<tag> (list (~+ (list/map (to-code env) scope)))
+ (~ (to-code env body)))))
([#.UnivQ] [#.ExQ])
))
diff --git a/stdlib/source/lux/macro/poly/eq.lux b/stdlib/source/lux/macro/poly/eq.lux
index 3550df0c0..1da35d91e 100644
--- a/stdlib/source/lux/macro/poly/eq.lux
+++ b/stdlib/source/lux/macro/poly/eq.lux
@@ -36,7 +36,7 @@
inputT poly.peek
#let [@Eq (: (-> Type Code)
(function [type]
- (` (eq.Eq (~ (poly.to-ast *env* type))))))]]
+ (` (eq.Eq (~ (poly.to-code *env* type))))))]]
($_ p.either
## Basic types
(~~ (do-template [<matcher> <eq>]
@@ -136,7 +136,7 @@
[[funcC varsC bodyC] (poly.polymorphic Eq<?>)]
(wrap (` (: (All [(~+ varsC)]
(-> (~+ (list/map (|>> (~) eq.Eq (`)) varsC))
- (eq.Eq ((~ (poly.to-ast *env* inputT)) (~+ varsC)))))
+ (eq.Eq ((~ (poly.to-code *env* inputT)) (~+ varsC)))))
(function (~ funcC) [(~+ varsC)]
(~ bodyC))))))
poly.recursive-call
diff --git a/stdlib/source/lux/macro/poly/functor.lux b/stdlib/source/lux/macro/poly/functor.lux
index 79740c32c..f3ed46041 100644
--- a/stdlib/source/lux/macro/poly/functor.lux
+++ b/stdlib/source/lux/macro/poly/functor.lux
@@ -28,10 +28,10 @@
#let [@Functor (: (-> Type Code)
(function [unwrappedT]
(if (n/= +1 num-vars)
- (` (functor.Functor (~ (poly.to-ast *env* unwrappedT))))
+ (` (functor.Functor (~ (poly.to-code *env* unwrappedT))))
(let [paramsC (|> num-vars n/dec list.indices (L/map (|>> %n code.local-symbol)))]
(` (All [(~+ paramsC)]
- (functor.Functor ((~ (poly.to-ast *env* unwrappedT)) (~+ paramsC)))))))))
+ (functor.Functor ((~ (poly.to-code *env* unwrappedT)) (~+ paramsC)))))))))
Arg<?> (: (-> Code (poly.Poly Code))
(function Arg<?> [valueC]
($_ p.either
diff --git a/stdlib/source/lux/macro/poly/json.lux b/stdlib/source/lux/macro/poly/json.lux
index 155042437..9a3096dff 100644
--- a/stdlib/source/lux/macro/poly/json.lux
+++ b/stdlib/source/lux/macro/poly/json.lux
@@ -105,7 +105,7 @@
[*env* poly.env
#let [@JSON//encode (: (-> Type Code)
(function [type]
- (` (-> (~ (poly.to-ast *env* type)) //.JSON))))]
+ (` (-> (~ (poly.to-code *env* type)) //.JSON))))]
inputT poly.peek]
($_ p.either
<basic>
@@ -178,7 +178,7 @@
(wrap (` (: (All [(~+ varsC)]
(-> (~+ (list/map (function [varC] (` (-> (~ varC) //.JSON)))
varsC))
- (-> ((~ (poly.to-ast *env* inputT)) (~+ varsC))
+ (-> ((~ (poly.to-code *env* inputT)) (~+ varsC))
//.JSON)))
(function (~ funcC) [(~+ varsC)]
(~ bodyC))))))
@@ -217,7 +217,7 @@
[*env* poly.env
#let [@JSON//decode (: (-> Type Code)
(function [type]
- (` (//.Reader (~ (poly.to-ast *env* type))))))]
+ (` (//.Reader (~ (poly.to-code *env* type))))))]
inputT poly.peek]
($_ p.either
<basic>
@@ -273,7 +273,7 @@
[[funcC varsC bodyC] (poly.polymorphic Codec<JSON,?>//decode)]
(wrap (` (: (All [(~+ varsC)]
(-> (~+ (list/map (|>> (~) //.Reader (`)) varsC))
- (//.Reader ((~ (poly.to-ast *env* inputT)) (~+ varsC)))))
+ (//.Reader ((~ (poly.to-code *env* inputT)) (~+ varsC)))))
(function (~ funcC) [(~+ varsC)]
(~ bodyC))))))
poly.bound
diff --git a/stdlib/source/lux/type/refinement.lux b/stdlib/source/lux/type/refinement.lux
new file mode 100644
index 000000000..55aa3cdd7
--- /dev/null
+++ b/stdlib/source/lux/type/refinement.lux
@@ -0,0 +1,72 @@
+(.module:
+ [lux #- Ref type]
+ (lux (control [predicate #+ Pred]
+ [monad #+ do]
+ ["p" parser])
+ (data ["e" error #+ Error])
+ (lang [type "type/" Eq<Type>])
+ (type abstract)
+ [macro]
+ (macro ["s" syntax #+ syntax:]
+ [poly])))
+
+(abstract: #export (Ref t r)
+ {#.doc "A refinement 'r' on type 't' based on a predicate."}
+
+ {#value t
+ #predicate (Pred t)}
+
+ (def: #export (refinement predicate)
+ (All [t]
+ (Ex [r]
+ (-> (Pred t) (-> t (Maybe (Ref t r))))))
+ (function [un-refined]
+ (if (predicate un-refined)
+ (#.Some (@abstraction {#value un-refined
+ #predicate predicate}))
+ #.None)))
+
+ (do-template [<name> <output> <slot>]
+ [(def: #export (<name> refined)
+ (All [t r] (-> (Ref t r) <output>))
+ (|> refined @representation (get@ <slot>)))]
+
+ [un-refine t #value]
+ [predicate (Pred t) #predicate]
+ )
+
+ (def: #export (lift transform)
+ (All [t r]
+ (-> (-> t t)
+ (-> (Ref t r) (Maybe (Ref t r)))))
+ (function [refined]
+ (let [[value predicate] (@representation refined)
+ value' (transform value)]
+ (if (predicate value')
+ (#.Some (@abstraction {#value value'
+ #predicate predicate}))
+ #.None))))
+ )
+
+(def: (refinement-type constructor-type)
+ (-> Type (Error Type))
+ (<| (poly.run constructor-type)
+ (do p.Monad<Parser>
+ [[un-refinedT outputT] (poly.function poly.any poly.any)
+ refined-ex (<| (poly.local (list outputT))
+ poly.apply (p.after (poly.this .Maybe))
+ poly.apply (p.after (poly.this ..Ref))
+ (p.after (poly.this un-refinedT))
+ poly.existential)]
+ (wrap (.type (..Ref un-refinedT (#.Ex refined-ex)))))))
+
+(syntax: #export (type [refinement s.symbol])
+ (do @
+ [constructorT (macro.find-type refinement)
+ refinementT (case (refinement-type constructorT)
+ (#e.Success refinementT)
+ (wrap refinementT)
+
+ (#e.Error error)
+ (p.fail error))]
+ (wrap (list (type.to-code refinementT)))))
diff --git a/stdlib/test/test/lux/math/modular.lux b/stdlib/test/test/lux/math/modular.lux
index 76d56cbc2..1adc737a4 100644
--- a/stdlib/test/test/lux/math/modular.lux
+++ b/stdlib/test/test/lux/math/modular.lux
@@ -11,7 +11,7 @@
lux/test)
(def: %3 (/.modulus 3))
-(def: Mod3 Type (type-of %3))
+(type: Mod3 (~ (type-of %3)))
(def: modulusR
(r.Random Int)
diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux
index 1742334d8..12ab83fc0 100644
--- a/stdlib/test/tests.lux
+++ b/stdlib/test/tests.lux
@@ -74,7 +74,8 @@
["_." udp]))
))
(lux (control [contract]
- [concatenative])
+ [concatenative]
+ [predicate])
(data [env]
[trace]
[store]
@@ -85,7 +86,8 @@
(coll (tree ["tree_." parser])))
[macro]
(macro (poly [json]))
- (type [unit])
+ (type [unit]
+ [refinement])
[world/env]
[world/console])
)
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 05:55:01 +0000