Ur/Web: tests/rpcM.ur annotate

Implemented proper congruence closure, to the point where tests/policy works

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 08 Apr 2010 12:46:21 -0400
parents	4a125bbc602d
children

rev	line source
adamc@642	1 datatype list t = Nil \| Cons of t * list t
adamc@642	2
adamc@642	3 sequence s
adamc@642	4
adamc@642	5 fun main () : transaction page =
adamc@642	6 let
adamc@642	7 fun getIndices srcs =
adamc@642	8 case srcs of
adamc@642	9 Nil => return Nil
adamc@642	10 \| Cons (src, srcs') =>
adamc@642	11 i <- nextval s;
adamc@642	12 set src i;
adamc@642	13 ls <- getIndices srcs';
adamc@642	14 return (Cons (i, ls))
adamc@642	15
adamc@642	16 fun show ls =
adamc@642	17 case ls of
adamc@642	18 Nil => <xml/>
adamc@642	19 \| Cons (x, ls') => <xml>{[x]}<br/>{show ls'}</xml>
adamc@642	20 in
adamc@642	21 src1 <- source 0;
adamc@642	22 src2 <- source 1;
adamc@642	23 s <- source Nil;
adamc@642	24 return <xml><body>
adamc@642	25 <button value="Get It On!"
adamc@642	26 onclick={ns <- getIndices (Cons (src1, Cons (src2, Nil)));
adamc@642	27 set s ns}/><br/>
adamc@642	28 <br/>
adamc@642	29 #1: <dyn signal={n <- signal src1; return <xml>{[n]}</xml>}/><br/>
adamc@642	30 #2: <dyn signal={n <- signal src2; return <xml>{[n]}</xml>}/><br/>
adamc@642	31 Current: <dyn signal={ns <- signal s; return (show ns)}/>
adamc@642	32 </body></xml>
adamc@642	33 end

Mercurial > urweb