comparison demo/more/conference.ur @ 1022:4de35df3d545

Start of bidding implementation compiles
author Adam Chlipala <adamc@hcoop.net>
date Sat, 31 Oct 2009 15:51:50 -0400
parents e47303e5d73d
children e46227efcbba
comparison
equal deleted inserted replaced
1021:7a4a55e05081 1022:4de35df3d545
1 signature INPUT = sig
2 con paper :: {(Type * Type)}
3 constraint [Id, Document] ~ paper
4
5 type userId
6 val userId_inj : sql_injectable_prim userId
7 table user : {Id : userId, Nam : string, Password : string, Chair : bool, OnPc : bool}
8 PRIMARY KEY Id,
9 CONSTRAINT Nam UNIQUE Nam
10
11 type paperId
12 val paperId_inj : sql_injectable_prim paperId
13 table paper : ([Id = paperId, Document = blob] ++ map fst paper)
14 PRIMARY KEY Id
15
16 val checkLogin : transaction (option {Id : userId, Nam : string, Chair : bool, OnPc : bool})
17 val getLogin : transaction {Id : userId, Nam : string, Chair : bool, OnPc : bool}
18 end
19
20 signature OUTPUT = sig
21 type userId
22 type paperId
23
24 val linksForPc : xbody
25
26 con yourPaperTables :: {{Type}}
27 constraint [Paper] ~ yourPaperTables
28 val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type}
29 -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] =>
30 sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)
31 -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs)
32 end
33
1 open Meta 34 open Meta
2 35
3 functor Make(M : sig 36 functor Make(M : sig
4 con paper :: {(Type * Type)} 37 con paper :: {(Type * Type)}
5 constraint [Id, Document, Authors] ~ paper 38 constraint [Id, Document, Authors] ~ paper
11 val review : $(map meta review) 44 val review : $(map meta review)
12 val reviewFolder : folder review 45 val reviewFolder : folder review
13 46
14 val submissionDeadline : time 47 val submissionDeadline : time
15 val summarizePaper : $(map fst paper) -> xbody 48 val summarizePaper : $(map fst paper) -> xbody
49
50 functor Make (M : INPUT where con paper = paper)
51 : OUTPUT where con userId = M.userId
52 where con paperId = M.paperId
16 end) = struct 53 end) = struct
17 54
18 table user : {Id : int, Nam : string, Password : string, Chair : bool, OnPc : bool} 55 table user : {Id : int, Nam : string, Password : string, Chair : bool, OnPc : bool}
19 PRIMARY KEY Id, 56 PRIMARY KEY Id,
20 CONSTRAINT Nam UNIQUE Nam 57 CONSTRAINT Nam UNIQUE Nam
52 val getLogin = 89 val getLogin =
53 ro <- checkLogin; 90 ro <- checkLogin;
54 case ro of 91 case ro of
55 None => error <xml>You must be logged in to do that.</xml> 92 None => error <xml>You must be logged in to do that.</xml>
56 | Some r => return r 93 | Some r => return r
94
95 structure O = M.Make(struct
96 val user = user
97 val paper = paper
98 val checkLogin = checkLogin
99 val getLogin = getLogin
100 end)
101
102 val checkOnPc =
103 r <- getLogin;
104 if r.OnPc then
105 return ()
106 else
107 error <xml>You aren't authorized to do that.</xml>
57 108
58 fun checkPaper id = 109 fun checkPaper id =
59 r <- getLogin; 110 r <- getLogin;
60 if r.OnPc then 111 if r.OnPc then
61 return () 112 return ()
140 <xml><li><a link={Users.main ()}>Manage users</a></li></xml> 191 <xml><li><a link={Users.main ()}>Manage users</a></li></xml>
141 else 192 else
142 <xml/>} 193 <xml/>}
143 194
144 {if me.OnPc then 195 {if me.OnPc then
145 <xml><li><a link={all ()}>All papers</a></li></xml> 196 <xml>
197 <li><a link={all ()}>All papers</a></li>
198 {O.linksForPc}
199 </xml>
146 else 200 else
147 <xml/>} 201 <xml/>}
148 202
149 {if now < M.submissionDeadline then 203 {if now < M.submissionDeadline then
150 <xml><li><a link={submit ()}>Submit</a></li></xml> 204 <xml><li><a link={submit ()}>Submit</a></li></xml>
200 <submit value="Submit" action={doSubmit}/> 254 <submit value="Submit" action={doSubmit}/>
201 </form> 255 </form>
202 </body></xml> 256 </body></xml>
203 end 257 end
204 258
205 and all () = 259 and listPapers [tabs] [[Paper] ~ tabs] (q : sql_query ([Paper = [Id = int] ++ map fst M.paper] ++ tabs) []) =
206 ps <- queryX (SELECT paper.Id, paper.{{map fst M.paper}} FROM paper) 260 checkOnPc;
207 (fn r => <xml><li><a link={one r.Paper.Id}>{M.summarizePaper (r.Paper -- #Id)}</a></li></xml>); 261 ps <- queryX q
262 (fn r => <xml><li><a link={one r.Paper.Id}>{M.summarizePaper (r.Paper -- #Id)}</a></li></xml>);
208 return <xml><body> 263 return <xml><body>
209 <h1>All Papers</h1> 264 <h1>All Papers</h1>
210 265
211 <ul> 266 <ul>
212 {ps} 267 {ps}
213 </ul> 268 </ul>
214 </body></xml> 269 </body></xml>
270
271 and all () =
272 checkOnPc;
273 listPapers (SELECT paper.Id, paper.{{map fst M.paper}} FROM paper)
274
275 and your () =
276 me <- getLogin;
277 listPapers (sql_query {Rows = sql_query1 {Distinct = False,
278 From = O.joinYourPaper (sql_from_table [#Paper] paper),
279 Where = (WHERE TRUE),
280 GroupBy = sql_subset_all [_],
281 Having = (WHERE TRUE),
282 SelectFields = sql_subset [[Paper = ([Id = _] ++ map fst M.paper, _)]
283 ++ map (fn ts => ([], ts))
284 O.yourPaperTables],
285 SelectExps = {}},
286 OrderBy = sql_order_by_Nil [_],
287 Limit = sql_no_limit,
288 Offset = sql_no_offset})
215 289
216 and one id = 290 and one id =
217 let 291 let
218 fun newReview r = 292 fun newReview r =
219 me <- getLogin; 293 me <- getLogin;