diff demo/more/conference.ur @ 1023:e46227efcbba

Bidding interface
author Adam Chlipala <adamc@hcoop.net>
date Sun, 01 Nov 2009 10:20:20 -0500
parents 4de35df3d545
children 7facf72aaf0a
line wrap: on
line diff
--- a/demo/more/conference.ur	Sat Oct 31 15:51:50 2009 -0400
+++ b/demo/more/conference.ur	Sun Nov 01 10:20:20 2009 -0500
@@ -1,5 +1,5 @@
 signature INPUT = sig
-    con paper :: {(Type * Type)}
+    con paper :: {Type}
     constraint [Id, Document] ~ paper
 
     type userId
@@ -10,14 +10,19 @@
 
     type paperId
     val paperId_inj : sql_injectable_prim paperId
-    table paper : ([Id = paperId, Document = blob] ++ map fst paper)
+    val paperId_show : show paperId
+    val paperId_read : read paperId
+    table paper : ([Id = paperId, Document = blob] ++ 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}
+    val getPcLogin : transaction {Id : userId, Nam : string, Chair : bool}
+    val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $paper -> xml ([Body] ++ ctx) [] []
 end
 
 signature OUTPUT = sig
+    con paper :: {Type}
     type userId
     type paperId
 
@@ -45,10 +50,11 @@
                  val reviewFolder : folder review
 
                  val submissionDeadline : time
-                 val summarizePaper : $(map fst paper) -> xbody
+                 val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper) -> xml ([Body] ++ ctx) [] []
 
-                 functor Make (M : INPUT where con paper = paper)
-                         : OUTPUT where con userId = M.userId
+                 functor Make (M : INPUT where con paper = map fst paper)
+                         : OUTPUT where con paper = map fst paper
+                                  where con userId = M.userId
                                   where con paperId = M.paperId
              end) = struct
 
@@ -92,11 +98,20 @@
             None => error <xml>You must be logged in to do that.</xml>
           | Some r => return r
 
+    val getPcLogin =
+        r <- getLogin;
+        if r.OnPc then
+            return (r -- #OnPc)
+        else
+            error <xml>You are not on the PC.</xml>
+
     structure O = M.Make(struct
                              val user = user
                              val paper = paper
                              val checkLogin = checkLogin
                              val getLogin = getLogin
+                             val getPcLogin = getPcLogin
+                             val summarizePaper = @@M.summarizePaper
                          end)
 
     val checkOnPc =
@@ -195,6 +210,7 @@
                {if me.OnPc then
                     <xml>
                       <li><a link={all ()}>All papers</a></li>
+                      <li><a link={your ()}>Your papers</a></li>
                       {O.linksForPc}
                     </xml>
                 else