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