2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
14 val repeat : ('a -> 'a option) -> 'a -> 'a
16 module type Elem = sig type t val pp : t -> string end ;;
18 module type ZipTree = sig
20 type tree = Node of (t * tree) list
23 val start : tree -> position
25 val up : position -> position option
26 val down : position -> position option
27 val left : position -> position option
28 val right : position -> position option
30 val root: position -> tree
31 val previsit: ('a -> t -> 'a) -> 'a -> position -> 'a
33 val get: position -> t
34 val set: t -> position -> position
36 val inject: tree -> position -> position
37 val eject: position -> tree
41 module Make(T : Elem) : ZipTree with type t = T.t