diff options
author | Eduardo Julian | 2018-05-26 19:49:45 -0400 |
---|---|---|
committer | Eduardo Julian | 2018-05-26 19:49:45 -0400 |
commit | 8934a10fb289ea0c09891bdd7a409b8dd1152256 (patch) | |
tree | 11e902b40eed5cd96c35480f4037ed65a3cf4465 /stdlib/source | |
parent | 223a2fad3a6140b942923fe43712ac0f7d8caf52 (diff) |
- Added filter/partition functionality to refinement types.
Diffstat (limited to 'stdlib/source')
-rw-r--r-- | stdlib/source/lux/type/refinement.lux | 36 |
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) |