Mercurial > urweb

annotate demo/more/conference.ur @ 1228:7dfa67560916

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Using multiple policies to check a written value
author Adam Chlipala <adamc@hcoop.net>
date Sun, 11 Apr 2010 16:46:38 -0400
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