From 2ed54658340ec7c94084ed21d9a4964b2c6d0afc Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 5 Oct 2009 17:24:21 -0400 Subject: Orm searching --- demo/more/orm.ur | 44 +++++++++++++++++++++++++++++++++++++++++--- demo/more/orm.urs | 17 +++++++++++++++++ 2 files changed, 58 insertions(+), 3 deletions(-) diff --git a/demo/more/orm.ur b/demo/more/orm.ur index 16b82c84..f976fcb2 100644 --- a/demo/more/orm.ur +++ b/demo/more/orm.ur @@ -16,10 +16,12 @@ functor Table(M : sig val id : meta id = {Link = (), Inj = inj} + con fs = [Id = id] ++ M.cols + sequence s - table t : ([Id = id] ++ M.cols) + table t : fs - type row = $([Id = id] ++ M.cols) + type row = $fs fun ensql [avail] (r : $M.cols) : $(map (sql_exp avail [] []) M.cols) = map2 [meta] [Top.id] [sql_exp avail [] []] @@ -39,5 +41,41 @@ functor Table(M : sig ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]}); return (Option.mp (fn r => r.T) ro) - val list = query (SELECT * FROM t) (fn r ls => return (r.T :: ls)) [] + fun resultsOut q = query q (fn r ls => return (r.T :: ls)) [] + + 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 = _} + val cols = foldR [meta] [fn before => after :: {Type} -> [before ~ after] => + $(map (fn t => {Exp : sql_exp [T = before ++ after] [] [] t, + Inj : sql_injectable t}) before)] + (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before] (meta : meta t) + (acc : after :: {Type} -> [before ~ after] => + $(map (fn t => {Exp : sql_exp [T = before ++ after] [] [] t, + Inj : sql_injectable t}) before)) + [after :: {Type}] [[nm = t] ++ before ~ after] => + {nm = {Exp = sql_field [#T] [nm], + Inj = meta.Inj}} ++ acc [[nm = t] ++ after] !) + (fn [after :: {Type}] [[] ~ after] => {}) + [_] M.folder M.cols + [[Id = id]] ! + + type filter = sql_exp [T = fs] [] [] bool + 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 diff --git a/demo/more/orm.urs b/demo/more/orm.urs index f25f9ff0..f284d3ec 100644 --- a/demo/more/orm.urs +++ b/demo/more/orm.urs @@ -22,4 +22,21 @@ functor Table(M : sig val save : row -> transaction unit val lookup : id -> transaction (option row) val list : transaction (list row) + + con col :: Type -> Type + val idCol : col id + val cols : $(map col M.cols) + + type filter + val search : filter -> transaction (list row) + + val eq : t ::: Type -> col t -> t -> filter + val ne : t ::: Type -> col t -> t -> filter + val lt : t ::: Type -> col t -> t -> filter + val le : t ::: Type -> col t -> t -> filter + val gt : t ::: Type -> col t -> t -> filter + val ge : t ::: Type -> col t -> t -> filter + + val _and : filter -> filter -> filter + val or : filter -> filter -> filter end -- cgit v1.2.3