summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-10-31 15:51:50 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-10-31 15:51:50 -0400
commite8ec918ad64bb1008ca7a3184d3e647a62d28404 (patch)
tree83db5727103dd54a22787218cd8325e80059cc96
parente6cdd060b73ad081dd3dab2e278b994e9442c6da (diff)
Start of bidding implementation compiles
-rw-r--r--demo/more/bid.ur34
-rw-r--r--demo/more/bid.urs2
-rw-r--r--demo/more/conference.ur84
-rw-r--r--demo/more/conference.urp1
-rw-r--r--demo/more/conference.urs37
-rw-r--r--demo/more/conference1.ur4
-rw-r--r--src/elaborate.sml1
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