Mercurial > urweb

annotate demo/more/orm.ur @ 1554:396e8d881205

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