Mercurial > urweb
comparison demo/more/orm.ur @ 1093:8d3aa6c7cee0
Make summary unification more conservative; infer implicit arguments after applications
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 26 Dec 2009 11:56:40 -0500 |
parents | bb3fc575cfe7 |
children | f0afe61a6f8b |
comparison
equal
deleted
inserted
replaced
1092:6f4b05fc4361 | 1093:8d3aa6c7cee0 |
---|---|
30 val inj = _ | 30 val inj = _ |
31 val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}), | 31 val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}), |
32 Inj = inj} | 32 Inj = inj} |
33 | 33 |
34 fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') = | 34 fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') = |
35 map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1] | 35 @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1] |
36 (fn [ts] meta v => @sql_inject meta.Inj v) | 36 (fn [ts] meta v => @sql_inject meta.Inj v) |
37 [_] M.folder M.cols r | 37 M.folder M.cols r |
38 | 38 |
39 fun create (r : row') = | 39 fun create (r : row') = |
40 id <- nextval s; | 40 id <- nextval s; |
41 dml (insert t ({Id = sql_inject id} ++ ensql r)); | 41 dml (insert t ({Id = sql_inject id} ++ ensql r)); |
42 return ({Id = id} ++ r) | 42 return ({Id = id} ++ r) |
43 | 43 |
44 fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]}) | 44 fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]}) |
45 | 45 |
46 fun save r = dml (update [fs'] ! (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]})) | 46 fun save r = dml (update [fs'] (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]})) |
47 | 47 |
48 fun lookup id = | 48 fun lookup id = |
49 ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]}); | 49 ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]}); |
50 return (Option.mp (fn r => r.T) ro) | 50 return (Option.mp (fn r => r.T) ro) |
51 | 51 |
57 val idCol = {Exp = sql_field [#T] [#Id], Inj = _} | 57 val idCol = {Exp = sql_field [#T] [#Id], Inj = _} |
58 con meta' = fn (fs :: {Type}) (col :: Type, parent :: Type) => | 58 con meta' = fn (fs :: {Type}) (col :: Type, parent :: Type) => |
59 {Col : {Exp : sql_exp [T = fs] [] [] col, | 59 {Col : {Exp : sql_exp [T = fs] [] [] col, |
60 Inj : sql_injectable col}, | 60 Inj : sql_injectable col}, |
61 Parent : $fs -> transaction (option parent)} | 61 Parent : $fs -> transaction (option parent)} |
62 val cols = foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] => | 62 val cols = @foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] => |
63 $(map (meta' (map fst (before ++ after))) before)] | 63 $(map (meta' (map fst (before ++ after))) before)] |
64 (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}] | 64 (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}] |
65 [[nm] ~ before] (meta : meta ts) | 65 [[nm] ~ before] (meta : meta ts) |
66 (acc : after :: {(Type * Type)} -> [before ~ after] => | 66 (acc : after :: {(Type * Type)} -> [before ~ after] => |
67 $(map (meta' (map fst (before ++ after))) before)) | 67 $(map (meta' (map fst (before ++ after))) before)) |
68 [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] => | 68 [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] => |
69 {nm = {Col = {Exp = sql_field [#T] [nm], | 69 {nm = {Col = {Exp = sql_field [#T] [nm], |
70 Inj = meta.Inj}, | 70 Inj = meta.Inj}, |
71 Parent = fn r => meta.Link r.nm}} | 71 Parent = fn r => meta.Link r.nm}} |
72 ++ acc [[nm = ts] ++ after] !) | 72 ++ acc [[nm = ts] ++ after] !) |
73 (fn [after :: {(Type * Type)}] [[] ~ after] => {}) | 73 (fn [after :: {(Type * Type)}] [[] ~ after] => {}) |
74 [_] M.folder M.cols | 74 M.folder M.cols |
75 [[Id = (id, row)]] ! | 75 [[Id = (id, row)]] ! |
76 | 76 |
77 type filter = sql_exp [T = fs] [] [] bool | 77 type filter = sql_exp [T = fs] [] [] bool |
78 fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f}) | 78 fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f}) |
79 fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f}) | 79 fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f}) |
80 | 80 |
81 fun bin (b : t ::: Type -> sql_binary t t bool) [t] (c : col t) (v : t) = | 81 fun bin (b : t ::: Type -> sql_binary t t bool) [t] (c : col t) (v : t) = |
82 sql_binary b c.Exp (@sql_inject c.Inj v) | 82 sql_binary b c.Exp (@sql_inject c.Inj v) |
83 val eq = bin @@sql_eq | 83 val eq = @@bin @@sql_eq |
84 val ne = bin @@sql_ne | 84 val ne = @@bin @@sql_ne |
85 val lt = bin @@sql_lt | 85 val lt = @@bin @@sql_lt |
86 val le = bin @@sql_le | 86 val le = @@bin @@sql_le |
87 val gt = bin @@sql_gt | 87 val gt = @@bin @@sql_gt |
88 val ge = bin @@sql_ge | 88 val ge = @@bin @@sql_ge |
89 | 89 |
90 fun bb (b : sql_binary bool bool bool) (f1 : filter) (f2 : filter) = | 90 fun bb (b : sql_binary bool bool bool) (f1 : filter) (f2 : filter) = |
91 sql_binary b f1 f2 | 91 sql_binary b f1 f2 |
92 val _and = bb sql_and | 92 val _and = bb sql_and |
93 val or = bb sql_or | 93 val or = bb sql_or |