Mercurial > urweb

annotate demo/more/dbgrid.urs @ 2010:403f0cc65b9c

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