summaryrefslogtreecommitdiff
path: root/demo
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
parent8e944e62818045b820f45776a396bc1b66ab3056 (diff)
Filters implementation type-checking
Diffstat (limited to 'demo')
-rw-r--r--demo/more/dbgrid.ur210
-rw-r--r--demo/more/dbgrid.urs91
-rw-r--r--demo/more/dlist.ur37
-rw-r--r--demo/more/dlist.urs2
-rw-r--r--demo/more/grid.ur95
-rw-r--r--demo/more/grid.urp1
-rw-r--r--demo/more/grid.urs23
7 files changed, 303 insertions, 156 deletions
diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur
index 04eb6dc5..59214348 100644
--- a/demo/more/dbgrid.ur
+++ b/demo/more/dbgrid.ur
@@ -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,22 +23,26 @@ con aggregateMeta = fn (row :: {Type}) (acc :: Type) =>
Display : acc -> xbody}
structure Direct = struct
- 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 (ts :: (Type * Type * Type)) = (ts.1, ts.3)
+ 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 (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
(editableState ts) =
let
@@ -48,7 +55,10 @@ structure Direct = struct
| Some v => r -- nm ++ {nm = v}),
Display = mr.Display,
Edit = mr.Edit,
- Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo)}
+ Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo),
+ CreateFilter = mr.CreateFilter,
+ DisplayFilter = mr.DisplayFilter,
+ Filter = fn i r => mr.Filter i r.nm}
in
{Initialize = m.Initialize,
Handlers = fn data => case m.Handlers data of
@@ -56,7 +66,7 @@ structure Direct = struct
| Nullable mr => doMr mr}
end
- con readOnlyState (ts :: (Type * Type * Type)) = (ts.1, ts.3)
+ con readOnlyState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
fun readOnly [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
(readOnlyState ts) =
let
@@ -65,7 +75,10 @@ structure Direct = struct
Update = fn r _ => return r,
Display = mr.Display,
Edit = mr.Display,
- Validate = fn _ => return True}
+ Validate = fn _ => return True,
+ CreateFilter = mr.CreateFilter,
+ DisplayFilter = mr.DisplayFilter,
+ Filter = fn i r => mr.Filter i r.nm}
in
{Initialize = m.Initialize,
Handlers = fn data => case m.Handlers data of
@@ -73,22 +86,30 @@ structure Direct = struct
| Nullable mr => doMr mr}
end
- con metaBasic = fn actual_input :: (Type * Type) =>
- {Display : actual_input.2 -> xbody,
- Edit : source actual_input.2 -> xbody,
- Initialize : actual_input.1 -> actual_input.2,
- InitializeNull : actual_input.2,
- IsNull : actual_input.2 -> bool,
- Parse : actual_input.2 -> option actual_input.1}
+ con metaBasic = fn actual_input_filter :: (Type * Type * Type) =>
+ {Display : actual_input_filter.2 -> xbody,
+ Edit : source actual_input_filter.2 -> xbody,
+ Initialize : actual_input_filter.1 -> actual_input_filter.2,
+ InitializeNull : actual_input_filter.2,
+ IsNull : actual_input_filter.2 -> bool,
+ Parse : actual_input_filter.2 -> option actual_input_filter.1,
+ CreateFilter : actual_input_filter.3,
+ DisplayFilter : source actual_input_filter.3 -> xbody,
+ Filter : actual_input_filter.3 -> actual_input_filter.1 -> bool,
+ FilterIsNull : actual_input_filter.3 -> bool}
con basicState = source
- fun basic [ts ::: (Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2) =
+ con basicFilter = source
+ fun basic [ts ::: (Type * Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2, basicFilter ts.3) =
{Initialize = return (),
Handlers = fn () => NonNull (
{Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
Edit = m.Edit,
Initialize = fn v => source (m.Initialize v),
- Parse = fn s => v <- signal s; return (m.Parse v)},
+ Parse = fn s => v <- signal s; return (m.Parse v),
+ CreateFilter = source m.CreateFilter,
+ DisplayFilter = m.DisplayFilter,
+ Filter = fn f v => f <- signal f; return (m.Filter f v)},
{Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
Edit = m.Edit,
Initialize = fn v => source (case v of
@@ -100,9 +121,18 @@ structure Direct = struct
else
case m.Parse v of
None => None
- | Some v' => Some (Some v'))})}
-
- fun nullable [global] [actual] [input] (m : meta (global, actual, input)) =
+ | Some v' => Some (Some v')),
+ CreateFilter = source m.CreateFilter,
+ DisplayFilter = m.DisplayFilter,
+ Filter = fn f v => f <- signal f;
+ return (if m.FilterIsNull f then
+ Option.isNone v
+ else
+ case v of
+ None => False
+ | Some v => m.Filter f v) : signal bool})}
+
+ fun nullable [global] [actual] [input] [filter] (m : meta (global, actual, input, filter)) =
{Initialize = m.Initialize,
Handlers = fn d => case m.Handlers d of
Nullable _ => error <xml>Don't stack calls to Direct.nullable!</xml>
@@ -110,33 +140,62 @@ structure Direct = struct
type intGlobal = unit
type intInput = basicState string
- val int : meta (intGlobal, int, intInput) =
+ type intFilter = basicFilter string
+ val int : meta (intGlobal, int, intInput, intFilter) =
basic {Display = fn s => <xml>{[s]}</xml>,
Edit = fn s => <xml><ctextbox source={s}/></xml>,
Initialize = fn n => show n,
InitializeNull = "",
IsNull = eq "",
- Parse = fn v => read v}
+ Parse = fn v => read v,
+ CreateFilter = "",
+ DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody,
+ Filter = fn s n =>
+ case read s of
+ None => True
+ | Some n' => n' = n,
+ FilterIsNull = eq ""}
type stringGlobal = unit
type stringInput = basicState string
- val string : meta (stringGlobal, string, stringInput) =
+ type stringFilter = basicFilter string
+ val string : meta (stringGlobal, string, stringInput, stringFilter) =
basic {Display = fn s => <xml>{[s]}</xml>,
Edit = fn s => <xml><ctextbox source={s}/></xml>,
Initialize = fn s => s,
InitializeNull = "",
IsNull = eq "",
- Parse = fn s => Some s}
+ Parse = fn s => Some s,
+ CreateFilter = "",
+ DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody,
+ Filter = fn s n =>
+ case read s of
+ None => True
+ | Some n' => n' = n,
+ FilterIsNull = eq ""}
type boolGlobal = unit
type boolInput = basicState bool
- val bool : meta (boolGlobal, bool, boolInput) =
+ type boolFilter = basicFilter string
+ val bool : meta (boolGlobal, bool, boolInput, boolFilter) =
basic {Display = fn b => <xml>{[b]}</xml>,
Edit = fn s => <xml><ccheckbox source={s}/></xml>,
Initialize = fn b => b,
InitializeNull = False,
IsNull = fn _ => False,
- Parse = fn b => Some b}
+ Parse = fn b => Some b,
+ CreateFilter = "",
+ DisplayFilter = fn s => <xml><cselect source={s}>
+ <coption/>
+ <coption value="0">False</coption>
+ <coption value="1">True</coption>
+ </cselect></xml> : xbody,
+ Filter = fn s b =>
+ case s of
+ "0" => b = False
+ | "1" => b = True
+ | _ => True,
+ FilterIsNull = eq ""}
functor Foreign (M : sig
con row :: {Type}
@@ -152,8 +211,9 @@ structure Direct = struct
end) = struct
open M
- con global = list (t * string)
- con input = source string * option (t * $row)
+ type global = list (t * string)
+ type input = source string * option (t * $row)
+ type filter = source string
val getChoices = List.mapQuery (SELECT * FROM tab AS T)
(fn r => (r.T.nm, render r.T))
@@ -162,7 +222,7 @@ structure Direct = struct
r <- oneRow (SELECT T.{{row}} FROM tab AS T WHERE T.{nm} = {[k]});
return r.T
- val meta : meta (global, M.t, input) =
+ val meta : meta (global, M.t, input, filter) =
{Initialize = getChoices,
Handlers = fn choices =>
NonNull (
@@ -182,7 +242,19 @@ structure Direct = struct
Initialize = fn k => s <- source (show k);
r <- rpc (getChoice k);
return (s, Some (k, r)),
- Parse = fn (s, _) => k <- signal s; return (read k : option t)},
+ Parse = fn (s, _) => k <- signal s; return (read k : option t),
+ CreateFilter = source "",
+ DisplayFilter = fn s =>
+ <xml><cselect source={s}>
+ <coption/>
+ {List.mapX (fn (k, rend) =>
+ <xml><coption value={show k}>{[rend]}</coption></xml>)
+ choices}
+ </cselect></xml> : xbody,
+ Filter = fn s k => s <- signal s;
+ return (case read s : option t of
+ None => True
+ | Some k' => k' = k)},
{Display = fn (_, kr) => case kr of
None => <xml>NULL</xml>
| Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>,
@@ -212,11 +284,31 @@ structure Direct = struct
"" => Some None
| _ => case read ks : option t of
None => None
- | Some k => Some (Some k))})}
+ | Some k => Some (Some k)),
+ CreateFilter = source "",
+ DisplayFilter = fn s =>
+ <xml><cselect source={s}>
+ <coption/>
+ <coption value="0">NULL</coption>
+ {List.mapX (fn (k, rend) =>
+ <xml><coption value={"1" ^ show k}>{[rend]}</coption>
+ </xml>)
+ choices}
+ </cselect></xml> : xbody,
+ Filter = fn s ko => s <- signal s;
+ return (case s of
+ "" => True
+ | "0" => ko = None
+ | _ =>
+ case read (String.substring s {Start = 1,
+ Len = String.length s - 1})
+ : option t of
+ None => True
+ | Some k => ko = Some k)})}
end
end
-con computedState = (unit, xbody)
+con computedState = (unit, xbody, unit)
fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState =
{Initialize = return (),
Handlers = fn () => {Header = name,
@@ -224,7 +316,10 @@ fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedS
Update = fn r _ => return r,
Display = fn x => x,
Edit = fn _ => <xml>...</xml>,
- Validate = fn _ => return True}}
+ Validate = fn _ => return True,
+ CreateFilter = return (),
+ DisplayFilter = fn _ => <xml/>,
+ Filter = fn _ _ => return True}}
fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState =
{Initialize = return (),
Handlers = fn () => {Header = name,
@@ -232,7 +327,10 @@ fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState =
Update = fn r _ => return r,
Display = fn x => x,
Edit = fn _ => <xml>...</xml>,
- Validate = fn _ => return True}}
+ Validate = fn _ => return True,
+ CreateFilter = return (),
+ DisplayFilter = fn _ => <xml/>,
+ Filter = fn _ _ => return True}}
functor Make(M : sig
con key :: {Type}
@@ -242,7 +340,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
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
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index 850836b0..d4a255ee 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -6,18 +6,19 @@ datatype dlist' t =
Empty
| Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) }
-con dlist t = source (dlist' t)
+con dlist t = {Filter: t -> signal bool,
+ Elements : source (dlist' t)}
type position = transaction unit
fun headPos [t] (dl : dlist t) =
- dl' <- get dl;
+ dl' <- get dl.Elements;
case dl' of
Nonempty { Head = Cons (_, tl), Tail = tl' } =>
cur <- get tl;
- set dl (case cur of
- Nil => Empty
- | _ => Nonempty {Head = cur, Tail = tl'})
+ set dl.Elements (case cur of
+ Nil => Empty
+ | _ => Nonempty {Head = cur, Tail = tl'})
| _ => return ()
fun tailPos [t] (cur : source (dlist'' t)) new tail =
@@ -28,17 +29,20 @@ fun tailPos [t] (cur : source (dlist'' t)) new tail =
Nil => set tail cur
| _ => return ()
-val create = fn [t] => source Empty
+fun create [t] r =
+ s <- source Empty;
+ return {Filter = r.Filter,
+ Elements = s}
-fun clear [t] (s : dlist t) = set s Empty
+fun clear [t] (s : dlist t) = set s.Elements Empty
fun append [t] dl v =
- dl' <- get dl;
+ dl' <- get dl.Elements;
case dl' of
Empty =>
tl <- source Nil;
tl' <- source tl;
- set dl (Nonempty {Head = Cons (v, tl), Tail = tl'});
+ set dl.Elements (Nonempty {Head = Cons (v, tl), Tail = tl'});
return (headPos dl)
| Nonempty {Tail = tl, ...} =>
@@ -49,7 +53,7 @@ fun append [t] dl v =
return (tailPos cur new tl)
fun render [ctx] [ctx ~ body] [t] f dl = <xml>
- <dyn signal={dl' <- signal dl;
+ <dyn signal={dl' <- signal dl.Elements;
return (case dl' of
Empty => <xml/>
| Nonempty {Head = hd, Tail = tlTop} =>
@@ -63,8 +67,13 @@ fun render [ctx] [ctx ~ body] [t] f dl = <xml>
None => headPos dl
| Some prev => tailPos prev tl tlTop
in
- <xml>{f v pos}<dyn signal={tl' <- signal tl;
- return (render' (Some tl) tl')}/></xml>
+ <xml><dyn signal={b <- dl.Filter v;
+ return (if b then
+ f v pos
+ else
+ <xml/>)}/>
+ <dyn signal={tl' <- signal tl;
+ return (render' (Some tl) tl')}/></xml>
end
in
render' None hd
@@ -82,7 +91,7 @@ fun elements' [t] (dl'' : dlist'' t) =
return (x :: tl)
fun elements [t] (dl : dlist t) =
- dl' <- signal dl;
+ dl' <- signal dl.Elements;
case dl' of
Empty => return []
| Nonempty {Head = hd, ...} => elements' hd
@@ -98,7 +107,7 @@ fun foldl [t] [acc] (f : t -> acc -> signal acc) =
foldl'' i' dl'
fun foldl' (i : acc) (dl : dlist t) : signal acc =
- dl <- signal dl;
+ dl <- signal dl.Elements;
case dl of
Empty => return i
| Nonempty {Head = dl, ...} => foldl'' i dl
diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs
index fcfe15ee..a55a1774 100644
--- a/demo/more/dlist.urs
+++ b/demo/more/dlist.urs
@@ -1,7 +1,7 @@
con dlist :: Type -> Type
type position
-val create : t ::: Type -> transaction (dlist t)
+val create : t ::: Type -> {Filter : t -> signal bool} -> transaction (dlist t)
val clear : t ::: Type -> dlist t -> transaction unit
val append : t ::: Type -> dlist t -> t -> transaction position
val delete : position -> transaction unit
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
index 74ce6b38..424c3b6f 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -1,14 +1,17 @@
-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,
@@ -25,7 +28,7 @@ functor Make(M : sig
val save : key -> row -> transaction unit
val delete : key -> transaction unit
- con cols :: {(Type * Type)}
+ con cols :: {(Type * Type * Type)}
val cols : $(map (colMeta row) cols)
val folder : folder cols
@@ -40,20 +43,21 @@ functor Make(M : sig
style td
style agg
- fun make (row : M.row) [t] (m : colMeta' M.row t) : transaction t = m.Project row
+ fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row
- fun makeAll cols row = @@Monad.exec [transaction] _ [map snd M.cols]
- (map2 [fst] [colMeta M.row] [fn p :: (Type * Type) => transaction p.2]
- (fn [p] data meta => make row [_] (meta.Handlers data))
+ fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols]
+ (map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
+ (fn [p] data meta => make row [_] [_] (meta.Handlers data))
[_] M.folder cols M.cols)
(@@Folder.mp [_] [_] M.folder)
- type grid = {Cols : $(map fst M.cols),
+ type grid = {Cols : $(map fst3 M.cols),
Rows : Dlist.dlist {Row : source M.row,
- Cols : source ($(map snd M.cols)),
+ Cols : source ($(map snd3 M.cols)),
Updating : source bool,
Selected : source bool},
- Selection : source bool}
+ Selection : source bool,
+ Filters : $(map thd3 M.cols)}
fun addRow cols rows row =
rowS <- source row;
@@ -66,15 +70,29 @@ functor Make(M : sig
Updating = ud,
Selected = sd})
- val createMetas = Monad.mapR [colMeta M.row] [fst]
- (fn [nm :: Name] [p :: (Type * Type)] meta => meta.Initialize)
- [_] M.folder M.cols
-
val grid =
- cols <- createMetas;
- rows <- Dlist.create;
+ cols <- Monad.mapR [colMeta M.row] [fst3]
+ (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize)
+ [_] M.folder M.cols;
+
+ filters <- Monad.mapR2 [colMeta M.row] [fst3] [thd3]
+ (fn [nm :: Name] [p :: (Type * Type * Type)] meta state =>
+ (meta.Handlers state).CreateFilter)
+ [_] M.folder M.cols cols;
+
+ rows <- Dlist.create {Filter = fn all =>
+ row <- signal all.Row;
+ foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]
+ (fn [nm :: Name] [p :: (Type * Type * Type)]
+ [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
+ meta state filter combinedFilter row =>
+ previous <- combinedFilter row;
+ this <- (meta.Handlers state).Filter filter row;
+ return (previous && this))
+ (fn _ => return True)
+ [_] M.folder M.cols cols filters row};
sel <- source False;
- return {Cols = cols, Rows = rows, Selection = sel}
+ return {Cols = cols, Rows = rows, Selection = sel, Filters = filters}
fun sync {Cols = cols, Rows = rows, ...} =
Dlist.clear rows;
@@ -85,8 +103,8 @@ functor Make(M : sig
<table class={tabl}>
<tr class={tr}>
<th/> <th/> <th/>
- {foldRX2 [fst] [colMeta M.row] [_]
- (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest]
+ {foldRX2 [fst3] [colMeta M.row] [_]
+ (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
data (meta : colMeta M.row p) =>
<xml><th class={th}>{[(meta.Handlers data).Header]}</th></xml>)
[_] M.folder grid.Cols M.cols}
@@ -109,8 +127,8 @@ functor Make(M : sig
val save =
cols <- get colsS;
- errors <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => option string]
- (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
+ errors <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => option string]
+ (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}]
[[nm] ~ rest] data meta v errors =>
b <- current ((meta.Handlers data).Validate v);
return (if b then
@@ -128,9 +146,9 @@ functor Make(M : sig
| None =>
set ud False;
row <- get rowS;
- row' <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => M.row]
- (fn [nm :: Name] [t :: (Type * Type)]
- [rest :: {(Type * Type)}]
+ row' <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => M.row]
+ (fn [nm :: Name] [t :: (Type * Type * Type)]
+ [rest :: {(Type * Type * Type)}]
[[nm] ~ rest] data meta v row' =>
(meta.Handlers data).Update row' v)
row [_] M.folder grid.Cols M.cols cols;
@@ -165,9 +183,9 @@ functor Make(M : sig
</td>
<dyn signal={cols <- signal colsS;
- return (foldRX3 [fst] [colMeta M.row] [snd] [_]
- (fn [nm :: Name] [t :: (Type * Type)]
- [rest :: {(Type * Type)}]
+ return (foldRX3 [fst3] [colMeta M.row] [snd3] [_]
+ (fn [nm :: Name] [t :: (Type * Type * Type)]
+ [rest :: {(Type * Type * Type)}]
[[nm] ~ rest] data meta v =>
<xml><td class={td}>
<dyn signal={b <- signal ud;
@@ -206,6 +224,13 @@ functor Make(M : sig
<xml><td class={agg}>{meta.Display acc}</td></xml>)
[_] M.aggFolder M.aggregates rows}
</tr></xml>}/>
+
+ <tr><th colspan={3}>Filters</th>
+ {foldRX3 [colMeta M.row] [fst3] [thd3] [_]
+ (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
+ meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>)
+ [_] M.folder M.cols grid.Cols grid.Filters}
+ </tr>
</table>
<button value="New row" onclick={row <- rpc M.new;
diff --git a/demo/more/grid.urp b/demo/more/grid.urp
index 0736e4fe..a67abdb2 100644
--- a/demo/more/grid.urp
+++ b/demo/more/grid.urp
@@ -2,6 +2,7 @@
$/option
$/monad
$/list
+$/string
dlist
grid
dbgrid
diff --git a/demo/more/grid.urs b/demo/more/grid.urs
index e3d8f828..2ab9fbcc 100644
--- a/demo/more/grid.urs
+++ b/demo/more/grid.urs
@@ -1,14 +1,17 @@
-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}
+ 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_t :: (Type * Type)) =>
- {Initialize : transaction global_t.1,
- Handlers : global_t.1 -> colMeta' row global_t.2}
+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,
@@ -25,7 +28,7 @@ functor Make(M : sig
val save : key -> row -> transaction unit
val delete : key -> transaction unit
- con cols :: {(Type * Type)}
+ con cols :: {(Type * Type * Type)}
val cols : $(map (colMeta row) cols)
val folder : folder cols