Mercurial > urweb

annotate demo/more/conference.ur @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents 5d9f47124c4c
children
rev   line source
adamc@1022 1 signature INPUT = sig
adamc@1023 2 con paper :: {Type}
adamc@1022 3 constraint [Id, Document] ~ paper
adamc@1022 4
adamc@1022 5 type userId
adamc@1022 6 val userId_inj : sql_injectable_prim userId
adamc@1022 7 table user : {Id : userId, Nam : string, Password : string, Chair : bool, OnPc : bool}
adamc@1022 8 PRIMARY KEY Id,
adamc@1022 9 CONSTRAINT Nam UNIQUE Nam
adamc@1022 10
adamc@1022 11 type paperId
adamc@1022 12 val paperId_inj : sql_injectable_prim paperId
adamc@1023 13 val paperId_show : show paperId
adamc@1023 14 val paperId_read : read paperId
adamc@1025 15 val paperId_eq : eq paperId
adamc@1023 16 table paper : ([Id = paperId, Document = blob] ++ paper)
adamc@1022 17 PRIMARY KEY Id
adamc@1022 18
adamc@1032 19 con review :: {Type}
adamc@1032 20 constraint [Paper, User] ~ review
adamc@1032 21 table review : ([Paper = paperId, User = userId] ++ review)
adamc@1032 22 PRIMARY KEY (Paper, User)
adamc@1032 23
adamc@1022 24 val checkLogin : transaction (option {Id : userId, Nam : string, Chair : bool, OnPc : bool})
adamc@1022 25 val getLogin : transaction {Id : userId, Nam : string, Chair : bool, OnPc : bool}
adamc@1023 26 val getPcLogin : transaction {Id : userId, Nam : string, Chair : bool}
adamc@1025 27 val checkChair : transaction unit
adamc@1023 28 val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $paper -> xml ([Body] ++ ctx) [] []
adamc@1022 29 end
adamc@1022 30
adamc@1022 31 signature OUTPUT = sig
adamc@1023 32 con paper :: {Type}
adamc@1022 33 type userId
adamc@1022 34 type paperId
adamc@1022 35
adamc@1022 36 val linksForPc : xbody
adamc@1025 37 val linksForChair : xbody
adamc@1022 38
adamc@1022 39 con yourPaperTables :: {{Type}}
adamc@1022 40 constraint [Paper] ~ yourPaperTables
adamc@1022 41 val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type}
adamc@1022 42 -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] =>
adamc@1027 43 userId
adamc@1027 44 -> sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)
adamc@1022 45 -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs)
adamc@1022 46 end
adamc@1022 47
adamc@1004 48 open Meta
adamc@1001 49
adamc@1001 50 functor Make(M : sig
adamc@1003 51 con paper :: {(Type * Type)}
adamc@1010 52 constraint [Id, Document, Authors] ~ paper
adamc@1030 53 val paper : $(map Meta.meta paper)
adamc@1007 54 val paperFolder : folder paper
adamc@1003 55
adamc@1030 56 con paperPrivate :: {Type}
adamc@1030 57 constraint [Id, Document, Authors] ~ paperPrivate
adamc@1030 58 constraint paper ~ paperPrivate
adamc@1030 59 val paperPrivate : $(map Meta.private paperPrivate)
adamc@1030 60 val paperPrivateFolder : folder paperPrivate
adamc@1030 61
adamc@1001 62 con review :: {(Type * Type)}
adamc@1003 63 constraint [Paper, User] ~ review
adamc@1030 64 val review : $(map Meta.meta review)
adamc@1011 65 val reviewFolder : folder review
adamc@1006 66
adamc@1006 67 val submissionDeadline : time
adamc@1030 68 val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper ++ paperPrivate)
adamc@1030 69 -> xml ([Body] ++ ctx) [] []
adamc@1022 70
adamc@1032 71 functor Make (M : INPUT where con paper = map fst paper ++ paperPrivate
adamc@1032 72 where con review = map fst review)
adamc@1030 73 : OUTPUT where con paper = map fst paper ++ paperPrivate
adamc@1023 74 where con userId = M.userId
adamc@1022 75 where con paperId = M.paperId
adamc@1001 76 end) = struct
adamc@1001 77
adamc@1003 78 table user : {Id : int, Nam : string, Password : string, Chair : bool, OnPc : bool}
adamc@1003 79 PRIMARY KEY Id,
adamc@1003 80 CONSTRAINT Nam UNIQUE Nam
adamc@1003 81 sequence userId
adamc@1003 82
adamc@1030 83 con paper = [Id = int, Document = blob] ++ map fst M.paper ++ M.paperPrivate
adamc@1003 84 table paper : paper
adamc@1003 85 PRIMARY KEY Id
adamc@1003 86 sequence paperId
adamc@1003 87
adamc@1010 88 table authorship : {Paper : int, User : int}
adamc@1010 89 PRIMARY KEY (Paper, User),
adamc@1011 90 CONSTRAINT Paper FOREIGN KEY Paper REFERENCES paper(Id) ON DELETE CASCADE,
adamc@1010 91 CONSTRAINT User FOREIGN KEY User REFERENCES user(Id)
adamc@1010 92
adamc@1003 93 con review = [Paper = int, User = int] ++ map fst M.review
adamc@1003 94 table review : review
adamc@1003 95 PRIMARY KEY (Paper, User),
adamc@1003 96 CONSTRAINT Paper FOREIGN KEY Paper REFERENCES paper(Id),
adamc@1003 97 CONSTRAINT User FOREIGN KEY User REFERENCES user(Id)
adamc@1003 98 sequence reviewId
adamc@1003 99
adamc@1003 100 cookie login : {Id : int, Password : string}
adamc@1003 101
adamc@1004 102 val checkLogin =
adamc@1003 103 r <- getCookie login;
adamc@1003 104 case r of
adamc@1003 105 None => return None
adamc@1003 106 | Some r =>
adamc@1003 107 oneOrNoRows1 (SELECT user.Id, user.Nam, user.Chair, user.OnPc
adamc@1003 108 FROM user
adamc@1003 109 WHERE user.Id = {[r.Id]}
adamc@1003 110 AND user.Password = {[r.Password]})
adamc@1003 111
adamc@1010 112 val getLogin =
adamc@1010 113 ro <- checkLogin;
adamc@1010 114 case ro of
adamc@1010 115 None => error <xml>You must be logged in to do that.</xml>
adamc@1010 116 | Some r => return r
adamc@1010 117
adamc@1023 118 val getPcLogin =
adamc@1023 119 r <- getLogin;
adamc@1023 120 if r.OnPc then
adamc@1023 121 return (r -- #OnPc)
adamc@1023 122 else
adamc@1023 123 error <xml>You are not on the PC.</xml>
adamc@1023 124
adamc@1025 125 val checkChair =
adamc@1025 126 r <- getLogin;
adamc@1025 127 if r.Chair then
adamc@1025 128 return ()
adamc@1025 129 else
adamc@1025 130 error <xml>You are not a chair.</xml>
adamc@1025 131
adamc@1022 132 structure O = M.Make(struct
adamc@1022 133 val user = user
adamc@1022 134 val paper = paper
adamc@1032 135 val review = review
adamc@1022 136 val checkLogin = checkLogin
adamc@1022 137 val getLogin = getLogin
adamc@1023 138 val getPcLogin = getPcLogin
adamc@1025 139 val checkChair = checkChair
adamc@1023 140 val summarizePaper = @@M.summarizePaper
adamc@1022 141 end)
adamc@1022 142
adamc@1022 143 val checkOnPc =
adamc@1022 144 r <- getLogin;
adamc@1022 145 if r.OnPc then
adamc@1022 146 return ()
adamc@1022 147 else
adamc@1022 148 error <xml>You aren't authorized to do that.</xml>
adamc@1022 149
adamc@1009 150 fun checkPaper id =
adamc@1010 151 r <- getLogin;
adamc@1010 152 if r.OnPc then
adamc@1009 153 return ()
adamc@1009 154 else
adamc@1010 155 error <xml>You aren't authorized to see that paper.</xml>
adamc@1009 156
adamc@1004 157 structure Users = BulkEdit.Make(struct
adamc@1004 158 con keyName = #Id
adamc@1004 159 val visible = {Nam = string "Name",
adamc@1004 160 Chair = bool "Chair?",
adamc@1004 161 OnPc = bool "On PC?"}
adamc@1004 162
adamc@1004 163 val title = "Users"
adamc@1004 164 val isAllowed =
adamc@1004 165 me <- checkLogin;
adamc@1004 166 return (Option.isSome me)
adamc@1004 167
adamc@1004 168 val t = user
adamc@1004 169 end)
adamc@1004 170
adamc@1003 171 fun doRegister r =
adamc@1003 172 n <- oneRowE1 (SELECT COUNT( * ) AS N
adamc@1003 173 FROM user
adamc@1003 174 WHERE user.Nam = {[r.Nam]});
adamc@1003 175 if n > 0 then
adamc@1003 176 register (Some "Sorry; that username is taken.")
adamc@1003 177 else
adamc@1003 178 id <- nextval userId;
adamc@1003 179 dml (INSERT INTO user (Id, Nam, Password, Chair, OnPc)
adamc@1003 180 VALUES ({[id]}, {[r.Nam]}, {[r.Password]}, FALSE, FALSE));
adamc@1003 181 setCookie login {Id = id, Password = r.Password};
adamc@1003 182 main ()
adamc@1003 183
adamc@1003 184 and register msg = return <xml><body>
adamc@1003 185 <h1>Registering a New Account</h1>
adamc@1003 186
adamc@1003 187 {case msg of
adamc@1003 188 None => <xml/>
adamc@1003 189 | Some msg => <xml><div>{[msg]}</div></xml>}
adamc@1003 190
adamc@1003 191 <form><table>
adamc@1003 192 <tr> <th>Username:</th> <td><textbox{#Nam}/></td> </tr>
adamc@1003 193 <tr> <th>Password:</th> <td><password{#Password}/></td> </tr>
adamc@1003 194 <tr> <th><submit action={doRegister}/></th> </tr>
adamc@1003 195 </table></form>
adamc@1003 196 </body></xml>
adamc@1003 197
adamc@1006 198 and signin r =
adamc@1006 199 ro <- oneOrNoRowsE1 (SELECT user.Id AS N
adamc@1006 200 FROM user
adamc@1006 201 WHERE user.Nam = {[r.Nam]}
adamc@1006 202 AND user.Password = {[r.Password]});
adamc@1006 203 (case ro of
adamc@1006 204 None => return ()
adamc@1006 205 | Some id => setCookie login {Id = id, Password = r.Password});
adamc@1006 206 m <- main' ();
adamc@1006 207 return <xml><body>
adamc@1006 208 {case ro of
adamc@1006 209 None => <xml><div>Invalid username or password.</div></xml>
adamc@1006 210 | _ => <xml/>}
adamc@1006 211
adamc@1006 212 {m}
adamc@1006 213 </body></xml>
adamc@1006 214
adamc@1006 215 and main' () =
adamc@1004 216 me <- checkLogin;
adamc@1006 217 now <- now;
adamc@1006 218 return <xml><ul>
adamc@1003 219 {case me of
adamc@1006 220 None => <xml>
adamc@1006 221 <li><a link={register None}>Register for access</a></li>
adamc@1006 222 <li><b>Log in:</b> <form><table>
adamc@1006 223 <tr> <th>Username:</th> <td><textbox{#Nam}/></td> </tr>
adamc@1006 224 <tr> <th>Password:</th> <td><password{#Password}/></td> </tr>
adamc@1006 225 <tr> <th><submit value="Log in" action={signin}/></th> </tr>
adamc@1006 226 </table></form></li>
adamc@1006 227 </xml>
adamc@1004 228 | Some me => <xml>
adamc@1004 229 <div>Welcome, {[me.Nam]}!</div>
adamc@1004 230
adamc@1004 231 {if me.Chair then
adamc@1025 232 <xml>
adamc@1025 233 <li><a link={Users.main ()}>Manage users</a></li>
adamc@1025 234 {O.linksForChair}
adamc@1025 235 </xml>
adamc@1004 236 else
adamc@1004 237 <xml/>}
adamc@1006 238
adamc@1009 239 {if me.OnPc then
adamc@1022 240 <xml>
adamc@1022 241 <li><a link={all ()}>All papers</a></li>
adamc@1023 242 <li><a link={your ()}>Your papers</a></li>
adamc@1022 243 {O.linksForPc}
adamc@1022 244 </xml>
adamc@1009 245 else
adamc@1009 246 <xml/>}
adamc@1009 247
adamc@1006 248 {if now < M.submissionDeadline then
adamc@1007 249 <xml><li><a link={submit ()}>Submit</a></li></xml>
adamc@1006 250 else
adamc@1006 251 <xml/>}
adamc@1004 252 </xml>}
adamc@1006 253 </ul></xml>
adamc@1006 254
adamc@1006 255 and main () =
adamc@1006 256 m <- main' ();
adamc@1006 257 return <xml><body>{m}</body></xml>
adamc@1001 258
adamc@1008 259 and submit () =
adamc@1008 260 let
adamc@1009 261 fun doSubmit r =
adamc@1010 262 me <- getLogin;
adamc@1010 263 coauthors <- List.mapM (fn name => oneOrNoRowsE1 (SELECT user.Id AS N
adamc@1010 264 FROM user
adamc@1010 265 WHERE user.Nam = {[name.Nam]})) r.Authors;
adamc@1010 266 if List.exists Option.isNone coauthors then
adamc@1010 267 error <xml>At least one of those coauthor usernames isn't registered.</xml>
adamc@1010 268 else
adamc@1010 269 id <- nextval paperId;
adamc@1010 270 dml (insert paper ({Id = sql_inject id, Document = sql_inject (fileData r.Document)}
adamc@1030 271 ++ ensql M.paper (r -- #Authors -- #Document) M.paperFolder
adamc@1030 272 ++ initialize M.paperPrivate M.paperPrivateFolder));
adamc@1010 273 List.app (fn uid =>
adamc@1010 274 case uid of
adamc@1010 275 None => error <xml>Impossible empty uid!</xml>
adamc@1010 276 | Some uid => dml (INSERT INTO authorship (Paper, User)
adamc@1010 277 VALUES ({[id]}, {[uid]})))
adamc@1010 278 (Some me.Id :: coauthors);
adamc@1010 279 return <xml><body>
adamc@1010 280 Thanks for submitting!
adamc@1010 281 </body></xml>
adamc@1008 282 in
adamc@1010 283 me <- getLogin;
adamc@1015 284 numAuthors <- Dnat.zero;
adamc@1010 285
adamc@1008 286 return <xml><body>
adamc@1008 287 <h1>Submit a Paper</h1>
adamc@1008 288
adamc@1008 289 <form>
adamc@1010 290 <b>Author:</b> {[me.Nam]}<br/>
adamc@1010 291 <subforms{#Authors}>
adamc@1015 292 {Dnat.render <xml><entry><b>Author:</b> <textbox{#Nam}/><br/></entry></xml> numAuthors}
adamc@1010 293 </subforms>
adamc@1015 294 <button value="Add author" onclick={Dnat.inc numAuthors}/><br/>
adamc@1015 295 <button value="Remove author" onclick={Dnat.dec numAuthors}/><br/>
adamc@1010 296 <br/>
adamc@1010 297
adamc@1010 298 {useMore (allWidgets M.paper M.paperFolder)}
adamc@1008 299 <b>Paper:</b> <upload{#Document}/><br/>
adamc@1008 300 <submit value="Submit" action={doSubmit}/>
adamc@1008 301 </form>
adamc@1008 302 </body></xml>
adamc@1008 303 end
adamc@1007 304
adamc@1030 305 and listPapers [tabs] [[Paper] ~ tabs]
adamc@1030 306 (q : sql_query ([Paper = [Id = int] ++ map fst M.paper ++ M.paperPrivate] ++ tabs) []) =
adamc@1022 307 checkOnPc;
adamc@1022 308 ps <- queryX q
adamc@1030 309 (fn r => <xml><li><a link={one r.Paper.Id}>{M.summarizePaper (r.Paper -- #Id)}</a>
adamc@1030 310 </li></xml>);
adamc@1009 311 return <xml><body>
adamc@1009 312 <h1>All Papers</h1>
adamc@1022 313
adamc@1009 314 <ul>
adamc@1009 315 {ps}
adamc@1009 316 </ul>
adamc@1009 317 </body></xml>
adamc@1009 318
adamc@1022 319 and all () =
adamc@1022 320 checkOnPc;
adamc@1030 321 listPapers (SELECT paper.Id, paper.{{map fst M.paper ++ M.paperPrivate}} FROM paper)
adamc@1022 322
adamc@1022 323 and your () =
adamc@1022 324 me <- getLogin;
adamc@1022 325 listPapers (sql_query {Rows = sql_query1 {Distinct = False,
adamc@1027 326 From = O.joinYourPaper me.Id (sql_from_table [#Paper] paper),
adamc@1022 327 Where = (WHERE TRUE),
adamc@1022 328 GroupBy = sql_subset_all [_],
adamc@1022 329 Having = (WHERE TRUE),
adamc@1030 330 SelectFields = sql_subset [[Paper =
adamc@1030 331 ([Id = _]
adamc@1030 332 ++ map fst M.paper
adamc@1030 333 ++ M.paperPrivate, _)]
adamc@1022 334 ++ map (fn ts => ([], ts))
adamc@1022 335 O.yourPaperTables],
adamc@1022 336 SelectExps = {}},
adamc@1022 337 OrderBy = sql_order_by_Nil [_],
adamc@1022 338 Limit = sql_no_limit,
adamc@1022 339 Offset = sql_no_offset})
adamc@1022 340
adamc@1009 341 and one id =
adamc@1012 342 let
adamc@1012 343 fun newReview r =
adamc@1012 344 me <- getLogin;
adamc@1012 345 checkPaper id;
adamc@1012 346 dml (insert review ({Paper = sql_inject id, User = sql_inject me.Id}
adamc@1012 347 ++ ensql M.review r M.reviewFolder));
adamc@1012 348 one id
adamc@1009 349
adamc@1012 350 fun saveReview r =
adamc@1012 351 me <- getLogin;
adamc@1012 352 checkPaper id;
adamc@1012 353 dml (update [map fst M.review] ! (ensql M.review r M.reviewFolder)
adamc@1012 354 review (WHERE T.Paper = {[id]} AND T.User = {[me.Id]}));
adamc@1012 355 one id
adamc@1012 356 in
adamc@1012 357 me <- getLogin;
adamc@1012 358 checkPaper id;
adamc@1012 359 ro <- oneOrNoRows (SELECT paper.{{map fst M.paper}}, octet_length(paper.Document) AS N
adamc@1012 360 FROM paper
adamc@1012 361 WHERE paper.Id = {[id]});
adamc@1012 362 authors <- queryX (SELECT user.Nam
adamc@1012 363 FROM authorship
adamc@1012 364 JOIN user ON authorship.User = user.Id
adamc@1012 365 WHERE authorship.Paper = {[id]})
adamc@1012 366 (fn r => <xml><li>{[r.User.Nam]}</li></xml>);
adamc@1012 367 myReview <- oneOrNoRows1 (SELECT review.{{map fst M.review}}
adamc@1012 368 FROM review
adamc@1012 369 WHERE review.User = {[me.Id]}
adamc@1012 370 AND review.Paper = {[id]});
adamc@1029 371 otherReviews <- queryX (SELECT user.Nam, review.{{map fst M.review}}
adamc@1029 372 FROM review JOIN user ON review.User = user.Id
adamc@1029 373 WHERE review.Paper = {[id]}
adamc@1029 374 AND review.User <> {[me.Id]})
adamc@1029 375 (fn r => <xml>
adamc@1029 376 <hr/>
adamc@1029 377 <b>User:</b> {[r.User.Nam]}<br/>
adamc@1029 378 {allContent M.review r.Review M.reviewFolder}
adamc@1029 379 </xml>);
adamc@1029 380
adamc@1012 381 case ro of
adamc@1012 382 None => error <xml>Paper not found!</xml>
adamc@1012 383 | Some r => return <xml><body>
adamc@1012 384 <h1>Paper #{[id]}</h1>
adamc@1010 385
adamc@1012 386 <h3>Authors:</h3>
adamc@1012 387 <ul>
adamc@1012 388 {authors}
adamc@1012 389 </ul>
adamc@1009 390
adamc@1012 391 {allContent M.paper r.Paper M.paperFolder}<br/>
adamc@1011 392
adamc@1012 393 {if r.N = 0 then
adamc@1012 394 <xml><div>No paper uploaded yet.</div></xml>
adamc@1012 395 else
adamc@1012 396 <xml><a link={download id}>Download paper</a> ({[r.N]} bytes)</xml>}
adamc@1011 397
adamc@1012 398 <hr/>
adamc@1011 399
adamc@1012 400 {case myReview of
adamc@1012 401 None => <xml>
adamc@1012 402 <h2>Add Your Review</h2>
adamc@1012 403
adamc@1012 404 <form>
adamc@1012 405 {allWidgets M.review M.reviewFolder}
adamc@1012 406 <submit value="Add" action={newReview}/>
adamc@1012 407 </form>
adamc@1012 408 </xml>
adamc@1012 409 | Some myReview => <xml>
adamc@1012 410 <h2>Edit Your Review</h2>
adamc@1012 411
adamc@1012 412 <form>
adamc@1012 413 {allPopulated M.review myReview M.reviewFolder}
adamc@1012 414 <submit value="Save" action={saveReview}/>
adamc@1012 415 </form>
adamc@1012 416 </xml>}
adamc@1029 417
adamc@1029 418 <hr/>
adamc@1029 419 <h2>Other reviews</h2>
adamc@1029 420
adamc@1029 421 {otherReviews}
adamc@1012 422 </body></xml>
adamc@1012 423 end
adamc@1009 424
adamc@1009 425 and download id =
adamc@1009 426 checkPaper id;
adamc@1009 427 ro <- oneOrNoRows (SELECT paper.Document
adamc@1009 428 FROM paper
adamc@1009 429 WHERE paper.Id = {[id]});
adamc@1009 430 case ro of
adamc@1009 431 None => error <xml>Paper not found!</xml>
adamc@1009 432 | Some r => returnBlob r.Paper.Document (blessMime "application/pdf")
adamc@1009 433
adamc@1001 434 end
adamc@1030 435
adamc@1030 436
adamc@1030 437 functor Join(M : sig
adamc@1030 438 structure O1 : OUTPUT
adamc@1030 439
adamc@1030 440 structure O2 : OUTPUT where con paper = O1.paper
adamc@1030 441 where con userId = O1.userId
adamc@1030 442 where con paperId = O1.paperId
adamc@1030 443
adamc@1030 444 constraint O1.yourPaperTables ~ O2.yourPaperTables
adamc@1030 445 end)
adamc@1030 446 = struct
adamc@1030 447 open M
adamc@1030 448 open O1
adamc@1030 449
adamc@1030 450 val linksForPc = <xml>{O1.linksForPc}{O2.linksForPc}</xml>
adamc@1030 451 val linksForChair = <xml>{O1.linksForChair}{O2.linksForChair}</xml>
adamc@1030 452
adamc@1030 453 con yourPaperTables = O1.yourPaperTables ++ O2.yourPaperTables
adamc@1030 454 constraint [Paper] ~ yourPaperTables
adamc@1030 455
adamc@1030 456 fun joinYourPaper [tabs] [paper] [[Paper] ~ tabs] [[Paper] ~ _] [tabs ~ yourPaperTables] [[Id] ~ paper]
adamc@1030 457 uid (fi : sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)) =
adamc@1030 458 O2.joinYourPaper uid (O1.joinYourPaper uid fi)
adamc@1030 459 end