summaryrefslogtreecommitdiff
path: root/demo/more/dbgrid.urs
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-09-15 15:48:53 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-09-15 15:48:53 -0400
commitefa6f97eee79311cd06592ed0241acfc40561785 (patch)
tree47760017bfc37999184289878129fd3e64115e52 /demo/more/dbgrid.urs
parent8e944e62818045b820f45776a396bc1b66ab3056 (diff)
Filters implementation type-checking
Diffstat (limited to 'demo/more/dbgrid.urs')
-rw-r--r--demo/more/dbgrid.urs91
1 files changed, 51 insertions, 40 deletions
diff --git a/demo/more/dbgrid.urs b/demo/more/dbgrid.urs
index 404d0f62..58c5197a 100644
--- a/demo/more/dbgrid.urs
+++ b/demo/more/dbgrid.urs
@@ -2,17 +2,20 @@ con rawMeta = fn t :: Type =>
{New : transaction t,
Inj : sql_injectable t}
-con colMeta' = fn (row :: {Type}) (t :: Type) =>
+con colMeta' = fn (row :: {Type}) (input :: Type) (filter :: Type) =>
{Header : string,
- Project : $row -> transaction t,
- Update : $row -> t -> transaction ($row),
- Display : t -> xbody,
- Edit : t -> xbody,
- Validate : t -> signal bool}
-
-con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) =>
- {Initialize : transaction global_t.1,
- Handlers : global_t.1 -> colMeta' row global_t.2}
+ Project : $row -> transaction input,
+ Update : $row -> input -> transaction ($row),
+ Display : input -> xbody,
+ Edit : input -> xbody,
+ Validate : input -> signal bool,
+ CreateFilter : transaction filter,
+ DisplayFilter : filter -> xbody,
+ Filter : filter -> $row -> signal bool}
+
+con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) =>
+ {Initialize : transaction global_input_filter.1,
+ Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
{Initial : acc,
@@ -20,48 +23,55 @@ con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
Display : acc -> xbody}
structure Direct : sig
- con metaBase = fn actual_input :: (Type * Type) =>
- {Display : actual_input.2 -> xbody,
- Edit : actual_input.2 -> xbody,
- Initialize : actual_input.1 -> transaction actual_input.2,
- Parse : actual_input.2 -> signal (option actual_input.1)}
-
- datatype metaBoth actual input =
- NonNull of metaBase (actual, input) * metaBase (option actual, input)
- | Nullable of metaBase (actual, input)
-
- con meta = fn global_actual_input :: (Type * Type * Type) =>
- {Initialize : transaction global_actual_input.1,
- Handlers : global_actual_input.1
- -> metaBoth global_actual_input.2 global_actual_input.3}
-
- con editableState :: (Type * Type * Type) -> (Type * Type)
- val editable : ts ::: (Type * Type * Type) -> rest ::: {Type}
+ con metaBase = fn actual_input_filter :: (Type * Type * Type) =>
+ {Display : actual_input_filter.2 -> xbody,
+ Edit : actual_input_filter.2 -> xbody,
+ Initialize : actual_input_filter.1 -> transaction actual_input_filter.2,
+ Parse : actual_input_filter.2 -> signal (option actual_input_filter.1),
+ CreateFilter : transaction actual_input_filter.3,
+ DisplayFilter : actual_input_filter.3 -> xbody,
+ Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool}
+
+ datatype metaBoth actual input filter =
+ NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
+ | Nullable of metaBase (actual, input, filter)
+
+ con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
+ {Initialize : transaction global_actual_input_filter.1,
+ Handlers : global_actual_input_filter.1
+ -> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
+ global_actual_input_filter.4}
+
+ con editableState :: (Type * Type * Type * Type) -> (Type * Type * Type)
+ val editable : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
-> nm :: Name -> [[nm] ~ rest] => string -> meta ts
-> colMeta ([nm = ts.2] ++ rest)
(editableState ts)
- con readOnlyState :: (Type * Type * Type) -> (Type * Type)
- val readOnly : ts ::: (Type * Type * Type) -> rest ::: {Type}
+ con readOnlyState :: (Type * Type * Type * Type) -> (Type * Type * Type)
+ val readOnly : ts ::: (Type * Type * Type * Type) -> rest ::: {Type}
-> nm :: Name -> [[nm] ~ rest] => string -> meta ts
-> colMeta ([nm = ts.2] ++ rest)
(readOnlyState ts)
- val nullable : global ::: Type -> actual ::: Type -> input ::: Type
- -> meta (global, actual, input)
- -> meta (global, option actual, input)
+ val nullable : global ::: Type -> actual ::: Type -> input ::: Type -> filter ::: Type
+ -> meta (global, actual, input, filter)
+ -> meta (global, option actual, input, filter)
type intGlobal
type intInput
- val int : meta (intGlobal, int, intInput)
+ type intFilter
+ val int : meta (intGlobal, int, intInput, intFilter)
type stringGlobal
type stringInput
- val string : meta (stringGlobal, string, stringInput)
+ type stringFilter
+ val string : meta (stringGlobal, string, stringInput, stringFilter)
type boolGlobal
type boolInput
- val bool : meta (boolGlobal, bool, boolInput)
+ type boolFilter
+ val bool : meta (boolGlobal, bool, boolInput, boolFilter)
functor Foreign (M : sig
con row :: {Type}
@@ -75,13 +85,14 @@ structure Direct : sig
table tab : ([nm = t] ++ row)
val render : $([nm = t] ++ row) -> string
end) : sig
- con global :: Type
- con input :: Type
- val meta : meta (global, M.t, input)
+ type global
+ type input
+ type filter
+ val meta : meta (global, M.t, input, filter)
end
end
-con computedState :: (Type * Type)
+con computedState :: (Type * Type * Type)
val computed : row ::: {Type} -> t ::: Type -> show t
-> string -> ($row -> t) -> colMeta row computedState
val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState
@@ -94,7 +105,7 @@ functor Make(M : sig
val raw : $(map rawMeta (key ++ row))
- con cols :: {(Type * Type)}
+ con cols :: {(Type * Type * Type)}
val cols : $(map (colMeta (key ++ row)) cols)
val keyFolder : folder key