diff options
Diffstat (limited to 'demo/more/dbgrid.urs')
-rw-r--r-- | demo/more/dbgrid.urs | 91 |
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 |