comparison demo/more/orm.ur @ 990:46803e668a89

Fix a de Bruijn index bug in map fusion
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Oct 2009 10:15:26 -0400
parents 0bdc4d538f1c
children b132f8620a66
comparison
equal deleted inserted replaced
989:0bdc4d538f1c 990:46803e668a89
1 con link = fn t :: Type => unit 1 con link = fn col_parent :: (Type * Type) => col_parent.1 -> transaction (option col_parent.2)
2 fun noParent [t ::: Type] _ = return None
2 3
3 con meta = fn col :: Type => { 4 con meta = fn col_parent :: (Type * Type) => {
4 Link : link col, 5 Link : link col_parent,
5 Inj : sql_injectable col 6 Inj : sql_injectable col_parent.1
6 } 7 }
7 8
8 functor Table(M : sig 9 functor Table(M : sig
9 con cols :: {Type} 10 con cols :: {(Type * Type)}
10 val cols : $(map meta cols) 11 val cols : $(map meta cols)
11 constraint [Id] ~ cols 12 constraint [Id] ~ cols
12 val folder : folder cols 13 val folder : folder cols
13 end) = struct 14 end) = struct
14 type id = int 15 type id = int
15 val inj = _ 16 con fs' = map fst M.cols
16 val id : meta id = {Link = (), 17 con fs = [Id = id] ++ fs'
17 Inj = inj} 18 type row' = $fs'
19 type row = $fs
18 20
19 con fs = [Id = id] ++ M.cols 21 fun resultsOut q = query q (fn r ls => return (r.T :: ls)) []
22 fun resultOut q = ro <- oneOrNoRows q; return (Option.mp (fn r => r .T) ro)
20 23
21 sequence s 24 sequence s
22 table t : fs 25 table t : fs
23 26
24 type row = $fs 27 val inj = _
28 val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}),
29 Inj = inj}
25 30
26 fun ensql [avail] (r : $M.cols) : $(map (sql_exp avail [] []) M.cols) = 31 fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') =
27 map2 [meta] [Top.id] [sql_exp avail [] []] 32 map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1]
28 (fn [t] meta v => @sql_inject meta.Inj v) 33 (fn [ts] meta v => @sql_inject meta.Inj v)
29 [_] M.folder M.cols r 34 [_] M.folder M.cols r
30 35
31 fun create (r : $M.cols) = 36 fun create (r : row') =
32 id <- nextval s; 37 id <- nextval s;
33 dml (insert t ({Id = sql_inject id} ++ ensql r)); 38 dml (insert t ({Id = sql_inject id} ++ ensql r));
34 return ({Id = id} ++ r) 39 return ({Id = id} ++ r)
35 40
36 fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]}) 41 fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]})
37 42
38 fun save r = dml (update [M.cols] ! (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]})) 43 fun save r = dml (update [fs'] ! (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]}))
39 44
40 fun lookup id = 45 fun lookup id =
41 ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]}); 46 ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]});
42 return (Option.mp (fn r => r.T) ro) 47 return (Option.mp (fn r => r.T) ro)
43 48
44 fun resultsOut q = query q (fn r ls => return (r.T :: ls)) []
45 49
46 val list = resultsOut (SELECT * FROM t) 50 val list = resultsOut (SELECT * FROM t)
47 51
48 con col = fn t => {Exp : sql_exp [T = fs] [] [] t, 52 con col = fn t => {Exp : sql_exp [T = fs] [] [] t,
49 Inj : sql_injectable t} 53 Inj : sql_injectable t}
50 val idCol = {Exp = sql_field [#T] [#Id], Inj = _} 54 val idCol = {Exp = sql_field [#T] [#Id], Inj = _}
51 val cols = foldR [meta] [fn before => after :: {Type} -> [before ~ after] => 55 con meta' = fn (fs :: {Type}) (col_parent :: (Type * Type)) =>
52 $(map (fn t => {Exp : sql_exp [T = before ++ after] [] [] t, 56 {Col : {Exp : sql_exp [T = fs] [] [] col_parent.1,
53 Inj : sql_injectable t}) before)] 57 Inj : sql_injectable col_parent.1},
54 (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before] (meta : meta t) 58 Parent : $fs -> transaction (option col_parent.2)}
55 (acc : after :: {Type} -> [before ~ after] => 59 val cols = foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] =>
56 $(map (fn t => {Exp : sql_exp [T = before ++ after] [] [] t, 60 $(map (meta' (map fst (before ++ after))) before)]
57 Inj : sql_injectable t}) before)) 61 (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}]
58 [after :: {Type}] [[nm = t] ++ before ~ after] => 62 [[nm] ~ before] (meta : meta ts)
59 {nm = {Exp = sql_field [#T] [nm], 63 (acc : after :: {(Type * Type)} -> [before ~ after] =>
60 Inj = meta.Inj}} ++ acc [[nm = t] ++ after] !) 64 $(map (meta' (map fst (before ++ after))) before))
61 (fn [after :: {Type}] [[] ~ after] => {}) 65 [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] =>
66 {nm = {Col = {Exp = sql_field [#T] [nm],
67 Inj = meta.Inj},
68 Parent = fn r => meta.Link r.nm}}
69 ++ acc [[nm = ts] ++ after] !)
70 (fn [after :: {(Type * Type)}] [[] ~ after] => {})
62 [_] M.folder M.cols 71 [_] M.folder M.cols
63 [[Id = id]] ! 72 [[Id = (id, row)]] !
64 73
65 type filter = sql_exp [T = fs] [] [] bool 74 type filter = sql_exp [T = fs] [] [] bool
75 fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f})
66 fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f}) 76 fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f})
67 77
68 fun bin (b : t ::: Type -> sql_binary t t bool) [t] (c : col t) (v : t) = 78 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) 79 sql_binary b c.Exp (@sql_inject c.Inj v)
70 val eq = bin @@sql_eq 80 val eq = bin @@sql_eq