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