summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--demo/more/bid.ur158
-rw-r--r--demo/more/bid.urs7
-rw-r--r--demo/more/bulkEdit.ur52
-rw-r--r--demo/more/bulkEdit.urs24
-rw-r--r--demo/more/checkGroup.ur15
-rw-r--r--demo/more/checkGroup.urs5
-rw-r--r--demo/more/conference.ur459
-rw-r--r--demo/more/conference.urp15
-rw-r--r--demo/more/conference.urs91
-rw-r--r--demo/more/conference1.ur33
-rw-r--r--demo/more/conference1.urp5
-rw-r--r--demo/more/conferenceFields.ur25
-rw-r--r--demo/more/conferenceFields.urs7
-rw-r--r--demo/more/decision.ur74
-rw-r--r--demo/more/decision.urs14
-rw-r--r--demo/more/dnat.ur42
-rw-r--r--demo/more/dnat.urs8
-rw-r--r--demo/more/expandable.ur23
-rw-r--r--demo/more/expandable.urs6
-rw-r--r--demo/more/meta.ur91
-rw-r--r--demo/more/meta.urs36
-rw-r--r--demo/more/select.ur3
-rw-r--r--demo/more/select.urs1
-rw-r--r--doc/manual.tex2
24 files changed, 1 insertions, 1195 deletions
diff --git a/demo/more/bid.ur b/demo/more/bid.ur
deleted file mode 100644
index 50645f38..00000000
--- a/demo/more/bid.ur
+++ /dev/null
@@ -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
diff --git a/demo/more/bid.urs b/demo/more/bid.urs
deleted file mode 100644
index 1504c1b7..00000000
--- a/demo/more/bid.urs
+++ /dev/null
@@ -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]
diff --git a/demo/more/bulkEdit.ur b/demo/more/bulkEdit.ur
deleted file mode 100644
index 0226c3dd..00000000
--- a/demo/more/bulkEdit.ur
+++ /dev/null
@@ -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
diff --git a/demo/more/bulkEdit.urs b/demo/more/bulkEdit.urs
deleted file mode 100644
index 0e5d7a6c..00000000
--- a/demo/more/bulkEdit.urs
+++ /dev/null
@@ -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
diff --git a/demo/more/checkGroup.ur b/demo/more/checkGroup.ur
deleted file mode 100644
index ab1cc781..00000000
--- a/demo/more/checkGroup.ur
+++ /dev/null
@@ -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
diff --git a/demo/more/checkGroup.urs b/demo/more/checkGroup.urs
deleted file mode 100644
index d448527e..00000000
--- a/demo/more/checkGroup.urs
+++ /dev/null
@@ -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)
diff --git a/demo/more/conference.ur b/demo/more/conference.ur
deleted file mode 100644
index bf8e364a..00000000
--- a/demo/more/conference.ur
+++ /dev/null
@@ -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
diff --git a/demo/more/conference.urp b/demo/more/conference.urp
deleted file mode 100644
index 663fd681..00000000
--- a/demo/more/conference.urp
+++ /dev/null
@@ -1,15 +0,0 @@
-allow mime application/pdf
-
-$/string
-$/option
-$/list
-meta
-bulkEdit
-dnat
-conference
-conferenceFields
-select
-checkGroup
-expandable
-bid
-decision
diff --git a/demo/more/conference.urs b/demo/more/conference.urs
deleted file mode 100644
index de35ad05..00000000
--- a/demo/more/conference.urs
+++ /dev/null
@@ -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
diff --git a/demo/more/conference1.ur b/demo/more/conference1.ur
deleted file mode 100644
index 646ba489..00000000
--- a/demo/more/conference1.ur
+++ /dev/null
@@ -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)
diff --git a/demo/more/conference1.urp b/demo/more/conference1.urp
deleted file mode 100644
index c78219c4..00000000
--- a/demo/more/conference1.urp
+++ /dev/null
@@ -1,5 +0,0 @@
-library conference
-database dbname=conf1
-sql conf1.sql
-
-conference1
diff --git a/demo/more/conferenceFields.ur b/demo/more/conferenceFields.ur
deleted file mode 100644
index 18387c96..00000000
--- a/demo/more/conferenceFields.ur
+++ /dev/null
@@ -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 = _
diff --git a/demo/more/conferenceFields.urs b/demo/more/conferenceFields.urs
deleted file mode 100644
index 3a034770..00000000
--- a/demo/more/conferenceFields.urs
+++ /dev/null
@@ -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
diff --git a/demo/more/decision.ur b/demo/more/decision.ur
deleted file mode 100644
index efd1b9c7..00000000
--- a/demo/more/decision.ur
+++ /dev/null
@@ -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
diff --git a/demo/more/decision.urs b/demo/more/decision.urs
deleted file mode 100644
index e33403cb..00000000
--- a/demo/more/decision.urs
+++ /dev/null
@@ -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 = []
diff --git a/demo/more/dnat.ur b/demo/more/dnat.ur
deleted file mode 100644
index 8d8095e7..00000000
--- a/demo/more/dnat.ur
+++ /dev/null
@@ -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
diff --git a/demo/more/dnat.urs b/demo/more/dnat.urs
deleted file mode 100644
index 2dd7e938..00000000
--- a/demo/more/dnat.urs
+++ /dev/null
@@ -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 []
diff --git a/demo/more/expandable.ur b/demo/more/expandable.ur
deleted file mode 100644
index 92d8743c..00000000
--- a/demo/more/expandable.ur
+++ /dev/null
@@ -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>
diff --git a/demo/more/expandable.urs b/demo/more/expandable.urs
deleted file mode 100644
index 820b89b7..00000000
--- a/demo/more/expandable.urs
+++ /dev/null
@@ -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
diff --git a/demo/more/meta.ur b/demo/more/meta.ur
deleted file mode 100644
index b8a3d584..00000000
--- a/demo/more/meta.ur
+++ /dev/null
@@ -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
diff --git a/demo/more/meta.urs b/demo/more/meta.urs
deleted file mode 100644
index cd3e183a..00000000
--- a/demo/more/meta.urs
+++ /dev/null
@@ -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)
diff --git a/demo/more/select.ur b/demo/more/select.ur
deleted file mode 100644
index 17cff4dd..00000000
--- a/demo/more/select.ur
+++ /dev/null
@@ -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
diff --git a/demo/more/select.urs b/demo/more/select.urs
deleted file mode 100644
index f9208b91..00000000
--- a/demo/more/select.urs
+++ /dev/null
@@ -1 +0,0 @@
-val selectChar : list (char * string) -> option char -> xml select [] []
diff --git a/doc/manual.tex b/doc/manual.tex
index da12d3c2..f517411d 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -524,7 +524,7 @@ A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is e
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 13:09:21 +0000