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

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 (2009-11-17)
parents 5d9f47124c4c
children
line wrap: on
line source
signature INPUT = sig
    con paper :: {Type}
    constraint [Id, Document] ~ paper

    type userId
    val userId_inj : sql_injectable_prim userId
    table user : {Id : userId, Nam : string, Password : string, Chair : bool, OnPc : bool}
                     PRIMARY KEY Id,
          CONSTRAINT Nam UNIQUE Nam

    type paperId
    val paperId_inj : sql_injectable_prim paperId
    val paperId_show : show paperId
    val paperId_read : read paperId
    val paperId_eq : eq paperId
    table paper : ([Id = paperId, Document = blob] ++ paper)
                      PRIMARY KEY Id

    con review :: {Type}
    constraint [Paper, User] ~ review
    table review : ([Paper = paperId, User = userId] ++ review)
                       PRIMARY KEY (Paper, User)

    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 checkChair : transaction unit
    val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $paper -> xml ([Body] ++ ctx) [] []
end

signature OUTPUT = sig
    con paper :: {Type}
    type userId
    type paperId

    val linksForPc : xbody
    val linksForChair : xbody

    con yourPaperTables :: {{Type}}
    constraint [Paper] ~ yourPaperTables
    val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type}
        -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] =>
        userId
        -> sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)
        -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs)
end

open Meta

functor Make(M : sig
                 con paper :: {(Type * Type)}
                 constraint [Id, Document, Authors] ~ paper
                 val paper : $(map Meta.meta paper)
                 val paperFolder : folder paper

                 con paperPrivate :: {Type}
                 constraint [Id, Document, Authors] ~ paperPrivate
                 constraint paper ~ paperPrivate
                 val paperPrivate : $(map Meta.private paperPrivate)
                 val paperPrivateFolder : folder paperPrivate

                 con review :: {(Type * Type)}
                 constraint [Paper, User] ~ review
                 val review : $(map Meta.meta review)
                 val reviewFolder : folder review

                 val submissionDeadline : time
                 val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper ++ paperPrivate)
                                                                          -> xml ([Body] ++ ctx) [] []

                 functor Make (M : INPUT where con paper = map fst paper ++ paperPrivate
                                         where con review = map fst review)
                         : OUTPUT where con paper = map fst paper ++ paperPrivate
                                  where con userId = M.userId
                                  where con paperId = M.paperId
             end) = struct

    table user : {Id : int, Nam : string, Password : string, Chair : bool, OnPc : bool}
          PRIMARY KEY Id,
          CONSTRAINT Nam UNIQUE Nam
    sequence userId

    con paper = [Id = int, Document = blob] ++ map fst M.paper ++ M.paperPrivate
    table paper : paper
          PRIMARY KEY Id
    sequence paperId

    table authorship : {Paper : int, User : int}
          PRIMARY KEY (Paper, User),
          CONSTRAINT Paper FOREIGN KEY Paper REFERENCES paper(Id) ON DELETE CASCADE,
          CONSTRAINT User FOREIGN KEY User REFERENCES user(Id)

    con review = [Paper = int, User = int] ++ map fst M.review
    table review : review
          PRIMARY KEY (Paper, User),
          CONSTRAINT Paper FOREIGN KEY Paper REFERENCES paper(Id),
          CONSTRAINT User FOREIGN KEY User REFERENCES user(Id)
    sequence reviewId

    cookie login : {Id : int, Password : string}

    val checkLogin =
        r <- getCookie login;
        case r of
            None => return None
          | Some r =>
            oneOrNoRows1 (SELECT user.Id, user.Nam, user.Chair, user.OnPc
                          FROM user
                          WHERE user.Id = {[r.Id]}
                            AND user.Password = {[r.Password]})

    val getLogin =
        ro <- checkLogin;
        case ro of
            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>

    val checkChair =
        r <- getLogin;
        if r.Chair then
            return ()
        else
            error <xml>You are not a chair.</xml>

    structure O = M.Make(struct
                             val user = user
                             val paper = paper
                             val review = review
                             val checkLogin = checkLogin
                             val getLogin = getLogin
                             val getPcLogin = getPcLogin
                             val checkChair = checkChair
                             val summarizePaper = @@M.summarizePaper
                         end)

    val checkOnPc =
        r <- getLogin;
        if r.OnPc then
            return ()
        else
            error <xml>You aren't authorized to do that.</xml>

    fun checkPaper id =
        r <- getLogin;
        if r.OnPc then
            return ()
        else
            error <xml>You aren't authorized to see that paper.</xml>

    structure Users = BulkEdit.Make(struct
                                        con keyName = #Id
                                        val visible = {Nam = string "Name",
                                                       Chair = bool "Chair?",
                                                       OnPc = bool "On PC?"}

                                        val title = "Users"
                                        val isAllowed =
                                            me <- checkLogin;
                                            return (Option.isSome me)

                                        val t = user
                                    end)

    fun doRegister r =
        n <- oneRowE1 (SELECT COUNT( * ) AS N
                       FROM user
                       WHERE user.Nam = {[r.Nam]});
        if n > 0 then
            register (Some "Sorry; that username is taken.")
        else
            id <- nextval userId;
            dml (INSERT INTO user (Id, Nam, Password, Chair, OnPc)
                 VALUES ({[id]}, {[r.Nam]}, {[r.Password]}, FALSE, FALSE));
            setCookie login {Id = id, Password = r.Password};
            main ()

    and register msg = return <xml><body>
      <h1>Registering a New Account</h1>

      {case msg of
           None => <xml/>
         | Some msg => <xml><div>{[msg]}</div></xml>}

      <form><table>
        <tr> <th>Username:</th> <td><textbox{#Nam}/></td> </tr>
        <tr> <th>Password:</th> <td><password{#Password}/></td> </tr>
        <tr> <th><submit action={doRegister}/></th> </tr>
      </table></form>
    </body></xml>

    and signin r =
        ro <- oneOrNoRowsE1 (SELECT user.Id AS N
                             FROM user
                             WHERE user.Nam = {[r.Nam]}
                               AND user.Password = {[r.Password]});
        (case ro of
             None => return ()
           | Some id => setCookie login {Id = id, Password = r.Password});
        m <- main' ();
        return <xml><body>
          {case ro of
               None => <xml><div>Invalid username or password.</div></xml>
             | _ => <xml/>}

          {m}
        </body></xml>

    and main' () =
        me <- checkLogin;
        now <- now;
        return <xml><ul>
          {case me of
               None => <xml>
                 <li><a link={register None}>Register for access</a></li>
                 <li><b>Log in:</b> <form><table>
                   <tr> <th>Username:</th> <td><textbox{#Nam}/></td> </tr>
                   <tr> <th>Password:</th> <td><password{#Password}/></td> </tr>
                   <tr> <th><submit value="Log in" action={signin}/></th> </tr>
                 </table></form></li>
               </xml>
             | Some me => <xml>
               <div>Welcome, {[me.Nam]}!</div>

               {if me.Chair then
                    <xml>
                      <li><a link={Users.main ()}>Manage users</a></li>
                      {O.linksForChair}
                    </xml>
                else
                    <xml/>}

               {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
                    <xml/>}

               {if now < M.submissionDeadline then
                    <xml><li><a link={submit ()}>Submit</a></li></xml>
                else
                    <xml/>}
             </xml>}
        </ul></xml>

    and main () =
        m <- main' ();
        return <xml><body>{m}</body></xml>

    and submit () =
        let
            fun doSubmit r =
                me <- getLogin;
                coauthors <- List.mapM (fn name => oneOrNoRowsE1 (SELECT user.Id AS N
                                                                  FROM user
                                                                  WHERE user.Nam = {[name.Nam]})) r.Authors;
                if List.exists Option.isNone coauthors then
                    error <xml>At least one of those coauthor usernames isn't registered.</xml>
                else
                    id <- nextval paperId;
                    dml (insert paper ({Id = sql_inject id, Document = sql_inject (fileData r.Document)}
                                           ++ ensql M.paper (r -- #Authors -- #Document) M.paperFolder
                                           ++ initialize M.paperPrivate M.paperPrivateFolder));
                    List.app (fn uid =>
                                 case uid of
                                     None => error <xml>Impossible empty uid!</xml>
                                   | Some uid => dml (INSERT INTO authorship (Paper, User)
                                                      VALUES ({[id]}, {[uid]})))
                             (Some me.Id :: coauthors);
                    return <xml><body>
                      Thanks for submitting!
                    </body></xml>
        in
            me <- getLogin;
            numAuthors <- Dnat.zero;

            return <xml><body>
              <h1>Submit a Paper</h1>
              
              <form>
                <b>Author:</b> {[me.Nam]}<br/>
                <subforms{#Authors}>
                  {Dnat.render <xml><entry><b>Author:</b> <textbox{#Nam}/><br/></entry></xml> numAuthors}
                </subforms>
                <button value="Add author" onclick={Dnat.inc numAuthors}/><br/>
                <button value="Remove author" onclick={Dnat.dec numAuthors}/><br/>
                <br/>

                {useMore (allWidgets M.paper M.paperFolder)}
                <b>Paper:</b> <upload{#Document}/><br/>
                <submit value="Submit" action={doSubmit}/>
              </form>
            </body></xml>
        end

    and listPapers [tabs] [[Paper] ~ tabs]
                   (q : sql_query ([Paper = [Id = int] ++ map fst M.paper ++ M.paperPrivate] ++ tabs) []) =
        checkOnPc;
        ps <- queryX q
                     (fn r => <xml><li><a link={one r.Paper.Id}>{M.summarizePaper (r.Paper -- #Id)}</a>
                     </li></xml>);
        return <xml><body>
          <h1>All Papers</h1>
          
          <ul>
            {ps}
          </ul>
        </body></xml>

    and all () =
        checkOnPc;
        listPapers (SELECT paper.Id, paper.{{map fst M.paper ++ M.paperPrivate}} FROM paper)

    and your () =
        me <- getLogin;
        listPapers (sql_query {Rows = sql_query1 {Distinct = False,
                                                  From = O.joinYourPaper me.Id (sql_from_table [#Paper] paper),
                                                  Where = (WHERE TRUE),
                                                  GroupBy = sql_subset_all [_],
                                                  Having = (WHERE TRUE),
                                                  SelectFields = sql_subset [[Paper =
                                                                              ([Id = _]
                                                                                   ++ map fst M.paper
                                                                                   ++ M.paperPrivate, _)]
                                                                                 ++ map (fn ts => ([], ts))
                                                                                            O.yourPaperTables],
                                                  SelectExps = {}},
                               OrderBy = sql_order_by_Nil [_],
                               Limit = sql_no_limit,
                               Offset = sql_no_offset})

    and one id =
        let
            fun newReview r =
                me <- getLogin;
                checkPaper id;
                dml (insert review ({Paper = sql_inject id, User = sql_inject me.Id}
                                        ++ ensql M.review r M.reviewFolder));
                one id

            fun saveReview r =
                me <- getLogin;
                checkPaper id;
                dml (update [map fst M.review] ! (ensql M.review r M.reviewFolder)
                            review (WHERE T.Paper = {[id]} AND T.User = {[me.Id]}));
                one id
        in
            me <- getLogin;
            checkPaper id;
            ro <- oneOrNoRows (SELECT paper.{{map fst M.paper}}, octet_length(paper.Document) AS N
                               FROM paper
                               WHERE paper.Id = {[id]});
            authors <- queryX (SELECT user.Nam
                               FROM authorship
                                 JOIN user ON authorship.User = user.Id
                               WHERE authorship.Paper = {[id]})
                              (fn r => <xml><li>{[r.User.Nam]}</li></xml>);
            myReview <- oneOrNoRows1 (SELECT review.{{map fst M.review}}
                                      FROM review
                                      WHERE review.User = {[me.Id]}
                                        AND review.Paper = {[id]});
            otherReviews <- queryX (SELECT user.Nam, review.{{map fst M.review}}
                                    FROM review JOIN user ON review.User = user.Id
                                    WHERE review.Paper = {[id]}
                                      AND review.User <> {[me.Id]})
                            (fn r => <xml>
                              <hr/>
                              <b>User:</b> {[r.User.Nam]}<br/>
                              {allContent M.review r.Review M.reviewFolder}
                            </xml>);

            case ro of
                None => error <xml>Paper not found!</xml>
              | Some r => return <xml><body>
                <h1>Paper #{[id]}</h1>

                <h3>Authors:</h3>
                <ul>
                  {authors}
                </ul>

                {allContent M.paper r.Paper M.paperFolder}<br/>

                {if r.N = 0 then
                     <xml><div>No paper uploaded yet.</div></xml>
                 else
                     <xml><a link={download id}>Download paper</a> ({[r.N]} bytes)</xml>}

                <hr/>

                {case myReview of
                     None => <xml>
                       <h2>Add Your Review</h2>
                       
                       <form>
                         {allWidgets M.review M.reviewFolder}
                         <submit value="Add" action={newReview}/>
                       </form>
                     </xml>
                   | Some myReview => <xml>
                     <h2>Edit Your Review</h2>

                     <form>
                       {allPopulated M.review myReview M.reviewFolder}
                       <submit value="Save" action={saveReview}/>
                     </form>
                   </xml>}

                <hr/>
                <h2>Other reviews</h2>

                {otherReviews}
              </body></xml>
        end

    and download id =
        checkPaper id;
        ro <- oneOrNoRows (SELECT paper.Document
                           FROM paper
                           WHERE paper.Id = {[id]});
        case ro of
            None => error <xml>Paper not found!</xml>
          | Some r => returnBlob r.Paper.Document (blessMime "application/pdf")

end


functor Join(M : sig
                 structure O1 : OUTPUT

                 structure O2 : OUTPUT where con paper = O1.paper
                                       where con userId = O1.userId
                                       where con paperId = O1.paperId

                 constraint O1.yourPaperTables ~ O2.yourPaperTables
             end)
        = struct
            open M
            open O1

            val linksForPc = <xml>{O1.linksForPc}{O2.linksForPc}</xml>
            val linksForChair = <xml>{O1.linksForChair}{O2.linksForChair}</xml>

            con yourPaperTables = O1.yourPaperTables ++ O2.yourPaperTables
            constraint [Paper] ~ yourPaperTables

            fun joinYourPaper [tabs] [paper] [[Paper] ~ tabs] [[Paper] ~ _] [tabs ~ yourPaperTables] [[Id] ~ paper]
                              uid (fi : sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)) =
                O2.joinYourPaper uid (O1.joinYourPaper uid fi)
        end