Mercurial > urweb

comparison 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
comparison
equal deleted inserted replaced
943:e2194a6793ae 944:da3ec6014d2f
1 con rawMeta = fn t :: Type => 1 con rawMeta = fn t :: Type =>
2 {New : transaction t, 2 {New : transaction t,
3 Inj : sql_injectable t} 3 Inj : sql_injectable t}
4 4
5 con colMeta' = fn (row :: {Type}) (t :: Type) => 5 con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) =>
6 {Header : string, 6 {Header : string,
7 Project : $row -> transaction t, 7 Project : $row -> transaction input,
8 Update : $row -> t -> transaction ($row), 8 Update : $row -> input -> transaction ($row),
9 Display : t -> xbody, 9 Display : input -> xbody,
10 Edit : t -> xbody, 10 Edit : input -> xbody,
11 Validate : t -> signal bool} 11 Validate : input -> signal bool,
12 CreateFilter : transaction filter,
13 DisplayFilter : filter -> xbody,
14 Filter : filter -> $row -> signal bool}
12 15
13 con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) => 16 con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) =>
14 {Initialize : transaction global_t.1, 17 {Initialize : transaction global_input_filter.1,
15 Handlers : global_t.1 -> colMeta' row global_t.2} 18 Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
16 19
17 con aggregateMeta = fn (row :: {Type}) (acc :: Type) => 20 con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
18 {Initial : acc, 21 {Initial : acc,
19 Step : $row -> acc -> acc, 22 Step : $row -> acc -> acc,
20 Display : acc -> xbody} 23 Display : acc -> xbody}
21 24
22 structure Direct : sig 25 structure Direct : sig
23 con metaBase = fn actual_input :: (Type * Type) => 26 con metaBase = fn actual_input_filter :: (Type * Type * Type) =>
24 {Display : actual_input.2 -> xbody, 27 {Display : actual_input_filter.2 -> xbody,
25 Edit : actual_input.2 -> xbody, 28 Edit : actual_input_filter.2 -> xbody,
26 Initialize : actual_input.1 -> transaction actual_input.2, 29 Initialize : actual_input_filter.1 -> transaction actual_input_filter.2,
27 Parse : actual_input.2 -> signal (option actual_input.1)} 30 Parse : actual_input_filter.2 -> signal (option actual_input_filter.1),
31 CreateFilter : transaction actual_input_filter.3,
32 DisplayFilter : actual_input_filter.3 -> xbody,
33 Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool}
28 34
29 datatype metaBoth actual input = 35 datatype metaBoth actual input filter =
30 NonNull of metaBase (actual, input) * metaBase (option actual, input) 36 NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
31 | Nullable of metaBase (actual, input) 37 | Nullable of metaBase (actual, input, filter)
32 38
33 con meta = fn global_actual_input :: (Type * Type * Type) => 39 con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
34 {Initialize : transaction global_actual_input.1, 40 {Initialize : transaction global_actual_input_filter.1,
35 Handlers : global_actual_input.1 41 Handlers : global_actual_input_filter.1
36 -> metaBoth global_actual_input.2 global_actual_input.3} 42 -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
43 global_actual_input_filter.4}
37 44
38 con editableState :: (Type * Type * Type) -> (Type * Type) 45 con editableState :: (Type * Type * Type * Type) -> (Type * Type * Type)
39 val editable : ts ::: (Type * Type * Type) -> rest ::: {Type} 46 val editable : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
40 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts 47 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
41 -> colMeta ([nm = ts.2] ++ rest) 48 -> colMeta ([nm = ts.2] ++ rest)
42 (editableState ts) 49 (editableState ts)
43 50
44 con readOnlyState :: (Type * Type * Type) -> (Type * Type) 51 con readOnlyState :: (Type * Type * Type * Type) -> (Type * Type * Type)
45 val readOnly : ts ::: (Type * Type * Type) -> rest ::: {Type} 52 val readOnly : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
46 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts 53 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
47 -> colMeta ([nm = ts.2] ++ rest) 54 -> colMeta ([nm = ts.2] ++ rest)
48 (readOnlyState ts) 55 (readOnlyState ts)
49 56
50 val nullable : global ::: Type -> actual ::: Type -> input ::: Type 57 val nullable : global ::: Type -> actual ::: Type -> input ::: Type -> filter ::: Type
51 -> meta (global, actual, input) 58 -> meta (global, actual, input, filter)
52 -> meta (global, option actual, input) 59 -> meta (global, option actual, input, filter)
53 60
54 type intGlobal 61 type intGlobal
55 type intInput 62 type intInput
56 val int : meta (intGlobal, int, intInput) 63 type intFilter
64 val int : meta (intGlobal, int, intInput, intFilter)
57 65
58 type stringGlobal 66 type stringGlobal
59 type stringInput 67 type stringInput
60 val string : meta (stringGlobal, string, stringInput) 68 type stringFilter
69 val string : meta (stringGlobal, string, stringInput, stringFilter)
61 70
62 type boolGlobal 71 type boolGlobal
63 type boolInput 72 type boolInput
64 val bool : meta (boolGlobal, bool, boolInput) 73 type boolFilter
74 val bool : meta (boolGlobal, bool, boolInput, boolFilter)
65 75
66 functor Foreign (M : sig 76 functor Foreign (M : sig
67 con row :: {Type} 77 con row :: {Type}
68 con t :: Type 78 con t :: Type
69 val show_t : show t 79 val show_t : show t
73 con nm :: Name 83 con nm :: Name
74 constraint [nm] ~ row 84 constraint [nm] ~ row
75 table tab : ([nm = t] ++ row) 85 table tab : ([nm = t] ++ row)
76 val render : $([nm = t] ++ row) -> string 86 val render : $([nm = t] ++ row) -> string
77 end) : sig 87 end) : sig
78 con global :: Type 88 type global
79 con input :: Type 89 type input
80 val meta : meta (global, M.t, input) 90 type filter
91 val meta : meta (global, M.t, input, filter)
81 end 92 end
82 end 93 end
83 94
84 con computedState :: (Type * Type) 95 con computedState :: (Type * Type * Type)
85 val computed : row ::: {Type} -> t ::: Type -> show t 96 val computed : row ::: {Type} -> t ::: Type -> show t
86 -> string -> ($row -> t) -> colMeta row computedState 97 -> string -> ($row -> t) -> colMeta row computedState
87 val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState 98 val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState
88 99
89 functor Make(M : sig 100 functor Make(M : sig
92 constraint key ~ row 103 constraint key ~ row
93 table tab : (key ++ row) 104 table tab : (key ++ row)
94 105
95 val raw : $(map rawMeta (key ++ row)) 106 val raw : $(map rawMeta (key ++ row))
96 107
97 con cols :: {(Type * Type)} 108 con cols :: {(Type * Type * Type)}
98 val cols : $(map (colMeta (key ++ row)) cols) 109 val cols : $(map (colMeta (key ++ row)) cols)
99 110
100 val keyFolder : folder key 111 val keyFolder : folder key
101 val rowFolder : folder row 112 val rowFolder : folder row
102 val colsFolder : folder cols 113 val colsFolder : folder cols