annotate demo/more/dbgrid.urs @ 937:37dd42935dad

Summary row with aggregates
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 10:18:56 -0400
parents 2422360c78a3
children e2be476673f2
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@915 5 con colMeta' = fn (row :: {Type}) (t :: Type) =>
adamc@915 6 {Header : string,
adamc@915 7 Project : $row -> transaction t,
adamc@915 8 Update : $row -> t -> transaction ($row),
adamc@915 9 Display : t -> xbody,
adamc@915 10 Edit : t -> xbody,
adamc@915 11 Validate : t -> signal bool}
adamc@915 12
adamc@915 13 con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) =>
adamc@915 14 {Initialize : transaction global_t.1,
adamc@915 15 Handlers : global_t.1 -> colMeta' row global_t.2}
adamc@915 16
adamc@935 17 con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
adamc@935 18 {Initial : acc,
adamc@935 19 Step : $row -> acc -> acc,
adamc@935 20 Display : acc -> xbody}
adamc@935 21
adamc@915 22 structure Direct : sig
adamc@930 23 con metaBase = fn actual_input :: (Type * Type) =>
adamc@930 24 {Display : actual_input.2 -> xbody,
adamc@930 25 Edit : actual_input.2 -> xbody,
adamc@930 26 Initialize : actual_input.1 -> transaction actual_input.2,
adamc@930 27 Parse : actual_input.2 -> signal (option actual_input.1)}
adamc@930 28
adamc@930 29 datatype metaBoth actual input =
adamc@930 30 NonNull of metaBase (actual, input) * metaBase (option actual, input)
adamc@930 31 | Nullable of metaBase (actual, input)
adamc@930 32
adamc@915 33 con meta = fn global_actual_input :: (Type * Type * Type) =>
adamc@915 34 {Initialize : transaction global_actual_input.1,
adamc@915 35 Handlers : global_actual_input.1
adamc@930 36 -> metaBoth global_actual_input.2 global_actual_input.3}
adamc@915 37
adamc@915 38 con editableState :: (Type * Type * Type) -> (Type * Type)
adamc@915 39 val editable : ts ::: (Type * Type * Type) -> rest ::: {Type}
adamc@915 40 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
adamc@915 41 -> colMeta ([nm = ts.2] ++ rest)
adamc@915 42 (editableState ts)
adamc@915 43
adamc@915 44 con readOnlyState :: (Type * Type * Type) -> (Type * Type)
adamc@915 45 val readOnly : ts ::: (Type * Type * Type) -> rest ::: {Type}
adamc@915 46 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
adamc@915 47 -> colMeta ([nm = ts.2] ++ rest)
adamc@915 48 (readOnlyState ts)
adamc@915 49
adamc@930 50 val nullable : global ::: Type -> actual ::: Type -> input ::: Type
adamc@930 51 -> meta (global, actual, input)
adamc@930 52 -> meta (global, option actual, input)
adamc@930 53
adamc@915 54 type intGlobal
adamc@915 55 type intInput
adamc@915 56 val int : meta (intGlobal, int, intInput)
adamc@915 57
adamc@915 58 type stringGlobal
adamc@915 59 type stringInput
adamc@915 60 val string : meta (stringGlobal, string, stringInput)
adamc@915 61
adamc@915 62 type boolGlobal
adamc@915 63 type boolInput
adamc@915 64 val bool : meta (boolGlobal, bool, boolInput)
adamc@915 65
adamc@915 66 functor Foreign (M : sig
adamc@915 67 con row :: {Type}
adamc@915 68 con t :: Type
adamc@915 69 val show_t : show t
adamc@915 70 val read_t : read t
adamc@915 71 val eq_t : eq t
adamc@915 72 val inj_t : sql_injectable t
adamc@915 73 con nm :: Name
adamc@915 74 constraint [nm] ~ row
adamc@915 75 table tab : ([nm = t] ++ row)
adamc@915 76 val render : $([nm = t] ++ row) -> string
adamc@915 77 end) : sig
adamc@915 78 con global :: Type
adamc@915 79 con input :: Type
adamc@915 80 val meta : meta (global, M.t, input)
adamc@915 81 end
adamc@915 82 end
adamc@915 83
adamc@915 84 con computedState :: (Type * Type)
adamc@915 85 val computed : row ::: {Type} -> t ::: Type -> show t
adamc@915 86 -> string -> ($row -> t) -> colMeta row computedState
adamc@915 87 val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState
adamc@915 88
adamc@915 89 functor Make(M : sig
adamc@915 90 con key :: {Type}
adamc@915 91 con row :: {Type}
adamc@915 92 constraint key ~ row
adamc@915 93 table tab : (key ++ row)
adamc@915 94
adamc@915 95 val raw : $(map rawMeta (key ++ row))
adamc@915 96
adamc@915 97 con cols :: {(Type * Type)}
adamc@915 98 val cols : $(map (colMeta (key ++ row)) cols)
adamc@915 99
adamc@915 100 val keyFolder : folder key
adamc@915 101 val rowFolder : folder row
adamc@915 102 val colsFolder : folder cols
adamc@935 103
adamc@935 104 con aggregates :: {Type}
adamc@935 105 val aggregates : $(map (aggregateMeta (key ++ row)) aggregates)
adamc@937 106 val aggFolder : folder aggregates
adamc@915 107 end) : sig
adamc@915 108 type grid
adamc@915 109
adamc@915 110 val grid : transaction grid
adamc@915 111 val sync : grid -> transaction unit
adamc@915 112 val render : grid -> xbody
adamc@915 113 end