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 module type Elem = sig type t val pp : t -> string end ;;
16 module type ZipTree = sig
18 type tree = Node of (t * tree) list
21 val start : tree -> position
23 val up : position -> position option
24 val down : position -> position option
25 val left : position -> position option
26 val right : position -> position option
28 val root: position -> tree
29 val previsit: ('a -> t -> 'a) -> 'a -> position -> 'a
31 val get: position -> t
32 val set: t -> position -> position
34 val inject: tree -> position -> position
35 val eject: position -> tree
39 let rec repeat f l = match f l with None -> l | Some l -> repeat f l;;
41 module Make(T : Elem) = struct
45 type tree = Node of (T.t * tree) list
48 | Ctx of tree_ctx * (T.t * tree) list * T.t * (T.t * tree) list
51 type position = Loc of tree_ctx * tree
53 let start (t : tree) : position = Loc (Top, t);;
56 | Loc (_,Node []) -> None
57 | Loc (ctx, Node ((x,t)::tl)) -> Some (Loc (Ctx (ctx,[],x,tl),t))
62 | Loc (Ctx(ctx,l,x,r),t) -> Some (Loc (ctx,Node (l@[x,t]@r)))
66 | Loc (Top,_) | Loc (Ctx(_,_,_,[]),_) -> None
67 | Loc (Ctx(ctx,l,x,(rx,rt)::tl),t) -> Some (Loc(Ctx(ctx,l@[x,t],rx,tl),rt))
71 | Loc (Top,_) | Loc (Ctx(_,[],_,_),_) -> None
72 | Loc (Ctx(ctx,(lx,lt)::tl,x,r),t) -> Some (Loc(Ctx(ctx,tl,lx,(x,t)::r),lt))
76 | Loc(Top,_) -> assert false
77 | Loc(Ctx(_,_,x,_),_) -> x
81 | Loc(Top,_) -> assert false
82 | Loc(Ctx(c,l,_,r),t) -> Loc(Ctx(c,l,x,r),t)
86 match repeat up t with
91 let eject (Loc (_,t)) = t ;;
93 let inject t (Loc (c,_)) = Loc(c,t) ;;
95 let previsit f acc (p : position) =
96 let rec aux acc = function
99 let acc = aux acc t in