diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-10-31 15:51:50 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-10-31 15:51:50 -0400 |
commit | e8ec918ad64bb1008ca7a3184d3e647a62d28404 (patch) | |
tree | 83db5727103dd54a22787218cd8325e80059cc96 | |
parent | e6cdd060b73ad081dd3dab2e278b994e9442c6da (diff) |
Start of bidding implementation compiles
-rw-r--r-- | demo/more/bid.ur | 34 | ||||
-rw-r--r-- | demo/more/bid.urs | 2 | ||||
-rw-r--r-- | demo/more/conference.ur | 84 | ||||
-rw-r--r-- | demo/more/conference.urp | 1 | ||||
-rw-r--r-- | demo/more/conference.urs | 37 | ||||
-rw-r--r-- | demo/more/conference1.ur | 4 | ||||
-rw-r--r-- | src/elaborate.sml | 1 |
7 files changed, 158 insertions, 5 deletions
diff --git a/demo/more/bid.ur b/demo/more/bid.ur new file mode 100644 index 00000000..5bcaea3a --- /dev/null +++ b/demo/more/bid.ur @@ -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 diff --git a/demo/more/bid.urs b/demo/more/bid.urs new file mode 100644 index 00000000..976d1ab6 --- /dev/null +++ b/demo/more/bid.urs @@ -0,0 +1,2 @@ +functor Make (M : Conference.INPUT) : Conference.OUTPUT where con userId = M.userId + where con paperId = M.paperId diff --git a/demo/more/conference.ur b/demo/more/conference.ur index 0488d52e..a80f1ab1 100644 --- a/demo/more/conference.ur +++ b/demo/more/conference.ur @@ -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 @@ functor Make(M : sig 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 @@ functor Make(M : sig 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 @@ functor Make(M : sig <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 @@ functor Make(M : sig </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 = diff --git a/demo/more/conference.urp b/demo/more/conference.urp index 14181554..3bc9156c 100644 --- a/demo/more/conference.urp +++ b/demo/more/conference.urp @@ -8,3 +8,4 @@ bulkEdit dnat conference conferenceFields +bid diff --git a/demo/more/conference.urs b/demo/more/conference.urs index 53fd478d..226e9768 100644 --- a/demo/more/conference.urs +++ b/demo/more/conference.urs @@ -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 @@ functor Make(M : sig 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 diff --git a/demo/more/conference1.ur b/demo/more/conference1.ur index 4cf2ae92..c51904e5 100644 --- a/demo/more/conference1.ur +++ b/demo/more/conference1.ur @@ -8,4 +8,8 @@ open Conference.Make(struct 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) diff --git a/src/elaborate.sml b/src/elaborate.sml index b46c262e..f13f6f1d 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -3418,6 +3418,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = 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 |