Ur/Web: demo/more/dnat.ur annotate

Hooks for measuring how much interesting proving is going on in elaboration

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 17 Nov 2009 12:44:14 -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

Mercurial > urweb