From 2ed54658340ec7c94084ed21d9a4964b2c6d0afc Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
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