Mercurial > urweb
changeset 1022:4de35df3d545
Start of bidding implementation compiles
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 31 Oct 2009 15:51:50 -0400 |
parents | 7a4a55e05081 |
children | e46227efcbba |
files | demo/more/bid.ur demo/more/bid.urs demo/more/conference.ur demo/more/conference.urp demo/more/conference.urs demo/more/conference1.ur src/elaborate.sml |
diffstat | 7 files changed, 158 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/more/bid.ur Sat Oct 31 15:51:50 2009 -0400 @@ -0,0 +1,34 @@ +functor Make(M : Conference.INPUT) = struct + open M + + table bid : {User : userId, Paper : paperId, Interest : char} + PRIMARY KEY (User, Paper) + + table assignment : {User : userId, Paper : paperId} + PRIMARY KEY (User, Paper) + + fun isOnPc id = + ro <- oneOrNoRows1 (SELECT user.OnPc + FROM user + WHERE user.Id = {[id]}); + return (case ro of + None => False + | Some r => r.OnPc) + + val linksForPc = + let + fun bid () = + me <- getLogin; + return <xml>Bidding time!</xml> + in + <xml> + <li> <a link={bid ()}>Bid on papers</a></li> + </xml> + end + + con yourPaperTables = [Assignment = _] + constraint [Paper] ~ yourPaperTables + fun joinYourPaper [tabs] [paper] [[Paper] ~ tabs] [[Paper] ~ _] [tabs ~ yourPaperTables] [[Id] ~ paper] + (fi : sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)) = + sql_inner_join fi (sql_from_table [#Assignment] assignment) (WHERE Paper.Id = Assignment.Paper) +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/more/bid.urs Sat Oct 31 15:51:50 2009 -0400 @@ -0,0 +1,2 @@ +functor Make (M : Conference.INPUT) : Conference.OUTPUT where con userId = M.userId + where con paperId = M.paperId
--- a/demo/more/conference.ur Sun Oct 25 15:29:21 2009 -0400 +++ b/demo/more/conference.ur Sat Oct 31 15:51:50 2009 -0400 @@ -1,3 +1,36 @@ +signature INPUT = sig + con paper :: {(Type * 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 + table paper : ([Id = paperId, Document = blob] ++ map fst 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} +end + +signature OUTPUT = sig + type userId + type paperId + + val linksForPc : xbody + + con yourPaperTables :: {{Type}} + constraint [Paper] ~ yourPaperTables + val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type} + -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] => + sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs) + -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs) +end + open Meta functor Make(M : sig @@ -13,6 +46,10 @@ val submissionDeadline : time val summarizePaper : $(map fst paper) -> xbody + + functor Make (M : INPUT where con paper = paper) + : OUTPUT where con userId = M.userId + where con paperId = M.paperId end) = struct table user : {Id : int, Nam : string, Password : string, Chair : bool, OnPc : bool} @@ -55,6 +92,20 @@ None => error <xml>You must be logged in to do that.</xml> | Some r => return r + structure O = M.Make(struct + val user = user + val paper = paper + val checkLogin = checkLogin + val getLogin = getLogin + 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 @@ -142,7 +193,10 @@ <xml/>} {if me.OnPc then - <xml><li><a link={all ()}>All papers</a></li></xml> + <xml> + <li><a link={all ()}>All papers</a></li> + {O.linksForPc} + </xml> else <xml/>} @@ -202,17 +256,37 @@ </body></xml> end - and all () = - ps <- queryX (SELECT paper.Id, paper.{{map fst M.paper}} FROM paper) - (fn r => <xml><li><a link={one r.Paper.Id}>{M.summarizePaper (r.Paper -- #Id)}</a></li></xml>); + and listPapers [tabs] [[Paper] ~ tabs] (q : sql_query ([Paper = [Id = int] ++ map fst M.paper] ++ 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}} FROM paper) + + and your () = + me <- getLogin; + listPapers (sql_query {Rows = sql_query1 {Distinct = False, + From = O.joinYourPaper (sql_from_table [#Paper] paper), + Where = (WHERE TRUE), + GroupBy = sql_subset_all [_], + Having = (WHERE TRUE), + SelectFields = sql_subset [[Paper = ([Id = _] ++ map fst M.paper, _)] + ++ 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 =
--- a/demo/more/conference.urp Sun Oct 25 15:29:21 2009 -0400 +++ b/demo/more/conference.urp Sat Oct 31 15:51:50 2009 -0400 @@ -8,3 +8,4 @@ dnat conference conferenceFields +bid
--- a/demo/more/conference.urs Sun Oct 25 15:29:21 2009 -0400 +++ b/demo/more/conference.urs Sat Oct 31 15:51:50 2009 -0400 @@ -1,3 +1,36 @@ +signature INPUT = sig + con paper :: {(Type * 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 + table paper : ([Id = paperId, Document = blob] ++ map fst 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} +end + +signature OUTPUT = sig + type userId + type paperId + + val linksForPc : xbody + + con yourPaperTables :: {{Type}} + constraint [Paper] ~ yourPaperTables + val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type} + -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] => + sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs) + -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs) +end + functor Make(M : sig con paper :: {(Type * Type)} constraint [Id, Document, Authors] ~ paper @@ -11,6 +44,10 @@ val submissionDeadline : time val summarizePaper : $(map fst paper) -> xbody + + functor Make (M : INPUT where con paper = paper) + : OUTPUT where con userId = M.userId + where con paperId = M.paperId end) : sig val main : unit -> transaction page
--- a/demo/more/conference1.ur Sun Oct 25 15:29:21 2009 -0400 +++ b/demo/more/conference1.ur Sat Oct 31 15:51:50 2009 -0400 @@ -8,4 +8,8 @@ val submissionDeadline = readError "2009-11-22 23:59:59" fun summarizePaper r = cdata r.Title + + functor Make (M : Conference.INPUT where con paper = _) = struct + open Bid.Make(M) + end end)
--- a/src/elaborate.sml Sun Oct 25 15:29:21 2009 -0400 +++ b/src/elaborate.sml Sat Oct 31 15:51:50 2009 -0400 @@ -3418,6 +3418,7 @@ val denv' = case #1 str' of L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []} + | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []} | _ => denv in case #1 (hnormSgn env sgn') of