Mercurial > urweb
changeset 647:ae374df5ccbd
Prose for ListEdit
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 10 Mar 2009 13:46:45 -0400 |
parents | fb2a0e76dcef |
children | 3c6d535d3d8b |
files | demo/prose src/elaborate.sml |
diffstat | 2 files changed, 13 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/demo/prose Tue Mar 10 12:44:40 2009 -0400 +++ b/demo/prose Tue Mar 10 13:46:45 2009 -0400 @@ -197,3 +197,11 @@ <p>Most client-side JavaScript programs modify page contents imperatively, but Ur/Web is based on functional-reactive programming instead. Programs allocate data sources and then describe the page as a pure function of those data sources. When the sources change, the page changes automatically.</p> <p>Here's an example where a button modifies a data source that affects some text on the page. The affected portion of the page is indicated with the pseudo-HTML tag <tt>dyn</tt>, whose <tt>signal</tt> attribute specifies one of these pure functions over mutable sources. A source containing data of type <tt>t</tt> has type <tt>source t</tt> and is created with the <tt>source</tt> operation within the <tt>transaction</tt> monad. Functions over sources are represented in the monad <tt>signal</tt>. Like in Haskell, we overload monad notations, so that the same return and bind operators can be used to write signals and transactions. The <tt>signal</tt> function coerces a source to a signal.</p> + +listEdit.urp + +<p>This is a more involved functional-reactive example, involving recursive data structures that contain sources. We build a list editor similar to the one from the <tt>ListShop</tt> example, but with all editing happening on the client side.</p> + +<p>The central data structure is the <tt>rlist</tt>, a list whose individual elements are sources, enabling fine-grained mutation. Every rlist is either nil or is a cons cell made up of a source for a string data element, another source to serve as a scratchpad for GUI-based edits to the data element, and a final source that stores the remainder of the list.</p> + +<p>The main program provides operations to append to a list and to edit the data stored at any cell of the list. Append is implemented by maintaining a source <tt>head</tt>, which points to the first list element; and a source <tt>tailP</tt>, which points to a <tt>source rlist</tt> where we should place the next appended node.</p>
--- a/src/elaborate.sml Tue Mar 10 12:44:40 2009 -0400 +++ b/src/elaborate.sml Tue Mar 10 13:46:45 2009 -0400 @@ -706,13 +706,6 @@ ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) - fun eatMost unifs = - case unifs of - (_, r) :: (rest as _ :: _) => (r := SOME (L'.CRecord (k, []), loc); - eatMost rest) - | _ => unifs - val unifs1 = eatMost unifs1 - val unifs2 = eatMost unifs2 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2) (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), @@ -887,6 +880,11 @@ (L'.CError, _) => () | (_, L'.CError) => () + | (L'.CRecord _, _) => isRecord () + | (_, L'.CRecord _) => isRecord () + | (L'.CConcat _, _) => isRecord () + | (_, L'.CConcat _) => isRecord () + | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => if r1 = r2 then () @@ -1034,11 +1032,6 @@ | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => unifyCons' (E.pushKRel env x) c1 c2 - | (L'.CRecord _, _) => isRecord () - | (_, L'.CRecord _) => isRecord () - | (L'.CConcat _, _) => isRecord () - | (_, L'.CConcat _) => isRecord () - | _ => err CIncompatible end