Mercurial > urweb

annotate demo/more/orm.ur @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents bb3fc575cfe7
children 8d3aa6c7cee0
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@990 35 map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1]
adamc@990 36 (fn [ts] meta v => @sql_inject meta.Inj v)
adamc@988 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@990 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@990 62 val cols = foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] =>
adamc@990 63 $(map (meta' (map fst (before ++ after))) before)]
adamc@990 64 (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}]
adamc@990 65 [[nm] ~ before] (meta : meta ts)
adamc@990 66 (acc : after :: {(Type * Type)} -> [before ~ after] =>
adamc@990 67 $(map (meta' (map fst (before ++ after))) before))
adamc@990 68 [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] =>
adamc@990 69 {nm = {Col = {Exp = sql_field [#T] [nm],
adamc@990 70 Inj = meta.Inj},
adamc@990 71 Parent = fn r => meta.Link r.nm}}
adamc@990 72 ++ acc [[nm = ts] ++ after] !)
adamc@990 73 (fn [after :: {(Type * Type)}] [[] ~ after] => {})
adamc@989 74 [_] M.folder M.cols
adamc@990 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@989 83 val eq = bin @@sql_eq
adamc@989 84 val ne = bin @@sql_ne
adamc@989 85 val lt = bin @@sql_lt
adamc@989 86 val le = bin @@sql_le
adamc@989 87 val gt = bin @@sql_gt
adamc@989 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