# HG changeset patch # User Adam Chlipala # Date 1254777861 14400 # Node ID 0bdc4d538f1ca5f19665627561e244c17b65df00 # Parent d923b47e483dac0b54836f21c196003a9b8178f4 Orm searching diff -r d923b47e483d -r 0bdc4d538f1c demo/more/orm.ur --- a/demo/more/orm.ur Mon Oct 05 17:00:04 2009 -0400 +++ b/demo/more/orm.ur Mon Oct 05 17:24:21 2009 -0400 @@ -16,10 +16,12 @@ 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 @@ 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 -r d923b47e483d -r 0bdc4d538f1c demo/more/orm.urs --- a/demo/more/orm.urs Mon Oct 05 17:00:04 2009 -0400 +++ b/demo/more/orm.urs Mon Oct 05 17:24:21 2009 -0400 @@ -22,4 +22,21 @@ 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