annotate demo/more/dnat.ur @ 1180:ac3dbbc85c6e

Standard library moduls Incl and Mem; tweaks to Especialize and Unpoly
author Adam Chlipala <adamc@hcoop.net>
date Sat, 06 Mar 2010 16:15:26 -0500
parents e47303e5d73d
children
rev   line source
adamc@1015 1 datatype t' = O | S of source t'
adamc@1015 2 type t = source t'
adamc@1015 3
adamc@1015 4 val zero = source O
adamc@1015 5
adamc@1015 6 fun inc n =
adamc@1015 7 v <- get n;
adamc@1015 8 case v of
adamc@1015 9 O =>
adamc@1015 10 n' <- source O;
adamc@1015 11 set n (S n')
adamc@1015 12 | S n => inc n
adamc@1015 13
adamc@1015 14 fun dec n =
adamc@1015 15 let
adamc@1015 16 fun dec' last n =
adamc@1015 17 v <- get n;
adamc@1015 18 case v of
adamc@1015 19 O => (case last of
adamc@1015 20 None => return ()
adamc@1015 21 | Some n' => set n' O)
adamc@1015 22 | S n' => dec' (Some n) n'
adamc@1015 23 in
adamc@1015 24 dec' None n
adamc@1015 25 end
adamc@1015 26
adamc@1015 27 fun render [ctx] [inp] [[Body] ~ ctx] (xml : xml ([Body] ++ ctx) inp []) n =
adamc@1015 28 let
adamc@1015 29 fun render n =
adamc@1015 30 n <- signal n;
adamc@1015 31 return (render' n)
adamc@1015 32
adamc@1015 33 and render' n =
adamc@1015 34 case n of
adamc@1015 35 O => <xml/>
adamc@1015 36 | S n => <xml>
adamc@1015 37 {xml}
adamc@1015 38 <dyn signal={render n}/>
adamc@1015 39 </xml>
adamc@1015 40 in
adamc@1015 41 <xml><dyn signal={render n}/></xml>
adamc@1015 42 end