Mercurial > urweb
changeset 1354:1b286f2309bc
Fix manual mistake about '@' notations; remove obsolete demos
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 20 Dec 2010 19:28:41 -0500 |
| parents | e9cf053108ed |
| children | ccf1d445b794 |
| files | demo/more/bid.ur demo/more/bid.urs demo/more/bulkEdit.ur demo/more/bulkEdit.urs demo/more/checkGroup.ur demo/more/checkGroup.urs demo/more/conference.ur demo/more/conference.urp demo/more/conference.urs demo/more/conference1.ur demo/more/conference1.urp demo/more/conferenceFields.ur demo/more/conferenceFields.urs demo/more/decision.ur demo/more/decision.urs demo/more/dnat.ur demo/more/dnat.urs demo/more/expandable.ur demo/more/expandable.urs demo/more/meta.ur demo/more/meta.urs demo/more/select.ur demo/more/select.urs doc/manual.tex |
| diffstat | 24 files changed, 1 insertions(+), 1195 deletions(-) [+] |
line wrap: on
line diff
--- a/demo/more/bid.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,158 +0,0 @@ -con fields userId paperId = [User = userId, Paper = paperId] - -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 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, assignment.User - FROM paper JOIN bid ON bid.Paper = paper.Id - JOIN user ON bid.User = user.Id - LEFT JOIN assignment ON assignment.Paper = paper.Id AND assignment.User = user.Id - ORDER BY paper.Id, bid.Interest, user.Nam) - (fn r (paper, int, acc, ints, papers) => - if (case paper of None => False | Some r' => r'.Id = r.Paper.Id) then - if int = r.Bid.Interest then - return (paper, int, (r.User.Id, r.User.Nam, Option.isSome r.Assignment.User) :: acc, - ints, papers) - else - return (paper, r.Bid.Interest, (r.User.Id, r.User.Nam, - Option.isSome r.Assignment.User) :: [], - (int, acc) :: ints, papers) - else - return (Some r.Paper, r.Bid.Interest, - (r.User.Id, r.User.Nam, Option.isSome r.Assignment.User) :: [], [], - case paper of - None => papers - | Some r => (r.Id, r -- #Id, (int, acc) :: ints) :: papers)) - (None, #" ", [], [], []); - let - val papersL = case tup.1 of - Some r => (r.Id, r -- #Id, (tup.2, tup.3) :: tup.4) :: tup.5 - | None => [] - - fun makePapers () = List.mapM (fn (pid, extra, ints) => - ints <- List.mapM (fn (int, users) => - cg <- CheckGroup.create - (List.mp - (fn (id, nam, sel) => - (id, txt nam, sel)) - users); - ex <- Expandable.create - (CheckGroup.render cg); - return (int, cg, ex)) ints; - return (pid, extra, ints)) papersL - - fun saveAssignment ls = - dml (DELETE FROM assignment WHERE TRUE); - List.app (fn (pid, uids) => - List.app (fn uid => dml (INSERT INTO assignment (Paper, User) - VALUES ({[pid]}, {[uid]}))) uids) ls - 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, extra, ints) => <xml> - <hr/> - #{[pid]}: {summarizePaper extra}: - <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)}/> - - <br/> - <button value="Save" onclick={papers <- get papers; - ls <- List.mapM (fn (pid, _, ints) => - ints <- List.mapM (fn (_, cg, _) => - current - (CheckGroup.selected cg)) - ints; - return (pid, List.foldl List.append [] ints)) - papers; - rpc (saveAssignment ls)}/> - </body></xml> - end - in - <xml> - <li><a link={assignPapers ()}> Assign papers to people</a></li> - </xml> - end - - val linksForPc = - let - fun yourBids () = - me <- getPcLogin; - 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><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> - - <form> - <subforms{#Papers}><table> - <tr> <th>Paper</th> <th>Your Bid</th> </tr> - {ps} - </table></subforms> - <submit value="Change" action={changeBids}/> - </form> - </body></xml> - - and changeBids r = - me <- getPcLogin; - List.app (fn {Paper = p, Bid = b} => - case b of - "" => return () - | _ => let - val p = readError p - in - (dml (DELETE FROM bid WHERE Paper = {[p]} AND User = {[me.Id]}); - dml (INSERT INTO bid (Paper, User, Interest) - VALUES ({[p]}, {[me.Id]}, {[String.sub b 0]}))) - end) r.Papers; - yourBids () - in - <xml> - <li> <a link={yourBids ()}>Bid on papers</a></li> - </xml> - end - - con yourPaperTables = [Assignment = _] - constraint [Paper] ~ yourPaperTables - fun joinYourPaper [tabs] [paper] [[Paper] ~ tabs] [[Paper] ~ _] [tabs ~ yourPaperTables] [[Id] ~ paper] - (uid : userId) (fi : sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)) = - sql_inner_join fi (sql_from_table [#Assignment] assignment) - (WHERE Paper.Id = Assignment.Paper AND Assignment.User = {[uid]}) -end
--- a/demo/more/bid.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -con fields :: Type -> Type -> {Type} - -functor Make (M : Conference.INPUT) : Conference.OUTPUT where con paper = M.paper - where con userId = M.userId - where con paperId = M.paperId - where con yourPaperTables = [Assignment - = fields M.userId M.paperId]
--- a/demo/more/bulkEdit.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,52 +0,0 @@ -open Meta - -functor Make(M : sig - con keyName :: Name - con keyType :: Type - val showKey : show keyType - val readKey : read keyType - val injKey : sql_injectable keyType - - con visible :: {(Type * Type)} - constraint [keyName] ~ visible - val folder : folder visible - val visible : $(map Meta.meta visible) - - con invisible :: {Type} - constraint [keyName] ~ invisible - constraint visible ~ invisible - - val title : string - val isAllowed : transaction bool - table t : ([keyName = keyType] ++ map fst visible ++ invisible) - end) = struct - - open M - - fun main () = - items <- queryX (SELECT t.{keyName}, t.{{map fst visible}} FROM t) - (fn r => <xml><entry><tr> - <hidden{keyName} value={show r.T.keyName}/> - {useMore (allPopulatedTr visible (r.T -- keyName) folder)} - </tr></entry></xml>); - - return <xml><body> - <h1>{[title]}</h1> - - <form><table> - <tr>{foldRX [meta] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m => - <xml><th>{[m.Nam]}</th></xml>) [_] folder visible}</tr> - <subforms{#Users}>{items}</subforms> - <tr> <td><submit value="Save" action={save}/></td> </tr> - </table></form> - </body></xml> - - and save r = - List.app (fn user => dml (update [map fst visible] ! - (ensql visible (user -- keyName) folder) - t - (WHERE t.{keyName} = {[readError user.keyName]}))) r.Users; - main () - -end
--- a/demo/more/bulkEdit.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -functor Make(M : sig - con keyName :: Name - con keyType :: Type - val showKey : show keyType - val readKey : read keyType - val injKey : sql_injectable keyType - - con visible :: {(Type * Type)} - constraint [keyName] ~ visible - val folder : folder visible - val visible : $(map Meta.meta visible) - - con invisible :: {Type} - constraint [keyName] ~ invisible - constraint visible ~ invisible - - val title : string - val isAllowed : transaction bool - table t : ([keyName = keyType] ++ map fst visible ++ invisible) - end) : sig - - val main : unit -> transaction page - -end
--- a/demo/more/checkGroup.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -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
--- a/demo/more/checkGroup.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -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)
--- a/demo/more/conference.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,459 +0,0 @@ -signature INPUT = sig - con paper :: {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 - 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 - - con review :: {Type} - constraint [Paper, User] ~ review - table review : ([Paper = paperId, User = userId] ++ review) - PRIMARY KEY (Paper, User) - - 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 - -signature OUTPUT = sig - con paper :: {Type} - type userId - type paperId - - val linksForPc : xbody - val linksForChair : xbody - - con yourPaperTables :: {{Type}} - constraint [Paper] ~ yourPaperTables - val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type} - -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] => - userId - -> sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs) - -> sql_from_items (yourPaperTables ++ [Paper = [Id = paperId] ++ paper] ++ tabs) -end - -open Meta - -functor Make(M : sig - con paper :: {(Type * Type)} - constraint [Id, Document, Authors] ~ paper - val paper : $(map Meta.meta paper) - val paperFolder : folder paper - - con paperPrivate :: {Type} - constraint [Id, Document, Authors] ~ paperPrivate - constraint paper ~ paperPrivate - val paperPrivate : $(map Meta.private paperPrivate) - val paperPrivateFolder : folder paperPrivate - - con review :: {(Type * Type)} - constraint [Paper, User] ~ review - val review : $(map Meta.meta review) - val reviewFolder : folder review - - val submissionDeadline : time - val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper ++ paperPrivate) - -> xml ([Body] ++ ctx) [] [] - - functor Make (M : INPUT where con paper = map fst paper ++ paperPrivate - where con review = map fst review) - : OUTPUT where con paper = map fst paper ++ paperPrivate - where con userId = M.userId - where con paperId = M.paperId - end) = struct - - table user : {Id : int, Nam : string, Password : string, Chair : bool, OnPc : bool} - PRIMARY KEY Id, - CONSTRAINT Nam UNIQUE Nam - sequence userId - - con paper = [Id = int, Document = blob] ++ map fst M.paper ++ M.paperPrivate - table paper : paper - PRIMARY KEY Id - sequence paperId - - table authorship : {Paper : int, User : int} - PRIMARY KEY (Paper, User), - CONSTRAINT Paper FOREIGN KEY Paper REFERENCES paper(Id) ON DELETE CASCADE, - CONSTRAINT User FOREIGN KEY User REFERENCES user(Id) - - con review = [Paper = int, User = int] ++ map fst M.review - table review : review - PRIMARY KEY (Paper, User), - CONSTRAINT Paper FOREIGN KEY Paper REFERENCES paper(Id), - CONSTRAINT User FOREIGN KEY User REFERENCES user(Id) - sequence reviewId - - cookie login : {Id : int, Password : string} - - val checkLogin = - r <- getCookie login; - case r of - None => return None - | Some r => - oneOrNoRows1 (SELECT user.Id, user.Nam, user.Chair, user.OnPc - FROM user - WHERE user.Id = {[r.Id]} - AND user.Password = {[r.Password]}) - - val getLogin = - ro <- checkLogin; - case ro of - None => error <xml>You must be logged in to do that.</xml> - | Some r => return r - - val getPcLogin = - r <- getLogin; - if r.OnPc then - return (r -- #OnPc) - 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 review = review - val checkLogin = checkLogin - val getLogin = getLogin - val getPcLogin = getPcLogin - val checkChair = checkChair - val summarizePaper = @@M.summarizePaper - 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 - return () - else - error <xml>You aren't authorized to see that paper.</xml> - - structure Users = BulkEdit.Make(struct - con keyName = #Id - val visible = {Nam = string "Name", - Chair = bool "Chair?", - OnPc = bool "On PC?"} - - val title = "Users" - val isAllowed = - me <- checkLogin; - return (Option.isSome me) - - val t = user - end) - - fun doRegister r = - n <- oneRowE1 (SELECT COUNT( * ) AS N - FROM user - WHERE user.Nam = {[r.Nam]}); - if n > 0 then - register (Some "Sorry; that username is taken.") - else - id <- nextval userId; - dml (INSERT INTO user (Id, Nam, Password, Chair, OnPc) - VALUES ({[id]}, {[r.Nam]}, {[r.Password]}, FALSE, FALSE)); - setCookie login {Id = id, Password = r.Password}; - main () - - and register msg = return <xml><body> - <h1>Registering a New Account</h1> - - {case msg of - None => <xml/> - | Some msg => <xml><div>{[msg]}</div></xml>} - - <form><table> - <tr> <th>Username:</th> <td><textbox{#Nam}/></td> </tr> - <tr> <th>Password:</th> <td><password{#Password}/></td> </tr> - <tr> <th><submit action={doRegister}/></th> </tr> - </table></form> - </body></xml> - - and signin r = - ro <- oneOrNoRowsE1 (SELECT user.Id AS N - FROM user - WHERE user.Nam = {[r.Nam]} - AND user.Password = {[r.Password]}); - (case ro of - None => return () - | Some id => setCookie login {Id = id, Password = r.Password}); - m <- main' (); - return <xml><body> - {case ro of - None => <xml><div>Invalid username or password.</div></xml> - | _ => <xml/>} - - {m} - </body></xml> - - and main' () = - me <- checkLogin; - now <- now; - return <xml><ul> - {case me of - None => <xml> - <li><a link={register None}>Register for access</a></li> - <li><b>Log in:</b> <form><table> - <tr> <th>Username:</th> <td><textbox{#Nam}/></td> </tr> - <tr> <th>Password:</th> <td><password{#Password}/></td> </tr> - <tr> <th><submit value="Log in" action={signin}/></th> </tr> - </table></form></li> - </xml> - | Some me => <xml> - <div>Welcome, {[me.Nam]}!</div> - - {if me.Chair then - <xml> - <li><a link={Users.main ()}>Manage users</a></li> - {O.linksForChair} - </xml> - else - <xml/>} - - {if me.OnPc then - <xml> - <li><a link={all ()}>All papers</a></li> - <li><a link={your ()}>Your papers</a></li> - {O.linksForPc} - </xml> - else - <xml/>} - - {if now < M.submissionDeadline then - <xml><li><a link={submit ()}>Submit</a></li></xml> - else - <xml/>} - </xml>} - </ul></xml> - - and main () = - m <- main' (); - return <xml><body>{m}</body></xml> - - and submit () = - let - fun doSubmit r = - me <- getLogin; - coauthors <- List.mapM (fn name => oneOrNoRowsE1 (SELECT user.Id AS N - FROM user - WHERE user.Nam = {[name.Nam]})) r.Authors; - if List.exists Option.isNone coauthors then - error <xml>At least one of those coauthor usernames isn't registered.</xml> - else - id <- nextval paperId; - dml (insert paper ({Id = sql_inject id, Document = sql_inject (fileData r.Document)} - ++ ensql M.paper (r -- #Authors -- #Document) M.paperFolder - ++ initialize M.paperPrivate M.paperPrivateFolder)); - List.app (fn uid => - case uid of - None => error <xml>Impossible empty uid!</xml> - | Some uid => dml (INSERT INTO authorship (Paper, User) - VALUES ({[id]}, {[uid]}))) - (Some me.Id :: coauthors); - return <xml><body> - Thanks for submitting! - </body></xml> - in - me <- getLogin; - numAuthors <- Dnat.zero; - - return <xml><body> - <h1>Submit a Paper</h1> - - <form> - <b>Author:</b> {[me.Nam]}<br/> - <subforms{#Authors}> - {Dnat.render <xml><entry><b>Author:</b> <textbox{#Nam}/><br/></entry></xml> numAuthors} - </subforms> - <button value="Add author" onclick={Dnat.inc numAuthors}/><br/> - <button value="Remove author" onclick={Dnat.dec numAuthors}/><br/> - <br/> - - {useMore (allWidgets M.paper M.paperFolder)} - <b>Paper:</b> <upload{#Document}/><br/> - <submit value="Submit" action={doSubmit}/> - </form> - </body></xml> - end - - and listPapers [tabs] [[Paper] ~ tabs] - (q : sql_query ([Paper = [Id = int] ++ map fst M.paper ++ M.paperPrivate] ++ 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 ++ M.paperPrivate}} FROM paper) - - and your () = - me <- getLogin; - listPapers (sql_query {Rows = sql_query1 {Distinct = False, - From = O.joinYourPaper me.Id (sql_from_table [#Paper] paper), - Where = (WHERE TRUE), - GroupBy = sql_subset_all [_], - Having = (WHERE TRUE), - SelectFields = sql_subset [[Paper = - ([Id = _] - ++ map fst M.paper - ++ M.paperPrivate, _)] - ++ 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 = - me <- getLogin; - checkPaper id; - dml (insert review ({Paper = sql_inject id, User = sql_inject me.Id} - ++ ensql M.review r M.reviewFolder)); - one id - - fun saveReview r = - me <- getLogin; - checkPaper id; - dml (update [map fst M.review] ! (ensql M.review r M.reviewFolder) - review (WHERE T.Paper = {[id]} AND T.User = {[me.Id]})); - one id - in - me <- getLogin; - checkPaper id; - ro <- oneOrNoRows (SELECT paper.{{map fst M.paper}}, octet_length(paper.Document) AS N - FROM paper - WHERE paper.Id = {[id]}); - authors <- queryX (SELECT user.Nam - FROM authorship - JOIN user ON authorship.User = user.Id - WHERE authorship.Paper = {[id]}) - (fn r => <xml><li>{[r.User.Nam]}</li></xml>); - myReview <- oneOrNoRows1 (SELECT review.{{map fst M.review}} - FROM review - WHERE review.User = {[me.Id]} - AND review.Paper = {[id]}); - otherReviews <- queryX (SELECT user.Nam, review.{{map fst M.review}} - FROM review JOIN user ON review.User = user.Id - WHERE review.Paper = {[id]} - AND review.User <> {[me.Id]}) - (fn r => <xml> - <hr/> - <b>User:</b> {[r.User.Nam]}<br/> - {allContent M.review r.Review M.reviewFolder} - </xml>); - - case ro of - None => error <xml>Paper not found!</xml> - | Some r => return <xml><body> - <h1>Paper #{[id]}</h1> - - <h3>Authors:</h3> - <ul> - {authors} - </ul> - - {allContent M.paper r.Paper M.paperFolder}<br/> - - {if r.N = 0 then - <xml><div>No paper uploaded yet.</div></xml> - else - <xml><a link={download id}>Download paper</a> ({[r.N]} bytes)</xml>} - - <hr/> - - {case myReview of - None => <xml> - <h2>Add Your Review</h2> - - <form> - {allWidgets M.review M.reviewFolder} - <submit value="Add" action={newReview}/> - </form> - </xml> - | Some myReview => <xml> - <h2>Edit Your Review</h2> - - <form> - {allPopulated M.review myReview M.reviewFolder} - <submit value="Save" action={saveReview}/> - </form> - </xml>} - - <hr/> - <h2>Other reviews</h2> - - {otherReviews} - </body></xml> - end - - and download id = - checkPaper id; - ro <- oneOrNoRows (SELECT paper.Document - FROM paper - WHERE paper.Id = {[id]}); - case ro of - None => error <xml>Paper not found!</xml> - | Some r => returnBlob r.Paper.Document (blessMime "application/pdf") - -end - - -functor Join(M : sig - structure O1 : OUTPUT - - structure O2 : OUTPUT where con paper = O1.paper - where con userId = O1.userId - where con paperId = O1.paperId - - constraint O1.yourPaperTables ~ O2.yourPaperTables - end) - = struct - open M - open O1 - - val linksForPc = <xml>{O1.linksForPc}{O2.linksForPc}</xml> - val linksForChair = <xml>{O1.linksForChair}{O2.linksForChair}</xml> - - con yourPaperTables = O1.yourPaperTables ++ O2.yourPaperTables - constraint [Paper] ~ yourPaperTables - - fun joinYourPaper [tabs] [paper] [[Paper] ~ tabs] [[Paper] ~ _] [tabs ~ yourPaperTables] [[Id] ~ paper] - uid (fi : sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)) = - O2.joinYourPaper uid (O1.joinYourPaper uid fi) - end
--- a/demo/more/conference.urp Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -allow mime application/pdf - -$/string -$/option -$/list -meta -bulkEdit -dnat -conference -conferenceFields -select -checkGroup -expandable -bid -decision
--- a/demo/more/conference.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,91 +0,0 @@ -signature INPUT = sig - con paper :: {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 - 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 - - con review :: {Type} - constraint [Paper, User] ~ review - table review : ([Paper = paperId, User = userId] ++ review) - PRIMARY KEY (Paper, User) - - 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 - -signature OUTPUT = sig - con paper :: {Type} - type userId - type paperId - - val linksForPc : xbody - val linksForChair : xbody - - con yourPaperTables :: {{Type}} - constraint [Paper] ~ yourPaperTables - val joinYourPaper : tabs ::: {{Type}} -> paper ::: {Type} - -> [[Paper] ~ tabs] => [[Paper] ~ yourPaperTables] => [tabs ~ yourPaperTables] => [[Id] ~ paper] => - userId (* Current user *) - -> 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 - val paper : $(map Meta.meta paper) - val paperFolder : folder paper - - con paperPrivate :: {Type} - constraint [Id, Document, Authors] ~ paperPrivate - constraint paper ~ paperPrivate - val paperPrivate : $(map Meta.private paperPrivate) - val paperPrivateFolder : folder paperPrivate - - con review :: {(Type * Type)} - constraint [Paper, User] ~ review - val review : $(map Meta.meta review) - val reviewFolder : folder review - - val submissionDeadline : time - val summarizePaper : ctx ::: {Unit} -> [[Body] ~ ctx] => $(map fst paper ++ paperPrivate) - -> xml ([Body] ++ ctx) [] [] - - functor Make (M : INPUT where con paper = map fst paper ++ paperPrivate - where con review = map fst review) - : OUTPUT where con paper = map fst paper ++ paperPrivate - where con userId = M.userId - where con paperId = M.paperId - end) : sig - - val main : unit -> transaction page - -end - -functor Join(M : sig - structure O1 : OUTPUT - - structure O2 : OUTPUT where con paper = O1.paper - where con userId = O1.userId - where con paperId = O1.paperId - - constraint O1.yourPaperTables ~ O2.yourPaperTables - end) : OUTPUT where con paper = M.O1.paper - where con userId = M.O1.userId - where con paperId = M.O1.paperId - where con yourPaperTables = M.O1.yourPaperTables ++ M.O2.yourPaperTables
--- a/demo/more/conference1.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ -open ConferenceFields - -open Conference.Make(struct - val paper = {Title = title, - Abstract = abstract} - val paperPrivate = {Decision = Decision.decision} - val review = {Rating = dropdown "Rating" (#"A" :: #"B" :: #"C" :: #"D" :: []), - CommentsForAuthors = commentsForAuthors} - - val submissionDeadline = readError "2009-11-22 23:59:59" - - fun summarizePaper [ctx] [[Body] ~ ctx] r = txt r.Title - functor Make (M : Conference.INPUT where con paper = _ - where con review = _) = struct - open M - - fun status [ctx] [[Body] ~ ctx] r = - queryX (SELECT review.Rating - FROM review - WHERE review.Paper = {[r.Id]}) - (fn r => <xml>{[r.Review.Rating]}; </xml>) - - open Conference.Join(struct - structure O1 = Bid.Make(M) - structure O2 = Decision.Make(struct - con paperOther = _ - open M - - val status = @@status - end) - end) - end - end)
--- a/demo/more/conference1.urp Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -library conference -database dbname=conf1 -sql conf1.sql - -conference1
--- a/demo/more/conferenceFields.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -open Meta - -val title = string "Title" -val abstract = textarea "Abstract" -val commentsForAuthors = textarea "Comments for Authors" - -fun charIn s = - if String.length s = 0 then - error <xml>Impossible: Empty option value</xml> - else - String.sub s 0 - -con dropdown = (char, string) -fun dropdown name opts = {Nam = name, - Show = txt, - Widget = fn [nm :: Name] => <xml><select{nm}> - {List.mapX (fn x => <xml><option>{[x]}</option></xml>) opts} - </select></xml>, - WidgetPopulated = fn [nm :: Name] v => <xml><select{nm}> - {List.mapX (fn x => <xml><option selected={x = v}>{[x]}</option></xml>) opts} - </select></xml>, - Parse = charIn, - Inject = _} - -val dropdown_show = _
--- a/demo/more/conferenceFields.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -val title : Meta.meta (string, string) -val abstract : Meta.meta (string, string) -val commentsForAuthors : Meta.meta (string, string) - -con dropdown :: (Type * Type) -val dropdown : string -> list char -> Meta.meta dropdown -val dropdown_show : show dropdown.1
--- a/demo/more/decision.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,74 +0,0 @@ -val decision = {Nam = "Decision", - Initialize = None, - Show = fn bo => cdata (case bo of - None => "?" - | Some True => "Accept" - | Some False => "Reject"), - Inject = _} - -functor Make(M : sig - con paperOther :: {Type} - constraint [Id, Decision] ~ paperOther - include Conference.INPUT - where con paper = [Decision = option bool] ++ paperOther - - val status : ctx ::: {Unit} -> [[Body] ~ ctx] => $([Id = paperId] ++ paperOther) - -> transaction (xml ([Body] ++ ctx) [] []) - end) = struct - open M - - val linksForChair = - let - fun makeDecisions () = - ps <- queryX' (SELECT paper.Id, paper.Decision, paper.{{M.paperOther}} - FROM paper - ORDER BY paper.Id) - (fn r => st <- status (r.Paper -- #Decision); - return <xml><tr> - <td>{useMore (summarizePaper (r.Paper -- #Id))}</td> - <td>{useMore st}</td> - <td><entry> - <hidden{#Paper} value={show r.Paper.Id}/> - <select{#Decision}> - <option selected={r.Paper.Decision = None}>?</option> - <option selected={r.Paper.Decision = Some True}>Accept</option> - <option selected={r.Paper.Decision = Some False}>Reject</option> - </select></entry></td> - </tr></xml>); - return <xml><body> - <h1>Make acceptance decisions</h1> - - <form> - <subforms{#Papers}> - <table> - <tr> <th>Paper</th> <th>Status</th> <th>Decision</th> </tr> - {ps} - </table> - </subforms> - <submit value="Save" action={saveDecisions}/> - </form> - </body></xml> - - and saveDecisions r = - List.app (fn {Paper = pid, Decision = dec} => - dml (UPDATE paper - SET Decision = {[case dec of - "?" => None - | "Accept" => Some True - | "Reject" => Some False - | _ => error <xml>Invalid decision code</xml>]} - WHERE Id = {[readError pid]})) r.Papers; - makeDecisions () - in - <xml> - <li><a link={makeDecisions ()}>Make acceptance decisions</a></li> - </xml> - end - - val linksForPc = <xml/> - - con yourPaperTables = [] - constraint [Paper] ~ yourPaperTables - fun joinYourPaper [tabs] [paper] [[Paper] ~ tabs] [[Paper] ~ _] [tabs ~ yourPaperTables] [[Id] ~ paper] - uid (fi : sql_from_items ([Paper = [Id = paperId] ++ paper] ++ tabs)) = fi -end
--- a/demo/more/decision.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -val decision : Meta.private (option bool) - -functor Make (M : sig - con paperOther :: {Type} - constraint [Id, Decision] ~ paperOther - include Conference.INPUT - where con paper = [Decision = option bool] ++ paperOther - - val status : ctx ::: {Unit} -> [[Body] ~ ctx] => $([Id = paperId] ++ paperOther) - -> transaction (xml ([Body] ++ ctx) [] []) - end) : Conference.OUTPUT where con paper = [Decision = option bool] ++ M.paperOther - where con userId = M.userId - where con paperId = M.paperId - where con yourPaperTables = []
--- a/demo/more/dnat.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -datatype t' = O | S of source t' -type t = source t' - -val zero = source O - -fun inc n = - v <- get n; - case v of - O => - n' <- source O; - set n (S n') - | S n => inc n - -fun dec n = - let - fun dec' last n = - v <- get n; - case v of - O => (case last of - None => return () - | Some n' => set n' O) - | S n' => dec' (Some n) n' - in - dec' None n - end - -fun render [ctx] [inp] [[Body] ~ ctx] (xml : xml ([Body] ++ ctx) inp []) n = - let - fun render n = - n <- signal n; - return (render' n) - - and render' n = - case n of - O => <xml/> - | S n => <xml> - {xml} - <dyn signal={render n}/> - </xml> - in - <xml><dyn signal={render n}/></xml> - end
--- a/demo/more/dnat.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -type t - -val zero : transaction t -val inc : t -> transaction unit -val dec : t -> transaction unit - -val render : ctx ::: {Unit} -> inp ::: {Type} -> [[Body] ~ ctx] => - xml ([Body] ++ ctx) inp [] -> t -> xml ([Body] ++ ctx) inp []
--- a/demo/more/expandable.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -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>
--- a/demo/more/expandable.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -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
--- a/demo/more/meta.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,91 +0,0 @@ -con meta = fn (db :: Type, widget :: Type) => - {Nam : string, - Show : db -> xbody, - Widget : nm :: Name -> xml form [] [nm = widget], - WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], - Parse : widget -> db, - Inject : sql_injectable db} - -fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) name : meta (t, string) = - {Nam = name, - Show = txt, - Widget = fn [nm :: Name] => <xml><textbox{nm}/></xml>, - WidgetPopulated = fn [nm :: Name] n => - <xml><textbox{nm} value={show n}/></xml>, - Parse = readError, - Inject = _} - -val int = default -val float = default -val string = default -fun bool name = {Nam = name, - Show = txt, - Widget = fn [nm :: Name] => <xml><checkbox{nm}/></xml>, - WidgetPopulated = fn [nm :: Name] b => - <xml><checkbox{nm} checked={b}/></xml>, - Parse = fn x => x, - Inject = _} - -fun textarea name = {Nam = name, - Show = cdata, - Widget = fn [nm :: Name] => <xml><br/><textarea{nm} rows={10} cols={80}/></xml>, - WidgetPopulated = fn [nm :: Name] s => <xml><br/> - <textarea{nm} rows={10} cols={80}>{[s]}</textarea> - </xml>, - Parse = fn s => s, - Inject = _} - -fun allContent [ts ::: {(Type * Type)}] (r : $(map meta ts)) (vs : $(map fst ts)) (fl : folder ts) = - foldRX2 [meta] [fst] [_] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] - (m : meta p) v => - <xml><b>{[m.Nam]}</b>: {m.Show v}<br/></xml>) - [_] fl r vs - -fun allWidgets [ts ::: {(Type * Type)}] (r : $(map meta ts)) (fl : folder ts) = - foldR [meta] [fn ts :: {(Type * Type)} => xml form [] (map snd ts)] - (fn [nm :: Name] [t :: (Type * Type)] [rest :: {(Type * Type)}] - [[nm] ~ rest] (col : meta t) (acc : xml form [] (map snd rest)) => <xml> - <b>{[col.Nam]}</b>: {col.Widget [nm]}<br/> - {useMore acc} - </xml>) - <xml/> - [_] fl r - -fun allPopulated [ts ::: {(Type * Type)}] (r : $(map meta ts)) (vs : $(map fst ts)) (fl : folder ts) = - foldR2 [meta] [fst] [fn cols :: {(Type * Type)} => - xml form [] (map snd cols)] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] - (m : meta p) v (acc : xml form [] (map snd rest)) => - <xml> - {[m.Nam]}: {m.WidgetPopulated [nm] v}<br/> - {useMore acc} - </xml>) - <xml/> - [_] fl r vs - -fun allPopulatedTr [ts ::: {(Type * Type)}] (r : $(map meta ts)) (vs : $(map fst ts)) (fl : folder ts) = - foldR2 [meta] [fst] [fn cols :: {(Type * Type)} => - xml [Body, Form, Tr] [] (map snd cols)] - (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] - (m : meta p) v (acc : xml [Body, Form, Tr] [] (map snd rest)) => - <xml> - <td>{m.WidgetPopulated [nm] v}</td> - {useMore acc} - </xml>) - <xml/> - [_] fl r vs - -fun ensql [avail] [ts ::: {(Type * Type)}] (r : $(map meta ts)) (vs : $(map snd ts)) (fl : folder ts) = - map2 [meta] [snd] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1] - (fn [ts] meta v => @sql_inject meta.Inject (meta.Parse v)) - [_] fl r vs - -con private = fn t :: Type => - {Nam : string, - Initialize : t, - Show : t -> xbody, - Inject : sql_injectable t} - -fun initialize [ts] (r : $(map private ts)) (fl : folder ts) = - mp [private] [sql_exp [] [] []] (fn [t] r => @sql_inject r.Inject r.Initialize) [_] fl r
--- a/demo/more/meta.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ -con meta = fn (db :: Type, widget :: Type) => - {Nam : string, - Show : db -> xbody, - Widget : nm :: Name -> xml form [] [nm = widget], - WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], - Parse : widget -> db, - Inject : sql_injectable db} - -val int : string -> meta (int, string) -val float : string -> meta (float, string) -val string : string -> meta (string, string) -val bool : string -> meta (bool, bool) - -val textarea : string -> meta (string, string) - -val allContent : ts ::: {(Type * Type)} -> $(map meta ts) -> $(map fst ts) -> folder ts -> xbody - -val allWidgets : ts ::: {(Type * Type)} -> $(map meta ts) -> folder ts - -> xml form [] (map snd ts) - -val allPopulated : ts ::: {(Type * Type)} -> $(map meta ts) -> $(map fst ts) -> folder ts - -> xml form [] (map snd ts) - -val allPopulatedTr : ts ::: {(Type * Type)} -> $(map meta ts) -> $(map fst ts) -> folder ts - -> xml ([Tr] ++ form) [] (map snd ts) - -val ensql : avail ::: {{Type}} -> ts ::: {(Type * Type)} -> $(map meta ts) -> $(map snd ts) -> folder ts - -> $(map (sql_exp avail [] []) (map fst ts)) - -con private = fn t :: Type => - {Nam : string, - Initialize : t, - Show : t -> xbody, - Inject : sql_injectable t} - -val initialize : ts ::: {Type} -> $(map private ts) -> folder ts -> $(map (sql_exp [] [] []) ts)
--- a/demo/more/select.ur Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -fun selectChar choices current = - List.mapX (fn (ch, label) => - <xml><option value={String.str ch} selected={current = Some ch}>{[label]}</option></xml>) choices
--- a/demo/more/select.urs Mon Dec 20 13:29:56 2010 -0500 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -val selectChar : list (char * string) -> option char -> xml select [] []
--- a/doc/manual.tex Mon Dec 20 13:29:56 2010 -0500 +++ b/doc/manual.tex Mon Dec 20 19:28:41 2010 -0500 @@ -524,7 +524,7 @@ A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$. -Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all implicit constructor arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally halting automatic resolution of type class instances and automatic proving of disjointness constraints. The default is that implicit arguments are inserted automatically after any reference to a non-local variable, or after any application of a non-local variable to one or more arguments. For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors). +Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all type class instance and disjointness arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally making explicit all implicit constructor arguments. The default is that implicit arguments are inserted automatically after any reference to a non-local variable, or after any application of a non-local variable to one or more arguments. For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors). At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid X \mid [c \sim c]$. A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind. The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$. It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type.