diff demo/more/dnat.ur @ 1015:e47303e5d73d

Factor Dnat into separate module
author Adam Chlipala <adamc@hcoop.net>
date Sun, 25 Oct 2009 11:03:42 -0400
parents
children
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/more/dnat.ur	Sun Oct 25 11:03:42 2009 -0400
@@ -0,0 +1,42 @@
+datatype t' = O | S of source t'
+type t = source t'
+
+val zero = source O
+
+fun inc n =
+    v <- get n;
+    case v of
+        O =>
+        n' <- source O;
+        set n (S n')
+      | S n => inc n
+
+fun dec n =
+    let
+        fun dec' last n =
+            v <- get n;
+            case v of
+                O => (case last of
+                          None => return ()
+                        | Some n' => set n' O)
+              | S n' => dec' (Some n) n'
+    in
+        dec' None n
+    end
+
+fun render [ctx] [inp] [[Body] ~ ctx] (xml : xml ([Body] ++ ctx) inp []) n =
+    let
+        fun render n =
+            n <- signal n;
+            return (render' n)
+
+        and render' n =
+            case n of
+                O => <xml/>
+              | S n => <xml>
+                {xml}
+                <dyn signal={render n}/>
+              </xml>
+    in
+        <xml><dyn signal={render n}/></xml>
+    end