Mercurial > urweb
changeset 1304:f0afe61a6f8b
Tweaking unification fix to apply to demo/more
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 10 Oct 2010 15:37:14 -0400 |
| parents | c7b9a33c26c8 |
| children | a6fc03d28170 |
| files | demo/more/dbgrid.ur demo/more/dlist.ur demo/more/grid.ur demo/more/grid0.ur demo/more/orm.ur lib/ur/string.ur src/elaborate.sml |
| diffstat | 7 files changed, 86 insertions(+), 48 deletions(-) [+] |
line wrap: on
line diff
--- a/demo/more/dbgrid.ur Sun Oct 10 14:41:03 2010 -0400 +++ b/demo/more/dbgrid.ur Sun Oct 10 15:37:14 2010 -0400 @@ -38,7 +38,7 @@ 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 @@ 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)
--- a/demo/more/dlist.ur Sun Oct 10 14:41:03 2010 -0400 +++ b/demo/more/dlist.ur Sun Oct 10 15:37:14 2010 -0400 @@ -119,7 +119,8 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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
--- a/demo/more/grid.ur Sun Oct 10 14:41:03 2010 -0400 +++ b/demo/more/grid.ur Sun Oct 10 15:37:14 2010 -0400 @@ -49,16 +49,18 @@ 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 @@ 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;
--- a/demo/more/grid0.ur Sun Oct 10 14:41:03 2010 -0400 +++ b/demo/more/grid0.ur Sun Oct 10 15:37:14 2010 -0400 @@ -13,8 +13,8 @@ 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 = {}
--- a/demo/more/orm.ur Sun Oct 10 14:41:03 2010 -0400 +++ b/demo/more/orm.ur Sun Oct 10 15:37:14 2010 -0400 @@ -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 @@ 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]});
--- a/lib/ur/string.ur Sun Oct 10 14:41:03 2010 -0400 +++ b/lib/ur/string.ur Sun Oct 10 15:37:14 2010 -0400 @@ -57,7 +57,7 @@ mp' (length s - 1) "" end -fun newlines [ctx] [[Body] ~ ctx] s : xml ([Body] ++ ctx) [] [] = +fun newlines [ctx] [[Body] ~ ctx] (s : string) : xml ([Body] ++ ctx) [] [] = case split s #"\n" of None => cdata s | Some (s1, s2) => <xml>{[s1]}<br/>{newlines s2}</xml>
--- a/src/elaborate.sml Sun Oct 10 14:41:03 2010 -0400 +++ b/src/elaborate.sml Sun Oct 10 15:37:14 2010 -0400 @@ -655,6 +655,24 @@ val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list) + exception CantSquish + + fun squish by = + U.Con.mapB {kind = fn _ => fn k => k, + con = fn bound => fn c => + case c of + L'.CRel xn => + if xn < bound then + c + else if bound <= xn andalso xn < bound + by then + raise CantSquish + else + L'.CRel (xn - by) + | L'.CUnif _ => raise CantSquish + | _ => c, + bind = fn (bound, U.Con.RelC _) => bound + 1 + | (bound, _) => bound} 0 + fun unifyRecordCons env (loc, c1, c2) = let fun rkindof c = @@ -1056,6 +1074,19 @@ else r := SOME c1All + | (L'.CUnif (nl, _, _, _, r), _) => + if occursCon r c2All then + err COccursCheckFailed + else + (r := SOME (squish nl c2All) + handle CantSquish => err CIncompatible) + | (_, L'.CUnif (nl, _, _, _, r)) => + if occursCon r c1All then + err COccursCheckFailed + else + (r := SOME (squish nl c1All) + handle CantSquish => err CIncompatible) + | (L'.CUnit, L'.CUnit) => () | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => @@ -1290,7 +1321,8 @@ val k = (L'.KType, loc) val unifs = map (fn _ => cunif (loc, k)) xs val nxs = length unifs - 1 - val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, u) t) t unifs + val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, + E.mliftConInCon (nxs - i) u) t) t unifs val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs in ignore (checkPatCon env p' pt t);