adamc@915: datatype dlist'' t = adamc@915: Nil adamc@915: | Cons of t * source (dlist'' t) adamc@915: adamc@915: datatype dlist' t = adamc@915: Empty adamc@915: | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) } adamc@915: adamc@915: con dlist t = source (dlist' t) adamc@915: adamc@915: type position = transaction unit adamc@915: adamc@915: fun headPos [t] (dl : dlist t) = adamc@915: dl' <- get dl; adamc@915: case dl' of adamc@915: Nonempty { Head = Cons (_, tl), Tail = tl' } => adamc@915: cur <- get tl; adamc@915: set dl (case cur of adamc@915: Nil => Empty adamc@915: | _ => Nonempty {Head = cur, Tail = tl'}) adamc@915: | _ => return () adamc@915: adamc@915: fun tailPos [t] (cur : source (dlist'' t)) new tail = adamc@915: new' <- get new; adamc@915: set cur new'; adamc@915: adamc@915: case new' of adamc@915: Nil => set tail cur adamc@915: | _ => return () adamc@915: adamc@915: val create = fn [t] => source Empty adamc@915: adamc@915: fun clear [t] (s : dlist t) = set s Empty adamc@915: adamc@915: fun append [t] dl v = adamc@915: dl' <- get dl; adamc@915: case dl' of adamc@915: Empty => adamc@915: tl <- source Nil; adamc@915: tl' <- source tl; adamc@915: set dl (Nonempty {Head = Cons (v, tl), Tail = tl'}); adamc@915: return (headPos dl) adamc@915: adamc@915: | Nonempty {Tail = tl, ...} => adamc@915: cur <- get tl; adamc@915: new <- source Nil; adamc@915: set cur (Cons (v, new)); adamc@915: set tl new; adamc@915: return (tailPos cur new tl) adamc@915: adamc@915: fun render [ctx] [ctx ~ body] [t] f dl = adamc@915: adamc@915: | Nonempty {Head = hd, Tail = tlTop} => adamc@915: let adamc@915: fun render' prev dl'' = adamc@915: case dl'' of adamc@915: Nil => adamc@915: | Cons (v, tl) => adamc@915: let adamc@915: val pos = case prev of adamc@915: None => headPos dl adamc@915: | Some prev => tailPos prev tl tlTop adamc@915: in adamc@915: {f v pos} adamc@915: end adamc@915: in adamc@915: render' None hd adamc@915: end)}/> adamc@915: adamc@915: adamc@915: fun delete pos = pos adamc@915: adamc@915: fun elements' [t] (dl'' : dlist'' t) = adamc@915: case dl'' of adamc@915: Nil => return [] adamc@915: | Cons (x, dl'') => adamc@915: dl'' <- signal dl''; adamc@915: tl <- elements' dl''; adamc@915: return (x :: tl) adamc@915: adamc@915: fun elements [t] (dl : dlist t) = adamc@915: dl' <- signal dl; adamc@915: case dl' of adamc@915: Empty => return [] adamc@915: | Nonempty {Head = hd, ...} => elements' hd adamc@937: adamc@937: fun foldl [t] [acc] (f : t -> acc -> signal acc) = adamc@937: let adamc@937: fun foldl'' (i : acc) (dl : dlist'' t) : signal acc = adamc@937: case dl of adamc@937: Nil => return i adamc@937: | Cons (v, dl') => adamc@937: dl' <- signal dl'; adamc@937: i' <- f v i; adamc@937: foldl'' i' dl' adamc@937: adamc@937: fun foldl' (i : acc) (dl : dlist t) : signal acc = adamc@937: dl <- signal dl; adamc@937: case dl of adamc@937: Empty => return i adamc@937: | Nonempty {Head = dl, ...} => foldl'' i dl adamc@937: in adamc@937: foldl' adamc@937: end