Filters implementation type-checking

1 files changed, 51 insertions, 40 deletions

diff --git a/demo/more/dbgrid.urs b/demo/more/dbgrid.urs
index 404d0f62..58c5197a 100644
--- a/demo/more/dbgrid.urs
+++ b/demo/more/dbgrid.urs
@@ -2,17 +2,20 @@ con rawMeta = fn t :: Type =>
                  {New : transaction t,
                   Inj : sql_injectable t}
 
-con colMeta' = fn (row :: {Type}) (t :: Type) =>
+con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) =>
                   {Header : string,
-                   Project : $row -> transaction t,
-                   Update : $row -> t -> transaction ($row),
-                   Display : t -> xbody,
-                   Edit : t -> xbody,
-                   Validate : t -> signal bool}
-
-con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) =>
-                 {Initialize : transaction global_t.1,
-                  Handlers : global_t.1 -> colMeta' row global_t.2}
+                   Project : $row -> transaction input,
+                   Update : $row -> input -> transaction ($row),
+                   Display : input -> xbody,
+                   Edit : input -> xbody,
+                   Validate : input -> signal bool,
+                   CreateFilter : transaction filter,
+                   DisplayFilter : filter -> xbody,
+                   Filter : filter -> $row -> signal bool}
+
+con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) =>
+                 {Initialize : transaction global_input_filter.1,
+                  Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
 
 con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
                        {Initial : acc,
@@ -20,48 +23,55 @@ con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
                         Display : acc -> xbody}
 
 structure Direct : sig
-    con metaBase = fn actual_input :: (Type * Type) =>
-                  {Display : actual_input.2 -> xbody,
-                   Edit : actual_input.2 -> xbody,
-                   Initialize : actual_input.1 -> transaction actual_input.2,
-                   Parse : actual_input.2 -> signal (option actual_input.1)}
-
-    datatype metaBoth actual input =
-             NonNull of metaBase (actual, input) * metaBase (option actual, input)
-           | Nullable of metaBase (actual, input)
-
-    con meta = fn global_actual_input :: (Type * Type * Type) =>
-                  {Initialize : transaction global_actual_input.1,
-                   Handlers : global_actual_input.1
-                              -> metaBoth global_actual_input.2 global_actual_input.3}
-
-    con editableState :: (Type * Type * Type) -> (Type * Type)
-    val editable : ts ::: (Type * Type * Type) -> rest ::: {Type}
+    con metaBase = fn actual_input_filter :: (Type * Type * Type) =>
+                  {Display : actual_input_filter.2 -> xbody,
+                   Edit : actual_input_filter.2 -> xbody,
+                   Initialize : actual_input_filter.1 -> transaction actual_input_filter.2,
+                   Parse : actual_input_filter.2 -> signal (option actual_input_filter.1),
+                   CreateFilter : transaction actual_input_filter.3,
+                   DisplayFilter : actual_input_filter.3 -> xbody,
+                   Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool}
+
+    datatype metaBoth actual input filter =
+             NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
+           | Nullable of metaBase (actual, input, filter)
+
+    con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
+                  {Initialize : transaction global_actual_input_filter.1,
+                   Handlers : global_actual_input_filter.1
+                              -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
+                                          global_actual_input_filter.4}
+
+    con editableState :: (Type * Type * Type * Type) -> (Type * Type * Type)
+    val editable : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
                    -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
                                                      -> colMeta ([nm = ts.2] ++ rest)
                                                                 (editableState ts)
 
-    con readOnlyState :: (Type * Type * Type) -> (Type * Type)
-    val readOnly : ts ::: (Type * Type * Type) -> rest ::: {Type}
+    con readOnlyState :: (Type * Type * Type * Type) -> (Type * Type * Type)
+    val readOnly : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
                    -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
                                                      -> colMeta ([nm = ts.2] ++ rest)
                                                                 (readOnlyState ts)
 
-    val nullable : global ::: Type -> actual ::: Type -> input ::: Type
-                   -> meta (global, actual, input)
-                   -> meta (global, option actual, input)
+    val nullable : global ::: Type -> actual ::: Type -> input ::: Type -> filter ::: Type
+                   -> meta (global, actual, input, filter)
+                   -> meta (global, option actual, input, filter)
 
     type intGlobal
     type intInput
-    val int : meta (intGlobal, int, intInput)
+    type intFilter
+    val int : meta (intGlobal, int, intInput, intFilter)
 
     type stringGlobal
     type stringInput
-    val string : meta (stringGlobal, string, stringInput)
+    type stringFilter
+    val string : meta (stringGlobal, string, stringInput, stringFilter)
 
     type boolGlobal
     type boolInput
-    val bool : meta (boolGlobal, bool, boolInput)
+    type boolFilter
+    val bool : meta (boolGlobal, bool, boolInput, boolFilter)
 
     functor Foreign (M : sig
                          con row :: {Type}
@@ -75,13 +85,14 @@ structure Direct : sig
                          table tab : ([nm = t] ++ row)
                          val render : $([nm = t] ++ row) -> string
                      end) : sig
-        con global :: Type
-        con input :: Type
-        val meta : meta (global, M.t, input)
+        type global
+        type input
+        type filter
+        val meta : meta (global, M.t, input, filter)
     end
 end
 
-con computedState :: (Type * Type)
+con computedState :: (Type * Type * Type)
 val computed : row ::: {Type} -> t ::: Type -> show t
                -> string -> ($row -> t) -> colMeta row computedState
 val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState
@@ -94,7 +105,7 @@ functor Make(M : sig
 
                  val raw : $(map rawMeta (key ++ row))
 
-                 con cols :: {(Type * Type)}
+                 con cols :: {(Type * Type * Type)}
                  val cols : $(map (colMeta (key ++ row)) cols)
 
                  val keyFolder : folder key