diff demo/more/conference.urs @ 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.urs	Sat Oct 31 15:51:50 2009 -0400
+++ b/demo/more/conference.urs	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
 
@@ -43,10 +48,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) : sig