summaryrefslogtreecommitdiff
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 15:37:14 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 15:37:14 -0400
commit3944b599134b89f12f24ae3f52d21f954463c765 (patch)
tree59ec01525ded42885a850c9e83ba458c79843ce5 /demo
parent948aa854af8ca5560a1eea5221c4a1f3a6901970 (diff)
Tweaking unification fix to apply to demo/more
Diffstat (limited to 'demo')
-rw-r--r--demo/more/dbgrid.ur35
-rw-r--r--demo/more/dlist.ur17
-rw-r--r--demo/more/grid.ur29
-rw-r--r--demo/more/grid0.ur4
-rw-r--r--demo/more/orm.ur13
5 files changed, 52 insertions, 46 deletions
diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur
index b6cd94ae..43ad7725 100644
--- a/demo/more/dbgrid.ur
+++ b/demo/more/dbgrid.ur
@@ -38,7 +38,7 @@ structure Direct = struct
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) =>
+ con meta = fn global_actual_input_filter =>
{Initialize : transaction global_actual_input_filter.1,
Handlers : global_actual_input_filter.1
-> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
@@ -48,25 +48,26 @@ structure Direct = struct
fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
(editableState ts) =
let
- fun doMr mr = {Header = name,
- Project = fn r => mr.Initialize r.nm,
- Update = fn r s =>
- vo <- current (mr.Parse s);
- return (case vo of
- None => r
- | Some v => r -- nm ++ {nm = v}),
- Display = mr.Display,
- Edit = mr.Edit,
- 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,
- Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)}
+ fun doMr (mr : metaBase (ts.2, ts.3, ts.4)) : colMeta' ([nm = ts.2] ++ rest) ts.3 ts.4 =
+ {Header = name,
+ Project = fn r => mr.Initialize r.nm,
+ Update = fn r s =>
+ vo <- current (mr.Parse s);
+ return (case vo of
+ None => r
+ | Some v => r -- nm ++ {nm = v}),
+ Display = mr.Display,
+ Edit = mr.Edit,
+ 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,
+ Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)}
in
{Initialize = m.Initialize,
Handlers = fn data => case m.Handlers data of
- NonNull (mr, _) => doMr mr
- | Nullable mr => doMr mr}
+ NonNull (mr, _) => doMr mr
+ | Nullable mr => doMr mr}
end
con readOnlyState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index 1e5b8020..884ab8a1 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -119,7 +119,8 @@ fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) []
end}/>
</xml>
-fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter =
+fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] [])
+ : option int -> list (t * position) -> xml (ctx ++ body) [] [] =
let
fun renderFlat' len ls =
case len of
@@ -233,13 +234,13 @@ fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
None => elems
| Some pos => skip pos elems
in
- return (renderFlat f r.Filter len elems)
+ return (renderFlat f len elems)
end}/>
</xml>
fun delete pos = pos
-fun elements' [t] (dl'' : dlist'' t) =
+fun elements' [t] (dl'' : dlist'' t) : signal (list t) =
case dl'' of
Nil => return []
| Cons (x, dl'') =>
@@ -247,13 +248,13 @@ fun elements' [t] (dl'' : dlist'' t) =
tl <- elements' dl'';
return (x :: tl)
-fun elements [t] (dl : dlist t) =
+fun elements [t] (dl : dlist t) : signal (list t) =
dl' <- signal dl;
case dl' of
Empty => return []
| Nonempty {Head = hd, ...} => elements' hd
-fun size' [t] (dl'' : dlist'' t) =
+fun size' [t] (dl'' : dlist'' t) : signal int =
case dl'' of
Nil => return 0
| Cons (x, dl'') =>
@@ -261,13 +262,13 @@ fun size' [t] (dl'' : dlist'' t) =
n <- size' dl'';
return (n + 1)
-fun size [t] (dl : dlist t) =
+fun size [t] (dl : dlist t) : signal int =
dl' <- signal dl;
case dl' of
Empty => return 0
| Nonempty {Head = hd, ...} => size' hd
-fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) =
+fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) : signal int =
case dl'' of
Nil => return 0
| Cons (x, dl'') =>
@@ -276,7 +277,7 @@ fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) =
n <- numPassing' f dl'';
return (if b then n + 1 else n)
-fun numPassing [t] (f : t -> signal bool) (dl : dlist t) =
+fun numPassing [t] (f : t -> signal bool) (dl : dlist t) : signal int =
dl' <- signal dl;
case dl' of
Empty => return 0
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
index d560c556..e0b4a351 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -49,16 +49,18 @@ functor Make(M : sig
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 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)
+ (@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 listT = {Row : source M.row,
+ Cols : source ($(map snd3 M.cols)),
+ Updating : source bool,
+ Selected : source bool}
type grid = {Cols : $(map fst3 M.cols),
- Rows : Dlist.dlist {Row : source M.row,
- Cols : source ($(map snd3 M.cols)),
- Updating : source bool,
- Selected : source bool},
+ Rows : Dlist.dlist listT,
Selection : source bool,
Filters : $(map thd3 M.cols),
Sort : source (option (M.row -> M.row -> bool)),
@@ -250,11 +252,12 @@ functor Make(M : sig
return (f r1 r2)) f)}
grid.Rows}
- <dyn signal={rows <- Dlist.foldl (fn row => @Monad.mapR2 _ [aggregateMeta M.row] [id] [id]
- (fn [nm :: Name] [t :: Type] meta acc =>
- Monad.mp (fn v => meta.Step v acc)
- (signal row.Row))
- M.aggFolder M.aggregates)
+ <dyn signal={rows <- Dlist.foldl (fn row : listT =>
+ @Monad.mapR2 _ [aggregateMeta M.row] [id] [id]
+ (fn [nm :: Name] [t :: Type] meta acc =>
+ Monad.mp (fn v => meta.Step v acc)
+ (signal row.Row))
+ M.aggFolder M.aggregates)
(@mp [aggregateMeta M.row] [id]
(fn [t] meta => meta.Initial)
M.aggFolder M.aggregates) grid.Rows;
diff --git a/demo/more/grid0.ur b/demo/more/grid0.ur
index 3e3d27ab..410554c9 100644
--- a/demo/more/grid0.ur
+++ b/demo/more/grid0.ur
@@ -13,8 +13,8 @@ open Make(struct
A = {New = return 0,
Inj = _}}
- val cols = {Id = Direct.readOnly [#Id] ! "Id" Direct.int,
- A = Direct.editable [#A] ! "A" Direct.int}
+ val cols = {Id = Direct.readOnly [#Id] "Id" Direct.int,
+ A = Direct.editable [#A] "A" Direct.int}
val aggregates = {}
diff --git a/demo/more/orm.ur b/demo/more/orm.ur
index d9f57f3b..068e3b5c 100644
--- a/demo/more/orm.ur
+++ b/demo/more/orm.ur
@@ -1,13 +1,14 @@
con link = fn col_parent :: (Type * Type) => col_parent.1 -> transaction (option col_parent.2)
-fun noParent [t ::: Type] (_ : t) = return None
+fun noParent [t ::: Type] (_ : t) : transaction (option unit) = return None
con meta = fn (col :: Type, parent :: Type) => {
Link : link (col, parent),
Inj : sql_injectable col
}
-fun local [t :: Type] (inj : sql_injectable t) = {Link = noParent,
- Inj = inj}
+fun local [t :: Type] (inj : sql_injectable t) : meta (t, unit) =
+ {Link = noParent,
+ Inj = inj}
functor Table(M : sig
con cols :: {(Type * Type)}
@@ -31,19 +32,19 @@ functor Table(M : sig
val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}),
Inj = inj}
- fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') =
+ fun ensql [avail ::_] (r : row') : $(map (sql_exp avail [] []) fs') =
@map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1]
(fn [ts] meta v => @sql_inject meta.Inj v)
M.folder M.cols r
fun create (r : row') =
id <- nextval s;
- dml (insert t ({Id = sql_inject id} ++ ensql r));
+ dml (insert t ({Id = sql_inject id} ++ ensql [[]] r));
return ({Id = id} ++ r)
fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]})
- fun save r = dml (update [fs'] (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]}))
+ fun save r = dml (update [fs'] (ensql [[T = [Id = int] ++ map fst M.cols]] (r -- #Id)) t (WHERE T.Id = {[r.Id]}))
fun lookup id =
ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]});