view demo/more/dlist.ur @ 952:07569af40069

Insert dummy Sort parameter
author Adam Chlipala <adamc@hcoop.net>
date Thu, 17 Sep 2009 14:42:02 -0400
parents 103ac1792c41
children 301530da2062
line wrap: on
line source
datatype dlist'' t =
         Nil
       | Cons of t * source (dlist'' t)

datatype dlist' t =
         Empty
       | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) }

con dlist t = source (dlist' t)

type position = transaction unit

fun headPos [t] (dl : dlist t) =
    dl' <- get dl;
    case dl' of
        Nonempty { Head = Cons (_, tl), Tail = tl' } =>
        cur <- get tl;
        set dl (case cur of
                    Nil => Empty
                  | _ => Nonempty {Head = cur, Tail = tl'})
      | _ => return ()

fun tailPos [t] (cur : source (dlist'' t)) new tail =
    new' <- get new;
    set cur new';

    case new' of
        Nil => set tail cur
      | _ => return ()

val create [t] = source Empty

fun clear [t] (s : dlist t) = set s Empty

fun append [t] dl v =
    dl' <- get dl;
    case dl' of
        Empty =>
        tl <- source Nil;
        tl' <- source tl;
        set dl (Nonempty {Head = Cons (v, tl), Tail = tl'});
        return (headPos dl)
                
      | Nonempty {Tail = tl, ...} =>
        cur <- get tl;
        new <- source Nil;
        set cur (Cons (v, new));
        set tl new;
        return (tailPos cur new tl)

fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter dl = <xml>
  <dyn signal={dl' <- signal dl;
               return (case dl' of
                           Empty => <xml/>
                         | Nonempty {Head = hd, Tail = tlTop} => 
                           let
                               fun render' prev dl'' =
                                   case dl'' of
                                       Nil => <xml/>
                                     | Cons (v, tl) =>
                                       let
                                           val pos = case prev of
                                                         None => headPos dl
                                                       | Some prev => tailPos prev tl tlTop
                                       in
                                           <xml><dyn signal={b <- filter v;
                                                             return (if b then
                                                                         f v pos
                                                                     else
                                                                         <xml/>)}/>
                                             <dyn signal={tl' <- signal tl;
                                                          return (render' (Some tl) tl')}/></xml>
                                       end
                           in
                               render' None hd
                           end)}/>
</xml>

fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls =
    List.mapX (fn p => f p.1 p.2) ls

fun render [ctx] [ctx ~ body] [t] f r dl = <xml>
    <dyn signal={sort <- r.Sort;
                 case sort of
                     None => return (renderDyn f r.Filter dl)
                   | Some sort =>
                     dl' <- signal dl;
                     elems <- (case dl' of
                                   Empty => return []
                                 | Nonempty {Head = hd, Tail = tlTop} =>
                                   let
                                       fun listOut prev dl'' acc =
                                           case dl'' of
                                               Nil => return acc
                                             | Cons (v, tl) =>
                                               let
                                                   val pos = case prev of
                                                                 None => headPos dl
                                                               | Some prev => tailPos prev tl tlTop
                                               in
                                                   tl' <- signal tl;
                                                   listOut (Some tl) tl' ((v, pos) :: acc)
                                               end
                                   in
                                       listOut None hd []
                                   end);
                     return (renderFlat f r.Filter elems)}/>
</xml>
                             
        

fun delete pos = pos

fun elements' [t] (dl'' : dlist'' t) =
    case dl'' of
        Nil => return []
      | Cons (x, dl'') =>
        dl'' <- signal dl'';
        tl <- elements' dl'';
        return (x :: tl)

fun elements [t] (dl : dlist t) =
    dl' <- signal dl;
    case dl' of
        Empty => return []
      | Nonempty {Head = hd, ...} => elements' hd

fun foldl [t] [acc] (f : t -> acc -> signal acc) =
    let
        fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
            case dl of
                Nil => return i
              | Cons (v, dl') =>
                dl' <- signal dl';
                i' <- f v i;
                foldl'' i' dl'

        fun foldl' (i : acc) (dl : dlist t) : signal acc =
            dl <- signal dl;
            case dl of
                Empty => return i
              | Nonempty {Head = dl, ...} => foldl'' i dl
    in
        foldl'
    end