# HG changeset patch # User Adam Chlipala # Date 1227198876 18000 # Node ID 7ef4b2911b096856a6f3abaa267a1d1ef7371d49 # Parent 581554f8e642a0a7615b947cd5455a31457092e1 Some demo improvements diff -r 581554f8e642 -r 7ef4b2911b09 demo/list.ur --- a/demo/list.ur Thu Nov 20 10:44:28 2008 -0500 +++ b/demo/list.ur Thu Nov 20 11:34:36 2008 -0500 @@ -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 -r 581554f8e642 -r 7ef4b2911b09 demo/listFun.ur --- a/demo/listFun.ur Thu Nov 20 10:44:28 2008 -0500 +++ b/demo/listFun.ur Thu Nov 20 11:34:36 2008 -0500 @@ -10,21 +10,24 @@ Nil => [] | Cons (x, ls') => {[M.toString x]} :: {toXml ls'} - fun console (ls : list M.t) = return - Current list: {toXml ls}
- Reversed list: {toXml (rev ls)}
- Length: {[length ls]}
-
+ fun console (ls : list M.t) = + let + fun cons (r : {X : string}) = + case M.fromString r.X of + None => return Invalid string! + | Some v => console (Cons (v, ls)) + in + return + Current list: {toXml ls}
+ Reversed list: {toXml (rev ls)}
+ Length: {[length ls]}
+
- - - and cons (ls : list M.t) (r : {X : string}) = - case M.fromString r.X of - None => return Invalid string! - | Some v => console (Cons (v, ls)) + + end fun main () = console Nil end diff -r 581554f8e642 -r 7ef4b2911b09 demo/prose --- a/demo/prose Thu Nov 20 10:44:28 2008 -0500 +++ b/demo/prose Thu Nov 20 11:34:36 2008 -0500 @@ -1,4 +1,4 @@ -

Ur/Web 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). Ur 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 Standard ML, with a few Haskell-isms added, and kinder, gentler versions added of many features from dependently-typed languages like the logic behind Coq. 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.

+

Ur/Web 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). Ur 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 Standard ML, with a few Haskell-isms added, and kinder, gentler versions added of many features from dependently-typed languages like the logic behind Coq. 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.

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 @@

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.

+tree.urp + +

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.

+ sum.urp

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.

@@ -132,10 +136,6 @@

This example showcases code reuse by applying the same functor as in the last example. The Metaform2 module mixes pages from the functor with some new pages of its own.

-tree.urp - -

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.

- crud1.urp

This example pulls together much of what we have seen so far. It involves a generic "admin interface" builder. That is, we have the Crud.Make functor, which takes in a description of a table and outputs a sub-application for viewing and editing that table.

diff -r 581554f8e642 -r 7ef4b2911b09 demo/refFun.ur --- a/demo/refFun.ur Thu Nov 20 10:44:28 2008 -0500 +++ b/demo/refFun.ur Thu Nov 20 11:34:36 2008 -0500 @@ -15,9 +15,9 @@ fun read r = o <- oneOrNoRows (SELECT t.Data FROM t WHERE t.Id = {[r]}); - return (case o of + case o of None => error You already deleted that ref! - | Some r => r.T.Data) + | Some r => return r.T.Data fun write r d = dml (UPDATE t SET Data = {[d]} WHERE Id = {[r]}) diff -r 581554f8e642 -r 7ef4b2911b09 src/demo.sig --- a/src/demo.sig Thu Nov 20 10:44:28 2008 -0500 +++ b/src/demo.sig Thu Nov 20 11:34:36 2008 -0500 @@ -27,6 +27,6 @@ signature DEMO = sig - val make : {prefix : string, dirname : string} -> unit + val make : {prefix : string, dirname : string, guided : bool} -> unit end diff -r 581554f8e642 -r 7ef4b2911b09 src/demo.sml --- a/src/demo.sml Thu Nov 20 10:44:28 2008 -0500 +++ b/src/demo.sml Thu Nov 20 11:34:36 2008 -0500 @@ -27,7 +27,7 @@ structure Demo :> DEMO = struct -fun make {prefix, dirname} = +fun make {prefix, dirname, guided} = let val prose = OS.Path.joinDirFile {dir = dirname, file = "prose"} @@ -127,7 +127,12 @@ file = out} val out = TextIO.openOut out - val () = (TextIO.output (out, "\n"); + val () = (TextIO.output (out, "\n"); TextIO.output (out, " (timing, demo, rev sources) | "-demo" :: prefix :: rest => - doArgs (rest, (timing, SOME prefix, sources)) + doArgs (rest, (timing, SOME (prefix, false), sources)) + | "-guided-demo" :: prefix :: rest => + doArgs (rest, (timing, SOME (prefix, true), sources)) | arg :: rest => let val acc = @@ -52,8 +54,8 @@ val () = case demo of - SOME prefix => - Demo.make {prefix = prefix, dirname = job} + SOME (prefix, guided) => + Demo.make {prefix = prefix, dirname = job, guided = guided} | NONE => if timing then Compiler.time Compiler.toCjrize job