# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1257018710 14400
# Node ID 4de35df3d545cb232ec6bdf30fb6509d786124fc
# Parent  7a4a55e05081eaaea1adef832473886f67e67301
Start of bidding implementation compiles

diff -r 7a4a55e05081 -r 4de35df3d545 demo/more/bid.ur
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/more/bid.ur	Sat Oct 31 15:51:50 2009 -0400
@@ -0,0 +1,34 @@
+functor Make(M : Conference.INPUT) = struct
+    open M
+
+    table bid : {User : userId, Paper : paperId, Interest : char}
+          PRIMARY KEY (User, Paper)
+
+    table assignment : {User : userId, Paper : paperId}
+          PRIMARY KEY (User, Paper)
+
+    fun isOnPc id =
+        ro <- oneOrNoRows1 (SELECT user.OnPc
+                            FROM user
+                            WHERE user.Id = {[id]});
+        return (case ro of
+                    None => False
+                  | Some r => r.OnPc)
+
+    val linksForPc =
+        let
+            fun bid () =
+                me <- getLogin;
+                return <xml>Bidding time!</xml>
+        in
+            <xml>
+              <li> <a link={bid ()}>Bid on papers</a></li>
+            </xml>
+        end
+
+    con yourPaperTables = [Assignment = _]
+    constraint [Paper] ~ yourPaperTables
+    fun joinYourPaper [tabs] [paper] [[Paper] ~ tabs] [[Paper] ~ _] [tabs ~ yourPaperTables] [[Id] ~ paper]
+        (fi : sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)) =
+        sql_inner_join fi (sql_from_table [#Assignment] assignment) (WHERE Paper.Id = Assignment.Paper)
+end
diff -r 7a4a55e05081 -r 4de35df3d545 demo/more/bid.urs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/more/bid.urs	Sat Oct 31 15:51:50 2009 -0400
@@ -0,0 +1,2 @@
+functor Make (M : Conference.INPUT) : Conference.OUTPUT where con userId = M.userId
+                                                        where con paperId = M.paperId
diff -r 7a4a55e05081 -r 4de35df3d545 demo/more/conference.ur
--- a/demo/more/conference.ur	Sun Oct 25 15:29:21 2009 -0400
+++ b/demo/more/conference.ur	Sat Oct 31 15:51:50 2009 -0400
@@ -1,3 +1,36 @@
+signature INPUT = sig
+    con paper :: {(Type * Type)}
+    constraint [Id, Document] ~ paper
+
+    type userId
+    val userId_inj : sql_injectable_prim userId
+    table user : {Id : userId, Nam : string, Password : string, Chair : bool, OnPc : bool}
+                     PRIMARY KEY Id,
+          CONSTRAINT Nam UNIQUE Nam
+
+    type paperId
+    val paperId_inj : sql_injectable_prim paperId
+    table paper : ([Id = paperId, Document = blob] ++ map fst paper)
+                      PRIMARY KEY Id
+
+    val checkLogin : transaction (option {Id : userId, Nam : string, Chair : bool, OnPc : bool})
+    val getLogin : transaction {Id : userId, Nam : string, Chair : bool, OnPc : bool}
+end
+
+signature OUTPUT = sig
+    type userId
+    type paperId
+
+    val linksForPc : xbody
+
+    con yourPaperTables :: {{Type}}
+    constraint [Paper] ~ yourPaperTables
+    val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type}
+        -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] =>
+        sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)
+        -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs)
+end
+
 open Meta
 
 functor Make(M : sig
@@ -13,6 +46,10 @@
 
                  val submissionDeadline : time
                  val summarizePaper : $(map fst paper) -> xbody
+
+                 functor Make (M : INPUT where con paper = paper)
+                         : OUTPUT where con userId = M.userId
+                                  where con paperId = M.paperId
              end) = struct
 
     table user : {Id : int, Nam : string, Password : string, Chair : bool, OnPc : bool}
@@ -55,6 +92,20 @@
             None => error <xml>You must be logged in to do that.</xml>
           | Some r => return r
 
+    structure O = M.Make(struct
+                             val user = user
+                             val paper = paper
+                             val checkLogin = checkLogin
+                             val getLogin = getLogin
+                         end)
+
+    val checkOnPc =
+        r <- getLogin;
+        if r.OnPc then
+            return ()
+        else
+            error <xml>You aren't authorized to do that.</xml>
+
     fun checkPaper id =
         r <- getLogin;
         if r.OnPc then
@@ -142,7 +193,10 @@
                     <xml/>}
 
                {if me.OnPc then
-                    <xml><li><a link={all ()}>All papers</a></li></xml>
+                    <xml>
+                      <li><a link={all ()}>All papers</a></li>
+                      {O.linksForPc}
+                    </xml>
                 else
                     <xml/>}
 
@@ -202,17 +256,37 @@
             </body></xml>
         end
 
-    and all () =
-        ps <- queryX (SELECT paper.Id, paper.{{map fst M.paper}} FROM paper)
-              (fn r => <xml><li><a link={one r.Paper.Id}>{M.summarizePaper (r.Paper -- #Id)}</a></li></xml>);
+    and listPapers [tabs] [[Paper] ~ tabs] (q : sql_query ([Paper = [Id = int] ++ map fst M.paper] ++ tabs) []) =
+        checkOnPc;
+        ps <- queryX q
+                     (fn r => <xml><li><a link={one r.Paper.Id}>{M.summarizePaper (r.Paper -- #Id)}</a></li></xml>);
         return <xml><body>
           <h1>All Papers</h1>
-
+          
           <ul>
             {ps}
           </ul>
         </body></xml>
 
+    and all () =
+        checkOnPc;
+        listPapers (SELECT paper.Id, paper.{{map fst M.paper}} FROM paper)
+
+    and your () =
+        me <- getLogin;
+        listPapers (sql_query {Rows = sql_query1 {Distinct = False,
+                                                  From = O.joinYourPaper (sql_from_table [#Paper] paper),
+                                                  Where = (WHERE TRUE),
+                                                  GroupBy = sql_subset_all [_],
+                                                  Having = (WHERE TRUE),
+                                                  SelectFields = sql_subset [[Paper = ([Id = _] ++ map fst M.paper, _)]
+                                                                                 ++ map (fn ts => ([], ts))
+                                                                                            O.yourPaperTables],
+                                                  SelectExps = {}},
+                               OrderBy = sql_order_by_Nil [_],
+                               Limit = sql_no_limit,
+                               Offset = sql_no_offset})
+
     and one id =
         let
             fun newReview r =
diff -r 7a4a55e05081 -r 4de35df3d545 demo/more/conference.urp
--- a/demo/more/conference.urp	Sun Oct 25 15:29:21 2009 -0400
+++ b/demo/more/conference.urp	Sat Oct 31 15:51:50 2009 -0400
@@ -8,3 +8,4 @@
 dnat
 conference
 conferenceFields
+bid
diff -r 7a4a55e05081 -r 4de35df3d545 demo/more/conference.urs
--- a/demo/more/conference.urs	Sun Oct 25 15:29:21 2009 -0400
+++ b/demo/more/conference.urs	Sat Oct 31 15:51:50 2009 -0400
@@ -1,3 +1,36 @@
+signature INPUT = sig
+    con paper :: {(Type * Type)}
+    constraint [Id, Document] ~ paper
+
+    type userId
+    val userId_inj : sql_injectable_prim userId
+    table user : {Id : userId, Nam : string, Password : string, Chair : bool, OnPc : bool}
+                     PRIMARY KEY Id,
+          CONSTRAINT Nam UNIQUE Nam
+
+    type paperId
+    val paperId_inj : sql_injectable_prim paperId
+    table paper : ([Id = paperId, Document = blob] ++ map fst paper)
+                      PRIMARY KEY Id
+
+    val checkLogin : transaction (option {Id : userId, Nam : string, Chair : bool, OnPc : bool})
+    val getLogin : transaction {Id : userId, Nam : string, Chair : bool, OnPc : bool}
+end
+
+signature OUTPUT = sig
+    type userId
+    type paperId
+
+    val linksForPc : xbody
+
+    con yourPaperTables :: {{Type}}
+    constraint [Paper] ~ yourPaperTables
+    val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type}
+        -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] =>
+        sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)
+        -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs)
+end
+
 functor Make(M : sig
                  con paper :: {(Type * Type)}
                  constraint [Id, Document, Authors] ~ paper
@@ -11,6 +44,10 @@
 
                  val submissionDeadline : time
                  val summarizePaper : $(map fst paper) -> xbody
+
+                 functor Make (M : INPUT where con paper = paper)
+                         : OUTPUT where con userId = M.userId
+                                  where con paperId = M.paperId
              end) : sig
 
     val main : unit -> transaction page
diff -r 7a4a55e05081 -r 4de35df3d545 demo/more/conference1.ur
--- a/demo/more/conference1.ur	Sun Oct 25 15:29:21 2009 -0400
+++ b/demo/more/conference1.ur	Sat Oct 31 15:51:50 2009 -0400
@@ -8,4 +8,8 @@
                          val submissionDeadline = readError "2009-11-22 23:59:59"
 
                          fun summarizePaper r = cdata r.Title
+
+                         functor Make (M : Conference.INPUT where con paper = _) = struct
+                             open Bid.Make(M)
+                         end
                      end)
diff -r 7a4a55e05081 -r 4de35df3d545 src/elaborate.sml
--- a/src/elaborate.sml	Sun Oct 25 15:29:21 2009 -0400
+++ b/src/elaborate.sml	Sat Oct 31 15:51:50 2009 -0400
@@ -3418,6 +3418,7 @@
                     val denv' =
                         case #1 str' of
                             L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
+                          | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
                           | _ => denv
                 in
                     case #1 (hnormSgn env sgn') of