Mercurial > urweb

annotate demo/more/dbgrid.urs @ 944:da3ec6014d2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Filters implementation type-checking
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 15:48:53 -0400
parents e2be476673f2
children 8c37699de273
rev   line source
adamc@915 1 con rawMeta = fn t :: Type =>
adamc@915 2 {New : transaction t,
adamc@915 3 Inj : sql_injectable t}
adamc@915 4
adamc@944 5 con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) =>
adamc@915 6 {Header : string,
adamc@944 7 Project : $row -> transaction input,
adamc@944 8 Update : $row -> input -> transaction ($row),
adamc@944 9 Display : input -> xbody,
adamc@944 10 Edit : input -> xbody,
adamc@944 11 Validate : input -> signal bool,
adamc@944 12 CreateFilter : transaction filter,
adamc@944 13 DisplayFilter : filter -> xbody,
adamc@944 14 Filter : filter -> $row -> signal bool}
adamc@915 15
adamc@944 16 con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) =>
adamc@944 17 {Initialize : transaction global_input_filter.1,
adamc@944 18 Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
adamc@915 19
adamc@935 20 con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
adamc@935 21 {Initial : acc,
adamc@935 22 Step : $row -> acc -> acc,
adamc@935 23 Display : acc -> xbody}
adamc@935 24
adamc@915 25 structure Direct : sig
adamc@944 26 con metaBase = fn actual_input_filter :: (Type * Type * Type) =>
adamc@944 27 {Display : actual_input_filter.2 -> xbody,
adamc@944 28 Edit : actual_input_filter.2 -> xbody,
adamc@944 29 Initialize : actual_input_filter.1 -> transaction actual_input_filter.2,
adamc@944 30 Parse : actual_input_filter.2 -> signal (option actual_input_filter.1),
adamc@944 31 CreateFilter : transaction actual_input_filter.3,
adamc@944 32 DisplayFilter : actual_input_filter.3 -> xbody,
adamc@944 33 Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool}
adamc@930 34
adamc@944 35 datatype metaBoth actual input filter =
adamc@944 36 NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
adamc@944 37 | Nullable of metaBase (actual, input, filter)
adamc@930 38
adamc@944 39 con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
adamc@944 40 {Initialize : transaction global_actual_input_filter.1,
adamc@944 41 Handlers : global_actual_input_filter.1
adamc@944 42 -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
adamc@944 43 global_actual_input_filter.4}
adamc@915 44
adamc@944 45 con editableState :: (Type * Type * Type * Type) -> (Type * Type * Type)
adamc@944 46 val editable : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
adamc@915 47 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
adamc@915 48 -> colMeta ([nm = ts.2] ++ rest)
adamc@915 49 (editableState ts)
adamc@915 50
adamc@944 51 con readOnlyState :: (Type * Type * Type * Type) -> (Type * Type * Type)
adamc@944 52 val readOnly : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
adamc@915 53 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
adamc@915 54 -> colMeta ([nm = ts.2] ++ rest)
adamc@915 55 (readOnlyState ts)
adamc@915 56
adamc@944 57 val nullable : global ::: Type -> actual ::: Type -> input ::: Type -> filter ::: Type
adamc@944 58 -> meta (global, actual, input, filter)
adamc@944 59 -> meta (global, option actual, input, filter)
adamc@930 60
adamc@915 61 type intGlobal
adamc@915 62 type intInput
adamc@944 63 type intFilter
adamc@944 64 val int : meta (intGlobal, int, intInput, intFilter)
adamc@915 65
adamc@915 66 type stringGlobal
adamc@915 67 type stringInput
adamc@944 68 type stringFilter
adamc@944 69 val string : meta (stringGlobal, string, stringInput, stringFilter)
adamc@915 70
adamc@915 71 type boolGlobal
adamc@915 72 type boolInput
adamc@944 73 type boolFilter
adamc@944 74 val bool : meta (boolGlobal, bool, boolInput, boolFilter)
adamc@915 75
adamc@915 76 functor Foreign (M : sig
adamc@915 77 con row :: {Type}
adamc@915 78 con t :: Type
adamc@915 79 val show_t : show t
adamc@915 80 val read_t : read t
adamc@915 81 val eq_t : eq t
adamc@915 82 val inj_t : sql_injectable t
adamc@915 83 con nm :: Name
adamc@915 84 constraint [nm] ~ row
adamc@915 85 table tab : ([nm = t] ++ row)
adamc@915 86 val render : $([nm = t] ++ row) -> string
adamc@915 87 end) : sig
adamc@944 88 type global
adamc@944 89 type input
adamc@944 90 type filter
adamc@944 91 val meta : meta (global, M.t, input, filter)
adamc@915 92 end
adamc@915 93 end
adamc@915 94
adamc@944 95 con computedState :: (Type * Type * Type)
adamc@915 96 val computed : row ::: {Type} -> t ::: Type -> show t
adamc@915 97 -> string -> ($row -> t) -> colMeta row computedState
adamc@915 98 val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState
adamc@915 99
adamc@915 100 functor Make(M : sig
adamc@915 101 con key :: {Type}
adamc@915 102 con row :: {Type}
adamc@915 103 constraint key ~ row
adamc@915 104 table tab : (key ++ row)
adamc@915 105
adamc@915 106 val raw : $(map rawMeta (key ++ row))
adamc@915 107
adamc@944 108 con cols :: {(Type * Type * Type)}
adamc@915 109 val cols : $(map (colMeta (key ++ row)) cols)
adamc@915 110
adamc@915 111 val keyFolder : folder key
adamc@915 112 val rowFolder : folder row
adamc@915 113 val colsFolder : folder cols
adamc@935 114
adamc@935 115 con aggregates :: {Type}
adamc@935 116 val aggregates : $(map (aggregateMeta (key ++ row)) aggregates)
adamc@937 117 val aggFolder : folder aggregates
adamc@915 118 end) : sig
adamc@915 119 type grid
adamc@915 120
adamc@915 121 val grid : transaction grid
adamc@915 122 val sync : grid -> transaction unit
adamc@915 123 val render : grid -> xbody
adamc@940 124
adamc@940 125 val showSelection : grid -> source bool
adamc@940 126 val selection : grid -> signal (list ($(M.key ++ M.row)))
adamc@915 127 end