From 3944b599134b89f12f24ae3f52d21f954463c765 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 10 Oct 2010 15:37:14 -0400 Subject: Tweaking unification fix to apply to demo/more --- demo/more/dbgrid.ur | 35 ++++++++++++++++++----------------- demo/more/dlist.ur | 17 +++++++++-------- demo/more/grid.ur | 29 ++++++++++++++++------------- demo/more/grid0.ur | 4 ++-- demo/more/orm.ur | 13 +++++++------ 5 files changed, 52 insertions(+), 46 deletions(-) (limited to 'demo') 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}/> -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}/> 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} - @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) + + @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]}); -- cgit v1.2.3