From 70da89d392d5c9649157e53944db9a49d2149da3 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 1 Nov 2009 14:26:20 -0500 Subject: Initial form for paper assignment --- demo/more/bid.ur | 92 ++++++++++++++++++++++++++++++++++++++++++------ demo/more/checkGroup.ur | 15 ++++++++ demo/more/checkGroup.urs | 5 +++ demo/more/conference.ur | 16 ++++++++- demo/more/conference.urp | 2 ++ demo/more/conference.urs | 3 ++ demo/more/expandable.ur | 23 ++++++++++++ demo/more/expandable.urs | 6 ++++ 8 files changed, 151 insertions(+), 11 deletions(-) create mode 100644 demo/more/checkGroup.ur create mode 100644 demo/more/checkGroup.urs create mode 100644 demo/more/expandable.ur create mode 100644 demo/more/expandable.urs (limited to 'demo/more') 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 Bid: Invalid Interest code + + 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 +

Assign papers

+ + +

+ Paper #{[pid]}: + + this <- CheckGroup.selected cg; + total <- total; + return (List.length this + total)) (return 0) ints; + return (txt n)}/>
+ + {List.mapX (fn (int, _, ex) => + {[intOut int]}: {Expandable.render ex} + ) ints} + ) papers)}/> + + end + in + +

Assign papers to people

+ + 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 => - - {useMore - {summarizePaper (r.Paper -- #Id)} - - {Select.selectChar ((#"-", "No") :: (#"_", "Maybe") :: (#"+", "Yes") :: []) - r.Bid.Interest} - - } - ); + (fn r => + {useMore (summarizePaper (r.Paper -- #Id))} + + + + {useMore (Select.selectChar ((#"-", "No") :: (#"_", "Maybe") :: (#"+", "Yes") :: []) + r.Bid.Interest)} + + ); return

Bid on papers

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) => {x}
) 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 You are not on the PC. + val checkChair = + r <- getLogin; + if r.Chair then + return () + else + error You are not a chair. + 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

Welcome, {[me.Nam]}!

{if me.Chair then -

Manage users

+ +

Manage users

+ {O.linksForChair} + else } 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)) = + +