diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-11-20 11:34:36 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-20 11:34:36 -0500 |
| commit | eb171fceba46cbe600d8e29adc526e86719cdc4f (patch) | |
| tree | be1fb9f820200f6d2620e1e597ff809b1f438d29 /demo | |
| parent | 55ad38ebb900b84fcfdeefe68678348e1cd3c36c (diff) | |
Some demo improvements
Diffstat (limited to 'demo')
| -rw-r--r-- | demo/list.ur | 30 | ||||
| -rw-r--r-- | demo/listFun.ur | 31 | ||||
| -rw-r--r-- | demo/prose | 10 | ||||
| -rw-r--r-- | demo/refFun.ur | 4 |
4 files changed, 42 insertions, 33 deletions
diff --git a/demo/list.ur b/demo/list.ur index c2dfce22..107bf92c 100644 --- a/demo/list.ur +++ b/demo/list.ur @@ -1,15 +1,21 @@ datatype list t = Nil | Cons of t * list t -fun length' (t ::: Type) (ls : list t) (acc : int) = - case ls of - Nil => acc - | Cons (_, ls') => length' ls' (acc + 1) +fun length (t ::: Type) (ls : list t) = + let + fun length' (ls : list t) (acc : int) = + case ls of + Nil => acc + | Cons (_, ls') => length' ls' (acc + 1) + in + length' ls 0 + end -fun length (t ::: Type) (ls : list t) = length' ls 0 - -fun rev' (t ::: Type) (ls : list t) (acc : list t) = - case ls of - Nil => acc - | Cons (x, ls') => rev' ls' (Cons (x, acc)) - -fun rev (t ::: Type) (ls : list t) = rev' ls Nil +fun rev (t ::: Type) (ls : list t) = + let + fun rev' (ls : list t) (acc : list t) = + case ls of + Nil => acc + | Cons (x, ls') => rev' ls' (Cons (x, acc)) + in + rev' ls Nil + end diff --git a/demo/listFun.ur b/demo/listFun.ur index c281a07d..d679c2fb 100644 --- a/demo/listFun.ur +++ b/demo/listFun.ur @@ -10,21 +10,24 @@ functor Make(M : sig Nil => <xml>[]</xml> | Cons (x, ls') => <xml>{[M.toString x]} :: {toXml ls'}</xml> - fun console (ls : list M.t) = return <xml><body> - Current list: {toXml ls}<br/> - Reversed list: {toXml (rev ls)}<br/> - Length: {[length ls]}<br/> - <br/> + fun console (ls : list M.t) = + let + fun cons (r : {X : string}) = + case M.fromString r.X of + None => return <xml><body>Invalid string!</body></xml> + | Some v => console (Cons (v, ls)) + in + return <xml><body> + Current list: {toXml ls}<br/> + Reversed list: {toXml (rev ls)}<br/> + Length: {[length ls]}<br/> + <br/> - <form> - Add element: <textbox{#X}/> <submit action={cons ls}/> - </form> - </body></xml> - - and cons (ls : list M.t) (r : {X : string}) = - case M.fromString r.X of - None => return <xml><body>Invalid string!</body></xml> - | Some v => console (Cons (v, ls)) + <form> + Add element: <textbox{#X}/> <submit action={cons}/> + </form> + </body></xml> + end fun main () = console Nil end @@ -1,4 +1,4 @@ -<p><b>Ur/Web</b> is a domain-specific language for programming web applications backed by SQL databases. It is (strongly) statically-typed (like ML and Haskell) and purely functional (like Haskell). <b>Ur</b> is the base language, and the web-specific features of Ur/Web (mostly) come only in the form of special rules for parsing, type inference, and optimization. The Ur core looks a lot like <a href="http://sml.sourceforge.net/">Standard ML</a>, with a few <a href="http://www.haskell.org/">Haskell</a>-isms added, and kinder, gentler versions added of many features from dependently-typed languages like the logic behind <a href="http://coq.inria.fr/">Coq</a>. The type system is much more expressive than in ML and Haskell, such that well-typed web applications cannot "go wrong," not just in handling single HTTP requests, but across their entire lifetimes of interacting with HTTP clients. Beyond that, Ur is unusual is using ideas from dependent typing to enable very effective metaprogramming, or programming with explicit analysis of type structure. Many common web application components can be built by Ur/Web functions that operate on types, where it seems impossible to achieve similar code re-use in more established languages.</p> +<p><b>Ur/Web</b> is a domain-specific language for programming web applications backed by SQL databases. It is (strongly) statically-typed (like ML and Haskell) and purely functional (like Haskell). <b>Ur</b> is the base language, and the web-specific features of Ur/Web (mostly) come only in the form of special rules for parsing and optimization. The Ur core looks a lot like <a href="http://sml.sourceforge.net/">Standard ML</a>, with a few <a href="http://www.haskell.org/">Haskell</a>-isms added, and kinder, gentler versions added of many features from dependently-typed languages like the logic behind <a href="http://coq.inria.fr/">Coq</a>. The type system is much more expressive than in ML and Haskell, such that well-typed web applications cannot "go wrong," not just in handling single HTTP requests, but across their entire lifetimes of interacting with HTTP clients. Beyond that, Ur is unusual is using ideas from dependent typing to enable very effective metaprogramming, or programming with explicit analysis of type structure. Many common web application components can be built by Ur/Web functions that operate on types, where it seems impossible to achieve similar code re-use in more established languages.</p> <p>This demo is built automatically from Ur/Web sources and supporting files. If you unpack the Ur/Web source distribution, then the following steps will build you a local version of this demo: @@ -92,6 +92,10 @@ ref.urp <p>The functor creates a new encapsulated SQL sequence and table on each call. These local relations show up in the automatically-generated SQL file that should be run to prepare the database for use, but they are invisible from client code. We could change the functor to create different SQL relations, without needing to change client code.</p> +tree.urp + +<p>Here we see how we can abstract over common patterns of SQL queries. In particular, since standard SQL does not help much with queries over trees, we write a function for traversing an SQL tree, building an HTML representation, based on a user-provided function for rendering individual rows.</p> + sum.urp <p>Metaprogramming is one of the most important facilities of Ur. This example shows how to write a function that is able to sum up the fields of records of integers, no matter which set of fields the particular record has.</p> @@ -132,10 +136,6 @@ metaform2.urp <p>This example showcases code reuse by applying the same functor as in the last example. The <tt>Metaform2</tt> module mixes pages from the functor with some new pages of its own.</p> -tree.urp - -<p>Here we see how we can abstract over common patterns of SQL queries. In particular, since standard SQL does not help much with queries over trees, we write a function for traversing an SQL tree, building an HTML representation, based on a user-provided function for rendering individual rows.</p> - crud1.urp <p>This example pulls together much of what we have seen so far. It involves a generic "admin interface" builder. That is, we have the <tt>Crud.Make</tt> functor, which takes in a description of a table and outputs a sub-application for viewing and editing that table.</p> diff --git a/demo/refFun.ur b/demo/refFun.ur index e523bac7..c6a4ea5f 100644 --- a/demo/refFun.ur +++ b/demo/refFun.ur @@ -15,9 +15,9 @@ functor Make(M : sig fun read r = o <- oneOrNoRows (SELECT t.Data FROM t WHERE t.Id = {[r]}); - return (case o of + case o of None => error <xml>You already deleted that ref!</xml> - | Some r => r.T.Data) + | Some r => return r.T.Data fun write r d = dml (UPDATE t SET Data = {[d]} WHERE Id = {[r]}) |