summaryrefslogtreecommitdiff
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-11-01 14:26:20 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-11-01 14:26:20 -0500
commit7560a81cd846d47d3d4d642cc470e3b09c5e1826 (patch)
tree554465c7355d6fe0d310a16f4a7fa5a4e0675870 /demo
parent1beaf9527c0b6ab4b2f06267966e9e89a26550ff (diff)
Initial form for paper assignment
Diffstat (limited to 'demo')
-rw-r--r--demo/more/bid.ur92
-rw-r--r--demo/more/checkGroup.ur15
-rw-r--r--demo/more/checkGroup.urs5
-rw-r--r--demo/more/conference.ur16
-rw-r--r--demo/more/conference.urp2
-rw-r--r--demo/more/conference.urs3
-rw-r--r--demo/more/expandable.ur23
-rw-r--r--demo/more/expandable.urs6
8 files changed, 151 insertions, 11 deletions
diff --git a/demo/more/bid.ur b/demo/more/bid.ur
index 692f8e14..931fc9c0 100644
--- a/demo/more/bid.ur
+++ b/demo/more/bid.ur
@@ -7,6 +7,79 @@ functor Make(M : Conference.INPUT) = struct
table assignment : {User : userId, Paper : paperId}
PRIMARY KEY (User, Paper)
+ fun intOut ch =
+ case ch of
+ #"_" => "Maybe"
+ | #"-" => "No"
+ | #"+" => "Yes"
+ | _ => error <xml>Bid: Invalid Interest code</xml>
+
+ val linksForChair =
+ let
+ fun assignPapers () =
+ tup <- query (SELECT paper.Id, paper.{{M.paper}}, user.Id, user.Nam, bid.Interest
+ FROM paper JOIN bid ON bid.Paper = paper.Id
+ JOIN user ON bid.User = user.Id
+ ORDER BY paper.Id, bid.Interest, user.Nam)
+ (fn r (pid, int, acc, ints, papers) =>
+ if pid = Some r.Paper.Id then
+ if int = r.Bid.Interest then
+ return (pid, int, (r.User.Id, r.User.Nam) :: acc, ints, papers)
+ else
+ return (pid, r.Bid.Interest, (r.User.Id, r.User.Nam) :: [],
+ (int, acc) :: ints, papers)
+ else
+ return (Some r.Paper.Id, r.Bid.Interest,
+ (r.User.Id, r.User.Nam) :: [], [],
+ case pid of
+ None => papers
+ | Some pid => (pid, (int, acc) :: ints) :: papers))
+ (None, #" ", [], [], []);
+ let
+ val papersL = case tup.1 of
+ Some pid => (pid, (tup.2, tup.3) :: tup.4) :: tup.5
+ | _ => []
+
+ fun makePapers () = List.mapM (fn (pid, ints) =>
+ ints <- List.mapM (fn (int, users) =>
+ cg <- CheckGroup.create
+ (List.mp
+ (fn (id, nam) => (id, txt nam,
+ False))
+ users);
+ ex <- Expandable.create
+ (CheckGroup.render cg);
+ return (int, cg, ex)) ints;
+ return (pid, ints)) papersL
+ in
+ papers <- source [];
+
+ return <xml><body onload={papersL <- makePapers ();
+ set papers papersL}>
+ <h1>Assign papers</h1>
+
+ <dyn signal={papers <- signal papers;
+ return (List.mapX (fn (pid, ints) => <xml>
+ <hr/>
+ Paper #{[pid]}:
+ <dyn signal={n <- List.foldl (fn (_, cg, _) total =>
+ this <- CheckGroup.selected cg;
+ total <- total;
+ return (List.length this + total)) (return 0) ints;
+ return (txt n)}/><br/>
+
+ {List.mapX (fn (int, _, ex) => <xml>
+ {[intOut int]}: {Expandable.render ex}
+ </xml>) ints}
+ </xml>) papers)}/>
+ </body></xml>
+ end
+ in
+ <xml>
+ <li><a link={assignPapers ()}> Assign papers to people</a></li>
+ </xml>
+ end
+
val linksForPc =
let
fun yourBids () =
@@ -14,16 +87,15 @@ functor Make(M : Conference.INPUT) = struct
ps <- queryX (SELECT paper.Id, paper.{{M.paper}}, bid.Interest
FROM paper LEFT JOIN bid ON bid.Paper = paper.Id
AND bid.User = {[me.Id]})
- (fn r => <xml><entry>
- <hidden{#Paper} value={show r.Paper.Id}/>
- {useMore <xml><tr>
- <td>{summarizePaper (r.Paper -- #Id)}</td>
- <td><select{#Bid}>
- {Select.selectChar ((#"-", "No") :: (#"_", "Maybe") :: (#"+", "Yes") :: [])
- r.Bid.Interest}
- </select></td>
- </tr></xml>}
- </entry></xml>);
+ (fn r => <xml><tr>
+ <td>{useMore (summarizePaper (r.Paper -- #Id))}</td>
+ <td><entry>
+ <hidden{#Paper} value={show r.Paper.Id}/>
+ <select{#Bid}>
+ {useMore (Select.selectChar ((#"-", "No") :: (#"_", "Maybe") :: (#"+", "Yes") :: [])
+ r.Bid.Interest)}
+ </select></entry></td>
+ </tr></xml>);
return <xml><body>
<h1>Bid on papers</h1>
diff --git a/demo/more/checkGroup.ur b/demo/more/checkGroup.ur
new file mode 100644
index 00000000..ab1cc781
--- /dev/null
+++ b/demo/more/checkGroup.ur
@@ -0,0 +1,15 @@
+con t ctx data = list (data * xml ctx [] [] * source bool)
+
+fun create [ctx] [data] (items : list (data * xml ctx [] [] * bool)) =
+ List.mapM (fn (d, x, b) => s <- source b; return (d, x, s)) items
+
+fun render [ctx] [data] [[Body] ~ ctx] (t : t ([Body] ++ ctx) data) =
+ List.mapX (fn (_, x, s) => <xml><ccheckbox source={s}/> {x}<br/></xml>) t
+
+fun selected [ctx] [data] (t : t ctx data) =
+ List.foldlM (fn (d, _, s) ls =>
+ s <- signal s;
+ return (if s then
+ d :: ls
+ else
+ ls)) [] t
diff --git a/demo/more/checkGroup.urs b/demo/more/checkGroup.urs
new file mode 100644
index 00000000..d448527e
--- /dev/null
+++ b/demo/more/checkGroup.urs
@@ -0,0 +1,5 @@
+con t :: {Unit} -> Type -> Type
+
+val create : ctx ::: {Unit} -> data ::: Type -> list (data * xml ctx [] [] * bool) -> transaction (t ctx data)
+val render : ctx ::: {Unit} -> data ::: Type -> [[Body] ~ ctx] => t ([Body] ++ ctx) data -> xml ([Body] ++ ctx) [] []
+val selected : ctx ::: {Unit} -> data ::: Type -> t ctx data -> signal (list data)
diff --git a/demo/more/conference.ur b/demo/more/conference.ur
index e810043b..7b3d3d71 100644
--- a/demo/more/conference.ur
+++ b/demo/more/conference.ur
@@ -12,12 +12,14 @@ signature INPUT = sig
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
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
@@ -27,6 +29,7 @@ signature OUTPUT = sig
type paperId
val linksForPc : xbody
+ val linksForChair : xbody
con yourPaperTables :: {{Type}}
constraint [Paper] ~ yourPaperTables
@@ -105,12 +108,20 @@ functor Make(M : sig
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 checkLogin = checkLogin
val getLogin = getLogin
val getPcLogin = getPcLogin
+ val checkChair = checkChair
val summarizePaper = @@M.summarizePaper
end)
@@ -203,7 +214,10 @@ functor Make(M : sig
<div>Welcome, {[me.Nam]}!</div>
{if me.Chair then
- <xml><li><a link={Users.main ()}>Manage users</a></li></xml>
+ <xml>
+ <li><a link={Users.main ()}>Manage users</a></li>
+ {O.linksForChair}
+ </xml>
else
<xml/>}
diff --git a/demo/more/conference.urp b/demo/more/conference.urp
index 844baed9..9e0d8eaa 100644
--- a/demo/more/conference.urp
+++ b/demo/more/conference.urp
@@ -9,4 +9,6 @@ dnat
conference
conferenceFields
select
+checkGroup
+expandable
bid
diff --git a/demo/more/conference.urs b/demo/more/conference.urs
index f9729851..2f24bac8 100644
--- a/demo/more/conference.urs
+++ b/demo/more/conference.urs
@@ -12,12 +12,14 @@ signature INPUT = sig
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
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
@@ -27,6 +29,7 @@ signature OUTPUT = sig
type paperId
val linksForPc : xbody
+ val linksForChair : xbody
con yourPaperTables :: {{Type}}
constraint [Paper] ~ yourPaperTables
diff --git a/demo/more/expandable.ur b/demo/more/expandable.ur
new file mode 100644
index 00000000..92d8743c
--- /dev/null
+++ b/demo/more/expandable.ur
@@ -0,0 +1,23 @@
+con t ctx = source bool * xml ctx [] []
+
+fun create [ctx] (x : xml ctx [] []) =
+ s <- source False;
+ return (s, x)
+
+fun expand [ctx] (t : t ctx) =
+ set t.1 True
+
+fun collapse [ctx] (t : t ctx) =
+ set t.1 False
+
+fun render [ctx] [[Body] ~ ctx] (t : t ([Body] ++ ctx)) =
+ <xml><dyn signal={b <- signal t.1;
+ return (if b then
+ <xml>
+ <button value="-" onclick={collapse t}/><br/>
+ {t.2}
+ </xml>
+ else
+ <xml>
+ <button value="+" onclick={expand t}/><br/>
+ </xml>)}/></xml>
diff --git a/demo/more/expandable.urs b/demo/more/expandable.urs
new file mode 100644
index 00000000..820b89b7
--- /dev/null
+++ b/demo/more/expandable.urs
@@ -0,0 +1,6 @@
+con t :: {Unit} -> Type
+
+val create : ctx ::: {Unit} -> xml ctx [] [] -> transaction (t ctx)
+val render : ctx ::: {Unit} -> [[Body] ~ ctx] => t ([Body] ++ ctx) -> xml ([Body] ++ ctx) [] []
+val expand : ctx ::: {Unit} -> t ctx -> transaction unit
+val collapse : ctx ::: {Unit} -> t ctx -> transaction unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 00:36:52 +0000