aboutsummaryrefslogtreecommitdiff
path: root/stdlib
diff options
context:
space:
mode:
authorEduardo Julian2018-05-26 19:49:45 -0400
committerEduardo Julian2018-05-26 19:49:45 -0400
commit8934a10fb289ea0c09891bdd7a409b8dd1152256 (patch)
tree11e902b40eed5cd96c35480f4037ed65a3cf4465 /stdlib
parent223a2fad3a6140b942923fe43712ac0f7d8caf52 (diff)
- Added filter/partition functionality to refinement types.
Diffstat (limited to 'stdlib')
-rw-r--r--stdlib/source/lux/type/refinement.lux36
1 files changed, 35 insertions, 1 deletions
diff --git a/stdlib/source/lux/type/refinement.lux b/stdlib/source/lux/type/refinement.lux
index 051166eb9..7431c93fe 100644
--- a/stdlib/source/lux/type/refinement.lux
+++ b/stdlib/source/lux/type/refinement.lux
@@ -16,10 +16,13 @@
{#value t
#predicate (Pred t)}
+ (type: #export (Refiner t r)
+ (-> t (Maybe (Ref t r))))
+
(def: #export (refinement predicate)
(All [t]
(Ex [r]
- (-> (Pred t) (-> t (Maybe (Ref t r))))))
+ (-> (Pred t) (Refiner t r))))
(function (_ un-refined)
(if (predicate un-refined)
(#.Some (@abstraction {#value un-refined
@@ -48,6 +51,37 @@
#.None))))
)
+(def: #export (filter refiner values)
+ (All [t r] (-> (Refiner t r) (List t) (List (Ref t r))))
+ (case values
+ #.Nil
+ #.Nil
+
+ (#.Cons head tail)
+ (case (refiner head)
+ (#.Some refined)
+ (#.Cons refined (filter refiner tail))
+
+ #.None
+ (filter refiner tail))))
+
+(def: #export (partition refiner values)
+ (All [t r] (-> (Refiner t r) (List t) [(List (Ref t r)) (List t)]))
+ (case values
+ #.Nil
+ [#.Nil #.Nil]
+
+ (#.Cons head tail)
+ (let [[yes no] (partition refiner tail)]
+ (case (refiner head)
+ (#.Some refined)
+ [(#.Cons refined yes)
+ no]
+
+ #.None
+ [yes
+ (#.Cons head no)]))))
+
(def: (refinement-type constructor-type)
(-> Type (Error Type))
(<| (poly.run constructor-type)