comparison demo/more/orm.ur @ 989:0bdc4d538f1c

Orm searching
author Adam Chlipala <adamc@hcoop.net>
date Mon, 05 Oct 2009 17:24:21 -0400
parents d923b47e483d
children 46803e668a89
comparison
equal deleted inserted replaced
988:d923b47e483d 989:0bdc4d538f1c
14 type id = int 14 type id = int
15 val inj = _ 15 val inj = _
16 val id : meta id = {Link = (), 16 val id : meta id = {Link = (),
17 Inj = inj} 17 Inj = inj}
18 18
19 con fs = [Id = id] ++ M.cols
20
19 sequence s 21 sequence s
20 table t : ([Id = id] ++ M.cols) 22 table t : fs
21 23
22 type row = $([Id = id] ++ M.cols) 24 type row = $fs
23 25
24 fun ensql [avail] (r : $M.cols) : $(map (sql_exp avail [] []) M.cols) = 26 fun ensql [avail] (r : $M.cols) : $(map (sql_exp avail [] []) M.cols) =
25 map2 [meta] [Top.id] [sql_exp avail [] []] 27 map2 [meta] [Top.id] [sql_exp avail [] []]
26 (fn [t] meta v => @sql_inject meta.Inj v) 28 (fn [t] meta v => @sql_inject meta.Inj v)
27 [_] M.folder M.cols r 29 [_] M.folder M.cols r
37 39
38 fun lookup id = 40 fun lookup id =
39 ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]}); 41 ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]});
40 return (Option.mp (fn r => r.T) ro) 42 return (Option.mp (fn r => r.T) ro)
41 43
42 val list = query (SELECT * FROM t) (fn r ls => return (r.T :: ls)) [] 44 fun resultsOut q = query q (fn r ls => return (r.T :: ls)) []
45
46 val list = resultsOut (SELECT * FROM t)
47
48 con col = fn t => {Exp : sql_exp [T = fs] [] [] t,
49 Inj : sql_injectable t}
50 val idCol = {Exp = sql_field [#T] [#Id], Inj = _}
51 val cols = foldR [meta] [fn before => after :: {Type} -> [before ~ after] =>
52 $(map (fn t => {Exp : sql_exp [T = before ++ after] [] [] t,
53 Inj : sql_injectable t}) before)]
54 (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before] (meta : meta t)
55 (acc : after :: {Type} -> [before ~ after] =>
56 $(map (fn t => {Exp : sql_exp [T = before ++ after] [] [] t,
57 Inj : sql_injectable t}) before))
58 [after :: {Type}] [[nm = t] ++ before ~ after] =>
59 {nm = {Exp = sql_field [#T] [nm],
60 Inj = meta.Inj}} ++ acc [[nm = t] ++ after] !)
61 (fn [after :: {Type}] [[] ~ after] => {})
62 [_] M.folder M.cols
63 [[Id = id]] !
64
65 type filter = sql_exp [T = fs] [] [] bool
66 fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f})
67
68 fun bin (b : t ::: Type -> sql_binary t t bool) [t] (c : col t) (v : t) =
69 sql_binary b c.Exp (@sql_inject c.Inj v)
70 val eq = bin @@sql_eq
71 val ne = bin @@sql_ne
72 val lt = bin @@sql_lt
73 val le = bin @@sql_le
74 val gt = bin @@sql_gt
75 val ge = bin @@sql_ge
76
77 fun bb (b : sql_binary bool bool bool) (f1 : filter) (f2 : filter) =
78 sql_binary b f1 f2
79 val _and = bb sql_and
80 val or = bb sql_or
43 end 81 end