Mercurial > urweb

annotate demo/more/orm.ur @ 1218:48d2ca496d2c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Path conditions, used to track implicit flows
author Adam Chlipala <adamc@hcoop.net>
date Sat, 10 Apr 2010 13:02:15 -0400
parents 8d3aa6c7cee0
children f0afe61a6f8b
rev   line source
adamc@990 1 con link = fn col_parent :: (Type * Type) => col_parent.1 -> transaction (option col_parent.2)
adamc@991 2 fun noParent [t ::: Type] (_ : t) = return None
adamc@987 3
adamc@1002 4 con meta = fn (col :: Type, parent :: Type) => {
adamc@1002 5 Link : link (col, parent),
adamc@1002 6 Inj : sql_injectable col
adamc@990 7 }
adamc@987 8
adamc@991 9 fun local [t :: Type] (inj : sql_injectable t) = {Link = noParent,
adamc@991 10 Inj = inj}
adamc@991 11
adamc@987 12 functor Table(M : sig
adamc@990 13 con cols :: {(Type * Type)}
adamc@987 14 val cols : $(map meta cols)
adamc@987 15 constraint [Id] ~ cols
adamc@987 16 val folder : folder cols
adamc@987 17 end) = struct
adamc@987 18 type id = int
adamc@990 19 con fs' = map fst M.cols
adamc@990 20 con fs = [Id = id] ++ fs'
adamc@990 21 type row' = $fs'
adamc@990 22 type row = $fs
adamc@987 23
adamc@990 24 fun resultsOut q = query q (fn r ls => return (r.T :: ls)) []
adamc@990 25 fun resultOut q = ro <- oneOrNoRows q; return (Option.mp (fn r => r .T) ro)
adamc@989 26
adamc@987 27 sequence s
adamc@989 28 table t : fs
adamc@987 29
adamc@990 30 val inj = _
adamc@990 31 val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}),
adamc@990 32 Inj = inj}
adamc@988 33
adamc@990 34 fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') =
adamc@1093 35 @map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1]
adamc@1093 36 (fn [ts] meta v => @sql_inject meta.Inj v)
adamc@1093 37 M.folder M.cols r
adamc@988 38
adamc@990 39 fun create (r : row') =
adamc@987 40 id <- nextval s;
adamc@988 41 dml (insert t ({Id = sql_inject id} ++ ensql r));
adamc@988 42 return ({Id = id} ++ r)
adamc@988 43
adamc@988 44 fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]})
adamc@988 45
adamc@1093 46 fun save r = dml (update [fs'] (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]}))
adamc@988 47
adamc@988 48 fun lookup id =
adamc@988 49 ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]});
adamc@988 50 return (Option.mp (fn r => r.T) ro)
adamc@988 51
adamc@989 52
adamc@989 53 val list = resultsOut (SELECT * FROM t)
adamc@989 54
adamc@989 55 con col = fn t => {Exp : sql_exp [T = fs] [] [] t,
adamc@989 56 Inj : sql_injectable t}
adamc@989 57 val idCol = {Exp = sql_field [#T] [#Id], Inj = _}
adamc@1002 58 con meta' = fn (fs :: {Type}) (col :: Type, parent :: Type) =>
adamc@1002 59 {Col : {Exp : sql_exp [T = fs] [] [] col,
adamc@1002 60 Inj : sql_injectable col},
adamc@1002 61 Parent : $fs -> transaction (option parent)}
adamc@1093 62 val cols = @foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] =>
adamc@1093 63 $(map (meta' (map fst (before ++ after))) before)]
adamc@1093 64 (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}]
adamc@1093 65 [[nm] ~ before] (meta : meta ts)
adamc@1093 66 (acc : after :: {(Type * Type)} -> [before ~ after] =>
adamc@1093 67 $(map (meta' (map fst (before ++ after))) before))
adamc@1093 68 [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] =>
adamc@1093 69 {nm = {Col = {Exp = sql_field [#T] [nm],
adamc@1093 70 Inj = meta.Inj},
adamc@1093 71 Parent = fn r => meta.Link r.nm}}
adamc@1093 72 ++ acc [[nm = ts] ++ after] !)
adamc@1093 73 (fn [after :: {(Type * Type)}] [[] ~ after] => {})
adamc@1093 74 M.folder M.cols
adamc@1093 75 [[Id = (id, row)]] !
adamc@989 76
adamc@989 77 type filter = sql_exp [T = fs] [] [] bool
adamc@990 78 fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f})
adamc@989 79 fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f})
adamc@989 80
adamc@989 81 fun bin (b : t ::: Type -> sql_binary t t bool) [t] (c : col t) (v : t) =
adamc@989 82 sql_binary b c.Exp (@sql_inject c.Inj v)
adamc@1093 83 val eq = @@bin @@sql_eq
adamc@1093 84 val ne = @@bin @@sql_ne
adamc@1093 85 val lt = @@bin @@sql_lt
adamc@1093 86 val le = @@bin @@sql_le
adamc@1093 87 val gt = @@bin @@sql_gt
adamc@1093 88 val ge = @@bin @@sql_ge
adamc@989 89
adamc@989 90 fun bb (b : sql_binary bool bool bool) (f1 : filter) (f2 : filter) =
adamc@989 91 sql_binary b f1 f2
adamc@989 92 val _and = bb sql_and
adamc@989 93 val or = bb sql_or
adamc@987 94 end