Ur/Web: demo/noisy.ur annotate

Mention src/coq in CHANGELOG

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 12 Mar 2009 12:37:02 -0400
parents	bab524996fca
children	1a317a707d71

rev	line source
adamc@651	1 datatype list t = Nil \| Cons of t * list t
adamc@651	2
adamc@651	3 table t : { Id : int, A : string }
adamc@651	4
adamc@651	5 fun add id s =
adamc@651	6 dml (INSERT INTO t (Id, A) VALUES ({[id]}, {[s]}))
adamc@651	7
adamc@651	8 fun del id =
adamc@651	9 dml (DELETE FROM t WHERE t.Id = {[id]})
adamc@651	10
adamc@651	11 fun lookup id =
adamc@651	12 ro <- oneOrNoRows (SELECT t.A FROM t WHERE t.Id = {[id]});
adamc@651	13 case ro of
adamc@651	14 None => return None
adamc@651	15 \| Some r => return (Some r.T.A)
adamc@651	16
adamc@651	17 fun check ls =
adamc@651	18 case ls of
adamc@651	19 Nil => return ()
adamc@651	20 \| Cons (id, ls') =>
adamc@651	21 ao <- lookup id;
adamc@651	22 alert (case ao of
adamc@651	23 None => "Nada"
adamc@651	24 \| Some a => a);
adamc@651	25 check ls'
adamc@651	26
adamc@651	27 fun main () =
adamc@651	28 idAdd <- source "";
adamc@651	29 aAdd <- source "";
adamc@651	30
adamc@651	31 idDel <- source "";
adamc@651	32
adamc@651	33 return <xml><body>
adamc@651	34 <button value="Check values of 1, 2, and 3" onclick={check (Cons (1, Cons (2, Cons (3, Nil))))}/><br/>
adamc@651	35 <br/>
adamc@651	36 <button value="Add" onclick={id <- get idAdd; a <- get aAdd; add (readError id) a}/>
adamc@651	37 <ctextbox source={idAdd}/>
adamc@651	38 <ctextbox source={aAdd}/><br/>
adamc@651	39 <br/>
adamc@651	40 <button value="Delete" onclick={id <- get idDel; del (readError id)}/>
adamc@651	41 <ctextbox source={idDel}/>
adamc@651	42 </body></xml>

Mercurial > urweb