1 files changed, 89 insertions, 0 deletions
diff --git a/stdlib/source/library/lux/type/refinement.lux b/stdlib/source/library/lux/type/refinement.lux
new file mode 100644
index 000000000..a3e49104d
--- /dev/null
+++ b/stdlib/source/library/lux/type/refinement.lux
@@ -0,0 +1,89 @@
+(.module:
+  [library
+   [lux (#- type)
+    [abstract
+     [predicate (#+ Predicate)]]
+    ["." macro
+     [syntax (#+ syntax:)]]
+    ["." type
+     abstract]]])
+
+(abstract: #export (Refined t %)
+  {#value t
+   #predicate (Predicate t)}
+
+  {#.doc "A refined type '%' of base type 't' using a predicate."}
+
+  (type: #export (Refiner t %)
+    (-> t (Maybe (Refined t %))))
+
+  (def: #export (refinement predicate)
+    (All [t]
+      (Ex [%]
+        (-> (Predicate t) (Refiner t %))))
+    (function (_ un_refined)
+      (if (predicate un_refined)
+        (#.Some (:abstraction {#value un_refined
+                               #predicate predicate}))
+        #.None)))
+
+  (template [<name> <output> <slot>]
+    [(def: #export <name>
+       (All [t %] (-> (Refined t %) <output>))
+       (|>> :representation (get@ <slot>)))]
+
+    [un_refine t             #value]
+    [predicate (Predicate t) #predicate]
+    )
+
+  (def: #export (lift transform)
+    (All [t %]
+      (-> (-> t t)
+          (-> (Refined t %) (Maybe (Refined t %)))))
+    (function (_ refined)
+      (let [(^slots [#value #predicate]) (:representation refined)
+            value' (transform value)]
+        (if (predicate value')
+          (#.Some (:abstraction {#value value'
+                                 #predicate predicate}))
+          #.None))))
+  )
+
+(def: #export (filter refiner values)
+  (All [t %] (-> (Refiner t %) (List t) (List (Refined t %))))
+  (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 %] (-> (Refiner t %) (List t) [(List (Refined t %)) (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)]))))
+
+(syntax: #export (type refiner)
+  (macro.with_gensyms [g!t g!%]
+    (wrap (list (` ((~! type.:by_example) [(~ g!t) (~ g!%)]
+                    (..Refiner (~ g!t) (~ g!%))
+                    (~ refiner)
+                    
+                    (..Refined (~ g!t) (~ g!%))))))))