Mercurial > urweb
comparison demo/more/dbgrid.urs @ 944:da3ec6014d2f
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 |