- Added module for predicates.

- Added refinement types.
- Small refactorings and fixes.
- Added the capacity to unquote expressions inside the 'lux.type' macro.

10 files changed, 158 insertions, 36 deletions

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])
   )