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

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
line wrap: on
line source
con link = fn col_parent :: (Type * Type) => col_parent.1 -> transaction (option col_parent.2)
fun noParent [t ::: Type] (_ : t) = return None

con meta = fn (col :: Type, parent :: Type) => {
	      Link : link (col, parent),
	      Inj : sql_injectable col
	      }

fun local [t :: Type] (inj : sql_injectable t) = {Link = noParent,
                                                  Inj = inj}

functor Table(M : sig
                  con cols :: {(Type * Type)}
                  val cols : $(map meta cols)
                  constraint [Id] ~ cols
                  val folder : folder cols
              end) = struct
    type id = int
    con fs' = map fst M.cols
    con fs = [Id = id] ++ fs'
    type row' = $fs'
    type row = $fs

    fun resultsOut q = query q (fn r ls => return (r.T :: ls)) []
    fun resultOut q = ro <- oneOrNoRows q; return (Option.mp (fn r => r .T) ro)

    sequence s
    table t : fs

    val inj = _
    val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}),
              Inj = inj}

    fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') =
        map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1]
             (fn [ts] meta v => @sql_inject meta.Inj v)
             [_] M.folder M.cols r

    fun create (r : row') =
        id <- nextval s;
        dml (insert t ({Id = sql_inject id} ++ ensql r));
        return ({Id = id} ++ r)

    fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]})

    fun save r = dml (update [fs'] ! (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]}))

    fun lookup id =
        ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]});
        return (Option.mp (fn r => r.T) ro)


    val list = resultsOut (SELECT * FROM t)

    con col = fn t => {Exp : sql_exp [T = fs] [] [] t,
                       Inj : sql_injectable t}
    val idCol = {Exp = sql_field [#T] [#Id], Inj = _}
    con meta' = fn (fs :: {Type}) (col :: Type, parent :: Type) =>
                   {Col : {Exp : sql_exp [T = fs] [] [] col,
                           Inj : sql_injectable col},
                    Parent : $fs -> transaction (option parent)}
    val cols = foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] =>
                                $(map (meta' (map fst (before ++ after))) before)]
               (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}]
                                [[nm] ~ before] (meta : meta ts)
                                (acc : after :: {(Type * Type)} -> [before ~ after] =>
                                 $(map (meta' (map fst (before ++ after))) before))
                                [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] =>
                   {nm = {Col = {Exp = sql_field [#T] [nm],
                                 Inj = meta.Inj},
                          Parent = fn r => meta.Link r.nm}}
                       ++ acc [[nm = ts] ++ after] !)
               (fn [after :: {(Type * Type)}] [[] ~ after] => {})
               [_] M.folder M.cols
               [[Id = (id, row)]] !

    type filter = sql_exp [T = fs] [] [] bool
    fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f})
    fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f})

    fun bin (b : t ::: Type -> sql_binary t t bool) [t] (c : col t) (v : t) =
        sql_binary b c.Exp (@sql_inject c.Inj v)
    val eq = bin @@sql_eq
    val ne = bin @@sql_ne
    val lt = bin @@sql_lt
    val le = bin @@sql_le
    val gt = bin @@sql_gt
    val ge = bin @@sql_ge

    fun bb (b : sql_binary bool bool bool) (f1 : filter) (f2 : filter) =
        sql_binary b f1 f2
    val _and = bb sql_and
    val or = bb sql_or
end