Mercurial > urweb
diff demo/more/dbgrid.urs @ 944:da3ec6014d2f
Filters implementation type-checking
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 15 Sep 2009 15:48:53 -0400 |
parents | e2be476673f2 |
children | 8c37699de273 |
line wrap: on
line diff
--- a/demo/more/dbgrid.urs Tue Sep 15 13:07:57 2009 -0400 +++ b/demo/more/dbgrid.urs Tue Sep 15 15:48:53 2009 -0400 @@ -2,17 +2,20 @@ {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} + 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_t :: (Type * Type)) => - {Initialize : transaction global_t.1, - Handlers : global_t.1 -> colMeta' row global_t.2} +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 @@ 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)} + 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 = - NonNull of metaBase (actual, input) * metaBase (option actual, input) - | Nullable of metaBase (actual, input) + 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 :: (Type * Type * Type) => - {Initialize : transaction global_actual_input.1, - Handlers : global_actual_input.1 - -> metaBoth global_actual_input.2 global_actual_input.3} + 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) - val editable : ts ::: (Type * Type * Type) -> rest ::: {Type} + 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 @@ 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 @@ 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