view demo/more/dnat.ur @ 1034:a779402841f6

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
line wrap: on
line source
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